Did you know ... | Search Documentation: |

Reification predicates |

- HOME
- DOWNLOAD
- DOCUMENTATION
- TUTORIALS
- Beginner▶
- Advanced▶
- Web applications▶
- Semantic web▶
- Graphics▶
- Machine learning▶
- External collections▶
- For packagers▶

- COMMUNITY
- COMMERCIAL
- WIKI

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

**#\**`+Q``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`**#<==>**`?Q``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`**#==>**`?Q``P`implies`Q`. See reification (section A.9.12).`?P`**#<==**`?Q``Q`implies`P`. See reification (section A.9.12).`?P`**#/\**`?Q``P`and`Q`hold. See reification (section A.9.12).`?P`**#\/**`?Q``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.

`?P`**#\**`?Q`- Either
`P`holds or`Q`holds, but not both. See reification (section A.9.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`<`

,`>`

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: