prolog::bdd_eval/2¶
bdd_eval(+ BDDHandle, Val)*
Unify Val with the value of the logical expression compiled in BDDHandle given an assignment to its variables.
bdd_new(X+(Y+X)*(-Z), BDD),
[X,Y,Z] = [0,0,0],
bdd_eval(BDD, V),
writeln(V).
would write 0 in the standard output stream.
The Prolog code equivalent to bdd_eval//22 is:
Tree = bdd(1, T, _Vs),
reverse(T, RT),
foldl(eval_bdd, RT, _, V).
eval_bdd(pp(P,X,L,R), _, P) :-
P is ( X/\L ) \/ ( (1-X) /\ R ).
eval_bdd(pn(P,X,L,R), _, P) :-
P is ( X/\L ) \/ ( (1-X) /\ (1-R) ).
First, the nodes are reversed to implement bottom-up evaluation. Then, we use the foldl
list manipulation predicate to walk every node, computing the disjunction of the two cases and binding the output variable. The top node gives the full expression value. Notice that (1- _X_)
implements negation.