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

This chapter is written by Tom Schrijvers, K.U. Leuven, and adjustments by
Jan Wielemaker.

The CHR system of SWI-Prolog is the {\em 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 licensed under compatible conditions with permission from the authors.

The main reference for the K.U.Leuven CHR system is:
\begin{itemize}
\item T. Schrijvers, and B. Demoen, {\em The K.U.Leuven CHR System: Implementation
and Application}, First Workshop on Constraint Handling Rules: Selected
Contributions (Fr\"uhwirth, T. and Meister, M., eds.), pp. 1--5, 2004.
\end{itemize}

On the K.U.Leuven CHR website (\url{http://dtai.cs.kuleuven.be/CHR/})
you can find more related papers, references and example programs.

\section{Introduction to CHR}			\label{sec:chr-intro}
%=====================

Constraint Handling Rules (CHR) is a committed-choice rule-based language
embedded in Prolog. It is designed for writing constraint solvers and is
particularly useful for providing application-specific constraints.
It has been used in many kinds of applications, like scheduling,
model checking, abduction, and 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
\cite{Freuhwirth:2009}. More background on CHR can be found at
\cite{chrSite}.

In \secref{chr-syntaxandsemantics} we present the syntax of CHR in
Prolog and explain informally its operational semantics. Next,
\secref{practical} deals with practical issues of writing and compiling
Prolog programs containing CHR. \Secref{chr-debugging} explains the
(currently primitive) CHR debugging facilities. \Secref{chr-debug-preds}
provides a few useful predicates to inspect the constraint store, and
\secref{chr-examples} illustrates CHR with two example programs.
\Secref{chr-compatibility} describes some compatibility issues with
older versions of this system and SICStus' CHR system. Finally,
\secref{chr-guidelines} concludes with a few practical guidelines for
using CHR.


\section{CHR Syntax and Semantics}		\label{sec:chr-syntaxandsemantics}
%=============================

\subsection{Syntax of CHR rules}
\label{sec:chr-syntax}
%-----------------

\begin{code}
rules --> rule, rules ; [].

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

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

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

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

head --> constraints.

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

constraint --> compound_term.

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

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{code}

\noindent
Note that the guard of a rule may not contain any goal that binds a variable
in the head of the rule with a non-variable or with another variable in the
head of the rule. It may, however, bind variables that do not appear in the
head of the rule, e.g. an auxiliary variable introduced in the guard.

\subsection{Semantics of CHR}
\label{sec:chr-semantics}
%--------------------

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 constraints can be found, or the matching 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 non-variable
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.

\paragraph{Rule Types}
%- - - - - - - - - -

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

\begin{itemlist}
    \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
$\backslash$ 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: \[ constraints_1
\backslash constraints_2 <=> body \] The $\mathit{constraints}_1$
constraints are not called in the body.
\end{itemlist}

\paragraph{Rule Names}
%- - - - - - - - - -
Naming a rule is optional and has no semantic meaning. It only functions
as documentation for the programmer.

\paragraph{Pragmas}
%- - - - - - - - -
The semantics of the pragmas are:

\begin{description}
    \termitem{passive}{Identifier}
The constraint in the head of a rule \arg{Identifier} can only match a
passive constraint in that rule.
There is an abbreviated syntax for this pragma. Instead of:
\begin{code}
                ..., c # Id, ... <=> ... pragma passive(Id)
\end{code}

\noindent
you can also write
\begin{code}
                ..., c # passive, ... <=> ...
\end{code}

\noindent
\end{description}

Additional pragmas may be released in the future.

\begin{description}
    \directive{chr_option}{2}{+Option, +Value}
It is possible to specify options that apply to all the CHR rules in the module.
Options are specified with the \texttt{\index{chr_option/2}\predref{chr_option}{2}} declaration:

\begin{code}
:- chr_option(Option,Value).
\end{code}

\noindent
and may appear in the file anywhere after the first constraints declaration.

Available options are:
\begin{description}
        \termitem{check_guard_bindings}{}
This option controls whether guards should be checked for (illegal) variable
bindings or not. Possible values for this option are \texttt{on} to enable
the checks, and \texttt{off} to disable the checks. If this option is on,
any guard fails when it binds a variable that appears in the head of the rule.
When the option is off (default), the behaviour of a binding in the guard is undefined.

        \termitem{optimize}{}
This option controls the degree of optimization.
Possible values are \texttt{full} to enable all available
optimizations, and \texttt{off} (default) to disable all optimizations.
The default is derived from the SWI-Prolog flag \prologflag{optimise}, where
\const{true} is mapped to \const{full}.  Therefore the command line
option \cmdlineoption{-O} provides full CHR optimization.
If optimization is enabled, debugging must be disabled.

	\termitem{debug}{}
This option enables or disables the possibility to debug the CHR code.
Possible values are \texttt{on} (default) and \texttt{off}. See
\secref{chr-debugging} for more details on debugging.  The default is
derived from the Prolog flag \prologflag{generate_debug_info}, which
is \const{true} by default.  See \cmdlineoption{--no-debug}.
If debugging is enabled, optimization must be disabled.
\end{description}
\end{description}

% The above mode, type_declaration and type_definition options are deprecated.
% The new syntax is described below.

\section{CHR in SWI-Prolog Programs}		\label{sec:practical}
%===========================


\subsection{Embedding CHR in Prolog Programs}
\label{sec:chr-embedding}

The CHR constraints defined in a \fileext{pl} file are
associated with a module. The default module is \const{user}. One should
never load different \fileext{pl} files with the same CHR module name.

\subsection{CHR Constraint declaration}
\label{sec:chr-declarations}

\begin{description}
    \directive{chr_constraint}{1}{+Specifier}
Every constraint used in CHR rules has to be declared with a
\index{chr_constraint/1}\predref{chr_constraint}{1} declaration by the {\em constraint specifier}. For
convenience multiple constraints may be declared at once with the same
\predref{chr_constraint}{1} declaration followed by a comma-separated
list of constraint specifiers.

A constraint specifier is, in its compact form, \texttt{$F$/$A$} where
$F$ and $A$ are respectively the functor name and arity of the
constraint, e.g.:

\begin{code}
:- chr_constraint foo/1.
:- chr_constraint bar/2, baz/3.
\end{code}

\noindent
In its extended form, a constraint specifier is
\texttt{$c$($A_1$,\ldots,$A_n$)} where $c$ is the constraint's functor,
$n$ its arity and the $A_i$ are argument specifiers. An argument
specifier is a mode, optionally followed by a type. Example:

\begin{code}
:- chr_constraint get_value(+,?).
:- chr_constraint domain(?int, +list(int)),
                  alldifferent(?list(int)).
\end{code}

\noindent
\end{description}

\paragraph{Modes}

A mode is one of:
	\begin{description}
	\termitem{\Sminus}{} The corresponding argument of every occurrence
	of the constraint is always unbound.
	\termitem{\Splus}{} The corresponding argument of every occurrence
	of the constraint is always ground.
	\termitem{\Squest}{} The corresponding argument of every occurrence
	of the constraint can have any instantiation, which may change
	over time. This is the default value.
	\end{description}

\paragraph{Types}

A type can be a user-defined type or one of the built-in types. A type
comprises a (possibly infinite) set of values. The type declaration for a
constraint argument means that for every instance of that constraint the
corresponding argument is only ever bound to values in that set. It does not
state that the argument necessarily has to be bound to a value.

The built-in types are:
	\begin{description}
	\termitem{int}{} The corresponding argument of every occurrence
	of the constraint is an integer number.
	\termitem{dense_int}{} The corresponding argument of every occurrence
	of the constraint is an integer that can be used as an array index.
	Note that if this argument takes values in $[0,n]$, the array takes
	$O(n)$ space.
	\termitem{float}{} \ldots a floating point number.
	\termitem{number}{} \ldots a number.
	\termitem{natural}{} \ldots a positive integer.
	\termitem{any}{} The corresponding argument of every occurrence
	of the constraint can have any type. This is the default value.
	\end{description}

\begin{description}
    \directive{chr_type}{1}{+TypeDeclaration}
User-defined types are algebraic data types, similar to those in Haskell
or the discriminated unions in Mercury. An algebraic data type is
defined using \index{chr_type/1}\predref{chr_type}{1}:

\begin{code}
:- chr_type type ---> body.
\end{code}

\noindent
If the type term is a functor of arity zero (i.e. one having zero
arguments), it names a monomorphic type. Otherwise, it names a
polymorphic type; the arguments of the functor must be distinct type
variables. The body term is defined as a sequence of constructor
definitions separated by semi-colons.

Each constructor definition must be a functor whose arguments (if
any) are types. Discriminated union definitions must be transparent:
all type variables occurring in the body must also occur in the type.

Here are some examples of algebraic data type definitions:

\begin{code}
:- chr_type color ---> red ; blue ; yellow ; green.

:- chr_type tree --->  empty ; leaf(int) ; branch(tree, tree).

:- chr_type list(T) ---> [] ; [T | list(T)].

:- chr_type pair(T1, T2) ---> (T1 - T2).
\end{code}

\noindent
Each algebraic data type definition introduces a distinct type.
Two algebraic data types that have the same bodies are considered to be
distinct types (name equivalence).

Constructors may be overloaded among different types: there may be any number
of constructors with a given name and arity, so long as they all have different
types.

Aliases can be defined using ==. For example, if your program uses lists
of lists of integers, you can define an alias as follows:

\begin{code}
:- chr_type lli == list(list(int)).
\end{code}

\noindent
\end{description}


\paragraph{Type Checking}

Currently two complementary forms of type checking are performed:
\begin{enumerate}
\item Static type checking is always performed by the compiler. It is
      limited to CHR rule heads and CHR constraint calls in rule bodies.

      Two kinds of type error are detected. The first is where a variable
      has to belong to two types. For example, in the program:
\begin{code}
:-chr_type foo ---> foo.
:-chr_type bar ---> bar.

:-chr_constraint abc(?foo).
:-chr_constraint def(?bar).

foobar @ abc(X) <=> def(X).
\end{code}

\noindent
the variable \texttt{X} has to be of both type \texttt{foo} and \texttt{bar}.
This is reported as a type clash error:

\begin{code}
CHR compiler ERROR:
    `--> Type clash for variable _ in rule foobar:
                expected type foo in body goal def(_, _)
                expected type bar in head def(_, _)
\end{code}

\noindent
The second kind of error is where a functor is used that does not belong
to the declared type. For example in:

\begin{code}
:- chr_type foo ---> foo.
:- chr_type bar ---> bar.

:- chr_constraint abc(?foo).

foo @ abc(bar) <=> true.
\end{code}

\noindent
\const{bar} appears in the head of the rule where something of
type \const{foo} is expected. This is reported as:

\begin{code}
CHR compiler ERROR:
    `--> Invalid functor in head abc(bar) of rule foo:
                found `bar',
                expected type `foo'!
\end{code}

\noindent
No runtime overhead is incurred in static type checking.

\item Dynamic type checking checks at runtime, during program execution,
      whether the arguments of CHR constraints respect their declared types.
      The \predref{when}{2} co-routining library is used to delay dynamic type
      checks until variables are instantiated.

      The kind of error detected by dynamic type checking is where a functor
      is used that does not belong to the declared type. For example, for the program:
\begin{code}
:-chr_type foo ---> foo.

:-chr_constraint abc(?foo).
\end{code}

\noindent
we get the following error in an erroneous query:

\begin{code}
?- abc(bar).
ERROR: Type error: `foo' expected, found `bar'
       (CHR Runtime Type Error)
\end{code}

\noindent
Dynamic type checking is weaker than static type checking in the sense
that it only checks the particular program execution at hand rather than
all possible executions. It is stronger in the sense that it tracks
types throughout the whole program.

Note that it is enabled only in debug mode, as it incurs some (minor)
runtime overhead.
\end{enumerate}

\subsection{CHR Compilation}
\label{sec:chr-compilation}
%--------------------

The SWI-Prolog CHR compiler exploits \index{term_expansion/2}\predref{term_expansion}{2} rules to translate
the constraint handling rules to plain Prolog. These rules are loaded
from the library \pllib{chr}. They are activated if the compiled file
has the \fileext{chr} extension or after finding a declaration in the
following format:

\begin{code}
:- chr_constraint ...
\end{code}

\noindent
It is advised to define CHR rules in a module file, where the module
declaration is immediately followed by including the library(chr) library
as exemplified below:

\begin{code}
:- module(zebra, [ zebra/0 ]).
:- use_module(library(chr)).

:- chr_constraint ...
\end{code}

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

\section{Debugging CHR programs}		\label{sec:chr-debugging}
%=================

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 \prologflag{debug}, whose default is derived
from the SWI-Prolog flag \prologflag{generate_debug_info}.  Therefore debug
info is provided unless the \cmdlineoption{--no-debug} is used.


\subsection{CHR debug ports}			\label{sec:chr-ports}
%===============

For CHR constraints the four standard ports are defined:

\begin{description}
	\termitem{call}{}
A new constraint is called and becomes active.
	\termitem{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.
	\termitem{fail}{}
An active constraint fails.
	\termitem{redo}{}
An active constraint starts looking for an alternative solution.
\end{description}


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

\begin{description}
	\termitem{wake}{}
A suspended constraint is woken and becomes active.
	\termitem{insert}{}
An active constraint has tried all rules and is suspended in
the constraint store.
	\termitem{remove}{}
An active or passive constraint is removed from the constraint
store.
\termitem{try}{}
	An active constraint tries a rule with possibly
	some passive constraints. The try port is entered
	just before committing to the rule.
\termitem{apply}{}
	An active constraint commits to a rule with possibly
	some passive constraints. The apply port is entered
	just after committing to the rule.
\end{description}

\subsection{Tracing CHR programs}
\label{sec:chr-tracing}
%=================

Tracing is enabled with the \index{chr_trace/0}\predref{chr_trace}{0} predicate
and disabled with the \index{chr_notrace/0}\predref{chr_notrace}{0} predicate.

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

The following debug commands are currently supported:

\begin{verbatim}
        CHR debug options:

                <cr>    creep           c       creep
                s       skip
                g       ancestors
                n       nodebug
                b       break
                a       abort
                f       fail
                ?       help            h       help
\end{verbatim}

\noindent
Their meaning is:

\begin{description}
	\termitem{creep}{}
Step to the next port.
	\termitem{skip}{}
Skip to exit port of this call or wake port.
	\termitem{ancestors}{}
Print list of ancestor call and wake ports.
	\termitem{nodebug}{}
Disable the tracer.
	\termitem{break}{}
Enter a recursive Prolog top level.  See \index{break/0}\predref{break}{0}.
	\termitem{abort}{}
Exit to the top level.  See \index{abort/0}\predref{abort}{0}.
	\termitem{fail}{}
Insert failure in execution.
	\termitem{help}{}
Print the above available debug options.
\end{description}

\subsection{CHR Debugging Predicates}		\label{sec:chr-debug-preds}
%====================================

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

\begin{description}
    \predicate{chr_trace}{0}{}
Activate the CHR tracer.  By default the CHR tracer is activated and
deactivated automatically by the Prolog predicates \index{trace/0}\predref{trace}{0} and
\index{notrace/0}\predref{notrace}{0}.

    \predicate{chr_notrace}{0}{}
Deactivate the CHR tracer.  By default the CHR tracer is activated and
deactivated automatically by the Prolog predicates \index{trace/0}\predref{trace}{0} and
\index{notrace/0}\predref{notrace}{0}.

    \predicate{chr_leash}{1}{+Spec}
Define the set of CHR ports on which the CHR tracer asks for user
intervention (i.e.\ stops). \arg{Spec} is either a list of ports as
defined in \secref{chr-ports} or a predefined `alias'. Defined aliases
are: \const{full} to stop at all ports, \const{none} or \const{off} to
never stop, and \const{default} to stop at the \const{call},
\const{exit}, \const{fail}, \const{wake} and \const{apply} ports.
See also \index{leash/1}\predref{leash}{1}.

    \predicate{chr_show_store}{1}{+Mod}
Prints all suspended constraints of module \arg{Mod} to the standard
output. This predicate is automatically called by the SWI-Prolog top level at
the end of each query for every CHR module currently loaded.  The Prolog flag
\const{chr_toplevel_show_store} controls whether the top level shows the
constraint stores. The value \const{true} enables it.  Any other value
disables it.

    \predicate{find_chr_constraint}{1}{-Constraint}
Returns a constraint in the constraint store. Via backtracking, all constraints
in the store can be enumerated.
\end{description}


\section{CHR Examples}			\label{sec:chr-examples}
%================

Here are two example constraint solvers written in CHR.

\begin{itemize}
    \item
The program below defines a solver with one constraint,
\nopredref{leq}{2}, which is a less-than-or-equal constraint, also known
as a partial order constraint.

\begin{code}
:- module(leq,[leq/2]).
:- use_module(library(chr)).

:- chr_constraint 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).
\end{code}

\noindent
When the above program is saved in a file and loaded in SWI-Prolog, you can
call the \nopredref{leq}{2} constraints in a query, e.g.:

\begin{code}
?- leq(X,Y), leq(Y,Z).
leq(_G23837, _G23841)
leq(_G23838, _G23841)
leq(_G23837, _G23838)
true .
\end{code}

\noindent
When the query succeeds, the SWI-Prolog top level prints the content of
the CHR constraint store and displays the bindings generated during the
query. Some of the query variables may have been bound to attributed
variables, as you see in the above example.

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

\begin{code}
:- module(dom,[dom/2]).
:- use_module(library(chr)).

:- chr_constraint dom(?int,+list(int)).
:- chr_type list(T) ---> [] ; [T|list(T)].

dom(X,[]) <=> fail.
dom(X,[Y]) <=> X = Y.
dom(X,L) <=> nonvar(X) | memberchk(X,L).
dom(X,L1), dom(X,L2) <=> intersection(L1,L2,L3), dom(X,L3).
\end{code}

\noindent
When the above program is saved in a file and loaded in SWI-Prolog, you can
call the \nopredref{dom}{2} constraints in a query, e.g.:

\begin{code}
?- dom(A,[1,2,3]), dom(A,[3,4,5]).
A = 3.
\end{code}

\noindent
\end{itemize}

\section{CHR compatibility}		\label{sec:chr-compatibility}
%==================

\subsection{The Old SICStus CHR implementation}
\label{sec:chr-sicstus}

There are small differences between the current K.U.Leuven CHR system
in SWI-Prolog, older versions of the same system, and SICStus' CHR system.

The current system maps old syntactic elements onto new ones and ignores a
number of no longer required elements. However, for each a {\em deprecated}
warning is issued. You are strongly urged to replace or remove deprecated
features.

Besides differences in available options and pragmas, the following differences
should be noted:

\begin{itemlist}
        \item [The \nopredref{constraints}{1} declaration]
This declaration is deprecated. It has been replaced with the
\index{chr_constraint/1}\predref{chr_constraint}{1} declaration.

        \item [The \nopredref{option}{2} declaration]
This declaration is deprecated. It has been replaced with the
\index{chr_option/2}\predref{chr_option}{2} declaration.

        \item [The \nopredref{handler}{1} declaration]
In SICStus every CHR module requires a \nopredref{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 \nopredref{rules}{1} declaration]
In SICStus, for every CHR module it is possible to only enable a subset
of the available rules through the \nopredref{rules}{1} declaration. The
declaration is valid syntax in SWI-Prolog, but has no effect. A
warning is given during compilation.

	\item [Guard bindings]
The \texttt{check_guard_bindings} option only turns invalid calls to
unification into failure. In SICStus this option does more: it intercepts
instantiation errors from Prolog built-ins such as \index{is/2}\predref{is}{2} and
turns them into failure. In SWI-Prolog, we do not go this far, as we like
to separate concerns more. The CHR compiler is aware of the CHR code, the Prolog
system, and the programmer should be aware of the appropriate meaning of the
Prolog goals used in guards and bodies of CHR rules.
\end{itemlist}

\subsection{The Old ECLiPSe CHR implementation}
\label{sec:chr-eclipse}

The old ECLiPSe CHR implementation features a \nopredref{label_with}{1} construct
for labeling variables in CHR constraints. This feature has long since been abandoned.
However, a simple transformation is all that is required to port the functionality.
\begin{code}
label_with Constraint1 if Condition1.
...
label_with ConstraintN if ConditionN.
Constraint1 :- Body1.
...
ConstraintN :- BodyN.
\end{code}

\noindent
is transformed into
\begin{code}
:- chr_constraint my_labeling/0.

my_labeling \ Constraint1 <=> Condition1 | Body1.
...
my_labeling \ ConstraintN <=> ConditionN | BodyN.
my_labeling <=> true.
\end{code}

\noindent
Be sure to put this code after all other rules in your program! With \nopredref{my_labeling}{0}
(or another predicate name of your choosing) the labeling is initiated, rather than ECLiPSe's
\nopredref{chr_labeling}{0}.

\section{CHR Programming Tips and Tricks}		\label{sec:chr-guidelines}
%==================

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

\begin{itemlist}

   \item [Check guard bindings yourself]
It is considered bad practice to write guards that bind variables of
the head and to rely on the system to detect this at runtime. It is
inefficient and obscures the working of the program.

    \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: \[ constraint \backslash constraint <=> true \]

    \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 (\cmdlineoption{--no-debug}) and enable
optimization (\cmdlineoption{-O}).

    \item [Compile once, run many times]
Does consulting your CHR program take a long time in SWI-Prolog? Probably
it takes the CHR compiler a long time to compile the CHR rules into Prolog
code. When you disable optimizations the CHR compiler will be a lot quicker,
but you may lose performance. Alternatively, you can just use SWI-Prolog's
\index{qcompile/1}\predref{qcompile}{1} to generate a \fileext{qlf} file once from your
\fileext{pl} file. This \fileext{qlf} contains the generated code of the
CHR compiler (be it in a binary format). When you consult the \fileext{qlf}
file, the CHR compiler is not invoked and consultation is much faster.

    \item [Finding Constraints]
The \predref{find_chr_constraint}{1} predicate is fairly expensive. Avoid it,
if possible. If you must use it, try to use it with an instantiated top-level
constraint symbol.
\end{itemlist}

\section{CHR Compiler Errors and Warnings}		\label{sec:chr-warnings-and-errors}
%==================

In this section we summarize the most important error and warning messages
of the CHR compiler.

\subsection{CHR Compiler Errors}
\label{sec:chr-errors}

\begin{description}
\item[Type clash] for variable ... in rule ...

	This error indicates an inconsistency between declared types;
	a variable can not belong to two types. See static type
	checking.

\item[Invalid functor] in head ... of rule ...

	This error indicates an inconsistency between a declared type
	and the use of a functor in a rule. See static type checking.

\item[Cyclic alias] definition: ... == ...

	You have defined a type alias in terms of itself, either
	directly or indirectly.

\item[Ambiguous type aliases]

	You have defined two overlapping type aliases.

\item[Multiple definitions] for type

	You have defined the same type multiple times.

\item[Non-ground type] in constraint definition: ...

	You have declared a non-ground type for a constraint argument.

\item[Could not find type definition] for ...

	You have used an undefined type in a type declaration.

\item[Illegal mode/type declaration]

	You have used invalid syntax in a constraint declaration.

\item[Constraint multiply defined]

	There is more than one declaration for the same constraint.

\item[Undeclared constraint] ... in head of ...

	You have used an undeclared constraint in the head of a rule.
	This often indicates a misspelled constraint name or wrong
	number of arguments.

\item[Invalid pragma] ... in ... Pragma should not be a variable.

	You have used a variable as a pragma in a rule. This is not
	allowed.

\item[Invalid identifier] ... in pragma passive in ...

	You have used an identifier in a passive pragma that
	does not correspond to an identifier in the head of the rule.
	Likely the identifier name is misspelled.

\item[Unknown pragma] ... in ...

	You have used an unknown pragma in a rule. Likely the
	pragma is misspelled or not supported.

\item[Something unexpected] happened in the CHR compiler

	You have most likely bumped into a bug in the CHR compiler.
	Please contact Tom Schrijvers to notify him of this error.

\end{description}