cuddsubsetsp.c

主要进行大规模的电路综合

	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);