📄 cuddpriority.c
字号:
/**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 lintstatic 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);
⌨️ 快捷键说明
复制代码
Ctrl + C
搜索代码
Ctrl + F
全屏模式
F11
切换主题
Ctrl + Shift + D
显示快捷键
?
增大字号
Ctrl + =
减小字号
Ctrl + -