Like the BDD library in the SMV system it does not use reference counting internally. Only external references are reference counted. This should in theory be faster then a reference counting scheme. However, in each recursive call the references to nodes in registers have to saved because a garbage collection deeper in the recursion need to know them.
A first improvement over the approach of SMV is to use a stack instead of a list to save this references. As an ultimate goal we want to implement non recursive versions of the BDD algorithms. Then the references are accessible on the explicitly modeled call stack and do not have to be saved.
We restricted the number of possible nodes to 2^25. At least for model checking this seems to be a reasonable choice. With restricting the number of variables to 2^11 we were able to fit one node into two 32 bit words. (These restriction can be remove at compile time, but then 3 words are needed for each node).
We use a direct hash scheme for the unique table. The nodes are stored directly in one gigantic hash table. Collision are resolved by traversing the hash table. This should give better cache behaviour than a hash table with pointers to actual nodes. The drawback is that we can not easily use unique tables on a level basis and that garbage collection requires a new hash table of the the same size (sort of copying collector).
In the newest version double hashing is used to avoid some extreme cases. We also realized that only one additional forward pointer and no copyspace is needed. But this is not implemented yet.
We suggest to investigate how direct hashing works with per level unique tables. It should have a much better memory behaviour than the current scheme.
Also it is possible to leave deleted nodes in the hash table. This would reduce the number of times the whole hash table has to be copied or avoid doubling the unique table during garbage collection at all.
The library heavily uses inlining of functions. To keep it still easy to debug we use a preprocessor that can generate macros or functions.
Armin Biere
Fri Jun 26 13:41:32 EDT 1998