glu-2.2: src/cuBdd/cuddBddAbs.c Source File

00001 
00065 #include "util.h"
00066 #include "cuddInt.h"
00067 
00068 
00069 /*---------------------------------------------------------------------------*/
00070 /* Constant declarations                                                     */
00071 /*---------------------------------------------------------------------------*/
00072 
00073 
00074 /*---------------------------------------------------------------------------*/
00075 /* Stucture declarations                                                     */
00076 /*---------------------------------------------------------------------------*/
00077 
00078 
00079 /*---------------------------------------------------------------------------*/
00080 /* Type declarations                                                         */
00081 /*---------------------------------------------------------------------------*/
00082 
00083 
00084 /*---------------------------------------------------------------------------*/
00085 /* Variable declarations                                                     */
00086 /*---------------------------------------------------------------------------*/
00087 
00088 #ifndef lint
00089 static char rcsid[] DD_UNUSED = "$Id: cuddBddAbs.c,v 1.26 2004/08/13 18:04:46 fabio Exp $";
00090 #endif
00091 
00092 /*---------------------------------------------------------------------------*/
00093 /* Macro declarations                                                        */
00094 /*---------------------------------------------------------------------------*/
00095 
00096 
00099 /*---------------------------------------------------------------------------*/
00100 /* Static function prototypes                                                */
00101 /*---------------------------------------------------------------------------*/
00102 
00103 static int bddCheckPositiveCube (DdManager *manager, DdNode *cube);
00104 
00108 /*---------------------------------------------------------------------------*/
00109 /* Definition of exported functions                                          */
00110 /*---------------------------------------------------------------------------*/
00111 
00112 
00125 DdNode *
00126 Cudd_bddExistAbstract(
00127   DdManager * manager,
00128   DdNode * f,
00129   DdNode * cube)
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 */
00148 
00149 
00164 DdNode *
00165 Cudd_bddXorExistAbstract(
00166   DdManager * manager,
00167   DdNode * f,
00168   DdNode * g,
00169   DdNode * cube)
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 */
00188 
00189 
00202 DdNode *
00203 Cudd_bddUnivAbstract(
00204   DdManager * manager,
00205   DdNode * f,
00206   DdNode * cube)
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 */
00226 
00227 
00241 DdNode *
00242 Cudd_bddBooleanDiff(
00243   DdManager * manager,
00244   DdNode * f,
00245   int  x)
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 */
00263 
00264 
00279 int
00280 Cudd_bddVarIsDependent(
00281   DdManager *dd,                /* manager */
00282   DdNode *f,                    /* function */
00283   DdNode *var                   /* variable */)
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 */
00326 
00327 
00328 /*---------------------------------------------------------------------------*/
00329 /* Definition of internal functions                                          */
00330 /*---------------------------------------------------------------------------*/
00331 
00332 
00347 DdNode *
00348 cuddBddExistAbstractRecur(
00349   DdManager * manager,
00350   DdNode * f,
00351   DdNode * cube)
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 */
00441 
00442 
00457 DdNode *
00458 cuddBddXorExistAbstractRecur(
00459   DdManager * manager,
00460   DdNode * f,
00461   DdNode * g,
00462   DdNode * cube)
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 */
00613 
00614 
00629 DdNode *
00630 cuddBddBooleanDiffRecur(
00631   DdManager * manager,
00632   DdNode * f,
00633   DdNode * var)
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 */
00685 
00686 
00687 /*---------------------------------------------------------------------------*/
00688 /* Definition of static functions                                            */
00689 /*---------------------------------------------------------------------------*/
00690 
00701 static int
00702 bddCheckPositiveCube(
00703   DdManager * manager,
00704   DdNode * cube)
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 */
00715