src/cuBdd/cuddZddSetop.c File Reference

#include "util.h"
#include "cuddInt.h"
Include dependency graph for cuddZddSetop.c:

Go to the source code of this file.

Functions

static DdNode * zdd_subset1_aux (DdManager *zdd, DdNode *P, DdNode *zvar)
static DdNode * zdd_subset0_aux (DdManager *zdd, DdNode *P, DdNode *zvar)
static void zddVarToConst (DdNode *f, DdNode **gp, DdNode **hp, DdNode *base, DdNode *empty)
DdNode * Cudd_zddIte (DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
DdNode * Cudd_zddUnion (DdManager *dd, DdNode *P, DdNode *Q)
DdNode * Cudd_zddIntersect (DdManager *dd, DdNode *P, DdNode *Q)
DdNode * Cudd_zddDiff (DdManager *dd, DdNode *P, DdNode *Q)
DdNode * Cudd_zddDiffConst (DdManager *zdd, DdNode *P, DdNode *Q)
DdNode * Cudd_zddSubset1 (DdManager *dd, DdNode *P, int var)
DdNode * Cudd_zddSubset0 (DdManager *dd, DdNode *P, int var)
DdNode * Cudd_zddChange (DdManager *dd, DdNode *P, int var)
DdNode * cuddZddIte (DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
DdNode * cuddZddUnion (DdManager *zdd, DdNode *P, DdNode *Q)
DdNode * cuddZddIntersect (DdManager *zdd, DdNode *P, DdNode *Q)
DdNode * cuddZddDiff (DdManager *zdd, DdNode *P, DdNode *Q)
DdNode * cuddZddChangeAux (DdManager *zdd, DdNode *P, DdNode *zvar)
DdNode * cuddZddSubset1 (DdManager *dd, DdNode *P, int var)
DdNode * cuddZddSubset0 (DdManager *dd, DdNode *P, int var)
DdNode * cuddZddChange (DdManager *dd, DdNode *P, int var)

Variables

static char rcsid[] DD_UNUSED = "$Id: cuddZddSetop.c,v 1.25 2004/08/13 18:04:54 fabio Exp $"

Function Documentation

DdNode* Cudd_zddChange ( DdManager *  dd,
DdNode *  P,
int  var 
)

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

Synopsis [Substitutes a variable with its complement in a ZDD.]

Description [Substitutes a variable with its complement in a ZDD. returns a pointer to the result if successful; NULL otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 388 of file cuddZddSetop.c.

00392 {
00393     DdNode      *res;
00394 
00395     if ((unsigned int) var >= CUDD_MAXINDEX - 1) return(NULL);
00396     
00397     do {
00398         dd->reordered = 0;
00399         res = cuddZddChange(dd, P, var);
00400     } while (dd->reordered == 1);
00401     return(res);
00402 
00403 } /* end of Cudd_zddChange */

DdNode* Cudd_zddDiff ( DdManager *  dd,
DdNode *  P,
DdNode *  Q 
)

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

Synopsis [Computes the difference of two ZDDs.]

Description [Computes the difference of two ZDDs. Returns a pointer to the result if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_zddDiffConst]

Definition at line 232 of file cuddZddSetop.c.

00236 {
00237     DdNode *res;
00238 
00239     do {
00240         dd->reordered = 0;
00241         res = cuddZddDiff(dd, P, Q);
00242     } while (dd->reordered == 1);
00243     return(res);
00244 
00245 } /* end of Cudd_zddDiff */

DdNode* Cudd_zddDiffConst ( DdManager *  zdd,
DdNode *  P,
DdNode *  Q 
)

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

Synopsis [Performs the inclusion test for ZDDs (P implies Q).]

Description [Inclusion test for ZDDs (P implies Q). No new nodes are generated by this procedure. Returns empty if true; a valid pointer different from empty or DD_NON_CONSTANT otherwise.]

SideEffects [None]

SeeAlso [Cudd_zddDiff]

Definition at line 262 of file cuddZddSetop.c.

00266 {
00267     int         p_top, q_top;
00268     DdNode      *empty = DD_ZERO(zdd), *t, *res;
00269     DdManager   *table = zdd;
00270 
00271     statLine(zdd);
00272     if (P == empty)
00273         return(empty);
00274     if (Q == empty)
00275         return(P);
00276     if (P == Q)
00277         return(empty);
00278 
00279     /* Check cache.  The cache is shared by cuddZddDiff(). */
00280     res = cuddCacheLookup2Zdd(table, cuddZddDiff, P, Q);
00281     if (res != NULL)
00282         return(res);
00283 
00284     if (cuddIsConstant(P))
00285         p_top = P->index;
00286     else
00287         p_top = zdd->permZ[P->index];
00288     if (cuddIsConstant(Q))
00289         q_top = Q->index;
00290     else
00291         q_top = zdd->permZ[Q->index];
00292     if (p_top < q_top) {
00293         res = DD_NON_CONSTANT;
00294     } else if (p_top > q_top) {
00295         res = Cudd_zddDiffConst(zdd, P, cuddE(Q));
00296     } else {
00297         t = Cudd_zddDiffConst(zdd, cuddT(P), cuddT(Q));
00298         if (t != empty)
00299             res = DD_NON_CONSTANT;
00300         else
00301             res = Cudd_zddDiffConst(zdd, cuddE(P), cuddE(Q));
00302     }
00303 
00304     cuddCacheInsert2(table, cuddZddDiff, P, Q, res);
00305 
00306     return(res);
00307 
00308 } /* end of Cudd_zddDiffConst */

DdNode* Cudd_zddIntersect ( DdManager *  dd,
DdNode *  P,
DdNode *  Q 
)

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

Synopsis [Computes the intersection of two ZDDs.]

Description [Computes the intersection of two ZDDs. Returns a pointer to the result if successful; NULL otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 203 of file cuddZddSetop.c.

00207 {
00208     DdNode *res;
00209 
00210     do {
00211         dd->reordered = 0;
00212         res = cuddZddIntersect(dd, P, Q);
00213     } while (dd->reordered == 1);
00214     return(res);
00215 
00216 } /* end of Cudd_zddIntersect */

DdNode* Cudd_zddIte ( DdManager *  dd,
DdNode *  f,
DdNode *  g,
DdNode *  h 
)

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

Synopsis [Computes the ITE of three ZDDs.]

Description [Computes the ITE of three ZDDs. Returns a pointer to the result if successful; NULL otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 144 of file cuddZddSetop.c.

00149 {
00150     DdNode *res;
00151 
00152     do {
00153         dd->reordered = 0;
00154         res = cuddZddIte(dd, f, g, h);
00155     } while (dd->reordered == 1);
00156     return(res);
00157 
00158 } /* end of Cudd_zddIte */

DdNode* Cudd_zddSubset0 ( DdManager *  dd,
DdNode *  P,
int  var 
)

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

Synopsis [Computes the negative cofactor of a ZDD w.r.t. a variable.]

Description [Computes the negative cofactor of a ZDD w.r.t. a variable. In terms of combinations, the result is the set of all combinations in which the variable is negated. Returns a pointer to the result if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_zddSubset1]

Definition at line 358 of file cuddZddSetop.c.

00362 {
00363     DdNode      *r;
00364 
00365     do {
00366         dd->reordered = 0;
00367         r = cuddZddSubset0(dd, P, var);
00368     } while (dd->reordered == 1);
00369 
00370     return(r);
00371 
00372 } /* end of Cudd_zddSubset0 */

DdNode* Cudd_zddSubset1 ( DdManager *  dd,
DdNode *  P,
int  var 
)

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

Synopsis [Computes the positive cofactor of a ZDD w.r.t. a variable.]

Description [Computes the positive cofactor of a ZDD w.r.t. a variable. In terms of combinations, the result is the set of all combinations in which the variable is asserted. Returns a pointer to the result if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_zddSubset0]

Definition at line 326 of file cuddZddSetop.c.

00330 {
00331     DdNode      *r;
00332 
00333     do {
00334         dd->reordered = 0;
00335         r = cuddZddSubset1(dd, P, var);
00336     } while (dd->reordered == 1);
00337 
00338     return(r);
00339 
00340 } /* end of Cudd_zddSubset1 */

DdNode* Cudd_zddUnion ( DdManager *  dd,
DdNode *  P,
DdNode *  Q 
)

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

Synopsis [Computes the union of two ZDDs.]

Description [Computes the union of two ZDDs. Returns a pointer to the result if successful; NULL otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 174 of file cuddZddSetop.c.

00178 {
00179     DdNode *res;
00180 
00181     do {
00182         dd->reordered = 0;
00183         res = cuddZddUnion(dd, P, Q);
00184     } while (dd->reordered == 1);
00185     return(res);
00186 
00187 } /* end of Cudd_zddUnion */

DdNode* cuddZddChange ( DdManager *  dd,
DdNode *  P,
int  var 
)

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

Synopsis [Substitutes a variable with its complement in a ZDD.]

Description [Substitutes a variable with its complement in a ZDD. returns a pointer to the result if successful; NULL otherwise. cuddZddChange performs the same function as Cudd_zddChange, but does not restart if reordering has taken place. Therefore it can be called from within a recursive procedure.]

SideEffects [None]

SeeAlso [Cudd_zddChange]

Definition at line 967 of file cuddZddSetop.c.

00971 {
00972     DdNode      *zvar, *res;
00973 
00974     zvar = cuddUniqueInterZdd(dd, var, DD_ONE(dd), DD_ZERO(dd));
00975     if (zvar == NULL) return(NULL);
00976     cuddRef(zvar);
00977 
00978     res = cuddZddChangeAux(dd, P, zvar);
00979     if (res == NULL) {
00980         Cudd_RecursiveDerefZdd(dd,zvar);
00981         return(NULL);
00982     }
00983     cuddRef(res);
00984     Cudd_RecursiveDerefZdd(dd,zvar);
00985     cuddDeref(res);
00986     return(res);
00987 
00988 } /* end of cuddZddChange */

DdNode* cuddZddChangeAux ( DdManager *  zdd,
DdNode *  P,
DdNode *  zvar 
)

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

Synopsis [Performs the recursive step of Cudd_zddChange.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 795 of file cuddZddSetop.c.

00799 {
00800     int         top_var, level;
00801     DdNode      *res, *t, *e;
00802     DdNode      *base = DD_ONE(zdd);
00803     DdNode      *empty = DD_ZERO(zdd);
00804 
00805     statLine(zdd);
00806     if (P == empty)
00807         return(empty);
00808     if (P == base)
00809         return(zvar);
00810 
00811     /* Check cache. */
00812     res = cuddCacheLookup2Zdd(zdd, cuddZddChangeAux, P, zvar);
00813     if (res != NULL)
00814         return(res);
00815 
00816     top_var = zdd->permZ[P->index];
00817     level = zdd->permZ[zvar->index];
00818 
00819     if (top_var > level) {
00820         res = cuddZddGetNode(zdd, zvar->index, P, DD_ZERO(zdd));
00821         if (res == NULL) return(NULL);
00822     } else if (top_var == level) {
00823         res = cuddZddGetNode(zdd, zvar->index, cuddE(P), cuddT(P));
00824         if (res == NULL) return(NULL);
00825     } else {
00826         t = cuddZddChangeAux(zdd, cuddT(P), zvar);
00827         if (t == NULL) return(NULL);
00828         cuddRef(t);
00829         e = cuddZddChangeAux(zdd, cuddE(P), zvar);
00830         if (e == NULL) {
00831             Cudd_RecursiveDerefZdd(zdd, t);
00832             return(NULL);
00833         }
00834         cuddRef(e);
00835         res = cuddZddGetNode(zdd, P->index, t, e);
00836         if (res == NULL) {
00837             Cudd_RecursiveDerefZdd(zdd, t);
00838             Cudd_RecursiveDerefZdd(zdd, e);
00839             return(NULL);
00840         }
00841         cuddDeref(t);
00842         cuddDeref(e);
00843     }
00844 
00845     cuddCacheInsert2(zdd, cuddZddChangeAux, P, zvar, res);
00846 
00847     return(res);
00848 
00849 } /* end of cuddZddChangeAux */

DdNode* cuddZddDiff ( DdManager *  zdd,
DdNode *  P,
DdNode *  Q 
)

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

Synopsis [Performs the recursive step of Cudd_zddDiff.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 713 of file cuddZddSetop.c.

00717 {
00718     int         p_top, q_top;
00719     DdNode      *empty = DD_ZERO(zdd), *t, *e, *res;
00720     DdManager   *table = zdd;
00721 
00722     statLine(zdd);
00723     if (P == empty)
00724         return(empty);
00725     if (Q == empty)
00726         return(P);
00727     if (P == Q)
00728         return(empty);
00729 
00730     /* Check cache.  The cache is shared by Cudd_zddDiffConst(). */
00731     res = cuddCacheLookup2Zdd(table, cuddZddDiff, P, Q);
00732     if (res != NULL && res != DD_NON_CONSTANT)
00733         return(res);
00734 
00735     if (cuddIsConstant(P))
00736         p_top = P->index;
00737     else
00738         p_top = zdd->permZ[P->index];
00739     if (cuddIsConstant(Q))
00740         q_top = Q->index;
00741     else
00742         q_top = zdd->permZ[Q->index];
00743     if (p_top < q_top) {
00744         e = cuddZddDiff(zdd, cuddE(P), Q);
00745         if (e == NULL) return(NULL);
00746         cuddRef(e);
00747         res = cuddZddGetNode(zdd, P->index, cuddT(P), e);
00748         if (res == NULL) {
00749             Cudd_RecursiveDerefZdd(table, e);
00750             return(NULL);
00751         }
00752         cuddDeref(e);
00753     } else if (p_top > q_top) {
00754         res = cuddZddDiff(zdd, P, cuddE(Q));
00755         if (res == NULL) return(NULL);
00756     } else {
00757         t = cuddZddDiff(zdd, cuddT(P), cuddT(Q));
00758         if (t == NULL) return(NULL);
00759         cuddRef(t);
00760         e = cuddZddDiff(zdd, cuddE(P), cuddE(Q));
00761         if (e == NULL) {
00762             Cudd_RecursiveDerefZdd(table, t);
00763             return(NULL);
00764         }
00765         cuddRef(e);
00766         res = cuddZddGetNode(zdd, P->index, t, e);
00767         if (res == NULL) {
00768             Cudd_RecursiveDerefZdd(table, t);
00769             Cudd_RecursiveDerefZdd(table, e);
00770             return(NULL);
00771         }
00772         cuddDeref(t);
00773         cuddDeref(e);
00774     }
00775 
00776     cuddCacheInsert2(table, cuddZddDiff, P, Q, res);
00777 
00778     return(res);
00779 
00780 } /* end of cuddZddDiff */

DdNode* cuddZddIntersect ( DdManager *  zdd,
DdNode *  P,
DdNode *  Q 
)

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

Synopsis [Performs the recursive step of Cudd_zddIntersect.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 638 of file cuddZddSetop.c.

00642 {
00643     int         p_top, q_top;
00644     DdNode      *empty = DD_ZERO(zdd), *t, *e, *res;
00645     DdManager   *table = zdd;
00646 
00647     statLine(zdd);
00648     if (P == empty)
00649         return(empty);
00650     if (Q == empty)
00651         return(empty);
00652     if (P == Q)
00653         return(P);
00654 
00655     /* Check cache. */
00656     res = cuddCacheLookup2Zdd(table, cuddZddIntersect, P, Q);
00657     if (res != NULL)
00658         return(res);
00659 
00660     if (cuddIsConstant(P))
00661         p_top = P->index;
00662     else
00663         p_top = zdd->permZ[P->index];
00664     if (cuddIsConstant(Q))
00665         q_top = Q->index;
00666     else
00667         q_top = zdd->permZ[Q->index];
00668     if (p_top < q_top) {
00669         res = cuddZddIntersect(zdd, cuddE(P), Q);
00670         if (res == NULL) return(NULL);
00671     } else if (p_top > q_top) {
00672         res = cuddZddIntersect(zdd, P, cuddE(Q));
00673         if (res == NULL) return(NULL);
00674     } else {
00675         t = cuddZddIntersect(zdd, cuddT(P), cuddT(Q));
00676         if (t == NULL) return(NULL);
00677         cuddRef(t);
00678         e = cuddZddIntersect(zdd, cuddE(P), cuddE(Q));
00679         if (e == NULL) {
00680             Cudd_RecursiveDerefZdd(table, t);
00681             return(NULL);
00682         }
00683         cuddRef(e);
00684         res = cuddZddGetNode(zdd, P->index, t, e);
00685         if (res == NULL) {
00686             Cudd_RecursiveDerefZdd(table, t);
00687             Cudd_RecursiveDerefZdd(table, e);
00688             return(NULL);
00689         }
00690         cuddDeref(t);
00691         cuddDeref(e);
00692     }
00693 
00694     cuddCacheInsert2(table, cuddZddIntersect, P, Q, res);
00695 
00696     return(res);
00697 
00698 } /* end of cuddZddIntersect */

DdNode* cuddZddIte ( DdManager *  dd,
DdNode *  f,
DdNode *  g,
DdNode *  h 
)

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

Synopsis [Performs the recursive step of Cudd_zddIte.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 423 of file cuddZddSetop.c.

00428 {
00429     DdNode *tautology, *empty;
00430     DdNode *r,*Gv,*Gvn,*Hv,*Hvn,*t,*e;
00431     unsigned int topf,topg,toph,v,top;
00432     int index;
00433 
00434     statLine(dd);
00435     /* Trivial cases. */
00436     /* One variable cases. */
00437     if (f == (empty = DD_ZERO(dd))) {   /* ITE(0,G,H) = H */
00438         return(h);
00439     }
00440     topf = cuddIZ(dd,f->index);
00441     topg = cuddIZ(dd,g->index);
00442     toph = cuddIZ(dd,h->index);
00443     v = ddMin(topg,toph);
00444     top  = ddMin(topf,v);
00445 
00446     tautology = (top == CUDD_MAXINDEX) ? DD_ONE(dd) : dd->univ[top];
00447     if (f == tautology) {                       /* ITE(1,G,H) = G */
00448         return(g);
00449     }
00450 
00451     /* From now on, f is known to not be a constant. */
00452     zddVarToConst(f,&g,&h,tautology,empty);
00453 
00454     /* Check remaining one variable cases. */
00455     if (g == h) {                       /* ITE(F,G,G) = G */
00456         return(g);
00457     }
00458 
00459     if (g == tautology) {                       /* ITE(F,1,0) = F */
00460         if (h == empty) return(f);
00461     }
00462 
00463     /* Check cache. */
00464     r = cuddCacheLookupZdd(dd,DD_ZDD_ITE_TAG,f,g,h);
00465     if (r != NULL) {
00466         return(r);
00467     }
00468 
00469     /* Recompute these because they may have changed in zddVarToConst. */
00470     topg = cuddIZ(dd,g->index);
00471     toph = cuddIZ(dd,h->index);
00472     v = ddMin(topg,toph);
00473 
00474     if (topf < v) {
00475         r = cuddZddIte(dd,cuddE(f),g,h);
00476         if (r == NULL) return(NULL);
00477     } else if (topf > v) {
00478         if (topg > v) {
00479             Gvn = g;
00480             index = h->index;
00481         } else {
00482             Gvn = cuddE(g);
00483             index = g->index;
00484         }
00485         if (toph > v) {
00486             Hv = empty; Hvn = h;
00487         } else {
00488             Hv = cuddT(h); Hvn = cuddE(h);
00489         }
00490         e = cuddZddIte(dd,f,Gvn,Hvn);
00491         if (e == NULL) return(NULL);
00492         cuddRef(e);
00493         r = cuddZddGetNode(dd,index,Hv,e);
00494         if (r == NULL) {
00495             Cudd_RecursiveDerefZdd(dd,e);
00496             return(NULL);
00497         }
00498         cuddDeref(e);
00499     } else {
00500         index = f->index;
00501         if (topg > v) {
00502             Gv = empty; Gvn = g;
00503         } else {
00504             Gv = cuddT(g); Gvn = cuddE(g);
00505         }
00506         if (toph > v) {
00507             Hv = empty; Hvn = h;
00508         } else {
00509             Hv = cuddT(h); Hvn = cuddE(h);
00510         }
00511         e = cuddZddIte(dd,cuddE(f),Gvn,Hvn);
00512         if (e == NULL) return(NULL);
00513         cuddRef(e);
00514         t = cuddZddIte(dd,cuddT(f),Gv,Hv);
00515         if (t == NULL) {
00516             Cudd_RecursiveDerefZdd(dd,e);
00517             return(NULL);
00518         }
00519         cuddRef(t);
00520         r = cuddZddGetNode(dd,index,t,e);
00521         if (r == NULL) {
00522             Cudd_RecursiveDerefZdd(dd,e);
00523             Cudd_RecursiveDerefZdd(dd,t);
00524             return(NULL);
00525         }
00526         cuddDeref(t);
00527         cuddDeref(e);
00528     }
00529 
00530     cuddCacheInsert(dd,DD_ZDD_ITE_TAG,f,g,h,r);
00531 
00532     return(r);
00533 
00534 } /* end of cuddZddIte */

DdNode* cuddZddSubset0 ( DdManager *  dd,
DdNode *  P,
int  var 
)

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

Synopsis [Computes the negative cofactor of a ZDD w.r.t. a variable.]

Description [Computes the negative cofactor of a ZDD w.r.t. a variable. In terms of combinations, the result is the set of all combinations in which the variable is negated. Returns a pointer to the result if successful; NULL otherwise. cuddZddSubset0 performs the same function as Cudd_zddSubset0, but does not restart if reordering has taken place. Therefore it can be called from within a recursive procedure.]

SideEffects [None]

SeeAlso [cuddZddSubset1 Cudd_zddSubset0]

Definition at line 919 of file cuddZddSetop.c.

00923 {
00924     DdNode      *zvar, *r;
00925     DdNode      *base, *empty;
00926 
00927     base = DD_ONE(dd);
00928     empty = DD_ZERO(dd);
00929 
00930     zvar = cuddUniqueInterZdd(dd, var, base, empty);
00931     if (zvar == NULL) {
00932         return(NULL);
00933     } else {
00934         cuddRef(zvar);
00935         r = zdd_subset0_aux(dd, P, zvar);
00936         if (r == NULL) {
00937             Cudd_RecursiveDerefZdd(dd, zvar);
00938             return(NULL);
00939         }
00940         cuddRef(r);
00941         Cudd_RecursiveDerefZdd(dd, zvar);
00942     }
00943 
00944     cuddDeref(r);
00945     return(r);
00946 
00947 } /* end of cuddZddSubset0 */

DdNode* cuddZddSubset1 ( DdManager *  dd,
DdNode *  P,
int  var 
)

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

Synopsis [Computes the positive cofactor of a ZDD w.r.t. a variable.]

Description [Computes the positive cofactor of a ZDD w.r.t. a variable. In terms of combinations, the result is the set of all combinations in which the variable is asserted. Returns a pointer to the result if successful; NULL otherwise. cuddZddSubset1 performs the same function as Cudd_zddSubset1, but does not restart if reordering has taken place. Therefore it can be called from within a recursive procedure.]

SideEffects [None]

SeeAlso [cuddZddSubset0 Cudd_zddSubset1]

Definition at line 870 of file cuddZddSetop.c.

00874 {
00875     DdNode      *zvar, *r;
00876     DdNode      *base, *empty;
00877 
00878     base = DD_ONE(dd);
00879     empty = DD_ZERO(dd);
00880 
00881     zvar = cuddUniqueInterZdd(dd, var, base, empty);
00882     if (zvar == NULL) {
00883         return(NULL);
00884     } else {
00885         cuddRef(zvar);
00886         r = zdd_subset1_aux(dd, P, zvar);
00887         if (r == NULL) {
00888             Cudd_RecursiveDerefZdd(dd, zvar);
00889             return(NULL);
00890         }
00891         cuddRef(r);
00892         Cudd_RecursiveDerefZdd(dd, zvar);
00893     }
00894 
00895     cuddDeref(r);
00896     return(r);
00897 
00898 } /* end of cuddZddSubset1 */

DdNode* cuddZddUnion ( DdManager *  zdd,
DdNode *  P,
DdNode *  Q 
)

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

Synopsis [Performs the recursive step of Cudd_zddUnion.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 549 of file cuddZddSetop.c.

00553 {
00554     int         p_top, q_top;
00555     DdNode      *empty = DD_ZERO(zdd), *t, *e, *res;
00556     DdManager   *table = zdd;
00557 
00558     statLine(zdd);
00559     if (P == empty)
00560         return(Q);
00561     if (Q == empty)
00562         return(P);
00563     if (P == Q)
00564         return(P);
00565 
00566     /* Check cache */
00567     res = cuddCacheLookup2Zdd(table, cuddZddUnion, P, Q);
00568     if (res != NULL)
00569         return(res);
00570 
00571     if (cuddIsConstant(P))
00572         p_top = P->index;
00573     else
00574         p_top = zdd->permZ[P->index];
00575     if (cuddIsConstant(Q))
00576         q_top = Q->index;
00577     else
00578         q_top = zdd->permZ[Q->index];
00579     if (p_top < q_top) {
00580         e = cuddZddUnion(zdd, cuddE(P), Q);
00581         if (e == NULL) return (NULL);
00582         cuddRef(e);
00583         res = cuddZddGetNode(zdd, P->index, cuddT(P), e);
00584         if (res == NULL) {
00585             Cudd_RecursiveDerefZdd(table, e);
00586             return(NULL);
00587         }
00588         cuddDeref(e);
00589     } else if (p_top > q_top) {
00590         e = cuddZddUnion(zdd, P, cuddE(Q));
00591         if (e == NULL) return(NULL);
00592         cuddRef(e);
00593         res = cuddZddGetNode(zdd, Q->index, cuddT(Q), e);
00594         if (res == NULL) {
00595             Cudd_RecursiveDerefZdd(table, e);
00596             return(NULL);
00597         }
00598         cuddDeref(e);
00599     } else {
00600         t = cuddZddUnion(zdd, cuddT(P), cuddT(Q));
00601         if (t == NULL) return(NULL);
00602         cuddRef(t);
00603         e = cuddZddUnion(zdd, cuddE(P), cuddE(Q));
00604         if (e == NULL) {
00605             Cudd_RecursiveDerefZdd(table, t);
00606             return(NULL);
00607         }
00608         cuddRef(e);
00609         res = cuddZddGetNode(zdd, P->index, t, e);
00610         if (res == NULL) {
00611             Cudd_RecursiveDerefZdd(table, t);
00612             Cudd_RecursiveDerefZdd(table, e);
00613             return(NULL);
00614         }
00615         cuddDeref(t);
00616         cuddDeref(e);
00617     }
00618 
00619     cuddCacheInsert2(table, cuddZddUnion, P, Q, res);
00620 
00621     return(res);
00622 
00623 } /* end of cuddZddUnion */

static DdNode * zdd_subset0_aux ( DdManager *  zdd,
DdNode *  P,
DdNode *  zvar 
) [static]

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

Synopsis [Performs the recursive step of Cudd_zddSubset0.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 1077 of file cuddZddSetop.c.

01081 {
01082     int         top_var, level;
01083     DdNode      *res, *t, *e;
01084 
01085     statLine(zdd);
01086 
01087     /* Check cache. */
01088     res = cuddCacheLookup2Zdd(zdd, zdd_subset0_aux, P, zvar);
01089     if (res != NULL)
01090         return(res);
01091 
01092     if (cuddIsConstant(P)) {
01093         res = P;
01094         cuddCacheInsert2(zdd, zdd_subset0_aux, P, zvar, res);
01095         return(res);
01096     }
01097 
01098     top_var = zdd->permZ[P->index];
01099     level = zdd->permZ[zvar->index];
01100 
01101     if (top_var > level) {
01102         res = P;
01103     }
01104     else if (top_var == level) {
01105         res = cuddE(P);
01106     }
01107     else {
01108         t = zdd_subset0_aux(zdd, cuddT(P), zvar);
01109         if (t == NULL) return(NULL);
01110         cuddRef(t);
01111         e = zdd_subset0_aux(zdd, cuddE(P), zvar);
01112         if (e == NULL) {
01113             Cudd_RecursiveDerefZdd(zdd, t);
01114             return(NULL);
01115         }
01116         cuddRef(e);
01117         res = cuddZddGetNode(zdd, P->index, t, e);
01118         if (res == NULL) {
01119             Cudd_RecursiveDerefZdd(zdd, t);
01120             Cudd_RecursiveDerefZdd(zdd, e);
01121             return(NULL);
01122         }
01123         cuddDeref(t);
01124         cuddDeref(e);
01125     }
01126 
01127     cuddCacheInsert2(zdd, zdd_subset0_aux, P, zvar, res);
01128 
01129     return(res);
01130 
01131 } /* end of zdd_subset0_aux */

static DdNode * zdd_subset1_aux ( DdManager *  zdd,
DdNode *  P,
DdNode *  zvar 
) [static]

AutomaticStart

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

Synopsis [Performs the recursive step of Cudd_zddSubset1.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 1008 of file cuddZddSetop.c.

01012 {
01013     int         top_var, level;
01014     DdNode      *res, *t, *e;
01015     DdNode      *empty;
01016 
01017     statLine(zdd);
01018     empty = DD_ZERO(zdd);
01019 
01020     /* Check cache. */
01021     res = cuddCacheLookup2Zdd(zdd, zdd_subset1_aux, P, zvar);
01022     if (res != NULL)
01023         return(res);
01024 
01025     if (cuddIsConstant(P)) {
01026         res = empty;
01027         cuddCacheInsert2(zdd, zdd_subset1_aux, P, zvar, res);
01028         return(res);
01029     }
01030 
01031     top_var = zdd->permZ[P->index];
01032     level = zdd->permZ[zvar->index];
01033 
01034     if (top_var > level) {
01035         res = empty;
01036     } else if (top_var == level) {
01037         res = cuddT(P);
01038     } else {
01039         t = zdd_subset1_aux(zdd, cuddT(P), zvar);
01040         if (t == NULL) return(NULL);
01041         cuddRef(t);
01042         e = zdd_subset1_aux(zdd, cuddE(P), zvar);
01043         if (e == NULL) {
01044             Cudd_RecursiveDerefZdd(zdd, t);
01045             return(NULL);
01046         }
01047         cuddRef(e);
01048         res = cuddZddGetNode(zdd, P->index, t, e);
01049         if (res == NULL) {
01050             Cudd_RecursiveDerefZdd(zdd, t);
01051             Cudd_RecursiveDerefZdd(zdd, e);
01052             return(NULL);
01053         }
01054         cuddDeref(t);
01055         cuddDeref(e);
01056     }
01057 
01058     cuddCacheInsert2(zdd, zdd_subset1_aux, P, zvar, res);
01059 
01060     return(res);
01061 
01062 } /* end of zdd_subset1_aux */

static void zddVarToConst ( DdNode *  f,
DdNode **  gp,
DdNode **  hp,
DdNode *  base,
DdNode *  empty 
) [static]

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

Synopsis [Replaces variables with constants if possible (part of canonical form).]

Description []

SideEffects [None]

SeeAlso []

Definition at line 1147 of file cuddZddSetop.c.

01153 {
01154     DdNode *g = *gp;
01155     DdNode *h = *hp;
01156 
01157     if (f == g) { /* ITE(F,F,H) = ITE(F,1,H) = F + H */
01158         *gp = base;
01159     }
01160 
01161     if (f == h) { /* ITE(F,G,F) = ITE(F,G,0) = F * G */
01162         *hp = empty;
01163     }
01164 
01165 } /* end of zddVarToConst */

Variable Documentation

char rcsid [] DD_UNUSED = "$Id: cuddZddSetop.c,v 1.25 2004/08/13 18:04:54 fabio Exp $" [static]

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

FileName [cuddZddSetop.c]

PackageName [cudd]

Synopsis [Set operations on ZDDs.]

Description [External procedures included in this module:

Internal procedures included in this module:

Static procedures included in this module:

]

SeeAlso []

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

Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado

All rights reserved.

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.

Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.

Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]

Definition at line 99 of file cuddZddSetop.c.

Generated on Tue Jan 12 13:57:22 2010 for glu-2.2 by  doxygen 1.6.1