Go to the first, previous, next, last section, table of contents.


Constraint Handling Rules

Copyright

This chapter is Copyright (C) 1996-98 LMU

LMU (Ludwig-Maximilians-University)
Munich, Germany

Permission is granted to make and distribute verbatim copies of this chapter provided the copyright notice and this permission notice are preserved on all copies.

Permission is granted to copy and distribute modified versions of this chapter under the conditions for verbatim copying, provided that the entire resulting derived work is distributed under the terms of a permission notice identical to this one.

Permission is granted to copy and distribute translations of this chapter into another language, under the above conditions for modified versions, except that this permission notice may be stated in a translation approved by LMU.

Introduction

Experience from real-life applications using constraint-based programming has shown that typically, one is confronted with a heterogeneous mix of different types of constraints. To be able to express constraints as they appear in the application and to write and combine constraint systems, a special purpose language for writing constraint systems called constraint handling rules (CHR) was developed. CHR have been used to encode a wide range of constraint handlers (solvers), including new domains such as terminological and temporal reasoning. Several CHR libraries exist in declarative languages such as Prolog and LISP, worldwide more than 20 projects use CHR. You can find more information about CHR at URL: http://www.pst.informatik.uni-muenchen.de/personen/fruehwir/chr-intro.html

The high-level CHR are an excellent tool for rapid prototyping and implementation of constraint handlers. The usual abstract formalism to describe a constraint system, i.e. inference rules, rewrite rules, sequents, formulas expressing axioms and theorems, can be written as CHR in a straightforward way. Starting from this executable specification, the rules can be refined and adapted to the specifics of the application.

The CHR library includes a compiler, which translates CHR programs into Prolog programs on the fly, and a runtime system, which includes a stepper for debugging. Many constraint handlers are provided in the example directory of the library.

CHR are essentially a committed-choice language consisting of guarded rules that rewrite constraints into simpler ones until they are solved. CHR define both simplification of and propagation over constraints. Simplification replaces constraints by simpler constraints while preserving logical equivalence (e.g. X>Y,Y>X <=> fail). Propagation adds new constraints which are logically redundant but may cause further simplification (e.g. X>Y,Y>Z ==> X>Z). Repeatedly applying CHR incrementally simplifies and finally solves constraints (e.g. A>B,B>C,C>A leads to fail.

With multiple heads and propagation rules, CHR provide two features which are essential for non-trivial constraint handling. The declarative reading of CHR as formulas of first order logic allows one to reason about their correctness. On the other hand, regarding CHR as a rewrite system on logical formulas allows one to reason about their termination and confluence.

In case the implementation of CHR disagrees with your expectations based on this chapter, drop a line to the current maintainer: christian@ai.univie.ac.at (Christian Holzbaur).

Introductory Examples

We define a CHR constraint for less-than-or-equal, leq, that can handle variable arguments. This handler can be found in the library as the file leq.pl. (The code works regardless of options switched on or off.)

:- use_module(library(chr)).

handler leq.
constraints leq/2.
:- op(500, xfx, leq).

reflexivity  @ X leq Y <=> X=Y | true.
antisymmetry @ X leq Y , Y leq X <=> X=Y.
idempotence  @ X leq Y \ X leq Y <=> true.
transitivity @ X leq Y , Y leq Z ==> X leq Z.

The CHR specify how leq simplifies and propagates as a constraint. They implement reflexivity, idempotence, antisymmetry and transitivity in a straightforward way. CHR reflexivity states that X leq Y simplifies to true, provided it is the case that X=Y. This test forms the (optional) guard of a rule, a precondition on the applicability of the rule. Hence, whenever we see a constraint of the form A leq A we can simplify it to true.

The rule antisymmetry means that if we find X leq Y as well as Y leq X in the constraint store, we can replace it by the logically equivalent X=Y. Note the different use of X=Y in the two rules: In the reflexivity rule the equality is a precondition (test) on the rule, while in the antisymmetry rule it is enforced when the rule fires. (The reflexivity rule could also have been written as reflexivity X leq X <=> true.)

The rules reflexivity and antisymmetry are simplification CHR. In such rules, the constraints found are removed when the rule applies and fires. The rule idempotence is a simpagation CHR, only the constraints right of '\' will be removed. The rule says that if we find X leq Y and another X leq Y in the constraint store, we can remove one.

Finally, the rule transitivity states that the conjunction X leq Y, Y leq Z implies X leq Z. Operationally, we add X leq Z as (redundant) constraint, without removing the constraints X leq Y, Y leq Z. This kind of CHR is called propagation CHR.

Propagation CHR are useful, as the query A leq B,C leq A,B leq C illustrates: The first two constraints cause CHR transitivity to fire and add C leq B to the query. This new constraint together with B leq C matches the head of CHR antisymmetry, X leq Y, Y leq X. So the two constraints are replaced by B=C. Since B=C makes B and C equivalent, CHR antisymmetry applies to the constraints A leq B, C leq A, resulting in A=B. The query contains no more CHR constraints, the simplification stops. The constraint handler we built has solved A leq B, C leq A, B leq C and produced the answer A=B, B=C:

A leq B,C leq A,B leq C. 
% C leq A, A leq B propagates C leq B by transitivity.
% C leq B, B leq C simplifies to B=C by antisymmetry.
% A leq B, C leq A simplifies to A=B by antisymmetry since B=C.
A=B,B=C.

Note that multiple heads of rules are essential in solving these constraints. Also note that this handler implements a (partial) order constraint over any constraint domain, this generality is only possible with CHR.

As another example, we can implement the sieve of Eratosthenes to compute primes simply as (for variations see the handler `primes.pl'):

:- use_module(library(chr)).
handler eratosthenes.
constraints primes/1,prime/1.

primes(1) <=> true.
primes(N) <=> N>1 | M is N-1,prime(N),primes(M). % generate candidates

absorb(J) @ prime(I) \ prime(J) <=> J mod I =:= 0 | true. 

The constraint primes(N) generates candidates for prime numbers, prime(M), where M is between 1 and N. The candidates react with each other such that each number absorbs multiples of itself. In the end, only prime numbers remain.

Looking at the two rules defining primes/1, note that head matching is used in CHR, so the first rule will only apply to primes(1). The test N>1 is a guard (precondition) on the second rule. A call with a free variable, like primes(X), will delay (suspend). The third, multi-headed rule absorb(J) reads as follows: If there is a constraint prime(I) and some other constraint prime(J) such that J mod I =:= 0 holds, i.e. J is a multiple of I, then keep prime(I) but remove prime(J) and execute the body of the rule, true.

CHR Library

CHR extend the Prolog syntax by a few constructs introduced in the next sections. Technically, the extension is achieved through the user:term_expansion/2 mechanism. A file that contains a constraint handler may also contain arbitrary Prolog code. Constraint handling rules can be scattered across a file. Declarations and options should precede rules. There can only be at most one constraint handler per module.

Loading the Library

Before you can load or compile any file containing a constraint handler (solver) written in CHR, the chr library module has to be imported:

| ?- use_module(library(chr)).

It is recommended to include the corresponding directive at the start of your files containing handlers:

  :- use_module(library(chr)).

Declarations

Declarations in files containing CHR affect the compilation and thus the behavior of the rules at runtime.

The mandatory handler declaration precedes any other CHR specific code. Example:

handler minmax.

A handler name must be a valid Prolog atom. Per module, only one constraint handler can be defined.

The constraints must be declared before they are used by rules. With this mandatory declaration one lists the constraints the rules will later talk about. The declaration can be used more than once per handler. Example:

constraints  leq/2, minimum/3, maximum/3.

The following optional declaration allows for conditional rule compilation. Only the rules mentioned get compiled. Rules are referred to by their names (see section Constraint Handling Rules, Syntax). The latest occurrence takes precedence if used more than once per handler. Although it can be put anywhere in the handler file, it makes sense, as with other declarations, to use it early. Example:

rules antisymmetry, transitivity.

To simplify the handling of operator declarations, in particular during fcompile/1, operator/3 declarations with the same denotation as op/3, but taking effect during compilation and loading, are helpful. Example:

operator(700, xfx, ::).
operator(600, xfx, :).

Constraint Handling Rules, Syntax

A constraint handling rule has one or more heads, an optional guard, a body and an optional name. A Head is a Constraint. A constraint is a callable Prolog term, whose functor is a declared constraint. The Guard is a Prolog goal. The Body of a rule is a Prolog goal (including constraints). A rule can be named with a Name which can be any Prolog term (including variables from the rule).

There are three kinds of constraint handling rules:

Rule           --> [Name @] 
                     (Simplification | Propagation | Simpagation) 
                        [pragma Pragma].

Simplification --> Heads         <=> [Guard '|'] Body
Propagation    --> Heads         ==> [Guard '|'] Body
Simpagation    --> Heads \ Heads <=> [Guard '|'] Body

Heads          --> Head | Head, Heads
Head           --> Constraint | Constraint # Id
Constraint     --> a callable term declared as constraint
Id             --> a unique variable

Guard          --> Ask | Ask & Tell
Ask            --> Goal
Tell           --> Goal
Goal           --> a callable term, including conjunction and disjunction etc.

Body           --> Goal

Pragma         --> a conjunction of terms usually referring to 
                   one or more heads identified via #/2

The symbol `|' separates the guard (if present) from the body of a rule. Since `|' is read as `;' (disjunction) by the reader, care has to be taken when using disjunction in the guard or body of the rule. The top level disjunction will always be interpreted as guard-body separator `|', so proper bracketing has to be used, e.g. a <=> (b;c) | (d;e) instead of a <=> b;c | d;e and a <=> true | (d;e) instead of a <=> (d;e).

In simpagation rules, `\' separates the heads of the rule into two parts.

Individual head constraints may be tagged with variables via `#', which may be used as identifiers in pragma declarations, for example. Constraint identifiers must be distinct variables, not occurring elsewhere in the heads.

Guards test the applicability of a rule. Guards come in two parts, tell and ask, separated by `&'. If the `&' operator is not present, the whole guard is assumed to be of the ask type.

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 combines a simplification and a propagation rule. The rule Heads1 \ Heads2 <=> Body is equivalent to the simplification rule Heads1, Heads2 <=> Heads1, Body. However, the simpagation rule is more compact to write, more efficient to execute and has better termination behavior than the corresponding simplification rule, since the constraints comprising Heads1 will not be removed and inserted again.

How CHR work

Each CHR constraint is associated with all rules in whose heads it occurs by the CHR compiler. Every time a CHR constraint is executed (called) or woken and reconsidered, it checks itself the applicability of its associated CHR by trying each CHR. By default, the rules are tried in textual order, i.e. in the order they occur in the defining file. To try a CHR, one of its heads is matched against the constraint. Matching succeeds if the constraint is an instance of the head. If a CHR has more than one head, the constraint store is searched for partner constraints that match the other heads. Heads are tried from left to right, except that in simpagation rules, the heads to be removed are tried before the head constraints to be kept (this is done for efficiency reasons). If the matching succeeds, the guard is executed. Otherwise the next rule is tried.

The guard either succeeds or fails. A guard succeeds if the execution of its Ask and Tell parts succeeds and in the ask part no variable that occurs also in the heads was touched or the cause of an instantiation error. The ask guard will fail otherwise. A variable is touched if it is unified with a term (including other variables from other constraints) different from itself. Tell guards, on the contrary, are trusted and not checked for that property. If the guard succeeds, the rule applies. Otherwise the next rule is tried.

If the firing CHR is a simplification rule, the matched constraints are removed from the store and the body of the CHR is executed. Similarly for a firing simpagation rule, except that the constraints that matched the heads preceding `\' are kept. If the firing CHR is a propagation rule the body of the CHR is executed without removing any constraints. It is remembered that the propagation rule fired, so it will not fire again with the same constraints if the constraint is woken and reconsidered. If the currently active constraint has not been removed, the next rule is tried.

If the current constraint has not been removed and all rules have been tried, it delays until a variable occurring in the constraint is touched. Delaying means that the constraint is inserted into the constraint store. When a constraint is woken, all its rules are tried again. (This process can be watched and inspected with the CHR debugger, see below.)

Pragmas

Pragmas are annotations to rules and constraints that enable the compiler to generate more specific, more optimized code. A pragma can be a conjunction of the following terms:

already_in_heads
The intention of simplification and simpagation rules is often to combine the heads into a stronger version of one of them. Depending on the strength of the guard, the new constraint may be identical to one of the heads to removed by the rule. This removal followed by addition is inefficient and may even cause termination problems. If the pragma is used, this situation is detected and the corresponding problems are avoided. The pragma applies to all constraints removed by the rule.
already_in_head(Id)
Shares the intention of the previous pragma, but affects only the constraint indicated via Id. Note that one can use more than one pragma per rule.
passive(Id)
No code will be generated for the specified constraint in the particular head position. This means that the constraint will not see the rule, it is passive in that rule. This changes the behavior of the CHR system, because normally, a rule can be entered starting from each head constraint. Usually this pragma will improve the efficiency of the constraint handler, but care has to be taken in order not to lose completeness. For example, in the handler leq, any pair of constraints, say A leq B, B leq A, that matches the head X leq Y , Y leq X of the antisymmetry rule, will also match it when the constraints are exchanged, B leq A, A leq B. Therefore it is enough if a currently active constraint enters this rule in the first head only, the second head can be declared to be passive. Similarly for the idempotence rule. For this rule, it is more efficient to declare the first head passive, so that the currently active constraint will be removed when the rule fires (instead of removing the older constraint and redoing all the propagation with the currently active constraint). Note that the compiler itself detects the symmetry of the two head constraints in the simplification rule antisymmetry, thus it is automatically declared passive and the compiler outputs CHR eliminated code for head 2 in antisymmetry.
antisymmetry  X leq Y , Y leq X # Id <=> X=Y pragma passive(Id).
idempotence   X leq Y # Id \ X leq Y <=> true pragma passive(Id).
transitivity  X leq Y # Id , Y leq Z ==> X leq Z pragma passive(Id).
Declaring the first head of rule transitivity passive changes the behavior of the handler. It will propagate less depending on the order in which the constraints arrive:
?- X leq Y, Y leq Z.
X leq Y,
Y leq Z,
X leq Z ? 

?- Y leq Z, X leq Y.
Y leq Z,
X leq Y ? 

?- Y leq Z, X leq Y, Z leq X.
Y = X,
Z = X ?
The last query shows that the handler is still complete in the sense that all circular chains of leq-relations are collapsed into equalities.

Options

Options parametrise the rule compilation process. Thus they should precede the rule definitions. Example:

option(check_guard_bindings, off).

The format below lists the names of the recognized options together with the acceptable values. The first entry in the lists is the default value.

option(debug_compile, [off,on]).
Instruments the generated code such that the execution of the rules may be traced (see section Debugging CHR Programs).
option(check_guard_bindings, [on,off]).
Per default, for guards of type ask the CHR runtime system makes sure that no variables are touched or the cause of an instantiation error. These checks may be turned off with this option, i.e. all guards are treated as if they were of the tell variety. The option was kept for backward compatibility. Tell and ask guards offer better granularity.
option(already_in_store, [off,on]).
If this option is on, the CHR runtime system checks for the presence of an identical constraint upon the insertion into the store. If present, the attempted insertion has no effect. Since checking for duplicates for all constraints costs, duplicate removal specific to individual constraints, using a few simpagation rules of the following form instead, may be a better solution.
Constraint \ Constraint <=> true.
option(already_in_heads, [off,on]).
The intention of simplification and simpagation rules is often to combine the heads into a stronger version of one of them. Depending on the strength of the guard, the new constraint may be identical to one of the heads removed by the rule. This removal followed by addition is inefficient and may even cause termination problems. If the option is enabled, this situation is detected and the corresponding problems are avoided. This option applies to all constraints and is provided mainly for backward compatibility. Better grained control can be achieved with corresponding pragmas. (see section Pragmas).

The remaining options are meant for CHR implementors only:

option(flatten, [on,off]).
option(rule_ordering, [canonical,heuristic]).
option(simpagation_scheme, [single,multi]).
option(revive_scheme, [new,old]).
option(dead_code_elimination, [on,off]).

Built-In Predicates

This table lists the predicates made available by the CHR library. They are meant for advanced users, who want to tailor the CHR system towards their specific needs.

current_handler(?Handler, ?Module)
Nondeterministically enumerates the defined handlers with the module they are defined in.
current_constraint(?Handler, ?Constraint)
Nondeterministically enumerates the defined constraints in the form Functor/Arity and the handlers they are defined in.
insert_constraint(+Constraint, -Id)
Inserts Constraint into the constraint store without executing any rules. The constraint will be woken and reconsidered when one of the variables in Constraint is touched. Id is unified with an internal object representing the constraint. This predicate only gets defined when a handler and constraints are declared (see section Declarations).
insert_constraint(+Constraint, -Id, ?Term)
Inserts Constraint into the constraint store without executing any rules. The constraint will be woken and reconsidered when one of the variables in Term is touched. Id is unified with an internal object representing the constraint. This predicate only gets defined when a handler and constraints are declared (see section Declarations).
find_constraint(?Pattern, -Id)
Nondeterministically enumerates constraints from the constraint store that match Pattern, i.e. which are instances of Pattern. Id is unified with an internal object representing the constraint.
find_constraint(-Var, ?Pattern, -Id)
Nondeterministically enumerates constraints from the constraint store that delay on Var and match Pattern, i.e. which are instances of Pattern. The identifier Id can be used to refer to the constraint later, e.g. for removal.
findall_constraints(?Pattern, ?List)
Unifies List with a list of Constraint # Id pairs from the constraint store that match Pattern.
findall_constraints(-Var, ?Pattern, ?List)
Unifies List with a list of Constraint # Id pairs from the constraint store that delay on Var and match Pattern.
remove_constraint(+Id)
Removes the constraint Id, obtained with one of the previous predicates, from the constraint store.
unconstrained(?Var)
Succeeds if no CHR constraint delays on Var. Defined as:
unconstrained(X) :- 
    find_constraint(X, _, _), !, fail.
unconstrained(_).
notify_constrained(?Var)
Leads to the reconsideration of the constraints associated with Var. This mechanism allows solvers to communicate reductions on the set of possible values of variables prior to making bindings.

Consulting and Compiling Constraint Handlers

The CHR compilation process has been made as transparent as possible. The user deals with files containing CHR just as with files containing ordinary Prolog predicates. Thus CHR may be consulted, compiled with various compilation modes, and compiled to file (see section Loading Programs).

Compiler-generated Predicates

Besides predicates for the defined constraints, the CHR compiler generates some support predicates in the module containing the handler. To avoid naming conflicts, the following predicates must not be defined or referred to by user code in the same module:

verify_attributes/3
attribute_goal/2
attach_increment/2
'attach_F/A'/2
for every defined constraint F/A.
'F/A_N_M_...'/Arity
for every defined constraint F/A. N,M is are integers, Arity > A.

For the prime number example that is:

        attach_increment/2
        attach_prime/1/2
        attach_primes/1/2
        attribute_goal/2
        goal_expansion/3
        prime/1
        prime/1_1/2
        prime/1_1_0/3
        prime/1_2/2
        primes/1
        primes/1_1/2
        verify_attributes/3

If an author of a handler wants to avoid naming conflicts with the code that uses the handler, it is easy to encapsulate the handler. The module declaration below puts the handler into module primes, which exports only selected predicates - the constraints in our example.

        :- module(primes, [primes/1,prime/1]).

        :- use_module(library(chr)).

        handler eratosthenes.
        constraints primes/1,prime/1.
        ...

Operator Declarations

This table lists the operators as used by the CHR library:

:- op(1200, xfx, @).
:- op(1190, xfx, pragma).
:- op(1180, xfx, [==>,<=>]).
:- op(1180, fy,  chr_spy).
:- op(1180, fy,  chr_nospy).
:- op(1150, fx,  handler).
:- op(1150, fx,  constraints).
:- op(1150, fx,  rules).
:- op(1100, xfx, '|').
:- op(1100, xfx, \ ).
:- op(1050, xfx, &).
:- op( 500, yfx, #).

Exceptions

The CHR runtime system reports instantiation and type errors for the predicates:

find_constraint/2
findall_constraints/3
insert_constraint/2
remove_constraint/1
notify_constrained/1

The only other CHR specific runtime error is:

{CHR ERROR: registering <New>, module <Module> already hosts <Old>}
An attempt to load a second handler New into module <Module> already hosting handler <Old> was made.

The following exceptional conditions are detected by the CHR compiler:

{CHR Compiler ERROR: syntax rule <N>: <Term>}
If the N-th <Term> in the file being loaded violates the CHR syntax (see section Constraint Handling Rules, Syntax).
{CHR Compiler ERROR: too many general heads in <Name>}
Unspecific heads in definitions like C \ C <=> true must not be combined with other heads in rule <Name>.
{CHR Compiler ERROR: bad pragma <Pragma> in <Name>}
The pragma <Pragma> used in rule <Name> does not qualify. Currently this only happens if <Pragma> is unbound.
{CHR Compiler ERROR: found head <F/A> in <Name>, expected one of: <F/A list>}
Rule <Name> has a head of given F/A which is not among the defined constraints.
{CHR Compiler ERROR: head identifiers in <Name> are not unique variables}
The identifiers to refer to individual constraints (heads) via `#' in rule <Name> do not meet the indicated requirements.
{CHR Compiler ERROR: no handler defined}
CHR specific language elements, declarations or rules for example, are used before a handler was defined. This error is usually reported a couple of times, i.e. as often as there are CHR forms in the file expecting the missing definition.
{CHR Compiler ERROR: compilation failed}
Not your fault. Send us a bug report.

Debugging CHR Programs

Use option(debug_compile,on) preceding any rules in the file containing the handler to enable CHR debugging. The CHR debugging mechanism works by instrumenting the code generated by the CHR compiler. Basically, the CHR debugger works like the Prolog debugger. The main differences are: there are extra ports specific to CHR, and the CHR debugger provides no means for the user to change the flow of control, i.e. there are currently no retry and fail options available.

Control Flow Model

The entities reflected by the CHR debugger are constraints and rules. Constraints are treated like ordinary Prolog goals with the usual ports: [call,exit,redo,fail]. In addition, constraints may get inserted into or removed from the constraint store (ports: insert,remove), and stored constraints containing variables will be woken and reconsidered (port: wake) when variables are touched.

The execution of a constraint consists of trying to apply the rules mentioning the constraint in their heads. Two ports for rules reflect this process: At a try port the active constraint matches one of the heads of the rule, and matching constraints for the remaining heads of the rule, if any, have been found as well. The transition from a try port to an apply port takes place when the guard has been successfully evaluated, i.e. when the rule commits. At the apply port, the body of the rule is just about to be executed. The body is a Prolog goal transparent to the CHR debugger. If the rule body contains CHR constraints, the CHR debugger will track them again. If the rules were consulted, the Prolog debugger can be used to study the evaluations of the other predicates in the body.

CHR Debugging Predicates

The following predicates control the operation of the CHR debugger:

chr_trace
Switches the CHR debugger on and ensures that the next time control enters a CHR port, a message will be produced and you will be asked to interact. At this point you have a number of options. See section CHR Debugging Options. In particular, you can just type cr (Return) to creep (or single-step) into your program. You will notice that the CHR debugger stops at many ports. If this is not what you want, the predicate chr_leash gives full control over the ports at which you are prompted.
chr_debug
Switches the CHR debugger on and ensures that the next time control enters a CHR port with a spy-point set, a message will be produced and you will be asked to interact.
chr_nodebug
Switches the CHR debugger off. If there are any spy-points set then they will be kept.
chr_notrace
Equivalent to chr_nodebug.
chr_debugging
Prints onto the standard error stream information about the current CHR debugging state. This will show:
  1. Whether the CHR debugger is switched on.
  2. What spy-points have been set (see below).
  3. What mode of leashing is in force (see below).
chr_leash(+Mode)
The leashing mode is set to Mode. It determines the CHR ports at which you are to be prompted when you creep through your program. At unleashed ports a tracing message is still output, but program execution does not stop to allow user interaction. Note that the ports of spy-points are always leashed (and cannot be unleashed). Mode is a list containing none, one or more of the following port names:
call
Prompt when a constraint is executed for the first time.
exit
Prompt when the constraint is successfully processed, i.e. the applicable rules have applied.
redo
Prompt at subsequent exits generated by non-deterministic rule bodies.
fail
Prompt when a constraint fails.
wake
Prompt when a constraint from the constraint store is woken and reconsidered because one of its variables has been touched.
try
Prompt just before the guard evaluation of a rule, after constraints matching the heads have been found.
apply
Prompt upon the application of a rule, after the successful guard evaluation, when the rule commits and fires, just before evaluating the body.
insert
Prompt when a constraint gets inserted into the constraint store, i.e. after all rules have been tried.
remove
Prompt when a constraint gets removed from the constraint store, e.g. when a simplification rule applies.
The initial value of the CHR leashing mode is [call,exit,fail,wake,apply]. Predefined shortcuts are:
chr_leash(none), chr_leash(off)
To turn leashing off.
chr_leash(all)
To prompt at every port.
chr_leash(default)
Same as chr_leash([call,exit,fail,wake,apply]).
chr_leash(call)
No need to use a list if only a singular port is to be leashed.

CHR Spy-points

For CHR programs of any size, it is clearly impractical to creep through the entire program. Spy-points make it possible to stop the program upon an event of interest. Once there, one can set further spy-points in order to catch the control flow a bit further on, or one can start creeping.

Setting a spy-point on a constraint or a rule indicates that you wish to see all control flow through the various ports involved, except during skips. When control passes through any port with a spy-point set on it, a message is output and the user is asked to interact. Note that the current mode of leashing does not affect spy-points: user interaction is requested on every port.

Spy-points are set and removed by the following predicates, which are declared as prefix operators:

chr_spy Spec
Sets spy-points on constraints and rules given by Spec, which is is of the form:
_ (variable)
denoting all constraints and rules, or:
constraints Cs
where Cs is one of
_ (variable)
denoting all constraints
C,...,C
denoting a list of constraints C
Name
denoting all constraints with this functor, regardless of arity
Name/Arity
denoting the constraint of that name and arity
rules Rs
where Rs is one of:
_ (variable)
denoting all rules
R,...,R
denoting a list of rules R
Name
where Name is the name of a rule in any handler.
already_in_store
The name of a rule implicitly defined by the system when the option already_in_store is in effect.
already_in_heads
The name of a rule implicitly defined by the system when the option already_in_heads or the corresponding pragmas are in effect.
Handler:Name
where Handler is the name of a constraint handler and Name is the name of a rule in that handler
Examples:
| ?- chr_spy rules rule(3), transitivity, already_in_store.
| ?- chr_spy constraints prime/1.
If you set spy-points, the CHR debugger will be switched on.
chr_nospy Spec
Removes spy-points on constraints and rules given by Spec, where Spec is of the form as described for chr_spy Spec. There is no chr_nospyall/0. To remove all CHR spy-points use chr_nospy _.

The options available when you arrive at a spy-point are described later. See section CHR Debugging Options.

CHR Debugging Messages

All trace messages are output to the standard error stream. This allows you to trace programs while they are performing file I/O. The basic format is as follows:

S 3   1 try     eratosthenes:absorb(10) @ prime(9)#<c4>, prime(10)#<c2> ?

S is a spy-point indicator. It is printed as ` ' if there is no spy-point, as `r', indicating that there is a spy-point on this rule, or as `c' if one of the involved constraints has a spy-point.

The first number indicates the current depth of the execution; i.e. the number of direct ancestors the currently active constraint has.

The second number indicates the head position of the currently active constraint at rule ports.

The next item tells you which port is currently traced.

A constraint or a matching rule are printed next. Constraints print as Term#Id, where Id is a unique identifier pointing into the constraint store. Rules are printed as Handler:Name @, followed by the constraints matching the heads.

The final `?' is the prompt indicating that you should type in one of the debug options (see section CHR Debugging Options).

CHR Debugging Options

This section describes the options available when the system prompts you after printing out a debugging message. Most of them you know from the standard Prolog debugger. All the options are one letter mnemonics, some of which can be optionally followed by a decimal integer. They are read from the standard input stream up to the end of the line (Return, <cr>). Blanks will be ignored.

The only option which you really have to remember is `h'. This provides help in the form of the following list of available options.

CHR debugging options:
   <cr>   creep            c      creep
    l     leap                         
    s     skip             s <i>  skip (ancestor i)
    g     ancestors                   
    &     constraints      & <i>  constraints (details)
    n     nodebug          =      debugging
    +     spy this                    
    -     nospy this       .      show rule
    <     reset printdepth < <n>  set printdepth
    a     abort            b      break
    ?     help             h      help
c
<cr>
creep causes the debugger to single-step to the very next port and print a message. Then if the port is leashed, the user is prompted for further interaction. Otherwise, it continues creeping. If leashing is off, creep is the same as leap (see below) except that a complete trace is printed on the standard error stream.
l
leap causes the debugger to resume running your program, only stopping when a spy-point is reached (or when the program terminates). Leaping can thus be used to follow the execution at a higher level than exhaustive tracing.
s
s i
skip over the entire execution of the constraint. That is, you will not see anything until control comes back to this constraint (at either the exit port or the fail port). This includes ports with spy-points set; they will be masked out during the skip. The command can be used with a numeric argument to skip the execution up to and including the ancestor indicated by the argument. Example:
      ...
      4   - exit    prime(8)#<c6> ? g
Ancestors:
      1   1 apply   eratosthenes:rule(2) @ primes(10)#<c1>
      2   1 apply   eratosthenes:rule(2) @ primes(9)#<c3>
      3   1 apply   eratosthenes:rule(2) @ primes(8)#<c5>
      4   - call    prime(8)#<c6>

      4   - exit    prime(8)#<c6> ? s 2
      2   - exit    primes(9)#<c3> ? 
g
print ancestors provides you with a list of ancestors to the currently active constraint, i.e. all constraints not yet exited that led to the current constraint in the derivation sequence. The format is the same as with trace messages. Constraints start with call entries in the stack. The subsequent application of a rule replaces the call entry in the stack with an apply entry. Later the constraint shows again as redo or fail entry. Example:
      0   - call    primes(10)#<c1> ? 
      1   1 try     eratosthenes:rule(2) @ primes(10)#<c1> ? g

Ancestors:
      1   - call    primes(10)#<c1>

      1   1 try     eratosthenes:rule(2) @ primes(10)#<c1> ? 
      1   1 apply   eratosthenes:rule(2) @ primes(10)#<c1> ? 
      1   - call    prime(10)#<c2> ? 
      2   - insert  prime(10)#<c2>
      2   - exit    prime(10)#<c2> ? g

Ancestors:
      1   1 apply   eratosthenes:rule(2) @ primes(10)#<c1>
      2   - call    prime(10)#<c2>
&
print constraints prints a list of the constraints in the constraint store. With a numeric argument, details relevant primarily to CHR implementors are shown.
n
nodebug switches the CHR debugger off.
=
debugging outputs information concerning the status of the CHR debugger as via chr_debugging/0
+
spy this sets a spy-point on the current constraint or rule.
-
nospy this removes the spy-point from the current constraint or rule, if it exists.
.
show rule prints the current rule instantiated by the matched constraints. Example:
 8   1 apply   era:absorb(8) @ prime(4)#<c14> \ prime(8)#<c6> ? .

 absorb(8) @
  prime(4)#<c14> \ 
    prime(8)#<c6> <=>

    8 mod 4=:=0
    |
    true.
<
< n
While in the debugger, a printdepth is in effect for limiting the subterm nesting level when printing rules and constraints. The limit is initially 10. This command, without arguments, resets the limit to 10. With an argument of n, the limit is set to n, treating 0 as infinity.
a
abort calls the built-in predicate abort/0.
b
break calls the built-in predicate break/0, thus putting you at a recursive top-level. When you end the break (entering ^D) you will be re-prompted at the port at which you broke. The CHR debugger is temporarily switched off as you call the break and will be switched on again when you finish the break and go back to the old execution. Any changes to the CHR leashing or to spy-points during the break will remain in effect.
?
h
help displays the table of options given above.

Programming Hints

This section gives you some programming hints for CHR. For maximum efficiency of your constraint handler, see also the previous subsections on declarations and options.

Constraint handling rules for a given constraint system can often be derived from its definition in formalisms such as inference rules, rewrite rules, sequents, formulas expressing axioms and theorems. CHR can also be found by first considering special cases of each constraint and then looking at interactions of pairs of constraints sharing a variable. Cases that do not occur in the application can be ignored.

It is important to find the right granularity of the constraints. Assume one wants to express that n variables are different from each other. It is more efficient to have a single constraint all_different(List_of_n_Vars) than n*n inequality constraints between each pair of different variables. However, the extreme case of having a single constraint modeling the whole constraint store will usually be inefficient.

Starting from an executable specification, the rules can then be refined and adapted to the specifics of the application. Efficiency can be improved by weakening the guards to perform simplification as early as needed and by strengthening the guards to do the just right amount of propagation. Propagation rules can be expensive, because no constraints are removed.

The more heads a rule has, the more expensive it is. Rules with several heads are more efficient, if the heads of the rule share a variable (which is usually the case). Then the search for a partner constraint has to consider less candidates. In the current implementation, constraints are indexed by their functors, so that the search is only performed among the constraints containing the shared variable. Moreover, two rules with identical (or sufficiently similar) heads can be merged into one rule so that the search for a partner constraint is only performed once instead of twice.

As guards are tried frequently, they should be simple tests not involving side-effects. Head matching is more efficient than explicitly checking equalities in the ask-part of the guard. In the tell part of a guard, it should be made sure that variables from the head are never touched (e.g. by using nonvar or ground if necessary). For efficiency and clarity reasons, one should also avoid using constraints in guards. Besides conjunctions, disjunctions are allowed in the guard, but they should be used with care. The use of other control built-in predicates in the guard is discouraged. Negation and if-then-else in the ask part of a guard can give wrong results, since e.g. failure of the negated goal may be due to touching its variables.

Several handlers can be used simultaneously if they do not share constraints with the same name. The implementation will not work correctly if the same constraint is defined in rules of different handlers that have been compiled separately. In such a case, the handlers must be merged by hand. This means that the source code has to be edited so that the rules for the shared constraint are together (in one module). Changes may be necessary (like strengthening guards) to avoid divergence or loops in the computation.

Constraint Handlers

The CHR library comes with plenty of constraint handlers written in CHR. The most recent versions of these are maintained at:

http://www.pst.informatik.uni-muenchen.de/~fruehwir/chr-solver.html
`arc.pl'
classical arc-consistency over finite domains
`bool.pl'
simple Boolean constraints
`cft.pl'
feature term constraints according to the CFT theory
`domain.pl'
finite domains over arbitrary ground terms and interval domains over integers and reals, but without arithmetic functions
`gcd.pl'
elegant two-liner for the greatest common divisor
`interval.pl'
straightforward interval domains over integers and reals, with arithmetic functions
`kl-one.pl'
terminological reasoning similar to KL-ONE or feature trees
`leq.pl'
standard introductory CHR example handler for less-than-or-equal
`list.pl'
equality constraints over concatenations of lists (or strings)
`listdom.pl'
a straightforward finite enumeration list domains over integers, similar to `interval.pl'
`math-elim.pl'
solves linear polynomial equations and inequations using variable elimination, several variations possible
`math-fougau.pl'
solves linear polynomial equations and inequations by combining variable elimination for equations with Fourier's algorithm for inequations, several variations possible
`math-fourier.pl'
a straightforward Fouriers algorithm to solve polynomial inequations over the real or rational numbers
`math-gauss.pl'
a straightforward, elegant implementation of variable elimination for equations in one rule
`minmax.pl'
simple less-than and less-than-or-equal ordering constraints together with minimum and maximum constraints
`modelgenerator.pl'
example of how to use CHR for model generation in theorem proving
`monkey.pl'
classical monkey and banana problem, illustrates how CHR can be used as a fairly efficient production rule system
`osf.pl'
constraints over order sorted feature terms according to the OSF theory
`oztype.pl'
rational trees with disequality and OZ type constraint with intersection
`pathc.pl'
the most simple example of a handler for path consistency - two rules
`primes.pl'
elegant implementations of the sieve of Eratosthenes reminiscent of the chemical abstract machine model, also illustrates use of CHR as a general purpose concurrent constraint language
`scheduling.pl'
simple classical constraint logic programming scheduling example on building a house
`tarski.pl'
most of Tarski's axiomatization of geometry as constraint system
`term.pl'
Prolog term manipulation built-in predicates functor/3, arg/3, =../2 as constraints
`time-pc.pl'
grand generic handler for path-consistency over arbitrary constraints, load via `time.pl' to get a powerful solver for temporal constraints based on Meiri's unifying framework. `time-rnd.pl' contains a generator for random test problems.
`time-point.pl'
quantitative temporal constraints over time points using path-consistency
`tree.pl'
equality and disequality over finite and infinite trees (terms)
`type.pl'
equalities and type constraints over finite and infinite trees (terms)

You can consult or compile a constraint handler from the CHR library using e.g.:

?- [library('chr/examples/gcd')].
?- compile(library('chr/examples/gcd')).

If you want to learn more about the handlers, look at their documented source code.

In addition, there are files with example queries for some handlers, their file name starts with `examples-' and the file extension indicates the handler, e.g. `.bool':

examples-adder.bool
examples-benchmark.math
examples-deussen.bool
examples-diaz.bool
examples-fourier.math
examples-holzbaur.math
examples-lim1.math
examples-lim2.math
examples-lim3.math
examples-puzzle.bool
examples-queens.bool
examples-queens.domain
examples-stuckey.math
examples-thom.math

Backward Compatibility

In this section, we discuss backward compatibility with the CHR library of Eclipse Prolog.

  1. The restriction on at most two heads in a rule has been abandoned. A rule can have as many heads as you like. Note however, that searching for partner constraints can be expensive.
  2. By default, rules are compiled in textual order. This gives the programmer more control over the constraint handling process. In the Eclipse library of CHR, the compiler was optimizing the order of rules. Therefore, when porting a handler, rules may have to be reordered. A good heuristic is to prefer simplification to simpagation and propagation and to prefer rules with single heads to rules with several heads. Instead of manually rearranging an old handler one may also use the following combination of options to get the corresponding effect:
    option(rule_ordering,heuristic).
    option(revive_scheme,old).
    
  3. For backward compatibility, the already_in_store, already_in_head and guard_bindings options are still around, but there are CHR syntax extensions: section Constraint Handling Rules, Syntax and pragmas section Pragmas offering better grained control.
  4. The Eclipse library of CHR provided automatic built-in labeling through the label_with declaration. Since it was not widely used and can be easily simulated, built-in labeling was dropped. The same effect can be achieved by replacing the declaration label_with Constraint if Guard by the simplification rule chr_labeling, Constraint <=> Guard | Constraint', chr_labeling and by renaming the head in each clause Constraint :- Body into Constraint' :- Body where Constraint' is a new predicate. Efficiency can be improved by declaring Constraint to be passive: chr_labeling, Constraint#Id <=> Guard | Constraint', chr_labeling pragma passive(Id). This translation will not work if option(already_in_heads,on). In that case use e.g. chr_labeling(_), Constraint <=> Guard | Constraint', chr_labeling(_) to make the new call to chr_labeling differ from the head occurrence.
  5. The set of built-in predicates for advanced CHR users is now larger and better designed. Also the debugger has been improved. The Opium debugging environment is not available in SICStus Prolog.


Go to the first, previous, next, last section, table of contents.