From: Markus Triska <triska@metalevel.at>
Date: Wed, 12 Aug 2020 17:51:25 +0000 (+0200)
Subject: FIXED: CLP(B): Delay BDD restriction until after the instantiation.
X-Git-Tag: v0.9.0~174^2~11^2
X-Git-Url: https://git.sagredo.dev/?a=commitdiff_plain;h=e185b626bdf1a99ab8188ae39875f645c0de90f0;p=scryer-prolog.git

FIXED: CLP(B): Delay BDD restriction until after the instantiation.

This is necessary to actually take the new value into account.

Example:

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

This addresses #670.
---

diff --git a/src/lib/clpb.pl b/src/lib/clpb.pl
index ad49f61c..0b802a46 100644
--- a/src/lib/clpb.pl
+++ b/src/lib/clpb.pl
@@ -842,9 +842,8 @@ verify_attributes(Var, Other, Gs) :-
             (   integer(Other) ->
                 (   between(0, 1, Other) ->
                     root_get_formula_bdd(Root, Sat, BDD0),
-                    bdd_restriction(BDD0, I, Other, BDD),
                     root_put_formula_bdd(Root, Sat, BDD),
-                    Gs = [satisfiable_bdd(BDD)]
+                    Gs = [bdd_restriction(BDD0,I,Other,BDD),satisfiable_bdd(BDD)]
                 ;   no_truth_value(Other)
                 )
             ;   atom(Other) ->