src/bdd/cudd/cuddClip.c File Reference

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

Go to the source code of this file.

Functions

static DdNode
*cuddBddClippingAndRecur 		ARGS ((DdManager *manager, DdNode *f, DdNode *g, int distance, int direction))
static DdNode
*cuddBddClipAndAbsRecur 		ARGS ((DdManager *manager, DdNode *f, DdNode *g, DdNode *cube, int distance, int direction))
DdNode * Cudd_bddClippingAnd (DdManager *dd, DdNode *f, DdNode *g, int maxDepth, int direction)
DdNode * Cudd_bddClippingAndAbstract (DdManager *dd, DdNode *f, DdNode *g, DdNode *cube, int maxDepth, int direction)
DdNode * cuddBddClippingAnd (DdManager *dd, DdNode *f, DdNode *g, int maxDepth, int direction)
DdNode * cuddBddClippingAndAbstract (DdManager *dd, DdNode *f, DdNode *g, DdNode *cube, int maxDepth, int direction)
static DdNode * cuddBddClippingAndRecur (DdManager *manager, DdNode *f, DdNode *g, int distance, int direction)
static DdNode * cuddBddClipAndAbsRecur (DdManager *manager, DdNode *f, DdNode *g, DdNode *cube, int distance, int direction)

Variables

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

Function Documentation

static DdNode* cuddBddClipAndAbsRecur ARGS ( (DdManager *manager, DdNode *f, DdNode *g, DdNode *cube, int distance, int direction)   )  [static]
static DdNode* cuddBddClippingAndRecur ARGS ( (DdManager *manager, DdNode *f, DdNode *g, int distance, int direction)   )  [static]

AutomaticStart

DdNode* Cudd_bddClippingAnd ( DdManager *  dd,
DdNode *  f,
DdNode *  g,
int  maxDepth,
int  direction 
)

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

Synopsis [Approximates the conjunction of two BDDs f and g.]

Description [Approximates the conjunction of two BDDs f and g. Returns a pointer to the resulting BDD if successful; NULL if the intermediate result blows up.]

SideEffects [None]

SeeAlso [Cudd_bddAnd]

Definition at line 98 of file cuddClip.c.

00104 {
00105     DdNode *res;
00106 
00107     do {
00108         dd->reordered = 0;
00109         res = cuddBddClippingAnd(dd,f,g,maxDepth,direction);
00110     } while (dd->reordered == 1);
00111     return(res);
00112 
00113 } /* end of Cudd_bddClippingAnd */

DdNode* Cudd_bddClippingAndAbstract ( DdManager *  dd,
DdNode *  f,
DdNode *  g,
DdNode *  cube,
int  maxDepth,
int  direction 
)

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

Synopsis [Approximates the conjunction of two BDDs f and g and simultaneously abstracts the variables in cube.]

Description [Approximates the conjunction of two BDDs f and g and simultaneously abstracts the variables in cube. The variables are existentially abstracted. Returns a pointer to the resulting BDD if successful; NULL if the intermediate result blows up.]

SideEffects [None]

SeeAlso [Cudd_bddAndAbstract Cudd_bddClippingAnd]

Definition at line 132 of file cuddClip.c.

00139 {
00140     DdNode *res;
00141 
00142     do {
00143         dd->reordered = 0;
00144         res = cuddBddClippingAndAbstract(dd,f,g,cube,maxDepth,direction);
00145     } while (dd->reordered == 1);
00146     return(res);
00147 
00148 } /* end of Cudd_bddClippingAndAbstract */

static DdNode* cuddBddClipAndAbsRecur ( DdManager *  manager,
DdNode *  f,
DdNode *  g,
DdNode *  cube,
int  distance,
int  direction 
) [static]

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

Synopsis [Approximates the AND of two BDDs and simultaneously abstracts the variables in cube.]

Description [Approximates the AND 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_bddClippingAndAbstract]

Definition at line 374 of file cuddClip.c.

00381 {
00382     DdNode *F, *ft, *fe, *G, *gt, *ge;
00383     DdNode *one, *zero, *r, *t, *e, *Cube;
00384     unsigned int topf, topg, topcube, top, index;
00385     ptruint cacheTag;
00386 
00387     statLine(manager);
00388     one = DD_ONE(manager);
00389     zero = Cudd_Not(one);
00390 
00391     /* Terminal cases. */
00392     if (f == zero || g == zero || f == Cudd_Not(g)) return(zero);
00393     if (f == one && g == one)   return(one);
00394     if (cube == one) {
00395         return(cuddBddClippingAndRecur(manager, f, g, distance, direction));
00396     }
00397     if (f == one || f == g) {
00398         return (cuddBddExistAbstractRecur(manager, g, cube));
00399     }
00400     if (g == one) {
00401         return (cuddBddExistAbstractRecur(manager, f, cube));
00402     }
00403     if (distance == 0) return(Cudd_NotCond(one,(direction == 0)));
00404 
00405     /* At this point f, g, and cube are not constant. */
00406     distance--;
00407 
00408     /* Check cache. */
00409     if (f > g) { /* Try to increase cache efficiency. */
00410         DdNode *tmp = f;
00411         f = g; g = tmp;
00412     }
00413     F = Cudd_Regular(f);
00414     G = Cudd_Regular(g);
00415     cacheTag = direction ? DD_BDD_CLIPPING_AND_ABSTRACT_UP_TAG :
00416         DD_BDD_CLIPPING_AND_ABSTRACT_DOWN_TAG;
00417     if (F->ref != 1 || G->ref != 1) {
00418         r = cuddCacheLookup(manager, cacheTag,
00419                             f, g, cube);
00420         if (r != NULL) {
00421             return(r);
00422         }
00423     }
00424 
00425     /* Here we can skip the use of cuddI, because the operands are known
00426     ** to be non-constant.
00427     */
00428     topf = manager->perm[F->index];
00429     topg = manager->perm[G->index];
00430     top = ddMin(topf, topg);
00431     topcube = manager->perm[cube->index];
00432 
00433     if (topcube < top) {
00434         return(cuddBddClipAndAbsRecur(manager, f, g, cuddT(cube),
00435                                       distance, direction));
00436     }
00437     /* Now, topcube >= top. */
00438 
00439     if (topf == top) {
00440         index = F->index;
00441         ft = cuddT(F);
00442         fe = cuddE(F);
00443         if (Cudd_IsComplement(f)) {
00444             ft = Cudd_Not(ft);
00445             fe = Cudd_Not(fe);
00446         }
00447     } else {
00448         index = G->index;
00449         ft = fe = f;
00450     }
00451 
00452     if (topg == top) {
00453         gt = cuddT(G);
00454         ge = cuddE(G);
00455         if (Cudd_IsComplement(g)) {
00456             gt = Cudd_Not(gt);
00457             ge = Cudd_Not(ge);
00458         }
00459     } else {
00460         gt = ge = g;
00461     }
00462 
00463     if (topcube == top) {
00464         Cube = cuddT(cube);
00465     } else {
00466         Cube = cube;
00467     }
00468 
00469     t = cuddBddClipAndAbsRecur(manager, ft, gt, Cube, distance, direction);
00470     if (t == NULL) return(NULL);
00471 
00472     /* Special case: 1 OR anything = 1. Hence, no need to compute
00473     ** the else branch if t is 1.
00474     */
00475     if (t == one && topcube == top) {
00476         if (F->ref != 1 || G->ref != 1)
00477             cuddCacheInsert(manager, cacheTag, f, g, cube, one);
00478         return(one);
00479     }
00480     cuddRef(t);
00481 
00482     e = cuddBddClipAndAbsRecur(manager, fe, ge, Cube, distance, direction);
00483     if (e == NULL) {
00484         Cudd_RecursiveDeref(manager, t);
00485         return(NULL);
00486     }
00487     cuddRef(e);
00488 
00489     if (topcube == top) {       /* abstract */
00490         r = cuddBddClippingAndRecur(manager, Cudd_Not(t), Cudd_Not(e),
00491                                     distance, (direction == 0));
00492         if (r == NULL) {
00493             Cudd_RecursiveDeref(manager, t);
00494             Cudd_RecursiveDeref(manager, e);
00495             return(NULL);
00496         }
00497         r = Cudd_Not(r);
00498         cuddRef(r);
00499         Cudd_RecursiveDeref(manager, t);
00500         Cudd_RecursiveDeref(manager, e);
00501         cuddDeref(r);
00502     } else if (t == e) {
00503         r = t;
00504         cuddDeref(t);
00505         cuddDeref(e);
00506     } else {
00507         if (Cudd_IsComplement(t)) {
00508             r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e));
00509             if (r == NULL) {
00510                 Cudd_RecursiveDeref(manager, t);
00511                 Cudd_RecursiveDeref(manager, e);
00512                 return(NULL);
00513             }
00514             r = Cudd_Not(r);
00515         } else {
00516             r = cuddUniqueInter(manager,(int)index,t,e);
00517             if (r == NULL) {
00518                 Cudd_RecursiveDeref(manager, t);
00519                 Cudd_RecursiveDeref(manager, e);
00520                 return(NULL);
00521             }
00522         }
00523         cuddDeref(e);
00524         cuddDeref(t);
00525     }
00526     if (F->ref != 1 || G->ref != 1)
00527         cuddCacheInsert(manager, cacheTag, f, g, cube, r);
00528     return (r);
00529 
00530 } /* end of cuddBddClipAndAbsRecur */

DdNode* cuddBddClippingAnd ( DdManager *  dd,
DdNode *  f,
DdNode *  g,
int  maxDepth,
int  direction 
)

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

Synopsis [Approximates the conjunction of two BDDs f and g.]

Description [Approximates the conjunction of two BDDs f and g. Returns a pointer to the resulting BDD if successful; NULL if the intermediate result blows up.]

SideEffects [None]

SeeAlso [Cudd_bddClippingAnd]

Definition at line 170 of file cuddClip.c.

00176 {
00177     DdNode *res;
00178 
00179     res = cuddBddClippingAndRecur(dd,f,g,maxDepth,direction);
00180 
00181     return(res);
00182 
00183 } /* end of cuddBddClippingAnd */

DdNode* cuddBddClippingAndAbstract ( DdManager *  dd,
DdNode *  f,
DdNode *  g,
DdNode *  cube,
int  maxDepth,
int  direction 
)

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

Synopsis [Approximates the conjunction of two BDDs f and g and simultaneously abstracts the variables in cube.]

Description [Approximates the conjunction of two BDDs f and g and simultaneously abstracts the variables in cube. Returns a pointer to the resulting BDD if successful; NULL if the intermediate result blows up.]

SideEffects [None]

SeeAlso [Cudd_bddClippingAndAbstract]

Definition at line 202 of file cuddClip.c.

00209 {
00210     DdNode *res;
00211 
00212     res = cuddBddClipAndAbsRecur(dd,f,g,cube,maxDepth,direction);
00213 
00214     return(res);
00215 
00216 } /* end of cuddBddClippingAndAbstract */

static DdNode* cuddBddClippingAndRecur ( DdManager *  manager,
DdNode *  f,
DdNode *  g,
int  distance,
int  direction 
) [static]

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

Synopsis [Implements the recursive step of Cudd_bddClippingAnd.]

Description [Implements the recursive step of Cudd_bddClippingAnd by taking the conjunction of two BDDs. Returns a pointer to the result is successful; NULL otherwise.]

SideEffects [None]

SeeAlso [cuddBddClippingAnd]

Definition at line 238 of file cuddClip.c.

00244 {
00245     DdNode *F, *ft, *fe, *G, *gt, *ge;
00246     DdNode *one, *zero, *r, *t, *e;
00247     unsigned int topf, topg, index;
00248     DdNode *(*cacheOp)(DdManager *, DdNode *, DdNode *);
00249 
00250     statLine(manager);
00251     one = DD_ONE(manager);
00252     zero = Cudd_Not(one);
00253 
00254     /* Terminal cases. */
00255     if (f == zero || g == zero || f == Cudd_Not(g)) return(zero);
00256     if (f == g || g == one) return(f);
00257     if (f == one) return(g);
00258     if (distance == 0) {
00259         /* One last attempt at returning the right result. We sort of
00260         ** cheat by calling Cudd_bddLeq. */
00261         if (Cudd_bddLeq(manager,f,g)) return(f);
00262         if (Cudd_bddLeq(manager,g,f)) return(g);
00263         if (direction == 1) {
00264             if (Cudd_bddLeq(manager,f,Cudd_Not(g)) ||
00265                 Cudd_bddLeq(manager,g,Cudd_Not(f))) return(zero);
00266         }
00267         return(Cudd_NotCond(one,(direction == 0)));
00268     }
00269 
00270     /* At this point f and g are not constant. */
00271     distance--;
00272 
00273     /* Check cache. Try to increase cache efficiency by sorting the
00274     ** pointers. */
00275     if (f > g) {
00276         DdNode *tmp = f;
00277         f = g; g = tmp;
00278     }
00279     F = Cudd_Regular(f);
00280     G = Cudd_Regular(g);
00281     cacheOp = (DdNode *(*)(DdManager *, DdNode *, DdNode *))
00282         (direction ? Cudd_bddClippingAnd : cuddBddClippingAnd);
00283     if (F->ref != 1 || G->ref != 1) {
00284         r = cuddCacheLookup2(manager, cacheOp, f, g);
00285         if (r != NULL) return(r);
00286     }
00287 
00288     /* Here we can skip the use of cuddI, because the operands are known
00289     ** to be non-constant.
00290     */
00291     topf = manager->perm[F->index];
00292     topg = manager->perm[G->index];
00293 
00294     /* Compute cofactors. */
00295     if (topf <= topg) {
00296         index = F->index;
00297         ft = cuddT(F);
00298         fe = cuddE(F);
00299         if (Cudd_IsComplement(f)) {
00300             ft = Cudd_Not(ft);
00301             fe = Cudd_Not(fe);
00302         }
00303     } else {
00304         index = G->index;
00305         ft = fe = f;
00306     }
00307 
00308     if (topg <= topf) {
00309         gt = cuddT(G);
00310         ge = cuddE(G);
00311         if (Cudd_IsComplement(g)) {
00312             gt = Cudd_Not(gt);
00313             ge = Cudd_Not(ge);
00314         }
00315     } else {
00316         gt = ge = g;
00317     }
00318 
00319     t = cuddBddClippingAndRecur(manager, ft, gt, distance, direction);
00320     if (t == NULL) return(NULL);
00321     cuddRef(t);
00322     e = cuddBddClippingAndRecur(manager, fe, ge, distance, direction);
00323     if (e == NULL) {
00324         Cudd_RecursiveDeref(manager, t);
00325         return(NULL);
00326     }
00327     cuddRef(e);
00328 
00329     if (t == e) {
00330         r = t;
00331     } else {
00332         if (Cudd_IsComplement(t)) {
00333             r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e));
00334             if (r == NULL) {
00335                 Cudd_RecursiveDeref(manager, t);
00336                 Cudd_RecursiveDeref(manager, e);
00337                 return(NULL);
00338             }
00339             r = Cudd_Not(r);
00340         } else {
00341             r = cuddUniqueInter(manager,(int)index,t,e);
00342             if (r == NULL) {
00343                 Cudd_RecursiveDeref(manager, t);
00344                 Cudd_RecursiveDeref(manager, e);
00345                 return(NULL);
00346             }
00347         }
00348     }
00349     cuddDeref(e);
00350     cuddDeref(t);
00351     if (F->ref != 1 || G->ref != 1)
00352         cuddCacheInsert2(manager, cacheOp, f, g, r);
00353     return(r);
00354 
00355 } /* end of cuddBddClippingAndRecur */

Variable Documentation

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

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

FileName [cuddClip.c]

PackageName [cudd]

Synopsis [Clipping functions.]

Description [External procedures included in this module:

Internal procedures included in this module:

Static procedures included in this module:

SeeAlso []

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 59 of file cuddClip.c.

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