The following function implements the Boolean negation. Indeed, using this function is quite ineffective, since the built-in not operator does the same thing in constant time, but this simple algorithm shows the genaral structure of any unary bdd-based operator.
negation(a) := if compare(a, true) then false else if compare(a, false) then true else ite( root(a), negation(high(a)), negation(low(a)));
In order to understand this algorithm, remain that any bdd a is either:
The algorithm first treat the basic cases, by comparing the parameter to the constants true and false, and after the genaral case, where the parameter still depends on some argument. In this case, the function is recursively called on the corresponding high and low parts, and the results are combined under a test of the root argument.
This is another example of unary function, that builds, if it exists, an monomial that implies a :
path(a) := if compare(a, true) then true else if compare(a, false) then false else if compare(high(a), false) then (not root(a) and path(low(a))) else (root(a) and path(high(a))) ;
The following function implements the Boolean or. The only interest is in showing how to build a binary operator. We first treat the basic cases, where either a, b are constants. Then, we treat the case where both a and b are "binary" bdds. In this last case, we use the binary extension of the root operator to get the "minimal" argument between root(a) and root(b), and call it min_root. Then, the recursive calls are made by decomposing both parameters according to min_root.
union(a, b) := if (compare(a, true) or compare(b, false)) then a else if (compare(b, true) or compare(a, false)) then b else let min_root := root(a, b) in ite(min_root, union(constrain(a, min_root), constrain(b, min_root)), union(constrain(a, not min_root), constrain(b, not min_root)) );
The use of the generalized cofactor in the recursive calls may seem a little bit tricky. It is justified by the fact that (for instance) either constrain(a, min_root) = a if min_root ≠ root(a), or constrain(a, min_root) = high(a) if min_root = root(a).