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.
This commit is contained in:
Markus Triska
2020-08-12 19:51:25 +02:00
parent 099d9aaca6
commit e185b626bd

View File

@@ -842,9 +842,8 @@ verify_attributes(Var, Other, Gs) :-
( integer(Other) -> ( integer(Other) ->
( between(0, 1, Other) -> ( between(0, 1, Other) ->
root_get_formula_bdd(Root, Sat, BDD0), root_get_formula_bdd(Root, Sat, BDD0),
bdd_restriction(BDD0, I, Other, BDD),
root_put_formula_bdd(Root, Sat, 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) ; no_truth_value(Other)
) )
; atom(Other) -> ; atom(Other) ->