clpz icon indicating copy to clipboard operation
clpz copied to clipboard

Unification may fail with user attributes

Open jeshan opened this issue 5 months ago • 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?

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).

jeshan avatar Jan 13 '24 22:01 jeshan