Constraint Handling Rules were originally implemented in ECLiPSe. They are introduced in the paper [9].
CHR’s offer a rule-based programming style to express constraint simplification and constraint propagation. The rules all have a head, an explicit or implicit guard, and a body, and are written either
Head <=> Guard | Body. %Simplification Rule
or
Head ==> Guard | Body. %Propagation Rule
When a constraint is posted that is an instance of the head, the guard is checked to determine whether the rule can fire. If the guard is satisfied (i.e. CHR detects that it is entailed by the current search state), the rule fires. Unlike ECLiPSe clauses, the rules leave no choice points. Thus if several rules share the same head and one fires, the other rules are never fired even after a failure.
Normally the guards exclude each other, as in the noclash
example:
:- lib(ech). :- constraints noclash/2. noclash(S1,S2) <=> ic:(S2 #< S1+5) | ic:(S1 #>= S2+5). noclash(S1,S2) <=> ic:(S1 #< S2+5) | ic:(S2 #>= S1+5). |
Henceforth we will not explicitly load the ech library.
The power of guards lies in the behaviour of the rules when they are neither entailed, nor disentailed. Thus in the query
?- ic:([S1,S2]::1..10), noclash(S1,S2), S1 #>= 6.
when the noclash
constraint is initially posted, neither guard
is entailed, and CHR simply postpones the handling of the constraint
until further constraints are posted.
As soon as a guard becomes entailed, however, the rule fires.
For simplification rules, of the form
Head <=> Guard | Body
,
the head is replaced by the body.
In this example, therefore, noclash(S1,S2)
is replaced by
S1 #>= S2+5
.
Propagation rules are useful to add constraints, instead of replacing them. Consider, for example, an application to temporal reasoning. If the time T1 is before time T2, then we can propagate an additional ic constraint saying T1 =< T2:
:- constraints before/2. before(T1,T2) ==> ic:(T1 $=< T2) |
This rule simply posts the constraint T1 $=< T2
to ic.
When a propagation rule fires its body is invoked, but its head
remains in the constraint store.
Sometimes different constraints interact, and more can be deduced from the combination of constraints than can be deduced from the constraints separately. Consider the following query:
?- ic:([S1,S2]::1..10), noclash(S1,S2), before(S1,S2).
Unfortunately the ic bounds are not tight enough for the
noclash
rule to fire.
The two constraints can be combined so as to propagate S2 ≥ S1+5
using a two-headed
CHR:
noclash(S1,S2), before(S1,S2) ==> ic:(S2 #>= S1+5).
We would prefer to write a set of rules that captured this kind of inference in a general way.
This can be achieved by writing a more complete solver for
prec
, and combining it with noclash
.
prec(S1,D,S2) holds if the time S1 precedes the time S2 by at
least D units of time.
For the following code to work, S1 and S2 may be numbers or
variables, but D must be a number.
:- constraints prec/3. prec(S,D,S) <=> D=<0. prec(S1,0,S2), prec(S2,0,S1) <=> S1=S2. prec(S1,D1,S2), prec(S2,D2,S3) ==> D3 is D1+D2, prec(S1,D3,S3). prec(S1,D1,S2) |
Note the simpagation rule, whose head has two parts
Head1 \ Head2
.
In a simpagation rule Head2
is replaced, but Head1
is
kept in the constraint store.
CHRs are guarded rules which fire without leaving choice points. A CHR rule may have one or many goals in the head, and may take the following forms: Simplification rule, Propagation rule or Simpagation rule.