(this file is automatically generated from Java source)
Back to book index.

Basic BDD tutorial

This tutorial explains the basic BDD operations. It assumes however, that you are familiar with BDDs & co.

Creating a BDD object

The first thing to do, is to create a BDD object. This BDD object is your base for BDD operations. You may have several BDD objects in the same applications, you may however not exchange information between these. To create your a BDD object, you must specify the size of initial nodetable and cache. In this example we will use the values 10000 and 1000:

BDD bdd= new BDD(1000,1000);

Allocating variables

Before you can use you BDD object any further, you must create some BDD variables. It is recommended that you create BDD variables only in the beginning of your work. BDD variables are in JDD represented by Java integer:

int v1 = bdd.createVar();
int v2 = bdd.createVar();
int v3 = bdd.createVar();

Also, there are two special BDD variables that you do not need to allocate. These two are the boolean TRUE and FALSE. They are given the Java integer values 1 and 0.

BDD operations

BDD operations are carried out by simply calling the corresponding function in BDD:

int x = bdd.and(v1,v2);
int y = bdd.xor(v1,v3);
int z = bdd.not(v2);

You have now created three BDD trees.

Reference counting

Each BDD tree has a reference count. if this number is zero, your BDD tree may become removed by the internal garbage collector.The rule of thumb when working with BDDs is to reference your trees as soon as you get them, then de-reference them when you don need them anymore and they will be removed by the garbage collector at some future point:

bdd.ref(x);
bdd.ref(y);
bdd.ref(z);

And when you are done with them, you just do this

bdd.deref(i_dont_need_this_bdd_anymore);

Examining BDD trees

It might be useful to actually see your BDDs. For that, JDD contains a set of functions. You can print the BDD as a set or a cube:

bdd.printSet(y);
bdd.printCubes(y);

0-1
1-0

 v3
 v1

However, the best way to visualize a BDD is to draw its graph.
To do this, JDD uses AT&T dot, which must be installed in your system and available from your shell prompt [i.e. in your $PATH].

bdd.printDot("x", x);	bdd.printDot("y", y);	bdd.printDot("v1", v1);

Quantification

You are allowed to apply exists and forall to a BDD tree.

The first thing you need to do is to create the cube of variables to be quantified. For example, if you would like to compute (forall x(v1v2) ), you may do this:

int cube = jdd.ref( jdd.and(v1,v2) );

Then you can carry out the quantification:

int x2 = jdd.ref( jdd.forall(x,cube) );

Note that we demonstrated the proper use of ref() here.

The exists() operators work similarly. Furthermore, there is a relProd operator that computes the relational product, i.e. exists C. X and Y = relProd(X,Y,C). This operations is very useful during image computation in model checking, for example.

There also exists a createCube function that you might find useful.

Variable substitution

It is sometimes desired to substitute variables in a tree. To do this, you first need a JDD permutation:

int []p1 = new int[]{ v1 };
int []p2 = new int[]{ v2 };
Permutation perm1 = bdd.createPermutation(p1, p2);
Permutation perm2 = bdd.createPermutation(p2, p1);

Now we have two permutation to change from v1 to v2 and vice versa. To use it, just call the replace() operations:

int v12 = bdd.replace( v1, perm1);	int v21 = bdd.replace( v2, perm2);

As you can see, we have swapped v1 and v2 in these tress...