Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Unification may fail with user attributes #27

Open
jeshan opened this issue Jan 13, 2024 · 4 comments · May be fixed by #30
Open

Unification may fail with user attributes #27

jeshan opened this issue Jan 13, 2024 · 4 comments · May be fixed by #30

Comments

@jeshan
Copy link

jeshan commented Jan 13, 2024

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?

clpz/clpz.pl

Lines 7385 to 7388 in 281aaf0

variables_same_queue([Var,Other]),
phrase((fd_put(Other,Dom1,Ps1),
trigger_props(Ps1)), [Q0], _),
Gs = [phrase(do_queue, [Q0], _)]

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
Copy link
Owner

triska commented Jan 14, 2024

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

@jeshan
Copy link
Author

jeshan commented Jan 23, 2024

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

@jeshan
Copy link
Author

jeshan commented Jan 23, 2024

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

@triska
Copy link
Owner

triska commented Feb 3, 2024

Yes please do, thank you a lot!

jeshan pushed a commit to jeshan/clpz that referenced this issue Feb 5, 2024
@jeshan jeshan linked a pull request Feb 5, 2024 that will close this issue
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants