Did you know ... | Search Documentation: |

Predicate zcompare/3 |

Availability:

`:- 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.9.2). See reification (section
A.9.12). However, zcompare/3
lets you more conveniently distinguish the cases.

Tags are associated to your profile if you are logged in

Tags: