src/cuBdd/cuddBddAbs.c File Reference

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

Go to the source code of this file.

Functions

static int bddCheckPositiveCube (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)

Variables

static char rcsid[] DD_UNUSED = "$Id: cuddBddAbs.c,v 1.26 2004/08/13 18:04:46 fabio Exp $"

Function Documentation

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

AutomaticStart

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

00705 {
00706     if (Cudd_IsComplement(cube)) return(0);
00707     if (cube == DD_ONE(manager)) return(1);
00708     if (cuddIsConstant(cube)) return(0);
00709     if (cuddE(cube) == Cudd_Not(DD_ONE(manager))) {
00710         return(bddCheckPositiveCube(manager, cuddT(cube)));
00711     }
00712     return(0);
00713 
00714 } /* 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 242 of file cuddBddAbs.c.

00246 {
00247     DdNode *res, *var;
00248 
00249     /* If the variable is not currently in the manager, f cannot
00250     ** depend on it.
00251     */
00252     if (x >= manager->size) return(Cudd_Not(DD_ONE(manager)));
00253     var = manager->vars[x];
00254 
00255     do {
00256         manager->reordered = 0;
00257         res = cuddBddBooleanDiffRecur(manager, Cudd_Regular(f), var);
00258     } while (manager->reordered == 1);
00259 
00260     return(res);
00261 
00262 } /* 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 126 of file cuddBddAbs.c.

00130 {
00131     DdNode *res;
00132 
00133     if (bddCheckPositiveCube(manager, cube) == 0) {
00134         (void) fprintf(manager->err,
00135                        "Error: Can only abstract positive cubes\n");
00136         manager->errorCode = CUDD_INVALID_ARG;
00137         return(NULL);
00138     }
00139 
00140     do {
00141         manager->reordered = 0;
00142         res = cuddBddExistAbstractRecur(manager, f, cube);
00143     } while (manager->reordered == 1);
00144 
00145     return(res);
00146 
00147 } /* 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 203 of file cuddBddAbs.c.

00207 {
00208     DdNode      *res;
00209 
00210     if (bddCheckPositiveCube(manager, cube) == 0) {
00211         (void) fprintf(manager->err,
00212                        "Error: Can only abstract positive cubes\n");
00213         manager->errorCode = CUDD_INVALID_ARG;
00214         return(NULL);
00215     }
00216 
00217     do {
00218         manager->reordered = 0;
00219         res = cuddBddExistAbstractRecur(manager, Cudd_Not(f), cube);
00220     } while (manager->reordered == 1);
00221     if (res != NULL) res = Cudd_Not(res);
00222 
00223     return(res);
00224 
00225 } /* 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 280 of file cuddBddAbs.c.

00284 {
00285     DdNode *F, *res, *zero, *ft, *fe;
00286     unsigned topf, level;
00287     DD_CTFP cacheOp;
00288     int retval;
00289 
00290     zero = Cudd_Not(DD_ONE(dd));
00291     if (Cudd_IsConstant(f)) return(f == zero);
00292 
00293     /* From now on f is not constant. */
00294     F = Cudd_Regular(f);
00295     topf = (unsigned) dd->perm[F->index];
00296     level = (unsigned) dd->perm[var->index];
00297 
00298     /* Check terminal case. If topf > index of var, f does not depend on var.
00299     ** Therefore, var is not dependent in f. */
00300     if (topf > level) {
00301         return(0);
00302     }
00303 
00304     cacheOp = (DD_CTFP) Cudd_bddVarIsDependent;
00305     res = cuddCacheLookup2(dd,cacheOp,f,var);
00306     if (res != NULL) {
00307         return(res != zero);
00308     }
00309 
00310     /* Compute cofactors. */
00311     ft = Cudd_NotCond(cuddT(F), f != F);
00312     fe = Cudd_NotCond(cuddE(F), f != F);
00313 
00314     if (topf == level) {
00315         retval = Cudd_bddLeq(dd,ft,Cudd_Not(fe));
00316     } else {
00317         retval = Cudd_bddVarIsDependent(dd,ft,var) &&
00318             Cudd_bddVarIsDependent(dd,fe,var);
00319     }
00320 
00321     cuddCacheInsert2(dd,cacheOp,f,var,Cudd_NotCond(zero,retval));
00322 
00323     return(retval);
00324 
00325 } /* 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 165 of file cuddBddAbs.c.

00170 {
00171     DdNode *res;
00172 
00173     if (bddCheckPositiveCube(manager, cube) == 0) {
00174         (void) fprintf(manager->err,
00175                        "Error: Can only abstract positive cubes\n");
00176         manager->errorCode = CUDD_INVALID_ARG;
00177         return(NULL);
00178     }
00179 
00180     do {
00181         manager->reordered = 0;
00182         res = cuddBddXorExistAbstractRecur(manager, f, g, cube);
00183     } while (manager->reordered == 1);
00184 
00185     return(res);
00186 
00187 } /* 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 630 of file cuddBddAbs.c.

00634 {
00635     DdNode *T, *E, *res, *res1, *res2;
00636 
00637     statLine(manager);
00638     if (cuddI(manager,f->index) > manager->perm[var->index]) {
00639         /* f does not depend on var. */
00640         return(Cudd_Not(DD_ONE(manager)));
00641     }
00642 
00643     /* From now on, f is non-constant. */
00644 
00645     /* If the two indices are the same, so are their levels. */
00646     if (f->index == var->index) {
00647         res = cuddBddXorRecur(manager, cuddT(f), cuddE(f));
00648         return(res);
00649     }
00650 
00651     /* From now on, cuddI(manager,f->index) < cuddI(manager,cube->index). */
00652 
00653     /* Check the cache. */
00654     res = cuddCacheLookup2(manager, cuddBddBooleanDiffRecur, f, var);
00655     if (res != NULL) {
00656         return(res);
00657     }
00658 
00659     /* Compute the cofactors of f. */
00660     T = cuddT(f); E = cuddE(f);
00661 
00662     res1 = cuddBddBooleanDiffRecur(manager, T, var);
00663     if (res1 == NULL) return(NULL);
00664     cuddRef(res1);
00665     res2 = cuddBddBooleanDiffRecur(manager, Cudd_Regular(E), var);
00666     if (res2 == NULL) {
00667         Cudd_IterDerefBdd(manager, res1);
00668         return(NULL);
00669     }
00670     cuddRef(res2);
00671     /* ITE takes care of possible complementation of res1 and of the
00672     ** case in which res1 == res2. */
00673     res = cuddBddIteRecur(manager, manager->vars[f->index], res1, res2);
00674     if (res == NULL) {
00675         Cudd_IterDerefBdd(manager, res1);
00676         Cudd_IterDerefBdd(manager, res2);
00677         return(NULL);
00678     }
00679     cuddDeref(res1);
00680     cuddDeref(res2);
00681     cuddCacheInsert2(manager, cuddBddBooleanDiffRecur, f, var, res);
00682     return(res);
00683 
00684 } /* 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 348 of file cuddBddAbs.c.

00352 {
00353     DdNode      *F, *T, *E, *res, *res1, *res2, *one;
00354 
00355     statLine(manager);
00356     one = DD_ONE(manager);
00357     F = Cudd_Regular(f);
00358 
00359     /* Cube is guaranteed to be a cube at this point. */        
00360     if (cube == one || F == one) {  
00361         return(f);
00362     }
00363     /* From now on, f and cube are non-constant. */
00364 
00365     /* Abstract a variable that does not appear in f. */
00366     while (manager->perm[F->index] > manager->perm[cube->index]) {
00367         cube = cuddT(cube);
00368         if (cube == one) return(f);
00369     }
00370 
00371     /* Check the cache. */
00372     if (F->ref != 1 && (res = cuddCacheLookup2(manager, Cudd_bddExistAbstract, f, cube)) != NULL) {
00373         return(res);
00374     }
00375 
00376     /* Compute the cofactors of f. */
00377     T = cuddT(F); E = cuddE(F);
00378     if (f != F) {
00379         T = Cudd_Not(T); E = Cudd_Not(E);
00380     }
00381 
00382     /* If the two indices are the same, so are their levels. */
00383     if (F->index == cube->index) {
00384         if (T == one || E == one || T == Cudd_Not(E)) {
00385             return(one);
00386         }
00387         res1 = cuddBddExistAbstractRecur(manager, T, cuddT(cube));
00388         if (res1 == NULL) return(NULL);
00389         if (res1 == one) {
00390             if (F->ref != 1)
00391                 cuddCacheInsert2(manager, Cudd_bddExistAbstract, f, cube, one);
00392             return(one);
00393         }
00394         cuddRef(res1);
00395         res2 = cuddBddExistAbstractRecur(manager, E, cuddT(cube));
00396         if (res2 == NULL) {
00397             Cudd_IterDerefBdd(manager,res1);
00398             return(NULL);
00399         }
00400         cuddRef(res2);
00401         res = cuddBddAndRecur(manager, Cudd_Not(res1), Cudd_Not(res2));
00402         if (res == NULL) {
00403             Cudd_IterDerefBdd(manager, res1);
00404             Cudd_IterDerefBdd(manager, res2);
00405             return(NULL);
00406         }
00407         res = Cudd_Not(res);
00408         cuddRef(res);
00409         Cudd_IterDerefBdd(manager, res1);
00410         Cudd_IterDerefBdd(manager, res2);
00411         if (F->ref != 1)
00412             cuddCacheInsert2(manager, Cudd_bddExistAbstract, f, cube, res);
00413         cuddDeref(res);
00414         return(res);
00415     } else { /* if (cuddI(manager,F->index) < cuddI(manager,cube->index)) */
00416         res1 = cuddBddExistAbstractRecur(manager, T, cube);
00417         if (res1 == NULL) return(NULL);
00418         cuddRef(res1);
00419         res2 = cuddBddExistAbstractRecur(manager, E, cube);
00420         if (res2 == NULL) {
00421             Cudd_IterDerefBdd(manager, res1);
00422             return(NULL);
00423         }
00424         cuddRef(res2);
00425         /* ITE takes care of possible complementation of res1 and of the
00426         ** case in which res1 == res2. */
00427         res = cuddBddIteRecur(manager, manager->vars[F->index], res1, res2);
00428         if (res == NULL) {
00429             Cudd_IterDerefBdd(manager, res1);
00430             Cudd_IterDerefBdd(manager, res2);
00431             return(NULL);
00432         }
00433         cuddDeref(res1);
00434         cuddDeref(res2);
00435         if (F->ref != 1)
00436             cuddCacheInsert2(manager, Cudd_bddExistAbstract, f, cube, res);
00437         return(res);
00438     }       
00439 
00440 } /* 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 458 of file cuddBddAbs.c.

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

Variable Documentation

char rcsid [] DD_UNUSED = "$Id: cuddBddAbs.c,v 1.26 2004/08/13 18:04:46 fabio 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 [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 89 of file cuddBddAbs.c.

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