src/bdd/cudd/cuddZddPort.c File Reference

#include "util_hack.h"
#include "cuddInt.h"
Include dependency graph for cuddZddPort.c:

Go to the source code of this file.

Functions

static DdNode *zddPortFromBddStep ARGS ((DdManager *dd, DdNode *B, int expected))
static DdNode *zddPortToBddStep ARGS ((DdManager *dd, DdNode *f, int depth))
DdNode * Cudd_zddPortFromBdd (DdManager *dd, DdNode *B)
DdNode * Cudd_zddPortToBdd (DdManager *dd, DdNode *f)
static DdNode * zddPortFromBddStep (DdManager *dd, DdNode *B, int expected)
static DdNode * zddPortToBddStep (DdManager *dd, DdNode *f, int depth)

Variables

static char rcsid[] DD_UNUSED = "$Id: cuddZddPort.c,v 1.1.1.1 2003/02/24 22:23:54 wjiang Exp $"

Function Documentation

static DdNode* zddPortToBddStep ARGS ( (DdManager *dd, DdNode *f, int depth)   )  [static]
static DdNode* zddPortFromBddStep ARGS ( (DdManager *dd, DdNode *B, int expected)   )  [static]

AutomaticStart

DdNode* Cudd_zddPortFromBdd ( DdManager *  dd,
DdNode *  B 
)

AutomaticEnd Function********************************************************************

Synopsis [Converts a BDD into a ZDD.]

Description [Converts a BDD into a ZDD. This function assumes that there is a one-to-one correspondence between the BDD variables and the ZDD variables, and that the variable order is the same for both types of variables. These conditions are established if the ZDD variables are created by one call to Cudd_zddVarsFromBddVars with multiplicity = 1. Returns a pointer to the resulting ZDD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_zddVarsFromBddVars]

Definition at line 100 of file cuddZddPort.c.

00103 {
00104     DdNode *res;
00105 
00106     do {
00107         dd->reordered = 0;
00108         res = zddPortFromBddStep(dd,B,0);
00109     } while (dd->reordered == 1);
00110 
00111     return(res);
00112 
00113 } /* end of Cudd_zddPortFromBdd */

DdNode* Cudd_zddPortToBdd ( DdManager *  dd,
DdNode *  f 
)

Function********************************************************************

Synopsis [Converts a ZDD into a BDD.]

Description [Converts a ZDD into a BDD. Returns a pointer to the resulting ZDD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_zddPortFromBdd]

Definition at line 129 of file cuddZddPort.c.

00132 {
00133     DdNode *res;
00134 
00135     do {
00136         dd->reordered = 0;
00137         res = zddPortToBddStep(dd,f,0);
00138     } while (dd->reordered == 1);
00139 
00140     return(res);
00141 
00142 } /* end of Cudd_zddPortToBdd */

static DdNode* zddPortFromBddStep ( DdManager *  dd,
DdNode *  B,
int  expected 
) [static]

Function********************************************************************

Synopsis [Performs the recursive step of Cudd_zddPortFromBdd.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 166 of file cuddZddPort.c.

00170 {
00171     DdNode      *res, *prevZdd, *t, *e;
00172     DdNode      *Breg, *Bt, *Be;
00173     int         id, level;
00174 
00175     statLine(dd);
00176     /* Terminal cases. */
00177     if (B == Cudd_Not(DD_ONE(dd)))
00178         return(DD_ZERO(dd));
00179     if (B == DD_ONE(dd)) {
00180         if (expected >= dd->sizeZ) {
00181             return(DD_ONE(dd));
00182         } else {
00183             return(dd->univ[expected]);
00184         }
00185     }
00186 
00187     Breg = Cudd_Regular(B);
00188 
00189     /* Computed table look-up. */
00190     res = cuddCacheLookup1Zdd(dd,Cudd_zddPortFromBdd,B);
00191     if (res != NULL) {
00192         level = cuddI(dd,Breg->index);
00193         /* Adding DC vars. */
00194         if (expected < level) {
00195             /* Add suppressed variables. */
00196             cuddRef(res);
00197             for (level--; level >= expected; level--) {
00198                 prevZdd = res;
00199                 id = dd->invperm[level];
00200                 res = cuddZddGetNode(dd, id, prevZdd, prevZdd);
00201                 if (res == NULL) {
00202                     Cudd_RecursiveDerefZdd(dd, prevZdd);
00203                     return(NULL);
00204                 }
00205                 cuddRef(res);
00206                 Cudd_RecursiveDerefZdd(dd, prevZdd);
00207             }
00208             cuddDeref(res);
00209         }
00210         return(res);
00211     }   /* end of cache look-up */
00212 
00213     if (Cudd_IsComplement(B)) {
00214         Bt = Cudd_Not(cuddT(Breg));
00215         Be = Cudd_Not(cuddE(Breg));
00216     } else {
00217         Bt = cuddT(Breg);
00218         Be = cuddE(Breg);
00219     }
00220 
00221     id = Breg->index;
00222     level = cuddI(dd,id);
00223     t = zddPortFromBddStep(dd, Bt, level+1);
00224     if (t == NULL) return(NULL);
00225     cuddRef(t);
00226     e = zddPortFromBddStep(dd, Be, level+1);
00227     if (e == NULL) {
00228         Cudd_RecursiveDerefZdd(dd, t);
00229         return(NULL);
00230     }
00231     cuddRef(e);
00232     res = cuddZddGetNode(dd, id, t, e);
00233     if (res == NULL) {
00234         Cudd_RecursiveDerefZdd(dd, t);
00235         Cudd_RecursiveDerefZdd(dd, e);
00236         return(NULL);
00237     }
00238     cuddRef(res);
00239     Cudd_RecursiveDerefZdd(dd, t);
00240     Cudd_RecursiveDerefZdd(dd, e);
00241 
00242     cuddCacheInsert1(dd,Cudd_zddPortFromBdd,B,res);
00243 
00244     for (level--; level >= expected; level--) {
00245         prevZdd = res;
00246         id = dd->invperm[level];
00247         res = cuddZddGetNode(dd, id, prevZdd, prevZdd);
00248         if (res == NULL) {
00249             Cudd_RecursiveDerefZdd(dd, prevZdd);
00250             return(NULL);
00251         }
00252         cuddRef(res);
00253         Cudd_RecursiveDerefZdd(dd, prevZdd);
00254     }
00255 
00256     cuddDeref(res);
00257     return(res);
00258 
00259 } /* end of zddPortFromBddStep */

static DdNode* zddPortToBddStep ( DdManager *  dd,
DdNode *  f,
int  depth 
) [static]

Function********************************************************************

Synopsis [Performs the recursive step of Cudd_zddPortToBdd.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 274 of file cuddZddPort.c.

00278 {
00279     DdNode *one, *zero, *T, *E, *res, *var;
00280     unsigned int index;
00281     unsigned int level;
00282 
00283     statLine(dd);
00284     one = DD_ONE(dd);
00285     zero = DD_ZERO(dd);
00286     if (f == zero) return(Cudd_Not(one));
00287 
00288     if (depth == dd->sizeZ) return(one);
00289 
00290     index = dd->invpermZ[depth];
00291     level = cuddIZ(dd,f->index);
00292     var = cuddUniqueInter(dd,index,one,Cudd_Not(one));
00293     if (var == NULL) return(NULL);
00294     cuddRef(var);
00295 
00296     if (level > (unsigned) depth) {
00297         E = zddPortToBddStep(dd,f,depth+1);
00298         if (E == NULL) {
00299             Cudd_RecursiveDeref(dd,var);
00300             return(NULL);
00301         }
00302         cuddRef(E);
00303         res = cuddBddIteRecur(dd,var,Cudd_Not(one),E);
00304         if (res == NULL) {
00305             Cudd_RecursiveDeref(dd,var);
00306             Cudd_RecursiveDeref(dd,E);
00307             return(NULL);
00308         }
00309         cuddRef(res);
00310         Cudd_RecursiveDeref(dd,var);
00311         Cudd_RecursiveDeref(dd,E);
00312         cuddDeref(res);
00313         return(res);
00314     }
00315 
00316     res = cuddCacheLookup1(dd,Cudd_zddPortToBdd,f);
00317     if (res != NULL) {
00318         Cudd_RecursiveDeref(dd,var);
00319         return(res);
00320     }
00321 
00322     T = zddPortToBddStep(dd,cuddT(f),depth+1);
00323     if (T == NULL) {
00324         Cudd_RecursiveDeref(dd,var);
00325         return(NULL);
00326     }
00327     cuddRef(T);
00328     E = zddPortToBddStep(dd,cuddE(f),depth+1);
00329     if (E == NULL) {
00330         Cudd_RecursiveDeref(dd,var);
00331         Cudd_RecursiveDeref(dd,T);
00332         return(NULL);
00333     }
00334     cuddRef(E);
00335 
00336     res = cuddBddIteRecur(dd,var,T,E);
00337     if (res == NULL) {
00338         Cudd_RecursiveDeref(dd,var);
00339         Cudd_RecursiveDeref(dd,T);
00340         Cudd_RecursiveDeref(dd,E);
00341         return(NULL);
00342     }
00343     cuddRef(res);
00344     Cudd_RecursiveDeref(dd,var);
00345     Cudd_RecursiveDeref(dd,T);
00346     Cudd_RecursiveDeref(dd,E);
00347     cuddDeref(res);
00348 
00349     cuddCacheInsert1(dd,Cudd_zddPortToBdd,f,res);
00350 
00351     return(res);
00352 
00353 } /* end of zddPortToBddStep */

Variable Documentation

char rcsid [] DD_UNUSED = "$Id: cuddZddPort.c,v 1.1.1.1 2003/02/24 22:23:54 wjiang Exp $" [static]

CFile***********************************************************************

FileName [cuddZddPort.c]

PackageName [cudd]

Synopsis [Functions that translate BDDs to ZDDs.]

Description [External procedures included in this module:

Internal procedures included in this module:

procedures included in this module:

]

SeeAlso []

Author [Hyong-kyoon Shin, In-Ho Moon]

Copyright [ This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.]

Definition at line 58 of file cuddZddPort.c.

Generated on Tue Jan 5 12:18:57 2010 for abc70930 by  doxygen 1.6.1