Partial Breadth-First Package: PBF

Description

This package uses the partial breadth-first evaluation for BDD construction. Within each evaluation context, the breadth-first BDD construction is used until the context is full. Once the context is full, the remaining operations are partitioned. Each paritition is assigned to a new evaluation context. Each evaluation context is then executed recursively using the same algorithm. The size of an evaluation context currently set by the user. If the size is very large, then this is basically a breath-first construction. If the size is too small, then the depth-first construction is used.

The evalution context is also used to support doubly-recursive operations (e.g., quantification and relational product). During the reduction phase for a variable i, the new operations generated for second level of recursion are stored in a new child context. This child context is then evaluated using the partial breadth-first approach described above. Once the result of the child context is available, the reduction of variable i can resume to completion.

There are two types of cache maintained: uncomputed cache and computed cache. The uncomputed cache is for operations that are currently being computed. The computed cache stores the computed result. During the expansion phase (sift down), both caches are consulted to avoid redudant operations. During the reduction phase, the computed results are inserted into the computed cache. In our previous work for combinational BDD operations, we have combined both cache. This separation does slow down the BDD package, but it simplifies the code quite a bit.