For instance, consider:
t(X) :- X #= 1.
We *cannot* expand this to:
?- listing(t/1).
t(A) :-
( integer(A) ->
A=:=A
; ( var(A) ->
true
; true,
clpz:clpz_equal(A,A)
)
).
Also, a new binding *must not* be dragged outside of disjunctions,
since the code may look for example like this:
i(X) :-
( X #= 3
; X #= 4
).
This commit fixes such issues, and still rewrites CLP(ℤ) expressions
as far as possible already at compilation time.
For example:
n(X) :- X #= 1+3.
This is now compiled to (note that 1+3 is evaluated to 4):
?- listing(n/1).
n(A) :-
( integer(A) ->
A=:=4
; ( var(A) ->
A=4
; B=4,
clpz:clpz_equal(A,B)
)
).
Ideally, it should be compiled to:
n(4).
library(clpz) implements declarative integer arithmetic.
The most important predicates for reasoning about integers are:
(#=)/2 equality
(#\=)/2 disequality
(#<)/2 less than
(#>)/2 greater than
(#=<)/2 less than or equal to
(#>=)/2 greater than or equal to
In addition, the library provides several global constraints, such as
all_distinct/1 and global_cardinality/2, and reification predicates
that reflect the truth values of constraints into integer variables.
Enumeration predicates such label/1 and labeling/2 can be used to
search for solutions over finite domains.
Almost all Prolog programs also reason about integers. Therefore, I
recommend to add this library to your .scryerrc configuration file so
that declarative integer arithmetic is available in all your programs.
More information about CLP(ℤ):
https://www.metalevel.at/prolog/clpz
Enjoy!
