src/cuBdd/cuddClip.c File Reference

#include "util.h"
#include "cuddInt.h"

Include dependency graph for cuddClip.c:

Functions
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)
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)
Variables
static char rcsid[]	DD_UNUSED = "$Id: cuddClip.c,v 1.8 2004/08/13 18:04:47 fabio Exp $"

Function Documentation

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

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 */

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

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 */

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

00409 00410 00411 00412 00413 00414 00415 00416 00417 00418 00419 00420 00421 00422 00423     } 00424 00425 00426     } 00427 00428 00429     } 00430 00431 00432 00433 00434 00435 00436 00437 00438 00439     } 00440 00441 00442 00443 00444 00445 00446 00447 00448 00449         } 00450     } 00451 00452 00453 00454 00455 00456 00457 00458 00459 00460 00461 00462 00463     } 00464 00465 00466 00467 00468 00469 00470 00471 00472 00473         } 00474 00475 00476 00477     } 00478 00479 00480 00481 00482 00483 00484 00485         } 00486 00487 00488     } 00489 00490 00491 00492 00493 00494     } 00495 00496 00497 00498 00499 00500 00501 00502 00503 00504 00505 00506     } 00507 00508 00509 00510 00511 00512 00513     } 00514 00515 00516 00517 00518 00519 00520 00521 00522 00523         } 00524 00525 00526 00527 00528 00529 00530 00531 00532 00533 00534 00535 00536 00537 00538 00539 00540 00541 00542 00543 00544 00545 00546 00547 00548 00549         } 00550 00551 00552     } 00553 00554 00555 00556 00557

class="fragment">00408 { DdNode *F, *ft, *fe, *G, *gt, *ge; DdNode *one, *zero, *r, *t, *e, *Cube; unsigned int topf, topg, topcube, top, index; ptruint cacheTag; statLine(manager); one = DD_ONE(manager); zero = Cudd_Not(one); /* Terminal cases. */ if (f == zero || g == zero || f == Cudd_Not(g)) return(zero); if (f == one && g == one) return(one); if (cube == one) { return(cuddBddClippingAndRecur(manager, f, g, distance, direction)); if (f == one || f == g) { return (cuddBddExistAbstractRecur(manager, g, cube)); if (g == one) { return (cuddBddExistAbstractRecur(manager, f, cube)); if (distance == 0) return(Cudd_NotCond(one,(direction == 0))); /* At this point f, g, and cube are not constant. */ distance--; /* Check cache. */ if (f > g) { /* Try to increase cache efficiency. */ DdNode *tmp = f; f = g; g = tmp; F = Cudd_Regular(f); G = Cudd_Regular(g); cacheTag = direction ? DD_BDD_CLIPPING_AND_ABSTRACT_UP_TAG : DD_BDD_CLIPPING_AND_ABSTRACT_DOWN_TAG; if (F->ref != 1 || G->ref != 1) { r = cuddCacheLookup(manager, cacheTag, f, g, cube); if (r != NULL) { return(r); /* Here we can skip the use of cuddI, because the operands are known ** to be non-constant. */ topf = manager->perm[F->index]; topg = manager->perm[G->index]; top = ddMin(topf, topg); topcube = manager->perm[cube->index]; if (topcube < top) { return(cuddBddClipAndAbsRecur(manager, f, g, cuddT(cube), distance, direction)); /* Now, topcube >= top. */ if (topf == top) { index = F->index; ft = cuddT(F); fe = cuddE(F); if (Cudd_IsComplement(f)) { ft = Cudd_Not(ft); fe = Cudd_Not(fe); } else { index = G->index; ft = fe = f; if (topg == top) { gt = cuddT(G); ge = cuddE(G); if (Cudd_IsComplement(g)) { gt = Cudd_Not(gt); ge = Cudd_Not(ge); } else { gt = ge = g; if (topcube == top) { Cube = cuddT(cube); } else { Cube = cube; t = cuddBddClipAndAbsRecur(manager, ft, gt, Cube, distance, direction); if (t == NULL) return(NULL); /* Special case: 1 OR anything = 1. Hence, no need to compute ** the else branch if t is 1. */ if (t == one && topcube == top) { if (F->ref != 1 || G->ref != 1) cuddCacheInsert(manager, cacheTag, f, g, cube, one); return(one); cuddRef(t); e = cuddBddClipAndAbsRecur(manager, fe, ge, Cube, distance, direction); if (e == NULL) { Cudd_RecursiveDeref(manager, t); return(NULL); cuddRef(e); if (topcube == top) { /* abstract */ r = cuddBddClippingAndRecur(manager, Cudd_Not(t), Cudd_Not(e), distance, (direction == 0)); if (r == NULL) { Cudd_RecursiveDeref(manager, t); Cudd_RecursiveDeref(manager, e); return(NULL); r = Cudd_Not(r); cuddRef(r); Cudd_RecursiveDeref(manager, t); Cudd_RecursiveDeref(manager, e); cuddDeref(r); } else if (t == e) { r = t; cuddDeref(t); cuddDeref(e); } else { if (Cudd_IsComplement(t)) { r = cuddUniqueInter(manager,(int)index,Cudd_Not(t),Cudd_Not(e)); if (r == NULL) { Cudd_RecursiveDeref(manager, t); Cudd_RecursiveDeref(manager, e); return(NULL); } r = Cudd_Not(r); } else { r = cuddUniqueInter(manager,(int)index,t,e); if (r == NULL) { Cudd_RecursiveDeref(manager, t); Cudd_RecursiveDeref(manager, e); return(NULL); } cuddDeref(e); cuddDeref(t); if (F->ref != 1 || G->ref != 1) cuddCacheInsert(manager, cacheTag, f, g, cube, r); return (r); } /* 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 197 of file cuddClip.c.

00203 {
00204     DdNode *res;
00205 
00206     res = cuddBddClippingAndRecur(dd,f,g,maxDepth,direction);
00207 
00208     return(res);
00209 
00210 } /* 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 229 of file cuddClip.c.

00236 {
00237     DdNode *res;
00238 
00239     res = cuddBddClipAndAbsRecur(dd,f,g,cube,maxDepth,direction);
00240 
00241     return(res);
00242 
00243 } /* end of cuddBddClippingAndAbstract */

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

AutomaticStart

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

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 */

Variable Documentation

char rcsid [] DD_UNUSED = "$Id: cuddClip.c,v 1.8 2004/08/13 18:04:47 fabio 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]

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

src/cuBdd/cuddClip.c File Reference

Functions

Variables

Function Documentation

Variable Documentation