cuddsubsetsp.c

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

/**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.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