src/bdd/cudd/cuddBridge.c File Reference

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

Go to the source code of this file.

Functions

static DdNode *addBddDoThreshold ARGS ((DdManager *dd, DdNode *f, DdNode *val))
static DdNode *addBddDoInterval ARGS ((DdManager *dd, DdNode *f, DdNode *l, DdNode *u))
static DdNode *addBddDoIthBit ARGS ((DdManager *dd, DdNode *f, DdNode *index))
static DdNode *ddBddToAddRecur ARGS ((DdManager *dd, DdNode *B))
static DdNode *cuddBddTransferRecur ARGS ((DdManager *ddS, DdManager *ddD, DdNode *f, st_table *table))
DdNode * Cudd_addBddThreshold (DdManager *dd, DdNode *f, CUDD_VALUE_TYPE value)
DdNode * Cudd_addBddStrictThreshold (DdManager *dd, DdNode *f, CUDD_VALUE_TYPE value)
DdNode * Cudd_addBddInterval (DdManager *dd, DdNode *f, CUDD_VALUE_TYPE lower, CUDD_VALUE_TYPE upper)
DdNode * Cudd_addBddIthBit (DdManager *dd, DdNode *f, int bit)
DdNode * Cudd_BddToAdd (DdManager *dd, DdNode *B)
DdNode * Cudd_addBddPattern (DdManager *dd, DdNode *f)
DdNode * Cudd_bddTransfer (DdManager *ddSource, DdManager *ddDestination, DdNode *f)
DdNode * cuddBddTransfer (DdManager *ddS, DdManager *ddD, DdNode *f)
DdNode * cuddAddBddDoPattern (DdManager *dd, DdNode *f)
static DdNode * addBddDoThreshold (DdManager *dd, DdNode *f, DdNode *val)
static DdNode * addBddDoStrictThreshold (DdManager *dd, DdNode *f, DdNode *val)
static DdNode * addBddDoInterval (DdManager *dd, DdNode *f, DdNode *l, DdNode *u)
static DdNode * addBddDoIthBit (DdManager *dd, DdNode *f, DdNode *index)
static DdNode * ddBddToAddRecur (DdManager *dd, DdNode *B)
static DdNode * cuddBddTransferRecur (DdManager *ddS, DdManager *ddD, DdNode *f, st_table *table)

Variables

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

Function Documentation

static DdNode* addBddDoInterval ( DdManager *  dd,
DdNode *  f,
DdNode *  l,
DdNode *  u 
) [static]

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

Synopsis [Performs the recursive step for Cudd_addBddInterval.]

Description [Performs the recursive step for Cudd_addBddInterval. Returns a pointer to the BDD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [addBddDoThreshold addBddDoStrictThreshold]

Definition at line 677 of file cuddBridge.c.

00682 {
00683     DdNode *res, *T, *E;
00684     DdNode *fv, *fvn;
00685     int v;
00686 
00687     statLine(dd);
00688     /* Check terminal case. */
00689     if (cuddIsConstant(f)) {
00690         return(Cudd_NotCond(DD_ONE(dd),cuddV(f) < cuddV(l) || cuddV(f) > cuddV(u)));
00691     }
00692 
00693     /* Check cache. */
00694     res = cuddCacheLookup(dd,DD_ADD_BDD_DO_INTERVAL_TAG,f,l,u);
00695     if (res != NULL) return(res);
00696 
00697     /* Recursive step. */
00698     v = f->index;
00699     fv = cuddT(f); fvn = cuddE(f);
00700 
00701     T = addBddDoInterval(dd,fv,l,u);
00702     if (T == NULL) return(NULL);
00703     cuddRef(T);
00704 
00705     E = addBddDoInterval(dd,fvn,l,u);
00706     if (E == NULL) {
00707         Cudd_RecursiveDeref(dd, T);
00708         return(NULL);
00709     }
00710     cuddRef(E);
00711     if (Cudd_IsComplement(T)) {
00712         res = (T == E) ? Cudd_Not(T) : cuddUniqueInter(dd,v,Cudd_Not(T),Cudd_Not(E));
00713         if (res == NULL) {
00714             Cudd_RecursiveDeref(dd, T);
00715             Cudd_RecursiveDeref(dd, E);
00716             return(NULL);
00717         }
00718         res = Cudd_Not(res);
00719     } else {
00720         res = (T == E) ? T : cuddUniqueInter(dd,v,T,E);
00721         if (res == NULL) {
00722             Cudd_RecursiveDeref(dd, T);
00723             Cudd_RecursiveDeref(dd, E);
00724             return(NULL);
00725         }
00726     }
00727     cuddDeref(T);
00728     cuddDeref(E);
00729 
00730     /* Store result. */
00731     cuddCacheInsert(dd,DD_ADD_BDD_DO_INTERVAL_TAG,f,l,u,res);
00732 
00733     return(res);
00734 
00735 } /* end of addBddDoInterval */

static DdNode* addBddDoIthBit ( DdManager *  dd,
DdNode *  f,
DdNode *  index 
) [static]

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

Synopsis [Performs the recursive step for Cudd_addBddIthBit.]

Description [Performs the recursive step for Cudd_addBddIthBit. Returns a pointer to the BDD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 751 of file cuddBridge.c.

00755 {
00756     DdNode *res, *T, *E;
00757     DdNode *fv, *fvn;
00758     int mask, value;
00759     int v;
00760 
00761     statLine(dd);
00762     /* Check terminal case. */
00763     if (cuddIsConstant(f)) {
00764         mask = 1 << ((int) cuddV(index));
00765         value = (int) cuddV(f);
00766         return(Cudd_NotCond(DD_ONE(dd),(value & mask) == 0));
00767     }
00768 
00769     /* Check cache. */
00770     res = cuddCacheLookup2(dd,addBddDoIthBit,f,index);
00771     if (res != NULL) return(res);
00772 
00773     /* Recursive step. */
00774     v = f->index;
00775     fv = cuddT(f); fvn = cuddE(f);
00776 
00777     T = addBddDoIthBit(dd,fv,index);
00778     if (T == NULL) return(NULL);
00779     cuddRef(T);
00780 
00781     E = addBddDoIthBit(dd,fvn,index);
00782     if (E == NULL) {
00783         Cudd_RecursiveDeref(dd, T);
00784         return(NULL);
00785     }
00786     cuddRef(E);
00787     if (Cudd_IsComplement(T)) {
00788         res = (T == E) ? Cudd_Not(T) : cuddUniqueInter(dd,v,Cudd_Not(T),Cudd_Not(E));
00789         if (res == NULL) {
00790             Cudd_RecursiveDeref(dd, T);
00791             Cudd_RecursiveDeref(dd, E);
00792             return(NULL);
00793         }
00794         res = Cudd_Not(res);
00795     } else {
00796         res = (T == E) ? T : cuddUniqueInter(dd,v,T,E);
00797         if (res == NULL) {
00798             Cudd_RecursiveDeref(dd, T);
00799             Cudd_RecursiveDeref(dd, E);
00800             return(NULL);
00801         }
00802     }
00803     cuddDeref(T);
00804     cuddDeref(E);
00805 
00806     /* Store result. */
00807     cuddCacheInsert2(dd,addBddDoIthBit,f,index,res);
00808 
00809     return(res);
00810 
00811 } /* end of addBddDoIthBit */

static DdNode* addBddDoStrictThreshold ( DdManager *  dd,
DdNode *  f,
DdNode *  val 
) [static]

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

Synopsis [Performs the recursive step for Cudd_addBddStrictThreshold.]

Description [Performs the recursive step for Cudd_addBddStrictThreshold. Returns a pointer to the BDD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [addBddDoThreshold]

Definition at line 604 of file cuddBridge.c.

00608 {
00609     DdNode *res, *T, *E;
00610     DdNode *fv, *fvn;
00611     int v;
00612 
00613     statLine(dd);
00614     /* Check terminal case. */
00615     if (cuddIsConstant(f)) {
00616         return(Cudd_NotCond(DD_ONE(dd),cuddV(f) <= cuddV(val)));
00617     }
00618 
00619     /* Check cache. */
00620     res = cuddCacheLookup2(dd,addBddDoStrictThreshold,f,val);
00621     if (res != NULL) return(res);
00622 
00623     /* Recursive step. */
00624     v = f->index;
00625     fv = cuddT(f); fvn = cuddE(f);
00626 
00627     T = addBddDoStrictThreshold(dd,fv,val);
00628     if (T == NULL) return(NULL);
00629     cuddRef(T);
00630 
00631     E = addBddDoStrictThreshold(dd,fvn,val);
00632     if (E == NULL) {
00633         Cudd_RecursiveDeref(dd, T);
00634         return(NULL);
00635     }
00636     cuddRef(E);
00637     if (Cudd_IsComplement(T)) {
00638         res = (T == E) ? Cudd_Not(T) : cuddUniqueInter(dd,v,Cudd_Not(T),Cudd_Not(E));
00639         if (res == NULL) {
00640             Cudd_RecursiveDeref(dd, T);
00641             Cudd_RecursiveDeref(dd, E);
00642             return(NULL);
00643         }
00644         res = Cudd_Not(res);
00645     } else {
00646         res = (T == E) ? T : cuddUniqueInter(dd,v,T,E);
00647         if (res == NULL) {
00648             Cudd_RecursiveDeref(dd, T);
00649             Cudd_RecursiveDeref(dd, E);
00650             return(NULL);
00651         }
00652     }
00653     cuddDeref(T);
00654     cuddDeref(E);
00655 
00656     /* Store result. */
00657     cuddCacheInsert2(dd,addBddDoStrictThreshold,f,val,res);
00658 
00659     return(res);
00660 
00661 } /* end of addBddDoStrictThreshold */

static DdNode* addBddDoThreshold ( DdManager *  dd,
DdNode *  f,
DdNode *  val 
) [static]

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

Synopsis [Performs the recursive step for Cudd_addBddThreshold.]

Description [Performs the recursive step for Cudd_addBddThreshold. Returns a pointer to the BDD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [addBddDoStrictThreshold]

Definition at line 531 of file cuddBridge.c.

00535 {
00536     DdNode *res, *T, *E;
00537     DdNode *fv, *fvn;
00538     int v;
00539 
00540     statLine(dd);
00541     /* Check terminal case. */
00542     if (cuddIsConstant(f)) {
00543         return(Cudd_NotCond(DD_ONE(dd),cuddV(f) < cuddV(val)));
00544     }
00545 
00546     /* Check cache. */
00547     res = cuddCacheLookup2(dd,addBddDoThreshold,f,val);
00548     if (res != NULL) return(res);
00549 
00550     /* Recursive step. */
00551     v = f->index;
00552     fv = cuddT(f); fvn = cuddE(f);
00553 
00554     T = addBddDoThreshold(dd,fv,val);
00555     if (T == NULL) return(NULL);
00556     cuddRef(T);
00557 
00558     E = addBddDoThreshold(dd,fvn,val);
00559     if (E == NULL) {
00560         Cudd_RecursiveDeref(dd, T);
00561         return(NULL);
00562     }
00563     cuddRef(E);
00564     if (Cudd_IsComplement(T)) {
00565         res = (T == E) ? Cudd_Not(T) : cuddUniqueInter(dd,v,Cudd_Not(T),Cudd_Not(E));
00566         if (res == NULL) {
00567             Cudd_RecursiveDeref(dd, T);
00568             Cudd_RecursiveDeref(dd, E);
00569             return(NULL);
00570         }
00571         res = Cudd_Not(res);
00572     } else {
00573         res = (T == E) ? T : cuddUniqueInter(dd,v,T,E);
00574         if (res == NULL) {
00575             Cudd_RecursiveDeref(dd, T);
00576             Cudd_RecursiveDeref(dd, E);
00577             return(NULL);
00578         }
00579     }
00580     cuddDeref(T);
00581     cuddDeref(E);
00582 
00583     /* Store result. */
00584     cuddCacheInsert2(dd,addBddDoThreshold,f,val,res);
00585 
00586     return(res);
00587 
00588 } /* end of addBddDoThreshold */

static DdNode* cuddBddTransferRecur ARGS ( (DdManager *ddS, DdManager *ddD, DdNode *f, st_table *table)   )  [static]
static DdNode* ddBddToAddRecur ARGS ( (DdManager *dd, DdNode *B)   )  [static]
static DdNode* addBddDoIthBit ARGS ( (DdManager *dd, DdNode *f, DdNode *index)   )  [static]
static DdNode* addBddDoInterval ARGS ( (DdManager *dd, DdNode *f, DdNode *l, DdNode *u)   )  [static]
static DdNode *addBddDoStrictThreshold ARGS ( (DdManager *dd, DdNode *f, DdNode *val)   )  [static]

AutomaticStart

DdNode* Cudd_addBddInterval ( DdManager *  dd,
DdNode *  f,
CUDD_VALUE_TYPE  lower,
CUDD_VALUE_TYPE  upper 
)

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

Synopsis [Converts an ADD to a BDD.]

Description [Converts an ADD to a BDD by replacing all discriminants greater than or equal to lower and less than or equal to upper with 1, and all other discriminants with 0. Returns a pointer to the resulting BDD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_addBddThreshold Cudd_addBddStrictThreshold Cudd_addBddPattern Cudd_BddToAdd]

Definition at line 205 of file cuddBridge.c.

00210 {
00211     DdNode *res;
00212     DdNode *l;
00213     DdNode *u;
00214     
00215     /* Create constant nodes for the interval bounds, so that we can use
00216     ** the global cache.
00217     */
00218     l = cuddUniqueConst(dd,lower);
00219     if (l == NULL) return(NULL);
00220     cuddRef(l);
00221     u = cuddUniqueConst(dd,upper);
00222     if (u == NULL) {
00223         Cudd_RecursiveDeref(dd,l);
00224         return(NULL);
00225     }
00226     cuddRef(u);
00227 
00228     do {
00229         dd->reordered = 0;
00230         res = addBddDoInterval(dd, f, l, u);
00231     } while (dd->reordered == 1);
00232 
00233     if (res == NULL) {
00234         Cudd_RecursiveDeref(dd, l);
00235         Cudd_RecursiveDeref(dd, u);
00236         return(NULL);
00237     }
00238     cuddRef(res);
00239     Cudd_RecursiveDeref(dd, l);
00240     Cudd_RecursiveDeref(dd, u);
00241     cuddDeref(res);
00242     return(res);
00243 
00244 } /* end of Cudd_addBddInterval */

DdNode* Cudd_addBddIthBit ( DdManager *  dd,
DdNode *  f,
int  bit 
)

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

Synopsis [Converts an ADD to a BDD by extracting the i-th bit from the leaves.]

Description [Converts an ADD to a BDD by replacing all discriminants whose i-th bit is equal to 1 with 1, and all other discriminants with 0. The i-th bit refers to the integer representation of the leaf value. If the value is has a fractional part, it is ignored. Repeated calls to this procedure allow one to transform an integer-valued ADD into an array of BDDs, one for each bit of the leaf values. Returns a pointer to the resulting BDD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_addBddInterval Cudd_addBddPattern Cudd_BddToAdd]

Definition at line 267 of file cuddBridge.c.

00271 {
00272     DdNode *res;
00273     DdNode *index;
00274     
00275     index = cuddUniqueConst(dd,(CUDD_VALUE_TYPE) bit);
00276     if (index == NULL) return(NULL);
00277     cuddRef(index);
00278 
00279     do {
00280         dd->reordered = 0;
00281         res = addBddDoIthBit(dd, f, index);
00282     } while (dd->reordered == 1);
00283 
00284     if (res == NULL) {
00285         Cudd_RecursiveDeref(dd, index);
00286         return(NULL);
00287     }
00288     cuddRef(res);
00289     Cudd_RecursiveDeref(dd, index);
00290     cuddDeref(res);
00291     return(res);
00292 
00293 } /* end of Cudd_addBddIthBit */

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

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

Synopsis [Converts an ADD to a BDD.]

Description [Converts an ADD to a BDD by replacing all discriminants different from 0 with 1. Returns a pointer to the resulting BDD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_BddToAdd Cudd_addBddThreshold Cudd_addBddInterval Cudd_addBddStrictThreshold]

Definition at line 340 of file cuddBridge.c.

00343 {
00344     DdNode *res;
00345     
00346     do {
00347         dd->reordered = 0;
00348         res = cuddAddBddDoPattern(dd, f);
00349     } while (dd->reordered == 1);
00350     return(res);
00351 
00352 } /* end of Cudd_addBddPattern */

DdNode* Cudd_addBddStrictThreshold ( DdManager *  dd,
DdNode *  f,
CUDD_VALUE_TYPE  value 
)

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

Synopsis [Converts an ADD to a BDD.]

Description [Converts an ADD to a BDD by replacing all discriminants STRICTLY greater than value with 1, and all other discriminants with 0. Returns a pointer to the resulting BDD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_addBddInterval Cudd_addBddPattern Cudd_BddToAdd Cudd_addBddThreshold]

Definition at line 160 of file cuddBridge.c.

00164 {
00165     DdNode *res;
00166     DdNode *val;
00167     
00168     val = cuddUniqueConst(dd,value);
00169     if (val == NULL) return(NULL);
00170     cuddRef(val);
00171 
00172     do {
00173         dd->reordered = 0;
00174         res = addBddDoStrictThreshold(dd, f, val);
00175     } while (dd->reordered == 1);
00176 
00177     if (res == NULL) {
00178         Cudd_RecursiveDeref(dd, val);
00179         return(NULL);
00180     }
00181     cuddRef(res);
00182     Cudd_RecursiveDeref(dd, val);
00183     cuddDeref(res);
00184     return(res);
00185 
00186 } /* end of Cudd_addBddStrictThreshold */

DdNode* Cudd_addBddThreshold ( DdManager *  dd,
DdNode *  f,
CUDD_VALUE_TYPE  value 
)

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

Synopsis [Converts an ADD to a BDD.]

Description [Converts an ADD to a BDD by replacing all discriminants greater than or equal to value with 1, and all other discriminants with 0. Returns a pointer to the resulting BDD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_addBddInterval Cudd_addBddPattern Cudd_BddToAdd Cudd_addBddStrictThreshold]

Definition at line 115 of file cuddBridge.c.

00119 {
00120     DdNode *res;
00121     DdNode *val;
00122     
00123     val = cuddUniqueConst(dd,value);
00124     if (val == NULL) return(NULL);
00125     cuddRef(val);
00126 
00127     do {
00128         dd->reordered = 0;
00129         res = addBddDoThreshold(dd, f, val);
00130     } while (dd->reordered == 1);
00131 
00132     if (res == NULL) {
00133         Cudd_RecursiveDeref(dd, val);
00134         return(NULL);
00135     }
00136     cuddRef(res);
00137     Cudd_RecursiveDeref(dd, val);
00138     cuddDeref(res);
00139     return(res);
00140 
00141 } /* end of Cudd_addBddThreshold */

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

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

Synopsis [Converts a BDD to a 0-1 ADD.]

Description [Converts a BDD to a 0-1 ADD. Returns a pointer to the resulting ADD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_addBddPattern Cudd_addBddThreshold Cudd_addBddInterval Cudd_addBddStrictThreshold]

Definition at line 310 of file cuddBridge.c.

00313 {
00314     DdNode *res;
00315 
00316     do {
00317         dd->reordered = 0;
00318         res = ddBddToAddRecur(dd, B);
00319     } while (dd->reordered ==1);
00320     return(res);
00321 
00322 } /* end of Cudd_BddToAdd */

DdNode* Cudd_bddTransfer ( DdManager *  ddSource,
DdManager *  ddDestination,
DdNode *  f 
)

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

Synopsis [Convert a BDD from a manager to another one.]

Description [Convert a BDD from a manager to another one. The orders of the variables in the two managers may be different. Returns a pointer to the BDD in the destination manager if successful; NULL otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 370 of file cuddBridge.c.

00374 {
00375     DdNode *res;
00376     do {
00377         ddDestination->reordered = 0;
00378         res = cuddBddTransfer(ddSource, ddDestination, f);
00379     } while (ddDestination->reordered == 1);
00380     return(res);
00381 
00382 } /* end of Cudd_bddTransfer */

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

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

Synopsis [Performs the recursive step for Cudd_addBddPattern.]

Description [Performs the recursive step for Cudd_addBddPattern. Returns a pointer to the resulting BDD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 454 of file cuddBridge.c.

00457 {
00458     DdNode *res, *T, *E;
00459     DdNode *fv, *fvn;
00460     int v;
00461 
00462     statLine(dd);
00463     /* Check terminal case. */
00464     if (cuddIsConstant(f)) {
00465         return(Cudd_NotCond(DD_ONE(dd),f == DD_ZERO(dd)));
00466     }
00467 
00468     /* Check cache. */
00469     res = cuddCacheLookup1(dd,Cudd_addBddPattern,f);
00470     if (res != NULL) return(res);
00471 
00472     /* Recursive step. */
00473     v = f->index;
00474     fv = cuddT(f); fvn = cuddE(f);
00475 
00476     T = cuddAddBddDoPattern(dd,fv);
00477     if (T == NULL) return(NULL);
00478     cuddRef(T);
00479 
00480     E = cuddAddBddDoPattern(dd,fvn);
00481     if (E == NULL) {
00482         Cudd_RecursiveDeref(dd, T);
00483         return(NULL);
00484     }
00485     cuddRef(E);
00486     if (Cudd_IsComplement(T)) {
00487         res = (T == E) ? Cudd_Not(T) : cuddUniqueInter(dd,v,Cudd_Not(T),Cudd_Not(E));
00488         if (res == NULL) {
00489             Cudd_RecursiveDeref(dd, T);
00490             Cudd_RecursiveDeref(dd, E);
00491             return(NULL);
00492         }
00493         res = Cudd_Not(res);
00494     } else {
00495         res = (T == E) ? T : cuddUniqueInter(dd,v,T,E);
00496         if (res == NULL) {
00497             Cudd_RecursiveDeref(dd, T);
00498             Cudd_RecursiveDeref(dd, E);
00499             return(NULL);
00500         }
00501     }
00502     cuddDeref(T);
00503     cuddDeref(E);
00504 
00505     /* Store result. */
00506     cuddCacheInsert1(dd,Cudd_addBddPattern,f,res);
00507 
00508     return(res);
00509 
00510 } /* end of cuddAddBddDoPattern */

DdNode* cuddBddTransfer ( DdManager *  ddS,
DdManager *  ddD,
DdNode *  f 
)

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

Synopsis [Convert a BDD from a manager to another one.]

Description [Convert a BDD from a manager to another one. Returns a pointer to the BDD in the destination manager if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_bddTransfer]

Definition at line 404 of file cuddBridge.c.

00408 {
00409     DdNode *res;
00410     st_table *table = NULL;
00411     st_generator *gen = NULL;
00412     DdNode *key, *value;
00413 
00414     table = st_init_table(st_ptrcmp,st_ptrhash);
00415     if (table == NULL) goto failure;
00416     res = cuddBddTransferRecur(ddS, ddD, f, table);
00417     if (res != NULL) cuddRef(res);
00418 
00419     /* Dereference all elements in the table and dispose of the table.
00420     ** This must be done also if res is NULL to avoid leaks in case of
00421     ** reordering. */
00422     gen = st_init_gen(table);
00423     if (gen == NULL) goto failure;
00424     while (st_gen(gen, (char **) &key, (char **) &value)) {
00425         Cudd_RecursiveDeref(ddD, value);
00426     }
00427     st_free_gen(gen); gen = NULL;
00428     st_free_table(table); table = NULL;
00429 
00430     if (res != NULL) cuddDeref(res);
00431     return(res);
00432 
00433 failure:
00434     if (table != NULL) st_free_table(table);
00435     if (gen != NULL) st_free_gen(gen);
00436     return(NULL);
00437 
00438 } /* end of cuddBddTransfer */

static DdNode* cuddBddTransferRecur ( DdManager *  ddS,
DdManager *  ddD,
DdNode *  f,
st_table *  table 
) [static]

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

Synopsis [Performs the recursive step of Cudd_bddTransfer.]

Description [Performs the recursive step of Cudd_bddTransfer. Returns a pointer to the result if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [cuddBddTransfer]

Definition at line 914 of file cuddBridge.c.

00919 {
00920     DdNode *ft, *fe, *t, *e, *var, *res;
00921     DdNode *one, *zero;
00922     int    index;
00923     int    comple = 0;
00924 
00925     statLine(ddD);
00926     one = DD_ONE(ddD);
00927     comple = Cudd_IsComplement(f);
00928 
00929     /* Trivial cases. */
00930     if (Cudd_IsConstant(f)) return(Cudd_NotCond(one, comple));
00931 
00932     /* Make canonical to increase the utilization of the cache. */
00933     f = Cudd_NotCond(f,comple);
00934     /* Now f is a regular pointer to a non-constant node. */
00935 
00936     /* Check the cache. */
00937     if(st_lookup(table, (char *)f, (char **) &res))
00938         return(Cudd_NotCond(res,comple));
00939     
00940     /* Recursive step. */
00941     index = f->index;
00942     ft = cuddT(f); fe = cuddE(f);
00943 
00944     t = cuddBddTransferRecur(ddS, ddD, ft, table);
00945     if (t == NULL) {
00946         return(NULL);
00947     }
00948     cuddRef(t);
00949 
00950     e = cuddBddTransferRecur(ddS, ddD, fe, table);
00951     if (e == NULL) {
00952         Cudd_RecursiveDeref(ddD, t);
00953         return(NULL);
00954     }
00955     cuddRef(e);
00956 
00957     zero = Cudd_Not(one);
00958     var = cuddUniqueInter(ddD,index,one,zero);
00959     if (var == NULL) {
00960         Cudd_RecursiveDeref(ddD, t);
00961         Cudd_RecursiveDeref(ddD, e);
00962         return(NULL);
00963     }
00964     res = cuddBddIteRecur(ddD,var,t,e);
00965     if (res == NULL) {
00966         Cudd_RecursiveDeref(ddD, t);
00967         Cudd_RecursiveDeref(ddD, e);
00968         return(NULL);
00969     }
00970     cuddRef(res);
00971     Cudd_RecursiveDeref(ddD, t);
00972     Cudd_RecursiveDeref(ddD, e);
00973 
00974     if (st_add_direct(table, (char *) f, (char *) res) == ST_OUT_OF_MEM) {
00975         Cudd_RecursiveDeref(ddD, res);
00976         return(NULL);
00977     }
00978     return(Cudd_NotCond(res,comple));
00979 
00980 } /* end of cuddBddTransferRecur */

static DdNode* ddBddToAddRecur ( DdManager *  dd,
DdNode *  B 
) [static]

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

Synopsis [Performs the recursive step for Cudd_BddToAdd.]

Description [Performs the recursive step for Cudd_BddToAdd. Returns a pointer to the resulting ADD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 827 of file cuddBridge.c.

00830 {
00831     DdNode *one;
00832     DdNode *res, *res1, *T, *E, *Bt, *Be;
00833     int complement = 0;
00834 
00835     statLine(dd);
00836     one = DD_ONE(dd);
00837 
00838     if (Cudd_IsConstant(B)) {
00839         if (B == one) {
00840             res = one;
00841         } else {
00842             res = DD_ZERO(dd);
00843         }
00844         return(res);
00845     }
00846     /* Check visited table */
00847     res = cuddCacheLookup1(dd,ddBddToAddRecur,B);
00848     if (res != NULL) return(res);
00849 
00850     if (Cudd_IsComplement(B)) {
00851         complement = 1;
00852         Bt = cuddT(Cudd_Regular(B));
00853         Be = cuddE(Cudd_Regular(B));
00854     } else {
00855         Bt = cuddT(B);
00856         Be = cuddE(B);
00857     }
00858 
00859     T = ddBddToAddRecur(dd, Bt);
00860     if (T == NULL) return(NULL);
00861     cuddRef(T);
00862 
00863     E = ddBddToAddRecur(dd, Be);
00864     if (E == NULL) {
00865         Cudd_RecursiveDeref(dd, T);
00866         return(NULL);
00867     }
00868     cuddRef(E);
00869 
00870     /* No need to check for T == E, because it is guaranteed not to happen. */
00871     res = cuddUniqueInter(dd, (int) Cudd_Regular(B)->index, T, E);
00872     if (res == NULL) {
00873         Cudd_RecursiveDeref(dd ,T);
00874         Cudd_RecursiveDeref(dd ,E);
00875         return(NULL);
00876     }
00877     cuddDeref(T);
00878     cuddDeref(E);
00879 
00880     if (complement) {
00881         cuddRef(res);
00882         res1 = cuddAddCmplRecur(dd, res);
00883         if (res1 == NULL) {
00884             Cudd_RecursiveDeref(dd, res);
00885             return(NULL);
00886         }
00887         cuddRef(res1);
00888         Cudd_RecursiveDeref(dd, res);
00889         res = res1;
00890         cuddDeref(res);
00891     }
00892 
00893     /* Store result. */
00894     cuddCacheInsert1(dd,ddBddToAddRecur,B,res);
00895 
00896     return(res);
00897 
00898 } /* end of ddBddToAddRecur */

Variable Documentation

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

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

FileName [cuddBridge.c]

PackageName [cudd]

Synopsis [Translation from BDD to ADD and vice versa and transfer between different managers.]

Description [External procedures included in this file:

Internal procedures included in this file:

Static procedures included in this file:

]

SeeAlso []

Author [Fabio Somenzi]

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 70 of file cuddBridge.c.

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