A.9.17.5 Reification predicates
AllApplicationManualNameSummaryHelp

  • Documentation
    • Reference manual
      • The SWI-Prolog library
        • library(clpfd): CLP(FD): Constraint Logic Programming over Finite Domains
          • CLP(FD) predicate index
            • Reification predicates
              • #\/1
              • #<==>/2
              • #==>/2
              • #<==/2
              • #/\/2
              • #\//2
              • #\/2
              • zcompare/3
    • Packages
Availability::- use_module(library(clpfd)).
Sourcezcompare(?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.