Can a boolean expression be evaluated using its corresponding BDD (Binary Decision Diagram) in BuDDy?

Question

I am very new to BuDDy (http://buddy.sourceforge.net/manual/main.html), and I'm in a context where I have to evaluate a boolean expression based on its corresponding BDD.

Let's assume the expression looks like this: (!a && b). I want to be able to set the truth values for a and b and evaluate the entire formula using the BDD.

Is this possible by any means in BuDDy?

Answer 1

You can use bdd_retrict(formula, valuation) where formula is the BDD representing the expression you want to evaluate, and valuation is a BDD representing a conjunction of variables such as a & !b (if you want to set a to true, and !b to false). This will return a new formula with all variables in valuation replaced by their value. So if valuation covers all variables in formula, the result will be either bddtrue or bddfalse.