diff options
Diffstat (limited to 'abc70930/src/bdd/cudd/cuddUtil.c')
| -rw-r--r-- | abc70930/src/bdd/cudd/cuddUtil.c | 3633 |
1 files changed, 0 insertions, 3633 deletions
diff --git a/abc70930/src/bdd/cudd/cuddUtil.c b/abc70930/src/bdd/cudd/cuddUtil.c deleted file mode 100644 index d5fa18e2..00000000 --- a/abc70930/src/bdd/cudd/cuddUtil.c +++ /dev/null @@ -1,3633 +0,0 @@ -/**CFile*********************************************************************** - - FileName [cuddUtil.c] - - PackageName [cudd] - - Synopsis [Utility functions.] - - Description [External procedures included in this module: - <ul> - <li> Cudd_PrintMinterm() - <li> Cudd_PrintDebug() - <li> Cudd_DagSize() - <li> Cudd_EstimateCofactor() - <li> Cudd_EstimateCofactorSimple() - <li> Cudd_SharingSize() - <li> Cudd_CountMinterm() - <li> Cudd_EpdCountMinterm() - <li> Cudd_CountPath() - <li> Cudd_CountPathsToNonZero() - <li> Cudd_Support() - <li> Cudd_SupportIndex() - <li> Cudd_SupportSize() - <li> Cudd_VectorSupport() - <li> Cudd_VectorSupportIndex() - <li> Cudd_VectorSupportSize() - <li> Cudd_ClassifySupport() - <li> Cudd_CountLeaves() - <li> Cudd_bddPickOneCube() - <li> Cudd_bddPickOneMinterm() - <li> Cudd_bddPickArbitraryMinterms() - <li> Cudd_SubsetWithMaskVars() - <li> Cudd_FirstCube() - <li> Cudd_NextCube() - <li> Cudd_bddComputeCube() - <li> Cudd_addComputeCube() - <li> Cudd_FirstNode() - <li> Cudd_NextNode() - <li> Cudd_GenFree() - <li> Cudd_IsGenEmpty() - <li> Cudd_IndicesToCube() - <li> Cudd_PrintVersion() - <li> Cudd_AverageDistance() - <li> Cudd_Random() - <li> Cudd_Srandom() - <li> Cudd_Density() - </ul> - Internal procedures included in this module: - <ul> - <li> cuddP() - <li> cuddStCountfree() - <li> cuddCollectNodes() - </ul> - Static procedures included in this module: - <ul> - <li> dp2() - <li> ddPrintMintermAux() - <li> ddDagInt() - <li> ddCountMintermAux() - <li> ddEpdCountMintermAux() - <li> ddCountPathAux() - <li> ddSupportStep() - <li> ddClearFlag() - <li> ddLeavesInt() - <li> ddPickArbitraryMinterms() - <li> ddPickRepresentativeCube() - <li> ddEpdFree() - </ul>] - - 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_hack.h" -#include "cuddInt.h" - -/*---------------------------------------------------------------------------*/ -/* Constant declarations */ -/*---------------------------------------------------------------------------*/ - -/* Random generator constants. */ -#define MODULUS1 2147483563 -#define LEQA1 40014 -#define LEQQ1 53668 -#define LEQR1 12211 -#define MODULUS2 2147483399 -#define LEQA2 40692 -#define LEQQ2 52774 -#define LEQR2 3791 -#define STAB_SIZE 64 -#define STAB_DIV (1 + (MODULUS1 - 1) / STAB_SIZE) - -/*---------------------------------------------------------------------------*/ -/* Stucture declarations */ -/*---------------------------------------------------------------------------*/ - -/*---------------------------------------------------------------------------*/ -/* Type declarations */ -/*---------------------------------------------------------------------------*/ - - -/*---------------------------------------------------------------------------*/ -/* Variable declarations */ -/*---------------------------------------------------------------------------*/ - -#ifndef lint -static char rcsid[] DD_UNUSED = "$Id: cuddUtil.c,v 1.1.1.1 2003/02/24 22:23:53 wjiang Exp $"; -#endif - -static DdNode *background, *zero; - -static long cuddRand = 0; -static long cuddRand2; -static long shuffleSelect; -static long shuffleTable[STAB_SIZE]; - -/*---------------------------------------------------------------------------*/ -/* Macro declarations */ -/*---------------------------------------------------------------------------*/ - -#define bang(f) ((Cudd_IsComplement(f)) ? '!' : ' ') - -/**AutomaticStart*************************************************************/ - -/*---------------------------------------------------------------------------*/ -/* Static function prototypes */ -/*---------------------------------------------------------------------------*/ - -static int dp2 ARGS((DdManager *dd, DdNode *f, st_table *t)); -static void ddPrintMintermAux ARGS((DdManager *dd, DdNode *node, int *list)); -static int ddDagInt ARGS((DdNode *n)); -static int cuddEstimateCofactor ARGS((DdManager *dd, st_table *table, DdNode * node, int i, int phase, DdNode ** ptr)); -static DdNode * cuddUniqueLookup ARGS((DdManager * unique, int index, DdNode * T, DdNode * E)); -static int cuddEstimateCofactorSimple ARGS((DdNode * node, int i)); -static double ddCountMintermAux ARGS((DdNode *node, double max, DdHashTable *table)); -static int ddEpdCountMintermAux ARGS((DdNode *node, EpDouble *max, EpDouble *epd, st_table *table)); -static double ddCountPathAux ARGS((DdNode *node, st_table *table)); -static double ddCountPathsToNonZero ARGS((DdNode * N, st_table * table)); -static void ddSupportStep ARGS((DdNode *f, int *support)); -static void ddClearFlag ARGS((DdNode *f)); -static int ddLeavesInt ARGS((DdNode *n)); -static int ddPickArbitraryMinterms ARGS((DdManager *dd, DdNode *node, int nvars, int nminterms, char **string)); -static int ddPickRepresentativeCube ARGS((DdManager *dd, DdNode *node, int nvars, double *weight, char *string)); -static enum st_retval ddEpdFree ARGS((char * key, char * value, char * arg)); - -/**AutomaticEnd***************************************************************/ - - -/*---------------------------------------------------------------------------*/ -/* Definition of exported functions */ -/*---------------------------------------------------------------------------*/ - - -/**Function******************************************************************** - - Synopsis [Prints a disjoint sum of products.] - - Description [Prints a disjoint sum of product cover for the function - rooted at node. Each product corresponds to a path from node to a - leaf node different from the logical zero, and different from the - background value. Uses the package default output file. Returns 1 - if successful; 0 otherwise.] - - SideEffects [None] - - SeeAlso [Cudd_PrintDebug Cudd_bddPrintCover] - -******************************************************************************/ -int -Cudd_PrintMinterm( - DdManager * manager, - DdNode * node) -{ - int i, *list; - - background = manager->background; - zero = Cudd_Not(manager->one); - list = ALLOC(int,manager->size); - if (list == NULL) { - manager->errorCode = CUDD_MEMORY_OUT; - return(0); - } - for (i = 0; i < manager->size; i++) list[i] = 2; - ddPrintMintermAux(manager,node,list); - FREE(list); - return(1); - -} /* end of Cudd_PrintMinterm */ - - -/**Function******************************************************************** - - Synopsis [Prints a sum of prime implicants of a BDD.] - - Description [Prints a sum of product cover for an incompletely - specified function given by a lower bound and an upper bound. Each - product is a prime implicant obtained by expanding the product - corresponding to a path from node to the constant one. Uses the - package default output file. Returns 1 if successful; 0 otherwise.] - - SideEffects [None] - - SeeAlso [Cudd_PrintMinterm] - -******************************************************************************/ -int -Cudd_bddPrintCover( - DdManager *dd, - DdNode *l, - DdNode *u) -{ - int *array; - int q, result; - DdNode *lb; -#ifdef DD_DEBUG - DdNode *cover; -#endif - - array = ALLOC(int, Cudd_ReadSize(dd)); - if (array == NULL) return(0); - lb = l; - cuddRef(lb); -#ifdef DD_DEBUG - cover = Cudd_ReadLogicZero(dd); - cuddRef(cover); -#endif - while (lb != Cudd_ReadLogicZero(dd)) { - DdNode *implicant, *prime, *tmp; - int length; - implicant = Cudd_LargestCube(dd,lb,&length); - if (implicant == NULL) { - Cudd_RecursiveDeref(dd,lb); - FREE(array); - return(0); - } - cuddRef(implicant); - prime = Cudd_bddMakePrime(dd,implicant,u); - if (prime == NULL) { - Cudd_RecursiveDeref(dd,lb); - Cudd_RecursiveDeref(dd,implicant); - FREE(array); - return(0); - } - cuddRef(prime); - Cudd_RecursiveDeref(dd,implicant); - tmp = Cudd_bddAnd(dd,lb,Cudd_Not(prime)); - if (tmp == NULL) { - Cudd_RecursiveDeref(dd,lb); - Cudd_RecursiveDeref(dd,prime); - FREE(array); - return(0); - } - cuddRef(tmp); - Cudd_RecursiveDeref(dd,lb); - lb = tmp; - result = Cudd_BddToCubeArray(dd,prime,array); - if (result == 0) { - Cudd_RecursiveDeref(dd,lb); - Cudd_RecursiveDeref(dd,prime); - FREE(array); - return(0); - } - for (q = 0; q < dd->size; q++) { - switch (array[q]) { - case 0: - (void) fprintf(dd->out, "0"); - break; - case 1: - (void) fprintf(dd->out, "1"); - break; - case 2: - (void) fprintf(dd->out, "-"); - break; - default: - (void) fprintf(dd->out, "?"); - } - } - (void) fprintf(dd->out, " 1\n"); -#ifdef DD_DEBUG - tmp = Cudd_bddOr(dd,prime,cover); - if (tmp == NULL) { - Cudd_RecursiveDeref(dd,cover); - Cudd_RecursiveDeref(dd,lb); - Cudd_RecursiveDeref(dd,prime); - FREE(array); - return(0); - } - cuddRef(tmp); - Cudd_RecursiveDeref(dd,cover); - cover = tmp; -#endif - Cudd_RecursiveDeref(dd,prime); - } - (void) fprintf(dd->out, "\n"); - Cudd_RecursiveDeref(dd,lb); - FREE(array); -#ifdef DD_DEBUG - if (!Cudd_bddLeq(dd,cover,u) || !Cudd_bddLeq(dd,l,cover)) { - Cudd_RecursiveDeref(dd,cover); - return(0); - } - Cudd_RecursiveDeref(dd,cover); -#endif - return(1); - -} /* end of Cudd_bddPrintCover */ - - -/**Function******************************************************************** - - Synopsis [Prints to the standard output a DD and its statistics.] - - Description [Prints to the standard output a DD and its statistics. - The statistics include the number of nodes, the number of leaves, and - the number of minterms. (The number of minterms is the number of - assignments to the variables that cause the function to be different - from the logical zero (for BDDs) and from the background value (for - ADDs.) The statistics are printed if pr > 0. Specifically: - <ul> - <li> pr = 0 : prints nothing - <li> pr = 1 : prints counts of nodes and minterms - <li> pr = 2 : prints counts + disjoint sum of product - <li> pr = 3 : prints counts + list of nodes - <li> pr > 3 : prints counts + disjoint sum of product + list of nodes - </ul> - For the purpose of counting the number of minterms, the function is - supposed to depend on n variables. Returns 1 if successful; 0 otherwise.] - - SideEffects [None] - - SeeAlso [Cudd_DagSize Cudd_CountLeaves Cudd_CountMinterm - Cudd_PrintMinterm] - -******************************************************************************/ -int -Cudd_PrintDebug( - DdManager * dd, - DdNode * f, - int n, - int pr) -{ - DdNode *azero, *bzero; - int nodes; - int leaves; - double minterms; - int retval = 1; - - if (f == NULL) { - (void) fprintf(dd->out,": is the NULL DD\n"); - (void) fflush(dd->out); - return(0); - } - azero = DD_ZERO(dd); - bzero = Cudd_Not(DD_ONE(dd)); - if ((f == azero || f == bzero) && pr > 0){ - (void) fprintf(dd->out,": is the zero DD\n"); - (void) fflush(dd->out); - return(1); - } - if (pr > 0) { - nodes = Cudd_DagSize(f); - if (nodes == CUDD_OUT_OF_MEM) retval = 0; - leaves = Cudd_CountLeaves(f); - if (leaves == CUDD_OUT_OF_MEM) retval = 0; - minterms = Cudd_CountMinterm(dd, f, n); - if (minterms == (double)CUDD_OUT_OF_MEM) retval = 0; - (void) fprintf(dd->out,": %d nodes %d leaves %g minterms\n", - nodes, leaves, minterms); - if (pr > 2) { - if (!cuddP(dd, f)) retval = 0; - } - if (pr == 2 || pr > 3) { - if (!Cudd_PrintMinterm(dd,f)) retval = 0; - (void) fprintf(dd->out,"\n"); - } - (void) fflush(dd->out); - } - return(retval); - -} /* end of Cudd_PrintDebug */ - - -/**Function******************************************************************** - - Synopsis [Counts the number of nodes in a DD.] - - Description [Counts the number of nodes in a DD. Returns the number - of nodes in the graph rooted at node.] - - SideEffects [None] - - SeeAlso [Cudd_SharingSize Cudd_PrintDebug] - -******************************************************************************/ -int -Cudd_DagSize( - DdNode * node) -{ - int i; - - i = ddDagInt(Cudd_Regular(node)); - ddClearFlag(Cudd_Regular(node)); - - return(i); - -} /* end of Cudd_DagSize */ - - -/**Function******************************************************************** - - Synopsis [Estimates the number of nodes in a cofactor of a DD.] - - Description [Estimates the number of nodes in a cofactor of a DD. - Returns an estimate of the number of nodes in a cofactor of - the graph rooted at node with respect to the variable whose index is i. - In case of failure, returns CUDD_OUT_OF_MEM. - This function uses a refinement of the algorithm of Cabodi et al. - (ICCAD96). The refinement allows the procedure to account for part - of the recombination that may occur in the part of the cofactor above - the cofactoring variable. This procedure does no create any new node. - It does keep a small table of results; therefore itmay run out of memory. - If this is a concern, one should use Cudd_EstimateCofactorSimple, which - is faster, does not allocate any memory, but is less accurate.] - - SideEffects [None] - - SeeAlso [Cudd_DagSize Cudd_EstimateCofactorSimple] - -******************************************************************************/ -int -Cudd_EstimateCofactor( - DdManager *dd /* manager */, - DdNode * f /* function */, - int i /* index of variable */, - int phase /* 1: positive; 0: negative */ - ) -{ - int val; - DdNode *ptr; - st_table *table; - - table = st_init_table(st_ptrcmp,st_ptrhash); - if (table == NULL) return(CUDD_OUT_OF_MEM); - val = cuddEstimateCofactor(dd,table,Cudd_Regular(f),i,phase,&ptr); - ddClearFlag(Cudd_Regular(f)); - st_free_table(table); - - return(val); - -} /* end of Cudd_EstimateCofactor */ - - -/**Function******************************************************************** - - Synopsis [Estimates the number of nodes in a cofactor of a DD.] - - Description [Estimates the number of nodes in a cofactor of a DD. - Returns an estimate of the number of nodes in the positive cofactor of - the graph rooted at node with respect to the variable whose index is i. - This procedure implements with minor changes the algorithm of Cabodi et al. - (ICCAD96). It does not allocate any memory, it does not change the - state of the manager, and it is fast. However, it has been observed to - overestimate the size of the cofactor by as much as a factor of 2.] - - SideEffects [None] - - SeeAlso [Cudd_DagSize] - -******************************************************************************/ -int -Cudd_EstimateCofactorSimple( - DdNode * node, - int i) -{ - int val; - - val = cuddEstimateCofactorSimple(Cudd_Regular(node),i); - ddClearFlag(Cudd_Regular(node)); - - return(val); - -} /* end of Cudd_EstimateCofactorSimple */ - - -/**Function******************************************************************** - - Synopsis [Counts the number of nodes in an array of DDs.] - - Description [Counts the number of nodes in an array of DDs. Shared - nodes are counted only once. Returns the total number of nodes.] - - SideEffects [None] - - SeeAlso [Cudd_DagSize] - -******************************************************************************/ -int -Cudd_SharingSize( - DdNode ** nodeArray, - int n) -{ - int i,j; - - i = 0; - for (j = 0; j < n; j++) { - i += ddDagInt(Cudd_Regular(nodeArray[j])); - } - for (j = 0; j < n; j++) { - ddClearFlag(Cudd_Regular(nodeArray[j])); - } - return(i); - -} /* end of Cudd_SharingSize */ - - -/**Function******************************************************************** - - Synopsis [Counts the number of minterms of a DD.] - - Description [Counts the number of minterms of a DD. The function is - assumed to depend on nvars variables. The minterm count is - represented as a double, to allow for a larger number of variables. - Returns the number of minterms of the function rooted at node if - successful; (double) CUDD_OUT_OF_MEM otherwise.] - - SideEffects [None] - - SeeAlso [Cudd_PrintDebug Cudd_CountPath] - -******************************************************************************/ -double -Cudd_CountMinterm( - DdManager * manager, - DdNode * node, - int nvars) -{ - double max; - DdHashTable *table; - double res; - CUDD_VALUE_TYPE epsilon; - - background = manager->background; - zero = Cudd_Not(manager->one); - - max = pow(2.0,(double)nvars); - table = cuddHashTableInit(manager,1,2); - if (table == NULL) { - return((double)CUDD_OUT_OF_MEM); - } - epsilon = Cudd_ReadEpsilon(manager); - Cudd_SetEpsilon(manager,(CUDD_VALUE_TYPE)0.0); - res = ddCountMintermAux(node,max,table); - cuddHashTableQuit(table); - Cudd_SetEpsilon(manager,epsilon); - - return(res); - -} /* end of Cudd_CountMinterm */ - - -/**Function******************************************************************** - - Synopsis [Counts the number of paths of a DD.] - - Description [Counts the number of paths of a DD. Paths to all - terminal nodes are counted. The path count is represented as a - double, to allow for a larger number of variables. Returns the - number of paths of the function rooted at node if successful; - (double) CUDD_OUT_OF_MEM otherwise.] - - SideEffects [None] - - SeeAlso [Cudd_CountMinterm] - -******************************************************************************/ -double -Cudd_CountPath( - DdNode * node) -{ - - st_table *table; - double i; - - table = st_init_table(st_ptrcmp,st_ptrhash); - if (table == NULL) { - return((double)CUDD_OUT_OF_MEM); - } - i = ddCountPathAux(Cudd_Regular(node),table); - st_foreach(table, cuddStCountfree, NULL); - st_free_table(table); - return(i); - -} /* end of Cudd_CountPath */ - - -/**Function******************************************************************** - - Synopsis [Counts the number of minterms of a DD with extended precision.] - - Description [Counts the number of minterms of a DD with extended precision. - The function is assumed to depend on nvars variables. The minterm count is - represented as an EpDouble, to allow any number of variables. - Returns 0 if successful; CUDD_OUT_OF_MEM otherwise.] - - SideEffects [None] - - SeeAlso [Cudd_PrintDebug Cudd_CountPath] - -******************************************************************************/ -int -Cudd_EpdCountMinterm( - DdManager * manager, - DdNode * node, - int nvars, - EpDouble * epd) -{ - EpDouble max, tmp; - st_table *table; - int status; - - background = manager->background; - zero = Cudd_Not(manager->one); - - EpdPow2(nvars, &max); - table = st_init_table(EpdCmp, st_ptrhash); - if (table == NULL) { - EpdMakeZero(epd, 0); - return(CUDD_OUT_OF_MEM); - } - status = ddEpdCountMintermAux(Cudd_Regular(node),&max,epd,table); - st_foreach(table, ddEpdFree, NULL); - st_free_table(table); - if (status == CUDD_OUT_OF_MEM) { - EpdMakeZero(epd, 0); - return(CUDD_OUT_OF_MEM); - } - if (Cudd_IsComplement(node)) { - EpdSubtract3(&max, epd, &tmp); - EpdCopy(&tmp, epd); - } - return(0); - -} /* end of Cudd_EpdCountMinterm */ - - -/**Function******************************************************************** - - Synopsis [Counts the number of paths to a non-zero terminal of a DD.] - - Description [Counts the number of paths to a non-zero terminal of a - DD. The path count is - represented as a double, to allow for a larger number of variables. - Returns the number of paths of the function rooted at node.] - - SideEffects [None] - - SeeAlso [Cudd_CountMinterm Cudd_CountPath] - -******************************************************************************/ -double -Cudd_CountPathsToNonZero( - DdNode * node) -{ - - st_table *table; - double i; - - table = st_init_table(st_ptrcmp,st_ptrhash); - if (table == NULL) { - return((double)CUDD_OUT_OF_MEM); - } - i = ddCountPathsToNonZero(node,table); - st_foreach(table, cuddStCountfree, NULL); - st_free_table(table); - return(i); - -} /* end of Cudd_CountPathsToNonZero */ - - -/**Function******************************************************************** - - Synopsis [Finds the variables on which a DD depends.] - - Description [Finds the variables on which a DD depends. - Returns a BDD consisting of the product of the variables if - successful; NULL otherwise.] - - SideEffects [None] - - SeeAlso [Cudd_VectorSupport Cudd_ClassifySupport] - -******************************************************************************/ -DdNode * -Cudd_Support( - DdManager * dd /* manager */, - DdNode * f /* DD whose support is sought */) -{ - int *support; - DdNode *res, *tmp, *var; - int i,j; - int size; - - /* Allocate and initialize support array for ddSupportStep. */ - size = ddMax(dd->size, dd->sizeZ); - support = ALLOC(int,size); - if (support == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - return(NULL); - } - for (i = 0; i < size; i++) { - support[i] = 0; - } - - /* Compute support and clean up markers. */ - ddSupportStep(Cudd_Regular(f),support); - ddClearFlag(Cudd_Regular(f)); - - /* Transform support from array to cube. */ - do { - dd->reordered = 0; - res = DD_ONE(dd); - cuddRef(res); - for (j = size - 1; j >= 0; j--) { /* for each level bottom-up */ - i = (j >= dd->size) ? j : dd->invperm[j]; - if (support[i] == 1) { - var = cuddUniqueInter(dd,i,dd->one,Cudd_Not(dd->one)); - cuddRef(var); - tmp = cuddBddAndRecur(dd,res,var); - if (tmp == NULL) { - Cudd_RecursiveDeref(dd,res); - Cudd_RecursiveDeref(dd,var); - res = NULL; - break; - } - cuddRef(tmp); - Cudd_RecursiveDeref(dd,res); - Cudd_RecursiveDeref(dd,var); - res = tmp; - } - } - } while (dd->reordered == 1); - - FREE(support); - if (res != NULL) cuddDeref(res); - return(res); - -} /* end of Cudd_Support */ - - -/**Function******************************************************************** - - Synopsis [Finds the variables on which a DD depends.] - - Description [Finds the variables on which a DD depends. - Returns an index array of the variables if successful; NULL otherwise.] - - SideEffects [None] - - SeeAlso [Cudd_Support Cudd_VectorSupport Cudd_ClassifySupport] - -******************************************************************************/ -int * -Cudd_SupportIndex( - DdManager * dd /* manager */, - DdNode * f /* DD whose support is sought */) -{ - int *support; - int i; - int size; - - /* Allocate and initialize support array for ddSupportStep. */ - size = ddMax(dd->size, dd->sizeZ); - support = ALLOC(int,size); - if (support == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - return(NULL); - } - for (i = 0; i < size; i++) { - support[i] = 0; - } - - /* Compute support and clean up markers. */ - ddSupportStep(Cudd_Regular(f),support); - ddClearFlag(Cudd_Regular(f)); - - return(support); - -} /* end of Cudd_SupportIndex */ - - -/**Function******************************************************************** - - Synopsis [Counts the variables on which a DD depends.] - - Description [Counts the variables on which a DD depends. - Returns the number of the variables if successful; CUDD_OUT_OF_MEM - otherwise.] - - SideEffects [None] - - SeeAlso [Cudd_Support] - -******************************************************************************/ -int -Cudd_SupportSize( - DdManager * dd /* manager */, - DdNode * f /* DD whose support size is sought */) -{ - int *support; - int i; - int size; - int count; - - /* Allocate and initialize support array for ddSupportStep. */ - size = ddMax(dd->size, dd->sizeZ); - support = ALLOC(int,size); - if (support == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - return(CUDD_OUT_OF_MEM); - } - for (i = 0; i < size; i++) { - support[i] = 0; - } - - /* Compute support and clean up markers. */ - ddSupportStep(Cudd_Regular(f),support); - ddClearFlag(Cudd_Regular(f)); - - /* Count support variables. */ - count = 0; - for (i = 0; i < size; i++) { - if (support[i] == 1) count++; - } - - FREE(support); - return(count); - -} /* end of Cudd_SupportSize */ - - -/**Function******************************************************************** - - Synopsis [Finds the variables on which a set of DDs depends.] - - Description [Finds the variables on which a set of DDs depends. - The set must contain either BDDs and ADDs, or ZDDs. - Returns a BDD consisting of the product of the variables if - successful; NULL otherwise.] - - SideEffects [None] - - SeeAlso [Cudd_Support Cudd_ClassifySupport] - -******************************************************************************/ -DdNode * -Cudd_VectorSupport( - DdManager * dd /* manager */, - DdNode ** F /* array of DDs whose support is sought */, - int n /* size of the array */) -{ - int *support; - DdNode *res, *tmp, *var; - int i,j; - int size; - - /* Allocate and initialize support array for ddSupportStep. */ - size = ddMax(dd->size, dd->sizeZ); - support = ALLOC(int,size); - if (support == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - return(NULL); - } - for (i = 0; i < size; i++) { - support[i] = 0; - } - - /* Compute support and clean up markers. */ - for (i = 0; i < n; i++) { - ddSupportStep(Cudd_Regular(F[i]),support); - } - for (i = 0; i < n; i++) { - ddClearFlag(Cudd_Regular(F[i])); - } - - /* Transform support from array to cube. */ - res = DD_ONE(dd); - cuddRef(res); - for (j = size - 1; j >= 0; j--) { /* for each level bottom-up */ - i = (j >= dd->size) ? j : dd->invperm[j]; - if (support[i] == 1) { - var = cuddUniqueInter(dd,i,dd->one,Cudd_Not(dd->one)); - cuddRef(var); - tmp = Cudd_bddAnd(dd,res,var); - if (tmp == NULL) { - Cudd_RecursiveDeref(dd,res); - Cudd_RecursiveDeref(dd,var); - FREE(support); - return(NULL); - } - cuddRef(tmp); - Cudd_RecursiveDeref(dd,res); - Cudd_RecursiveDeref(dd,var); - res = tmp; - } - } - - FREE(support); - cuddDeref(res); - return(res); - -} /* end of Cudd_VectorSupport */ - - -/**Function******************************************************************** - - Synopsis [Finds the variables on which a set of DDs depends.] - - Description [Finds the variables on which a set of DDs depends. - The set must contain either BDDs and ADDs, or ZDDs. - Returns an index array of the variables if successful; NULL otherwise.] - - SideEffects [None] - - SeeAlso [Cudd_SupportIndex Cudd_VectorSupport Cudd_ClassifySupport] - -******************************************************************************/ -int * -Cudd_VectorSupportIndex( - DdManager * dd /* manager */, - DdNode ** F /* array of DDs whose support is sought */, - int n /* size of the array */) -{ - int *support; - int i; - int size; - - /* Allocate and initialize support array for ddSupportStep. */ - size = ddMax(dd->size, dd->sizeZ); - support = ALLOC(int,size); - if (support == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - return(NULL); - } - for (i = 0; i < size; i++) { - support[i] = 0; - } - - /* Compute support and clean up markers. */ - for (i = 0; i < n; i++) { - ddSupportStep(Cudd_Regular(F[i]),support); - } - for (i = 0; i < n; i++) { - ddClearFlag(Cudd_Regular(F[i])); - } - - return(support); - -} /* end of Cudd_VectorSupportIndex */ - - -/**Function******************************************************************** - - Synopsis [Counts the variables on which a set of DDs depends.] - - Description [Counts the variables on which a set of DDs depends. - The set must contain either BDDs and ADDs, or ZDDs. - Returns the number of the variables if successful; CUDD_OUT_OF_MEM - otherwise.] - - SideEffects [None] - - SeeAlso [Cudd_VectorSupport Cudd_SupportSize] - -******************************************************************************/ -int -Cudd_VectorSupportSize( - DdManager * dd /* manager */, - DdNode ** F /* array of DDs whose support is sought */, - int n /* size of the array */) -{ - int *support; - int i; - int size; - int count; - - /* Allocate and initialize support array for ddSupportStep. */ - size = ddMax(dd->size, dd->sizeZ); - support = ALLOC(int,size); - if (support == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - return(CUDD_OUT_OF_MEM); - } - for (i = 0; i < size; i++) { - support[i] = 0; - } - - /* Compute support and clean up markers. */ - for (i = 0; i < n; i++) { - ddSupportStep(Cudd_Regular(F[i]),support); - } - for (i = 0; i < n; i++) { - ddClearFlag(Cudd_Regular(F[i])); - } - - /* Count vriables in support. */ - count = 0; - for (i = 0; i < size; i++) { - if (support[i] == 1) count++; - } - - FREE(support); - return(count); - -} /* end of Cudd_VectorSupportSize */ - - -/**Function******************************************************************** - - Synopsis [Classifies the variables in the support of two DDs.] - - Description [Classifies the variables in the support of two DDs - <code>f</code> and <code>g</code>, depending on whther they appear - in both DDs, only in <code>f</code>, or only in <code>g</code>. - Returns 1 if successful; 0 otherwise.] - - SideEffects [The cubes of the three classes of variables are - returned as side effects.] - - SeeAlso [Cudd_Support Cudd_VectorSupport] - -******************************************************************************/ -int -Cudd_ClassifySupport( - DdManager * dd /* manager */, - DdNode * f /* first DD */, - DdNode * g /* second DD */, - DdNode ** common /* cube of shared variables */, - DdNode ** onlyF /* cube of variables only in f */, - DdNode ** onlyG /* cube of variables only in g */) -{ - int *supportF, *supportG; - DdNode *tmp, *var; - int i,j; - int size; - - /* Allocate and initialize support arrays for ddSupportStep. */ - size = ddMax(dd->size, dd->sizeZ); - supportF = ALLOC(int,size); - if (supportF == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - return(0); - } - supportG = ALLOC(int,size); - if (supportG == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - FREE(supportF); - return(0); - } - for (i = 0; i < size; i++) { - supportF[i] = 0; - supportG[i] = 0; - } - - /* Compute supports and clean up markers. */ - ddSupportStep(Cudd_Regular(f),supportF); - ddClearFlag(Cudd_Regular(f)); - ddSupportStep(Cudd_Regular(g),supportG); - ddClearFlag(Cudd_Regular(g)); - - /* Classify variables and create cubes. */ - *common = *onlyF = *onlyG = DD_ONE(dd); - cuddRef(*common); cuddRef(*onlyF); cuddRef(*onlyG); - for (j = size - 1; j >= 0; j--) { /* for each level bottom-up */ - i = (j >= dd->size) ? j : dd->invperm[j]; - if (supportF[i] == 0 && supportG[i] == 0) continue; - var = cuddUniqueInter(dd,i,dd->one,Cudd_Not(dd->one)); - cuddRef(var); - if (supportG[i] == 0) { - tmp = Cudd_bddAnd(dd,*onlyF,var); - if (tmp == NULL) { - Cudd_RecursiveDeref(dd,*common); - Cudd_RecursiveDeref(dd,*onlyF); - Cudd_RecursiveDeref(dd,*onlyG); - Cudd_RecursiveDeref(dd,var); - FREE(supportF); FREE(supportG); - return(0); - } - cuddRef(tmp); - Cudd_RecursiveDeref(dd,*onlyF); - *onlyF = tmp; - } else if (supportF[i] == 0) { - tmp = Cudd_bddAnd(dd,*onlyG,var); - if (tmp == NULL) { - Cudd_RecursiveDeref(dd,*common); - Cudd_RecursiveDeref(dd,*onlyF); - Cudd_RecursiveDeref(dd,*onlyG); - Cudd_RecursiveDeref(dd,var); - FREE(supportF); FREE(supportG); - return(0); - } - cuddRef(tmp); - Cudd_RecursiveDeref(dd,*onlyG); - *onlyG = tmp; - } else { - tmp = Cudd_bddAnd(dd,*common,var); - if (tmp == NULL) { - Cudd_RecursiveDeref(dd,*common); - Cudd_RecursiveDeref(dd,*onlyF); - Cudd_RecursiveDeref(dd,*onlyG); - Cudd_RecursiveDeref(dd,var); - FREE(supportF); FREE(supportG); - return(0); - } - cuddRef(tmp); - Cudd_RecursiveDeref(dd,*common); - *common = tmp; - } - Cudd_RecursiveDeref(dd,var); - } - - FREE(supportF); FREE(supportG); - cuddDeref(*common); cuddDeref(*onlyF); cuddDeref(*onlyG); - return(1); - -} /* end of Cudd_ClassifySupport */ - - -/**Function******************************************************************** - - Synopsis [Counts the number of leaves in a DD.] - - Description [Counts the number of leaves in a DD. Returns the number - of leaves in the DD rooted at node if successful; CUDD_OUT_OF_MEM - otherwise.] - - SideEffects [None] - - SeeAlso [Cudd_PrintDebug] - -******************************************************************************/ -int -Cudd_CountLeaves( - DdNode * node) -{ - int i; - - i = ddLeavesInt(Cudd_Regular(node)); - ddClearFlag(Cudd_Regular(node)); - return(i); - -} /* end of Cudd_CountLeaves */ - - -/**Function******************************************************************** - - Synopsis [Picks one on-set cube randomly from the given DD.] - - Description [Picks one on-set cube randomly from the given DD. The - cube is written into an array of characters. The array must have at - least as many entries as there are variables. Returns 1 if - successful; 0 otherwise.] - - SideEffects [None] - - SeeAlso [Cudd_bddPickOneMinterm] - -******************************************************************************/ -int -Cudd_bddPickOneCube( - DdManager * ddm, - DdNode * node, - char * string) -{ - DdNode *N, *T, *E; - DdNode *one, *bzero; - char dir; - int i; - - if (string == NULL || node == NULL) return(0); - - /* The constant 0 function has no on-set cubes. */ - one = DD_ONE(ddm); - bzero = Cudd_Not(one); - if (node == bzero) return(0); - - for (i = 0; i < ddm->size; i++) string[i] = 2; - - for (;;) { - - if (node == one) break; - - N = Cudd_Regular(node); - - T = cuddT(N); E = cuddE(N); - if (Cudd_IsComplement(node)) { - T = Cudd_Not(T); E = Cudd_Not(E); - } - if (T == bzero) { - string[N->index] = 0; - node = E; - } else if (E == bzero) { - string[N->index] = 1; - node = T; - } else { - dir = (char) ((Cudd_Random() & 0x2000) >> 13); - string[N->index] = dir; - node = dir ? T : E; - } - } - return(1); - -} /* end of Cudd_bddPickOneCube */ - - -/**Function******************************************************************** - - Synopsis [Picks one on-set minterm randomly from the given DD.] - - Description [Picks one on-set minterm randomly from the given - DD. The minterm is in terms of <code>vars</code>. The array - <code>vars</code> should contain at least all variables in the - support of <code>f</code>; if this condition is not met the minterm - built by this procedure may not be contained in - <code>f</code>. Builds a BDD for the minterm and returns a pointer - to it if successful; NULL otherwise. There are three reasons why the - procedure may fail: - <ul> - <li> It may run out of memory; - <li> the function <code>f</code> may be the constant 0; - <li> the minterm may not be contained in <code>f</code>. - </ul>] - - SideEffects [None] - - SeeAlso [Cudd_bddPickOneCube] - -******************************************************************************/ -DdNode * -Cudd_bddPickOneMinterm( - DdManager * dd /* manager */, - DdNode * f /* function from which to pick one minterm */, - DdNode ** vars /* array of variables */, - int n /* size of <code>vars</code> */) -{ - char *string; - int i, size; - int *indices; - int result; - DdNode *old, *neW; - - size = dd->size; - string = ALLOC(char, size); - if (string == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - return(NULL); - } - indices = ALLOC(int,n); - if (indices == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - FREE(string); - return(NULL); - } - - for (i = 0; i < n; i++) { - indices[i] = vars[i]->index; - } - - result = Cudd_bddPickOneCube(dd,f,string); - if (result == 0) { - FREE(string); - FREE(indices); - return(NULL); - } - - /* Randomize choice for don't cares. */ - for (i = 0; i < n; i++) { - if (string[indices[i]] == 2) - string[indices[i]] = (char) ((Cudd_Random() & 0x20) >> 5); - } - - /* Build result BDD. */ - old = Cudd_ReadOne(dd); - cuddRef(old); - - for (i = n-1; i >= 0; i--) { - neW = Cudd_bddAnd(dd,old,Cudd_NotCond(vars[i],string[indices[i]]==0)); - if (neW == NULL) { - FREE(string); - FREE(indices); - Cudd_RecursiveDeref(dd,old); - return(NULL); - } - cuddRef(neW); - Cudd_RecursiveDeref(dd,old); - old = neW; - } - -#ifdef DD_DEBUG - /* Test. */ - if (Cudd_bddLeq(dd,old,f)) { - cuddDeref(old); - } else { - Cudd_RecursiveDeref(dd,old); - old = NULL; - } -#else - cuddDeref(old); -#endif - - FREE(string); - FREE(indices); - return(old); - -} /* end of Cudd_bddPickOneMinterm */ - - -/**Function******************************************************************** - - Synopsis [Picks k on-set minterms evenly distributed from given DD.] - - Description [Picks k on-set minterms evenly distributed from given DD. - The minterms are in terms of <code>vars</code>. The array - <code>vars</code> should contain at least all variables in the - support of <code>f</code>; if this condition is not met the minterms - built by this procedure may not be contained in - <code>f</code>. Builds an array of BDDs for the minterms and returns a - pointer to it if successful; NULL otherwise. There are three reasons - why the procedure may fail: - <ul> - <li> It may run out of memory; - <li> the function <code>f</code> may be the constant 0; - <li> the minterms may not be contained in <code>f</code>. - </ul>] - - SideEffects [None] - - SeeAlso [Cudd_bddPickOneMinterm Cudd_bddPickOneCube] - -******************************************************************************/ -DdNode ** -Cudd_bddPickArbitraryMinterms( - DdManager * dd /* manager */, - DdNode * f /* function from which to pick k minterms */, - DdNode ** vars /* array of variables */, - int n /* size of <code>vars</code> */, - int k /* number of minterms to find */) -{ - char **string; - int i, j, l, size; - int *indices; - int result; - DdNode **old, *neW; - double minterms; - char *saveString; - int saveFlag, savePoint, isSame; - - minterms = Cudd_CountMinterm(dd,f,n); - if ((double)k > minterms) { - return(NULL); - } - - size = dd->size; - string = ALLOC(char *, k); - if (string == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - return(NULL); - } - for (i = 0; i < k; i++) { - string[i] = ALLOC(char, size + 1); - if (string[i] == NULL) { - for (j = 0; j < i; j++) - FREE(string[i]); - FREE(string); - dd->errorCode = CUDD_MEMORY_OUT; - return(NULL); - } - for (j = 0; j < size; j++) string[i][j] = '2'; - string[i][size] = '\0'; - } - indices = ALLOC(int,n); - if (indices == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - for (i = 0; i < k; i++) - FREE(string[i]); - FREE(string); - return(NULL); - } - - for (i = 0; i < n; i++) { - indices[i] = vars[i]->index; - } - - result = ddPickArbitraryMinterms(dd,f,n,k,string); - if (result == 0) { - for (i = 0; i < k; i++) - FREE(string[i]); - FREE(string); - FREE(indices); - return(NULL); - } - - old = ALLOC(DdNode *, k); - if (old == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - for (i = 0; i < k; i++) - FREE(string[i]); - FREE(string); - FREE(indices); - return(NULL); - } - saveString = ALLOC(char, size + 1); - if (saveString == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - for (i = 0; i < k; i++) - FREE(string[i]); - FREE(string); - FREE(indices); - FREE(old); - return(NULL); - } - saveFlag = 0; - - /* Build result BDD array. */ - for (i = 0; i < k; i++) { - isSame = 0; - if (!saveFlag) { - for (j = i + 1; j < k; j++) { - if (strcmp(string[i], string[j]) == 0) { - savePoint = i; - strcpy(saveString, string[i]); - saveFlag = 1; - break; - } - } - } else { - if (strcmp(string[i], saveString) == 0) { - isSame = 1; - } else { - saveFlag = 0; - for (j = i + 1; j < k; j++) { - if (strcmp(string[i], string[j]) == 0) { - savePoint = i; - strcpy(saveString, string[i]); - saveFlag = 1; - break; - } - } - } - } - /* Randomize choice for don't cares. */ - for (j = 0; j < n; j++) { - if (string[i][indices[j]] == '2') - string[i][indices[j]] = (Cudd_Random() & 0x20) ? '1' : '0'; - } - - while (isSame) { - isSame = 0; - for (j = savePoint; j < i; j++) { - if (strcmp(string[i], string[j]) == 0) { - isSame = 1; - break; - } - } - if (isSame) { - strcpy(string[i], saveString); - /* Randomize choice for don't cares. */ - for (j = 0; j < n; j++) { - if (string[i][indices[j]] == '2') - string[i][indices[j]] = (Cudd_Random() & 0x20) ? - '1' : '0'; - } - } - } - - old[i] = Cudd_ReadOne(dd); - cuddRef(old[i]); - - for (j = 0; j < n; j++) { - if (string[i][indices[j]] == '0') { - neW = Cudd_bddAnd(dd,old[i],Cudd_Not(vars[j])); - } else { - neW = Cudd_bddAnd(dd,old[i],vars[j]); - } - if (neW == NULL) { - FREE(saveString); - for (l = 0; l < k; l++) - FREE(string[l]); - FREE(string); - FREE(indices); - for (l = 0; l <= i; l++) - Cudd_RecursiveDeref(dd,old[l]); - FREE(old); - return(NULL); - } - cuddRef(neW); - Cudd_RecursiveDeref(dd,old[i]); - old[i] = neW; - } - - /* Test. */ - if (!Cudd_bddLeq(dd,old[i],f)) { - FREE(saveString); - for (l = 0; l < k; l++) - FREE(string[l]); - FREE(string); - FREE(indices); - for (l = 0; l <= i; l++) - Cudd_RecursiveDeref(dd,old[l]); - FREE(old); - return(NULL); - } - } - - FREE(saveString); - for (i = 0; i < k; i++) { - cuddDeref(old[i]); - FREE(string[i]); - } - FREE(string); - FREE(indices); - return(old); - -} /* end of Cudd_bddPickArbitraryMinterms */ - - -/**Function******************************************************************** - - Synopsis [Extracts a subset from a BDD.] - - Description [Extracts a subset from a BDD in the following procedure. - 1. Compute the weight for each mask variable by counting the number of - minterms for both positive and negative cofactors of the BDD with - respect to each mask variable. (weight = #positive - #negative) - 2. Find a representative cube of the BDD by using the weight. From the - top variable of the BDD, for each variable, if the weight is greater - than 0.0, choose THEN branch, othereise ELSE branch, until meeting - the constant 1. - 3. Quantify out the variables not in maskVars from the representative - cube and if a variable in maskVars is don't care, replace the - variable with a constant(1 or 0) depending on the weight. - 4. Make a subset of the BDD by multiplying with the modified cube.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -DdNode * -Cudd_SubsetWithMaskVars( - DdManager * dd /* manager */, - DdNode * f /* function from which to pick a cube */, - DdNode ** vars /* array of variables */, - int nvars /* size of <code>vars</code> */, - DdNode ** maskVars /* array of variables */, - int mvars /* size of <code>maskVars</code> */) -{ - double *weight; - char *string; - int i, size; - int *indices, *mask; - int result; - DdNode *zero, *cube, *newCube, *subset; - DdNode *cof; - - DdNode *support; - support = Cudd_Support(dd,f); - cuddRef(support); - Cudd_RecursiveDeref(dd,support); - - zero = Cudd_Not(dd->one); - size = dd->size; - - weight = ALLOC(double,size); - if (weight == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - return(NULL); - } - for (i = 0; i < size; i++) { - weight[i] = 0.0; - } - for (i = 0; i < mvars; i++) { - cof = Cudd_Cofactor(dd, f, maskVars[i]); - cuddRef(cof); - weight[i] = Cudd_CountMinterm(dd, cof, nvars); - Cudd_RecursiveDeref(dd,cof); - - cof = Cudd_Cofactor(dd, f, Cudd_Not(maskVars[i])); - cuddRef(cof); - weight[i] -= Cudd_CountMinterm(dd, cof, nvars); - Cudd_RecursiveDeref(dd,cof); - } - - string = ALLOC(char, size + 1); - if (string == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - return(NULL); - } - mask = ALLOC(int, size); - if (mask == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - FREE(string); - return(NULL); - } - for (i = 0; i < size; i++) { - string[i] = '2'; - mask[i] = 0; - } - string[size] = '\0'; - indices = ALLOC(int,nvars); - if (indices == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - FREE(string); - FREE(mask); - return(NULL); - } - for (i = 0; i < nvars; i++) { - indices[i] = vars[i]->index; - } - - result = ddPickRepresentativeCube(dd,f,nvars,weight,string); - if (result == 0) { - FREE(string); - FREE(mask); - FREE(indices); - return(NULL); - } - - cube = Cudd_ReadOne(dd); - cuddRef(cube); - zero = Cudd_Not(Cudd_ReadOne(dd)); - for (i = 0; i < nvars; i++) { - if (string[indices[i]] == '0') { - newCube = Cudd_bddIte(dd,cube,Cudd_Not(vars[i]),zero); - } else if (string[indices[i]] == '1') { - newCube = Cudd_bddIte(dd,cube,vars[i],zero); - } else - continue; - if (newCube == NULL) { - FREE(string); - FREE(mask); - FREE(indices); - Cudd_RecursiveDeref(dd,cube); - return(NULL); - } - cuddRef(newCube); - Cudd_RecursiveDeref(dd,cube); - cube = newCube; - } - Cudd_RecursiveDeref(dd,cube); - - for (i = 0; i < mvars; i++) { - mask[maskVars[i]->index] = 1; - } - for (i = 0; i < nvars; i++) { - if (mask[indices[i]]) { - if (string[indices[i]] == '2') { - if (weight[indices[i]] >= 0.0) - string[indices[i]] = '1'; - else - string[indices[i]] = '0'; - } - } else { - string[indices[i]] = '2'; - } - } - - cube = Cudd_ReadOne(dd); - cuddRef(cube); - zero = Cudd_Not(Cudd_ReadOne(dd)); - - /* Build result BDD. */ - for (i = 0; i < nvars; i++) { - if (string[indices[i]] == '0') { - newCube = Cudd_bddIte(dd,cube,Cudd_Not(vars[i]),zero); - } else if (string[indices[i]] == '1') { - newCube = Cudd_bddIte(dd,cube,vars[i],zero); - } else - continue; - if (newCube == NULL) { - FREE(string); - FREE(mask); - FREE(indices); - Cudd_RecursiveDeref(dd,cube); - return(NULL); - } - cuddRef(newCube); - Cudd_RecursiveDeref(dd,cube); - cube = newCube; - } - - subset = Cudd_bddAnd(dd,f,cube); - cuddRef(subset); - Cudd_RecursiveDeref(dd,cube); - - /* Test. */ - if (Cudd_bddLeq(dd,subset,f)) { - cuddDeref(subset); - } else { - Cudd_RecursiveDeref(dd,subset); - subset = NULL; - } - - FREE(string); - FREE(mask); - FREE(indices); - FREE(weight); - return(subset); - -} /* end of Cudd_SubsetWithMaskVars */ - - -/**Function******************************************************************** - - Synopsis [Finds the first cube of a decision diagram.] - - Description [Defines an iterator on the onset of a decision diagram - and finds its first cube. Returns a generator that contains the - information necessary to continue the enumeration if successful; NULL - otherwise.<p> - A cube is represented as an array of literals, which are integers in - {0, 1, 2}; 0 represents a complemented literal, 1 represents an - uncomplemented literal, and 2 stands for don't care. The enumeration - produces a disjoint cover of the function associated with the diagram. - The size of the array equals the number of variables in the manager at - the time Cudd_FirstCube is called.<p> - For each cube, a value is also returned. This value is always 1 for a - BDD, while it may be different from 1 for an ADD. - For BDDs, the offset is the set of cubes whose value is the logical zero. - For ADDs, the offset is the set of cubes whose value is the - background value. The cubes of the offset are not enumerated.] - - SideEffects [The first cube and its value are returned as side effects.] - - SeeAlso [Cudd_ForeachCube Cudd_NextCube Cudd_GenFree Cudd_IsGenEmpty - Cudd_FirstNode] - -******************************************************************************/ -DdGen * -Cudd_FirstCube( - DdManager * dd, - DdNode * f, - int ** cube, - CUDD_VALUE_TYPE * value) -{ - DdGen *gen; - DdNode *top, *treg, *next, *nreg, *prev, *preg; - int i; - int nvars; - - /* Sanity Check. */ - if (dd == NULL || f == NULL) return(NULL); - - /* Allocate generator an initialize it. */ - gen = ALLOC(DdGen,1); - if (gen == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - return(NULL); - } - - gen->manager = dd; - gen->type = CUDD_GEN_CUBES; - gen->status = CUDD_GEN_EMPTY; - gen->gen.cubes.cube = NULL; - gen->gen.cubes.value = DD_ZERO_VAL; - gen->stack.sp = 0; - gen->stack.stack = NULL; - gen->node = NULL; - - nvars = dd->size; - gen->gen.cubes.cube = ALLOC(int,nvars); - if (gen->gen.cubes.cube == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - FREE(gen); - return(NULL); - } - for (i = 0; i < nvars; i++) gen->gen.cubes.cube[i] = 2; - - /* The maximum stack depth is one plus the number of variables. - ** because a path may have nodes at all levels, including the - ** constant level. - */ - gen->stack.stack = ALLOC(DdNode *, nvars+1); - if (gen->stack.stack == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - FREE(gen->gen.cubes.cube); - FREE(gen); - return(NULL); - } - for (i = 0; i <= nvars; i++) gen->stack.stack[i] = NULL; - - /* Find the first cube of the onset. */ - gen->stack.stack[gen->stack.sp] = f; gen->stack.sp++; - - while (1) { - top = gen->stack.stack[gen->stack.sp-1]; - treg = Cudd_Regular(top); - if (!cuddIsConstant(treg)) { - /* Take the else branch first. */ - gen->gen.cubes.cube[treg->index] = 0; - next = cuddE(treg); - if (top != treg) next = Cudd_Not(next); - gen->stack.stack[gen->stack.sp] = next; gen->stack.sp++; - } else if (top == Cudd_Not(DD_ONE(dd)) || top == dd->background) { - /* Backtrack */ - while (1) { - if (gen->stack.sp == 1) { - /* The current node has no predecessor. */ - gen->status = CUDD_GEN_EMPTY; - gen->stack.sp--; - goto done; - } - prev = gen->stack.stack[gen->stack.sp-2]; - preg = Cudd_Regular(prev); - nreg = cuddT(preg); - if (prev != preg) {next = Cudd_Not(nreg);} else {next = nreg;} - if (next != top) { /* follow the then branch next */ - gen->gen.cubes.cube[preg->index] = 1; - gen->stack.stack[gen->stack.sp-1] = next; - break; - } - /* Pop the stack and try again. */ - gen->gen.cubes.cube[preg->index] = 2; - gen->stack.sp--; - top = gen->stack.stack[gen->stack.sp-1]; - treg = Cudd_Regular(top); - } - } else { - gen->status = CUDD_GEN_NONEMPTY; - gen->gen.cubes.value = cuddV(top); - goto done; - } - } - -done: - *cube = gen->gen.cubes.cube; - *value = gen->gen.cubes.value; - return(gen); - -} /* end of Cudd_FirstCube */ - - -/**Function******************************************************************** - - Synopsis [Generates the next cube of a decision diagram onset.] - - Description [Generates the next cube of a decision diagram onset, - using generator gen. Returns 0 if the enumeration is completed; 1 - otherwise.] - - SideEffects [The cube and its value are returned as side effects. The - generator is modified.] - - SeeAlso [Cudd_ForeachCube Cudd_FirstCube Cudd_GenFree Cudd_IsGenEmpty - Cudd_NextNode] - -******************************************************************************/ -int -Cudd_NextCube( - DdGen * gen, - int ** cube, - CUDD_VALUE_TYPE * value) -{ - DdNode *top, *treg, *next, *nreg, *prev, *preg; - DdManager *dd = gen->manager; - - /* Backtrack from previously reached terminal node. */ - while (1) { - if (gen->stack.sp == 1) { - /* The current node has no predecessor. */ - gen->status = CUDD_GEN_EMPTY; - gen->stack.sp--; - goto done; - } - top = gen->stack.stack[gen->stack.sp-1]; - treg = Cudd_Regular(top); - prev = gen->stack.stack[gen->stack.sp-2]; - preg = Cudd_Regular(prev); - nreg = cuddT(preg); - if (prev != preg) {next = Cudd_Not(nreg);} else {next = nreg;} - if (next != top) { /* follow the then branch next */ - gen->gen.cubes.cube[preg->index] = 1; - gen->stack.stack[gen->stack.sp-1] = next; - break; - } - /* Pop the stack and try again. */ - gen->gen.cubes.cube[preg->index] = 2; - gen->stack.sp--; - } - - while (1) { - top = gen->stack.stack[gen->stack.sp-1]; - treg = Cudd_Regular(top); - if (!cuddIsConstant(treg)) { - /* Take the else branch first. */ - gen->gen.cubes.cube[treg->index] = 0; - next = cuddE(treg); - if (top != treg) next = Cudd_Not(next); - gen->stack.stack[gen->stack.sp] = next; gen->stack.sp++; - } else if (top == Cudd_Not(DD_ONE(dd)) || top == dd->background) { - /* Backtrack */ - while (1) { - if (gen->stack.sp == 1) { - /* The current node has no predecessor. */ - gen->status = CUDD_GEN_EMPTY; - gen->stack.sp--; - goto done; - } - prev = gen->stack.stack[gen->stack.sp-2]; - preg = Cudd_Regular(prev); - nreg = cuddT(preg); - if (prev != preg) {next = Cudd_Not(nreg);} else {next = nreg;} - if (next != top) { /* follow the then branch next */ - gen->gen.cubes.cube[preg->index] = 1; - gen->stack.stack[gen->stack.sp-1] = next; - break; - } - /* Pop the stack and try again. */ - gen->gen.cubes.cube[preg->index] = 2; - gen->stack.sp--; - top = gen->stack.stack[gen->stack.sp-1]; - treg = Cudd_Regular(top); - } - } else { - gen->status = CUDD_GEN_NONEMPTY; - gen->gen.cubes.value = cuddV(top); - goto done; - } - } - -done: - if (gen->status == CUDD_GEN_EMPTY) return(0); - *cube = gen->gen.cubes.cube; - *value = gen->gen.cubes.value; - return(1); - -} /* end of Cudd_NextCube */ - - -/**Function******************************************************************** - - Synopsis [Computes the cube of an array of BDD variables.] - - Description [Computes the cube of an array of BDD variables. If - non-null, the phase argument indicates which literal of each - variable should appear in the cube. If phase\[i\] is nonzero, then the - positive literal is used. If phase is NULL, the cube is positive unate. - Returns a pointer to the result if successful; NULL otherwise.] - - SideEffects [None] - - SeeAlso [Cudd_addComputeCube Cudd_IndicesToCube Cudd_CubeArrayToBdd] - -******************************************************************************/ -DdNode * -Cudd_bddComputeCube( - DdManager * dd, - DdNode ** vars, - int * phase, - int n) -{ - DdNode *cube; - DdNode *fn; - int i; - - cube = DD_ONE(dd); - cuddRef(cube); - - for (i = n - 1; i >= 0; i--) { - if (phase == NULL || phase[i] != 0) { - fn = Cudd_bddAnd(dd,vars[i],cube); - } else { - fn = Cudd_bddAnd(dd,Cudd_Not(vars[i]),cube); - } - if (fn == NULL) { - Cudd_RecursiveDeref(dd,cube); - return(NULL); - } - cuddRef(fn); - Cudd_RecursiveDeref(dd,cube); - cube = fn; - } - cuddDeref(cube); - - return(cube); - -} /* end of Cudd_bddComputeCube */ - - -/**Function******************************************************************** - - Synopsis [Computes the cube of an array of ADD variables.] - - Description [Computes the cube of an array of ADD variables. If - non-null, the phase argument indicates which literal of each - variable should appear in the cube. If phase\[i\] is nonzero, then the - positive literal is used. If phase is NULL, the cube is positive unate. - Returns a pointer to the result if successful; NULL otherwise.] - - SideEffects [none] - - SeeAlso [Cudd_bddComputeCube] - -******************************************************************************/ -DdNode * -Cudd_addComputeCube( - DdManager * dd, - DdNode ** vars, - int * phase, - int n) -{ - DdNode *cube, *zero; - DdNode *fn; - int i; - - cube = DD_ONE(dd); - cuddRef(cube); - zero = DD_ZERO(dd); - - for (i = n - 1; i >= 0; i--) { - if (phase == NULL || phase[i] != 0) { - fn = Cudd_addIte(dd,vars[i],cube,zero); - } else { - fn = Cudd_addIte(dd,vars[i],zero,cube); - } - if (fn == NULL) { - Cudd_RecursiveDeref(dd,cube); - return(NULL); - } - cuddRef(fn); - Cudd_RecursiveDeref(dd,cube); - cube = fn; - } - cuddDeref(cube); - - return(cube); - -} /* end of Cudd_addComputeCube */ - - -/**Function******************************************************************** - - Synopsis [Builds the BDD of a cube from a positional array.] - - Description [Builds a cube from a positional array. The array must - have one integer entry for each BDD variable. If the i-th entry is - 1, the variable of index i appears in true form in the cube; If the - i-th entry is 0, the variable of index i appears complemented in the - cube; otherwise the variable does not appear in the cube. Returns a - pointer to the BDD for the cube if successful; NULL otherwise.] - - SideEffects [None] - - SeeAlso [Cudd_bddComputeCube Cudd_IndicesToCube Cudd_BddToCubeArray] - -******************************************************************************/ -DdNode * -Cudd_CubeArrayToBdd( - DdManager *dd, - int *array) -{ - DdNode *cube, *var, *tmp; - int i; - int size = Cudd_ReadSize(dd); - - cube = DD_ONE(dd); - cuddRef(cube); - for (i = size - 1; i >= 0; i--) { - if ((array[i] & ~1) == 0) { - var = Cudd_bddIthVar(dd,i); - tmp = Cudd_bddAnd(dd,cube,Cudd_NotCond(var,array[i]==0)); - if (tmp == NULL) { - Cudd_RecursiveDeref(dd,cube); - return(NULL); - } - cuddRef(tmp); - Cudd_RecursiveDeref(dd,cube); - cube = tmp; - } - } - cuddDeref(cube); - return(cube); - -} /* end of Cudd_CubeArrayToBdd */ - - -/**Function******************************************************************** - - Synopsis [Builds a positional array from the BDD of a cube.] - - Description [Builds a positional array from the BDD of a cube. - Array must have one entry for each BDD variable. The positional - array has 1 in i-th position if the variable of index i appears in - true form in the cube; it has 0 in i-th position if the variable of - index i appears in complemented form in the cube; finally, it has 2 - in i-th position if the variable of index i does not appear in the - cube. Returns 1 if successful (the BDD is indeed a cube); 0 - otherwise.] - - SideEffects [The result is in the array passed by reference.] - - SeeAlso [Cudd_CubeArrayToBdd] - -******************************************************************************/ -int -Cudd_BddToCubeArray( - DdManager *dd, - DdNode *cube, - int *array) -{ - DdNode *scan, *t, *e; - int i; - int size = Cudd_ReadSize(dd); - DdNode *zero = Cudd_Not(DD_ONE(dd)); - - for (i = size-1; i >= 0; i--) { - array[i] = 2; - } - scan = cube; - while (!Cudd_IsConstant(scan)) { - int index = Cudd_Regular(scan)->index; - cuddGetBranches(scan,&t,&e); - if (t == zero) { - array[index] = 0; - scan = e; - } else if (e == zero) { - array[index] = 1; - scan = t; - } else { - return(0); /* cube is not a cube */ - } - } - if (scan == zero) { - return(0); - } else { - return(1); - } - -} /* end of Cudd_BddToCubeArray */ - - -/**Function******************************************************************** - - Synopsis [Finds the first node of a decision diagram.] - - Description [Defines an iterator on the nodes of a decision diagram - and finds its first node. Returns a generator that contains the - information necessary to continue the enumeration if successful; NULL - otherwise.] - - SideEffects [The first node is returned as a side effect.] - - SeeAlso [Cudd_ForeachNode Cudd_NextNode Cudd_GenFree Cudd_IsGenEmpty - Cudd_FirstCube] - -******************************************************************************/ -DdGen * -Cudd_FirstNode( - DdManager * dd, - DdNode * f, - DdNode ** node) -{ - DdGen *gen; - int retval; - - /* Sanity Check. */ - if (dd == NULL || f == NULL) return(NULL); - - /* Allocate generator an initialize it. */ - gen = ALLOC(DdGen,1); - if (gen == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - return(NULL); - } - - gen->manager = dd; - gen->type = CUDD_GEN_NODES; - gen->status = CUDD_GEN_EMPTY; - gen->gen.nodes.visited = NULL; - gen->gen.nodes.stGen = NULL; - gen->stack.sp = 0; - gen->stack.stack = NULL; - gen->node = NULL; - - gen->gen.nodes.visited = st_init_table(st_ptrcmp,st_ptrhash); - if (gen->gen.nodes.visited == NULL) { - FREE(gen); - return(NULL); - } - - /* Collect all the nodes in a st table for later perusal. */ - retval = cuddCollectNodes(Cudd_Regular(f),gen->gen.nodes.visited); - if (retval == 0) { - st_free_table(gen->gen.nodes.visited); - FREE(gen); - return(NULL); - } - - /* Initialize the st table generator. */ - gen->gen.nodes.stGen = st_init_gen(gen->gen.nodes.visited); - if (gen->gen.nodes.stGen == NULL) { - st_free_table(gen->gen.nodes.visited); - FREE(gen); - return(NULL); - } - - /* Find the first node. */ - retval = st_gen(gen->gen.nodes.stGen, (char **) &(gen->node), NULL); - if (retval != 0) { - gen->status = CUDD_GEN_NONEMPTY; - *node = gen->node; - } - - return(gen); - -} /* end of Cudd_FirstNode */ - - -/**Function******************************************************************** - - Synopsis [Finds the next node of a decision diagram.] - - Description [Finds the node of a decision diagram, using generator - gen. Returns 0 if the enumeration is completed; 1 otherwise.] - - SideEffects [The next node is returned as a side effect.] - - SeeAlso [Cudd_ForeachNode Cudd_FirstNode Cudd_GenFree Cudd_IsGenEmpty - Cudd_NextCube] - -******************************************************************************/ -int -Cudd_NextNode( - DdGen * gen, - DdNode ** node) -{ - int retval; - - /* Find the next node. */ - retval = st_gen(gen->gen.nodes.stGen, (char **) &(gen->node), NULL); - if (retval == 0) { - gen->status = CUDD_GEN_EMPTY; - } else { - *node = gen->node; - } - - return(retval); - -} /* end of Cudd_NextNode */ - - -/**Function******************************************************************** - - Synopsis [Frees a CUDD generator.] - - Description [Frees a CUDD generator. Always returns 0, so that it can - be used in mis-like foreach constructs.] - - SideEffects [None] - - SeeAlso [Cudd_ForeachCube Cudd_ForeachNode Cudd_FirstCube Cudd_NextCube - Cudd_FirstNode Cudd_NextNode Cudd_IsGenEmpty] - -******************************************************************************/ -int -Cudd_GenFree( - DdGen * gen) -{ - - if (gen == NULL) return(0); - switch (gen->type) { - case CUDD_GEN_CUBES: - case CUDD_GEN_ZDD_PATHS: - FREE(gen->gen.cubes.cube); - FREE(gen->stack.stack); - break; - case CUDD_GEN_NODES: - st_free_gen(gen->gen.nodes.stGen); - st_free_table(gen->gen.nodes.visited); - break; - default: - return(0); - } - FREE(gen); - return(0); - -} /* end of Cudd_GenFree */ - - -/**Function******************************************************************** - - Synopsis [Queries the status of a generator.] - - Description [Queries the status of a generator. Returns 1 if the - generator is empty or NULL; 0 otherswise.] - - SideEffects [None] - - SeeAlso [Cudd_ForeachCube Cudd_ForeachNode Cudd_FirstCube Cudd_NextCube - Cudd_FirstNode Cudd_NextNode Cudd_GenFree] - -******************************************************************************/ -int -Cudd_IsGenEmpty( - DdGen * gen) -{ - if (gen == NULL) return(1); - return(gen->status == CUDD_GEN_EMPTY); - -} /* end of Cudd_IsGenEmpty */ - - -/**Function******************************************************************** - - Synopsis [Builds a cube of BDD variables from an array of indices.] - - Description [Builds a cube of BDD variables from an array of indices. - Returns a pointer to the result if successful; NULL otherwise.] - - SideEffects [None] - - SeeAlso [Cudd_bddComputeCube Cudd_CubeArrayToBdd] - -******************************************************************************/ -DdNode * -Cudd_IndicesToCube( - DdManager * dd, - int * array, - int n) -{ - DdNode *cube, *tmp; - int i; - - cube = DD_ONE(dd); - cuddRef(cube); - for (i = n - 1; i >= 0; i--) { - tmp = Cudd_bddAnd(dd,Cudd_bddIthVar(dd,array[i]),cube); - if (tmp == NULL) { - Cudd_RecursiveDeref(dd,cube); - return(NULL); - } - cuddRef(tmp); - Cudd_RecursiveDeref(dd,cube); - cube = tmp; - } - - cuddDeref(cube); - return(cube); - -} /* end of Cudd_IndicesToCube */ - - -/**Function******************************************************************** - - Synopsis [Prints the package version number.] - - Description [] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -void -Cudd_PrintVersion( - FILE * fp) -{ - (void) fprintf(fp, "%s\n", CUDD_VERSION); - -} /* end of Cudd_PrintVersion */ - - -/**Function******************************************************************** - - Synopsis [Computes the average distance between adjacent nodes.] - - Description [Computes the average distance between adjacent nodes in - the manager. Adjacent nodes are node pairs such that the second node - is the then child, else child, or next node in the collision list.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -double -Cudd_AverageDistance( - DdManager * dd) -{ - double tetotal, nexttotal; - double tesubtotal, nextsubtotal; - double temeasured, nextmeasured; - int i, j; - int slots, nvars; - long diff; - DdNode *scan; - DdNodePtr *nodelist; - DdNode *sentinel = &(dd->sentinel); - - nvars = dd->size; - if (nvars == 0) return(0.0); - - /* Initialize totals. */ - tetotal = 0.0; - nexttotal = 0.0; - temeasured = 0.0; - nextmeasured = 0.0; - - /* Scan the variable subtables. */ - for (i = 0; i < nvars; i++) { - nodelist = dd->subtables[i].nodelist; - tesubtotal = 0.0; - nextsubtotal = 0.0; - slots = dd->subtables[i].slots; - for (j = 0; j < slots; j++) { - scan = nodelist[j]; - while (scan != sentinel) { - diff = (long) scan - (long) cuddT(scan); - tesubtotal += (double) ddAbs(diff); - diff = (long) scan - (long) Cudd_Regular(cuddE(scan)); - tesubtotal += (double) ddAbs(diff); - temeasured += 2.0; - if (scan->next != NULL) { - diff = (long) scan - (long) scan->next; - nextsubtotal += (double) ddAbs(diff); - nextmeasured += 1.0; - } - scan = scan->next; - } - } - tetotal += tesubtotal; - nexttotal += nextsubtotal; - } - - /* Scan the constant table. */ - nodelist = dd->constants.nodelist; - nextsubtotal = 0.0; - slots = dd->constants.slots; - for (j = 0; j < slots; j++) { - scan = nodelist[j]; - while (scan != NULL) { - if (scan->next != NULL) { - diff = (long) scan - (long) scan->next; - nextsubtotal += (double) ddAbs(diff); - nextmeasured += 1.0; - } - scan = scan->next; - } - } - nexttotal += nextsubtotal; - - return((tetotal + nexttotal) / (temeasured + nextmeasured)); - -} /* end of Cudd_AverageDistance */ - - -/**Function******************************************************************** - - Synopsis [Portable random number generator.] - - Description [Portable number generator based on ran2 from "Numerical - Recipes in C." It is a long period (> 2 * 10^18) random number generator - of L'Ecuyer with Bays-Durham shuffle. Returns a long integer uniformly - distributed between 0 and 2147483561 (inclusive of the endpoint values). - The random generator can be explicitly initialized by calling - Cudd_Srandom. If no explicit initialization is performed, then the - seed 1 is assumed.] - - SideEffects [None] - - SeeAlso [Cudd_Srandom] - -******************************************************************************/ -long -Cudd_Random( - ) -{ - int i; /* index in the shuffle table */ - long int w; /* work variable */ - - /* cuddRand == 0 if the geneartor has not been initialized yet. */ - if (cuddRand == 0) Cudd_Srandom(1); - - /* Compute cuddRand = (cuddRand * LEQA1) % MODULUS1 avoiding - ** overflows by Schrage's method. - */ - w = cuddRand / LEQQ1; - cuddRand = LEQA1 * (cuddRand - w * LEQQ1) - w * LEQR1; - cuddRand += (cuddRand < 0) * MODULUS1; - - /* Compute cuddRand2 = (cuddRand2 * LEQA2) % MODULUS2 avoiding - ** overflows by Schrage's method. - */ - w = cuddRand2 / LEQQ2; - cuddRand2 = LEQA2 * (cuddRand2 - w * LEQQ2) - w * LEQR2; - cuddRand2 += (cuddRand2 < 0) * MODULUS2; - - /* cuddRand is shuffled with the Bays-Durham algorithm. - ** shuffleSelect and cuddRand2 are combined to generate the output. - */ - - /* Pick one element from the shuffle table; "i" will be in the range - ** from 0 to STAB_SIZE-1. - */ - i = (int) (shuffleSelect / STAB_DIV); - /* Mix the element of the shuffle table with the current iterate of - ** the second sub-generator, and replace the chosen element of the - ** shuffle table with the current iterate of the first sub-generator. - */ - shuffleSelect = shuffleTable[i] - cuddRand2; - shuffleTable[i] = cuddRand; - shuffleSelect += (shuffleSelect < 1) * (MODULUS1 - 1); - /* Since shuffleSelect != 0, and we want to be able to return 0, - ** here we subtract 1 before returning. - */ - return(shuffleSelect - 1); - -} /* end of Cudd_Random */ - - -/**Function******************************************************************** - - Synopsis [Initializer for the portable random number generator.] - - Description [Initializer for the portable number generator based on - ran2 in "Numerical Recipes in C." The input is the seed for the - generator. If it is negative, its absolute value is taken as seed. - If it is 0, then 1 is taken as seed. The initialized sets up the two - recurrences used to generate a long-period stream, and sets up the - shuffle table.] - - SideEffects [None] - - SeeAlso [Cudd_Random] - -******************************************************************************/ -void -Cudd_Srandom( - long seed) -{ - int i; - - if (seed < 0) cuddRand = -seed; - else if (seed == 0) cuddRand = 1; - else cuddRand = seed; - cuddRand2 = cuddRand; - /* Load the shuffle table (after 11 warm-ups). */ - for (i = 0; i < STAB_SIZE + 11; i++) { - long int w; - w = cuddRand / LEQQ1; - cuddRand = LEQA1 * (cuddRand - w * LEQQ1) - w * LEQR1; - cuddRand += (cuddRand < 0) * MODULUS1; - shuffleTable[i % STAB_SIZE] = cuddRand; - } - shuffleSelect = shuffleTable[1 % STAB_SIZE]; - -} /* end of Cudd_Srandom */ - - -/**Function******************************************************************** - - Synopsis [Computes the density of a BDD or ADD.] - - Description [Computes the density of a BDD or ADD. The density is - the ratio of the number of minterms to the number of nodes. If 0 is - passed as number of variables, the number of variables existing in - the manager is used. Returns the density if successful; (double) - CUDD_OUT_OF_MEM otherwise.] - - SideEffects [None] - - SeeAlso [Cudd_CountMinterm Cudd_DagSize] - -******************************************************************************/ -double -Cudd_Density( - DdManager * dd /* manager */, - DdNode * f /* function whose density is sought */, - int nvars /* size of the support of f */) -{ - double minterms; - int nodes; - double density; - - if (nvars == 0) nvars = dd->size; - minterms = Cudd_CountMinterm(dd,f,nvars); - if (minterms == (double) CUDD_OUT_OF_MEM) return(minterms); - nodes = Cudd_DagSize(f); - density = minterms / (double) nodes; - return(density); - -} /* end of Cudd_Density */ - - -/**Function******************************************************************** - - Synopsis [Warns that a memory allocation failed.] - - Description [Warns that a memory allocation failed. - This function can be used as replacement of MMout_of_memory to prevent - the safe_mem functions of the util package from exiting when malloc - returns NULL. One possible use is in case of discretionary allocations; - for instance, the allocation of memory to enlarge the computed table.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -void -Cudd_OutOfMem( - long size /* size of the allocation that failed */) -{ - (void) fflush(stdout); - (void) fprintf(stderr, "\nunable to allocate %ld bytes\n", size); - return; - -} /* end of Cudd_OutOfMem */ - - -/*---------------------------------------------------------------------------*/ -/* Definition of internal functions */ -/*---------------------------------------------------------------------------*/ - - -/**Function******************************************************************** - - Synopsis [Prints a DD to the standard output. One line per node is - printed.] - - Description [Prints a DD to the standard output. One line per node is - printed. Returns 1 if successful; 0 otherwise.] - - SideEffects [None] - - SeeAlso [Cudd_PrintDebug] - -******************************************************************************/ -int -cuddP( - DdManager * dd, - DdNode * f) -{ - int retval; - st_table *table = st_init_table(st_ptrcmp,st_ptrhash); - - if (table == NULL) return(0); - - retval = dp2(dd,f,table); - st_free_table(table); - (void) fputc('\n',dd->out); - return(retval); - -} /* end of cuddP */ - - -/**Function******************************************************************** - - Synopsis [Frees the memory used to store the minterm counts recorded - in the visited table.] - - Description [Frees the memory used to store the minterm counts - recorded in the visited table. Returns ST_CONTINUE.] - - SideEffects [None] - -******************************************************************************/ -enum st_retval -cuddStCountfree( - char * key, - char * value, - char * arg) -{ - double *d; - - d = (double *)value; - FREE(d); - return(ST_CONTINUE); - -} /* end of cuddStCountfree */ - - -/**Function******************************************************************** - - Synopsis [Recursively collects all the nodes of a DD in a symbol - table.] - - Description [Traverses the BDD f and collects all its nodes in a - symbol table. f is assumed to be a regular pointer and - cuddCollectNodes guarantees this assumption in the recursive calls. - Returns 1 in case of success; 0 otherwise.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -int -cuddCollectNodes( - DdNode * f, - st_table * visited) -{ - DdNode *T, *E; - int retval; - -#ifdef DD_DEBUG - assert(!Cudd_IsComplement(f)); -#endif - - /* If already visited, nothing to do. */ - if (st_is_member(visited, (char *) f) == 1) - return(1); - - /* Check for abnormal condition that should never happen. */ - if (f == NULL) - return(0); - - /* Mark node as visited. */ - if (st_add_direct(visited, (char *) f, NULL) == ST_OUT_OF_MEM) - return(0); - - /* Check terminal case. */ - if (cuddIsConstant(f)) - return(1); - - /* Recursive calls. */ - T = cuddT(f); - retval = cuddCollectNodes(T,visited); - if (retval != 1) return(retval); - E = Cudd_Regular(cuddE(f)); - retval = cuddCollectNodes(E,visited); - return(retval); - -} /* end of cuddCollectNodes */ - - -/*---------------------------------------------------------------------------*/ -/* Definition of static functions */ -/*---------------------------------------------------------------------------*/ - - -/**Function******************************************************************** - - Synopsis [Performs the recursive step of cuddP.] - - Description [Performs the recursive step of cuddP. Returns 1 in case - of success; 0 otherwise.] - - SideEffects [None] - -******************************************************************************/ -static int -dp2( - DdManager *dd, - DdNode * f, - st_table * t) -{ - DdNode *g, *n, *N; - int T,E; - - if (f == NULL) { - return(0); - } - g = Cudd_Regular(f); - if (cuddIsConstant(g)) { -#if SIZEOF_VOID_P == 8 - (void) fprintf(dd->out,"ID = %c0x%lx\tvalue = %-9g\n", bang(f), - (unsigned long) g / (unsigned long) sizeof(DdNode),cuddV(g)); -#else - (void) fprintf(dd->out,"ID = %c0x%x\tvalue = %-9g\n", bang(f), - (unsigned) g / (unsigned) sizeof(DdNode),cuddV(g)); -#endif - return(1); - } - if (st_is_member(t,(char *) g) == 1) { - return(1); - } - if (st_add_direct(t,(char *) g,NULL) == ST_OUT_OF_MEM) - return(0); -#ifdef DD_STATS -#if SIZEOF_VOID_P == 8 - (void) fprintf(dd->out,"ID = %c0x%lx\tindex = %d\tr = %d\t", bang(f), - (unsigned long) g / (unsigned long) sizeof(DdNode), g->index, g->ref); -#else - (void) fprintf(dd->out,"ID = %c0x%x\tindex = %d\tr = %d\t", bang(f), - (unsigned) g / (unsigned) sizeof(DdNode),g->index,g->ref); -#endif -#else -#if SIZEOF_VOID_P == 8 - (void) fprintf(dd->out,"ID = %c0x%lx\tindex = %d\t", bang(f), - (unsigned long) g / (unsigned long) sizeof(DdNode),g->index); -#else - (void) fprintf(dd->out,"ID = %c0x%x\tindex = %d\t", bang(f), - (unsigned) g / (unsigned) sizeof(DdNode),g->index); -#endif -#endif - n = cuddT(g); - if (cuddIsConstant(n)) { - (void) fprintf(dd->out,"T = %-9g\t",cuddV(n)); - T = 1; - } else { -#if SIZEOF_VOID_P == 8 - (void) fprintf(dd->out,"T = 0x%lx\t",(unsigned long) n / (unsigned long) sizeof(DdNode)); -#else - (void) fprintf(dd->out,"T = 0x%x\t",(unsigned) n / (unsigned) sizeof(DdNode)); -#endif - T = 0; - } - - n = cuddE(g); - N = Cudd_Regular(n); - if (cuddIsConstant(N)) { - (void) fprintf(dd->out,"E = %c%-9g\n",bang(n),cuddV(N)); - E = 1; - } else { -#if SIZEOF_VOID_P == 8 - (void) fprintf(dd->out,"E = %c0x%lx\n", bang(n), (unsigned long) N/(unsigned long) sizeof(DdNode)); -#else - (void) fprintf(dd->out,"E = %c0x%x\n", bang(n), (unsigned) N/(unsigned) sizeof(DdNode)); -#endif - E = 0; - } - if (E == 0) { - if (dp2(dd,N,t) == 0) - return(0); - } - if (T == 0) { - if (dp2(dd,cuddT(g),t) == 0) - return(0); - } - return(1); - -} /* end of dp2 */ - - -/**Function******************************************************************** - - Synopsis [Performs the recursive step of Cudd_PrintMinterm.] - - Description [] - - SideEffects [None] - -******************************************************************************/ -static void -ddPrintMintermAux( - DdManager * dd /* manager */, - DdNode * node /* current node */, - int * list /* current recursion path */) -{ - DdNode *N,*Nv,*Nnv; - int i,v,index; - - N = Cudd_Regular(node); - - if (cuddIsConstant(N)) { - /* Terminal case: Print one cube based on the current recursion - ** path, unless we have reached the background value (ADDs) or - ** the logical zero (BDDs). - */ - if (node != background && node != zero) { - for (i = 0; i < dd->size; i++) { - v = list[i]; - if (v == 0) (void) fprintf(dd->out,"0"); - else if (v == 1) (void) fprintf(dd->out,"1"); - else (void) fprintf(dd->out,"-"); - } - (void) fprintf(dd->out," % g\n", cuddV(node)); - } - } else { - Nv = cuddT(N); - Nnv = cuddE(N); - if (Cudd_IsComplement(node)) { - Nv = Cudd_Not(Nv); - Nnv = Cudd_Not(Nnv); - } - index = N->index; - list[index] = 0; - ddPrintMintermAux(dd,Nnv,list); - list[index] = 1; - ddPrintMintermAux(dd,Nv,list); - list[index] = 2; - } - return; - -} /* end of ddPrintMintermAux */ - - -/**Function******************************************************************** - - Synopsis [Performs the recursive step of Cudd_DagSize.] - - Description [Performs the recursive step of Cudd_DagSize. Returns the - number of nodes in the graph rooted at n.] - - SideEffects [None] - -******************************************************************************/ -static int -ddDagInt( - DdNode * n) -{ - int tval, eval; - - if (Cudd_IsComplement(n->next)) { - return(0); - } - n->next = Cudd_Not(n->next); - if (cuddIsConstant(n)) { - return(1); - } - tval = ddDagInt(cuddT(n)); - eval = ddDagInt(Cudd_Regular(cuddE(n))); - return(1 + tval + eval); - -} /* end of ddDagInt */ - - -/**Function******************************************************************** - - Synopsis [Performs the recursive step of Cudd_CofactorEstimate.] - - Description [Performs the recursive step of Cudd_CofactorEstimate. - Returns an estimate of the number of nodes in the DD of a - cofactor of node. Uses the least significant bit of the next field as - visited flag. node is supposed to be regular; the invariant is maintained - by this procedure.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -static int -cuddEstimateCofactor( - DdManager *dd, - st_table *table, - DdNode * node, - int i, - int phase, - DdNode ** ptr) -{ - int tval, eval, val; - DdNode *ptrT, *ptrE; - - if (Cudd_IsComplement(node->next)) { - if (!st_lookup(table,(char *)node,(char **)ptr)) { - st_add_direct(table,(char *)node,(char *)node); - *ptr = node; - } - return(0); - } - node->next = Cudd_Not(node->next); - if (cuddIsConstant(node)) { - *ptr = node; - if (st_add_direct(table,(char *)node,(char *)node) == ST_OUT_OF_MEM) - return(CUDD_OUT_OF_MEM); - return(1); - } - if ((int) node->index == i) { - if (phase == 1) { - *ptr = cuddT(node); - val = ddDagInt(cuddT(node)); - } else { - *ptr = cuddE(node); - val = ddDagInt(Cudd_Regular(cuddE(node))); - } - if (node->ref > 1) { - if (st_add_direct(table,(char *)node,(char *)*ptr) == - ST_OUT_OF_MEM) - return(CUDD_OUT_OF_MEM); - } - return(val); - } - if (dd->perm[node->index] > dd->perm[i]) { - *ptr = node; - tval = ddDagInt(cuddT(node)); - eval = ddDagInt(Cudd_Regular(cuddE(node))); - if (node->ref > 1) { - if (st_add_direct(table,(char *)node,(char *)node) == - ST_OUT_OF_MEM) - return(CUDD_OUT_OF_MEM); - } - val = 1 + tval + eval; - return(val); - } - tval = cuddEstimateCofactor(dd,table,cuddT(node),i,phase,&ptrT); - eval = cuddEstimateCofactor(dd,table,Cudd_Regular(cuddE(node)),i, - phase,&ptrE); - ptrE = Cudd_NotCond(ptrE,Cudd_IsComplement(cuddE(node))); - if (ptrT == ptrE) { /* recombination */ - *ptr = ptrT; - val = tval; - if (node->ref > 1) { - if (st_add_direct(table,(char *)node,(char *)*ptr) == - ST_OUT_OF_MEM) - return(CUDD_OUT_OF_MEM); - } - } else if ((ptrT != cuddT(node) || ptrE != cuddE(node)) && - (*ptr = cuddUniqueLookup(dd,node->index,ptrT,ptrE)) != NULL) { - if (Cudd_IsComplement((*ptr)->next)) { - val = 0; - } else { - val = 1 + tval + eval; - } - if (node->ref > 1) { - if (st_add_direct(table,(char *)node,(char *)*ptr) == - ST_OUT_OF_MEM) - return(CUDD_OUT_OF_MEM); - } - } else { - *ptr = node; - val = 1 + tval + eval; - } - return(val); - -} /* end of cuddEstimateCofactor */ - - -/**Function******************************************************************** - - Synopsis [Checks the unique table for the existence of an internal node.] - - Description [Checks the unique table for the existence of an internal - node. Returns a pointer to the node if it is in the table; NULL otherwise.] - - SideEffects [None] - - SeeAlso [cuddUniqueInter] - -******************************************************************************/ -static DdNode * -cuddUniqueLookup( - DdManager * unique, - int index, - DdNode * T, - DdNode * E) -{ - int posn; - unsigned int level; - DdNodePtr *nodelist; - DdNode *looking; - DdSubtable *subtable; - - if (index >= unique->size) { - return(NULL); - } - - level = unique->perm[index]; - subtable = &(unique->subtables[level]); - -#ifdef DD_DEBUG - assert(level < (unsigned) cuddI(unique,T->index)); - assert(level < (unsigned) cuddI(unique,Cudd_Regular(E)->index)); -#endif - - posn = ddHash(T, E, subtable->shift); - nodelist = subtable->nodelist; - looking = nodelist[posn]; - - while (T < cuddT(looking)) { - looking = Cudd_Regular(looking->next); - } - while (T == cuddT(looking) && E < cuddE(looking)) { - looking = Cudd_Regular(looking->next); - } - if (cuddT(looking) == T && cuddE(looking) == E) { - return(looking); - } - - return(NULL); - -} /* end of cuddUniqueLookup */ - - -/**Function******************************************************************** - - Synopsis [Performs the recursive step of Cudd_CofactorEstimateSimple.] - - Description [Performs the recursive step of Cudd_CofactorEstimateSimple. - Returns an estimate of the number of nodes in the DD of the positive - cofactor of node. Uses the least significant bit of the next field as - visited flag. node is supposed to be regular; the invariant is maintained - by this procedure.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -static int -cuddEstimateCofactorSimple( - DdNode * node, - int i) -{ - int tval, eval; - - if (Cudd_IsComplement(node->next)) { - return(0); - } - node->next = Cudd_Not(node->next); - if (cuddIsConstant(node)) { - return(1); - } - tval = cuddEstimateCofactorSimple(cuddT(node),i); - if ((int) node->index == i) return(tval); - eval = cuddEstimateCofactorSimple(Cudd_Regular(cuddE(node)),i); - return(1 + tval + eval); - -} /* end of cuddEstimateCofactorSimple */ - - -/**Function******************************************************************** - - Synopsis [Performs the recursive step of Cudd_CountMinterm.] - - Description [Performs the recursive step of Cudd_CountMinterm. - It is based on the following identity. Let |f| be the - number of minterms of f. Then: - <xmp> - |f| = (|f0|+|f1|)/2 - </xmp> - where f0 and f1 are the two cofactors of f. Does not use the - identity |f'| = max - |f|, to minimize loss of accuracy due to - roundoff. Returns the number of minterms of the function rooted at - node.] - - SideEffects [None] - -******************************************************************************/ -static double -ddCountMintermAux( - DdNode * node, - double max, - DdHashTable * table) -{ - DdNode *N, *Nt, *Ne; - double min, minT, minE; - DdNode *res; - - N = Cudd_Regular(node); - - if (cuddIsConstant(N)) { - if (node == background || node == zero) { - return(0.0); - } else { - return(max); - } - } - if (N->ref != 1 && (res = cuddHashTableLookup1(table,node)) != NULL) { - min = cuddV(res); - if (res->ref == 0) { - table->manager->dead++; - table->manager->constants.dead++; - } - return(min); - } - - Nt = cuddT(N); Ne = cuddE(N); - if (Cudd_IsComplement(node)) { - Nt = Cudd_Not(Nt); Ne = Cudd_Not(Ne); - } - - minT = ddCountMintermAux(Nt,max,table); - if (minT == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM); - minT *= 0.5; - minE = ddCountMintermAux(Ne,max,table); - if (minE == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM); - minE *= 0.5; - min = minT + minE; - - if (N->ref != 1) { - ptrint fanout = (ptrint) N->ref; - cuddSatDec(fanout); - res = cuddUniqueConst(table->manager,min); - if (!cuddHashTableInsert1(table,node,res,fanout)) { - cuddRef(res); Cudd_RecursiveDeref(table->manager, res); - return((double)CUDD_OUT_OF_MEM); - } - } - - return(min); - -} /* end of ddCountMintermAux */ - - -/**Function******************************************************************** - - Synopsis [Performs the recursive step of Cudd_CountPath.] - - Description [Performs the recursive step of Cudd_CountPath. - It is based on the following identity. Let |f| be the - number of paths of f. Then: - <xmp> - |f| = |f0|+|f1| - </xmp> - where f0 and f1 are the two cofactors of f. Uses the - identity |f'| = |f|, to improve the utilization of the (local) cache. - Returns the number of paths of the function rooted at node.] - - SideEffects [None] - -******************************************************************************/ -static double -ddCountPathAux( - DdNode * node, - st_table * table) -{ - - DdNode *Nv, *Nnv; - double paths, *ppaths, paths1, paths2; - double *dummy; - - - if (cuddIsConstant(node)) { - return(1.0); - } - if (st_lookup(table, (char *)node, (char **)&dummy)) { - paths = *dummy; - return(paths); - } - - Nv = cuddT(node); Nnv = cuddE(node); - - paths1 = ddCountPathAux(Nv,table); - if (paths1 == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM); - paths2 = ddCountPathAux(Cudd_Regular(Nnv),table); - if (paths2 == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM); - paths = paths1 + paths2; - - ppaths = ALLOC(double,1); - if (ppaths == NULL) { - return((double)CUDD_OUT_OF_MEM); - } - - *ppaths = paths; - - if (st_add_direct(table,(char *)node, (char *)ppaths) == ST_OUT_OF_MEM) { - FREE(ppaths); - return((double)CUDD_OUT_OF_MEM); - } - return(paths); - -} /* end of ddCountPathAux */ - - -/**Function******************************************************************** - - Synopsis [Performs the recursive step of Cudd_CountMinterm.] - - Description [Performs the recursive step of Cudd_CountMinterm. - It is based on the following identity. Let |f| be the - number of minterms of f. Then: - <xmp> - |f| = (|f0|+|f1|)/2 - </xmp> - where f0 and f1 are the two cofactors of f. Does not use the - identity |f'| = max - |f|, to minimize loss of accuracy due to - roundoff. Returns the number of minterms of the function rooted at - node.] - - SideEffects [None] - -******************************************************************************/ -static int -ddEpdCountMintermAux( - DdNode * node, - EpDouble * max, - EpDouble * epd, - st_table * table) -{ - DdNode *Nt, *Ne; - EpDouble *min, minT, minE; - EpDouble *res; - int status; - - if (cuddIsConstant(node)) { - if (node == background || node == zero) { - EpdMakeZero(epd, 0); - } else { - EpdCopy(max, epd); - } - return(0); - } - if (node->ref != 1 && st_lookup(table, (char *)node, (char **)&res)) { - EpdCopy(res, epd); - return(0); - } - - Nt = cuddT(node); Ne = cuddE(node); - if (Cudd_IsComplement(node)) { - Nt = Cudd_Not(Nt); Ne = Cudd_Not(Ne); - } - - status = ddEpdCountMintermAux(Nt,max,&minT,table); - if (status == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM); - EpdMultiply(&minT, (double)0.5); - status = ddEpdCountMintermAux(Ne,max,&minE,table); - if (status == CUDD_OUT_OF_MEM) return(CUDD_OUT_OF_MEM); - if (Cudd_IsComplement(Ne)) { - EpdSubtract3(max, &minE, epd); - EpdCopy(epd, &minE); - } - EpdMultiply(&minE, (double)0.5); - EpdAdd3(&minT, &minE, epd); - - if (node->ref > 1) { - min = EpdAlloc(); - if (!min) - return(CUDD_OUT_OF_MEM); - EpdCopy(epd, min); - if (st_insert(table, (char *)node, (char *)min) == ST_OUT_OF_MEM) { - EpdFree(min); - return(CUDD_OUT_OF_MEM); - } - } - - return(0); - -} /* end of ddEpdCountMintermAux */ - - -/**Function******************************************************************** - - Synopsis [Performs the recursive step of Cudd_CountPathsToNonZero.] - - Description [Performs the recursive step of Cudd_CountPathsToNonZero. - It is based on the following identity. Let |f| be the - number of paths of f. Then: - <xmp> - |f| = |f0|+|f1| - </xmp> - where f0 and f1 are the two cofactors of f. Returns the number of - paths of the function rooted at node.] - - SideEffects [None] - -******************************************************************************/ -static double -ddCountPathsToNonZero( - DdNode * N, - st_table * table) -{ - - DdNode *node, *Nt, *Ne; - double paths, *ppaths, paths1, paths2; - double *dummy; - - node = Cudd_Regular(N); - if (cuddIsConstant(node)) { - return((double) !(Cudd_IsComplement(N) || cuddV(node)==DD_ZERO_VAL)); - } - if (st_lookup(table, (char *)N, (char **)&dummy)) { - paths = *dummy; - return(paths); - } - - Nt = cuddT(node); Ne = cuddE(node); - if (node != N) { - Nt = Cudd_Not(Nt); Ne = Cudd_Not(Ne); - } - - paths1 = ddCountPathsToNonZero(Nt,table); - if (paths1 == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM); - paths2 = ddCountPathsToNonZero(Ne,table); - if (paths2 == (double)CUDD_OUT_OF_MEM) return((double)CUDD_OUT_OF_MEM); - paths = paths1 + paths2; - - ppaths = ALLOC(double,1); - if (ppaths == NULL) { - return((double)CUDD_OUT_OF_MEM); - } - - *ppaths = paths; - - if (st_add_direct(table,(char *)N, (char *)ppaths) == ST_OUT_OF_MEM) { - FREE(ppaths); - return((double)CUDD_OUT_OF_MEM); - } - return(paths); - -} /* end of ddCountPathsToNonZero */ - - -/**Function******************************************************************** - - Synopsis [Performs the recursive step of Cudd_Support.] - - Description [Performs the recursive step of Cudd_Support. Performs a - DFS from f. The support is accumulated in supp as a side effect. Uses - the LSB of the then pointer as visited flag.] - - SideEffects [None] - - SeeAlso [ddClearFlag] - -******************************************************************************/ -static void -ddSupportStep( - DdNode * f, - int * support) -{ - if (cuddIsConstant(f) || Cudd_IsComplement(f->next)) { - return; - } - - support[f->index] = 1; - ddSupportStep(cuddT(f),support); - ddSupportStep(Cudd_Regular(cuddE(f)),support); - /* Mark as visited. */ - f->next = Cudd_Not(f->next); - return; - -} /* end of ddSupportStep */ - - -/**Function******************************************************************** - - Synopsis [Performs a DFS from f, clearing the LSB of the next - pointers.] - - Description [] - - SideEffects [None] - - SeeAlso [ddSupportStep ddDagInt] - -******************************************************************************/ -static void -ddClearFlag( - DdNode * f) -{ - if (!Cudd_IsComplement(f->next)) { - return; - } - /* Clear visited flag. */ - f->next = Cudd_Regular(f->next); - if (cuddIsConstant(f)) { - return; - } - ddClearFlag(cuddT(f)); - ddClearFlag(Cudd_Regular(cuddE(f))); - return; - -} /* end of ddClearFlag */ - - -/**Function******************************************************************** - - Synopsis [Performs the recursive step of Cudd_CountLeaves.] - - Description [Performs the recursive step of Cudd_CountLeaves. Returns - the number of leaves in the DD rooted at n.] - - SideEffects [None] - - SeeAlso [Cudd_CountLeaves] - -******************************************************************************/ -static int -ddLeavesInt( - DdNode * n) -{ - int tval, eval; - - if (Cudd_IsComplement(n->next)) { - return(0); - } - n->next = Cudd_Not(n->next); - if (cuddIsConstant(n)) { - return(1); - } - tval = ddLeavesInt(cuddT(n)); - eval = ddLeavesInt(Cudd_Regular(cuddE(n))); - return(tval + eval); - -} /* end of ddLeavesInt */ - - -/**Function******************************************************************** - - Synopsis [Performs the recursive step of Cudd_bddPickArbitraryMinterms.] - - Description [Performs the recursive step of Cudd_bddPickArbitraryMinterms. - Returns 1 if successful; 0 otherwise.] - - SideEffects [none] - - SeeAlso [Cudd_bddPickArbitraryMinterms] - -******************************************************************************/ -static int -ddPickArbitraryMinterms( - DdManager *dd, - DdNode *node, - int nvars, - int nminterms, - char **string) -{ - DdNode *N, *T, *E; - DdNode *one, *bzero; - int i, t, result; - double min1, min2; - - if (string == NULL || node == NULL) return(0); - - /* The constant 0 function has no on-set cubes. */ - one = DD_ONE(dd); - bzero = Cudd_Not(one); - if (nminterms == 0 || node == bzero) return(1); - if (node == one) { - return(1); - } - - N = Cudd_Regular(node); - T = cuddT(N); E = cuddE(N); - if (Cudd_IsComplement(node)) { - T = Cudd_Not(T); E = Cudd_Not(E); - } - - min1 = Cudd_CountMinterm(dd, T, nvars) / 2.0; - if (min1 == (double)CUDD_OUT_OF_MEM) return(0); - min2 = Cudd_CountMinterm(dd, E, nvars) / 2.0; - if (min2 == (double)CUDD_OUT_OF_MEM) return(0); - - t = (int)((double)nminterms * min1 / (min1 + min2) + 0.5); - for (i = 0; i < t; i++) - string[i][N->index] = '1'; - for (i = t; i < nminterms; i++) - string[i][N->index] = '0'; - - result = ddPickArbitraryMinterms(dd,T,nvars,t,&string[0]); - if (result == 0) - return(0); - result = ddPickArbitraryMinterms(dd,E,nvars,nminterms-t,&string[t]); - return(result); - -} /* end of ddPickArbitraryMinterms */ - - -/**Function******************************************************************** - - Synopsis [Finds a representative cube of a BDD.] - - Description [Finds a representative cube of a BDD with the weight of - each variable. From the top variable, if the weight is greater than or - equal to 0.0, choose THEN branch unless the child is the constant 0. - Otherwise, choose ELSE branch unless the child is the constant 0.] - - SideEffects [Cudd_SubsetWithMaskVars Cudd_bddPickOneCube] - -******************************************************************************/ -static int -ddPickRepresentativeCube( - DdManager *dd, - DdNode *node, - int nvars, - double *weight, - char *string) -{ - DdNode *N, *T, *E; - DdNode *one, *bzero; - - if (string == NULL || node == NULL) return(0); - - /* The constant 0 function has no on-set cubes. */ - one = DD_ONE(dd); - bzero = Cudd_Not(one); - if (node == bzero) return(0); - - if (node == DD_ONE(dd)) return(1); - - for (;;) { - N = Cudd_Regular(node); - if (N == one) - break; - T = cuddT(N); - E = cuddE(N); - if (Cudd_IsComplement(node)) { - T = Cudd_Not(T); - E = Cudd_Not(E); - } - if (weight[N->index] >= 0.0) { - if (T == bzero) { - node = E; - string[N->index] = '0'; - } else { - node = T; - string[N->index] = '1'; - } - } else { - if (E == bzero) { - node = T; - string[N->index] = '1'; - } else { - node = E; - string[N->index] = '0'; - } - } - } - return(1); - -} /* end of ddPickRepresentativeCube */ - - -/**Function******************************************************************** - - Synopsis [Frees the memory used to store the minterm counts recorded - in the visited table.] - - Description [Frees the memory used to store the minterm counts - recorded in the visited table. Returns ST_CONTINUE.] - - SideEffects [None] - -******************************************************************************/ -static enum st_retval -ddEpdFree( - char * key, - char * value, - char * arg) -{ - EpDouble *epd; - - epd = (EpDouble *) value; - EpdFree(epd); - return(ST_CONTINUE); - -} /* end of ddEpdFree */ |