next up previous index
Next: Variable Reordering for ZDDs Up: User's Manual Previous: Variable Reordering for BDDs

Grouping Variables

  

CUDD allows the application to specify constraints on the positions of group of variables. It is possible to request that a group of contiguous variables be kept contiguous by the reordering procedures. It is also possible to request that the relative order of some groups of variables be left unchanged. The constraints on the order are specified by means of a tree , which is created in one of two ways:

Each node in the tree represents a range of variables. The lower bound of the range is given by the low field of the node, and the size of the group is given by the size field of the node. The variables in each range are kept contiguous. Furthermore, if a node is marked with the MTR_FIXED  flag, then the relative order of the variable ranges associated to its children is not changed. As an example, suppose the initial variable order is:

        x0, y0, z0, x1, y1, z1, ... , x9, y9, z9.
Suppose we want to keep each group of three variables with the same index (e.g., x3, y3, z3) contiguous, while allowing the package to change the order of the groups. We can accomplish this with the following code:
        for (i = 0; i < 10; i++) {
            (void) Cudd_MakeTreeNode(manager,i*3,3,MTR_DEFAULT);
        }
If we want to keep the order within each group of variables fixed (i.e., x before y before z) we need to change MTR_DEFAULT  into MTR_FIXED.

The low parameter passed to Cudd_MakeTreeNode  is the index of a variable (as opposed to its level or position in the order). The group tree  can be created at any time. The result obviously depends on the variable order in effect at creation time.

It is possible to create a variable group tree also before the variables themselves are created. The package assumes in this case that the index of the variables not yet in existence will equal their position in the order when they are created. Therefore, applications that rely on Cudd_bddNewVarAtLevel  or Cudd_addNewVarAtLevel  to create new variables have to create the variables before they group them.

The reordering procedure will skip all groups whose variables are not yet in existence. For groups that are only partially in existence, the reordering procedure will try to reorder the variables already instantiated, without violating the adjacency constraints.


next up previous index
Next: Variable Reordering for ZDDs Up: User's Manual Previous: Variable Reordering for BDDs

Fabio Somenzi
Tue May 12 18:47:58 MDT 1998