BuDDy: A BDD package

Programming with BuDDy

First of all a program needs to call 
 bdd_init(nodenum,cachesize);
to initialize the BDD package. The nodenum parameter sets the initial number of BDD nodes and cachesize sets the size of the caches used for the BDD operators (not the unique node table). These caches are used for bdd_apply among others.

Good initial values are

Too few nodes will only result in reduced performance as this increases the number of garbage collections needed. If the package needs more nodes, then it will automatically increase the size of the node table. Use bdd_setminfreenodes to change the parameters for when this is done and use bdd_setcacheratio to enable dynamical resizing of the operator caches. You may also use the function bdd_setmaxincrease to adjust how BuDDy resizes the node table.

After the initialization a call must be done to bdd_setvarnum to define how many variables to use in this session. This number may be increased later on either by calls to bdd_setvarnum or to bdd_extvarnum.

The atomic functions for getting new BDD nodes are bdd_ithvar(i) and bdd_nithvar(i) which return references to BDD nodes of the form $(v_i,0,1)$ and $(v_i,1,0)$. The nodes constructed in this way correspond to the positive and negative versions of a single variable. Initially the variable order is $v_0 < v_1 < \ldots < v_{n-1} < v_n$.

The BDDs returned from bdd_ithvar can then be used to form new BDDs by calling bdd_apply(a,b,op) where op may be bddop_and or any of the other operators defined in bdd.h. The bdd_apply function performs the binary operation indicated by op. Use bdd_not to negate a BDD. The result from bdd_apply and any other BDD operator must be handed over to bdd_addref to increase the reference count of the node before any other operation is performed. This is done to prevent the BDD from being garbage collected. When a BDD is no longer in use, it can be de-referenced by a call to bdd_delref. The exceptions to this are the return values from bdd_ithvar and bdd_nithvar. These do not need to be reference counted, although it is not an error to do so. The use of the BDD package ends with a call to bdd_done.

The example below demonstrates the standard C interface to BuDDy. In this mode both bdd and BDD can be used as BuDDy BDD types. The C interface requires the user to ensure garbage collection is handled correctly. This means calling bdd_addref every time a new BDD is created, and bdd_delref whenever a BDD is not in use anymore.

 #include <bdd.h>

 main(void)
 {
    bdd x,y,z;

    bdd_init(1000,100);
    bdd_setvarnum(5);

    x = bdd_ithvar(0);
    y = bdd_ithvar(1);
    z = bdd_addref(bdd_apply(x,y,bddop_and));

    bdd_printtable(z);
    bdd_delref(z);
    bdd_done();
 }

The following code demonstrates the C++ interface to BuDDy. In this mode bdd is a C++ class that wraps a handler around the standard C interface, and the BDD type referes to the standard C BDD type. The C++ interface handles all garbage collection, so no calls to bdd_addref and bdd_delref are needed.

 #include <bdd.h>

 main(void)
 {
    bdd x,y,z;

    bdd_init(1000,100);
    bdd_setvarnum(5);

    x = bdd_ithvar(0);
    y = bdd_ithvar(1);
    z = x & y;

    cout << bddtable << z << endl;

    bdd_done();
 }

Information on the BDDs can be found using the bdd_var, bdd_low and bdd_high functions that returns the variable labelling a BDD, the low branch and the high branch of a BDD.

Printing BDDs is done using the functions bdd_printall that prints all used nodes, bdd_printtable that prints the part of the nodetable that corresponds to a specific BDD and bdd_printset that prints a specific BDD as a list of elements in a set (all paths ending in the true terminal).

More Examples

More complex examples can be found in the buddy/examples directory.

Variable sets

For some functions like bdd_exist it is possible to pass a whole set of variables to be quantified, using BDDs that represent the variables. These BDDs are simply the conjunction of all the variables in their positive form and can either be build that way or by a call to bdd_makeset. For the bdd_restrict function the variables need to be included in both positive and negative form which can only be done manually.

If for example variable 1 and variable 3 are to be included in a set, then it can be done in two ways, as shown below.

 #include <bdd.h>

 main()
 {
    bdd v1, v3;
    bdd seta, setb;
    static int v[2] = {1,3};
    
    bdd_init(100,100);
    bdd_setvarnum(5);

    v1 = bdd_ithvar(1);
    v3 = bdd_ithvar(3);

       // One way 
    seta = bdd_addref( bdd_apply(v1,v3,bddop_and) );
    bdd_printtable(seta);

       // Another way 
    setb = bdd_addref( bdd_makeset(v,2) );
    bdd_printtable(setb);
 }

Dynamic Variable Reordering

Dynamic variable reordering can be done using the functions bdd_reorder(int method) (bd_reorder) and bdd_autoreorder(int method) (bdd_autoreorder), where the parameter method, for instance can be BDD_REORDER_WIN2ITE. The package must know how the BDD variables are related to each other, so the user must define blocks of BDD variables, using bdd_addvarblock(bdd var, int fixed) (bdd_addvarblock). A block is a range of BDD variables that should be kept together. It may either be a simple contiguous sequence of variables or a sequence of other blocks with ranges inside their parents range. In this way all the blocks form a tree of ranges. Partially overlapping blocks are not allowed.

Example: Assume the block $v_0\ldots v_9$, is added as the first block and then the block $v_1\ldots v_8$. This yields the $v_0\ldots v_9$ block at the top, with the $v_1\ldots v_8$ block as a child. If now the block $v_1\ldots v_4$ was added, it would become a child of the $v_1\ldots v_8$ block, similarly the block $v_5\ldots v_8$ would be a child of the $v_1\ldots v_8$ block. If we add the variables $v_1$, $v_2$, $v_3$ and $v_4$ as single variable blocks we at last get tree shown below. If all variables should be added as single variable blocks then bdd_varblockall can be used instead of doing it manually.

varblock.png

The reordering algorithm is then to first reorder the top most blocks and there after descend into each block and reorder these recursively, unless the block is defined as a fixed block.

If the user want to control the swapping of variables himself, then the functions bdd_swapvar and bdd_setvarorder may be used. But this is not possible in conjunction with the use of variable blocks and the bdd_swapvar is unfortunately quite slow since a full scan of all the nodes must be done both before and after the swap. Other reordering functions are bdd_autoreorder_times, bdd_reorder_verbose, bdd_sizeprobe_hook and bdd_reorder_hook.

Error Handling

If an error occurs then a check is done to see if there is any error handler defined and if so it is called with the error code of interest. The default error handler prints an error message on stderr and then aborts the program. A handler can also be defined by the user with a call to bdd_error_hook.

The C++ interface

Mostly this consists of a set of overloaded function wrappers that takes a bdd class and calls the appropriate C functions with the root number stored in the bdd class. The names of these wrappers are exactly the same as for the C functions. In addition to this a lot of the C++ operators like | & - = == are overloaded in order to perform most of the bdd_apply operations. These are listed together with bdd_apply. The rest are

       Operator Description Return value
       =        assignment 
       ==       test        returns 1 if two BDDs are equal, otherwise 0 
       !=       test        returns 0 if two BDDs are equal, otherwise 1 
       bdd.id() identity    returns the root number of the BDD

The default constructor for the bdd class initializes the bdds to the constant false value. Reference counting is totally automatic when the bdd class is used, here the constructors and destructors takes care of all reference counting! The C++ interface is also defined in bdd.h so nothing extra is needed to use it.

Finite Domain Blocks

Included in the BDD package is a set of functions for manipulating values of finite domains, like for example finite state machines. These functions are used to allocate blocks of BDD variables to represent integer values instead of only true and false.

New finite domain blocks are allocated using fdd_extdomain and BDDs representing integer values can be build using fdd_ithvar. The BDD representing identity between two sets of different domains can be build using fdd_equals. BDDs representing finite domain sets can be printed using fdd_printset and the overloaded C++ operator <<. Pairs for bdd_replace can be made using fdd_setpair and variable sets can be made using fdd_ithset and fdd_makeset. The finite domain block interface is defined for both C and C++. To use this interface you must include fdd.h.

Encoding using FDDs are done with the Least Significant Bits first in the ordering (top of the BDD). Assume variables $V_0 \ldots V_3$ are used to encode the value 12 - this would yield $V_0=0, V_1=0, V_2=1, V_3=1$.

An example program using the FDD interface can be found in the examples directory.

Boolean Vectors

Another interface layer for BuDDy implements boolean vectors for use with integer arithmetics. A boolean vector is simply an array of BDDs where each BDD represents one bit of an expression. To use this interface you must include bvec.h. As an example, suppose we want to express the following assignment from an expression

\[ x := y + 10 \]

what we do is to encode the variable $y$ and the value 10 as boolean vectors $y$ and $v$ of a fixed length. Assume we use four bits with LSB to the right, then we get

\[ y = \langle y_4, \ldots, y_1 \rangle \]

\[ v = \langle 1,0,1,0 \rangle \]

where each $y_i$ is the BDD variable used to encode the integer variable $y$. Now the result of the addition can be expressed as the vector $z = \langle z_4, \ldots, z_1\rangle $ where each $z_i$ is:

\[ z_i = y_i\ \mbox{xor}\ v_i\ \mbox{xor}\ c_{i-1} \]

and the carry in $c_i$ is

\[ c_i = (y_i\ \mbox{and}\ v_i)\ \mbox{or}\ (c_{i-1}\ \mbox{and} \ (y_i\ \mbox{or}\ v_i)). \]

with $c_0$ = 0. What is left now is to assign the result to $x$. This is a conjunction of a biimplication of each element in the vectors, so the result is

\[ R = \bigwedge_{i=1}^4 x_i \Leftrightarrow z_i. \]

The above example could be carried out with the following C++ program that utilizes the FDD interface for printing the result.

 #include "bvec.h"

 main()
 {
    int domain[2] = {16,16};

    bdd_init(100,100);
    fdd_extdomain(domain, 2);

    bvec y = bvec_varfdd(0);
    bvec v = bvec_con(4, 10);
    bvec z = bvec_add(y, v);

    bvec x = bvec_varfdd(1);
    bdd  result = bddtrue;
    
    for (int n=0 ; n<x.bitnum() ; n++)
       result &= bdd_apply(x[n], z[n], bddop_biimp);

    cout << fddset << result << endl << endl;
 }

The relational operators $<,>,\leq,\geq,=,\neq$ can also be encoded. Assume we want to encode $x \leq y$ using the same variables as in the above example. This would be done as:

 #include "bvec.h"

 main()
 {
    int domain[2] = {16,16};

    bdd_init(100,100);
    fdd_extdomain(domain, 2);

    bvec y = bvec_varfdd(1);
    bvec x = bvec_varfdd(0);

    bdd  result = bvec_lte(x,y);

    cout << fddset << result << endl << endl;
 }

Please note that all vectors that are returned from any of the bvec_xxx functions are referenced counted by the system.

The C++ interface defines the class 
 class bvec
 {
  public:

    bvec(void);
    bvec(int bitnum);
    bvec(int bitnum, int val);
    bvec(const bvec &v);
    ~bvec(void);

    void set(int i, const bdd &b);
    bdd operator[](int i)  const;
    int bitnum(void) const;
    int empty(void) const;
    bvec operator=(const bvec &src);
 }

The default constructor makes an empty vector with no elements, the integer constructor creates a vector with bitnum elements (all set to false) and the third constructor creates a vector with bitnum elements and assigns the integer value val to the vector. Reference counting is done automatically. The i'th element in the vector can be changed with set and read with operator[]. The number of bits can be found with bitnum and the method empty returns true if the vector is a NULL vector.

Efficiency Concerns

Getting the most out of any BDD package is not always easy. It requires some knowledge about the optimal order of the BDD variables and it also helps if you have some knowledge of the internals of the package.

So, to sum it up: if you want speed, then allocate as many nodes as possible, use small cache ratios and set maxincrease. If you need memory, then allocate a small number of nodes from the beginning, use a fixed size cache, do not change maxincrease and lower minfreenodes.

Some Implementation details

Generated on Mon Jul 23 13:25:13 2007 for BuDDy by  doxygen 1.5.1