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
@@ -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) ->
