src/bdd/cudd/cuddBddAbs.c File Reference

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

Go to the source code of this file.

Functions

static int bddCheckPositiveCube ARGS ((DdManager *manager, DdNode *cube))
DdNode * Cudd_bddExistAbstract (DdManager *manager, DdNode *f, DdNode *cube)
DdNode * Cudd_bddXorExistAbstract (DdManager *manager, DdNode *f, DdNode *g, DdNode *cube)
DdNode * Cudd_bddUnivAbstract (DdManager *manager, DdNode *f, DdNode *cube)
DdNode * Cudd_bddBooleanDiff (DdManager *manager, DdNode *f, int x)
int Cudd_bddVarIsDependent (DdManager *dd, DdNode *f, DdNode *var)
DdNode * cuddBddExistAbstractRecur (DdManager *manager, DdNode *f, DdNode *cube)
DdNode * cuddBddXorExistAbstractRecur (DdManager *manager, DdNode *f, DdNode *g, DdNode *cube)
DdNode * cuddBddBooleanDiffRecur (DdManager *manager, DdNode *f, DdNode *var)
static int bddCheckPositiveCube (DdManager *manager, DdNode *cube)

Variables

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

Function Documentation

static int bddCheckPositiveCube ARGS ( (DdManager *manager, DdNode *cube)   )  [static]

AutomaticStart

static int bddCheckPositiveCube ( DdManager *  manager,
DdNode *  cube 
) [static]

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

Synopsis [Checks whether cube is an BDD representing the product of positive literals.]

Description [Returns 1 in case of success; 0 otherwise.]

SideEffects [None]

Definition at line 676 of file cuddBddAbs.c.

00679 {
00680     if (Cudd_IsComplement(cube)) return(0);
00681     if (cube == DD_ONE(manager)) return(1);
00682     if (cuddIsConstant(cube)) return(0);
00683     if (cuddE(cube) == Cudd_Not(DD_ONE(manager))) {
00684         return(bddCheckPositiveCube(manager, cuddT(cube)));
00685     }
00686     return(0);
00687 
00688 } /* end of bddCheckPositiveCube */

DdNode* Cudd_bddBooleanDiff ( DdManager *  manager,
DdNode *  f,
int  x 
)

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

Synopsis [Computes the boolean difference of f with respect to x.]

Description [Computes the boolean difference of f with respect to the variable with index x. Returns the BDD of the boolean difference if successful; NULL otherwise.]

SideEffects [None]

SeeAlso []

Definition at line 215 of file cuddBddAbs.c.

00219 {
00220     DdNode *res, *var;
00221 
00222     /* If the variable is not currently in the manager, f cannot
00223     ** depend on it.
00224     */
00225     if (x >= manager->size) return(Cudd_Not(DD_ONE(manager)));
00226     var = manager->vars[x];
00227 
00228     do {
00229         manager->reordered = 0;
00230         res = cuddBddBooleanDiffRecur(manager, Cudd_Regular(f), var);
00231     } while (manager->reordered == 1);
00232 
00233     return(res);
00234 
00235 } /* end of Cudd_bddBooleanDiff */

DdNode* Cudd_bddExistAbstract ( DdManager *  manager,
DdNode *  f,
DdNode *  cube 
)

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

Synopsis [Existentially abstracts all the variables in cube from f.]

Description [Existentially abstracts all the variables in cube from f. Returns the abstracted BDD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_bddUnivAbstract Cudd_addExistAbstract]

Definition at line 99 of file cuddBddAbs.c.

00103 {
00104     DdNode *res;
00105 
00106     if (bddCheckPositiveCube(manager, cube) == 0) {
00107         (void) fprintf(manager->err,
00108                        "Error: Can only abstract positive cubes\n");
00109         manager->errorCode = CUDD_INVALID_ARG;
00110         return(NULL);
00111     }
00112 
00113     do {
00114         manager->reordered = 0;
00115         res = cuddBddExistAbstractRecur(manager, f, cube);
00116     } while (manager->reordered == 1);
00117 
00118     return(res);
00119 
00120 } /* end of Cudd_bddExistAbstract */

DdNode* Cudd_bddUnivAbstract ( DdManager *  manager,
DdNode *  f,
DdNode *  cube 
)

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

Synopsis [Universally abstracts all the variables in cube from f.]

Description [Universally abstracts all the variables in cube from f. Returns the abstracted BDD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_bddExistAbstract Cudd_addUnivAbstract]

Definition at line 176 of file cuddBddAbs.c.

00180 {
00181     DdNode      *res;
00182 
00183     if (bddCheckPositiveCube(manager, cube) == 0) {
00184         (void) fprintf(manager->err,
00185                        "Error: Can only abstract positive cubes\n");
00186         manager->errorCode = CUDD_INVALID_ARG;
00187         return(NULL);
00188     }
00189 
00190     do {
00191         manager->reordered = 0;
00192         res = cuddBddExistAbstractRecur(manager, Cudd_Not(f), cube);
00193     } while (manager->reordered == 1);
00194     if (res != NULL) res = Cudd_Not(res);
00195 
00196     return(res);
00197 
00198 } /* end of Cudd_bddUnivAbstract */

int Cudd_bddVarIsDependent ( DdManager *  dd,
DdNode *  f,
DdNode *  var 
)

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

Synopsis [Checks whether a variable is dependent on others in a function.]

Description [Checks whether a variable is dependent on others in a function. Returns 1 if the variable is dependent; 0 otherwise. No new nodes are created.]

SideEffects [None]

SeeAlso []

Definition at line 253 of file cuddBddAbs.c.

00257 {
00258     DdNode *F, *res, *zero, *ft, *fe;
00259     unsigned topf, level;
00260     DdNode *(*cacheOp)(DdManager *, DdNode *, DdNode *);
00261     int retval;
00262 
00263     zero = Cudd_Not(DD_ONE(dd));
00264     if (Cudd_IsConstant(f)) return(f == zero);
00265 
00266     /* From now on f is not constant. */
00267     F = Cudd_Regular(f);
00268     topf = (unsigned) dd->perm[F->index];
00269     level = (unsigned) dd->perm[var->index];
00270 
00271     /* Check terminal case. If topf > index of var, f does not depend on var.
00272     ** Therefore, var is not dependent in f. */
00273     if (topf > level) {
00274         return(0);
00275     }
00276 
00277     cacheOp =
00278         (DdNode *(*)(DdManager *, DdNode *, DdNode *)) Cudd_bddVarIsDependent;
00279     res = cuddCacheLookup2(dd,cacheOp,f,var);
00280     if (res != NULL) {
00281         return(res != zero);
00282     }
00283 
00284     /* Compute cofactors. */
00285     ft = Cudd_NotCond(cuddT(F), f != F);
00286     fe = Cudd_NotCond(cuddE(F), f != F);
00287 
00288     if (topf == level) {
00289         retval = Cudd_bddLeq(dd,ft,Cudd_Not(fe));
00290     } else {
00291         retval = Cudd_bddVarIsDependent(dd,ft,var) &&
00292             Cudd_bddVarIsDependent(dd,fe,var);
00293     }
00294 
00295     cuddCacheInsert2(dd,cacheOp,f,var,Cudd_NotCond(zero,retval));
00296 
00297     return(retval);
00298 
00299 } /* Cudd_bddVarIsDependent */

DdNode* Cudd_bddXorExistAbstract ( DdManager *  manager,
DdNode *  f,
DdNode *  g,
DdNode *  cube 
)

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

Synopsis [Takes the exclusive OR of two BDDs and simultaneously abstracts the variables in cube.]

Description [Takes the exclusive OR of two BDDs and simultaneously abstracts the variables in cube. The variables are existentially abstracted. Returns a pointer to the result is successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_bddUnivAbstract Cudd_bddExistAbstract Cudd_bddAndAbstract]

Definition at line 138 of file cuddBddAbs.c.

00143 {
00144     DdNode *res;
00145 
00146     if (bddCheckPositiveCube(manager, cube) == 0) {
00147         (void) fprintf(manager->err,
00148                        "Error: Can only abstract positive cubes\n");
00149         manager->errorCode = CUDD_INVALID_ARG;
00150         return(NULL);
00151     }
00152 
00153     do {
00154         manager->reordered = 0;
00155         res = cuddBddXorExistAbstractRecur(manager, f, g, cube);
00156     } while (manager->reordered == 1);
00157 
00158     return(res);
00159 
00160 } /* end of Cudd_bddXorExistAbstract */

DdNode* cuddBddBooleanDiffRecur ( DdManager *  manager,
DdNode *  f,
DdNode *  var 
)

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

Synopsis [Performs the recursive steps of Cudd_bddBoleanDiff.]

Description [Performs the recursive steps of Cudd_bddBoleanDiff. Returns the BDD obtained by XORing the cofactors of f with respect to var if successful; NULL otherwise. Exploits the fact that dF/dx = dF'/dx.]

SideEffects [None]

SeeAlso []

Definition at line 604 of file cuddBddAbs.c.

00608 {
00609     DdNode *T, *E, *res, *res1, *res2;
00610 
00611     statLine(manager);
00612     if (cuddI(manager,f->index) > manager->perm[var->index]) {
00613         /* f does not depend on var. */
00614         return(Cudd_Not(DD_ONE(manager)));
00615     }
00616 
00617     /* From now on, f is non-constant. */
00618 
00619     /* If the two indices are the same, so are their levels. */
00620     if (f->index == var->index) {
00621         res = cuddBddXorRecur(manager, cuddT(f), cuddE(f));
00622         return(res);
00623     }
00624 
00625     /* From now on, cuddI(manager,f->index) < cuddI(manager,cube->index). */
00626 
00627     /* Check the cache. */
00628     res = cuddCacheLookup2(manager, cuddBddBooleanDiffRecur, f, var);
00629     if (res != NULL) {
00630         return(res);
00631     }
00632 
00633     /* Compute the cofactors of f. */
00634     T = cuddT(f); E = cuddE(f);
00635 
00636     res1 = cuddBddBooleanDiffRecur(manager, T, var);
00637     if (res1 == NULL) return(NULL);
00638     cuddRef(res1);
00639     res2 = cuddBddBooleanDiffRecur(manager, Cudd_Regular(E), var);
00640     if (res2 == NULL) {
00641         Cudd_IterDerefBdd(manager, res1);
00642         return(NULL);
00643     }
00644     cuddRef(res2);
00645     /* ITE takes care of possible complementation of res1 and of the
00646     ** case in which res1 == res2. */
00647     res = cuddBddIteRecur(manager, manager->vars[f->index], res1, res2);
00648     if (res == NULL) {
00649         Cudd_IterDerefBdd(manager, res1);
00650         Cudd_IterDerefBdd(manager, res2);
00651         return(NULL);
00652     }
00653     cuddDeref(res1);
00654     cuddDeref(res2);
00655     cuddCacheInsert2(manager, cuddBddBooleanDiffRecur, f, var, res);
00656     return(res);
00657 
00658 } /* end of cuddBddBooleanDiffRecur */

DdNode* cuddBddExistAbstractRecur ( DdManager *  manager,
DdNode *  f,
DdNode *  cube 
)

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

Synopsis [Performs the recursive steps of Cudd_bddExistAbstract.]

Description [Performs the recursive steps of Cudd_bddExistAbstract. Returns the BDD obtained by abstracting the variables of cube from f if successful; NULL otherwise. It is also used by Cudd_bddUnivAbstract.]

SideEffects [None]

SeeAlso [Cudd_bddExistAbstract Cudd_bddUnivAbstract]

Definition at line 322 of file cuddBddAbs.c.

00326 {
00327     DdNode      *F, *T, *E, *res, *res1, *res2, *one;
00328 
00329     statLine(manager);
00330     one = DD_ONE(manager);
00331     F = Cudd_Regular(f);
00332 
00333     /* Cube is guaranteed to be a cube at this point. */        
00334     if (cube == one || F == one) {  
00335         return(f);
00336     }
00337     /* From now on, f and cube are non-constant. */
00338 
00339     /* Abstract a variable that does not appear in f. */
00340     while (manager->perm[F->index] > manager->perm[cube->index]) {
00341         cube = cuddT(cube);
00342         if (cube == one) return(f);
00343     }
00344 
00345     /* Check the cache. */
00346     if (F->ref != 1 && (res = cuddCacheLookup2(manager, Cudd_bddExistAbstract, f, cube)) != NULL) {
00347         return(res);
00348     }
00349 
00350     /* Compute the cofactors of f. */
00351     T = cuddT(F); E = cuddE(F);
00352     if (f != F) {
00353         T = Cudd_Not(T); E = Cudd_Not(E);
00354     }
00355 
00356     /* If the two indices are the same, so are their levels. */
00357     if (F->index == cube->index) {
00358         if (T == one || E == one || T == Cudd_Not(E)) {
00359             return(one);
00360         }
00361         res1 = cuddBddExistAbstractRecur(manager, T, cuddT(cube));
00362         if (res1 == NULL) return(NULL);
00363         if (res1 == one) {
00364             if (F->ref != 1)
00365                 cuddCacheInsert2(manager, Cudd_bddExistAbstract, f, cube, one);
00366             return(one);
00367         }
00368         cuddRef(res1);
00369         res2 = cuddBddExistAbstractRecur(manager, E, cuddT(cube));
00370         if (res2 == NULL) {
00371             Cudd_IterDerefBdd(manager,res1);
00372             return(NULL);
00373         }
00374         cuddRef(res2);
00375         res = cuddBddAndRecur(manager, Cudd_Not(res1), Cudd_Not(res2));
00376         if (res == NULL) {
00377             Cudd_IterDerefBdd(manager, res1);
00378             Cudd_IterDerefBdd(manager, res2);
00379             return(NULL);
00380         }
00381         res = Cudd_Not(res);
00382         cuddRef(res);
00383         Cudd_IterDerefBdd(manager, res1);
00384         Cudd_IterDerefBdd(manager, res2);
00385         if (F->ref != 1)
00386             cuddCacheInsert2(manager, Cudd_bddExistAbstract, f, cube, res);
00387         cuddDeref(res);
00388         return(res);
00389     } else { /* if (cuddI(manager,F->index) < cuddI(manager,cube->index)) */
00390         res1 = cuddBddExistAbstractRecur(manager, T, cube);
00391         if (res1 == NULL) return(NULL);
00392         cuddRef(res1);
00393         res2 = cuddBddExistAbstractRecur(manager, E, cube);
00394         if (res2 == NULL) {
00395             Cudd_IterDerefBdd(manager, res1);
00396             return(NULL);
00397         }
00398         cuddRef(res2);
00399         /* ITE takes care of possible complementation of res1 and of the
00400         ** case in which res1 == res2. */
00401         res = cuddBddIteRecur(manager, manager->vars[F->index], res1, res2);
00402         if (res == NULL) {
00403             Cudd_IterDerefBdd(manager, res1);
00404             Cudd_IterDerefBdd(manager, res2);
00405             return(NULL);
00406         }
00407         cuddDeref(res1);
00408         cuddDeref(res2);
00409         if (F->ref != 1)
00410             cuddCacheInsert2(manager, Cudd_bddExistAbstract, f, cube, res);
00411         return(res);
00412     }       
00413 
00414 } /* end of cuddBddExistAbstractRecur */

DdNode* cuddBddXorExistAbstractRecur ( DdManager *  manager,
DdNode *  f,
DdNode *  g,
DdNode *  cube 
)

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

Synopsis [Takes the exclusive OR of two BDDs and simultaneously abstracts the variables in cube.]

Description [Takes the exclusive OR of two BDDs and simultaneously abstracts the variables in cube. The variables are existentially abstracted. Returns a pointer to the result is successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_bddAndAbstract]

Definition at line 432 of file cuddBddAbs.c.

00437 {
00438     DdNode *F, *fv, *fnv, *G, *gv, *gnv;
00439     DdNode *one, *zero, *r, *t, *e, *Cube;
00440     unsigned int topf, topg, topcube, top, index;
00441 
00442     statLine(manager);
00443     one = DD_ONE(manager);
00444     zero = Cudd_Not(one);
00445 
00446     /* Terminal cases. */
00447     if (f == g) {
00448         return(zero);
00449     }
00450     if (f == Cudd_Not(g)) {
00451         return(one);
00452     }
00453     if (cube == one) {
00454         return(cuddBddXorRecur(manager, f, g));
00455     }
00456     if (f == one) {
00457         return(cuddBddExistAbstractRecur(manager, Cudd_Not(g), cube));
00458     }
00459     if (g == one) {
00460         return(cuddBddExistAbstractRecur(manager, Cudd_Not(f), cube));
00461     }
00462     if (f == zero) {
00463         return(cuddBddExistAbstractRecur(manager, g, cube));
00464     }
00465     if (g == zero) {
00466         return(cuddBddExistAbstractRecur(manager, f, cube));
00467     }
00468 
00469     /* At this point f, g, and cube are not constant. */
00470 
00471     if (f > g) { /* Try to increase cache efficiency. */
00472         DdNode *tmp = f;
00473         f = g;
00474         g = tmp;
00475     }
00476 
00477     /* Check cache. */
00478     r = cuddCacheLookup(manager, DD_BDD_XOR_EXIST_ABSTRACT_TAG, f, g, cube);
00479     if (r != NULL) {
00480         return(r);
00481     }
00482 
00483     /* Here we can skip the use of cuddI, because the operands are known
00484     ** to be non-constant.
00485     */
00486     F = Cudd_Regular(f);
00487     topf = manager->perm[F->index];
00488     G = Cudd_Regular(g);
00489     topg = manager->perm[G->index];
00490     top = ddMin(topf, topg);
00491     topcube = manager->perm[cube->index];
00492 
00493     if (topcube < top) {
00494         return(cuddBddXorExistAbstractRecur(manager, f, g, cuddT(cube)));
00495     }
00496     /* Now, topcube >= top. */
00497 
00498     if (topf == top) {
00499         index = F->index;
00500         fv = cuddT(F);
00501         fnv = cuddE(F);
00502         if (Cudd_IsComplement(f)) {
00503             fv = Cudd_Not(fv);
00504             fnv = Cudd_Not(fnv);
00505         }
00506     } else {
00507         index = G->index;
00508         fv = fnv = f;
00509     }
00510 
00511     if (topg == top) {
00512         gv = cuddT(G);
00513         gnv = cuddE(G);
00514         if (Cudd_IsComplement(g)) {
00515             gv = Cudd_Not(gv);
00516             gnv = Cudd_Not(gnv);
00517         }
00518     } else {
00519         gv = gnv = g;
00520     }
00521 
00522     if (topcube == top) {
00523         Cube = cuddT(cube);
00524     } else {
00525         Cube = cube;
00526     }
00527 
00528     t = cuddBddXorExistAbstractRecur(manager, fv, gv, Cube);
00529     if (t == NULL) return(NULL);
00530 
00531     /* Special case: 1 OR anything = 1. Hence, no need to compute
00532     ** the else branch if t is 1.
00533     */
00534     if (t == one && topcube == top) {
00535         cuddCacheInsert(manager, DD_BDD_XOR_EXIST_ABSTRACT_TAG, f, g, cube, one);
00536         return(one);
00537     }
00538     cuddRef(t);
00539 
00540     e = cuddBddXorExistAbstractRecur(manager, fnv, gnv, Cube);
00541     if (e == NULL) {
00542         Cudd_IterDerefBdd(manager, t);
00543         return(NULL);
00544     }
00545     cuddRef(e);
00546 
00547     if (topcube == top) {       /* abstract */
00548         r = cuddBddAndRecur(manager, Cudd_Not(t), Cudd_Not(e));
00549         if (r == NULL) {
00550             Cudd_IterDerefBdd(manager, t);
00551             Cudd_IterDerefBdd(manager, e);
00552             return(NULL);
00553         }
00554         r = Cudd_Not(r);
00555         cuddRef(r);
00556         Cudd_IterDerefBdd(manager, t);
00557         Cudd_IterDerefBdd(manager, e);
00558         cuddDeref(r);
00559     } else if (t == e) {
00560         r = t;
00561         cuddDeref(t);
00562         cuddDeref(e);
00563     } else {
00564         if (Cudd_IsComplement(t)) {
00565             r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e));
00566             if (r == NULL) {
00567                 Cudd_IterDerefBdd(manager, t);
00568                 Cudd_IterDerefBdd(manager, e);
00569                 return(NULL);
00570             }
00571             r = Cudd_Not(r);
00572         } else {
00573             r = cuddUniqueInter(manager,(int)index,t,e);
00574             if (r == NULL) {
00575                 Cudd_IterDerefBdd(manager, t);
00576                 Cudd_IterDerefBdd(manager, e);
00577                 return(NULL);
00578             }
00579         }
00580         cuddDeref(e);
00581         cuddDeref(t);
00582     }
00583     cuddCacheInsert(manager, DD_BDD_XOR_EXIST_ABSTRACT_TAG, f, g, cube, r);
00584     return (r);
00585 
00586 } /* end of cuddBddXorExistAbstractRecur */

Variable Documentation

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

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

FileName [cuddBddAbs.c]

PackageName [cudd]

Synopsis [Quantification functions for BDDs.]

Description [External procedures included in this module:

Internal procedures included in this module:

Static procedures included in this module:

]

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 62 of file cuddBddAbs.c.

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