In a constraint logic program, constraint handling is interleaved
with making choices. Typically, without making choices, constraint
problems cannot be solved completely. Labeling
is a controlled
way to make choices. Usually, a labeling predicate is called
at the end of the program which chooses values for the variables
constrained in the program.
We will understand labeling in the most general sense as a procedure
introducing arbitrary choices (additional constraints on constrained
variables) in a systematic way.
The CHR run-time system provides built-in labeling for
user-defined constraints. The idea is to write clauses for
user-defined constraints that are used for labeling the variables in
the constraint. These clauses are not used during constraint handling,
but only during built-in labeling. Therefore the “Head” of a clause may
be a user-defined “Constraint”.
The label_with declaration restricts the use of the
clauses for built-in labeling (see subsection on declarations). There
can be several label_with declarations for a constraint.
label_with minimum(X, Y, Z) if true.
minimum(X, Y, Z):- X leq Y, Z = X.
minimum(X, Y, Z):- Y lss X, Z = Y.
The built-in labeling is invoked by calling the CHR built-in predicate
chr_labeling/0 (no arguments). Once called, whenever no more
constraint handling is possible, the built-in labeling will choose a
constraint goal whose label_with declaration is satisfied for
labeling. It will introduce choices using the clauses of the constraint.
A query without and with built-in labeling:
[eclipse]: minimum(X,Y,Z), maximum(X,Y,W), Z neq W.
X = _g357
Y = _g389
Z = _g421
W = _g1227
(1) minimum(_g357, _g389, _g421)
(2) _g421 leq _g357
(3) _g421 leq _g389
(4) maximum(_g357, _g389, _g1227)
(5) _g357 leq _g1227
(7) _g389 leq _g1227
(10) _g421 lss _g1227
[eclipse]: minimum(X,Y,Z), maximum(X,Y,W), Z neq W, chr_labeling.
X = Z = _g363
Y = W = _g395
(10) _g363 lss _g395
X = W = _g363
Y = Z = _g395
(17) _g395 lss _g363
Advanced users can write their own labeling procedure taking into
account the constraints in the constraint store (see next subsection
for CHR built-in predicates to inspect and manipulate the constraint
The predicate chr_labeling/0 can be defined as: