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

00001 
00063 #include "util.h"
00064 #include "cuddInt.h"
00065 
00066 
00067 /*---------------------------------------------------------------------------*/
00068 /* Constant declarations                                                     */
00069 /*---------------------------------------------------------------------------*/
00070 
00071 
00072 /*---------------------------------------------------------------------------*/
00073 /* Stucture declarations                                                     */
00074 /*---------------------------------------------------------------------------*/
00075 
00076 
00077 /*---------------------------------------------------------------------------*/
00078 /* Type declarations                                                         */
00079 /*---------------------------------------------------------------------------*/
00080 
00081 /*---------------------------------------------------------------------------*/
00082 /* Variable declarations                                                     */
00083 /*---------------------------------------------------------------------------*/
00084 
00085 #ifndef lint
00086 static char rcsid[] DD_UNUSED = "$Id: cuddClip.c,v 1.8 2004/08/13 18:04:47 fabio Exp $";
00087 #endif
00088 
00089 /*---------------------------------------------------------------------------*/
00090 /* Macro declarations                                                        */
00091 /*---------------------------------------------------------------------------*/
00092 
00093 
00096 /*---------------------------------------------------------------------------*/
00097 /* Static function prototypes                                                */
00098 /*---------------------------------------------------------------------------*/
00099 
00100 static DdNode * cuddBddClippingAndRecur (DdManager *manager, DdNode *f, DdNode *g, int distance, int direction);
00101 static DdNode * cuddBddClipAndAbsRecur (DdManager *manager, DdNode *f, DdNode *g, DdNode *cube, int distance, int direction);
00102 
00106 /*---------------------------------------------------------------------------*/
00107 /* Definition of exported functions                                          */
00108 /*---------------------------------------------------------------------------*/
00109 
00110 
00124 DdNode *
00125 Cudd_bddClippingAnd(
00126   DdManager * dd /* manager */,
00127   DdNode * f /* first conjunct */,
00128   DdNode * g /* second conjunct */,
00129   int  maxDepth /* maximum recursion depth */,
00130   int  direction /* under (0) or over (1) approximation */)
00131 {
00132     DdNode *res;
00133 
00134     do {
00135         dd->reordered = 0;
00136         res = cuddBddClippingAnd(dd,f,g,maxDepth,direction);
00137     } while (dd->reordered == 1);
00138     return(res);
00139 
00140 } /* end of Cudd_bddClippingAnd */
00141 
00142 
00158 DdNode *
00159 Cudd_bddClippingAndAbstract(
00160   DdManager * dd /* manager */,
00161   DdNode * f /* first conjunct */,
00162   DdNode * g /* second conjunct */,
00163   DdNode * cube /* cube of variables to be abstracted */,
00164   int  maxDepth /* maximum recursion depth */,
00165   int  direction /* under (0) or over (1) approximation */)
00166 {
00167     DdNode *res;
00168 
00169     do {
00170         dd->reordered = 0;
00171         res = cuddBddClippingAndAbstract(dd,f,g,cube,maxDepth,direction);
00172     } while (dd->reordered == 1);
00173     return(res);
00174 
00175 } /* end of Cudd_bddClippingAndAbstract */
00176 
00177 
00178 /*---------------------------------------------------------------------------*/
00179 /* Definition of internal functions                                          */
00180 /*---------------------------------------------------------------------------*/
00181 
00182 
00196 DdNode *
00197 cuddBddClippingAnd(
00198   DdManager * dd /* manager */,
00199   DdNode * f /* first conjunct */,
00200   DdNode * g /* second conjunct */,
00201   int  maxDepth /* maximum recursion depth */,
00202   int  direction /* under (0) or over (1) approximation */)
00203 {
00204     DdNode *res;
00205 
00206     res = cuddBddClippingAndRecur(dd,f,g,maxDepth,direction);
00207 
00208     return(res);
00209 
00210 } /* end of cuddBddClippingAnd */
00211 
00212 
00228 DdNode *
00229 cuddBddClippingAndAbstract(
00230   DdManager * dd /* manager */,
00231   DdNode * f /* first conjunct */,
00232   DdNode * g /* second conjunct */,
00233   DdNode * cube /* cube of variables to be abstracted */,
00234   int  maxDepth /* maximum recursion depth */,
00235   int  direction /* under (0) or over (1) approximation */)
00236 {
00237     DdNode *res;
00238 
00239     res = cuddBddClipAndAbsRecur(dd,f,g,cube,maxDepth,direction);
00240 
00241     return(res);
00242 
00243 } /* end of cuddBddClippingAndAbstract */
00244 
00245 
00246 /*---------------------------------------------------------------------------*/
00247 /* Definition of static functions                                            */
00248 /*---------------------------------------------------------------------------*/
00249 
00250 
00264 static DdNode *
00265 cuddBddClippingAndRecur(
00266   DdManager * manager,
00267   DdNode * f,
00268   DdNode * g,
00269   int  distance,
00270   int  direction)
00271 {
00272     DdNode *F, *ft, *fe, *G, *gt, *ge;
00273     DdNode *one, *zero, *r, *t, *e;
00274     unsigned int topf, topg, index;
00275     DD_CTFP cacheOp;
00276 
00277     statLine(manager);
00278     one = DD_ONE(manager);
00279     zero = Cudd_Not(one);
00280 
00281     /* Terminal cases. */
00282     if (f == zero || g == zero || f == Cudd_Not(g)) return(zero);
00283     if (f == g || g == one) return(f);
00284     if (f == one) return(g);
00285     if (distance == 0) {
00286         /* One last attempt at returning the right result. We sort of
00287         ** cheat by calling Cudd_bddLeq. */
00288         if (Cudd_bddLeq(manager,f,g)) return(f);
00289         if (Cudd_bddLeq(manager,g,f)) return(g);
00290         if (direction == 1) {
00291             if (Cudd_bddLeq(manager,f,Cudd_Not(g)) ||
00292                 Cudd_bddLeq(manager,g,Cudd_Not(f))) return(zero);
00293         }
00294         return(Cudd_NotCond(one,(direction == 0)));
00295     }
00296 
00297     /* At this point f and g are not constant. */
00298     distance--;
00299 
00300     /* Check cache. Try to increase cache efficiency by sorting the
00301     ** pointers. */
00302     if (f > g) {
00303         DdNode *tmp = f;
00304         f = g; g = tmp;
00305     }
00306     F = Cudd_Regular(f);
00307     G = Cudd_Regular(g);
00308     cacheOp = (DD_CTFP)
00309         (direction ? Cudd_bddClippingAnd : cuddBddClippingAnd);
00310     if (F->ref != 1 || G->ref != 1) {
00311         r = cuddCacheLookup2(manager, cacheOp, f, g);
00312         if (r != NULL) return(r);
00313     }
00314 
00315     /* Here we can skip the use of cuddI, because the operands are known
00316     ** to be non-constant.
00317     */
00318     topf = manager->perm[F->index];
00319     topg = manager->perm[G->index];
00320 
00321     /* Compute cofactors. */
00322     if (topf <= topg) {
00323         index = F->index;
00324         ft = cuddT(F);
00325         fe = cuddE(F);
00326         if (Cudd_IsComplement(f)) {
00327             ft = Cudd_Not(ft);
00328             fe = Cudd_Not(fe);
00329         }
00330     } else {
00331         index = G->index;
00332         ft = fe = f;
00333     }
00334 
00335     if (topg <= topf) {
00336         gt = cuddT(G);
00337         ge = cuddE(G);
00338         if (Cudd_IsComplement(g)) {
00339             gt = Cudd_Not(gt);
00340             ge = Cudd_Not(ge);
00341         }
00342     } else {
00343         gt = ge = g;
00344     }
00345 
00346     t = cuddBddClippingAndRecur(manager, ft, gt, distance, direction);
00347     if (t == NULL) return(NULL);
00348     cuddRef(t);
00349     e = cuddBddClippingAndRecur(manager, fe, ge, distance, direction);
00350     if (e == NULL) {
00351         Cudd_RecursiveDeref(manager, t);
00352         return(NULL);
00353     }
00354     cuddRef(e);
00355 
00356     if (t == e) {
00357         r = t;
00358     } else {
00359         if (Cudd_IsComplement(t)) {
00360             r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e));
00361             if (r == NULL) {
00362                 Cudd_RecursiveDeref(manager, t);
00363                 Cudd_RecursiveDeref(manager, e);
00364                 return(NULL);
00365             }
00366             r = Cudd_Not(r);
00367         } else {
00368             r = cuddUniqueInter(manager,(int)index,t,e);
00369             if (r == NULL) {
00370                 Cudd_RecursiveDeref(manager, t);
00371                 Cudd_RecursiveDeref(manager, e);
00372                 return(NULL);
00373             }
00374         }
00375     }
00376     cuddDeref(e);
00377     cuddDeref(t);
00378     if (F->ref != 1 || G->ref != 1)
00379         cuddCacheInsert2(manager, cacheOp, f, g, r);
00380     return(r);
00381 
00382 } /* end of cuddBddClippingAndRecur */
00383 
00384 
00400 static DdNode *
00401 cuddBddClipAndAbsRecur(
00402   DdManager * manager,
00403   DdNode * f,
00404   DdNode * g,
00405   DdNode * cube,
00406   int  distance,
00407   int  direction)
00408 {
00409     DdNode *F, *ft, *fe, *G, *gt, *ge;
00410     DdNode *one, *zero, *r, *t, *e, *Cube;
00411     unsigned int topf, topg, topcube, top, index;
00412     ptruint cacheTag;
00413 
00414     statLine(manager);
00415     one = DD_ONE(manager);
00416     zero = Cudd_Not(one);
00417 
00418     /* Terminal cases. */
00419     if (f == zero || g == zero || f == Cudd_Not(g)) return(zero);
00420     if (f == one && g == one)   return(one);
00421     if (cube == one) {
00422         return(cuddBddClippingAndRecur(manager, f, g, distance, direction));
00423     }
00424     if (f == one || f == g) {
00425         return (cuddBddExistAbstractRecur(manager, g, cube));
00426     }
00427     if (g == one) {
00428         return (cuddBddExistAbstractRecur(manager, f, cube));
00429     }
00430     if (distance == 0) return(Cudd_NotCond(one,(direction == 0)));
00431 
00432     /* At this point f, g, and cube are not constant. */
00433     distance--;
00434 
00435     /* Check cache. */
00436     if (f > g) { /* Try to increase cache efficiency. */
00437         DdNode *tmp = f;
00438         f = g; g = tmp;
00439     }
00440     F = Cudd_Regular(f);
00441     G = Cudd_Regular(g);
00442     cacheTag = direction ? DD_BDD_CLIPPING_AND_ABSTRACT_UP_TAG :
00443         DD_BDD_CLIPPING_AND_ABSTRACT_DOWN_TAG;
00444     if (F->ref != 1 || G->ref != 1) {
00445         r = cuddCacheLookup(manager, cacheTag,
00446                             f, g, cube);
00447         if (r != NULL) {
00448             return(r);
00449         }
00450     }
00451 
00452     /* Here we can skip the use of cuddI, because the operands are known
00453     ** to be non-constant.
00454     */
00455     topf = manager->perm[F->index];
00456     topg = manager->perm[G->index];
00457     top = ddMin(topf, topg);
00458     topcube = manager->perm[cube->index];
00459 
00460     if (topcube < top) {
00461         return(cuddBddClipAndAbsRecur(manager, f, g, cuddT(cube),
00462                                       distance, direction));
00463     }
00464     /* Now, topcube >= top. */
00465 
00466     if (topf == top) {
00467         index = F->index;
00468         ft = cuddT(F);
00469         fe = cuddE(F);
00470         if (Cudd_IsComplement(f)) {
00471             ft = Cudd_Not(ft);
00472             fe = Cudd_Not(fe);
00473         }
00474     } else {
00475         index = G->index;
00476         ft = fe = f;
00477     }
00478 
00479     if (topg == top) {
00480         gt = cuddT(G);
00481         ge = cuddE(G);
00482         if (Cudd_IsComplement(g)) {
00483             gt = Cudd_Not(gt);
00484             ge = Cudd_Not(ge);
00485         }
00486     } else {
00487         gt = ge = g;
00488     }
00489 
00490     if (topcube == top) {
00491         Cube = cuddT(cube);
00492     } else {
00493         Cube = cube;
00494     }
00495 
00496     t = cuddBddClipAndAbsRecur(manager, ft, gt, Cube, distance, direction);
00497     if (t == NULL) return(NULL);
00498 
00499     /* Special case: 1 OR anything = 1. Hence, no need to compute
00500     ** the else branch if t is 1.
00501     */
00502     if (t == one && topcube == top) {
00503         if (F->ref != 1 || G->ref != 1)
00504             cuddCacheInsert(manager, cacheTag, f, g, cube, one);
00505         return(one);
00506     }
00507     cuddRef(t);
00508 
00509     e = cuddBddClipAndAbsRecur(manager, fe, ge, Cube, distance, direction);
00510     if (e == NULL) {
00511         Cudd_RecursiveDeref(manager, t);
00512         return(NULL);
00513     }
00514     cuddRef(e);
00515 
00516     if (topcube == top) {       /* abstract */
00517         r = cuddBddClippingAndRecur(manager, Cudd_Not(t), Cudd_Not(e),
00518                                     distance, (direction == 0));
00519         if (r == NULL) {
00520             Cudd_RecursiveDeref(manager, t);
00521             Cudd_RecursiveDeref(manager, e);
00522             return(NULL);
00523         }
00524         r = Cudd_Not(r);
00525         cuddRef(r);
00526         Cudd_RecursiveDeref(manager, t);
00527         Cudd_RecursiveDeref(manager, e);
00528         cuddDeref(r);
00529     } else if (t == e) {
00530         r = t;
00531         cuddDeref(t);
00532         cuddDeref(e);
00533     } else {
00534         if (Cudd_IsComplement(t)) {
00535             r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e));
00536             if (r == NULL) {
00537                 Cudd_RecursiveDeref(manager, t);
00538                 Cudd_RecursiveDeref(manager, e);
00539                 return(NULL);
00540             }
00541             r = Cudd_Not(r);
00542         } else {
00543             r = cuddUniqueInter(manager,(int)index,t,e);
00544             if (r == NULL) {
00545                 Cudd_RecursiveDeref(manager, t);
00546                 Cudd_RecursiveDeref(manager, e);
00547                 return(NULL);
00548             }
00549         }
00550         cuddDeref(e);
00551         cuddDeref(t);
00552     }
00553     if (F->ref != 1 || G->ref != 1)
00554         cuddCacheInsert(manager, cacheTag, f, g, cube, r);
00555     return (r);
00556 
00557 } /* end of cuddBddClipAndAbsRecur */
00558