next up previous contents
Next: Existential quantification Up: Reference - Preprocessing Previous: Strengthening   Contents


At BDD build time, meaning every time a BDD is modified by any preprocessing function, inferences are collected and attached to every pertinent node of the BDDs. This makes it a very simple process to check a BDD for inferences: just look at the list attached to the top node of any BDD and you'll see it's inferences. There are 4 types of inferences in the form of $x=T$, $x=F$, $x=y$, $x=-y$. As soon as any BDD has inferences to give, it's inferences are applied to every applicable BDD.

John Franco 2011-09-15