Previous: , Up: CLPFD Interface   [Contents][Index]

#### 10.10.3.4 Reified Constraints

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(X,L,N)`, defined to be true if 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.