User-defined constraints are defined by constraint handling rules - and optional ECLiPSe clauses for the built-in labeling feature. The constraints must be declared before they are defined. A CHR program (file extension chr) may also include other declarations, options and arbitrary ECLiPSe clauses.
| Program | ::= | Statement [ Program ] |
| Statement | ::= | Declaration | Option | Rule | Clause |
Constraint handling rules involving the same constraint can be scattered across a file as long as they are in the same module and compiled together. For readability declarations and options should precede rules and clauses.
In the following subsections, we introduce constraint handling rules and explain how they work. The next section describes declarations, clauses, options and built-in predicates for CHRs.
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 9.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 <=> \+nonground(X),\+nonground(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.
ECLiPSe will first solve the built-in constraints, then user-defined constraints by CHRs then the other goals.
Example, contd.:
[eclipse]: chr(minmax). minmax.chr compiled traceable 106874 bytes in 3.37 seconds minmax.pl compiled traceable 124980 bytes in 1.83 seconds yes. [eclipse]: minimum(X,Y,Z), maximum(X,Y,Z). X = Y = Z = _g496 yes.
Each user-defined constraint is associated with all rules in whose heads it occurs by the CHR compiler. Every time a user-defined constraint goal is added or re-activated, it checks itself the applicability of its associated CHRs by trying each CHR. To try a CHR, one of its heads is matched against the constraint goal. If a CHR has two heads, the constraint store is searched for a “partner” constraint that matches the other head. If the matching succeeded, the guard is executed as a test. Otherwise the rule delays and the next rule is tried.
The guard either succeeds, fails or delays. If the guard succeeds, the rule fires. Otherwise the rule delays and the next rule is tried. In the current implementation, a guard succeeds if its execution succeeds without delayed goals and attempts to “touch” a global variable (one that occurs in the heads). A variable is touched if it is unified with a term (including other variables), if it gets more constrained by built-in constraints (e.g. finite domains or equations over rationals) or if a goal delays on it (see also the check_guard_bindings option). Currently, built-in constraints used in a guard act as tests only (see also the section on writing good CHR programs).
If the firing CHR is a simplification rule, the matched constraint goals are removed and the body of the CHR is executed. Similarly for a firing simpagation rule, except that the first head is kept. If the firing CHR is a propagation rule the body of the CHR is executed and the next rule is tried. It is remembered that the propagation rule fired, so it will not fire again (with the same partner constraint) if the constraint goal is re-activated.
If the constraint goal has not been removed and all rules have been tried, it delays until a variable occurring in the constraint is touched. Then the constraint is re-activated and all its rules are tried again.
Example, contd.: The following trace is edited, rules that are tried in vain and redelay have been removed.
[eclipse]: chr_trace. yes. Debugger switched on - creep mode [eclipse]: notrace. % trace only constraints Debugger switched off yes. [eclipse]: minimum(X,Y,Z), maximum(X,Y,Z). ADD (1) minimum(X, Y, Z) TRY (1) minimum(_g218, _g220, _g222) with propagation RULE 'propagation' FIRED ADD (2) leq(_g665, _g601) ADD (3) leq(_g665, Var) ADD (4) maximum(_g601, Var, _g665) TRY (4) maximum(_g601, Var, _g665) with propagation RULE 'propagation' FIRED ADD (5) leq(_g601, _g665) TRY (5) leq(_g601, _g665) (2) leq(_g665, _g601) with antisymmetry RULE 'antisymmetry' FIRED TRY (4) maximum(_g601, Var, _g601) with max_eq RULE 'max_eq' FIRED ADD (6) leq(Var, _g601) TRY (3) leq(_g601, Var) (6) leq(Var, _g601) with antisymmetry RULE 'antisymmetry' FIRED TRY (1) minimum(_g601, _g601, _g601) with min_eq RULE 'min_eq' FIRED ADD (7) leq(_g601, _g601) TRY (7) leq(_g601, _g601) with reflexivity RULE 'reflexivity' FIRED X = Y = Z = _g558 yes.