Constraint Handling Rules

A constraint handling rule has one or two heads, an optional guard, a body and an optional name. A ``Head'' is a ``Constraint''. A ``Constraint'' is an ECLiPSe callable term (i.e. atom or structure) whose functor is a declared constraint. A ``Guard''  is an ECLiPSe goal. The guard is a test on the applicability of a rule. The ``Body'' of a rule is an ECLiPSe goal (including constraints). The execution of the guard and the body should not involve side-effects (like assert/1, write/1) (for more information see the section on writing CHR programs). A rule can be named with a ``RuleName'' which can be any ECLiPSe term (including variables from the rule). During debugging (see section 5.8), this name will be displayed instead of the whole rule.

There are three kinds of constraint handling rules.

Rule  ::=  SimplificationRule |  PropagationRule |  SimpagationRule

SimplificationRule  ::=  [ RuleName @ ] Head [ , Head ] <=> [Guard |] Body.

PropagationRule  ::=  [ RuleName @ ] Head [ , Head ] ==> [Guard |] Body.

SimpagationRule  ::=  [ RuleName @ ] Head \ Head <=> [Guard |] Body.

Declaratively, a rule relates heads and body provided the guard is true. A simplification rule  means that the heads are true if and only if the body is true. A propagation rule  means that the body is true if the heads are true. A simpagation rule  is a combination of a simplification and propagation rule. The rule ``Head1 \ Head2 <=> Body'' is equivalent to the simplification rule ``Head1 , Head2 <=> Body, Head1.'' However, the simpagation rule is more compact to write, more efficient to execute and has better termination behavior than the corresponding simplification rule.

Example: Assume you want to write a constraint handler for minimum and maximum based on inequality constraints. The complete code can be found in the handler file minmax.chr.

 handler minmax.

constraints leq/2, neq/2, minimum/3, maximum/3.
built_in     @ X leq Y <=> ground(X),ground(Y) | X @=< Y.
reflexivity  @ X leq X <=> true.
antisymmetry @ X leq Y, Y leq X <=> X = Y.
transitivity @ X leq Y, Y leq Z ==> X \== Y, Y \== Z, X \== Z | X leq Z.
...
built_in     @ X neq Y <=> X ~= Y | true.
irreflexivity@ X neq X <=> fail. 
...
subsumption  @ X lss Y \ X neq Y <=> true.
simplification @ X neq Y, X leq Y <=> X lss Y. 
...
min_eq @ minimum(X, X, Y) <=> X = Y.
min_eq @ minimum(X, Y, X) <=> X leq Y.
min_eq @ minimum(X, Y, Y) <=> Y leq X.
...
propagation @ minimum(X, Y, Z) ==> Z leq X, Z leq Y.
...

Procedurally, a rule can fire only if its guard succeeds. A firing simplification rule replaces the head constraints by the body constraints, a firing propagation rule keeps the head constraints and adds the body. A firing simpagation rule keeps the first head and replaces the second head by the body. See the next subsection for more details.