search

SWI-Prolog / swipl-devel

SWI-Prolog Main development repository
http://www.swi-prolog.org
Other
956 stars 172 forks source link

put_attr/3 within verify_attributes/3 may yield wrong results #108

Closed triska closed 7 years ago

triska commented 8 years ago

Let sat3.pl consist of the following program:

:- use_module(library(clpfd)).

sat(X) :- X in 0..9.

num(L) :-
        solve(As,Bs,Cs,Ds),
        append([As,Bs,Cs,Ds], Vs),
        findall(., labeling([ff,enum], Vs), Ls),
        length(Ls, L).

solve([A1,A2,A3,A4],[B1,B2,B3,B4],[C1,C2,C3,C4],[D1,D2,D3,D4]) :-
        maplist(sat, [A1,A2,A3,A4,B1,B2,B3,B4,C1,C2,C3,C4,D1,D2,D3,D4]),
        A1 #=< D4,
        A1 #=< D1,
        A1 + A2 + A3 + A4 #= B1 + B2 + B3 + B4,
        A1 + A2 + A3 + A4 #= C1 + C2 + C3 + C4,
        A1 + A2 + A3 + A4 #= D1 + D2 + D3 + D4,
        A1 + A2 + A3 + A4 #= A1 + B1 + C1 + D1,
        A1 + B1 + C1 + D1 #= A2 + B2 + C2 + D2,
        A1 + B1 + C1 + D1 #= A3 + B3 + C3 + D3,
        A1 + B1 + C1 + D1 #= A4 + B4 + C4 + D4,
        A1 + A2 + A3 + A4 #= A1 + B2 + C3 + D4,
        A1 + B2 + C3 + D4 #= A4 + B3 + C2 + D1.

Please try it with the latest git version:

$ swipl -O sat3.pl
Welcome to SWI-Prolog (Multi-threaded, 64 bits, Version 7.3.15-13-ga4b7b09-DIRTY)
...

?- time(num(N)).
% 29,869,788,769 inferences, 4345.776 CPU in 4346.341 seconds (100% CPU, 6873293 Lips)
N = 2715884.

Unfortunately, this answer is wrong. There are actually 34 fewer solutions than this, i.e., the correct answer is 2715850.

There is a surprising "fix" for this: Consider the current definition of verify_attributes/3 in library(clpfd), which is:

verify_attributes(Var, Other, Gs) :-
        (   get_attr(Var, clpfd, clpfd_attr(_,_,_,Dom,Ps0)) ->
            (   nonvar(Other) ->
                (   integer(Other) -> true
                ;   type_error(integer, Other)
                ),
                domain_contains(Dom, Other),
                Ps = Ps0
            ;   fd_get(Other, OD, OPs),
                domains_intersection(OD, Dom, Dom1),
                append_propagators(Ps0, OPs, Ps),
                fd_put(Other, Dom1, Ps)
            ),
            phrase(all_propagators(Ps), Gs, [do_queue])
        ;   Gs = []
        ).

I have highlighted one important feature of this code: It associates the Other variable with a new domain, using put_attr/3 (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.

In 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:

verify_attributes(Var, Other, Gs) :-
        (   get_attr(Var, clpfd, clpfd_attr(_,_,_,Dom,Ps0)) ->
            (   nonvar(Other) ->
                (   integer(Other) -> true
                ;   type_error(integer, Other)
                ),
                domain_contains(Dom, Other),
                Ps = Ps0,
                Gs = Gs1
            ;   fd_get(Other, OD, OPs),
                domains_intersection(OD, Dom, Dom1),
                append_propagators(Ps0, OPs, Ps),
                Gs = [fd_put(Other, Dom1, Ps)|Gs1]
            ),
            phrase(all_propagators(Ps), Gs1, [do_queue])
        ;   Gs = []
        ).

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

If we run the same query with this changed definition of verify_attributes/3, then we get the correct answer:

?- time(num(N)).
% 29,869,214,243 inferences, 4366.628 CPU in 4367.189 seconds (100% CPU, 6840338 Lips)
N = 2715850.

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

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

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

Many thanks in advance for any help with this!

TeamSPoon commented 8 years ago

All of this has to do with eh fact that currently at least one variable and its attributes must be destroyed after verify_attributes/3 which i think is a shame. Not only that, you as a programmer are not even allowed to decide which of the two are destroyed which has made master unusable to me. I have made several patches that remove this limitation I am just not good yet at explaining the complexities.

triska commented 8 years ago

The SICStus documentation is very clear on the following point, and the invariant is easy to understand at least from the users' perspective:

When verify_attributes(Var, Value, Gs) is called, and Value is an attributed variable, then the definition is expected to "copy the attributes of Var over to Value, or merge them with Value's, in preparation for Var to be bound to Value."

This means that the attributes of Value, i.e., the second argument of verify_attributes/3 must be retained when the unification is performed after verify_attributes/3 has succeeded.

Is there a way to implement this semantics in master? Without this guarantee, the implementation is indeed unusable.

TeamSPoon commented 8 years ago

@triska is there a less time taking testcase that yields incorrect results in master that I may test with?

DouglasRMiles commented 8 years ago

You may try the patch shown @ https://github.com/SWI-Prolog/swipl-devel/compare/master...logicmoo:ATT_NO_SWAP

Also I did a couple tests at completely removing any swapping of attvars and it still passed make check but I didnt want to completely remove the reordering code as it might served some purpose in the past. But for now that will keep the variables from swapping durring $assign_attvar/2.

On Wed, Jan 20, 2016 at 7:20 PM, Douglas R. Miles notifications@github.com wrote:

@triska https://github.com/triska is there a less time taking testcase that yields incorrect results in master that I may test with?

— Reply to this email directly or view it on GitHub https://github.com/SWI-Prolog/swipl-devel/issues/108#issuecomment-173438607 .

JanWielemaker commented 8 years ago

On 21/01/16 11:40, logicmoo wrote:

You may try the patch shown @ https://github.com/SWI-Prolog/swipl-devel/compare/master...logicmoo:ATT_NO_SWAP

Also I did a couple tests at completely removing any swapping of attvars and it still passed make check but I didnt want to completely remove the reordering code as it might served some purpose in the past. But for now that will keep the variables from swapping durring $assign_attvar/2.

I fear this is incorrect. If causes reference pointer to point upward and these beasts must point downwards to ensure they remain consistent during backtracking. That is why the swap is there ...

Seems we'll have to migrate the attributes to the other variable.

Cheers --- Jan

P.s. Can you create proposed patches as branches relative to master and create a pull request? That makes the whole thing a little more tracktable.

TeamSPoon commented 8 years ago

Seems we'll have to migrate the attributes to the other variable.

This merging of the attributes between two attvars has to be done anyways so the constraints narrow properly. (This was never an option) .

If causes reference pointer to point upward and these beasts must point downwards to ensure they remain consistent during backtracking. That is why the swap is there ..

Before verify_attributes/3 is called, supposedly the variables will have already been swapped to the correct order. There is no indication otherwise. However there is a chance that while in the deeper bowels to what verify_attrributes/3 calls the Value has been replaced by a different attvar that is now in some way going to make it point upwards so $assign_attvar happens and it is swapped once again. The variable that is destroyed was the one Markus was counting on surviving the assignment. (all of the merging of attributes had been for nothing )

Seems we'll have to migrate the attributes to the other variable.

Since Markus has no way of guessing which variable would survive.. The only foolproof method would to be to alter both variables. Since He cant guess what pointing downwards meant.

TeamSPoon commented 8 years ago

Seems we'll have to migrate the attributes to the other variable.

This merging of the attributes between two attvars has to be done anyways so the constraints narrow properly. (This was never optional)

TeamSPoon commented 8 years ago

I fear this is incorrect. If causes reference pointer to point upward and these beasts must point downwards to ensure they remain consistent during backtracking.

As you said, this might be incorrect, I don't know what else can be tried so currently a pull request is not an option. We can wait until a better idea is possible.

TeamSPoon commented 8 years ago

Seems we'll have to migrate the attributes to the other variable.

Ok, I can provide a patch that swaps the attributes to the the variable that is going to be destroyed is the one Markus least expected. But this will be very confusing to his code since the wrong variable is going to be assigned and therefore any closures are going to be assuming the wrong variable has been bound. Any shared references are now also wrong.

triska commented 8 years ago

Please reexplain what you wrote, there are too many statements in your last paragraphs that do not make any sense to me.

It is not an option to require any code changes on the user level, because that would defeat the purpose of compatibility via verify_attributes/3. The Prolog engine itself must ensure that attributes of Value (not Var) are always retained. Is this now ensured?

JanWielemaker commented 8 years ago

On 01/21/2016 09:21 PM, Markus Triska wrote:

Please reexplain what you wrote, there are too many statements in your last paragraphs that do not make any sense to me.

It is not an option to require any code changes on the user level, because that would defeat the purpose of compatibility via |verify_attributes/3|. The Prolog engine itself must ensure that attributes are always copied from |Var| to |Value|, not the other way around. Is this now ensured?

Douglas' pull request #109 (https://github.com/SWI-Prolog/swipl-devel/pull/109) does this. I think it is fine. You are the one having the tricky test cases though and I'm not 100% sure.

Cheers --- Jan
triska commented 8 years ago

The test case I posted shows that the mistake still exists even when the pull request is applied:

?- time(num(N)).
% 29,869,788,769 inferences, 4205.152 CPU in 4205.730 seconds (100% CPU, 7103142 Lips)
N = 2715884.

When I replace the definition of verify_attributes/3 with the one I showed, I get the correct answer:

?- time(num(N)).
% 29,869,214,243 inferences, 4209.189 CPU in 4209.758 seconds (100% CPU, 7096192 Lips)
N = 2715850.
JanWielemaker commented 8 years ago

Although it looked promising, I have my doubt that swapping the variables is indeed the reason because registerWakeup() is called with the variables in the proper order. A simple test unifying two attvars in swapped memory order confirms this. I'm running Markus' test now in two versions: one with the patch and a print statement if the attribute move is done and one fetching the attribute after fd_put() and checking it in the continuation. Both are still silent.

Would be really nice to have a counter example that runs a little quicker ... I have little clue what might be wrong or even whether it is a bug in Prolog itself. After all, the first argument of verify_attributes gets the new attribute later. Could it be involved in anything else in between?

JanWielemaker commented 8 years ago

Hmm. Douglas attribute migration is not called on sat3.pl, so that explains why it doesn't help. What helps though is the code below in clpfd. Not that this is just the original, after which we pick up the clpfd attribute and use the continuation to verify it landed correctly. No messages are printed, but the result is correct!? So, just fetching the attribute and checking it changes the behaviour. I'm starting to get the idea that something is not reachable for GC. Now running with GC disabled.

verify_attributes(Var, Other, Gs) :-
        (   get_attr(Var, clpfd, clpfd_attr(_,_,_,Dom,Ps0)) ->
            (   nonvar(Other) ->
                (   integer(Other) -> true
                ;   type_error(integer, Other)
                ),
                domain_contains(Dom, Other),
                Ps = Ps0,
                Gs = Gs1
            ;   fd_get(Other, OD, OPs),
                domains_intersection(OD, Dom, Dom1),
                append_propagators(Ps0, OPs, Ps),
        fd_put(Other, Dom1, Ps),
        get_attr(Other, clpfd, Value),
                Gs = [check_attr(Other, clpfd, Value)|Gs1]
            ),
            phrase(all_propagators(Ps), Gs1, [do_queue])
        ;   Gs = []
        ).

check_attr(Var, Attr, Value) :-
    get_attr(Var, Attr, V),
    (   same_term(V, Value)
    ->  true
    ;   format(user_error, '~q: ~q \\=== ~q~n', [Attr, V, Value])
    ).

P.s. GC has become unlikely as the problem persists after ?- set_prolog_flag(gc, false). Shifts still happen, but are far less likely to cause this type of trouble as reachability is not considered.

TeamSPoon commented 8 years ago

Do we have a last known good?

For example, was 7.2.3 wrong?

Welcome to SWI-Prolog (Multi-threaded, 64 bits, Version 7.2.3) Copyright (c) 1990-2015 University of Amsterdam, VU Amsterdam SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software, and you are welcome to redistribute it under certain conditions. Please visit http://www.swi-prolog.org for details.

For help, use ?- help(Topic). or ?- apropos(Word).

?- time(num(X)). % 97,405,524,529 inferences, 11216.238 CPU in 11234.917 seconds (100% CPU, 8684331 Lips) X = 7130034.

DouglasRMiles commented 8 years ago

On Sat, Jan 23, 2016 at 6:14 PM, Douglas R. Miles notifications@github.com wrote:

Do we have a last known good?

For example, was 7.2.3 wrong?

Welcome to SWI-Prolog (Multi-threaded, 64 bits, Version 7.2.3) Copyright (c) 1990-2015 University of Amsterdam, VU Amsterdam SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software, and you are welcome to redistribute it under certain conditions. Please visit http://www.swi-prolog.org for details.

For help, use ?- help(Topic). or ?- apropos(Word).

?- time(num(X)). % 97,405,524,529 inferences, 11216.238 CPU in 11234.917 seconds (100% CPU, 8684331 Lips) X = 7130034.

Wanted to let you know I ran this on SICStus

And got this .... num(7130034) took 176.270 sec.

— Reply to this email directly or view it on GitHub https://github.com/SWI-Prolog/swipl-devel/issues/108#issuecomment-174243635 .

JanWielemaker commented 8 years ago

Thanks for running this. Now running the current git version with the 7.2.3 version from clpfd. We badly need a smaller example. I'd like to release 7.3.16, but this is a real show stopper. If nobody gets an idea soon, I propose to switch back to unify_attr_hook/2 until this is all sorted out.

TeamSPoon commented 8 years ago

To make tests easier to run I ended up making this file..

https://github.com/logicmoo/fluentvars/blob/master/prolog/sat2.pl#L53-L109

Looks like instead of needing 0...9

Issues will manifest 0...5 and 0...6

At the end of the file it shows the various offsets/errors

JanWielemaker commented 8 years ago

Thanks! Very confusing though :( Running the current master with the 7.2.3 clpfd.pl results in this:

1 ?- time(num(N)).
% 23,683,160,532 inferences, 2199.860 CPU in 2199.395 seconds (100% CPU, 10765758 Lips)
N = 2715850.

Which is the number Markus claimed to be correct, but in fact is wrong. Oddly enough it does the job in half the time!? Anyway, that is not the biggest worry now. No matter what, we must understand what happens before moving anywhere.

triska commented 8 years ago

That's the correct number, why do you say "but in fact is wrong"?

I have a separate patch that restores the full speed of earlier CLP(FD) versions, but please let us indeed first focus on this massive regression that leads to incorrect results.

triska commented 8 years ago

Douglas, your tests with SICStus are definitely not with the program I posted.

Please make sure to use the test case I stated in the original post. SICStus also finds the correct number of solutions, which is 2715850.

TeamSPoon commented 8 years ago 
root@gitlab:/devel/LogicmooDeveloperFramework/swipl-devel/packages/fluentvars/prolog# cat sat3.pl
:- use_module(library(clpfd)).
:- use_module(library(lists)).

sat(X) :- X in 0..9.

num(L) :-
    solve(As,Bs,Cs,Ds),
    append([As,Bs,Cs,Ds], Vs),
    findall(., labeling([ff], Vs), Ls),
    length(Ls, L).

solve([A1,A2,A3,A4],[B1,B2,B3,B4],[C1,C2,C3,C4],[D1,D2,D3,D4]) :-
    maplist(sat, [A1,A2,A3,A4,B1,B2,B3,B4,C1,C2,C3,C4,D1,D2,D3,D4]),
    A1 + A2 + A3 + A4 #= B1 + B2 + B3 + B4,
    A1 + A2 + A3 + A4 #= C1 + C2 + C3 + C4,
    A1 + A2 + A3 + A4 #= D1 + D2 + D3 + D4,
    A1 + A2 + A3 + A4 #= A1 + B1 + C1 + D1,
    A1 + B1 + C1 + D1 #= A2 + B2 + C2 + D2,
    A1 + B1 + C1 + D1 #= A3 + B3 + C3 + D3,
    A1 + B1 + C1 + D1 #= A4 + B4 + C4 + D4,
    A1 + A2 + A3 + A4 #= A1 + B2 + C3 + D4,
    A1 + B2 + C3 + D4 #= A4 + B3 + C2 + D1.

mytime(G):- statistics(runtime, [T0|_]),
        G,
        statistics(runtime, [T1|_]),
        T is T1 - T0,
        format('~q took ~3d sec.~n', [G,T]).

:- mytime(num(_X)).
root@gitlab:/devel/LogicmooDeveloperFramework/swipl-devel/packages/fluentvars/prolog# sicstus -l sat3.pl
% compiling /devel/LogicmooDeveloperFramework/swipl-devel/packages/fluentvars/prolog/sat3.pl...
%  loading /usr/local/sicstus4.3.2/bin/sp-4.3.2/sicstus-4.3.2/library/clpfd.po...
%  module clpfd imported into user
%   loading /usr/local/sicstus4.3.2/bin/sp-4.3.2/sicstus-4.3.2/library/atts.po...
%   module attributes imported into clpfd
%    loading /usr/local/sicstus4.3.2/bin/sp-4.3.2/sicstus-4.3.2/library/types.po...
%    module types imported into attributes
%    loaded /usr/local/sicstus4.3.2/bin/sp-4.3.2/sicstus-4.3.2/library/types.po in module types, 10 msec 4112 bytes
%   loaded /usr/local/sicstus4.3.2/bin/sp-4.3.2/sicstus-4.3.2/library/atts.po in module attributes, 10 msec 40176 bytes
%   loading /usr/local/sicstus4.3.2/bin/sp-4.3.2/sicstus-4.3.2/library/avl.po...
%   module avl imported into clpfd
%   loaded /usr/local/sicstus4.3.2/bin/sp-4.3.2/sicstus-4.3.2/library/avl.po in module avl, 0 msec 47376 bytes
%   loading /usr/local/sicstus4.3.2/bin/sp-4.3.2/sicstus-4.3.2/library/lists.po...
%   module lists imported into clpfd
%    module types imported into lists
%   loaded /usr/local/sicstus4.3.2/bin/sp-4.3.2/sicstus-4.3.2/library/lists.po in module lists, 0 msec 105744 bytes
%   loading /usr/local/sicstus4.3.2/bin/sp-4.3.2/sicstus-4.3.2/library/ordsets.po...
%   module ordsets imported into clpfd
%   loaded /usr/local/sicstus4.3.2/bin/sp-4.3.2/sicstus-4.3.2/library/ordsets.po in module ordsets, 0 msec 37312 bytes
%   loading /usr/local/sicstus4.3.2/bin/sp-4.3.2/sicstus-4.3.2/library/trees.po...
%   module trees imported into clpfd
%   loaded /usr/local/sicstus4.3.2/bin/sp-4.3.2/sicstus-4.3.2/library/trees.po in module trees, 0 msec 9856 bytes
%   module types imported into clpfd
%   loading /usr/local/sicstus4.3.2/bin/sp-4.3.2/sicstus-4.3.2/library/samsort.po...
%   module samsort imported into clpfd
%   loaded /usr/local/sicstus4.3.2/bin/sp-4.3.2/sicstus-4.3.2/library/samsort.po in module samsort, 0 msec 21424 bytes
%   loading /usr/local/sicstus4.3.2/bin/sp-4.3.2/sicstus-4.3.2/library/terms.po...
%   module terms imported into clpfd
%    module types imported into terms
%    module avl imported into terms
%   loaded /usr/local/sicstus4.3.2/bin/sp-4.3.2/sicstus-4.3.2/library/terms.po in module terms, 0 msec 39648 bytes
%   loading /usr/local/sicstus4.3.2/bin/sp-4.3.2/sicstus-4.3.2/library/timeout.po...
%   module timeout imported into clpfd
%    module types imported into timeout
%    loading foreign resource /usr/local/sicstus4.3.2/bin/sp-4.3.2/sicstus-4.3.2/library/x86_64-linux-glibc2.12/timeout.so in module timeout
%   loaded /usr/local/sicstus4.3.2/bin/sp-4.3.2/sicstus-4.3.2/library/timeout.po in module timeout, 10 msec 37280 bytes
%   loading foreign resource /usr/local/sicstus4.3.2/bin/sp-4.3.2/sicstus-4.3.2/library/x86_64-linux-glibc2.12/clpfd.so in module clpfd
%  loaded /usr/local/sicstus4.3.2/bin/sp-4.3.2/sicstus-4.3.2/library/clpfd.po in module clpfd, 40 msec 1930848 bytes
%  module lists imported into user
num(7130034) took 211.760 sec.
% compiled /devel/LogicmooDeveloperFramework/swipl-devel/packages/fluentvars/prolog/sat3.pl in module user, 213250 msec 145427088 bytes
SICStus 4.3.2 (x86_64-linux-glibc2.12): Fri May  8 01:05:09 PDT 2015
Licensed to Miles Douglas
| ?-
triska commented 8 years ago

Please use the test case I posted. You are missing the two constraints A1 #=< D4 and A1 #=< D1 in solve/4.

triska commented 8 years ago

I have created a test case that runs in 1 minute:

:- use_module(library(clpfd)).
sat(X) :- X in 0..5.
num(L) :-
        solve(As,Bs,Cs,Ds),
        append([As,Bs,Cs,Ds], Vs),
        findall(., labeling([ff,enum], Vs), Ls),
        length(Ls, L).
solve([A1,A2,A3,A4],[B1,B2,B3,B4],[C1,C2,C3,C4],[D1,D2,D3,D4]) :-
        maplist(sat, [A1,A2,A3,A4,B1,B2,B3,B4,C1,C2,C3,C4,D1,D2,D3,D4]),
        A1 #=< D4,
        A1 #=< D1,
        A1 + A2 + A3 + A4 #= B1 + B2 + B3 + B4,
        A1 + A2 + A3 + A4 #= C1 + C2 + C3 + C4,
        A1 + A2 + A3 + A4 #= D1 + D2 + D3 + D4,
        A1 + A2 + A3 + A4 #= A1 + B1 + C1 + D1,
        A1 + B1 + C1 + D1 #= A2 + B2 + C2 + D2,
        A1 + B1 + C1 + D1 #= A3 + B3 + C3 + D3,
        A1 + B1 + C1 + D1 #= A4 + B4 + C4 + D4,
        A1 + A2 + A3 + A4 #= A1 + B2 + C3 + D4,
        A1 + B2 + C3 + D4 #= A4 + B3 + C2 + D1.

The correct answer is:

?- time(num(N)).
% 374,157,809 inferences, 35.718 CPU in 35.978 seconds (99% CPU, 10475315 Lips)
N = 52400.

and with the latest git version, I get:

?- time(num(N)).
% 447,018,111 inferences, 50.789 CPU in 51.181 seconds (99% CPU, 8801477 Lips)
N = 52401.

If I replace the definition of verify_attributes/3 with the version shown in my original report, then I get the correct answer also with the latest git version.

TeamSPoon commented 8 years ago

@triska Aha, thank you for clarifying I was missing A1 #=< D4, A1 #=< D1, !

And now with the right test I get the answer num(2715850) took 77.490 sec. Good Good.

Will use your latest 0..5. Thank you!

Btw, both Jan and I do not think it is not something wrong with your code but some sneaky GC shift that is happening.

For example GC shifts can happen whenever one PL_new_term_refs() Also a person may wish to put values into term_t to protect them.. So normally in order to do that they open/close a frame to do so However to even PLopen*_frame() it may shift meaning all the pointers you are about to save are going to be wrong. The bug can even be somewhere between I_USERCALLN -> I_FCALLNDET3 (I doubt it is)

JanWielemaker commented 8 years ago

Btw, both Jan and I do not think it is not something wrong with your code but some sneaky GC shift that is happening.

Considering I tried with set_prolog_flag(gc, false)., GC is not that a likely assumption. For now, I simply have no clue.

Thanks to Markus' new test case I could now simply write all results of both the broken and new versions to a file and find the extra result. That leads to the following trivial program going wrong:

wrong :-
    solve(As,Bs,Cs,Ds),
        append([As,Bs,Cs,Ds], Vs),
    Vs = [0,2,4,3,4,4,1,0,5,3,0,1,0,0,4,5],
    labeling([ff,enum], Vs).

I didn't really expect this to work, but the above says true in the current version and fails in 7.2.3.

That is not a solution, but it might be manageable to sort out why this succeeds.

triska commented 8 years ago

Yes, it's definitely a mistake (if not exclusively, then at least also) in the SWI-Prolog engine. This already follows from my original post, where two Prolog snippets that are known to be equivalent yield different results. I hope the faster test case helps to track this down more easily. The flip side of it: Please resist the temptation to "fix" this by trial-and-error. Instead, please really carefully consider what is going on here, and fix the root cause of this.

Fortunately, we have this time obtained a reliable test case that runs within a few hours or even minutes. Even more miraculously, we found it only weeks after the new hook was introduced. Next time, we may not be so lucky. If subtle problems remain in the engine, many more users may be affected, and the program that shows the mistake may take weeks, months or years of running time. I once found a mistake in the CLP(FD) system of a different Prolog system that required running a test case for one month.

Thank you for looking into this!

triska commented 8 years ago

That's a great test case Jan! In fact labeling/2 is not even needed:

wrong :-
    solve(As,Bs,Cs,Ds),
        append([As,Bs,Cs,Ds], Vs),
    Vs = [0,2,4,3,4,4,1,0,5,3,0,1,0,0,4,5].

And now the interesting fact: This snippet does not even involve the case where verify_attributes/3 is called to unify two attributed variables!

In this case, CLP(FD)'s verify_attributes/3 is called exclusively in cases where an attributed variable is unified with a concrete integer. You can check this with:

verify_attributes(Var, Other, Gs) :-
        writeln(Var=Other),
        ...

Closely related to this issue seems to be another attribute (clpfd_aux), which is used to store which propagators are currently queued.

If I queue propagators in all cases (even if they are marked as "already queued"), the problem disappears: Simply insert false at the right place in propagator_//1 of library(clpfd):

propagator_(Propagator) -->
        { propagator_state(Propagator, State) },
        (   { State == dead } -> []
        ;   { false, get_attr(State, clpfd_aux, queued) } -> []
        ;   { b_getval('$clpfd_current_propagator', C), C == State } -> []
        ;   % passive
            % format("triggering: ~w\n", [Propagator]),
            { put_attr(State, clpfd_aux, queued) },
            (   { arg(1, Propagator, C),
                  functor(C, F, _), global_constraint(F) } ->
                { push_queue(Propagator, 2) }
            ;   [clpfd:activate_propagator(Propagator)]
            )
        ).

So at least this other attributed variable is closely related. This is in all likelihood not the root cause though, since we have now also the issue where simply inspecting some variables changes the program behaviour etc., which are posted in this thread.

triska commented 8 years ago

In fact, based on this, the CLP(FD) queuing code may also contain a mistake. Please give me a few hours to think about this. Concurrently, if possible, please think about how simply fetching the attribute and inspecting it could have influenced the result, which you mentioned above.

JanWielemaker commented 8 years ago

Seems we are making some progress. I hope you know enough about how this is supposed to work to see where it goes wrong. There are roughly three suspect areas:

My suspicion goes to the last point. GC/shift problems typically crash the system and the fact that this one solution generated too many can be used in a completely different scenario makes gc/shift very unlikely.

B.t.w. yes, why the fetch changes things is weird. That points at GC as it changes reachability, but we excluded that (almost). Going to try some stuff ...

JanWielemaker commented 8 years ago

freeze/2 isn't called by my wrong/0. test case. Of course we still have to keep this in mind, but it is not what is causing this test to fail. Unless something similar happens between the various attributes of clpfd. Markus will tell us that.

TeamSPoon commented 8 years ago

I haven't looked at your wrong/0 yet I was trying to fixing clp(fd) to not forget about some attributes and forget to run verify_attrrbutes/3. And i think I almost have it fixed now

JanWielemaker commented 8 years ago

I'm with Markus here. The bug is rather subtle and easily goes away with just about any change you make in the code. We must understand exactly why this goes wrong. As Markus points out, the case doesn't even seem to involve unification of two attributed variables. I just verified that by activating the print statement in assignAttVar(). So, the underlying error must be elsewhere.

TeamSPoon commented 8 years ago

Not sure what direction you are going there. There was nothing subtle about the bug. I already told you the problem (but in the other report). freeze/2 wasn't running.

I fixed that and now it works fine.

TeamSPoon commented 8 years ago

But at least the bug was my fault :P

JanWielemaker commented 8 years ago

I see two things in the patch. First of all, you keep iterating, also if the attvar is bound and second you changed the loop stop condition. I think the latter is unrelated, no? What exactly is the rationale behind the first. Before, the idea was to avoid running wakeup twice if the same unification was made multiple times. That is something that may still happen.

But .... my wrong/0 still incorrectly succeeds, so this is not the solution.

JanWielemaker commented 8 years ago

@triska: your false in propagate_() fixes wrong/0, but yields 52402 solutions and is thus also wrong. The extra solutions are

[0,4,3,1,2,3,3,0,5,1,0,2,1,0,2,5]
[0,4,4,0,1,3,3,1,5,1,0,2,2,0,1,5]

Unlike my initial wrong/0, the two above are generated, but inserting them in wrong/0 correctly results in false. @logicmoo's patch in attvar.pl doesn't fix any of this.

DouglasRMiles commented 8 years ago

the attvar guard was there as a workaround for ATT_WAKEBINDS also it was there incase someone wanted to implement verify_attributes/2.

The problem is though: imagine when the variable is bound and it's time to call call attr_unify_hook as done in a few places of clp(fd) . Like imagine the case of freeze.. well.. If the variable can only call verify_attrbutes/3 while its an attvar.. When could the freeze ever be bound ? The loop exit case gets no extra happiness just becasue of a []. The most important factor of the loop is when you find a attr/3 you must call va/3 if you dont find it you must succeed.

On Sun, Jan 24, 2016 at 7:13 AM, Jan Wielemaker notifications@github.com wrote:

I see two things in the patch. First of all, you keep iterating, also if the attvar is bound and second you changed the loop stop condition. I think the latter is unrelated, no? What exactly is the rationale behind the first. Before, the idea was to avoid running wakeup twice if the same unification was made multiple times. That is something that may still happen.

But .... my wrong/0 still incorrectly succeeds, so this is not the solution.

— Reply to this email directly or view it on GitHub https://github.com/SWI-Prolog/swipl-devel/issues/108#issuecomment-174308069 .

JanWielemaker commented 8 years ago

Nothing in '$wakeup'/1 binds Var. It could only happen if the implementation of verify_attribute/3 explicitly binds the Var to a concrete value. @markus, is this allowed? I think the answer ought to be no. So, I think I agree this is an improvement, but it doesn't solve the problem. This is easily verified using the code below, which doesn't trigger the backtrace in our famous ?- num(X). query.

collect_va_goal_list(att(Module, _AttVal, Rest), Var, Value) --> !,
    { attvar(Var) -> true ; backtrace(10) },

As far as the loop is concerned, the old code is better as it makes it explicit that the input is an att/3 term or the empty list. It is probably also faster as the system doesn't have to create a choice point because clause indexing already tells it there is only one candidate, although the result is probably not measurable.

In summary, I'll accept removing the attvar/1 guard as it is pointless. I'll delay that until we really know what is wrong though.

triska commented 8 years ago

Your intuition is right: verify_attributes/3 must not bind the variable.

As to the other cases you mentioned: Both issues you mention are by themselves already an indication that something is very wrong. If everything worked correctly, then

  1. inserting false/0 at the place I showed can at most decrease, never increase the number of solutions. This is because inserting false/0 can at most lead to more (redundant) propagators being invoked.
  2. a solution that is generated should of course also succeed when it is given.

So, both issues are in fact additional test cases and invariants that must hold.

I have produced CLP(FD) traces that show that inserting false/0 indeed leads to more propagators being invoked (as expected) when wrong/0 is called, but that does not explain why that (erroneously!) leads to more solutions when generating solutions. This last issue is probably closely related to the one we are already facing.

In my view however, a CLP(FD) trace is the wrong level of attacking this issue as long as we cannot rely on lower-level system invariants and face the quantum mechanical "mistake vanishes when looking at the attribute".

TeamSPoon commented 8 years ago

Well for whatever reason I get N = 52400. with the patch and N = 52401 without.. odd maybe i have mixed versions but I think it be a good idea with try Markus' initial test case and see if they are fixed.

On Sun, Jan 24, 2016 at 8:36 AM, Jan Wielemaker notifications@github.com wrote:

Nothing in '$wakeup'/1 binds Var. It could only happen if the implementation of verify_attribute/3 explicitly binds the Var to a concrete value. @markus https://github.com/markus, is this allowed? I think the answer ought to be no. So, I think I agree this is an improvement, but it doesn't solve the problem. This is easily verified using the code below, which doesn't trigger the backtrace in our famous ?- num(X). query.

collect_va_goal_list(att(Module, _AttVal, Rest), Var, Value) --> !, { attvar(Var) -> true ; backtrace(10) },

As far as the loop is concerned, the old code is better as it makes it explicit that the input is an att/3 term or the empty list. It is probably also faster as the system doesn't have to create a choice point because clause indexing already tells it there is only one candidate, although the result is probably not measurable.

In summary, I'll accept removing the attvar/1 guard as it is pointless. I'll delay that until we really know what is wrong though.

— Reply to this email directly or view it on GitHub https://github.com/SWI-Prolog/swipl-devel/issues/108#issuecomment-174314338 .

JanWielemaker commented 8 years ago

In my view however, a CLP(FD) trace is the wrong level of attacking this issue as long as we cannot rely on lower-level system invariants and face the quantum mechanical "mistake vanishes when looking at the attribute".

I do agree with that, but I fear that the wrong/0 is one of the few hopes to find what is wrong at a lower level. We already gone from over an hour to a few milliseconds. I have some trouble tracking down the deviation from correct behaviour as I can only compare the old attr_unify_hook version, which still runs correctly, with the new version. I'm afraid you are the best equipped to turn this into a simple thing to reproduce ...

JanWielemaker commented 8 years ago

Well for whatever reason I get N = 52400. with the patch and *N = 52401 without.

Possibly we use slightly different versions. The condition you removed though never makes a difference. Neither is freeze/2 involved in the test cases under consideration. So, my conclusions is that these changes at best just make the underlying problem go away due to different memory layout, stack shifting, or something similar. I excluded GC. Shifts are not yet excluded as the `min_free' property of stack is no longer honoured at the place I expected it to be. Doesn't make much sense either, except for ruling out stack shifts in cases like this.

TeamSPoon commented 8 years ago

BTW running the old tests

SICStus 4.3.2 (x86_64-linux-glibc2.12)

sicstus -l sat2.pl

num(3=2492) took 0.060 sec. num(4=13240) took 0.250 sec. num(5=52400) took 1.130 sec. num(6=171220) took 4.000 sec.

SWI Version 7.3.15-29-g6a6915a-DIRTY

swipl -O -l sat2.pl va3

num(3=2492) took 3.902 sec. num(4=13240) took 22.779 sec. num(5=52400) took 99.521 sec.

so sat 0..5 is good

But then... disappointedly

num(6,171221) (+1?!) took 353.829 sec.

I understand the value of the new test cases but I also wanted to see were things are at with the old.

JanWielemaker commented 8 years ago

That was to be expected. Pushed the simplification to collect_va_goal_list/3 as that looks correct but otherwise unrelated. Tried compiled with -DO_DEBUG, running Prolog with -d chk_secure. This adds a lot of consistency checks and wipes memory that is supposed to be uninitialised. Didn't trigger any issues though. I'm giving up for today. I'm completely clueless. If nothing shows up shortly, I propose to revert back to safe ground. Unfortunately we have also done some definitely good stuff in this project, making the reverse a little complicated.

triska commented 8 years ago

Here is my high-level guess of where the mistake may be located: In all cases we have seen so far, changing the third argument of verify_attributes/3, i.e., the continuation goals, in user code has changed the outcome.

This was the case in the original report, where moving a single goal from the body to the continuation goals"fixed" the issue, and it was also the case in Jan's much more mysterious case, where a single new goal (which only inspected the attribute) was added to the list of continuation goals and also changed the outcome.

The third argument of verify_attributes/3 is used by recent versions of CLP(FD) to trigger propagators after domain changes. We found one case where some propagators are not triggered—most likely because they are incorrectly classified as "already queued", since the clpfd_aux attribute of the propagator's State variable is (still) set to queued. Triggering all propagators, even if they are already marked as queued "fixed" that particular problem (but came with its own strange issues).

My guess is therefore that there may be a problem not whether, but how the continuation goals are invoked. Can there be any situation where the continuation goals are called, but the goals erroneously see the wrong state of existing attributes, for example, values they had before the unification has taken place (and verify_attributes/3 was called)? That would explain many issues we have seen in this discussion.

Note also that in CLP(FD), the following sequence can arise:

  1. CLP(FD) variable is unified (for example, with an integer)
  2. verify_attributes/3 is called; propagators are triggered, put into the continuation goals and marked as queued
  3. the first continuation goal is run; the propagator is marked as no longer queued (that is, its clpfd_aux attribute is removed)
  4. in the continuatino goal, again a CLP(FD) variable is unified (for example, again with an integer)
  5. verify_attributes/3 is called.

In step (5), we now have the situation that some propagators are already queued and therefore do not need to be queued again, and other propagators do have to be queued. It is therefore necessary that the continuation goals always see the latest version of all attributes. From the cases described above, it seems that this may get out of synch in some situations.

TeamSPoon commented 8 years ago

I am not saying this to be argumentative I jsut want to make sure we are on the same page:

Nothing in '$wakeup'/1 binds Var.

'$wakeup'/1 binds Var using $attvar_assign/2 (but that is after verify_attributes/3) While the Goals part of verify_attributes/3 run, the attvar must have it's value changed. And this is fine.

Here is a trapshot that binds the Var

verify_attributes(Var, Other, Goals) :-
        get_atts(Var, dom(Da)), !,          % are we involved?
        (   var(Other) ->                   % must be attributed then
            (   get_atts(Other, dom(Db)) -> %   has a domain?
                ord_intersection(Da, Db, Dc),
                Dc = [Other|Els],              % at least one element
                (   Els = [] ->             % exactly one element
                    Goals = []    
                ;   Goals = [],
                    put_atts(Other, dom(Dc))% rescue intersection
                )
            ;   Goals = [],
                put_atts(Other, dom(Da))    % rescue the domain
            )
        ;   Goals = [],
            ord_intersect([Other], Da)      % value in domain?
        ).
verify_attributes(_, _, []).                % unification triggered
                                            % because of attributes
                                            % in other modules

The workaround 

verify_attributes(Var, Other, Goals) :-
        get_atts(Var, dom(Da)), !,          % are we involved?
        (   var(Other) ->                   % must be attributed then
            (   get_atts(Other, dom(Db)) -> %   has a domain?
                ord_intersection(Da, Db, Dc),
                Dc = [El|Els],              % at least one element
                (   Els = [] ->             % exactly one element
                    Goals = [Other=El]      % implied binding  (THIS WORKAROUND)
                ;   Goals = [],
                    put_atts(Other, dom(Dc))% rescue intersection
                )
            ;   Goals = [],
                put_atts(Other, dom(Da))    % rescue the domain
            )
        ;   Goals = [],
            ord_intersect([Other], Da)      % value in domain?
        ).
verify_attributes(_, _, []).                % unification triggered
                                            % because of attributes
                                            % in other modules

See (THIS WORKAROUND) above Note that the "implied binding" Other=El was deferred until after the completion of verify_attribute/3. However Initially someone might not create the Other since it is not very logical to do, But they have to since there might be a danger binding the Var, which is not allowed inside the scope of verify_attribute/3. Deferring unifications into the third argument of verify_attribute/3 effectively serializes th calls to verify_attribute/3.

https://github.com/SWI-Prolog/swipl-devel/compare/master...logicmoo:throw_on_bind

This branch will detect and complain whenever the status of Var changes (sometimes to to GC or sometimes due to code va/3 code)

Sometimes these are too subtle to noticed. Also ran the exact same code more than once and only sometimes did something drastic change. There are intentionally a false positives..

They look like 

ERROR> attrs(_G3443661,...)"== attrs(_G122,...)

but can't let that shifting slide (Big numbers converting to smaller numbers)

will be false positives (prefered over false negatives) they are happening intermittently in clp(fd). Thus I can't say that CLP(fd) is doing something wrong like the above example.. however clp(fd) gets falsely accused (my next post)

I suggest once you checkout this branch that you run make check at least once. And look at a few of the stack traces to understand what a "Ok situation may be"

https://github.com/SWI-Prolog/swipl-devel/compare/master...logicmoo:throw_on_bind

TeamSPoon commented 8 years ago

This is the type of issues its finds...

ERROR: Assertion failed: '$attvar':get_attr(1,cookie,_G40722)
  [71] backtrace(10) at /usr/local/lib/swipl-7.3.15/library/prolog_stack.pl:393
  [70] prolog_debug:assertion_failed(fail,'$attvar': ...) at /usr/local/lib/swipl-7.3.15/library/debug.pl:306
  [69] prolog_debug:assertion('$attvar': ...) at /usr/local/lib/swipl-7.3.15/library/debug.pl:296
  [68] '$attvar':check_var_cookie(1,"_G2234":"attrs(_G2234,att(clpfd,clpfd_attr(no,no,no,from_to(n(0),n(1)),fd_props([],[propagator(pplus(0,_G2173,_G2234),dead),propagator(pplus(_G2173,_G2234,2),_G38692),propagator(pplus(_G2234,_G2478,2),_G35661),propagator(scalar_product_eq([1,-1,1,-1,-1,1,-1,1],[0,1,2,0,_G2173,_G2234,2,1],0),dead),propagator(scalar_product_eq([1,1,1,-1,-1,-1],[1,3,1,2,_G2234,1],0),_G37083),propagator(scalar_product_eq([1,-1,1,-1,1,-1,1,-1],[0,3,0,0,3,_G2234,2,_G2478],0),dead),propagator(scalar_product_eq([1,1,1,1,-1,-1,-1,-1],[0,1,3,1,3,_G2173,_G2234,0],0),dead)],[])),[]))") at /usr/local/lib/swipl-7.3.15/boot/attvar.pl:73
  [67] '$attvar':collect_all_va_goal_lists(wakeup(1,...,1,[]),[...|...],[]) at /usr/local/lib/swipl-7.3.15/boot/attvar.pl:94
  [66] '$attvar':'$wakeup'(wakeup(1,...,1,[])) at /usr/local/lib/swipl-7.3.15/boot/attvar.pl:54
  [65] clpfd:run_propagator(pplus(0,1,1),dead) at /usr/local/lib/swipl-7.3.15/library/clp/clpfd.pl:3989
  [63] clpfd:do_queue at /usr/local/lib/swipl-7.3.15/library/clp/clpfd.pl:3486
  [60] clpfd:clpfd_equal(1,0+1) at /usr/local/lib/swipl-7.3.15/library/clp/clpfd.pl:2396
  [57] '$attvar':map_goals([...|...]) at /usr/local/lib/swipl-7.3.15/boot/attvar.pl:59
   Redo: (65) clpfd:run_propagator(pplus(0, 1, 1), dead) ?
TeamSPoon commented 8 years ago

4-> 5. in the continuation goal, again a CLP(FD) variable is unified (for example, again with an integer) verify_attributes/3 is called.

Exactly

TeamSPoon commented 8 years ago

Here was 15 second testcase:


:- use_module(library(clpfd)).

sat(N,X) :- X in 0..N.

num(L):- between(3,6,N),time(num(N,L)),writeln(num(N=L)),fail.
num(N,L) :-
    solve(N,As,Bs,Cs,Ds),
    append([As,Bs,Cs,Ds], Vs),
    findall(., labeling([ff], Vs), Ls),
    length(Ls, L).

solve(N,[A1,A2,A3,A4],[B1,B2,B3,B4],[C1,C2,C3,C4],[D1,D2,D3,D4]) :-
    maplist(sat(N), [A1,A2,A3,A4,B1,B2,B3,B4,C1,C2,C3,C4,D1,D2,D3,D4]),
    A1 #=< D4,
    A1 #=< D1,
    A1 + A2 + A3 + A4 #= B1 + B2 + B3 + B4,
    A1 + A2 + A3 + A4 #= C1 + C2 + C3 + C4,
    A1 + A2 + A3 + A4 #= D1 + D2 + D3 + D4,
    A1 + A2 + A3 + A4 #= A1 + B1 + C1 + D1,
    A1 + B1 + C1 + D1 #= A2 + B2 + C2 + D2,
    A1 + B1 + C1 + D1 #= A3 + B3 + C3 + D3,
    A1 + B1 + C1 + D1 #= A4 + B4 + C4 + D4,
    A1 + A2 + A3 + A4 #= A1 + B2 + C3 + D4,
    A1 + B2 + C3 + D4 #= A4 + B3 + C2 + D1.

?- time(num(W)).
% 24,295,418 inferences, 10.057 CPU in 10.064 seconds (100% CPU, 2415813 Lips)
num(3=2492)
ERROR: Assertion failed: '$attvar':get_attr(1,cookie,_G25494)
  [74] backtrace(10) at /usr/local/lib/swipl-7.3.15/library/prolog_stack.pl:393
  [73] prolog_debug:assertion_failed(fail,'$attvar': ...) at /usr/local/lib/swipl-7.3.15/library/debug.pl:306
  [72] prolog_debug:assertion('<garbage_collected>') at /usr/local/lib/swipl-7.3.15/library/debug.pl:296
  [71] '$attvar':check_var_cookie(1,'<garbage_collected>') at /usr/local/lib/swipl-7.3.15/boot/attvar.pl:73
  [70] '$attvar':collect_all_va_goal_lists('<garbage_collected>',[...|...],[]) at /usr/local/lib/swipl-7.3.15/boot/attvar.pl:96
  [69] '$attvar':'$wakeup'('<garbage_collected>') at /usr/local/lib/swipl-7.3.15/boot/attvar.pl:54
  [68] clpfd:run_propagator('<garbage_collected>','<garbage_collected>') at /usr/local/lib/swipl-7.3.15/library/clp/clpfd.pl:3989
  [66] clpfd:do_queue at /usr/local/lib/swipl-7.3.15/library/clp/clpfd.pl:3486
  [63] clpfd:clpfd_equal(1,'<garbage_collected>') at /usr/local/lib/swipl-7.3.15/library/clp/clpfd.pl:2396
  [60] '$attvar':map_goals('<garbage_collected>') at /usr/local/lib/swipl-7.3.15/boot/attvar.pl:59
   Redo: (68) clpfd:run_propagator('<garbage_collected>', '<garbage_collected>') ? abort
% 11,451,000 inferences, 4.199 CPU in 88.958 seconds (5% CPU, 2727232 Lips)
% 35,746,640 inferences, 14.256 CPU in 99.022 seconds (14% CPU, 2507509 Lips)
% Execution Aborted
?- set_prolog_flag(gc,false).
true.

?- time(num(W)).
% 33,035,246 inferences, 10.021 CPU in 10.032 seconds (100% CPU, 3296608 Lips)
num(3=2492)
ERROR: Assertion failed: '$attvar':get_attr(1,cookie,_G58652)
  [76] backtrace(10) at /usr/local/lib/swipl-7.3.15/library/prolog_stack.pl:393
  [75] prolog_debug:assertion_failed(fail,'$attvar': ...) at /usr/local/lib/swipl-7.3.15/library/debug.pl:306
  [74] prolog_debug:assertion('$attvar': ...) at /usr/local/lib/swipl-7.3.15/library/debug.pl:296
  [73] '$attvar':check_var_cookie(1,"_G1947":"attrs(_G1947,att(clpfd,clpfd_attr(no,no,no,from_to(n(0),n(1)),fd_props([],[propagator(pplus(0,_G1874,_G1947),dead),propagator(pplus(_G1874,_G1947,2),_G56421),propagator(pplus(_G1947,_G2239,2),_G52609),propagator(scalar_product_eq([1,-1,1,-1,-1,1,-1,1],[0,1,2,0,_G1874,_G1947,2,1],0),dead),propagator(scalar_product_eq([1,1,1,-1,-1,-1],[1,3,1,2,_G1947,1],0),_G54713),propagator(scalar_product_eq([1,-1,1,-1,1,-1,1,-1],[0,3,0,0,3,_G1947,2,_G2239],0),dead),propagator(scalar_product_eq([1,1,1,1,-1,-1,-1,-1],[0,1,3,1,3,_G1874,_G1947,0],0),dead)],[])),[]))") at /usr/local/lib/swipl-7.3.15/boot/attvar.pl:73
  [72] '$attvar':collect_all_va_goal_lists(wakeup(1,...,1,[]),[...|...],[]) at /usr/local/lib/swipl-7.3.15/boot/attvar.pl:96
  [71] '$attvar':'$wakeup'(wakeup(1,...,1,[])) at /usr/local/lib/swipl-7.3.15/boot/attvar.pl:54
  [70] 1=1 <foreign>
  [69] clpfd:run_propagator(pplus(0,1,1),dead) at /usr/local/lib/swipl-7.3.15/library/clp/clpfd.pl:3989
  [67] clpfd:do_queue at /usr/local/lib/swipl-7.3.15/library/clp/clpfd.pl:3486
  [64] clpfd:clpfd_equal(1,0+1) at /usr/local/lib/swipl-7.3.15/library/clp/clpfd.pl:2396
   Redo: (70) 1=1 ?
?- time(num(6,W)).
ERROR: Assertion failed: '$attvar':get_attr(6,cookie,_G87494)
 [125] backtrace(10) at /usr/local/lib/swipl-7.3.15/library/prolog_stack.pl:393
 [124] prolog_debug:assertion_failed(fail,'$attvar': ...) at /usr/local/lib/swipl-7.3.15/library/debug.pl:306
 [123] prolog_debug:assertion('$attvar': ...) at /usr/local/lib/swipl-7.3.15/library/debug.pl:296
 [122] '$attvar':check_var_cookie(6,"_G4434":"attrs(_G4434,att(clpfd,clpfd_attr('.','.','.',from_to(n(4),n(6)),fd_props([],[propagator(pplus(_G4142,_G4434,7),_G84949),propagator(pplus(0,_G4434,_G3996),dead),propagator(pplus(0,_G4434,6),_G84966),propagator(scalar_product_eq([1,-1,1,-1,-1,1,-1,1],[0,4,5,1,_G3996,0,0,_G4434],0),dead),propagator(scalar_product_eq([1,1,1,-1,-1,-1],[1,6,4,5,0,_G4434],0),dead),propagator(scalar_product_eq([1,-1,1,-1,1,-1,1,-1],[0,4,5,0,6,_G4142,0,_G4434],0),dead),propagator(scalar_product_eq([1,1,1,1,-1,-1,-1,-1],[0,1,6,4,0,_G4288,_G4361,_G4434],0),_G84888),propagator(pgeq(_G4434,0),dead)],[])),[]))") at /usr/local/lib/swipl-7.3.15/boot/attvar.pl:73
 [121] '$attvar':collect_all_va_goal_lists(wakeup(6,...,4,[]),[...|...],[]) at /usr/local/lib/swipl-7.3.15/boot/attvar.pl:96
 [120] '$attvar':'$wakeup'(wakeup(6,...,4,[])) at /usr/local/lib/swipl-7.3.15/boot/attvar.pl:54
 [119] 6=4 <foreign>
 [118] clpfd:run_propagator(pplus(0,6,4),dead) at /usr/local/lib/swipl-7.3.15/library/clp/clpfd.pl:3989
 [116] '$attvar':map_goals([...|...]) at /usr/local/lib/swipl-7.3.15/boot/attvar.pl:59
 [113] n(0)=n(0) <foreign>
   Redo: (119) 6=4 ? abort
% 133,316,255 inferences, 36.990 CPU in 40.143 seconds (92% CPU, 3604105 Lips)
% Execution Aborted