FIXED: Unification between two CLP(B) variables in certain cases.
FIXED: Unification between two CLP(B) variables in certain cases.

So far, the only way I have found to show the problem is to disable
domain and aliasing propagation, by letting satisfiable_bdd/1 consist
only of the single clause:

   satisfiable_bdd(BDD) :- BDD \== 0.

This is certainly valid, because such a BDD is satisfiable.

Then, we find with our standard testing.pl:

   :- use_module(library(clpb)).

   :- set_prolog_flag(clpb_validation, true).
   :- set_prolog_flag(clpb_residuals, bdd).

   sat(_)  --> [].
   %sat(X*Y) --> [_], sat(X), sat(Y).
   sat(X+Y) --> [_], sat(X), sat(Y).
   sat(X#Y) --> [_], sat(X), sat(Y).
   %sat(card([0,1],[X,Y])) --> [_], sat(X), sat(Y).

   vs_eqs(Vs, Eqs) :- phrase(vs_eqs(Vs), Eqs).

   vs_eqs([]) --> [].
   vs_eqs([V|Vs]) --> vs_eqs_(Vs, V), vs_eqs(Vs).

   vs_eqs_([], _) --> [].
   vs_eqs_([V|Vs], X) --> vs_eqs_(Vs, X), ( [X=V] ; [] ).

   run(N) :-
           length(Ls, N),
           portray_clause(N),
           phrase(sat(Sat1), Ls),
           phrase(sat(Sat2), Ls),
           term_variables(Sat1-Sat2, Vs0),
           permutation(Vs0, Vs),
           vs_eqs(Vs, Eqs),
           findall(Vs, (sat(Sat1),sat(Sat2),maplist(call, Eqs),labeling(Vs)), Sols1),
           findall(Vs, (labeling(Vs),maplist(call,Eqs),sat(Sat1*Sat2)), Sols2),
           (   sort(Sols1, Sols), sort(Sols2, Sols) -> true
           ;   throw(neq-Sat1-Sat2-Eqs-Vs0-Vs-Sols1-Sols2)
           ),
           false.

   run :- run(_).

already the case:

   ?- run.
   0.
   1.
   ERROR: Unhandled exception: neq- (_G245+_G246)- (_G248+_G249)-[_G248=_G249,_G248=_G246,_G246=_G249]-[_G245,_G246,_G248,_G249]-[_G245,_G248,_G246,_G249]-[[0,1,1,1],[1,0,0,0],[1,1,1,1]]-[[0,1,1,1],[1,1,1,1]]

We can even find a simpler case with a similar program:

   ?- sat(A+B), sat(C), A = C.

The underlying problem here is that it is not sufficient to parse the
"Other" variable (in this case: C) to obtain the BDD, because the
variables are already aliased when the hook is called, so Other is in
fact A too. Instead, we need to build the conjunction of both original
formulas, and use it to build the new BDD.

Two remaining TODOs:

(1) the second branch probably has an analogous problem, so construct a
    test case for it and correct it.

(2) find a test case that shows the problem also when full propagation is
    enabled.

jn7163/swipl-devel,koryonik/swipl-devel,koryonik/swipl-devel,mndrix/swipl-devel,koryonik/swipl-devel,koryonik/swipl-devel,mndrix/swipl-devel,edechter/swipl-devel,edechter/swipl-devel,mndrix/swipl-devel,jn7163/swipl-devel,jn7163/swipl-devel,edechter/swipl-devel,koryonik/swipl-devel,jn7163/swipl-devel,edechter/swipl-devel,mndrix/swipl-devel,mndrix/swipl-devel,edechter/swipl-devel,jn7163/swipl-devel