mthom
Variable bindings are sometimes unexpectedly lost
The following could be due to the same underlying issue as #1605. However, I file it as a separate issue because the observed result is somewhat different.
To reproduce this issue, please consider the following program:
:- use_module(library(clpz)).
:- use_module(library(format)).
:- use_module(library(between)).
p(B, N, P, I) :-
( integer(B) ->
between(0,255,B)
; clpz:clpz_in(B,0..255)
),
B is I mod 256,
( integer(_),
false
-> ...
; portray_clause(t(B,N,P)),
false
-> ...
; true
).
With the rebis-dev branch, I unexpectedly get:
?- p(B, 0, 0, 0). t(0,0,A). B = 0.
The variable A which occurs in the output of portray_clause/1 is unexpected, since P ought to be the concrete integers 0, not a variable.
Surprisingly, we get the expected output if we add for example the (entailed) constraint N=N as follows:
p(B, N, P, I) :-
( integer(B) ->
between(0,255,B)
; clpz:clpz_in(B,0..255)
),
B is I mod 256,
N = N,
( integer(_),
false
-> ...
; portray_clause(t(B,N,P)),
false
-> ...
; true
).
Yielding:
?- p(B, 0, 0, 0). t(0,0,0). B = 0.
Note how, instead of A, we now correctly see 0 as the last argument of the emitted t/3 term.
We also get the expected output by various other modifications to the original program. For instance, the following generalization of the program (where I generalized away the entire first goal, i.e., the first 4 lines of the body, using (*)/1 from library(debug) yields the intended output:
p(B, N, P, I) :-
* ( integer(B) ->
between(0,255,B)
; clpz:clpz_in(B,0..255)
),
B is I mod 256,
( integer(_),
false
-> ...
; portray_clause(t(B,N,P)),
false
-> ...
; true
).
These phenomenona also occur on master, and seem to indicate a rather elementary mistake at some level in the engine.
This concrete example, by itself, may look extremely contrived and not very important in itself. However, I actually distilled the example from a case that occurred in a real program, namely:
:- use_module(library(clpz)).
:- use_module(library(lists)).
:- use_module(library(time)).
bytes_integer(Bs, N) :-
foldl(pow, Bs, t(0,0,N), t(N,_,_)).
pow(B, t(N0,P0,I0), t(N,P,I)) :-
B in 0..255,
B #= I0 mod 256,
N #= N0 + B*256^P0,
P #= P0 + 1,
I #= I0 >> 8.
rel(N, N0, B, P0) :-
N #= N0 + B*256^P0.
With the rebis-dev branch, I unexpectedly get:
?- I is 256^200+2, time(bytes_integer(Bs, I)). % CPU time: 0.383s ...
What is unexpected about this? (The result is correct!) Well, it's much slower than expected!
For comparison, if I slightly change the code by introducing an auxiliary predicate for the goal in pow/3 which is highlighted in bold in the above snippet, and write instead (equivalently!):
pow(B, t(N0,P0,I0), t(N,P,I)) :-
B in 0..255,
B #= I0 mod 256,
rel(N, N0, B, P0),
P #= P0 + 1,
I #= I0 >> 8.
rel(N, N0, B, P0) :-
N #= N0 + B*256^P0.
Then I get:
?- I is 256^200+2, time(bytes_integer(Bs, I)). % CPU time: 0.027s ...
i.e., a program that is more than 10 times faster!
The reason is that all these integer constraints from library(clpz) make extensive use of goal expansion. For example, rel/4 is goal-expanded to:
?- clause(rel(N,N0,B,P0), Body). Body = (integer(N)->(((integer(N0),integer(B)),integer(P0)),(P0>=0;256=:= -1)->N=:=N0+B*256^P0;_A is N,clpz:clpz_equal(_A,N0+B*256^P0));((integer(N0),integer(B)),integer(P0)),(P0>=0;256=:= -1)->(true,var(N)->N is N0+B*256^P0;_A is N0+B*256^P0,clpz:clpz_equal(N,_A));clpz:clpz_equal(N,N0+B*256^P0)).
And somewhere in the expanded code which involves many conditions and arithmetic experssions, the variable bindings are unexpectedly lost!
I am posting this so that the casual reader does not walk away with the impression that this is some rare case that does not occur in practice. Such constructs occur in all programs that use library(clpz) constraints, and typically in code that is automatically generated at compilation time via goal expansion.