diff options
Diffstat (limited to 'src/bdd/cudd/cuddPriority.c')
| -rw-r--r-- | src/bdd/cudd/cuddPriority.c | 1475 |
1 files changed, 1475 insertions, 0 deletions
diff --git a/src/bdd/cudd/cuddPriority.c b/src/bdd/cudd/cuddPriority.c new file mode 100644 index 00000000..bb0b83d3 --- /dev/null +++ b/src/bdd/cudd/cuddPriority.c @@ -0,0 +1,1475 @@ +/**CFile*********************************************************************** + + FileName [cuddPriority.c] + + PackageName [cudd] + + Synopsis [Priority functions.] + + Description [External procedures included in this file: + <ul> + <li> Cudd_PrioritySelect() + <li> Cudd_Xgty() + <li> Cudd_Xeqy() + <li> Cudd_addXeqy() + <li> Cudd_Dxygtdxz() + <li> Cudd_Dxygtdyz() + <li> Cudd_CProjection() + <li> Cudd_addHamming() + <li> Cudd_MinHammingDist() + <li> Cudd_bddClosestCube() + </ul> + Internal procedures included in this module: + <ul> + <li> cuddCProjectionRecur() + <li> cuddBddClosestCube() + </ul> + Static procedures included in this module: + <ul> + <li> cuddMinHammingDistRecur() + <li> separateCube() + <li> createResult() + </ul> + ] + + 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.] + +******************************************************************************/ + +#include "util.h" +#include "cuddInt.h" + + +/*---------------------------------------------------------------------------*/ +/* Constant declarations */ +/*---------------------------------------------------------------------------*/ + + +/*---------------------------------------------------------------------------*/ +/* Stucture declarations */ +/*---------------------------------------------------------------------------*/ + + +/*---------------------------------------------------------------------------*/ +/* Type declarations */ +/*---------------------------------------------------------------------------*/ + + +/*---------------------------------------------------------------------------*/ +/* Variable declarations */ +/*---------------------------------------------------------------------------*/ + +#ifndef lint +static char rcsid[] DD_UNUSED = "$Id: cuddPriority.c,v 1.1.1.1 2003/02/24 22:23:52 wjiang Exp $"; +#endif + +/*---------------------------------------------------------------------------*/ +/* Macro declarations */ +/*---------------------------------------------------------------------------*/ + + +/**AutomaticStart*************************************************************/ + +/*---------------------------------------------------------------------------*/ +/* Static function prototypes */ +/*---------------------------------------------------------------------------*/ +static int cuddMinHammingDistRecur ARGS((DdNode * f, int *minterm, DdHashTable * table, int upperBound)); +static DdNode * separateCube ARGS((DdManager *dd, DdNode *f, CUDD_VALUE_TYPE *distance)); +static DdNode * createResult ARGS((DdManager *dd, unsigned int index, unsigned int phase, DdNode *cube, CUDD_VALUE_TYPE distance)); + +/**AutomaticEnd***************************************************************/ + + +/*---------------------------------------------------------------------------*/ +/* Definition of exported functions */ +/*---------------------------------------------------------------------------*/ + + +/**Function******************************************************************** + + Synopsis [Selects pairs from R using a priority function.] + + Description [Selects pairs from a relation R(x,y) (given as a BDD) + in such a way that a given x appears in one pair only. Uses a + priority function to determine which y should be paired to a given x. + Cudd_PrioritySelect returns a pointer to + the selected function if successful; NULL otherwise. + Three of the arguments--x, y, and z--are vectors of BDD variables. + The first two are the variables on which R depends. The third vectore + is a vector of auxiliary variables, used during the computation. This + vector is optional. If a NULL value is passed instead, + Cudd_PrioritySelect will create the working variables on the fly. + The sizes of x and y (and z if it is not NULL) should equal n. + The priority function Pi can be passed as a BDD, or can be built by + Cudd_PrioritySelect. If NULL is passed instead of a DdNode *, + parameter Pifunc is used by Cudd_PrioritySelect to build a BDD for the + priority function. (Pifunc is a pointer to a C function.) If Pi is not + NULL, then Pifunc is ignored. Pifunc should have the same interface as + the standard priority functions (e.g., Cudd_Dxygtdxz). + Cudd_PrioritySelect and Cudd_CProjection can sometimes be used + interchangeably. Specifically, calling Cudd_PrioritySelect with + Cudd_Xgty as Pifunc produces the same result as calling + Cudd_CProjection with the all-zero minterm as reference minterm. + However, depending on the application, one or the other may be + preferable: + <ul> + <li> When extracting representatives from an equivalence relation, + Cudd_CProjection has the advantage of nor requiring the auxiliary + variables. + <li> When computing matchings in general bipartite graphs, + Cudd_PrioritySelect normally obtains better results because it can use + more powerful matching schemes (e.g., Cudd_Dxygtdxz). + </ul> + ] + + SideEffects [If called with z == NULL, will create new variables in + the manager.] + + SeeAlso [Cudd_Dxygtdxz Cudd_Dxygtdyz Cudd_Xgty + Cudd_bddAdjPermuteX Cudd_CProjection] + +******************************************************************************/ +DdNode * +Cudd_PrioritySelect( + DdManager * dd /* manager */, + DdNode * R /* BDD of the relation */, + DdNode ** x /* array of x variables */, + DdNode ** y /* array of y variables */, + DdNode ** z /* array of z variables (optional: may be NULL) */, + DdNode * Pi /* BDD of the priority function (optional: may be NULL) */, + int n /* size of x, y, and z */, + DdNode * (*Pifunc)(DdManager *, int, DdNode **, DdNode **, DdNode **) /* function used to build Pi if it is NULL */) +{ + DdNode *res = NULL; + DdNode *zcube = NULL; + DdNode *Rxz, *Q; + int createdZ = 0; + int createdPi = 0; + int i; + + /* Create z variables if needed. */ + if (z == NULL) { + if (Pi != NULL) return(NULL); + z = ALLOC(DdNode *,n); + if (z == NULL) { + dd->errorCode = CUDD_MEMORY_OUT; + return(NULL); + } + createdZ = 1; + for (i = 0; i < n; i++) { + if (dd->size >= (int) CUDD_MAXINDEX - 1) goto endgame; + z[i] = cuddUniqueInter(dd,dd->size,dd->one,Cudd_Not(dd->one)); + if (z[i] == NULL) goto endgame; + } + } + + /* Create priority function BDD if needed. */ + if (Pi == NULL) { + Pi = Pifunc(dd,n,x,y,z); + if (Pi == NULL) goto endgame; + createdPi = 1; + cuddRef(Pi); + } + + /* Initialize abstraction cube. */ + zcube = DD_ONE(dd); + cuddRef(zcube); + for (i = n - 1; i >= 0; i--) { + DdNode *tmpp; + tmpp = Cudd_bddAnd(dd,z[i],zcube); + if (tmpp == NULL) goto endgame; + cuddRef(tmpp); + Cudd_RecursiveDeref(dd,zcube); + zcube = tmpp; + } + + /* Compute subset of (x,y) pairs. */ + Rxz = Cudd_bddSwapVariables(dd,R,y,z,n); + if (Rxz == NULL) goto endgame; + cuddRef(Rxz); + Q = Cudd_bddAndAbstract(dd,Rxz,Pi,zcube); + if (Q == NULL) { + Cudd_RecursiveDeref(dd,Rxz); + goto endgame; + } + cuddRef(Q); + Cudd_RecursiveDeref(dd,Rxz); + res = Cudd_bddAnd(dd,R,Cudd_Not(Q)); + if (res == NULL) { + Cudd_RecursiveDeref(dd,Q); + goto endgame; + } + cuddRef(res); + Cudd_RecursiveDeref(dd,Q); + +endgame: + if (zcube != NULL) Cudd_RecursiveDeref(dd,zcube); + if (createdZ) { + FREE(z); + } + if (createdPi) { + Cudd_RecursiveDeref(dd,Pi); + } + if (res != NULL) cuddDeref(res); + return(res); + +} /* Cudd_PrioritySelect */ + + +/**Function******************************************************************** + + Synopsis [Generates a BDD for the function x > y.] + + Description [This function generates a BDD for the function x > y. + Both x and y are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\] and + y\[0\] y\[1\] ... y\[N-1\], with 0 the most significant bit. + The BDD is built bottom-up. + It has 3*N-1 internal nodes, if the variables are ordered as follows: + x\[0\] y\[0\] x\[1\] y\[1\] ... x\[N-1\] y\[N-1\]. + Argument z is not used by Cudd_Xgty: it is included to make it + call-compatible to Cudd_Dxygtdxz and Cudd_Dxygtdyz.] + + SideEffects [None] + + SeeAlso [Cudd_PrioritySelect Cudd_Dxygtdxz Cudd_Dxygtdyz] + +******************************************************************************/ +DdNode * +Cudd_Xgty( + DdManager * dd /* DD manager */, + int N /* number of x and y variables */, + DdNode ** z /* array of z variables: unused */, + DdNode ** x /* array of x variables */, + DdNode ** y /* array of y variables */) +{ + DdNode *u, *v, *w; + int i; + + /* Build bottom part of BDD outside loop. */ + u = Cudd_bddAnd(dd, x[N-1], Cudd_Not(y[N-1])); + if (u == NULL) return(NULL); + cuddRef(u); + + /* Loop to build the rest of the BDD. */ + for (i = N-2; i >= 0; i--) { + v = Cudd_bddAnd(dd, y[i], Cudd_Not(u)); + if (v == NULL) { + Cudd_RecursiveDeref(dd, u); + return(NULL); + } + cuddRef(v); + w = Cudd_bddAnd(dd, Cudd_Not(y[i]), u); + if (w == NULL) { + Cudd_RecursiveDeref(dd, u); + Cudd_RecursiveDeref(dd, v); + return(NULL); + } + cuddRef(w); + Cudd_RecursiveDeref(dd, u); + u = Cudd_bddIte(dd, x[i], Cudd_Not(v), w); + if (u == NULL) { + Cudd_RecursiveDeref(dd, v); + Cudd_RecursiveDeref(dd, w); + return(NULL); + } + cuddRef(u); + Cudd_RecursiveDeref(dd, v); + Cudd_RecursiveDeref(dd, w); + + } + cuddDeref(u); + return(u); + +} /* end of Cudd_Xgty */ + + +/**Function******************************************************************** + + Synopsis [Generates a BDD for the function x==y.] + + Description [This function generates a BDD for the function x==y. + Both x and y are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\] and + y\[0\] y\[1\] ... y\[N-1\], with 0 the most significant bit. + The BDD is built bottom-up. + It has 3*N-1 internal nodes, if the variables are ordered as follows: + x\[0\] y\[0\] x\[1\] y\[1\] ... x\[N-1\] y\[N-1\]. ] + + SideEffects [None] + + SeeAlso [Cudd_addXeqy] + +******************************************************************************/ +DdNode * +Cudd_Xeqy( + DdManager * dd /* DD manager */, + int N /* number of x and y variables */, + DdNode ** x /* array of x variables */, + DdNode ** y /* array of y variables */) +{ + DdNode *u, *v, *w; + int i; + + /* Build bottom part of BDD outside loop. */ + u = Cudd_bddIte(dd, x[N-1], y[N-1], Cudd_Not(y[N-1])); + if (u == NULL) return(NULL); + cuddRef(u); + + /* Loop to build the rest of the BDD. */ + for (i = N-2; i >= 0; i--) { + v = Cudd_bddAnd(dd, y[i], u); + if (v == NULL) { + Cudd_RecursiveDeref(dd, u); + return(NULL); + } + cuddRef(v); + w = Cudd_bddAnd(dd, Cudd_Not(y[i]), u); + if (w == NULL) { + Cudd_RecursiveDeref(dd, u); + Cudd_RecursiveDeref(dd, v); + return(NULL); + } + cuddRef(w); + Cudd_RecursiveDeref(dd, u); + u = Cudd_bddIte(dd, x[i], v, w); + if (u == NULL) { + Cudd_RecursiveDeref(dd, v); + Cudd_RecursiveDeref(dd, w); + return(NULL); + } + cuddRef(u); + Cudd_RecursiveDeref(dd, v); + Cudd_RecursiveDeref(dd, w); + } + cuddDeref(u); + return(u); + +} /* end of Cudd_Xeqy */ + + +/**Function******************************************************************** + + Synopsis [Generates an ADD for the function x==y.] + + Description [This function generates an ADD for the function x==y. + Both x and y are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\] and + y\[0\] y\[1\] ... y\[N-1\], with 0 the most significant bit. + The ADD is built bottom-up. + It has 3*N-1 internal nodes, if the variables are ordered as follows: + x\[0\] y\[0\] x\[1\] y\[1\] ... x\[N-1\] y\[N-1\]. ] + + SideEffects [None] + + SeeAlso [Cudd_Xeqy] + +******************************************************************************/ +DdNode * +Cudd_addXeqy( + DdManager * dd /* DD manager */, + int N /* number of x and y variables */, + DdNode ** x /* array of x variables */, + DdNode ** y /* array of y variables */) +{ + DdNode *one, *zero; + DdNode *u, *v, *w; + int i; + + one = DD_ONE(dd); + zero = DD_ZERO(dd); + + /* Build bottom part of ADD outside loop. */ + v = Cudd_addIte(dd, y[N-1], one, zero); + if (v == NULL) return(NULL); + cuddRef(v); + w = Cudd_addIte(dd, y[N-1], zero, one); + if (w == NULL) { + Cudd_RecursiveDeref(dd, v); + return(NULL); + } + cuddRef(w); + u = Cudd_addIte(dd, x[N-1], v, w); + if (w == NULL) { + Cudd_RecursiveDeref(dd, v); + Cudd_RecursiveDeref(dd, w); + return(NULL); + } + cuddRef(u); + Cudd_RecursiveDeref(dd, v); + Cudd_RecursiveDeref(dd, w); + + /* Loop to build the rest of the ADD. */ + for (i = N-2; i >= 0; i--) { + v = Cudd_addIte(dd, y[i], u, zero); + if (v == NULL) { + Cudd_RecursiveDeref(dd, u); + return(NULL); + } + cuddRef(v); + w = Cudd_addIte(dd, y[i], zero, u); + if (w == NULL) { + Cudd_RecursiveDeref(dd, u); + Cudd_RecursiveDeref(dd, v); + return(NULL); + } + cuddRef(w); + Cudd_RecursiveDeref(dd, u); + u = Cudd_addIte(dd, x[i], v, w); + if (w == NULL) { + Cudd_RecursiveDeref(dd, v); + Cudd_RecursiveDeref(dd, w); + return(NULL); + } + cuddRef(u); + Cudd_RecursiveDeref(dd, v); + Cudd_RecursiveDeref(dd, w); + } + cuddDeref(u); + return(u); + +} /* end of Cudd_addXeqy */ + + +/**Function******************************************************************** + + Synopsis [Generates a BDD for the function d(x,y) > d(x,z).] + + Description [This function generates a BDD for the function d(x,y) + > d(x,z); + x, y, and z are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\], + y\[0\] y\[1\] ... y\[N-1\], and z\[0\] z\[1\] ... z\[N-1\], + with 0 the most significant bit. + The distance d(x,y) is defined as: + \sum_{i=0}^{N-1}(|x_i - y_i| \cdot 2^{N-i-1}). + The BDD is built bottom-up. + It has 7*N-3 internal nodes, if the variables are ordered as follows: + x\[0\] y\[0\] z\[0\] x\[1\] y\[1\] z\[1\] ... x\[N-1\] y\[N-1\] z\[N-1\]. ] + + SideEffects [None] + + SeeAlso [Cudd_PrioritySelect Cudd_Dxygtdyz Cudd_Xgty Cudd_bddAdjPermuteX] + +******************************************************************************/ +DdNode * +Cudd_Dxygtdxz( + DdManager * dd /* DD manager */, + int N /* number of x, y, and z variables */, + DdNode ** x /* array of x variables */, + DdNode ** y /* array of y variables */, + DdNode ** z /* array of z variables */) +{ + DdNode *one, *zero; + DdNode *z1, *z2, *z3, *z4, *y1_, *y2, *x1; + int i; + + one = DD_ONE(dd); + zero = Cudd_Not(one); + + /* Build bottom part of BDD outside loop. */ + y1_ = Cudd_bddIte(dd, y[N-1], one, Cudd_Not(z[N-1])); + if (y1_ == NULL) return(NULL); + cuddRef(y1_); + y2 = Cudd_bddIte(dd, y[N-1], z[N-1], one); + if (y2 == NULL) { + Cudd_RecursiveDeref(dd, y1_); + return(NULL); + } + cuddRef(y2); + x1 = Cudd_bddIte(dd, x[N-1], y1_, y2); + if (x1 == NULL) { + Cudd_RecursiveDeref(dd, y1_); + Cudd_RecursiveDeref(dd, y2); + return(NULL); + } + cuddRef(x1); + Cudd_RecursiveDeref(dd, y1_); + Cudd_RecursiveDeref(dd, y2); + + /* Loop to build the rest of the BDD. */ + for (i = N-2; i >= 0; i--) { + z1 = Cudd_bddIte(dd, z[i], one, Cudd_Not(x1)); + if (z1 == NULL) { + Cudd_RecursiveDeref(dd, x1); + return(NULL); + } + cuddRef(z1); + z2 = Cudd_bddIte(dd, z[i], x1, one); + if (z2 == NULL) { + Cudd_RecursiveDeref(dd, x1); + Cudd_RecursiveDeref(dd, z1); + return(NULL); + } + cuddRef(z2); + z3 = Cudd_bddIte(dd, z[i], one, x1); + if (z3 == NULL) { + Cudd_RecursiveDeref(dd, x1); + Cudd_RecursiveDeref(dd, z1); + Cudd_RecursiveDeref(dd, z2); + return(NULL); + } + cuddRef(z3); + z4 = Cudd_bddIte(dd, z[i], x1, zero); + if (z4 == NULL) { + Cudd_RecursiveDeref(dd, x1); + Cudd_RecursiveDeref(dd, z1); + Cudd_RecursiveDeref(dd, z2); + Cudd_RecursiveDeref(dd, z3); + return(NULL); + } + cuddRef(z4); + Cudd_RecursiveDeref(dd, x1); + y1_ = Cudd_bddIte(dd, y[i], z2, Cudd_Not(z1)); + if (y1_ == NULL) { + Cudd_RecursiveDeref(dd, z1); + Cudd_RecursiveDeref(dd, z2); + Cudd_RecursiveDeref(dd, z3); + Cudd_RecursiveDeref(dd, z4); + return(NULL); + } + cuddRef(y1_); + y2 = Cudd_bddIte(dd, y[i], z4, z3); + if (y2 == NULL) { + Cudd_RecursiveDeref(dd, z1); + Cudd_RecursiveDeref(dd, z2); + Cudd_RecursiveDeref(dd, z3); + Cudd_RecursiveDeref(dd, z4); + Cudd_RecursiveDeref(dd, y1_); + return(NULL); + } + cuddRef(y2); + Cudd_RecursiveDeref(dd, z1); + Cudd_RecursiveDeref(dd, z2); + Cudd_RecursiveDeref(dd, z3); + Cudd_RecursiveDeref(dd, z4); + x1 = Cudd_bddIte(dd, x[i], y1_, y2); + if (x1 == NULL) { + Cudd_RecursiveDeref(dd, y1_); + Cudd_RecursiveDeref(dd, y2); + return(NULL); + } + cuddRef(x1); + Cudd_RecursiveDeref(dd, y1_); + Cudd_RecursiveDeref(dd, y2); + } + cuddDeref(x1); + return(Cudd_Not(x1)); + +} /* end of Cudd_Dxygtdxz */ + + +/**Function******************************************************************** + + Synopsis [Generates a BDD for the function d(x,y) > d(y,z).] + + Description [This function generates a BDD for the function d(x,y) + > d(y,z); + x, y, and z are N-bit numbers, x\[0\] x\[1\] ... x\[N-1\], + y\[0\] y\[1\] ... y\[N-1\], and z\[0\] z\[1\] ... z\[N-1\], + with 0 the most significant bit. + The distance d(x,y) is defined as: + \sum_{i=0}^{N-1}(|x_i - y_i| \cdot 2^{N-i-1}). + The BDD is built bottom-up. + It has 7*N-3 internal nodes, if the variables are ordered as follows: + x\[0\] y\[0\] z\[0\] x\[1\] y\[1\] z\[1\] ... x\[N-1\] y\[N-1\] z\[N-1\]. ] + + SideEffects [None] + + SeeAlso [Cudd_PrioritySelect Cudd_Dxygtdxz Cudd_Xgty Cudd_bddAdjPermuteX] + +******************************************************************************/ +DdNode * +Cudd_Dxygtdyz( + DdManager * dd /* DD manager */, + int N /* number of x, y, and z variables */, + DdNode ** x /* array of x variables */, + DdNode ** y /* array of y variables */, + DdNode ** z /* array of z variables */) +{ + DdNode *one, *zero; + DdNode *z1, *z2, *z3, *z4, *y1_, *y2, *x1; + int i; + + one = DD_ONE(dd); + zero = Cudd_Not(one); + + /* Build bottom part of BDD outside loop. */ + y1_ = Cudd_bddIte(dd, y[N-1], one, z[N-1]); + if (y1_ == NULL) return(NULL); + cuddRef(y1_); + y2 = Cudd_bddIte(dd, y[N-1], z[N-1], zero); + if (y2 == NULL) { + Cudd_RecursiveDeref(dd, y1_); + return(NULL); + } + cuddRef(y2); + x1 = Cudd_bddIte(dd, x[N-1], y1_, Cudd_Not(y2)); + if (x1 == NULL) { + Cudd_RecursiveDeref(dd, y1_); + Cudd_RecursiveDeref(dd, y2); + return(NULL); + } + cuddRef(x1); + Cudd_RecursiveDeref(dd, y1_); + Cudd_RecursiveDeref(dd, y2); + + /* Loop to build the rest of the BDD. */ + for (i = N-2; i >= 0; i--) { + z1 = Cudd_bddIte(dd, z[i], x1, zero); + if (z1 == NULL) { + Cudd_RecursiveDeref(dd, x1); + return(NULL); + } + cuddRef(z1); + z2 = Cudd_bddIte(dd, z[i], x1, one); + if (z2 == NULL) { + Cudd_RecursiveDeref(dd, x1); + Cudd_RecursiveDeref(dd, z1); + return(NULL); + } + cuddRef(z2); + z3 = Cudd_bddIte(dd, z[i], one, x1); + if (z3 == NULL) { + Cudd_RecursiveDeref(dd, x1); + Cudd_RecursiveDeref(dd, z1); + Cudd_RecursiveDeref(dd, z2); + return(NULL); + } + cuddRef(z3); + z4 = Cudd_bddIte(dd, z[i], one, Cudd_Not(x1)); + if (z4 == NULL) { + Cudd_RecursiveDeref(dd, x1); + Cudd_RecursiveDeref(dd, z1); + Cudd_RecursiveDeref(dd, z2); + Cudd_RecursiveDeref(dd, z3); + return(NULL); + } + cuddRef(z4); + Cudd_RecursiveDeref(dd, x1); + y1_ = Cudd_bddIte(dd, y[i], z2, z1); + if (y1_ == NULL) { + Cudd_RecursiveDeref(dd, z1); + Cudd_RecursiveDeref(dd, z2); + Cudd_RecursiveDeref(dd, z3); + Cudd_RecursiveDeref(dd, z4); + return(NULL); + } + cuddRef(y1_); + y2 = Cudd_bddIte(dd, y[i], z4, Cudd_Not(z3)); + if (y2 == NULL) { + Cudd_RecursiveDeref(dd, z1); + Cudd_RecursiveDeref(dd, z2); + Cudd_RecursiveDeref(dd, z3); + Cudd_RecursiveDeref(dd, z4); + Cudd_RecursiveDeref(dd, y1_); + return(NULL); + } + cuddRef(y2); + Cudd_RecursiveDeref(dd, z1); + Cudd_RecursiveDeref(dd, z2); + Cudd_RecursiveDeref(dd, z3); + Cudd_RecursiveDeref(dd, z4); + x1 = Cudd_bddIte(dd, x[i], y1_, Cudd_Not(y2)); + if (x1 == NULL) { + Cudd_RecursiveDeref(dd, y1_); + Cudd_RecursiveDeref(dd, y2); + return(NULL); + } + cuddRef(x1); + Cudd_RecursiveDeref(dd, y1_); + Cudd_RecursiveDeref(dd, y2); + } + cuddDeref(x1); + return(Cudd_Not(x1)); + +} /* end of Cudd_Dxygtdyz */ + + +/**Function******************************************************************** + + Synopsis [Computes the compatible projection of R w.r.t. cube Y.] + + Description [Computes the compatible projection of relation R with + respect to cube Y. Returns a pointer to the c-projection if + successful; NULL otherwise. For a comparison between Cudd_CProjection + and Cudd_PrioritySelect, see the documentation of the latter.] + + SideEffects [None] + + SeeAlso [Cudd_PrioritySelect] + +******************************************************************************/ +DdNode * +Cudd_CProjection( + DdManager * dd, + DdNode * R, + DdNode * Y) +{ + DdNode *res; + DdNode *support; + + if (cuddCheckCube(dd,Y) == 0) { + (void) fprintf(dd->err, + "Error: The third argument of Cudd_CProjection should be a cube\n"); + dd->errorCode = CUDD_INVALID_ARG; + return(NULL); + } + + /* Compute the support of Y, which is used by the abstraction step + ** in cuddCProjectionRecur. + */ + support = Cudd_Support(dd,Y); + if (support == NULL) return(NULL); + cuddRef(support); + + do { + dd->reordered = 0; + res = cuddCProjectionRecur(dd,R,Y,support); + } while (dd->reordered == 1); + + if (res == NULL) { + Cudd_RecursiveDeref(dd,support); + return(NULL); + } + cuddRef(res); + Cudd_RecursiveDeref(dd,support); + cuddDeref(res); + + return(res); + +} /* end of Cudd_CProjection */ + + +/**Function******************************************************************** + + Synopsis [Computes the Hamming distance ADD.] + + Description [Computes the Hamming distance ADD. Returns an ADD that + gives the Hamming distance between its two arguments if successful; + NULL otherwise. The two vectors xVars and yVars identify the variables + that form the two arguments.] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +DdNode * +Cudd_addHamming( + DdManager * dd, + DdNode ** xVars, + DdNode ** yVars, + int nVars) +{ + DdNode *result,*tempBdd; + DdNode *tempAdd,*temp; + int i; + + result = DD_ZERO(dd); + cuddRef(result); + + for (i = 0; i < nVars; i++) { + tempBdd = Cudd_bddIte(dd,xVars[i],Cudd_Not(yVars[i]),yVars[i]); + if (tempBdd == NULL) { + Cudd_RecursiveDeref(dd,result); + return(NULL); + } + cuddRef(tempBdd); + tempAdd = Cudd_BddToAdd(dd,tempBdd); + if (tempAdd == NULL) { + Cudd_RecursiveDeref(dd,tempBdd); + Cudd_RecursiveDeref(dd,result); + return(NULL); + } + cuddRef(tempAdd); + Cudd_RecursiveDeref(dd,tempBdd); + temp = Cudd_addApply(dd,Cudd_addPlus,tempAdd,result); + if (temp == NULL) { + Cudd_RecursiveDeref(dd,tempAdd); + Cudd_RecursiveDeref(dd,result); + return(NULL); + } + cuddRef(temp); + Cudd_RecursiveDeref(dd,tempAdd); + Cudd_RecursiveDeref(dd,result); + result = temp; + } + + cuddDeref(result); + return(result); + +} /* end of Cudd_addHamming */ + + +/**Function******************************************************************** + + Synopsis [Returns the minimum Hamming distance between f and minterm.] + + Description [Returns the minimum Hamming distance between the + minterms of a function f and a reference minterm. The function is + given as a BDD; the minterm is given as an array of integers, one + for each variable in the manager. Returns the minimum distance if + it is less than the upper bound; the upper bound if the minimum + distance is at least as large; CUDD_OUT_OF_MEM in case of failure.] + + SideEffects [None] + + SeeAlso [Cudd_addHamming Cudd_bddClosestCube] + +******************************************************************************/ +int +Cudd_MinHammingDist( + DdManager *dd /* DD manager */, + DdNode *f /* function to examine */, + int *minterm /* reference minterm */, + int upperBound /* distance above which an approximate answer is OK */) +{ + DdHashTable *table; + CUDD_VALUE_TYPE epsilon; + int res; + + table = cuddHashTableInit(dd,1,2); + if (table == NULL) { + return(CUDD_OUT_OF_MEM); + } + epsilon = Cudd_ReadEpsilon(dd); + Cudd_SetEpsilon(dd,(CUDD_VALUE_TYPE)0.0); + res = cuddMinHammingDistRecur(f,minterm,table,upperBound); + cuddHashTableQuit(table); + Cudd_SetEpsilon(dd,epsilon); + + return(res); + +} /* end of Cudd_MinHammingDist */ + + +/**Function******************************************************************** + + Synopsis [Finds a cube of f at minimum Hamming distance from g.] + + Description [Finds a cube of f at minimum Hamming distance from the + minterms of g. All the minterms of the cube are at the minimum + distance. If the distance is 0, the cube belongs to the + intersection of f and g. Returns the cube if successful; NULL + otherwise.] + + SideEffects [The distance is returned as a side effect.] + + SeeAlso [Cudd_MinHammingDist] + +******************************************************************************/ +DdNode * +Cudd_bddClosestCube( + DdManager *dd, + DdNode * f, + DdNode *g, + int *distance) +{ + DdNode *res, *acube; + CUDD_VALUE_TYPE rdist; + + /* Compute the cube and distance as a single ADD. */ + do { + dd->reordered = 0; + res = cuddBddClosestCube(dd,f,g,CUDD_CONST_INDEX + 1.0); + } while (dd->reordered == 1); + if (res == NULL) return(NULL); + cuddRef(res); + + /* Unpack distance and cube. */ + do { + dd->reordered = 0; + acube = separateCube(dd, res, &rdist); + } while (dd->reordered == 1); + if (acube == NULL) { + Cudd_RecursiveDeref(dd, res); + return(NULL); + } + cuddRef(acube); + Cudd_RecursiveDeref(dd, res); + + /* Convert cube from ADD to BDD. */ + do { + dd->reordered = 0; + res = cuddAddBddDoPattern(dd, acube); + } while (dd->reordered == 1); + if (res == NULL) { + Cudd_RecursiveDeref(dd, acube); + return(NULL); + } + cuddRef(res); + Cudd_RecursiveDeref(dd, acube); + + *distance = (int) rdist; + cuddDeref(res); + return(res); + +} /* end of Cudd_bddClosestCube */ + + +/*---------------------------------------------------------------------------*/ +/* Definition of internal functions */ +/*---------------------------------------------------------------------------*/ + + +/**Function******************************************************************** + + Synopsis [Performs the recursive step of Cudd_CProjection.] + + Description [Performs the recursive step of Cudd_CProjection. Returns + the projection if successful; NULL otherwise.] + + SideEffects [None] + + SeeAlso [Cudd_CProjection] + +******************************************************************************/ +DdNode * +cuddCProjectionRecur( + DdManager * dd, + DdNode * R, + DdNode * Y, + DdNode * Ysupp) +{ + DdNode *res, *res1, *res2, *resA; + DdNode *r, *y, *RT, *RE, *YT, *YE, *Yrest, *Ra, *Ran, *Gamma, *Alpha; + unsigned int topR, topY, top, index; + DdNode *one = DD_ONE(dd); + + statLine(dd); + if (Y == one) return(R); + +#ifdef DD_DEBUG + assert(!Cudd_IsConstant(Y)); +#endif + + if (R == Cudd_Not(one)) return(R); + + res = cuddCacheLookup2(dd, Cudd_CProjection, R, Y); + if (res != NULL) return(res); + + r = Cudd_Regular(R); + topR = cuddI(dd,r->index); + y = Cudd_Regular(Y); + topY = cuddI(dd,y->index); + + top = ddMin(topR, topY); + + /* Compute the cofactors of R */ + if (topR == top) { + index = r->index; + RT = cuddT(r); + RE = cuddE(r); + if (r != R) { + RT = Cudd_Not(RT); RE = Cudd_Not(RE); + } + } else { + RT = RE = R; + } + + if (topY > top) { + /* Y does not depend on the current top variable. + ** We just need to compute the results on the two cofactors of R + ** and make them the children of a node labeled r->index. + */ + res1 = cuddCProjectionRecur(dd,RT,Y,Ysupp); + if (res1 == NULL) return(NULL); + cuddRef(res1); + res2 = cuddCProjectionRecur(dd,RE,Y,Ysupp); + if (res2 == NULL) { + Cudd_RecursiveDeref(dd,res1); + return(NULL); + } + cuddRef(res2); + res = cuddBddIteRecur(dd, dd->vars[index], res1, res2); + if (res == NULL) { + Cudd_RecursiveDeref(dd,res1); + Cudd_RecursiveDeref(dd,res2); + return(NULL); + } + /* If we have reached this point, res1 and res2 are now + ** incorporated in res. cuddDeref is therefore sufficient. + */ + cuddDeref(res1); + cuddDeref(res2); + } else { + /* Compute the cofactors of Y */ + index = y->index; + YT = cuddT(y); + YE = cuddE(y); + if (y != Y) { + YT = Cudd_Not(YT); YE = Cudd_Not(YE); + } + if (YT == Cudd_Not(one)) { + Alpha = Cudd_Not(dd->vars[index]); + Yrest = YE; + Ra = RE; + Ran = RT; + } else { + Alpha = dd->vars[index]; + Yrest = YT; + Ra = RT; + Ran = RE; + } + Gamma = cuddBddExistAbstractRecur(dd,Ra,cuddT(Ysupp)); + if (Gamma == NULL) return(NULL); + if (Gamma == one) { + res1 = cuddCProjectionRecur(dd,Ra,Yrest,cuddT(Ysupp)); + if (res1 == NULL) return(NULL); + cuddRef(res1); + res = cuddBddAndRecur(dd, Alpha, res1); + if (res == NULL) { + Cudd_RecursiveDeref(dd,res1); + return(NULL); + } + cuddDeref(res1); + } else if (Gamma == Cudd_Not(one)) { + res1 = cuddCProjectionRecur(dd,Ran,Yrest,cuddT(Ysupp)); + if (res1 == NULL) return(NULL); + cuddRef(res1); + res = cuddBddAndRecur(dd, Cudd_Not(Alpha), res1); + if (res == NULL) { + Cudd_RecursiveDeref(dd,res1); + return(NULL); + } + cuddDeref(res1); + } else { + cuddRef(Gamma); + resA = cuddCProjectionRecur(dd,Ran,Yrest,cuddT(Ysupp)); + if (resA == NULL) { + Cudd_RecursiveDeref(dd,Gamma); + return(NULL); + } + cuddRef(resA); + res2 = cuddBddAndRecur(dd, Cudd_Not(Gamma), resA); + if (res2 == NULL) { + Cudd_RecursiveDeref(dd,Gamma); + Cudd_RecursiveDeref(dd,resA); + return(NULL); + } + cuddRef(res2); + Cudd_RecursiveDeref(dd,Gamma); + Cudd_RecursiveDeref(dd,resA); + res1 = cuddCProjectionRecur(dd,Ra,Yrest,cuddT(Ysupp)); + if (res1 == NULL) { + Cudd_RecursiveDeref(dd,res2); + return(NULL); + } + cuddRef(res1); + res = cuddBddIteRecur(dd, Alpha, res1, res2); + if (res == NULL) { + Cudd_RecursiveDeref(dd,res1); + Cudd_RecursiveDeref(dd,res2); + return(NULL); + } + cuddDeref(res1); + cuddDeref(res2); + } + } + + cuddCacheInsert2(dd,Cudd_CProjection,R,Y,res); + + return(res); + +} /* end of cuddCProjectionRecur */ + + +/**Function******************************************************************** + + Synopsis [Performs the recursive step of Cudd_bddClosestCube.] + + Description [Performs the recursive step of Cudd_bddClosestCube. + Returns the cube if succesful; NULL otherwise. The procedure uses a + four-way recursion to examine all four combinations of cofactors of + f and g. The most interesting feature of this function is the + scheme used for caching the results in the global computed table. + Since we have a cube and a distance, we combine them to form an ADD. + The combination replaces the zero child of the top node of the cube + with the negative of the distance. (The use of the negative is to + avoid ambiguity with 1.) The degenerate cases (zero and one) are + treated specially because the distance is known (0 for one, and + infinity for zero).] + + SideEffects [None] + + SeeAlso [Cudd_bddClosestCube] + +******************************************************************************/ +DdNode * +cuddBddClosestCube( + DdManager *dd, + DdNode *f, + DdNode *g, + CUDD_VALUE_TYPE bound) +{ + DdNode *res, *F, *G, *ft, *fe, *gt, *ge, *tt, *ee; + DdNode *ctt, *cee, *cte, *cet; + CUDD_VALUE_TYPE minD, dtt, dee, dte, det; + DdNode *one = DD_ONE(dd); + DdNode *lzero = Cudd_Not(one); + DdNode *azero = DD_ZERO(dd); + unsigned int topf, topg, index; + + statLine(dd); + if (bound < (f == Cudd_Not(g))) return(azero); + /* Terminal cases. */ + if (g == lzero || f == lzero) return(azero); + if (f == one && g == one) return(one); + + /* Check cache. */ + F = Cudd_Regular(f); + G = Cudd_Regular(g); + if (F->ref != 1 || G->ref != 1) { + res = cuddCacheLookup2(dd,(DdNode * (*)(DdManager *, DdNode *, + DdNode *)) Cudd_bddClosestCube, f, g); + if (res != NULL) return(res); + } + + topf = cuddI(dd,F->index); + topg = cuddI(dd,G->index); + + /* Compute cofactors. */ + if (topf <= topg) { + 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 <= topf) { + gt = cuddT(G); + ge = cuddE(G); + if (Cudd_IsComplement(g)) { + gt = Cudd_Not(gt); + ge = Cudd_Not(ge); + } + } else { + gt = ge = g; + } + + tt = cuddBddClosestCube(dd,ft,gt,bound); + if (tt == NULL) return(NULL); + cuddRef(tt); + ctt = separateCube(dd,tt,&dtt); + if (ctt == NULL) { + Cudd_RecursiveDeref(dd, tt); + return(NULL); + } + cuddRef(ctt); + Cudd_RecursiveDeref(dd, tt); + minD = dtt; + bound = ddMin(bound,minD); + + ee = cuddBddClosestCube(dd,fe,ge,bound); + if (ee == NULL) { + Cudd_RecursiveDeref(dd, ctt); + return(NULL); + } + cuddRef(ee); + cee = separateCube(dd,ee,&dee); + if (cee == NULL) { + Cudd_RecursiveDeref(dd, ctt); + Cudd_RecursiveDeref(dd, ee); + return(NULL); + } + cuddRef(cee); + Cudd_RecursiveDeref(dd, ee); + minD = ddMin(dtt, dee); + bound = ddMin(bound,minD-1); + + if (minD > 0 && topf == topg) { + DdNode *te = cuddBddClosestCube(dd,ft,ge,bound-1); + if (te == NULL) { + Cudd_RecursiveDeref(dd, ctt); + Cudd_RecursiveDeref(dd, cee); + return(NULL); + } + cuddRef(te); + cte = separateCube(dd,te,&dte); + if (cte == NULL) { + Cudd_RecursiveDeref(dd, ctt); + Cudd_RecursiveDeref(dd, cee); + Cudd_RecursiveDeref(dd, te); + return(NULL); + } + cuddRef(cte); + Cudd_RecursiveDeref(dd, te); + dte += 1.0; + minD = ddMin(minD, dte); + } else { + cte = azero; + cuddRef(cte); + dte = CUDD_CONST_INDEX + 1.0; + } + bound = ddMin(bound,minD-1); + + if (minD > 0 && topf == topg) { + DdNode *et = cuddBddClosestCube(dd,fe,gt,bound-1); + if (et == NULL) { + Cudd_RecursiveDeref(dd, ctt); + Cudd_RecursiveDeref(dd, cee); + Cudd_RecursiveDeref(dd, cte); + return(NULL); + } + cuddRef(et); + cet = separateCube(dd,et,&det); + if (cet == NULL) { + Cudd_RecursiveDeref(dd, ctt); + Cudd_RecursiveDeref(dd, cee); + Cudd_RecursiveDeref(dd, cte); + Cudd_RecursiveDeref(dd, et); + return(NULL); + } + cuddRef(cet); + Cudd_RecursiveDeref(dd, et); + det += 1.0; + minD = ddMin(minD, det); + } else { + cet = azero; + cuddRef(cet); + det = CUDD_CONST_INDEX + 1.0; + } + + if (minD == dtt) { + if (dtt == dee && ctt == cee) { + res = createResult(dd,CUDD_CONST_INDEX,1,ctt,dtt); + } else { + res = createResult(dd,index,1,ctt,dtt); + } + } else if (minD == dee) { + res = createResult(dd,index,0,cee,dee); + } else if (minD == dte) { + res = createResult(dd,index,(topf <= topg),cte,dte); + } else { + res = createResult(dd,index,(topf > topg),cet,det); + } + cuddRef(res); + Cudd_RecursiveDeref(dd, ctt); + Cudd_RecursiveDeref(dd, cee); + Cudd_RecursiveDeref(dd, cte); + Cudd_RecursiveDeref(dd, cet); + + if (F->ref != 1 || G->ref != 1) + cuddCacheInsert2(dd,(DdNode * (*)(DdManager *, DdNode *, + DdNode *)) Cudd_bddClosestCube, f, g, res); + + cuddDeref(res); + return(res); + +} /* end of cuddBddClosestCube */ + + +/*---------------------------------------------------------------------------*/ +/* Definition of static functions */ +/*---------------------------------------------------------------------------*/ + + +/**Function******************************************************************** + + Synopsis [Performs the recursive step of Cudd_MinHammingDist.] + + Description [Performs the recursive step of Cudd_MinHammingDist. + It is based on the following identity. Let H(f) be the + minimum Hamming distance of the minterms of f from the reference + minterm. Then: + <xmp> + H(f) = min(H(f0)+h0,H(f1)+h1) + </xmp> + where f0 and f1 are the two cofactors of f with respect to its top + variable; h0 is 1 if the minterm assigns 1 to the top variable of f; + h1 is 1 if the minterm assigns 0 to the top variable of f. + The upper bound on the distance is used to bound the depth of the + recursion. + Returns the minimum distance unless it exceeds the upper bound or + computation fails.] + + SideEffects [None] + + SeeAlso [Cudd_MinHammingDist] + +******************************************************************************/ +static int +cuddMinHammingDistRecur( + DdNode * f, + int *minterm, + DdHashTable * table, + int upperBound) +{ + DdNode *F, *Ft, *Fe; + double h, hT, hE; + DdNode *zero, *res; + DdManager *dd = table->manager; + + statLine(dd); + if (upperBound == 0) return(0); + + F = Cudd_Regular(f); + + if (cuddIsConstant(F)) { + zero = Cudd_Not(DD_ONE(dd)); + if (f == dd->background || f == zero) { + return(upperBound); + } else { + return(0); + } + } + if ((res = cuddHashTableLookup1(table,f)) != NULL) { + h = cuddV(res); + if (res->ref == 0) { + dd->dead++; + dd->constants.dead++; + } + return((int) h); + } + + Ft = cuddT(F); Fe = cuddE(F); + if (Cudd_IsComplement(f)) { + Ft = Cudd_Not(Ft); Fe = Cudd_Not(Fe); + } + if (minterm[F->index] == 0) { + DdNode *temp = Ft; + Ft = Fe; Fe = temp; + } + + hT = cuddMinHammingDistRecur(Ft,minterm,table,upperBound); + if (hT == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM); + if (hT == 0) { + hE = upperBound; + } else { + hE = cuddMinHammingDistRecur(Fe,minterm,table,upperBound - 1); + if (hE == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM); + } + h = ddMin(hT, hE + 1); + + if (F->ref != 1) { + ptrint fanout = (ptrint) F->ref; + cuddSatDec(fanout); + res = cuddUniqueConst(dd, (CUDD_VALUE_TYPE) h); + if (!cuddHashTableInsert1(table,f,res,fanout)) { + cuddRef(res); Cudd_RecursiveDeref(dd, res); + return(CUDD_OUT_OF_MEM); + } + } + + return((int) h); + +} /* end of cuddMinHammingDistRecur */ + + +/**Function******************************************************************** + + Synopsis [Separates cube from distance.] + + Description [Separates cube from distance. Returns the cube if + successful; NULL otherwise.] + + SideEffects [The distance is returned as a side effect.] + + SeeAlso [cuddBddClosestCube createResult] + +******************************************************************************/ +static DdNode * +separateCube( + DdManager *dd, + DdNode *f, + CUDD_VALUE_TYPE *distance) +{ + DdNode *cube, *t; + + /* One and zero are special cases because the distance is implied. */ + if (Cudd_IsConstant(f)) { + *distance = (f == DD_ONE(dd)) ? 0.0 : + (1.0 + (CUDD_VALUE_TYPE) CUDD_CONST_INDEX); + return(f); + } + + /* Find out which branch points to the distance and replace the top + ** node with one pointing to zero instead. */ + t = cuddT(f); + if (Cudd_IsConstant(t) && cuddV(t) <= 0) { +#ifdef DD_DEBUG + assert(!Cudd_IsConstant(cuddE(f)) || cuddE(f) == DD_ONE(dd)); +#endif + *distance = -cuddV(t); + cube = cuddUniqueInter(dd, f->index, DD_ZERO(dd), cuddE(f)); + } else { +#ifdef DD_DEBUG + assert(!Cudd_IsConstant(t) || t == DD_ONE(dd)); +#endif + *distance = -cuddV(cuddE(f)); + cube = cuddUniqueInter(dd, f->index, t, DD_ZERO(dd)); + } + + return(cube); + +} /* end of separateCube */ + + +/**Function******************************************************************** + + Synopsis [Builds a result for cache storage.] + + Description [Builds a result for cache storage. Returns a pointer + to the resulting ADD if successful; NULL otherwise.] + + SideEffects [None] + + SeeAlso [cuddBddClosestCube separateCube] + +******************************************************************************/ +static DdNode * +createResult( + DdManager *dd, + unsigned int index, + unsigned int phase, + DdNode *cube, + CUDD_VALUE_TYPE distance) +{ + DdNode *res, *constant; + + /* Special case. The cube is either one or zero, and we do not + ** add any variables. Hence, the result is also one or zero, + ** and the distance remains implied by teh value of the constant. */ + if (index == CUDD_CONST_INDEX && Cudd_IsConstant(cube)) return(cube); + + constant = cuddUniqueConst(dd,-distance); + if (constant == NULL) return(NULL); + cuddRef(constant); + + if (index == CUDD_CONST_INDEX) { + /* Replace the top node. */ + if (cuddT(cube) == DD_ZERO(dd)) { + res = cuddUniqueInter(dd,cube->index,constant,cuddE(cube)); + } else { + res = cuddUniqueInter(dd,cube->index,cuddT(cube),constant); + } + } else { + /* Add a new top node. */ +#ifdef DD_DEBUG + assert(cuddI(dd,index) < cuddI(dd,cube->index)); +#endif + if (phase) { + res = cuddUniqueInter(dd,index,cube,constant); + } else { + res = cuddUniqueInter(dd,index,constant,cube); + } + } + if (res == NULL) { + Cudd_RecursiveDeref(dd, constant); + return(NULL); + } + cuddDeref(constant); /* safe because constant is part of res */ + + return(res); + +} /* end of createResult */ |