Unification may fail with user attributes
jeshan opened this issue · 4 comments
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?
Lines 7385 to 7388 in 281aaf0
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)
.
Thank you a lot for looking into this, I greatly appreciate your help!
pred1
is the only minimal test case that I can find so far 😓
The fix for scryer seems to work: mthom/scryer-prolog#420
Should I submit a PR that copies that fix into this repo?
Yes please do, thank you a lot!