Previous: Constraint Satisfaction Problems, Up: CLPFD Interface [Contents][Index]

Instead of merely posting constraints it is often useful to reflect its
truth value into a 0/1-variable `B`, so that:

- the constraint is posted if
`B`is set to 1 - the negation of the constraint is posted if
`B`is set to 0 -
`B`is set to 1 if the constraint becomes entailed -
`B`is set to 0 if the constraint becomes disentailed

This mechanism is known as *reification*. Several frequently used
operations can be defined in terms of reified constraints. A reified
constraint is written:

| ?-Constraint#<=>B.

where `Constraint` is reifiable. As an example of a constraint that
uses reification, consider `exactly(`

,
defined to be true if `X`,`L`,`N`)`X` occurs exactly `N` times in the list
`L`. It can be defined thus:

exactly(_, [], 0). exactly(X, [Y|L], N) :- X #= Y #<=> B, N #= M+B, exactly(X, L, M).

Finally, reified constraints can be used as terms inside arithmetic expression. The value of the term is 1 if the constraint is true, and 0 otherwise. For example:

| ?-X #= 10, B #= (X#>=2) + (X#>=4) + (X#>=8).B = 3, X = 10

Send feedback on this subject.