next up previous index
Next: Converting ADDs to BDDs Up: User's Manual Previous: Basic ADD Manipulation

Basic ZDD Manipulation


ZDDs are often generated by converting  existing BDDs. (See Section 3.11.) However, it is also possible to build ZDDs by applying boolean operators to other ZDDs, starting from constants and projection  functions. The following fragment of code illustrates how to build the ZDD for the function tex2html_wrap_inline2292. We assume that the four variables already exist in the manager when the ZDD for f is built. Note the use of De Morgan's law.

        DdManager *manager;
        DdNode *f, *var, *tmp;
        int i;

        manager = Cudd_Init(0,4,CUDD_UNIQUE_SLOTS,

        tmp = Cudd_ReadZddOne(manager,0);
        for (i = 3; i >= 0; i--) {
            var = Cudd_zddIthVar(manager,i);
            f = Cudd_zddIntersect(manager,var,tmp);
            tmp = f;
        f = Cudd_zddDiff(manager,Cudd_ReadZddOne(manager,0),tmp);
This example illustrates the following points: CUDD provides functions for the manipulation of covers  represented by ZDDs. For instance, Cudd_zddIsop  builds a ZDD representing an irredundant  sum of products for the incompletely specified function defined by the two BDDs L and U. Cudd_zddWeakDiv  performs the weak division of two covers given as ZDDs. These functions expect the two ZDD variables corresponding to the two literals of the function variable to be adjacent. One has to create variable groups (see Section 3.14) for reordering  of the ZDD variables to work. BDD automatic reordering is safe even without groups: If realignment of ZDD and ADD/BDD variables is requested (see Section 3.15) groups will be kept adjacent.

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