Bug in tuples_in/2 of CLP(FD)
leuschel opened this issue · 13 comments
According to my understanding of tuples_in/2 this behaviour is not correct:
?- tuples_in([[A,B]],[[11,0],[12,1]]), tuples_in([[A,B]],[[12,0],[13,1]]).
A = 12,
B = 1.
?- tuples_in([[A,B]],[[11,0],[12,2]]), tuples_in([[A,B]],[[12,0],[13,1]]).
A = 12,
B = 2.
Funnily enough, here it corresponds to my understanding:
?- tuples_in([[A,B]],[[11,0],[12,2]]), tuples_in([[A,B]],[[12,1],[13,1]]).
false.
Version info:
$ swipl --version
SWI-Prolog version 9.0.3 for fat-darwin
Reproduces in the latest version (not a surprise, clp(fd) didn't change). If I read the docs correctly, you are right. @triska, would you agree?
Here another example, maybe it helps detecting the cause:
?- tuples_in([[A,B]],[[13,10],[122,2]]), tuples_in([[A,B]],[[13,2]]).
A = 13,
B = 10.
In these examples, there are pending unsatisfiable constraints which SWI-Prolog does not show, it instead shows incorrect answers.
For comparison, I get with Scryer Prolog:
?- tuples_in([[A,B]],[[11,0],[12,1]]), tuples_in([[A,B]],[[12,0],[13,1]]). A = 12, B = 1, clpz:put_atts(_A,clpz_relation([[11,0],[12,1]])), clpz:put_atts(_B,clpz_relation([[12,0]])).
The answer is correct in the sense that it is equivalent to the query, and the residual constraints are unsatisfiable in this case.
The constraint solver could, and arguably should, propagate more strongly in this case, and simply fail in this example. At the same time, unsatisfiable residual goals that succeed conditionally are not unusual, and not limited to this concrete example. For instance, consider this example program:
p :-
X #> Y,
X #< Y.
SWI-Prolog incorrectly yields:
?- p. true, unexpected.
For comparison, Scryer Prolog yields:
?- p. clpz:(_A#=<_B+ -1), clpz:(_B#=<_A+ -1).
This is achieved by wrapping toplevel queries in call_residue_vars/2 and displaying pending constraints.
How strongly a particular constraint propagates may change over time. I will look into this example and see what it would take to implement stronger propagation. It is always a trade-off between strength, efficiency and complexity, and necessarily remains undecidable in general for constraints over integers. As a workaround in the meantime, you can manually wrap the goals you post in call_residue_vars/2, and see whether there are pending unsatisfiable constraints, a task that a correct Prolog toplevel would perform for you.
Note that the wrong solution remains even after labeling is done; I would not expect that CLP(FD) has pending co-routines after labeling:
?- tuples_in([[A,B]],[[13,10],[12,2]]), tuples_in([[A,B]],[[13,2]]), labeling([],[A,B]).
A = 13,
B = 10.
Also note that ProB uses call_residure_vars to detect pending co-routines and create a warning. However, this did not seem be triggered (in the initial more complex context where I first uncovered the bug).
The SWI-Prolog toplevel does not show all pending constraints. For comparison, with Scryer Prolog:
?- tuples_in([[A,B]],[[13,10],[12,2]]), tuples_in([[A,B]],[[13,2]]), labeling([],[A,B]). A = 13, B = 10, clpz:put_atts(_A,clpz_relation([[13,10],[12,2]])), clpz:put_atts(_B,clpz_relation([[13,2]])).
So, a conditional answer.
I guess there are some existentially quantified internal variables that are not labelled:
?- call_residue_vars((tuples_in([[A,B]],[[13,10],[12,2]]), tuples_in([[A,B]],[[13,2]]), labeling([],[A,B])),CV).
A = 13,
B = 10,
CV = [_, _].
Note in SICStus we get
| ?- table([[A,B]],[[13,10],[12,2]]).
A in 12..13,
B in{2}\/{10} ?
yes
| ?- table([[A,B]],[[13,10],[12,2]]), table([[A,B]],[[13,2]]).
no
I think I addressed this in mthom/scryer-prolog@5dce7d9.
The key change is that Firsts = [Unique] -> T = Unique is performed under all circumstances (not only if T is a variable).
If possible, could you please try the analogous change with clpfd.pl, and see how that works?
If possible, could you please try the analogous change with
clpfd.pl, and see how that works?
Thanks. Works fine on the example by @leuschel and the examples from the documentation. See #1161. Is there any danger applying this?
The SWI-Prolog toplevel does not show all pending constraints. For comparison, with Scryer Prolog
I vaguely recalled there was some flag for this. Indeed. In was not documented though. Added to the docs.
?- set_prolog_flag(toplevel_residue_vars, true).
It is by default not on because call_residue_vars/2 it is not free. It requires additional data to keep track of attributed variables and negatively affects garbage collection.
It was always my understanding that a well-behaved constraint program does not leave residual variables behind that are not reachable from its arguments and call_residue_vars/2 is (thus) only required for debugging purposes. Is that wrong?
Is there any danger applying this?
Personally, I think it is OK to apply it! The main open question is whether there are other cases where tuples_in/2 can be rightfully expected to propagate more strongly. So, if anyone finds such issues, please do report them.
It was always my understanding that a well-behaved constraint program does not leave residual variables behind that are > not reachable from its arguments and call_residue_vars/2 is (thus) only required for debugging purposes. Is that wrong?
If we expect the key invariant of a Prolog toplevel to hold, i.e., that answers are declaratively equivalent to queries, then we must use call_residue_vars/2 by default so that all pending constraints are reliably reported in all cases. One of the simplest programs to test this is:
p :- freeze(_, false).
A correct Prolog toplevel, such as the one provided by Scryer or SICStus Prolog, yields for example:
?- p. freeze:freeze(_A,false).
The most important feature of a toplevel is arguably that it yields correct results. You may want to provide a flag to disable correct behaviour, so that wrong answers are computed very efficiently.
Personally, I think it is OK to apply it!
Thanks. Done.
SICStus Prolog, yields for example:
Not my copy (4.6.0) 😄 I have my doubt about this. In my view a program that introduced constraints that are never triggered is buggy. Printing these is useful for debugging. debug' mode is also useful for debugging, but we do not enable it by default because it makes the program behave different wrt. resource usage (time and space). It could be an option to enable printing residuals by default when the toplevel is in debug mode. Surely the impact of wrapping in call_residue_vars/2is way smaller than that ofdebug` mode.
Closing this issue as the problem reported is fixed.
Not my copy (4.6.0)
Both 4.4.1 and 4.8 :
| ?- [user].
% compiling user...
| p:-freeze(_,false).
|
% compiled user in module user, 129 msec 549456 bytes
yes
| ?- p.
prolog:freeze(_A,user:false) ?
yes