next up previous contents
Next: Reference - Search heuristics Up: Reference - Preprocessing Previous: Splitter   Contents


Universally quantify a variable away from a BDD. This operation exists only in canonical form. The pseudo C++ description of this operation is as follows:

BDD Universe (BDD f, variable x) {
if (root(f) == x) return true(root(f))$\wedge$false(root(f));
if (index(x) > index(root(f))) return f; // If x is not in f do nothing
$h_{f_T}$ = Universe (true(root(f)), x);
$h_{f_F}$ = Universe (false(root(f)), x);
if ($h_{f_T}$ == $h_{f_F}$) return $h_{f_T}$;
return find_or_add_node (root(f), $h_{f_T}$, $h_{f_F}$);

John Franco 2011-09-15