Main Page | Namespace List | Class Hierarchy | Class List | File List | Namespace Members | Class Members | File Members

BDDs are good when there is some structure of the set, giving a small representation of large sets. A BDD is a binary tree representing choices on assignments of boolean variables. Each node represents a variable and each choice (left or right) represents the assignments 0 and 1. If it does not matter what the assignment of the variable is, i.e., if an assignment is or is not in the set independently of the value of the variable it is not included in the tree. The leaves of a BDD is a boolean variable saying whether the assignment represented by traversing from the root to the leaf is in the set.

Since (finite) sets can be represented using BDDs, so can relations. Usually, the set of variables are partitioned such that different variables represent different components of the relation. Normal relation operators such as image, range, composition etc. can be implemented using operations on BDDs.

When many relations of different types exist and many different types of operations are performed, the complexity of keeping track of which variables represent what becomes harder. Imagine taking the image R(S) of a binary relation R under a set S. The binary relation R have two components, each represented by a set of variables V1 and V2, and the set S is represented by a set of variables V3. The image is contructed by intersecting the BDD representing the relation R with the BDD representing S, constraining the first compoment of the relation R to the set S, and projecting on the second component. For this to work, the set of variables V1 used to represent the first compoment of R must be the same as the set of variables V3 used to represent S. If they are not the same, the BDD representing S has to be renamed such that each variable in V3 is represented with the corresponding variable in V1. With complex expressions involving relations of different arities, the bookkeeping of variables becomes a tedious task.

The package GBDD is designed to perform this bookkeeping of variables automatically, providing an abstration on top of BDDs that is simply finite relations . A relation is defined to be a BDD and a vector of domains, sets of variables, used in the BDD to represent each component of the relation. When operations such as composition, image etc. are performed, renamings are performed automatically if needed. Also, there is support for allocating variables from a set in different ways, releiving the user from having to specify exactly what variables should be used to represent different domains.

Furthermore, more than one BDD package can be plugged into GBDD providing one unified API for all BDD packages. This makes it easy to change BDD packages. Currently, A (slow) reference implementation and an interface to the BuDDy BDD package has been implemented as well as the CUDD BDD package.

Spaces are created by the constructor of the desired BDD implementation, or by using the create_default method of the ancestor class gbdd::Space, which currently creates a BuDDy space (if compiled in).

A space contains methods for creating BDDs, and all the operations on BDDs such as product, renaming etc. Added a new BDD implementation or adding support for an existing BDD package involves subclassing Space and implementating all the virtual methods.

The class gbdd::Bdd wraps around a BDD identifier and the space it belongs to for convenience. Its constructor takes a BDD space and a boolean value to create a leaf and contains several static methods to create different kinds of BDDs given other BDDs. Two instances of Bdd can also be combined by the usual C++ operators such as & and |, with the obvious meanings. There are also more specific methods, like Bdd::value_follow, which are there for performance. They can be used to implement certain operations more efficiently than just using normal BDD products.

Using the class Bdd is the normal way of using BDDs in this package, the methods in Space are considered low-level.

A vector of domains is represented by the class gbdd::Domains. There are several useful operations on vectors of domains, for example * which represents concatenation meaning the cartesian product of the domains.

The relation concept is generalized in gbdd::StructureRelation, which operates on any structure inheriting from gbdd::StructureConstraint, of which gbdd:Bdd is a special case.

Generated on Mon Aug 1 04:04:43 2005 for gbdd by 1.3.6