@chapter CHR: Constraint Handling Rules 
@c 		\label{sec:chr}

This chapter is written by Tom Schrijvers, K.U. Leuven for the hProlog
system. Adjusted by Jan Wielemaker to fit the SWI-Prolog documentation
infrastructure and remove hProlog specific references.

The CHR system of SWI-Prolog is the K.U.Leuven CHR system.  The runtime
environment is written by Christian Holzbaur and Tom Schrijvers while the
compiler is written by Tom Schrijvers. Both are integrated with SWI-Prolog
and licenced under compatible conditions with permission from the authors.

The main reference for SWI-Prolog's CHR system is:
@itemize
@item T. Schrijvers, and B. Demoen, @emph{The K.U.Leuven CHR System: Implementation
and Application}, First Workshop on Constraint Handling Rules: Selected
Contributions (Fruwirth, T. and Meister, M., eds.), pp. 1--5, 2004.
@end itemize

@node CHR Introduction, CHR Syntax and Semantics, , CHR
@section Introduction
@c =====================

Constraint Handling Rules (CHR) is a committed-choice bottom-up language
embedded in Prolog. It is designed for writing constraint solvers and is
particularily useful for providing application-specific constraints.
It has been used in many kinds of applications, like scheduling,
model checking, abduction, type checking among many others.

CHR has previously been implemented in other Prolog systems (SICStus,
Eclipse, Yap), Haskell and Java. This CHR system is based on the
compilation scheme and runtime environment of CHR in SICStus.

In this documentation we restrict ourselves to giving a short overview
of CHR in general and mainly focus on elements specific to this
implementation. For a more thorough review of CHR we refer the reader to
[Freuhwirth:98]. More background on CHR can be found at the CHR web site.

@c \secref{SyntaxAndSemantics} we present the syntax of CHR in Prolog and
@c explain informally its operational semantics. Next, \secref{practical}
@c deals with practical issues of writing and compiling hProlog programs
@c containing CHR. \Secref{debugging} explains the currently primitive CHR
@c debugging facilities. \Secref{predicates} provides a few useful predicates
@c to inspect the constraint store and \secref{examples} illustrates CHR with
@c two example programs. In \secref{sicstus-chr} some compatibility issues with
@c SICStus CHR are listed. Finally, \secref{guidelines} concludes with a few
@c practical guidelines for using CHR.


@node CHR Syntax and Semantics, CHR in YAP Programs, CHR Introduction, CHR
@section Syntax and Semantics
@c		\label{sec:SyntaxAndSemantics}
@c=============================

@subsection Syntax
@c -----------------

The syntax of CHR rules in hProlog is the following:

@example
rules --> rule, rules.
rules --> [].

rule --> name, actual_rule, pragma, [atom('.')].

name --> atom, [atom('@')].
name --> [].

actual_rule --> simplification_rule.
actual_rule --> propagation_rule.
actual_rule --> simpagation_rule.

simplification_rule --> constraints, [atom('<=>')], guard, body.
propagation_rule --> constraints, [atom('==>')], guard, body.
simpagation_rule --> constraints, [atom('\')], constraints, [atom('<=>')], 
                     guard, body.

constraints --> constraint, constraint_id.
constraints --> constraint, [atom(',')], constraints.

constraint --> compound_term.

constraint_id --> [].
constraint_id --> [atom('#')], variable.

guard --> [].
guard --> goal, [atom('|')].

body --> goal.

pragma --> [].
pragma --> [atom('pragma')], actual_pragmas.

actual_pragmas --> actual_pragma.
actual_pragmas --> actual_pragma, [atom(',')], actual_pragmas.

actual_pragma --> [atom('passive(')], variable, [atom(')')].

@end example

Additional syntax-related terminology:

@itemize
@item @strong{head:} the constraints in an @code{actual_rule} before
                     the arrow (either @code{<=>} or @code{==>})
@end itemize

@subsection Semantics
@c --------------------

In this subsection the operational semantics of CHR in Prolog are presented
informally. They do not differ essentially from other CHR systems.

When a constraint is called, it is considered an active constraint and
the system will try to apply the rules to it. Rules are tried and executed
sequentially in the order they are written. 

A rule is conceptually tried for an active constraint in the following
way. The active constraint is matched with a constraint in the head of
the rule. If more constraints appear in the head they are looked for
among the suspended constraints, which are called passive constraints in
this context. If the necessary passive constraints can be found and all
match with the head of the rule and the guard of the rule succeeds, then
the rule is committed and the body of the rule executed. If not all the
necessary passive constraint can be found, the matching fails or the
guard fails, then the body is not executed and the process of trying and
executing simply continues with the following rules. If for a rule,
there are multiple constraints in the head, the active constraint will
try the rule sequentially multiple times, each time trying to match with
another constraint.

This process ends either when the active constraint disappears, i.e. it
is removed by some rule, or after the last rule has been processed. In
the latter case the active constraint becomes suspended.

A suspended constraint is eligible as a passive constraint for an active
constraint. The other way it may interact again with the rules, is when
a variable appearing in the constraint becomes bound to either a nonvariable
or another variable involved in one or more constraints. In that case the
constraint is triggered, i.e. it becomes an active constraint and all
the rules are tried.

@unnumberedsubsubsec Rule Types
@c - - - - - - - - - - 

There are three different kinds of rules, each with their specific semantics:

@table @code
@item simplification
The simplification rule removes the constraints in its head and calls its body.

@item propagation
The propagation rule calls its body exactly once for the constraints in
its head.

@item simpagation
The simpagation rule removes the constraints in its head after the
@code{\} and then calls its body. It is an optimization of
simplification rules of the form: \[constraints_1, constraints_2 <=>
constraints_1, body \] Namely, in the simpagation form: 

@example
constraints1 \ constraints2 <=> body
@end example
@noindent
@var{constraints1}
constraints are not called in the body.
@end table

@unnumberedsubsubsec Rule Names
@c - - - - - - - - - - 
Naming a rule is optional and has no semantical meaning. It only functions
as documentation for the programmer.

@unnumberedsubsubsec Pragmas
@c - - - - - - - - -
The semantics of the pragmas are:

@table @option
@item passive(Identifier)
The constraint in the head of a rule @var{Identifier} can only act as a
passive constraint in that rule.
@end table

Additional pragmas may be released in the future.

@unnumberedsubsubsec Options
@c - - - - - - - - -
It is possible to specify options that apply to all the CHR rules in the module.
Options are specified with the @code{option/2} declaration:

@example
                option(Option,Value).
@end example

Available options are:
@table @code
        @item check_guard_bindings
This option controls whether guards should be checked for illegal
variable bindings or not. Possible values for this option are
@code{on}, to enable the checks, and @code{off}, to disable the
checks.

        @item optimize
This is an experimental option controlling the degree of optimization.
Possible values are @code{full}, to enable all available
optimizations, and @code{off} (default), to disable all optimizations.  
The default is derived from the SWI-Prolog flag @code{optimise}, where
@code{true} is mapped to @code{full}.  Therefore the commandline
option @option{-O} provides full CHR optimization.
If optimization is enabled, debugging should be disabled.

	@item debug
This options enables or disables the possibility to debug the CHR code.
Possible values are @code{on} (default) and @code{off}. See
@option{debugging} for more details on debugging.  The default is
derived from the prolog flag @code{generate_debug_info}, which
is @code{true} by default.  See @option{-nodebug}.
If debugging is enabled, optimization should be disabled.

	@item mode
This option specifies the mode for a particular constraint. The
value is a term with functor and arity equal to that of a constraint.
The arguments can be one of @code{-}, @code{+} or @code{?}.
The latter is the default. The meaning is the following:
	@table @code
	@item -
         The corresponding argument of every occurrence
	of the constraint is always unbound.
	@item + 
        The corresponding argument of every occurrence
	of the constraint is always ground.
	@item ?
         The corresponding argument of every occurrence
	of the constraint can have any instantiation, which may change
	over time. This is the default value.
	@end table
The declaration is used by the compiler for various optimizations. 
Note that it is up to the user the ensure that the mode declaration
is correct with respect to the use of the constraint.
This option may occur once for each constraint.

	@item type_declaration
This option specifies the argument types for a particular constraint. The
value is a term with functor and arity equal to that of a constraint.
The arguments can be a user-defined type or one of
the built-in types:
    @table @code
	@item int
         The corresponding argument of every occurrence
	of the constraint is an integer number.
	@item float
         @dots{} a floating point number.
	@item number
         @dots{} a number.
	@item natural
         @dots{} a positive integer.
	@item any
         The corresponding argument of every occurrence
	of the constraint can have any type. This is the default value.
   @end table

Currently, type declarations are only used to improve certain
optimizations (guard simplification, occurrence subsumption, @dots{}).

	@item type_definition
This option defines a new user-defined type which can be used in
type declarations. The value is a term of the form
@code{type(}@var{name}@code{,}@var{list}@code{)}, where
@var{name} is a term and @var{list} is a list of alternatives.
Variables can be used to define generic types. Recursive definitions
are allowed. Examples are 

@example
type(bool,[true,false]).
type(complex_number,[float + float * i]).
type(binary_tree(T),[ leaf(T) | node(binary_tree(T),binary_tree(T)) ]).
type(list(T),[ [] | [T | list(T)]).
@end example


@end table

The mode, type_declaration and type_definition options are provided
for backward compatibility. The new syntax is described below.

@node CHR in YAP Programs, CHR Debugging, CHR Syntax and Semantics, CHR
@section CHR in YAP Programs	
@c	\label{sec:practical}
@c===========================


@subsection Embedding in Prolog Programs

The CHR constraints defined in a particulary @file{chr} file are
associated with a module. The default module is @code{user}. One should
never load different @file{chr} files with the same CHR module name.

@subsection Constraint declaration

Every constraint used in CHR rules has to be declared.
There are two ways to do this. The old style is as follows:

@example
option(type_definition,type(list(T),[ [] , [T|list(T)] ]).
option(mode,foo(+,?)).
option(type_declaration,foo(list(int),float)).
:- constraints foo/2, bar/0.
@end example

The new style is as follows:

@example
:- chr_type list(T) ---> [] ; [T|list(T)].
:- constraints foo(+list(int),?float), bar.
@end example


@subsection Compilation

The SWI-Prolog CHR compiler exploits term_expansion/2 rules to translate
the constraint handling rules to plain Prolog. These rules are loaded
from the library @file{chr}.   They are activated if the compiled file
has the @file{chr} extension or after finding a declaration of the
format below.

@example
:- constraints ...
@end example

It is adviced to define CHR rules in a module file, where the module
declaration is immediately followed by including the @file{chr}
library as examplified below:

@example
:- module(zebra, [ zebra/0 ]).
:- use_module(library(chr)).

:- constraints ...
@end example

Using this style CHR rules can be defined in ordinary Prolog
@file{pl} files and the operator definitions required by CHR do not
leak into modules where they might cause conflicts.


@node CHR Debugging, CHR Examples,CHR in YAP Programs, CHR
@section Debugging
@c			\label{sec:debugging}
@c=================

The CHR debugging facilities are currently rather limited. Only tracing
is currently available. To use the CHR debugging facilities for a CHR
file it must be compiled for debugging. Generating debug info is
controlled by the CHR option @code{debug}, whose default is derived
from the SWI-Prolog flag @code{generate_debug_info}.  Therefore debug
info is provided unless the @option{-nodebug} is used.


@subsection Ports
@c				\label{sec:chrports
@c===============

For CHR constraints the four standard ports are defined:

@table @code
	@item call
A new constraint is called and becomes active.
	@item exit
An active constraint exits: it has either been inserted in the store after
trying all rules or has been removed from the constraint store.
	@item fail
An active constraint fails.
	@item redo
An active constraint starts looking for an alternative solution.
@end table

In addition to the above ports, CHR constraints have five additional
ports:

@table @code
@item wake
A suspended constraint is woken and becomes active.
@item insert
An active constraint has tried all rules and is suspended in
the constraint store.
@item remove
An active or passive constraint is removed from the constraint
store, if it had been inserted.
@item try
	An active constraints tries a rule with possibly
	some passive constraints. The try port is entered
	just before committing to the rule.
@item apply
	An active constraints commits to a rule with possibly
	some passive constraints. The apply port is entered
	just after committing to the rule.
@end table

@subsection Tracing
@c=================

Tracing is enabled with the chr_trace/0 predicate
and disabled with the chr_notrace/0 predicate.

When enabled the tracer will step through the @code{call},
@code{exit}, @code{fail}, @code{wake} and @code{apply} ports,
accepting debug commands, and simply write out the other ports.

The following debug commans are currently supported:

@example
        CHR debug options:

                <cr>    creep           c       creep
		s	skip
		g	ancestors
                n       nodebug
		b	break
                a       abort
                f       fail
                ?       help            h       help
@end example

Their meaning is:

@table @code
@item creep
Step to the next port.
@item skip
Skip to exit port of this call or wake port.
@item ancestors
Print list of ancestor call and wake ports.
@item nodebug
Disable the tracer.
@item break
Enter a recursive Prolog toplevel.  See break/0.
@item abort
Exit to the toplevel.  See abort/0.
@item fail
Insert failure in execution.
@item help
Print the above available debug options.
@end table

@subsection CHR Debugging Predicates
@c 		\label{sec:predicates
@c====================================

The @file{chr} module contains several predicates that allow
inspecting and printing the content of the constraint store.

@table @code
    @item chr_trace/0
Activate the CHR tracer.  By default the CHR tracer is activated and
deactivated automatically by the Prolog predicates trace/0 and
notrace/0.

    @item chr_notrace/0
De-activate the CHR tracer.  By default the CHR tracer is activated and
deactivated automatically by the Prolog predicates trace/0 and
notrace/0.
    
    @item chr_leash/0 

Define the set of CHR ports on which the CHR
tracer asks for user intervention (i.e. stops). @var{Spec} is either a
list of ports or a predefined `alias'. Defined aliases are:
@code{full} to stop at all ports, @code{none} or @code{off} to never
stop, and @code{default} to stop at the @code{call}, @code{exit},
@code{fail}, @code{wake} and @code{apply} ports.  See also leash/1.

    @item chr_show_store(+@var{Mod})
Prints all suspended constraints of module @var{Mod} to the standard
output. This predicate is automatically called by the SWI-Prolog toplevel at
the end of each query for every CHR module currently loaded.  The prolog-flag
@code{chr_toplevel_show_store} controls whether the toplevel shows the
constraint stores. The value @code{true} enables it.  Any other value
disables it.


@end table


@node CHR Examples, CHR Compatibility,CHR Debugging, CHR
@section Examples
@c			\label{sec:examples}
@c================

Here are two example constraint solvers written in CHR.

@itemize
 @item
The program below defines a solver with one constraint, 
@code{leq/2}, which is a less-than-or-equal constraint.

@example
:- module(leq,[cycle/3, leq/2]).
:- use_module(library(chr)).

:- constraints leq/2.
reflexivity  @ leq(X,X) <=> true.
antisymmetry @ leq(X,Y), leq(Y,X) <=> X = Y.
idempotence  @ leq(X,Y) \ leq(X,Y) <=> true.
transitivity @ leq(X,Y), leq(Y,Z) ==> leq(X,Z).

cycle(X,Y,Z):-
        leq(X,Y),
        leq(Y,Z),
        leq(Z,X).
@end example

    @item
The program below implements a simple finite domain
constraint solver.

@example
:- module(dom,[dom/2]).
:- use_module(library(chr)).

:- constraints dom/2. 

dom(X,[]) <=> fail.
dom(X,[Y]) <=> X = Y.
dom(X,L1), dom(X,L2) <=> intersection(L1,L2,L3), dom(X,L3).

intersection([],_,[]).
intersection([H|T],L2,[H|L3]) :-
        member(H,L2), !,
        intersection(T,L2,L3).
intersection([_|T],L2,L3) :-
        intersection(T,L2,L3).
@end example
		
@end itemize

@node CHR Compatibility, CHR Guidelines,CHR Examples, CHR
@section Compatibility with SICStus CHR
@c 		\label{sec:sicstus-chr}
@c==================

There are small differences between CHR in SWI-Prolog and newer
YAPs and SICStus and older versions of YAP.  Besides differences in
available options and pragmas, the following differences should be
noted:

@table @code
        @item [The handler/1 declaration]
In SICStus every CHR module requires a @code{handler/1}
declaration declaring a unique handler name. This declaration is valid
syntax in SWI-Prolog, but will have no effect. A warning will be given
during compilation.

        @item [The rules/1 declaration]
In SICStus, for every CHR module it is possible to only enable a subset
of the available rules through the @code{rules/1} declaration. The
declaration is valid syntax in SWI-Prolog, but has no effect. A
warning is given during compilation.

	@item [Sourcefile naming]
SICStus uses a two-step compiler, where @file{chr} files are
first translated into @file{pl} files.  For SWI-Prolog CHR
rules may be defined in a file with any extension.
@end table


@node CHR Guidelines, ,CHR Compatibility, CHR
@section Guidelines
@c 			\label{sec:guidelines}
@c ==================

In this section we cover several guidelines on how to use CHR to write
constraint solvers and how to do so efficiently.

@table @code
    @item [Set semantics]
The CHR system allows the presence of identical constraints, i.e.
multiple constraints with the same functor, arity and arguments. For
most constraint solvers, this is not desirable: it affects efficiency
and possibly termination. Hence appropriate simpagation rules should be
added of the form:

@example
@{constraint \ constraint <=> true@}.
@end example

    @item [Multi-headed rules]
Multi-headed rules are executed more efficiently when the constraints
share one or more variables.

    @item [Mode and type declarations]
Provide mode and type declarations to get more efficient program execution.
Make sure to disable debug (@option{-nodebug}) and enable optimization
(@option{-O}).
@end table