triska / clpz

Constraint Logic Programming over Integers
https://www.metalevel.at/prolog/clpz
184 stars 15 forks source link

Unification may fail with user attributes #27

Open jeshan opened 10 months ago

jeshan commented 10 months ago

I've found that we have a situation where unification could fail if a custom attribute is added before a clpz constraint is posted.

Consider this code

:- use_module(library(atts)).
:- use_module(library(clpz)).

:- attribute some_attr/0.

verify_attributes(_Var1, _Var2, []). % to satisfy pred3

pred1 :- % fails
    put_atts(A, some_attr),
    B #= _,
    A = B.

pred2 :- % works (but pointless)
    B #= _,
    _A = B.

pred3 :- % works
    B #= _,
    put_atts(A, some_attr),
    A = B.

pred4 :- % works
    A #= _,
    put_atts(A, some_attr),
    B #= _,
    A = B.

Running this on sicstus, we see that only pred1 fails. However swapping a goal (like pred3) or declare the var as a clpz constraint first (like pred4) works!

Output:

[jeshan@pc ~]$ sicstus --nologo --noinfo -l hello.pl --goal pred1.
* user:pred1 - goal failed
| ?- [jeshan@pc ~]$ sicstus --nologo --noinfo -l hello.pl --goal pred2.
| ?- [jeshan@pc ~]$ sicstus --nologo --noinfo -l hello.pl --goal pred3.
| ?- [jeshan@pc ~]$ sicstus --nologo --noinfo -l hello.pl --goal pred4.
| ?- [jeshan@pc ~]$ 

I'm not familiar with the clpz code but could it be because you assumed that variables_same_queue([Var,Other]) would always hold here?

https://github.com/triska/clpz/blob/281aaf0841729e159bb0e978c61e990781889132/clpz.pl#L7385-L7388

Am I reading this correctly or should the bug be fixed in my code?

_Update: I've found that it makes a difference if the clpz var is either on left-hand side of X#=Y or right-hand side. If I have a specific example, I'll add it but I think you'll know that it's about verify_attributes implementation which may not have been tested for if Var and Other have been swapped in verify_attributes(Var, Other, Gs)._

triska commented 10 months ago

Thank you a lot for looking into this, I greatly appreciate your help!

jeshan commented 9 months ago

pred1 is the only minimal test case that I can find so far :sweat:

jeshan commented 9 months ago

The fix for scryer seems to work: https://github.com/mthom/scryer-prolog/pull/420 Should I submit a PR that copies that fix into this repo?

triska commented 9 months ago

Yes please do, thank you a lot!