:- use_module(library(clpfd)).
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.8.2). See reification (section
A.8.12). However, zcompare/3
lets you more conveniently distinguish the cases.