A.9.17.5 Reification predicates

Many CLP(FD) constraints can be reified. This means that their truth value is itself turned into a CLP(FD) variable, so that we can explicitly reason about whether a constraint holds or not. See reification (section A.9.12).

#\ +Q

Q does not hold. See reification (section A.9.12).

For example, to obtain the complement of a domain:

?- #\ X in -3..0\/10..80.
X in inf.. -4\/1..9\/81..sup.

?P #<==> ?Q

P and Q are equivalent. See reification (section A.9.12).

For example:

?- X #= 4 #<==> B, X #\= 4.
B = 0,
X in inf..3\/5..sup.

The following example uses reified constraints to relate a list of finite domain variables to the number of occurrences of a given value:

vs_n_num(Vs, N, Num) :-
        maplist(eq_b(N), Vs, Bs),
        sum(Bs, #=, Num).

eq_b(X, Y, B) :- X #= Y #<==> B.

Sample queries and their results:

?- Vs = [X,Y,Z], Vs ins 0..1, vs_n_num(Vs, 4, Num).
Vs = [X, Y, Z],
Num = 0,
X in 0..1,
Y in 0..1,
Z in 0..1.

?- vs_n_num([X,Y,Z], 2, 3).
X = 2,
Y = 2,
Z = 2.

?P #==> ?Q

P implies Q. See reification (section A.9.12).

?P #<== ?Q

Q implies P. See reification (section A.9.12).

?P #/\ ?Q

P and Q hold. See reification (section A.9.12).

?P #\/ ?Q

P or Q holds. See reification (section A.9.12).

For example, the sum of natural numbers below 1000 that are multiples of 3 or 5:

?- findall(N, (N mod 3 #= 0 #\/ N mod 5 #= 0, N in 0..999,
               indomain(N)),
           Ns),
   sum(Ns, #=, Sum).
Ns = [0, 3, 5, 6, 9, 10, 12, 15, 18|...],
Sum = 233168.

?P #\ ?Q

Either P holds or Q holds, but not both. See reification (section A.9.12).

zcompare(?Order, ?A, ?B)

Analogous to compare/3, with finite domain variables A and B.

Think of zcompare/3 as reifying an arithmetic comparison of two integers. This means that we can explicitly reason about the different cases within our programs. As in compare/3, the atoms <, > and = denote the different cases of the trichotomy. In contrast to compare/3 though, zcompare/3 works correctly for all modes, also if only a subset of the arguments is instantiated. This allows you to make several predicates over integers deterministic while preserving their generality and completeness. For example:

n_factorial(N, F) :-
        zcompare(C, N, 0),
        n_factorial_(C, N, F).

n_factorial_(=, _, 1).
n_factorial_(>, N, F) :-
        F #= F0*N,
        N1 #= N - 1,
        n_factorial(N1, F0).

This version of n_factorial/2 is deterministic if the first argument is instantiated, because argument indexing can distinguish the different clauses that reflect the possible and admissible outcomes of a comparison of N against 0. Example:

?- n_factorial(30, F).
F = 265252859812191058636308480000000.

Since there is no clause for <, the predicate automatically fails if N is less than 0. The predicate can still be used in all directions, including the most general query:

?- n_factorial(N, F).
N = 0,
F = 1 ;
N = F, F = 1 ;
N = F, F = 2 .

In this case, all clauses are tried on backtracking, and zcompare/3 ensures that the respective ordering between N and 0 holds in each case.

The truth value of a comparison can also be reified with (#<==>)/2 in combination with one of the arithmetic constraints (section A.9.2). See reification (section A.9.12). However, zcompare/3 lets you more conveniently distinguish the cases.