src/bdd/cudd/cuddZddSetop.c File Reference

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

Go to the source code of this file.

Functions

static DdNode *zdd_subset1_aux ARGS ((DdManager *zdd, DdNode *P, DdNode *zvar))
static void zddVarToConst ARGS ((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)
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)

Variables

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

Function Documentation

static void zddVarToConst ARGS ( (DdNode *f, DdNode **gp, DdNode **hp, DdNode *base, DdNode *empty)   )  [static]
static DdNode* zdd_subset1_aux ARGS ( (DdManager *zdd, DdNode *P, DdNode *zvar)   )  [static]

AutomaticStart

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 355 of file cuddZddSetop.c.

00359 {
00360     DdNode      *res;
00361 
00362     if ((unsigned int) var >= CUDD_MAXINDEX - 1) return(NULL);
00363     
00364     do {
00365         dd->reordered = 0;
00366         res = cuddZddChange(dd, P, var);
00367     } while (dd->reordered == 1);
00368     return(res);
00369 
00370 } /* 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 199 of file cuddZddSetop.c.

00203 {
00204     DdNode *res;
00205 
00206     do {
00207         dd->reordered = 0;
00208         res = cuddZddDiff(dd, P, Q);
00209     } while (dd->reordered == 1);
00210     return(res);
00211 
00212 } /* 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 229 of file cuddZddSetop.c.

00233 {
00234     int         p_top, q_top;
00235     DdNode      *empty = DD_ZERO(zdd), *t, *res;
00236     DdManager   *table = zdd;
00237 
00238     statLine(zdd);
00239     if (P == empty)
00240         return(empty);
00241     if (Q == empty)
00242         return(P);
00243     if (P == Q)
00244         return(empty);
00245 
00246     /* Check cache.  The cache is shared by cuddZddDiff(). */
00247     res = cuddCacheLookup2Zdd(table, cuddZddDiff, P, Q);
00248     if (res != NULL)
00249         return(res);
00250 
00251     if (cuddIsConstant(P))
00252         p_top = P->index;
00253     else
00254         p_top = zdd->permZ[P->index];
00255     if (cuddIsConstant(Q))
00256         q_top = Q->index;
00257     else
00258         q_top = zdd->permZ[Q->index];
00259     if (p_top < q_top) {
00260         res = DD_NON_CONSTANT;
00261     } else if (p_top > q_top) {
00262         res = Cudd_zddDiffConst(zdd, P, cuddE(Q));
00263     } else {
00264         t = Cudd_zddDiffConst(zdd, cuddT(P), cuddT(Q));
00265         if (t != empty)
00266             res = DD_NON_CONSTANT;
00267         else
00268             res = Cudd_zddDiffConst(zdd, cuddE(P), cuddE(Q));
00269     }
00270 
00271     cuddCacheInsert2(table, cuddZddDiff, P, Q, res);
00272 
00273     return(res);
00274 
00275 } /* 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 170 of file cuddZddSetop.c.

00174 {
00175     DdNode *res;
00176 
00177     do {
00178         dd->reordered = 0;
00179         res = cuddZddIntersect(dd, P, Q);
00180     } while (dd->reordered == 1);
00181     return(res);
00182 
00183 } /* 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 111 of file cuddZddSetop.c.

00116 {
00117     DdNode *res;
00118 
00119     do {
00120         dd->reordered = 0;
00121         res = cuddZddIte(dd, f, g, h);
00122     } while (dd->reordered == 1);
00123     return(res);
00124 
00125 } /* 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 325 of file cuddZddSetop.c.

00329 {
00330     DdNode      *r;
00331 
00332     do {
00333         dd->reordered = 0;
00334         r = cuddZddSubset0(dd, P, var);
00335     } while (dd->reordered == 1);
00336 
00337     return(r);
00338 
00339 } /* 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 293 of file cuddZddSetop.c.

00297 {
00298     DdNode      *r;
00299 
00300     do {
00301         dd->reordered = 0;
00302         r = cuddZddSubset1(dd, P, var);
00303     } while (dd->reordered == 1);
00304 
00305     return(r);
00306 
00307 } /* 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 141 of file cuddZddSetop.c.

00145 {
00146     DdNode *res;
00147 
00148     do {
00149         dd->reordered = 0;
00150         res = cuddZddUnion(dd, P, Q);
00151     } while (dd->reordered == 1);
00152     return(res);
00153 
00154 } /* 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 934 of file cuddZddSetop.c.

00938 {
00939     DdNode      *zvar, *res;
00940 
00941     zvar = cuddUniqueInterZdd(dd, var, DD_ONE(dd), DD_ZERO(dd));
00942     if (zvar == NULL) return(NULL);
00943     cuddRef(zvar);
00944 
00945     res = cuddZddChangeAux(dd, P, zvar);
00946     if (res == NULL) {
00947         Cudd_RecursiveDerefZdd(dd,zvar);
00948         return(NULL);
00949     }
00950     cuddRef(res);
00951     Cudd_RecursiveDerefZdd(dd,zvar);
00952     cuddDeref(res);
00953     return(res);
00954 
00955 } /* 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 762 of file cuddZddSetop.c.

00766 {
00767     int         top_var, level;
00768     DdNode      *res, *t, *e;
00769     DdNode      *base = DD_ONE(zdd);
00770     DdNode      *empty = DD_ZERO(zdd);
00771 
00772     statLine(zdd);
00773     if (P == empty)
00774         return(empty);
00775     if (P == base)
00776         return(zvar);
00777 
00778     /* Check cache. */
00779     res = cuddCacheLookup2Zdd(zdd, cuddZddChangeAux, P, zvar);
00780     if (res != NULL)
00781         return(res);
00782 
00783     top_var = zdd->permZ[P->index];
00784     level = zdd->permZ[zvar->index];
00785 
00786     if (top_var > level) {
00787         res = cuddZddGetNode(zdd, zvar->index, P, DD_ZERO(zdd));
00788         if (res == NULL) return(NULL);
00789     } else if (top_var == level) {
00790         res = cuddZddGetNode(zdd, zvar->index, cuddE(P), cuddT(P));
00791         if (res == NULL) return(NULL);
00792     } else {
00793         t = cuddZddChangeAux(zdd, cuddT(P), zvar);
00794         if (t == NULL) return(NULL);
00795         cuddRef(t);
00796         e = cuddZddChangeAux(zdd, cuddE(P), zvar);
00797         if (e == NULL) {
00798             Cudd_RecursiveDerefZdd(zdd, t);
00799             return(NULL);
00800         }
00801         cuddRef(e);
00802         res = cuddZddGetNode(zdd, P->index, t, e);
00803         if (res == NULL) {
00804             Cudd_RecursiveDerefZdd(zdd, t);
00805             Cudd_RecursiveDerefZdd(zdd, e);
00806             return(NULL);
00807         }
00808         cuddDeref(t);
00809         cuddDeref(e);
00810     }
00811 
00812     cuddCacheInsert2(zdd, cuddZddChangeAux, P, zvar, res);
00813 
00814     return(res);
00815 
00816 } /* 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 680 of file cuddZddSetop.c.

00684 {
00685     int         p_top, q_top;
00686     DdNode      *empty = DD_ZERO(zdd), *t, *e, *res;
00687     DdManager   *table = zdd;
00688 
00689     statLine(zdd);
00690     if (P == empty)
00691         return(empty);
00692     if (Q == empty)
00693         return(P);
00694     if (P == Q)
00695         return(empty);
00696 
00697     /* Check cache.  The cache is shared by Cudd_zddDiffConst(). */
00698     res = cuddCacheLookup2Zdd(table, cuddZddDiff, P, Q);
00699     if (res != NULL && res != DD_NON_CONSTANT)
00700         return(res);
00701 
00702     if (cuddIsConstant(P))
00703         p_top = P->index;
00704     else
00705         p_top = zdd->permZ[P->index];
00706     if (cuddIsConstant(Q))
00707         q_top = Q->index;
00708     else
00709         q_top = zdd->permZ[Q->index];
00710     if (p_top < q_top) {
00711         e = cuddZddDiff(zdd, cuddE(P), Q);
00712         if (e == NULL) return(NULL);
00713         cuddRef(e);
00714         res = cuddZddGetNode(zdd, P->index, cuddT(P), e);
00715         if (res == NULL) {
00716             Cudd_RecursiveDerefZdd(table, e);
00717             return(NULL);
00718         }
00719         cuddDeref(e);
00720     } else if (p_top > q_top) {
00721         res = cuddZddDiff(zdd, P, cuddE(Q));
00722         if (res == NULL) return(NULL);
00723     } else {
00724         t = cuddZddDiff(zdd, cuddT(P), cuddT(Q));
00725         if (t == NULL) return(NULL);
00726         cuddRef(t);
00727         e = cuddZddDiff(zdd, cuddE(P), cuddE(Q));
00728         if (e == NULL) {
00729             Cudd_RecursiveDerefZdd(table, t);
00730             return(NULL);
00731         }
00732         cuddRef(e);
00733         res = cuddZddGetNode(zdd, P->index, t, e);
00734         if (res == NULL) {
00735             Cudd_RecursiveDerefZdd(table, t);
00736             Cudd_RecursiveDerefZdd(table, e);
00737             return(NULL);
00738         }
00739         cuddDeref(t);
00740         cuddDeref(e);
00741     }
00742 
00743     cuddCacheInsert2(table, cuddZddDiff, P, Q, res);
00744 
00745     return(res);
00746 
00747 } /* 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 605 of file cuddZddSetop.c.

00609 {
00610     int         p_top, q_top;
00611     DdNode      *empty = DD_ZERO(zdd), *t, *e, *res;
00612     DdManager   *table = zdd;
00613 
00614     statLine(zdd);
00615     if (P == empty)
00616         return(empty);
00617     if (Q == empty)
00618         return(empty);
00619     if (P == Q)
00620         return(P);
00621 
00622     /* Check cache. */
00623     res = cuddCacheLookup2Zdd(table, cuddZddIntersect, P, Q);
00624     if (res != NULL)
00625         return(res);
00626 
00627     if (cuddIsConstant(P))
00628         p_top = P->index;
00629     else
00630         p_top = zdd->permZ[P->index];
00631     if (cuddIsConstant(Q))
00632         q_top = Q->index;
00633     else
00634         q_top = zdd->permZ[Q->index];
00635     if (p_top < q_top) {
00636         res = cuddZddIntersect(zdd, cuddE(P), Q);
00637         if (res == NULL) return(NULL);
00638     } else if (p_top > q_top) {
00639         res = cuddZddIntersect(zdd, P, cuddE(Q));
00640         if (res == NULL) return(NULL);
00641     } else {
00642         t = cuddZddIntersect(zdd, cuddT(P), cuddT(Q));
00643         if (t == NULL) return(NULL);
00644         cuddRef(t);
00645         e = cuddZddIntersect(zdd, cuddE(P), cuddE(Q));
00646         if (e == NULL) {
00647             Cudd_RecursiveDerefZdd(table, t);
00648             return(NULL);
00649         }
00650         cuddRef(e);
00651         res = cuddZddGetNode(zdd, P->index, t, e);
00652         if (res == NULL) {
00653             Cudd_RecursiveDerefZdd(table, t);
00654             Cudd_RecursiveDerefZdd(table, e);
00655             return(NULL);
00656         }
00657         cuddDeref(t);
00658         cuddDeref(e);
00659     }
00660 
00661     cuddCacheInsert2(table, cuddZddIntersect, P, Q, res);
00662 
00663     return(res);
00664 
00665 } /* 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 390 of file cuddZddSetop.c.

00395 {
00396     DdNode *tautology, *empty;
00397     DdNode *r,*Gv,*Gvn,*Hv,*Hvn,*t,*e;
00398     unsigned int topf,topg,toph,v,top;
00399     int index;
00400 
00401     statLine(dd);
00402     /* Trivial cases. */
00403     /* One variable cases. */
00404     if (f == (empty = DD_ZERO(dd))) {   /* ITE(0,G,H) = H */
00405         return(h);
00406     }
00407     topf = cuddIZ(dd,f->index);
00408     topg = cuddIZ(dd,g->index);
00409     toph = cuddIZ(dd,h->index);
00410     v = ddMin(topg,toph);
00411     top  = ddMin(topf,v);
00412 
00413     tautology = (top == CUDD_MAXINDEX) ? DD_ONE(dd) : dd->univ[top];
00414     if (f == tautology) {                       /* ITE(1,G,H) = G */
00415         return(g);
00416     }
00417 
00418     /* From now on, f is known to not be a constant. */
00419     zddVarToConst(f,&g,&h,tautology,empty);
00420 
00421     /* Check remaining one variable cases. */
00422     if (g == h) {                       /* ITE(F,G,G) = G */
00423         return(g);
00424     }
00425 
00426     if (g == tautology) {                       /* ITE(F,1,0) = F */
00427         if (h == empty) return(f);
00428     }
00429 
00430     /* Check cache. */
00431     r = cuddCacheLookupZdd(dd,DD_ZDD_ITE_TAG,f,g,h);
00432     if (r != NULL) {
00433         return(r);
00434     }
00435 
00436     /* Recompute these because they may have changed in zddVarToConst. */
00437     topg = cuddIZ(dd,g->index);
00438     toph = cuddIZ(dd,h->index);
00439     v = ddMin(topg,toph);
00440 
00441     if (topf < v) {
00442         r = cuddZddIte(dd,cuddE(f),g,h);
00443         if (r == NULL) return(NULL);
00444     } else if (topf > v) {
00445         if (topg > v) {
00446             Gvn = g;
00447             index = h->index;
00448         } else {
00449             Gvn = cuddE(g);
00450             index = g->index;
00451         }
00452         if (toph > v) {
00453             Hv = empty; Hvn = h;
00454         } else {
00455             Hv = cuddT(h); Hvn = cuddE(h);
00456         }
00457         e = cuddZddIte(dd,f,Gvn,Hvn);
00458         if (e == NULL) return(NULL);
00459         cuddRef(e);
00460         r = cuddZddGetNode(dd,index,Hv,e);
00461         if (r == NULL) {
00462             Cudd_RecursiveDerefZdd(dd,e);
00463             return(NULL);
00464         }
00465         cuddDeref(e);
00466     } else {
00467         index = f->index;
00468         if (topg > v) {
00469             Gv = empty; Gvn = g;
00470         } else {
00471             Gv = cuddT(g); Gvn = cuddE(g);
00472         }
00473         if (toph > v) {
00474             Hv = empty; Hvn = h;
00475         } else {
00476             Hv = cuddT(h); Hvn = cuddE(h);
00477         }
00478         e = cuddZddIte(dd,cuddE(f),Gvn,Hvn);
00479         if (e == NULL) return(NULL);
00480         cuddRef(e);
00481         t = cuddZddIte(dd,cuddT(f),Gv,Hv);
00482         if (t == NULL) {
00483             Cudd_RecursiveDerefZdd(dd,e);
00484             return(NULL);
00485         }
00486         cuddRef(t);
00487         r = cuddZddGetNode(dd,index,t,e);
00488         if (r == NULL) {
00489             Cudd_RecursiveDerefZdd(dd,e);
00490             Cudd_RecursiveDerefZdd(dd,t);
00491             return(NULL);
00492         }
00493         cuddDeref(t);
00494         cuddDeref(e);
00495     }
00496 
00497     cuddCacheInsert(dd,DD_ZDD_ITE_TAG,f,g,h,r);
00498 
00499     return(r);
00500 
00501 } /* 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 886 of file cuddZddSetop.c.

00890 {
00891     DdNode      *zvar, *r;
00892     DdNode      *base, *empty;
00893 
00894     base = DD_ONE(dd);
00895     empty = DD_ZERO(dd);
00896 
00897     zvar = cuddUniqueInterZdd(dd, var, base, empty);
00898     if (zvar == NULL) {
00899         return(NULL);
00900     } else {
00901         cuddRef(zvar);
00902         r = zdd_subset0_aux(dd, P, zvar);
00903         if (r == NULL) {
00904             Cudd_RecursiveDerefZdd(dd, zvar);
00905             return(NULL);
00906         }
00907         cuddRef(r);
00908         Cudd_RecursiveDerefZdd(dd, zvar);
00909     }
00910 
00911     cuddDeref(r);
00912     return(r);
00913 
00914 } /* 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 837 of file cuddZddSetop.c.

00841 {
00842     DdNode      *zvar, *r;
00843     DdNode      *base, *empty;
00844 
00845     base = DD_ONE(dd);
00846     empty = DD_ZERO(dd);
00847 
00848     zvar = cuddUniqueInterZdd(dd, var, base, empty);
00849     if (zvar == NULL) {
00850         return(NULL);
00851     } else {
00852         cuddRef(zvar);
00853         r = zdd_subset1_aux(dd, P, zvar);
00854         if (r == NULL) {
00855             Cudd_RecursiveDerefZdd(dd, zvar);
00856             return(NULL);
00857         }
00858         cuddRef(r);
00859         Cudd_RecursiveDerefZdd(dd, zvar);
00860     }
00861 
00862     cuddDeref(r);
00863     return(r);
00864 
00865 } /* 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 516 of file cuddZddSetop.c.

00520 {
00521     int         p_top, q_top;
00522     DdNode      *empty = DD_ZERO(zdd), *t, *e, *res;
00523     DdManager   *table = zdd;
00524 
00525     statLine(zdd);
00526     if (P == empty)
00527         return(Q);
00528     if (Q == empty)
00529         return(P);
00530     if (P == Q)
00531         return(P);
00532 
00533     /* Check cache */
00534     res = cuddCacheLookup2Zdd(table, cuddZddUnion, P, Q);
00535     if (res != NULL)
00536         return(res);
00537 
00538     if (cuddIsConstant(P))
00539         p_top = P->index;
00540     else
00541         p_top = zdd->permZ[P->index];
00542     if (cuddIsConstant(Q))
00543         q_top = Q->index;
00544     else
00545         q_top = zdd->permZ[Q->index];
00546     if (p_top < q_top) {
00547         e = cuddZddUnion(zdd, cuddE(P), Q);
00548         if (e == NULL) return (NULL);
00549         cuddRef(e);
00550         res = cuddZddGetNode(zdd, P->index, cuddT(P), e);
00551         if (res == NULL) {
00552             Cudd_RecursiveDerefZdd(table, e);
00553             return(NULL);
00554         }
00555         cuddDeref(e);
00556     } else if (p_top > q_top) {
00557         e = cuddZddUnion(zdd, P, cuddE(Q));
00558         if (e == NULL) return(NULL);
00559         cuddRef(e);
00560         res = cuddZddGetNode(zdd, Q->index, cuddT(Q), e);
00561         if (res == NULL) {
00562             Cudd_RecursiveDerefZdd(table, e);
00563             return(NULL);
00564         }
00565         cuddDeref(e);
00566     } else {
00567         t = cuddZddUnion(zdd, cuddT(P), cuddT(Q));
00568         if (t == NULL) return(NULL);
00569         cuddRef(t);
00570         e = cuddZddUnion(zdd, cuddE(P), cuddE(Q));
00571         if (e == NULL) {
00572             Cudd_RecursiveDerefZdd(table, t);
00573             return(NULL);
00574         }
00575         cuddRef(e);
00576         res = cuddZddGetNode(zdd, P->index, t, e);
00577         if (res == NULL) {
00578             Cudd_RecursiveDerefZdd(table, t);
00579             Cudd_RecursiveDerefZdd(table, e);
00580             return(NULL);
00581         }
00582         cuddDeref(t);
00583         cuddDeref(e);
00584     }
00585 
00586     cuddCacheInsert2(table, cuddZddUnion, P, Q, res);
00587 
00588     return(res);
00589 
00590 } /* 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 1045 of file cuddZddSetop.c.

01049 {
01050     int         top_var, level;
01051     DdNode      *res, *t, *e;
01052     DdNode      *base, *empty;
01053 
01054     statLine(zdd);
01055     base = DD_ONE(zdd);
01056     empty = DD_ZERO(zdd);
01057 
01058     /* Check cache. */
01059     res = cuddCacheLookup2Zdd(zdd, zdd_subset0_aux, P, zvar);
01060     if (res != NULL)
01061         return(res);
01062 
01063     if (cuddIsConstant(P)) {
01064         res = P;
01065         cuddCacheInsert2(zdd, zdd_subset0_aux, P, zvar, res);
01066         return(res);
01067     }
01068 
01069     top_var = zdd->permZ[P->index];
01070     level = zdd->permZ[zvar->index];
01071 
01072     if (top_var > level) {
01073         res = P;
01074     }
01075     else if (top_var == level) {
01076         res = cuddE(P);
01077     }
01078     else {
01079         t = zdd_subset0_aux(zdd, cuddT(P), zvar);
01080         if (t == NULL) return(NULL);
01081         cuddRef(t);
01082         e = zdd_subset0_aux(zdd, cuddE(P), zvar);
01083         if (e == NULL) {
01084             Cudd_RecursiveDerefZdd(zdd, t);
01085             return(NULL);
01086         }
01087         cuddRef(e);
01088         res = cuddZddGetNode(zdd, P->index, t, e);
01089         if (res == NULL) {
01090             Cudd_RecursiveDerefZdd(zdd, t);
01091             Cudd_RecursiveDerefZdd(zdd, e);
01092             return(NULL);
01093         }
01094         cuddDeref(t);
01095         cuddDeref(e);
01096     }
01097 
01098     cuddCacheInsert2(zdd, zdd_subset0_aux, P, zvar, res);
01099 
01100     return(res);
01101 
01102 } /* end of zdd_subset0_aux */

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

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

Synopsis [Performs the recursive step of Cudd_zddSubset1.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 975 of file cuddZddSetop.c.

00979 {
00980     int         top_var, level;
00981     DdNode      *res, *t, *e;
00982     DdNode      *base, *empty;
00983 
00984     statLine(zdd);
00985     base = DD_ONE(zdd);
00986     empty = DD_ZERO(zdd);
00987 
00988     /* Check cache. */
00989     res = cuddCacheLookup2Zdd(zdd, zdd_subset1_aux, P, zvar);
00990     if (res != NULL)
00991         return(res);
00992 
00993     if (cuddIsConstant(P)) {
00994         res = empty;
00995         cuddCacheInsert2(zdd, zdd_subset1_aux, P, zvar, res);
00996         return(res);
00997     }
00998 
00999     top_var = zdd->permZ[P->index];
01000     level = zdd->permZ[zvar->index];
01001 
01002     if (top_var > level) {
01003         res = empty;
01004     } else if (top_var == level) {
01005         res = cuddT(P);
01006     } else {
01007         t = zdd_subset1_aux(zdd, cuddT(P), zvar);
01008         if (t == NULL) return(NULL);
01009         cuddRef(t);
01010         e = zdd_subset1_aux(zdd, cuddE(P), zvar);
01011         if (e == NULL) {
01012             Cudd_RecursiveDerefZdd(zdd, t);
01013             return(NULL);
01014         }
01015         cuddRef(e);
01016         res = cuddZddGetNode(zdd, P->index, t, e);
01017         if (res == NULL) {
01018             Cudd_RecursiveDerefZdd(zdd, t);
01019             Cudd_RecursiveDerefZdd(zdd, e);
01020             return(NULL);
01021         }
01022         cuddDeref(t);
01023         cuddDeref(e);
01024     }
01025 
01026     cuddCacheInsert2(zdd, zdd_subset1_aux, P, zvar, res);
01027 
01028     return(res);
01029 
01030 } /* 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 1118 of file cuddZddSetop.c.

01124 {
01125     DdNode *g = *gp;
01126     DdNode *h = *hp;
01127 
01128     if (f == g) { /* ITE(F,F,H) = ITE(F,1,H) = F + H */
01129         *gp = base;
01130     }
01131 
01132     if (f == h) { /* ITE(F,G,F) = ITE(F,G,0) = F * G */
01133         *hp = empty;
01134     }
01135 
01136 } /* end of zddVarToConst */

Variable Documentation

char rcsid [] DD_UNUSED = "$Id: cuddZddSetop.c,v 1.1.1.1 2003/02/24 22:23:54 wjiang 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 [ 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 72 of file cuddZddSetop.c.

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