- Reference manual
- The SWI-Prolog library
- Reference manual
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.8.12).
- #\ +Q
- Q does not hold. See reification (section
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
?- 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.8.12).
- ?P #<== ?Q
- Q implies P. See reification (section A.8.12).
- ?P #/\ ?Q
- P and Q hold. See reification (section A.8.12).
- ?P #\/ ?Q
- P or Q holds. See reification (section
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.8.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
=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.8.2). See reification (section A.8.12). However, zcompare/3 lets you more conveniently distinguish the cases.