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 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 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.
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.
