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

Attributed variables behaviour has changed unexpectedly #2732

Open
triska opened this issue Dec 30, 2024 · 3 comments
Open

Attributed variables behaviour has changed unexpectedly #2732

triska opened this issue Dec 30, 2024 · 3 comments

Comments

@triska
Copy link
Contributor

triska commented Dec 30, 2024

I noticed that in recent Scryer Prolog versions (v0.9.4-273), the following query works as expected even without e185b62 applied:

?- sat(A*B>=C*D), A=1,B=0,C=1,D=1.
   false. % expected

This means that there must have been a change that affects how attributed variables are handled, and which may have been unintentional and also have other effects.

As far as I remember, I found e185b62 to be justified back then (it was introduced to correct #670), and it now comes as a surprise to me that it is no longer necessary.

This is a low priority issue: Currently, everything works as expected in application code. Still, I would like to know what exactly caused this, and I would greatly appreciate your help with this. I recall that I thought Scryer followed the SICStus specification more closely than SICStus itself in that respect (the change was apparently not necessary for the SICStus version, even though it seemed its necessity was entailed by the SICStus documentation), and as a reference, it is always valuable to have a system that follows the specification as strictly as possible. If the previous behaviour was indeed more strictly following the specification of verify_attributes/3, then it would be valuable to have it reinstated if that is feasible.

@triska
Copy link
Contributor Author

triska commented Dec 30, 2024

I am now comparing this with older Scryer Prolog versions. Note that they are subject to #249 and #356, yielding unexpected existence errors. This problem can be mitigated by replacing the 3 goal expansions in library(clpb) with regular predicates:

get_attr(Var, Module, Value) :-
        Access =.. [Module,Value],
        var(Var),
        get_atts(Var, Access).

put_attr(Var, Module, Value) :-
        Access =.. [Module,Value],
        put_atts(Var, Access).

del_attr(Var, Module) :-
        Access =.. [Module,_],
        (   var(Var) -> put_atts(Var, -Access);true).

@triska
Copy link
Contributor Author

triska commented Dec 30, 2024

I have reduced it to the following test case:

  1. Check out library(clpb) from 099d9aa and apply the change mentioned in Attributed variables behaviour has changed unexpectedly #2732 (comment) to make it work in earlier version of Scryer Prolog.
  2. In verify_attributes/3, put a $ from library(debug) in front of the goal bdd_restriction(BDD0, I, Other, BDD).
  3. Post: ?- sat(A*B>=C*D), A=1, B=0.

With Scryer Prolog as it was in git commit 099d9aa, the output is:

call:bdd_restriction(node(9,A,1,node(8,B,1,node(7,C,0,node(6,D,0,1,E),F),G),H),2,1,I).
exit:bdd_restriction(node(9,A,1,node(8,B,1,node(7,C,0,node(6,D,0,1,E),F),G),H),2,1,node(11,A,1,node(10,B,1,node(6,D,0,1,E),I),J)).
call:bdd_restriction(node(11,A,1,node(10,B,1,node(6,C,0,1,D),E),F),3,0,G).
exit:bdd_restriction(node(11,A,1,node(10,B,1,node(6,C,0,1,D),E),F),3,0,node(11,A,1,node(10,B,1,node(6,C,0,1,D),E),F)).

Whereas with current master on the same file (i.e., library(clpb) as defined above, plus a small fix to avoid the use of (->)//2 in bdd_restriction_//4, see 665f319), the output is:

call:clpb:bdd_restriction(node(9,A,1,node(8,B,1,node(7,C,0,node(6,D,0,1,E),F),G),H),2,1,I).
exit:clpb:bdd_restriction(node(9,A,1,node(8,B,1,node(7,C,0,node(6,D,0,1,E),F),G),H),2,1,node(11,A,1,node(10,B,1,node(6,D,0,1,E),I),J)).
call:clpb:bdd_restriction(node(11,A,1,node(10,B,1,node(6,C,0,1,D),E),F),3,0,G).
exit:clpb:bdd_restriction(node(11,A,1,node(10,B,1,node(6,C,0,1,D),E),F),3,0,node(13,A,1,node(12,B,1,0,G),H)).

This is an unexpected difference in attributed variable handling between 099d9aa and the current master branch.

It may well be the case that master is correct. Independent of which version is correct, I would like to know which change(s) caused this difference, and whether they also have other unexpected effects.

triska added a commit to triska/scryer-prolog that referenced this issue Dec 31, 2024
This suffices to show a discrepancy. With Scryer Prolog built from the
previous commit, I get, after consulting this version of clpb.pl:

    ?- sat(A*B>=C*D), A=1,B=0.
    current_id_next_id('$clpb_next_var',0,1).
    current_id_next_id('$clpb_next_var',1,2).
    current_id_next_id('$clpb_next_var',2,3).
    current_id_next_id('$clpb_next_var',3,4).
    call:lookup_node(A,node(false,true),B).
    lookup_failed.
    current_id_next_id('$clpb_next_node',0,1).
    call:lookup_node(A,node(false,true),B).
    lookup_failed.
    current_id_next_id('$clpb_next_node',1,2).
    call:lookup_node(A,node(false,1),B).
    lookup_failed.
    current_id_next_id('$clpb_next_node',2,3).
    call:lookup_node(A,node(true,false),B).
    lookup_failed.
    current_id_next_id('$clpb_next_node',3,4).
    call:lookup_node(A,node(true,3),B).
    lookup_failed.
    current_id_next_id('$clpb_next_node',4,5).
    call:lookup_node(A,node(false,true),B).
    lookup_failed.
    current_id_next_id('$clpb_next_node',5,6).
    call:lookup_node(A,node(false,true),B).
    lookup_failed.
    current_id_next_id('$clpb_next_node',6,7).
    call:lookup_node(A,node(false,6),B).
    lookup_failed.
    current_id_next_id('$clpb_next_node',7,8).
    call:lookup_node(A,node(true,7),B).
    lookup_failed.
    current_id_next_id('$clpb_next_node',8,9).
    call:lookup_node(A,node(true,8),B).
    lookup_failed.
    current_id_next_id('$clpb_next_node',9,10).
    A = 1
    index(2)=1.
    start_bdd.
    node(9)-(v(A,0)->node(8);true).
    node(8)-(v(A,1)->node(7);true).
    node(7)-(v(A,2)->node(6);false).
    node(6)-(v(A,3)->true;false).
    end_bdd.
    restricting(2,1).
    call:bdd_restriction(node(9,A,1,node(8,B,1,node(7,C,0,node(6,D,0,1,E),F),G),H),2,1,I).
    call:make_node(A,1,node(6,B,0,1,C),D).
    call:lookup_node(A,node(true,6),B).
    lookup_failed.
    current_id_next_id('$clpb_next_node',10,11).
    exit:make_node(A,1,node(6,B,0,1,C),node(10,A,1,node(6,B,0,1,C),D)).
    call:make_node(A,1,node(10,B,1,node(6,C,0,1,D),E),F).
    call:lookup_node(A,node(true,10),B).
    lookup_failed.
    current_id_next_id('$clpb_next_node',11,12).
    exit:make_node(A,1,node(10,B,1,node(6,C,0,1,D),E),node(11,A,1,node(10,B,1,node(6,C,0,1,D),E),F)).
    exit:bdd_restriction(node(9,A,1,node(8,B,1,node(7,C,0,node(6,D,0,1,E),F),G),H),2,1,node(11,A,1,node(10,B,1,node(6,D,0,1,E),I),J)).
    start_bdd.
    node(11)-(v(A,0)->node(10);true).
    node(10)-(v(A,1)->node(6);true).
    node(6)-(v(A,3)->true;false).
    end_bdd.
    A = 0
    index(3)=0.
    start_bdd.
    node(11)-(v(A,0)->node(10);true).
    node(10)-(v(A,1)->node(6);true).
    node(6)-(v(A,3)->true;false).
    end_bdd.
    restricting(3,0).
    call:bdd_restriction(node(11,A,1,node(10,B,1,node(6,C,0,1,D),E),F),3,0,G).
    call:make_node(A,1,0,B).
    call:lookup_node(A,node(true,false),B).
    lookup_failed.
    current_id_next_id('$clpb_next_node',10,11).
    exit:make_node(A,1,0,node(10,A,1,0,B)).
    call:make_node(A,1,node(10,B,1,0,C),D).
    call:lookup_node(A,node(true,10),B).
    exit:lookup_node(A,node(true,10),node(11,A,1,node(10,B,1,node(6,C,0,1,D),E),F)).
    lookup_succeeded.
    exit:make_node(A,1,node(10,B,1,0,C),node(11,A,1,node(10,B,1,node(6,D,0,1,E),F),G)).
    exit:bdd_restriction(node(11,A,1,node(10,B,1,node(6,C,0,1,D),E),F),3,0,node(11,A,1,node(10,B,1,node(6,C,0,1,D),E),F)).
    start_bdd.
    node(11)-(v(A,0)->node(10);true).
    node(10)-(v(A,1)->node(6);true).
    node(6)-(v(A,3)->true;false).
    end_bdd.
    current_id_next_id('$clpb_next_var',4,5).
    current_id_next_id('$clpb_next_node',10,11).
    current_id_next_id('$clpb_next_var',4,5).
    current_id_next_id('$clpb_next_node',10,11).
       A = 1, B = 0, clpb:put_atts(C,clpb(index_root(0,_A))), clpb:put_atts(C,clpb_hash(t(node(true,8),node(9,C,1,node(8,D,A,node(7,A,0,node(6,B,B,A,_B),_C),_D),_E),>,t,t(node(true,10),node(11,C,A,node(10,D,A,node(6,B,B,A,_B),_F),_G),-,t,t)))), clpb:put_atts(D,clpb(index_root(1,_A))), clpb:put_atts(D,clpb_hash(t(node(true,7),node(8,D,1,node(7,A,0,node(6,B,B,A,_B),_C),_D),-,t(node(true,6),node(10,D,A,node(6,B,B,A,_B),_F),-,t,t),t(node(true,false),node(10,D,A,B,_H),-,t,t)))), clpb:put_atts(_A,clpb_bdd((1*0>=C*D)-node(11,C,A,node(10,D,A,node(6,B,B,A,_B),_F),_G)))
    ;  ...

Note that after B = 0 (index(3)=0.), the BDD is incorrectly
restricted, from:

    start_bdd.
    node(11)-(v(A,0)->node(10);true).
    node(10)-(v(A,1)->node(6);true).
    node(6)-(v(A,3)->true;false).
    end_bdd.

to the same BDD, i.e., again:

    start_bdd.
    node(11)-(v(A,0)->node(10);true).
    node(10)-(v(A,1)->node(6);true).
    node(6)-(v(A,3)->true;false).
    end_bdd.

It is still unclear why this happens. The mistake may be independent
of attributed variables. It may be because nodes are not correctly
found, or accidentally wrongly "found" during lookup. The fact that
"current_id_next_id(10,11)." appears after
"current_id_next_id(11,12)." may be related; this seems like another
severe (possibly separate) issue, because the ID counter is supposed
to be monotonically increasing.

For comparison, with the current master, I get, for the same file:

    ?- sat(A*B>=C*D), A=1,B=0.
    current_id_next_id('$clpb_next_var',0,1).
    current_id_next_id('$clpb_next_var',1,2).
    current_id_next_id('$clpb_next_var',2,3).
    current_id_next_id('$clpb_next_var',3,4).
    call:clpb:lookup_node(A,node(false,true),B).
    lookup_failed.
    current_id_next_id('$clpb_next_node',0,1).
    call:clpb:lookup_node(A,node(false,true),B).
    lookup_failed.
    current_id_next_id('$clpb_next_node',1,2).
    call:clpb:lookup_node(A,node(false,1),B).
    lookup_failed.
    current_id_next_id('$clpb_next_node',2,3).
    call:clpb:lookup_node(A,node(true,false),B).
    lookup_failed.
    current_id_next_id('$clpb_next_node',3,4).
    call:clpb:lookup_node(A,node(true,3),B).
    lookup_failed.
    current_id_next_id('$clpb_next_node',4,5).
    call:clpb:lookup_node(A,node(false,true),B).
    lookup_failed.
    current_id_next_id('$clpb_next_node',5,6).
    call:clpb:lookup_node(A,node(false,true),B).
    lookup_failed.
    current_id_next_id('$clpb_next_node',6,7).
    call:clpb:lookup_node(A,node(false,6),B).
    lookup_failed.
    current_id_next_id('$clpb_next_node',7,8).
    call:clpb:lookup_node(A,node(true,7),B).
    lookup_failed.
    current_id_next_id('$clpb_next_node',8,9).
    call:clpb:lookup_node(A,node(true,8),B).
    lookup_failed.
    current_id_next_id('$clpb_next_node',9,10).
    A = 1
    index(2)=1.
    start_bdd.
    node(9)-(v(A,0)->node(8);true).
    node(8)-(v(A,1)->node(7);true).
    node(7)-(v(A,2)->node(6);false).
    node(6)-(v(A,3)->true;false).
    end_bdd.
    restricting(2,1).
    call:clpb:bdd_restriction(node(9,A,1,node(8,B,1,node(7,C,0,node(6,D,0,1,E),F),G),H),2,1,I).
    call:clpb:make_node(A,1,node(6,B,0,1,C),D).
    call:clpb:lookup_node(A,node(true,6),B).
    lookup_failed.
    current_id_next_id('$clpb_next_node',10,11).
    exit:clpb:make_node(A,1,node(6,B,0,1,C),node(10,A,1,node(6,B,0,1,C),D)).
    call:clpb:make_node(A,1,node(10,B,1,node(6,C,0,1,D),E),F).
    call:clpb:lookup_node(A,node(true,10),B).
    lookup_failed.
    current_id_next_id('$clpb_next_node',11,12).
    exit:clpb:make_node(A,1,node(10,B,1,node(6,C,0,1,D),E),node(11,A,1,node(10,B,1,node(6,C,0,1,D),E),F)).
    exit:clpb:bdd_restriction(node(9,A,1,node(8,B,1,node(7,C,0,node(6,D,0,1,E),F),G),H),2,1,node(11,A,1,node(10,B,1,node(6,D,0,1,E),I),J)).
    start_bdd.
    node(11)-(v(A,0)->node(10);true).
    node(10)-(v(A,1)->node(6);true).
    node(6)-(v(A,3)->true;false).
    end_bdd.
    A = 0
    index(3)=0.
    start_bdd.
    node(11)-(v(A,0)->node(10);true).
    node(10)-(v(A,1)->node(6);true).
    node(6)-(v(A,3)->true;false).
    end_bdd.
    restricting(3,0).
    call:clpb:bdd_restriction(node(11,A,1,node(10,B,1,node(6,C,0,1,D),E),F),3,0,G).
    call:clpb:make_node(A,1,0,B).
    call:clpb:lookup_node(A,node(true,false),B).
    lookup_failed.
    current_id_next_id('$clpb_next_node',12,13).
    exit:clpb:make_node(A,1,0,node(12,A,1,0,B)).
    call:clpb:make_node(A,1,node(12,B,1,0,C),D).
    call:clpb:lookup_node(A,node(true,12),B).
    lookup_failed.
    current_id_next_id('$clpb_next_node',13,14).
    exit:clpb:make_node(A,1,node(12,B,1,0,C),node(13,A,1,node(12,B,1,0,C),D)).
    exit:clpb:bdd_restriction(node(11,A,1,node(10,B,1,node(6,C,0,1,D),E),F),3,0,node(13,A,1,node(12,B,1,0,G),H)).
    start_bdd.
    node(13)-(v(A,0)->node(12);true).
    node(12)-(v(A,1)->false;true).
    end_bdd.
    current_id_next_id('$clpb_next_var',4,5).
    current_id_next_id('$clpb_next_node',14,15).
    call:clpb:lookup_node(A,node(false,true),B).
    lookup_failed.
    current_id_next_id('$clpb_next_node',15,16).
    call:clpb:lookup_node(A,node(false,true),B).
    lookup_failed.
    current_id_next_id('$clpb_next_node',16,17).
    call:clpb:lookup_node(A,node(false,16),B).
    lookup_failed.
    current_id_next_id('$clpb_next_node',17,18).
    call:clpb:lookup_node(A,node(true,false),B).
    exit:clpb:lookup_node(A,node(true,false),node(12,A,1,0,B)).
    lookup_succeeded.
    call:clpb:lookup_node(A,node(true,12),B).
    exit:clpb:lookup_node(A,node(true,12),node(13,A,1,node(12,B,1,0,C),D)).
    lookup_succeeded.
    call:clpb:lookup_node(A,node(false,true),B).
    exit:clpb:lookup_node(A,node(false,true),node(15,A,0,1,B)).
    lookup_succeeded.
    call:clpb:lookup_node(A,node(false,true),B).
    exit:clpb:lookup_node(A,node(false,true),node(16,A,0,1,B)).
    lookup_succeeded.
    call:clpb:lookup_node(A,node(false,16),B).
    exit:clpb:lookup_node(A,node(false,16),node(17,A,0,node(16,B,0,1,C),D)).
    lookup_succeeded.
    call:clpb:lookup_node(A,node(true,false),B).
    exit:clpb:lookup_node(A,node(true,false),node(12,A,1,0,B)).
    lookup_succeeded.
    call:clpb:lookup_node(A,node(true,12),B).
    exit:clpb:lookup_node(A,node(true,12),node(13,A,1,node(12,B,1,0,C),D)).
    lookup_succeeded.
    call:clpb:make_node(A,1,1,B).
    exit:clpb:make_node(A,1,1,1).
    call:clpb:make_node(A,1,0,B).
    call:clpb:lookup_node(A,node(true,false),B).
    lookup_failed.
    current_id_next_id('$clpb_next_node',18,19).
    exit:clpb:make_node(A,1,0,node(18,A,1,0,B)).
       A = 1, B = 0, clpb:sat(1#C*D).

This shows the correct restriction of the above BDD:

    start_bdd.
    node(13)-(v(A,0)->node(12);true).
    node(12)-(v(A,1)->false;true).
    end_bdd.

Note also the strictly increasing node counter, ending at 19.
@triska
Copy link
Contributor Author

triska commented Dec 31, 2024

I have described everything I found out so far in dd41176b97d8369c3bb7de1c9932a9c3d10a0466.

In case anyone wants to take a look at this, I would greatly appreciate your help to narrow this down further, in particular finding the commit in Scryer Prolog that made it work as expected.

Also, I wish everyone a great slide into the Year 2025! Thank you all for your great contributions and for forming Scryer Prolog into such a fantastic Prolog system, please keep up the amazing work!

triska added a commit to triska/scryer-prolog that referenced this issue Jan 2, 2025
…ation."

This reverts commit e185b62.

This change is now no longer needed, and the underlying issue is
apparently somewhere else entirely. See the description at:

    mthom#2732

Current master behaves differently from Scryer as it was at
099d9aa (i.e., preceding
the commit that is now being reverted), even on the same file.

For an example, see:

    dd41176

Scryer now works as expected, and compatibly with SICStus. We still
need to find out what fixed the root cause of this issue.
triska added a commit to triska/scryer-prolog that referenced this issue Jan 2, 2025
…ation."

This reverts commit e185b62.

This change is now no longer needed, and the underlying issue is
apparently somewhere else entirely. See the description at:

    mthom#2732

Current master behaves differently from Scryer as it was at
099d9aa (i.e., preceding
the commit that is now being reverted), even on the same file.

For an example, see:

    dd41176

Scryer now works as expected, and compatibly with SICStus. We still
need to find out what fixed the root cause of 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

No branches or pull requests

1 participant