{"action":"created","issue":{"url":"https://api.github.com/repos/SWI-Prolog/swipl-devel/issues/108","labels_url":"https://api.github.com/repos/SWI-Prolog/swipl-devel/issues/108/labels{/name}","comments_url":"https://api.github.com/repos/SWI-Prolog/swipl-devel/issues/108/comments","events_url":"https://api.github.com/repos/SWI-Prolog/swipl-devel/issues/108/events","html_url":"https://github.com/SWI-Prolog/swipl-devel/issues/108","id":127754777,"number":108,"title":"put_attr/3 within verify_attributes/3 may yield wrong results","user":{"login":"triska","id":7482140,"avatar_url":"https://avatars.githubusercontent.com/u/7482140?v=3","gravatar_id":"","url":"https://api.github.com/users/triska","html_url":"https://github.com/triska","followers_url":"https://api.github.com/users/triska/followers","following_url":"https://api.github.com/users/triska/following{/other_user}","gists_url":"https://api.github.com/users/triska/gists{/gist_id}","starred_url":"https://api.github.com/users/triska/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/triska/subscriptions","organizations_url":"https://api.github.com/users/triska/orgs","repos_url":"https://api.github.com/users/triska/repos","events_url":"https://api.github.com/users/triska/events{/privacy}","received_events_url":"https://api.github.com/users/triska/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":116,"created_at":"2016-01-20T18:37:48Z","updated_at":"2016-01-29T21:51:00Z","closed_at":null,"body":"Let `sat3.pl` consist of the following program:\r\n\r\n    :- use_module(library(clpfd)).\r\n\r\n    sat(X) :- X in 0..9.\r\n\r\n    num(L) :-\r\n            solve(As,Bs,Cs,Ds),\r\n            append([As,Bs,Cs,Ds], Vs),\r\n            findall(., labeling([ff,enum], Vs), Ls),\r\n            length(Ls, L).\r\n\r\n    solve([A1,A2,A3,A4],[B1,B2,B3,B4],[C1,C2,C3,C4],[D1,D2,D3,D4]) :-\r\n            maplist(sat, [A1,A2,A3,A4,B1,B2,B3,B4,C1,C2,C3,C4,D1,D2,D3,D4]),\r\n            A1 #=< D4,\r\n            A1 #=< D1,\r\n            A1 + A2 + A3 + A4 #= B1 + B2 + B3 + B4,\r\n            A1 + A2 + A3 + A4 #= C1 + C2 + C3 + C4,\r\n            A1 + A2 + A3 + A4 #= D1 + D2 + D3 + D4,\r\n            A1 + A2 + A3 + A4 #= A1 + B1 + C1 + D1,\r\n            A1 + B1 + C1 + D1 #= A2 + B2 + C2 + D2,\r\n            A1 + B1 + C1 + D1 #= A3 + B3 + C3 + D3,\r\n            A1 + B1 + C1 + D1 #= A4 + B4 + C4 + D4,\r\n            A1 + A2 + A3 + A4 #= A1 + B2 + C3 + D4,\r\n            A1 + B2 + C3 + D4 #= A4 + B3 + C2 + D1.\r\n\r\nPlease try it with the latest git version:\r\n\r\n<pre>\r\n$ swipl -O sat3.pl\r\nWelcome to SWI-Prolog (Multi-threaded, 64 bits, Version 7.3.15-13-ga4b7b09-DIRTY)\r\n...\r\n\r\n?- time(num(N)).\r\n% 29,869,788,769 inferences, 4345.776 CPU in 4346.341 seconds (100% CPU, 6873293 Lips)\r\nN = <b>2715884</b>.\r\n</pre>\r\n\r\nUnfortunately, this answer is **wrong**. There are actually 34 fewer solutions than this, i.e., the correct answer is&nbsp;**2715850**.\r\n\r\nThere is a surprising \"fix\" for this: Consider the current definition of `verify_attributes/3` in `library(clpfd)`, which is:\r\n\r\n<pre>\r\nverify_attributes(Var, Other, Gs) :-\r\n        (   get_attr(Var, clpfd, clpfd_attr(_,_,_,Dom,Ps0)) ->\r\n            (   nonvar(Other) ->\r\n                (   integer(Other) -> true\r\n                ;   type_error(integer, Other)\r\n                ),\r\n                domain_contains(Dom, Other),\r\n                Ps = Ps0\r\n            ;   fd_get(Other, OD, OPs),\r\n                domains_intersection(OD, Dom, Dom1),\r\n                append_propagators(Ps0, OPs, Ps),\r\n                <b>fd_put(Other, Dom1, Ps)</b>\r\n            ),\r\n            phrase(all_propagators(Ps), Gs, [do_queue])\r\n        ;   Gs = []\r\n        ).\r\n</pre>\r\n\r\nI have highlighted one important feature of this code: It associates the `Other` variable with a new domain, using `put_attr/3`&nbsp;(via `fd_put/3`). Using `put_attr/3` either directly or indirectly within `verify_attributes/3` is a completely natural and important operation when writing constraint solvers, and also the example code in `attvar.doc` shows such usage to propagate domain changes. **After** `Var` is unified with `Other` and `verify_attributes/3` has succeeded, we expect **both** variables (which are then of course aliased) to have the attributes that `Other` has after `verify_attributes/3`.\r\n\r\nIn other words, we expect the above definition of `verify_attributes/3` to be **equivalent** to the following definition, where the changes are shown in bold:\r\n\r\n<pre>\r\nverify_attributes(Var, Other, Gs) :-\r\n        (   get_attr(Var, clpfd, clpfd_attr(_,_,_,Dom,Ps0)) ->\r\n            (   nonvar(Other) ->\r\n                (   integer(Other) -> true\r\n                ;   type_error(integer, Other)\r\n                ),\r\n                domain_contains(Dom, Other),\r\n                Ps = Ps0,\r\n                <b>Gs = Gs1</b>\r\n            ;   fd_get(Other, OD, OPs),\r\n                domains_intersection(OD, Dom, Dom1),\r\n                append_propagators(Ps0, OPs, Ps),\r\n                <b>Gs = [fd_put(Other, Dom1, Ps)|Gs1]</b>\r\n            ),\r\n            phrase(all_propagators(Ps), <b>Gs1</b>, [do_queue])\r\n        ;   Gs = []\r\n        ).\r\n</pre>\r\n\r\nNote the main difference to the version above: Using the continuation goals, the call of `fd_put/3` is now delayed until **after** `verify_attributes/3`.\r\n\r\nIf we run the same query with this changed definition of `verify_attributes/3`, then we get the **correct** answer:\r\n\r\n<pre>\r\n?- time(num(N)).\r\n% 29,869,214,243 inferences, 4366.628 CPU in 4367.189 seconds (100% CPU, 6840338 Lips)\r\nN = <b>2715850</b>.\r\n</pre>\r\n\r\nI am only showing this \"fix\" in the hope that it helps to find the actual cause of this. In actuality, the two versions should of course be completely equivalent.\r\n\r\nA bit more information about this: CLP(FD) propagators, and in particular intersections of domains as they take place in `verify_attributes/3`, are **monotonic** operations. This means that performing them can at most **decrease**, never *increase* the number of solutions.\r\n\r\nSince the wrong answer shows **more** solutions than the correct one, it seems that SWI may in some cases get confused about which attributes are actually attached to a given variable. It may for instance in some cases put the the attributes of `Var` onto `Other` instead of the other way around, or become confused when backtracking over such a unification. The fact that the wrong answer is actually quite close to the correct one also suggests that this may happen only in very specific cases. \r\n\r\nMany thanks in advance for any help with this!"},"comment":{"url":"https://api.github.com/repos/SWI-Prolog/swipl-devel/issues/comments/176985011","html_url":"https://github.com/SWI-Prolog/swipl-devel/issues/108#issuecomment-176985011","issue_url":"https://api.github.com/repos/SWI-Prolog/swipl-devel/issues/108","id":176985011,"user":{"login":"JanWielemaker","id":3071146,"avatar_url":"https://avatars.githubusercontent.com/u/3071146?v=3","gravatar_id":"","url":"https://api.github.com/users/JanWielemaker","html_url":"https://github.com/JanWielemaker","followers_url":"https://api.github.com/users/JanWielemaker/followers","following_url":"https://api.github.com/users/JanWielemaker/following{/other_user}","gists_url":"https://api.github.com/users/JanWielemaker/gists{/gist_id}","starred_url":"https://api.github.com/users/JanWielemaker/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/JanWielemaker/subscriptions","organizations_url":"https://api.github.com/users/JanWielemaker/orgs","repos_url":"https://api.github.com/users/JanWielemaker/repos","events_url":"https://api.github.com/users/JanWielemaker/events{/privacy}","received_events_url":"https://api.github.com/users/JanWielemaker/received_events","type":"User","site_admin":false},"created_at":"2016-01-29T21:51:00Z","updated_at":"2016-01-29T21:51:00Z","body":"On 01/29/2016 09:52 PM, logicmoo wrote:\n>     My intuition is that the simple register wakeup and no-binding\n>     approach will not be sound. The approach I outlined that uses the\n>     trail to build the wakeup is sound (I think) and minimizes wakeups,\n>     but does not allow for the dirty tricks where verify_attributes/2\n>     does not call attv_unify(Var Value) Douglas is keen about for the\n>     case where an attributed variable is unified with multiple different\n>     values between two wakeups. One option might be to have a\n>     declaration that some attribute will not call attv_unify(Var Value).\n>     Not sure how to handle that though.\n> \n> I can compromise and be OK with using term_expansion/ goal_expansion in\n> /my/ code to linearize the args of programs that I load. As long as I\n> get to make the choice on attv_unify/2.\n\nThat might open doors :)\n\n> But i have a suspicion Markus might not be OK with some of this:\n> \n> Take this example:\n> \n> |[X,Y]=[1,2] , X=Y. |\n> \n> will not be the same as\n> \n> |X=Y , [X,Y]=[1,2] . |\n\nCan we find a real example?  The above two will fail anyway.  I can\nthink of `f(X,Y) = f(1,1), X = Y` and the swapped versions.  This\nboils down to `X=1,Y=1,X=Y` and `X=Y,X=1` but the constraint solver\nmust ensure these two things are the same anyway.\n"}}