diff options
Diffstat (limited to 'src/bdd/cudd/cuddSubsetSP.c')
| -rw-r--r-- | src/bdd/cudd/cuddSubsetSP.c | 1624 |
1 files changed, 0 insertions, 1624 deletions
diff --git a/src/bdd/cudd/cuddSubsetSP.c b/src/bdd/cudd/cuddSubsetSP.c deleted file mode 100644 index 55ee3470..00000000 --- a/src/bdd/cudd/cuddSubsetSP.c +++ /dev/null @@ -1,1624 +0,0 @@ -/**CFile*********************************************************************** - - FileName [cuddSubsetSP.c] - - PackageName [cudd] - - Synopsis [Procedure to subset the given BDD choosing the shortest paths - (largest cubes) in the BDD.] - - - Description [External procedures included in this module: - <ul> - <li> Cudd_SubsetShortPaths() - <li> Cudd_SupersetShortPaths() - </ul> - Internal procedures included in this module: - <ul> - <li> cuddSubsetShortPaths() - </ul> - Static procedures included in this module: - <ul> - <li> BuildSubsetBdd() - <li> CreatePathTable() - <li> AssessPathLength() - <li> CreateTopDist() - <li> CreateBotDist() - <li> ResizeNodeDistPages() - <li> ResizeQueuePages() - <li> stPathTableDdFree() - </ul> - ] - - SeeAlso [cuddSubsetHB.c] - - Author [Kavita Ravi] - - 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 */ -/*---------------------------------------------------------------------------*/ - -#define DEFAULT_PAGE_SIZE 2048 /* page size to store the BFS queue element type */ -#define DEFAULT_NODE_DIST_PAGE_SIZE 2048 /* page sizesto store NodeDist_t type */ -#define MAXSHORTINT ((DdHalfWord) ~0) /* constant defined to store - * maximum distance of a node - * from the root or the - * constant - */ -#define INITIAL_PAGES 128 /* number of initial pages for the - * queue/NodeDist_t type */ - -/*---------------------------------------------------------------------------*/ -/* Stucture declarations */ -/*---------------------------------------------------------------------------*/ - -/* structure created to store subset results for each node and distances with - * odd and even parity of the node from the root and sink. Main data structure - * in this procedure. - */ -struct NodeDist{ - DdHalfWord oddTopDist; - DdHalfWord evenTopDist; - DdHalfWord oddBotDist; - DdHalfWord evenBotDist; - DdNode *regResult; - DdNode *compResult; -}; - -/* assorted information needed by the BuildSubsetBdd procedure. */ -struct AssortedInfo { - unsigned int maxpath; - int findShortestPath; - int thresholdReached; - st_table *maxpathTable; - int threshold; -}; - -/*---------------------------------------------------------------------------*/ -/* Type declarations */ -/*---------------------------------------------------------------------------*/ - -typedef struct NodeDist NodeDist_t; - -/*---------------------------------------------------------------------------*/ -/* Variable declarations */ -/*---------------------------------------------------------------------------*/ - -#ifndef lint -static char rcsid[] DD_UNUSED = "$Id: cuddSubsetSP.c,v 1.1.1.1 2003/02/24 22:23:53 wjiang Exp $"; -#endif - -#ifdef DD_DEBUG -static int numCalls; -static int hits; -static int thishit; -#endif - - -static int memOut; /* flag to indicate out of memory */ -static DdNode *zero, *one; /* constant functions */ - -static NodeDist_t **nodeDistPages; /* pointers to the pages */ -static int nodeDistPageIndex; /* index to next element */ -static int nodeDistPage; /* index to current page */ -static int nodeDistPageSize = DEFAULT_NODE_DIST_PAGE_SIZE; /* page size */ -static int maxNodeDistPages; /* number of page pointers */ -static NodeDist_t *currentNodeDistPage; /* current page */ - -static DdNode ***queuePages; /* pointers to the pages */ -static int queuePageIndex; /* index to next element */ -static int queuePage; /* index to current page */ -static int queuePageSize = DEFAULT_PAGE_SIZE; /* page size */ -static int maxQueuePages; /* number of page pointers */ -static DdNode **currentQueuePage; /* current page */ - - -/*---------------------------------------------------------------------------*/ -/* Macro declarations */ -/*---------------------------------------------------------------------------*/ - -/**AutomaticStart*************************************************************/ - -/*---------------------------------------------------------------------------*/ -/* Static function prototypes */ -/*---------------------------------------------------------------------------*/ - -static void ResizeNodeDistPages ARGS(()); -static void ResizeQueuePages ARGS(()); -static void CreateTopDist ARGS((st_table *pathTable, int parentPage, int parentQueueIndex, int topLen, DdNode **childPage, int childQueueIndex, int numParents, FILE *fp)); -static int CreateBotDist ARGS((DdNode *node, st_table *pathTable, unsigned int *pathLengthArray, FILE *fp)); -static st_table * CreatePathTable ARGS((DdNode *node, unsigned int *pathLengthArray, FILE *fp)); -static unsigned int AssessPathLength ARGS((unsigned int *pathLengthArray, int threshold, int numVars, unsigned int *excess, FILE *fp)); -static DdNode * BuildSubsetBdd ARGS((DdManager *dd, st_table *pathTable, DdNode *node, struct AssortedInfo *info, st_table *subsetNodeTable)); -static enum st_retval stPathTableDdFree ARGS((char *key, char *value, char *arg)); - -/**AutomaticEnd***************************************************************/ - - -/*---------------------------------------------------------------------------*/ -/* Definition of Exported functions */ -/*---------------------------------------------------------------------------*/ - - -/**Function******************************************************************** - - Synopsis [Extracts a dense subset from a BDD with the shortest paths - heuristic.] - - Description [Extracts a dense subset from a BDD. This procedure - tries to preserve the shortest paths of the input BDD, because they - give many minterms and contribute few nodes. This procedure may - increase the number of nodes in trying to create the subset or - reduce the number of nodes due to recombination as compared to the - original BDD. Hence the threshold may not be strictly adhered to. In - practice, recombination overshadows the increase in the number of - nodes and results in small BDDs as compared to the threshold. The - hardlimit specifies whether threshold needs to be strictly adhered - to. If it is set to 1, the procedure ensures that result is never - larger than the specified limit but may be considerably less than - the threshold. Returns a pointer to the BDD for the subset if - successful; NULL otherwise. The value for numVars should be as - close as possible to the size of the support of f for better - efficiency. However, it is safe to pass the value returned by - Cudd_ReadSize for numVars. If 0 is passed, then the value returned - by Cudd_ReadSize is used.] - - SideEffects [None] - - SeeAlso [Cudd_SupersetShortPaths Cudd_SubsetHeavyBranch Cudd_ReadSize] - -******************************************************************************/ -DdNode * -Cudd_SubsetShortPaths( - DdManager * dd /* manager */, - DdNode * f /* function to be subset */, - int numVars /* number of variables in the support of f */, - int threshold /* maximum number of nodes in the subset */, - int hardlimit /* flag: 1 if threshold is a hard limit */) -{ - DdNode *subset; - - memOut = 0; - do { - dd->reordered = 0; - subset = cuddSubsetShortPaths(dd, f, numVars, threshold, hardlimit); - } while((dd->reordered ==1) && (!memOut)); - - return(subset); - -} /* end of Cudd_SubsetShortPaths */ - - -/**Function******************************************************************** - - Synopsis [Extracts a dense superset from a BDD with the shortest paths - heuristic.] - - Description [Extracts a dense superset from a BDD. The procedure is - identical to the subset procedure except for the fact that it - receives the complement of the given function. Extracting the subset - of the complement function is equivalent to extracting the superset - of the function. This procedure tries to preserve the shortest - paths of the complement BDD, because they give many minterms and - contribute few nodes. This procedure may increase the number of - nodes in trying to create the superset or reduce the number of nodes - due to recombination as compared to the original BDD. Hence the - threshold may not be strictly adhered to. In practice, recombination - overshadows the increase in the number of nodes and results in small - BDDs as compared to the threshold. The hardlimit specifies whether - threshold needs to be strictly adhered to. If it is set to 1, the - procedure ensures that result is never larger than the specified - limit but may be considerably less than the threshold. Returns a - pointer to the BDD for the superset if successful; NULL - otherwise. The value for numVars should be as close as possible to - the size of the support of f for better efficiency. However, it is - safe to pass the value returned by Cudd_ReadSize for numVar. If 0 - is passed, then the value returned by Cudd_ReadSize is used.] - - SideEffects [None] - - SeeAlso [Cudd_SubsetShortPaths Cudd_SupersetHeavyBranch Cudd_ReadSize] - -******************************************************************************/ -DdNode * -Cudd_SupersetShortPaths( - DdManager * dd /* manager */, - DdNode * f /* function to be superset */, - int numVars /* number of variables in the support of f */, - int threshold /* maximum number of nodes in the subset */, - int hardlimit /* flag: 1 if threshold is a hard limit */) -{ - DdNode *subset, *g; - - g = Cudd_Not(f); - memOut = 0; - do { - dd->reordered = 0; - subset = cuddSubsetShortPaths(dd, g, numVars, threshold, hardlimit); - } while((dd->reordered ==1) && (!memOut)); - - return(Cudd_NotCond(subset, (subset != NULL))); - -} /* end of Cudd_SupersetShortPaths */ - - -/*---------------------------------------------------------------------------*/ -/* Definition of internal functions */ -/*---------------------------------------------------------------------------*/ - - -/**Function******************************************************************** - - Synopsis [The outermost procedure to return a subset of the given BDD - with the shortest path lengths.] - - Description [The outermost procedure to return a subset of the given - BDD with the largest cubes. The path lengths are calculated, the maximum - allowable path length is determined and the number of nodes of this - path length that can be used to build a subset. If the threshold is - larger than the size of the original BDD, the original BDD is - returned. ] - - SideEffects [None] - - SeeAlso [Cudd_SubsetShortPaths] - -******************************************************************************/ -DdNode * -cuddSubsetShortPaths( - DdManager * dd /* DD manager */, - DdNode * f /* function to be subset */, - int numVars /* total number of variables in consideration */, - int threshold /* maximum number of nodes allowed in the subset */, - int hardlimit /* flag determining whether thershold should be respected strictly */) -{ - st_table *pathTable; - DdNode *N, *subset; - - unsigned int *pathLengthArray; - unsigned int maxpath, oddLen, evenLen, pathLength, *excess; - int i; - NodeDist_t *nodeStat; - struct AssortedInfo *info; - st_table *subsetNodeTable; - - one = DD_ONE(dd); - zero = Cudd_Not(one); - - if (numVars == 0) { - /* set default value */ - numVars = Cudd_ReadSize(dd); - } - - if (threshold > numVars) { - threshold = threshold - numVars; - } - if (f == NULL) { - fprintf(dd->err, "Cannot partition, nil object\n"); - dd->errorCode = CUDD_INVALID_ARG; - return(NULL); - } - if (Cudd_IsConstant(f)) - return (f); - - pathLengthArray = ALLOC(unsigned int, numVars+1); - for (i = 0; i < numVars+1; i++) pathLengthArray[i] = 0; - - -#ifdef DD_DEBUG - numCalls = 0; -#endif - - pathTable = CreatePathTable(f, pathLengthArray, dd->err); - - if ((pathTable == NULL) || (memOut)) { - if (pathTable != NULL) - st_free_table(pathTable); - FREE(pathLengthArray); - return (NIL(DdNode)); - } - - excess = ALLOC(unsigned int, 1); - *excess = 0; - maxpath = AssessPathLength(pathLengthArray, threshold, numVars, excess, - dd->err); - - if (maxpath != (unsigned) (numVars + 1)) { - - info = ALLOC(struct AssortedInfo, 1); - info->maxpath = maxpath; - info->findShortestPath = 0; - info->thresholdReached = *excess; - info->maxpathTable = st_init_table(st_ptrcmp, st_ptrhash); - info->threshold = threshold; - -#ifdef DD_DEBUG - (void) fprintf(dd->out, "Path length array\n"); - for (i = 0; i < (numVars+1); i++) { - if (pathLengthArray[i]) - (void) fprintf(dd->out, "%d ",i); - } - (void) fprintf(dd->out, "\n"); - for (i = 0; i < (numVars+1); i++) { - if (pathLengthArray[i]) - (void) fprintf(dd->out, "%d ",pathLengthArray[i]); - } - (void) fprintf(dd->out, "\n"); - (void) fprintf(dd->out, "Maxpath = %d, Thresholdreached = %d\n", - maxpath, info->thresholdReached); -#endif - - N = Cudd_Regular(f); - if (!st_lookup(pathTable, (char *)N, (char **)&nodeStat)) { - fprintf(dd->err, "Something wrong, root node must be in table\n"); - dd->errorCode = CUDD_INTERNAL_ERROR; - return(NULL); - } else { - if ((nodeStat->oddTopDist != MAXSHORTINT) && - (nodeStat->oddBotDist != MAXSHORTINT)) - oddLen = (nodeStat->oddTopDist + nodeStat->oddBotDist); - else - oddLen = MAXSHORTINT; - - if ((nodeStat->evenTopDist != MAXSHORTINT) && - (nodeStat->evenBotDist != MAXSHORTINT)) - evenLen = (nodeStat->evenTopDist +nodeStat->evenBotDist); - else - evenLen = MAXSHORTINT; - - pathLength = (oddLen <= evenLen) ? oddLen : evenLen; - if (pathLength > maxpath) { - (void) fprintf(dd->err, "All computations are bogus, since root has path length greater than max path length within threshold %d, %d\n", maxpath, pathLength); - dd->errorCode = CUDD_INTERNAL_ERROR; - return(NULL); - } - } - -#ifdef DD_DEBUG - numCalls = 0; - hits = 0; - thishit = 0; -#endif - /* initialize a table to store computed nodes */ - if (hardlimit) { - subsetNodeTable = st_init_table(st_ptrcmp, st_ptrhash); - } else { - subsetNodeTable = NIL(st_table); - } - subset = BuildSubsetBdd(dd, pathTable, f, info, subsetNodeTable); - if (subset != NULL) { - cuddRef(subset); - } - /* record the number of times a computed result for a node is hit */ - -#ifdef DD_DEBUG - (void) fprintf(dd->out, "Hits = %d, New==Node = %d, NumCalls = %d\n", - hits, thishit, numCalls); -#endif - - if (subsetNodeTable != NIL(st_table)) { - st_free_table(subsetNodeTable); - } - st_free_table(info->maxpathTable); - st_foreach(pathTable, stPathTableDdFree, (char *)dd); - - FREE(info); - - } else {/* if threshold larger than size of dd */ - subset = f; - cuddRef(subset); - } - FREE(excess); - st_free_table(pathTable); - FREE(pathLengthArray); - for (i = 0; i <= nodeDistPage; i++) FREE(nodeDistPages[i]); - FREE(nodeDistPages); - -#ifdef DD_DEBUG - /* check containment of subset in f */ - if (subset != NULL) { - DdNode *check; - check = Cudd_bddIteConstant(dd, subset, f, one); - if (check != one) { - (void) fprintf(dd->err, "Wrong partition\n"); - dd->errorCode = CUDD_INTERNAL_ERROR; - return(NULL); - } - } -#endif - - if (subset != NULL) { - cuddDeref(subset); - return(subset); - } else { - return(NULL); - } - -} /* end of cuddSubsetShortPaths */ - - -/*---------------------------------------------------------------------------*/ -/* Definition of static functions */ -/*---------------------------------------------------------------------------*/ - - -/**Function******************************************************************** - - Synopsis [Resize the number of pages allocated to store the distances - related to each node.] - - Description [Resize the number of pages allocated to store the distances - related to each node. The procedure moves the counter to the - next page when the end of the page is reached and allocates new - pages when necessary. ] - - SideEffects [Changes the size of pages, page, page index, maximum - number of pages freeing stuff in case of memory out. ] - - SeeAlso [] - -******************************************************************************/ -static void -ResizeNodeDistPages( - ) -{ - int i; - NodeDist_t **newNodeDistPages; - - /* move to next page */ - nodeDistPage++; - - /* If the current page index is larger than the number of pages - * allocated, allocate a new page array. Page numbers are incremented by - * INITIAL_PAGES - */ - if (nodeDistPage == maxNodeDistPages) { - newNodeDistPages = ALLOC(NodeDist_t *,maxNodeDistPages + INITIAL_PAGES); - if (newNodeDistPages == NULL) { - for (i = 0; i < nodeDistPage; i++) FREE(nodeDistPages[i]); - FREE(nodeDistPages); - memOut = 1; - return; - } else { - for (i = 0; i < maxNodeDistPages; i++) { - newNodeDistPages[i] = nodeDistPages[i]; - } - /* Increase total page count */ - maxNodeDistPages += INITIAL_PAGES; - FREE(nodeDistPages); - nodeDistPages = newNodeDistPages; - } - } - /* Allocate a new page */ - currentNodeDistPage = nodeDistPages[nodeDistPage] = ALLOC(NodeDist_t, - nodeDistPageSize); - if (currentNodeDistPage == NULL) { - for (i = 0; i < nodeDistPage; i++) FREE(nodeDistPages[i]); - FREE(nodeDistPages); - memOut = 1; - return; - } - /* reset page index */ - nodeDistPageIndex = 0; - return; - -} /* end of ResizeNodeDistPages */ - - -/**Function******************************************************************** - - Synopsis [Resize the number of pages allocated to store nodes in the BFS - traversal of the Bdd .] - - Description [Resize the number of pages allocated to store nodes in the BFS - traversal of the Bdd. The procedure moves the counter to the - next page when the end of the page is reached and allocates new - pages when necessary.] - - SideEffects [Changes the size of pages, page, page index, maximum - number of pages freeing stuff in case of memory out. ] - - SeeAlso [] - -******************************************************************************/ -static void -ResizeQueuePages( - ) -{ - int i; - DdNode ***newQueuePages; - - queuePage++; - /* If the current page index is larger than the number of pages - * allocated, allocate a new page array. Page numbers are incremented by - * INITIAL_PAGES - */ - if (queuePage == maxQueuePages) { - newQueuePages = ALLOC(DdNode **,maxQueuePages + INITIAL_PAGES); - if (newQueuePages == NULL) { - for (i = 0; i < queuePage; i++) FREE(queuePages[i]); - FREE(queuePages); - memOut = 1; - return; - } else { - for (i = 0; i < maxQueuePages; i++) { - newQueuePages[i] = queuePages[i]; - } - /* Increase total page count */ - maxQueuePages += INITIAL_PAGES; - FREE(queuePages); - queuePages = newQueuePages; - } - } - /* Allocate a new page */ - currentQueuePage = queuePages[queuePage] = ALLOC(DdNode *,queuePageSize); - if (currentQueuePage == NULL) { - for (i = 0; i < queuePage; i++) FREE(queuePages[i]); - FREE(queuePages); - memOut = 1; - return; - } - /* reset page index */ - queuePageIndex = 0; - return; - -} /* end of ResizeQueuePages */ - - -/**Function******************************************************************** - - Synopsis [ Labels each node with its shortest distance from the root] - - Description [ Labels each node with its shortest distance from the root. - This is done in a BFS search of the BDD. The nodes are processed - in a queue implemented as pages(array) to reduce memory fragmentation. - An entry is created for each node visited. The distance from the root - to the node with the corresponding parity is updated. The procedure - is called recursively each recusion level handling nodes at a given - level from the root.] - - - SideEffects [Creates entries in the pathTable] - - SeeAlso [CreatePathTable CreateBotDist] - -******************************************************************************/ -static void -CreateTopDist( - st_table * pathTable /* hast table to store path lengths */, - int parentPage /* the pointer to the page on which the first parent in the queue is to be found. */, - int parentQueueIndex /* pointer to the first parent on the page */, - int topLen /* current distance from the root */, - DdNode ** childPage /* pointer to the page on which the first child is to be added. */, - int childQueueIndex /* pointer to the first child */, - int numParents /* number of parents to process in this recursive call */, - FILE *fp /* where to write messages */) -{ - NodeDist_t *nodeStat; - DdNode *N, *Nv, *Nnv, *node, *child, *regChild; - int i; - int processingDone, childrenCount; - -#ifdef DD_DEBUG - numCalls++; - - /* assume this procedure comes in with only the root node*/ - /* set queue index to the next available entry for addition */ - /* set queue page to page of addition */ - if ((queuePages[parentPage] == childPage) && (parentQueueIndex == - childQueueIndex)) { - fprintf(fp, "Should not happen that they are equal\n"); - } - assert(queuePageIndex == childQueueIndex); - assert(currentQueuePage == childPage); -#endif - /* number children added to queue is initialized , needed for - * numParents in the next call - */ - childrenCount = 0; - /* process all the nodes in this level */ - while (numParents) { - numParents--; - if (parentQueueIndex == queuePageSize) { - parentPage++; - parentQueueIndex = 0; - } - /* a parent to process */ - node = *(queuePages[parentPage] + parentQueueIndex); - parentQueueIndex++; - /* get its children */ - N = Cudd_Regular(node); - Nv = Cudd_T(N); - Nnv = Cudd_E(N); - - Nv = Cudd_NotCond(Nv, Cudd_IsComplement(node)); - Nnv = Cudd_NotCond(Nnv, Cudd_IsComplement(node)); - - processingDone = 2; - while (processingDone) { - /* processing the THEN and the ELSE children, the THEN - * child first - */ - if (processingDone == 2) { - child = Nv; - } else { - child = Nnv; - } - - regChild = Cudd_Regular(child); - /* dont process if the child is a constant */ - if (!Cudd_IsConstant(child)) { - /* check is already visited, if not add a new entry in - * the path Table - */ - if (!st_lookup(pathTable, (char *)regChild, (char **)&nodeStat)) { - /* if not in table, has never been visited */ - /* create entry for table */ - if (nodeDistPageIndex == nodeDistPageSize) - ResizeNodeDistPages(); - if (memOut) { - for (i = 0; i <= queuePage; i++) FREE(queuePages[i]); - FREE(queuePages); - st_free_table(pathTable); - return; - } - /* New entry for child in path Table is created here */ - nodeStat = currentNodeDistPage + nodeDistPageIndex; - nodeDistPageIndex++; - - /* Initialize fields of the node data */ - nodeStat->oddTopDist = MAXSHORTINT; - nodeStat->evenTopDist = MAXSHORTINT; - nodeStat->evenBotDist = MAXSHORTINT; - nodeStat->oddBotDist = MAXSHORTINT; - nodeStat->regResult = NULL; - nodeStat->compResult = NULL; - /* update the table entry element, the distance keeps - * track of the parity of the path from the root - */ - if (Cudd_IsComplement(child)) { - nodeStat->oddTopDist = (DdHalfWord) topLen + 1; - } else { - nodeStat->evenTopDist = (DdHalfWord) topLen + 1; - } - - /* insert entry element for child in the table */ - if (st_insert(pathTable, (char *)regChild, - (char *)nodeStat) == ST_OUT_OF_MEM) { - memOut = 1; - for (i = 0; i <= nodeDistPage; i++) - FREE(nodeDistPages[i]); - FREE(nodeDistPages); - for (i = 0; i <= queuePage; i++) FREE(queuePages[i]); - FREE(queuePages); - st_free_table(pathTable); - return; - } - - /* Create list element for this child to process its children. - * If this node has been processed already, then it appears - * in the path table and hence is never added to the list - * again. - */ - - if (queuePageIndex == queuePageSize) ResizeQueuePages(); - if (memOut) { - for (i = 0; i <= nodeDistPage; i++) - FREE(nodeDistPages[i]); - FREE(nodeDistPages); - st_free_table(pathTable); - return; - } - *(currentQueuePage + queuePageIndex) = child; - queuePageIndex++; - - childrenCount++; - } else { - /* if not been met in a path with this parity before */ - /* put in list */ - if (((Cudd_IsComplement(child)) && (nodeStat->oddTopDist == - MAXSHORTINT)) || ((!Cudd_IsComplement(child)) && - (nodeStat->evenTopDist == MAXSHORTINT))) { - - if (queuePageIndex == queuePageSize) ResizeQueuePages(); - if (memOut) { - for (i = 0; i <= nodeDistPage; i++) - FREE(nodeDistPages[i]); - FREE(nodeDistPages); - st_free_table(pathTable); - return; - - } - *(currentQueuePage + queuePageIndex) = child; - queuePageIndex++; - - /* update the distance with the appropriate parity */ - if (Cudd_IsComplement(child)) { - nodeStat->oddTopDist = (DdHalfWord) topLen + 1; - } else { - nodeStat->evenTopDist = (DdHalfWord) topLen + 1; - } - childrenCount++; - } - - } /* end of else (not found in st_table) */ - } /*end of if Not constant child */ - processingDone--; - } /*end of while processing Nv, Nnv */ - } /*end of while numParents */ - -#ifdef DD_DEBUG - assert(queuePages[parentPage] == childPage); - assert(parentQueueIndex == childQueueIndex); -#endif - - if (childrenCount != 0) { - topLen++; - childPage = currentQueuePage; - childQueueIndex = queuePageIndex; - CreateTopDist(pathTable, parentPage, parentQueueIndex, topLen, - childPage, childQueueIndex, childrenCount, fp); - } - - return; - -} /* end of CreateTopDist */ - - -/**Function******************************************************************** - - Synopsis [ Labels each node with the shortest distance from the constant.] - - Description [Labels each node with the shortest distance from the constant. - This is done in a DFS search of the BDD. Each node has an odd - and even parity distance from the sink (since there exists paths to both - zero and one) which is less than MAXSHORTINT. At each node these distances - are updated using the minimum distance of its children from the constant. - SInce now both the length from the root and child is known, the minimum path - length(length of the shortest path between the root and the constant that - this node lies on) of this node can be calculated and used to update the - pathLengthArray] - - SideEffects [Updates Path Table and path length array] - - SeeAlso [CreatePathTable CreateTopDist AssessPathLength] - -******************************************************************************/ -static int -CreateBotDist( - DdNode * node /* current node */, - st_table * pathTable /* path table with path lengths */, - unsigned int * pathLengthArray /* array that stores number of nodes belonging to a particular path length. */, - FILE *fp /* where to write messages */) -{ - DdNode *N, *Nv, *Nnv; - DdNode *realChild; - DdNode *child, *regChild; - NodeDist_t *nodeStat, *nodeStatChild; - unsigned int oddLen, evenLen, pathLength; - DdHalfWord botDist; - int processingDone; - - if (Cudd_IsConstant(node)) - return(1); - N = Cudd_Regular(node); - /* each node has one table entry */ - /* update as you go down the min dist of each node from - the root in each (odd and even) parity */ - if (!st_lookup(pathTable, (char *)N, (char **)&nodeStat)) { - fprintf(fp, "Something wrong, the entry doesn't exist\n"); - return(0); - } - - /* compute length of odd parity distances */ - if ((nodeStat->oddTopDist != MAXSHORTINT) && - (nodeStat->oddBotDist != MAXSHORTINT)) - oddLen = (nodeStat->oddTopDist + nodeStat->oddBotDist); - else - oddLen = MAXSHORTINT; - - /* compute length of even parity distances */ - if (!((nodeStat->evenTopDist == MAXSHORTINT) || - (nodeStat->evenBotDist == MAXSHORTINT))) - evenLen = (nodeStat->evenTopDist +nodeStat->evenBotDist); - else - evenLen = MAXSHORTINT; - - /* assign pathlength to minimum of the two */ - pathLength = (oddLen <= evenLen) ? oddLen : evenLen; - - Nv = Cudd_T(N); - Nnv = Cudd_E(N); - - /* process each child */ - processingDone = 0; - while (processingDone != 2) { - if (!processingDone) { - child = Nv; - } else { - child = Nnv; - } - - realChild = Cudd_NotCond(child, Cudd_IsComplement(node)); - regChild = Cudd_Regular(child); - if (Cudd_IsConstant(realChild)) { - /* Found a minterm; count parity and shortest distance - ** from the constant. - */ - if (Cudd_IsComplement(child)) - nodeStat->oddBotDist = 1; - else - nodeStat->evenBotDist = 1; - } else { - /* If node not in table, recur. */ - if (!st_lookup(pathTable, (char *) regChild, - (char **)&nodeStatChild)) { - fprintf(fp, "Something wrong, node in table should have been created in top dist proc.\n"); - return(0); - } - - if (nodeStatChild->oddBotDist == MAXSHORTINT) { - if (nodeStatChild->evenBotDist == MAXSHORTINT) { - if (!CreateBotDist(realChild, pathTable, pathLengthArray, fp)) - return(0); - } else { - fprintf(fp, "Something wrong, both bot nodeStats should be there\n"); - return(0); - } - } - - /* Update shortest distance from the constant depending on - ** parity. */ - - if (Cudd_IsComplement(child)) { - /* If parity on the edge then add 1 to even distance - ** of child to get odd parity distance and add 1 to - ** odd distance of child to get even parity - ** distance. Change distance of current node only if - ** the calculated distance is less than existing - ** distance. */ - if (nodeStatChild->oddBotDist != MAXSHORTINT) - botDist = nodeStatChild->oddBotDist + 1; - else - botDist = MAXSHORTINT; - if (nodeStat->evenBotDist > botDist ) - nodeStat->evenBotDist = botDist; - - if (nodeStatChild->evenBotDist != MAXSHORTINT) - botDist = nodeStatChild->evenBotDist + 1; - else - botDist = MAXSHORTINT; - if (nodeStat->oddBotDist > botDist) - nodeStat->oddBotDist = botDist; - - } else { - /* If parity on the edge then add 1 to even distance - ** of child to get even parity distance and add 1 to - ** odd distance of child to get odd parity distance. - ** Change distance of current node only if the - ** calculated distance is lesser than existing - ** distance. */ - if (nodeStatChild->evenBotDist != MAXSHORTINT) - botDist = nodeStatChild->evenBotDist + 1; - else - botDist = MAXSHORTINT; - if (nodeStat->evenBotDist > botDist) - nodeStat->evenBotDist = botDist; - - if (nodeStatChild->oddBotDist != MAXSHORTINT) - botDist = nodeStatChild->oddBotDist + 1; - else - botDist = MAXSHORTINT; - if (nodeStat->oddBotDist > botDist) - nodeStat->oddBotDist = botDist; - } - } /* end of else (if not constant child ) */ - processingDone++; - } /* end of while processing Nv, Nnv */ - - /* Compute shortest path length on the fly. */ - if ((nodeStat->oddTopDist != MAXSHORTINT) && - (nodeStat->oddBotDist != MAXSHORTINT)) - oddLen = (nodeStat->oddTopDist + nodeStat->oddBotDist); - else - oddLen = MAXSHORTINT; - - if ((nodeStat->evenTopDist != MAXSHORTINT) && - (nodeStat->evenBotDist != MAXSHORTINT)) - evenLen = (nodeStat->evenTopDist +nodeStat->evenBotDist); - else - evenLen = MAXSHORTINT; - - /* Update path length array that has number of nodes of a particular - ** path length. */ - if (oddLen < pathLength ) { - if (pathLength != MAXSHORTINT) - pathLengthArray[pathLength]--; - if (oddLen != MAXSHORTINT) - pathLengthArray[oddLen]++; - pathLength = oddLen; - } - if (evenLen < pathLength ) { - if (pathLength != MAXSHORTINT) - pathLengthArray[pathLength]--; - if (evenLen != MAXSHORTINT) - pathLengthArray[evenLen]++; - } - - return(1); - -} /*end of CreateBotDist */ - - -/**Function******************************************************************** - - Synopsis [ The outer procedure to label each node with its shortest - distance from the root and constant] - - Description [ The outer procedure to label each node with its shortest - distance from the root and constant. Calls CreateTopDist and CreateBotDist. - The basis for computing the distance between root and constant is that - the distance may be the sum of even distances from the node to the root - and constant or the sum of odd distances from the node to the root and - constant. Both CreateTopDist and CreateBotDist create the odd and - even parity distances from the root and constant respectively.] - - SideEffects [None] - - SeeAlso [CreateTopDist CreateBotDist] - -******************************************************************************/ -static st_table * -CreatePathTable( - DdNode * node /* root of function */, - unsigned int * pathLengthArray /* array of path lengths to store nodes labeled with the various path lengths */, - FILE *fp /* where to write messages */) -{ - - st_table *pathTable; - NodeDist_t *nodeStat; - DdHalfWord topLen; - DdNode *N; - int i, numParents; - int insertValue; - DdNode **childPage; - int parentPage; - int childQueueIndex, parentQueueIndex; - - /* Creating path Table for storing data about nodes */ - pathTable = st_init_table(st_ptrcmp,st_ptrhash); - - /* initializing pages for info about each node */ - maxNodeDistPages = INITIAL_PAGES; - nodeDistPages = ALLOC(NodeDist_t *, maxNodeDistPages); - if (nodeDistPages == NULL) { - goto OUT_OF_MEM; - } - nodeDistPage = 0; - currentNodeDistPage = nodeDistPages[nodeDistPage] = - ALLOC(NodeDist_t, nodeDistPageSize); - if (currentNodeDistPage == NULL) { - for (i = 0; i <= nodeDistPage; i++) FREE(nodeDistPages[i]); - FREE(nodeDistPages); - goto OUT_OF_MEM; - } - nodeDistPageIndex = 0; - - /* Initializing pages for the BFS search queue, implemented as an array. */ - maxQueuePages = INITIAL_PAGES; - queuePages = ALLOC(DdNode **, maxQueuePages); - if (queuePages == NULL) { - goto OUT_OF_MEM; - } - queuePage = 0; - currentQueuePage = queuePages[queuePage] = ALLOC(DdNode *, queuePageSize); - if (currentQueuePage == NULL) { - for (i = 0; i <= queuePage; i++) FREE(queuePages[i]); - FREE(queuePages); - goto OUT_OF_MEM; - } - queuePageIndex = 0; - - /* Enter the root node into the queue to start with. */ - parentPage = queuePage; - parentQueueIndex = queuePageIndex; - topLen = 0; - *(currentQueuePage + queuePageIndex) = node; - queuePageIndex++; - childPage = currentQueuePage; - childQueueIndex = queuePageIndex; - - N = Cudd_Regular(node); - - if (nodeDistPageIndex == nodeDistPageSize) ResizeNodeDistPages(); - if (memOut) { - for (i = 0; i <= nodeDistPage; i++) FREE(nodeDistPages[i]); - FREE(nodeDistPages); - for (i = 0; i <= queuePage; i++) FREE(queuePages[i]); - FREE(queuePages); - st_free_table(pathTable); - goto OUT_OF_MEM; - } - - nodeStat = currentNodeDistPage + nodeDistPageIndex; - nodeDistPageIndex++; - - nodeStat->oddTopDist = MAXSHORTINT; - nodeStat->evenTopDist = MAXSHORTINT; - nodeStat->evenBotDist = MAXSHORTINT; - nodeStat->oddBotDist = MAXSHORTINT; - nodeStat->regResult = NULL; - nodeStat->compResult = NULL; - - insertValue = st_insert(pathTable, (char *)N, (char *)nodeStat); - if (insertValue == ST_OUT_OF_MEM) { - memOut = 1; - for (i = 0; i <= nodeDistPage; i++) FREE(nodeDistPages[i]); - FREE(nodeDistPages); - for (i = 0; i <= queuePage; i++) FREE(queuePages[i]); - FREE(queuePages); - st_free_table(pathTable); - goto OUT_OF_MEM; - } else if (insertValue == 1) { - fprintf(fp, "Something wrong, the entry exists but didnt show up in st_lookup\n"); - return(NULL); - } - - if (Cudd_IsComplement(node)) { - nodeStat->oddTopDist = 0; - } else { - nodeStat->evenTopDist = 0; - } - numParents = 1; - /* call the function that counts the distance of each node from the - * root - */ -#ifdef DD_DEBUG - numCalls = 0; -#endif - CreateTopDist(pathTable, parentPage, parentQueueIndex, (int) topLen, - childPage, childQueueIndex, numParents, fp); - if (memOut) { - fprintf(fp, "Out of Memory and cant count path lengths\n"); - goto OUT_OF_MEM; - } - -#ifdef DD_DEBUG - numCalls = 0; -#endif - /* call the function that counts the distance of each node from the - * constant - */ - if (!CreateBotDist(node, pathTable, pathLengthArray, fp)) return(NULL); - - /* free BFS queue pages as no longer required */ - for (i = 0; i <= queuePage; i++) FREE(queuePages[i]); - FREE(queuePages); - return(pathTable); - -OUT_OF_MEM: - (void) fprintf(fp, "Out of Memory, cannot allocate pages\n"); - memOut = 1; - return(NULL); - -} /*end of CreatePathTable */ - - -/**Function******************************************************************** - - Synopsis [Chooses the maximum allowable path length of nodes under the - threshold.] - - Description [Chooses the maximum allowable path length under each node. - The corner cases are when the threshold is larger than the number - of nodes in the BDD iself, in which case 'numVars + 1' is returned. - If all nodes of a particular path length are needed, then the - maxpath returned is the next one with excess nodes = 0;] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -static unsigned int -AssessPathLength( - unsigned int * pathLengthArray /* array determining number of nodes belonging to the different path lengths */, - int threshold /* threshold to determine maximum allowable nodes in the subset */, - int numVars /* maximum number of variables */, - unsigned int * excess /* number of nodes labeled maxpath required in the subset */, - FILE *fp /* where to write messages */) -{ - unsigned int i, maxpath; - int temp; - - temp = threshold; - i = 0; - maxpath = 0; - /* quit loop if i reaches max number of variables or if temp reaches - * below zero - */ - while ((i < (unsigned) numVars+1) && (temp > 0)) { - if (pathLengthArray[i] > 0) { - maxpath = i; - temp = temp - pathLengthArray[i]; - } - i++; - } - /* if all nodes of max path are needed */ - if (temp >= 0) { - maxpath++; /* now maxpath becomes the next maxppath or max number - of variables */ - *excess = 0; - } else { /* normal case when subset required is less than size of - original BDD */ - *excess = temp + pathLengthArray[maxpath]; - } - - if (maxpath == 0) { - fprintf(fp, "Path Length array seems to be all zeroes, check\n"); - } - return(maxpath); - -} /* end of AssessPathLength */ - - -/**Function******************************************************************** - - Synopsis [Builds the BDD with nodes labeled with path length less than or equal to maxpath] - - Description [Builds the BDD with nodes labeled with path length - under maxpath and as many nodes labeled maxpath as determined by the - threshold. The procedure uses the path table to determine which nodes - in the original bdd need to be retained. This procedure picks a - shortest path (tie break decided by taking the child with the shortest - distance to the constant) and recurs down the path till it reaches the - constant. the procedure then starts building the subset upward from - the constant. All nodes labeled by path lengths less than the given - maxpath are used to build the subset. However, in the case of nodes - that have label equal to maxpath, as many are chosen as required by - the threshold. This number is stored in the info structure in the - field thresholdReached. This field is decremented whenever a node - labeled maxpath is encountered and the nodes labeled maxpath are - aggregated in a maxpath table. As soon as the thresholdReached count - goes to 0, the shortest path from this node to the constant is found. - The extraction of nodes with the above labeling is based on the fact - that each node, labeled with a path length, P, has at least one child - labeled P or less. So extracting all nodes labeled a given path length - P ensures complete paths between the root and the constant. Extraction - of a partial number of nodes with a given path length may result in - incomplete paths and hence the additional number of nodes are grabbed - to complete the path. Since the Bdd is built bottom-up, other nodes - labeled maxpath do lie on complete paths. The procedure may cause the - subset to have a larger or smaller number of nodes than the specified - threshold. The increase in the number of nodes is caused by the - building of a subset and the reduction by recombination. However in - most cases, the recombination overshadows the increase and the - procedure returns a result with lower number of nodes than specified. - The subsetNodeTable is NIL when there is no hard limit on the number - of nodes. Further efforts towards keeping the subset closer to the - threshold number were abandoned in favour of keeping the procedure - simple and fast.] - - SideEffects [SubsetNodeTable is changed if it is not NIL.] - - SeeAlso [] - -******************************************************************************/ -static DdNode * -BuildSubsetBdd( - DdManager * dd /* DD manager */, - st_table * pathTable /* path table with path lengths and computed results */, - DdNode * node /* current node */, - struct AssortedInfo * info /* assorted information structure */, - st_table * subsetNodeTable /* table storing computed results */) -{ - DdNode *N, *Nv, *Nnv; - DdNode *ThenBranch, *ElseBranch, *childBranch; - DdNode *child, *regChild, *regNnv, *regNv; - NodeDist_t *nodeStatNv, *nodeStat, *nodeStatNnv; - DdNode *neW, *topv, *regNew; - char *entry; - unsigned int topid; - unsigned int childPathLength, oddLen, evenLen, NnvPathLength, NvPathLength; - unsigned int NvBotDist, NnvBotDist; - int tiebreakChild; - int processingDone, thenDone, elseDone; - - -#ifdef DD_DEBUG - numCalls++; -#endif - if (Cudd_IsConstant(node)) - return(node); - - N = Cudd_Regular(node); - /* Find node in table. */ - if (!st_lookup(pathTable, (char *)N, (char **)&nodeStat)) { - (void) fprintf(dd->err, "Something wrong, node must be in table \n"); - dd->errorCode = CUDD_INTERNAL_ERROR; - return(NULL); - } - /* If the node in the table has been visited, then return the corresponding - ** Dd. Since a node can become a subset of itself, its - ** complement (that is te same node reached by a different parity) will - ** become a superset of the original node and result in some minterms - ** that were not in the original set. Hence two different results are - ** maintained, corresponding to the odd and even parities. - */ - - /* If this node is reached with an odd parity, get odd parity results. */ - if (Cudd_IsComplement(node)) { - if (nodeStat->compResult != NULL) { -#ifdef DD_DEBUG - hits++; -#endif - return(nodeStat->compResult); - } - } else { - /* if this node is reached with an even parity, get even parity - * results - */ - if (nodeStat->regResult != NULL) { -#ifdef DD_DEBUG - hits++; -#endif - return(nodeStat->regResult); - } - } - - - /* get children */ - Nv = Cudd_T(N); - Nnv = Cudd_E(N); - - Nv = Cudd_NotCond(Nv, Cudd_IsComplement(node)); - Nnv = Cudd_NotCond(Nnv, Cudd_IsComplement(node)); - - /* no child processed */ - processingDone = 0; - /* then child not processed */ - thenDone = 0; - ThenBranch = NULL; - /* else child not processed */ - elseDone = 0; - ElseBranch = NULL; - /* if then child constant, branch is the child */ - if (Cudd_IsConstant(Nv)) { - /*shortest path found */ - if ((Nv == DD_ONE(dd)) && (info->findShortestPath)) { - info->findShortestPath = 0; - } - - ThenBranch = Nv; - cuddRef(ThenBranch); - if (ThenBranch == NULL) { - return(NULL); - } - - thenDone++; - processingDone++; - NvBotDist = MAXSHORTINT; - } else { - /* Derive regular child for table lookup. */ - regNv = Cudd_Regular(Nv); - /* Get node data for shortest path length. */ - if (!st_lookup(pathTable, (char *)regNv, (char **)&nodeStatNv) ) { - (void) fprintf(dd->err, "Something wrong, node must be in table\n"); - dd->errorCode = CUDD_INTERNAL_ERROR; - return(NULL); - } - /* Derive shortest path length for child. */ - if ((nodeStatNv->oddTopDist != MAXSHORTINT) && - (nodeStatNv->oddBotDist != MAXSHORTINT)) { - oddLen = (nodeStatNv->oddTopDist + nodeStatNv->oddBotDist); - } else { - oddLen = MAXSHORTINT; - } - - if ((nodeStatNv->evenTopDist != MAXSHORTINT) && - (nodeStatNv->evenBotDist != MAXSHORTINT)) { - evenLen = (nodeStatNv->evenTopDist +nodeStatNv->evenBotDist); - } else { - evenLen = MAXSHORTINT; - } - - NvPathLength = (oddLen <= evenLen) ? oddLen : evenLen; - NvBotDist = (oddLen <= evenLen) ? nodeStatNv->oddBotDist: - nodeStatNv->evenBotDist; - } - /* if else child constant, branch is the child */ - if (Cudd_IsConstant(Nnv)) { - /*shortest path found */ - if ((Nnv == DD_ONE(dd)) && (info->findShortestPath)) { - info->findShortestPath = 0; - } - - ElseBranch = Nnv; - cuddRef(ElseBranch); - if (ElseBranch == NULL) { - return(NULL); - } - - elseDone++; - processingDone++; - NnvBotDist = MAXSHORTINT; - } else { - /* Derive regular child for table lookup. */ - regNnv = Cudd_Regular(Nnv); - /* Get node data for shortest path length. */ - if (!st_lookup(pathTable, (char *)regNnv, (char **)&nodeStatNnv) ) { - (void) fprintf(dd->err, "Something wrong, node must be in table\n"); - dd->errorCode = CUDD_INTERNAL_ERROR; - return(NULL); - } - /* Derive shortest path length for child. */ - if ((nodeStatNnv->oddTopDist != MAXSHORTINT) && - (nodeStatNnv->oddBotDist != MAXSHORTINT)) { - oddLen = (nodeStatNnv->oddTopDist + nodeStatNnv->oddBotDist); - } else { - oddLen = MAXSHORTINT; - } - - if ((nodeStatNnv->evenTopDist != MAXSHORTINT) && - (nodeStatNnv->evenBotDist != MAXSHORTINT)) { - evenLen = (nodeStatNnv->evenTopDist +nodeStatNnv->evenBotDist); - } else { - evenLen = MAXSHORTINT; - } - - NnvPathLength = (oddLen <= evenLen) ? oddLen : evenLen; - NnvBotDist = (oddLen <= evenLen) ? nodeStatNnv->oddBotDist : - nodeStatNnv->evenBotDist; - } - - tiebreakChild = (NvBotDist <= NnvBotDist) ? 1 : 0; - /* while both children not processed */ - while (processingDone != 2) { - if (!processingDone) { - /* if no child processed */ - /* pick the child with shortest path length and record which one - * picked - */ - if ((NvPathLength < NnvPathLength) || - ((NvPathLength == NnvPathLength) && (tiebreakChild == 1))) { - child = Nv; - regChild = regNv; - thenDone = 1; - childPathLength = NvPathLength; - } else { - child = Nnv; - regChild = regNnv; - elseDone = 1; - childPathLength = NnvPathLength; - } /* then path length less than else path length */ - } else { - /* if one child processed, process the other */ - if (thenDone) { - child = Nnv; - regChild = regNnv; - elseDone = 1; - childPathLength = NnvPathLength; - } else { - child = Nv; - regChild = regNv; - thenDone = 1; - childPathLength = NvPathLength; - } /* end of else pick the Then child if ELSE child processed */ - } /* end of else one child has been processed */ - - /* ignore (replace with constant 0) all nodes which lie on paths larger - * than the maximum length of the path required - */ - if (childPathLength > info->maxpath) { - /* record nodes visited */ - childBranch = zero; - } else { - if (childPathLength < info->maxpath) { - if (info->findShortestPath) { - info->findShortestPath = 0; - } - childBranch = BuildSubsetBdd(dd, pathTable, child, info, - subsetNodeTable); - - } else { /* Case: path length of node = maxpath */ - /* If the node labeled with maxpath is found in the - ** maxpathTable, use it to build the subset BDD. */ - if (st_lookup(info->maxpathTable, (char *)regChild, - (char **)&entry)) { - /* When a node that is already been chosen is hit, - ** the quest for a complete path is over. */ - if (info->findShortestPath) { - info->findShortestPath = 0; - } - childBranch = BuildSubsetBdd(dd, pathTable, child, info, - subsetNodeTable); - } else { - /* If node is not found in the maxpathTable and - ** the threshold has been reached, then if the - ** path needs to be completed, continue. Else - ** replace the node with a zero. */ - if (info->thresholdReached <= 0) { - if (info->findShortestPath) { - if (st_insert(info->maxpathTable, (char *)regChild, - (char *)NIL(char)) == ST_OUT_OF_MEM) { - memOut = 1; - (void) fprintf(dd->err, "OUT of memory\n"); - info->thresholdReached = 0; - childBranch = zero; - } else { - info->thresholdReached--; - childBranch = BuildSubsetBdd(dd, pathTable, - child, info,subsetNodeTable); - } - } else { /* not find shortest path, we dont need this - node */ - childBranch = zero; - } - } else { /* Threshold hasn't been reached, - ** need the node. */ - if (st_insert(info->maxpathTable, (char *)regChild, - (char *)NIL(char)) == ST_OUT_OF_MEM) { - memOut = 1; - (void) fprintf(dd->err, "OUT of memory\n"); - info->thresholdReached = 0; - childBranch = zero; - } else { - info->thresholdReached--; - if (info->thresholdReached <= 0) { - info->findShortestPath = 1; - } - childBranch = BuildSubsetBdd(dd, pathTable, - child, info, subsetNodeTable); - - } /* end of st_insert successful */ - } /* end of threshold hasnt been reached yet */ - } /* end of else node not found in maxpath table */ - } /* end of if (path length of node = maxpath) */ - } /* end if !(childPathLength > maxpath) */ - if (childBranch == NULL) { - /* deref other stuff incase reordering has taken place */ - if (ThenBranch != NULL) { - Cudd_RecursiveDeref(dd, ThenBranch); - ThenBranch = NULL; - } - if (ElseBranch != NULL) { - Cudd_RecursiveDeref(dd, ElseBranch); - ElseBranch = NULL; - } - return(NULL); - } - - cuddRef(childBranch); - - if (child == Nv) { - ThenBranch = childBranch; - } else { - ElseBranch = childBranch; - } - processingDone++; - - } /*end of while processing Nv, Nnv */ - - info->findShortestPath = 0; - topid = Cudd_NodeReadIndex(N); - topv = Cudd_ReadVars(dd, topid); - cuddRef(topv); - neW = cuddBddIteRecur(dd, topv, ThenBranch, ElseBranch); - if (neW != NULL) { - cuddRef(neW); - } - Cudd_RecursiveDeref(dd, topv); - Cudd_RecursiveDeref(dd, ThenBranch); - Cudd_RecursiveDeref(dd, ElseBranch); - - - /* Hard Limit of threshold has been imposed */ - if (subsetNodeTable != NIL(st_table)) { - /* check if a new node is created */ - regNew = Cudd_Regular(neW); - /* subset node table keeps all new nodes that have been created to keep - * a running count of how many nodes have been built in the subset. - */ - if (!st_lookup(subsetNodeTable, (char *)regNew, (char **)&entry)) { - if (!Cudd_IsConstant(regNew)) { - if (st_insert(subsetNodeTable, (char *)regNew, - (char *)NULL) == ST_OUT_OF_MEM) { - (void) fprintf(dd->err, "Out of memory\n"); - return (NULL); - } - if (st_count(subsetNodeTable) > info->threshold) { - info->thresholdReached = 0; - } - } - } - } - - - if (neW == NULL) { - return(NULL); - } else { - /*store computed result in regular form*/ - if (Cudd_IsComplement(node)) { - nodeStat->compResult = neW; - cuddRef(nodeStat->compResult); - /* if the new node is the same as the corresponding node in the - * original bdd then its complement need not be computed as it - * cannot be larger than the node itself - */ - if (neW == node) { -#ifdef DD_DEBUG - thishit++; -#endif - /* if a result for the node has already been computed, then - * it can only be smaller than teh node itself. hence store - * the node result in order not to break recombination - */ - if (nodeStat->regResult != NULL) { - Cudd_RecursiveDeref(dd, nodeStat->regResult); - } - nodeStat->regResult = Cudd_Not(neW); - cuddRef(nodeStat->regResult); - } - - } else { - nodeStat->regResult = neW; - cuddRef(nodeStat->regResult); - if (neW == node) { -#ifdef DD_DEBUG - thishit++; -#endif - if (nodeStat->compResult != NULL) { - Cudd_RecursiveDeref(dd, nodeStat->compResult); - } - nodeStat->compResult = Cudd_Not(neW); - cuddRef(nodeStat->compResult); - } - } - - cuddDeref(neW); - return(neW); - } /* end of else i.e. Subset != NULL */ -} /* end of BuildSubsetBdd */ - - -/**Function******************************************************************** - - Synopsis [Procedure to free te result dds stored in the NodeDist pages.] - - Description [None] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -static enum st_retval -stPathTableDdFree( - char * key, - char * value, - char * arg) -{ - NodeDist_t *nodeStat; - DdManager *dd; - - nodeStat = (NodeDist_t *)value; - dd = (DdManager *)arg; - if (nodeStat->regResult != NULL) { - Cudd_RecursiveDeref(dd, nodeStat->regResult); - } - if (nodeStat->compResult != NULL) { - Cudd_RecursiveDeref(dd, nodeStat->compResult); - } - return(ST_CONTINUE); - -} /* end of stPathTableFree */ |