cuddsubsethb.c

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

/**CFile***********************************************************************

  FileName    [cuddSubsetHB.c]

  PackageName [cudd]

  Synopsis    [Procedure to subset the given BDD by choosing the heavier
		branches]


  Description [External procedures provided by this module:
                <ul>
		<li> Cudd_SubsetHeavyBranch()
		<li> Cudd_SupersetHeavyBranch()
		</ul>
	       Internal procedures included in this module:
		<ul>
		<li> cuddSubsetHeavyBranch()
		</ul>
	       Static procedures included in this module:
		<ul>
		<li> ResizeCountMintermPages();
		<li> ResizeNodeDataPages()
		<li> ResizeCountNodePages()
		<li> SubsetCountMintermAux()
		<li> SubsetCountMinterm()
		<li> SubsetCountNodesAux()
		<li> SubsetCountNodes()
		<li> BuildSubsetBdd()
		</ul>
		]

  SeeAlso     [cuddSubsetSP.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.]

******************************************************************************/

#ifdef __STDC__
#include <float.h>
#else
#define DBL_MAX_EXP 1024
#endif
#include "util.h"
#include "cuddInt.h"

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

#define	DEFAULT_PAGE_SIZE 2048
#define	DEFAULT_NODE_DATA_PAGE_SIZE 1024
#define INITIAL_PAGES 128


/*---------------------------------------------------------------------------*/
/* Stucture declarations                                                     */
/*---------------------------------------------------------------------------*/

/* data structure to store the information on each node. It keeps
 * the number of minterms represented by the DAG rooted at this node
 * in terms of the number of variables specified by the user, number
 * of nodes in this DAG and the number of nodes of its child with
 * lesser number of minterms that are not shared by the child with
 * more minterms
 */
struct NodeData {
    double *mintermPointer;
    int *nodesPointer;
    int *lightChildNodesPointer;
};

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/

typedef struct NodeData NodeData_t;

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

#ifndef lint
static char rcsid[] DD_UNUSED = "$Id: cuddSubsetHB.c,v 1.1.1.1 2003/02/24 22:23:53 wjiang Exp $";
#endif

static int memOut;
#ifdef DEBUG
static	int		num_calls;
#endif

static	DdNode	        *zero, *one; /* constant functions */
static	double		**mintermPages;	/* pointers to the pages */
static	int		**nodePages; /* pointers to the pages */
static	int		**lightNodePages; /* pointers to the pages */
static	double		*currentMintermPage; /* pointer to the current
						   page */
static  double 		max; /* to store the 2^n value of the number
			      * of variables */

static	int		*currentNodePage; /* pointer to the current
						   page */
static	int		*currentLightNodePage; /* pointer to the
						*  current page */
static	int		pageIndex; /* index to next element */
static	int		page; /* index to current page */
static	int		pageSize = DEFAULT_PAGE_SIZE; /* page size */
static  int             maxPages; /* number of page pointers */

static	NodeData_t	*currentNodeDataPage; /* pointer to the current
						 page */
static	int		nodeDataPage; /* index to next element */
static	int		nodeDataPageIndex; /* index to next element */
static	NodeData_t	**nodeDataPages; /* index to current page */
static	int		nodeDataPageSize = DEFAULT_NODE_DATA_PAGE_SIZE;
                                                     /* page size */
static  int             maxNodeDataPages; /* number of page pointers */


/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

/**AutomaticStart*************************************************************/

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

static void ResizeNodeDataPages ARGS(());
static void ResizeCountMintermPages ARGS(());
static void ResizeCountNodePages ARGS(());
static double SubsetCountMintermAux ARGS((DdNode *node, double max, st_table *table));
static st_table * SubsetCountMinterm ARGS((DdNode *node, int nvars));
static int SubsetCountNodesAux ARGS((DdNode *node, st_table *table, double max));
static int SubsetCountNodes ARGS((DdNode *node, st_table *table, int nvars));
static void StoreNodes ARGS((st_table *storeTable, DdManager *dd, DdNode *node));
static DdNode * BuildSubsetBdd ARGS((DdManager *dd, DdNode *node, int *size, st_table *visitedTable, int threshold, st_table *storeTable, st_table *approxTable));

/**AutomaticEnd***************************************************************/


/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/

/**Function********************************************************************

  Synopsis    [Extracts a dense subset from a BDD with the heavy branch
  heuristic.]

  Description [Extracts a dense subset from a BDD. This procedure
  builds a subset by throwing away one of the children of each node,
  starting from the root, until the result is small enough. The child
  that is eliminated from the result is the one that contributes the
  fewer minterms.  Returns a pointer to the BDD of the subset if
  successful. NULL if the procedure runs out of memory. The parameter
  numVars is the maximum number of variables to be used in minterm
  calculation and node count calculation.  The optimal number should
  be as close as possible to the size of the support of f.  However,
  it is safe to pass the value returned by Cudd_ReadSize for numVars
  when the number of variables is under 1023.  If numVars is larger
  than 1023, it will overflow. If a 0 parameter is passed then the
  procedure will compute a value which will avoid overflow but will
  cause underflow with 2046 variables or more.]

  SideEffects [None]

  SeeAlso     [Cudd_SubsetShortPaths Cudd_SupersetHeavyBranch Cudd_ReadSize]

******************************************************************************/
DdNode *
Cudd_SubsetHeavyBranch(
  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 */)
{
    DdNode *subset;

    memOut = 0;
    do {
	dd->reordered = 0;
	subset = cuddSubsetHeavyBranch(dd, f, numVars, threshold);
    } while ((dd->reordered == 1) && (!memOut));

    return(subset);

} /* end of Cudd_SubsetHeavyBranch */


/**Function********************************************************************

  Synopsis    [Extracts a dense superset from a BDD with the heavy branch
  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 builds a superset by throwing away
  one of the children of each node starting from the root of the
  complement function, until the result is small enough. The child
  that is eliminated from the result is the one that contributes the
  fewer minterms.
  Returns a pointer to the BDD of the superset if successful. NULL if
  intermediate result causes the procedure to run out of memory. The
  parameter numVars is the maximum number of variables to be used in
  minterm calculation and node count calculation.  The optimal number
  should be as close as possible to the size of the support of f.
  However, it is safe to pass the value returned by Cudd_ReadSize for
  numVars when the number of variables is under 1023.  If numVars is
  larger than 1023, it will overflow. If a 0 parameter is passed then
  the procedure will compute a value which will avoid overflow but
  will cause underflow with 2046 variables or more.]

  SideEffects [None]

  SeeAlso     [Cudd_SubsetHeavyBranch Cudd_SupersetShortPaths Cudd_ReadSize]

******************************************************************************/
DdNode *
Cudd_SupersetHeavyBranch(
  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 superset */)
{
    DdNode *subset, *g;

    g = Cudd_Not(f);    
    memOut = 0;
    do {
	dd->reordered = 0;
	subset = cuddSubsetHeavyBranch(dd, g, numVars, threshold);
    } while ((dd->reordered == 1) && (!memOut));
    
    return(Cudd_NotCond(subset, (subset != NULL)));
    
} /* end of Cudd_SupersetHeavyBranch */


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/


/**Function********************************************************************

  Synopsis    [The main procedure that returns a subset by choosing the heavier
  branch in the BDD.]

  Description [Here a subset BDD is built by throwing away one of the
  children. Starting at root, annotate each node with the number of
  minterms (in terms of the total number of variables specified -
  numVars), number of nodes taken by the DAG rooted at this node and
  number of additional nodes taken by the child that has the lesser
  minterms. The child with the lower number of minterms is thrown away
  and a dyanmic count of the nodes of the subset is kept. Once the
  threshold is reached the subset is returned to the calling
  procedure.]

  SideEffects [None]

  SeeAlso     [Cudd_SubsetHeavyBranch]

******************************************************************************/
DdNode *
cuddSubsetHeavyBranch(
  DdManager * dd /* DD manager */,
  DdNode * f /* current DD */,
  int  numVars /* maximum number of variables */,
  int  threshold /* threshold size for the subset */)
{

    int i, *size;
    st_table *visitedTable;
    int numNodes;
    NodeData_t *currNodeQual;
    DdNode *subset;
    double minN;
    st_table *storeTable, *approxTable;
    char *key, *value;
    st_generator *stGen;
    
    if (f == NULL) {
	fprintf(dd->err, "Cannot subset, nil object\n");
	dd->errorCode = CUDD_INVALID_ARG;
	return(NULL);
    }

    one	 = Cudd_ReadOne(dd);
    zero = Cudd_Not(one);

    /* If user does not know numVars value, set it to the maximum
     * exponent that the pow function can take. The -1 is due to the
     * discrepancy in the value that pow takes and the value that
     * log gives.
     */
    if (numVars == 0) {
	/* set default value */
	numVars = DBL_MAX_EXP - 1;
    }

    if (Cudd_IsConstant(f)) {
	return(f);
    }

    max = pow(2.0, (double)numVars);

    /* Create visited table where structures for node data are allocated and
       stored in a st_table */
    visitedTable = SubsetCountMinterm(f, numVars);
    if ((visitedTable == NULL) || memOut) {
	(void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
	dd->errorCode = CUDD_MEMORY_OUT;
	return(0);
    }
    numNodes = SubsetCountNodes(f, visitedTable, numVars);
    if (memOut) {
	(void) fprintf(dd->err, "Out-of-memory; Cannot subset\n");
	dd->errorCode = CUDD_MEMORY_OUT;
	return(0);
    }

    if (st_lookup(visitedTable, (char *)f, (char **)&currNodeQual)) {
	minN = *(((NodeData_t *)currNodeQual)->mintermPointer);
    } else {
	fprintf(dd->err,
		"Something is wrong, ought to be node quality table\n");
	dd->errorCode = CUDD_INTERNAL_ERROR;
    }

    size = ALLOC(int, 1);
    if (size == NULL) {
	dd->errorCode = CUDD_MEMORY_OUT;
	return(NULL);
    }
    *size = numNodes;

#ifdef DEBUG
    num_calls = 0;
#endif
    /* table to store nodes being created. */
    storeTable = st_init_table(st_ptrcmp, st_ptrhash);
    /* insert the constant */
    cuddRef(one);
    if (st_insert(storeTable, (char *)Cudd_ReadOne(dd), NIL(char)) ==
	ST_OUT_OF_MEM) {
	fprintf(dd->out, "Something wrong, st_table insert failed\n");
    }
    /* table to store approximations of nodes */
    approxTable = st_init_table(st_ptrcmp, st_ptrhash);
    subset = (DdNode *)BuildSubsetBdd(dd, f, size, visitedTable, threshold,
				      storeTable, approxTable);
    if (subset != NULL) {
	cuddRef(subset);
    }

    stGen = st_init_gen(approxTable);
    if (stGen == NULL) {
	st_free_table(approxTable);
	return(NULL);
    }
    while(st_gen(stGen, (char **)&key, (char **)&value)) {
	Cudd_RecursiveDeref(dd, (DdNode *)value);
    }
    st_free_gen(stGen); stGen = NULL;
    st_free_table(approxTable);

    stGen = st_init_gen(storeTable);
    if (stGen == NULL) {
	st_free_table(storeTable);
	return(NULL);
    }
    while(st_gen(stGen, (char **)&key, (char **)&value)) {
	Cudd_RecursiveDeref(dd, (DdNode *)key);
    }
    st_free_gen(stGen); stGen = NULL;
    st_free_table(storeTable);

    for (i = 0; i <= page; i++) {
	FREE(mintermPages[i]);
    }
    FREE(mintermPages);
    for (i = 0; i <= page; i++) {
	FREE(nodePages[i]);
    }
    FREE(nodePages);
    for (i = 0; i <= page; i++) {
	FREE(lightNodePages[i]);
    }
    FREE(lightNodePages);
    for (i = 0; i <= nodeDataPage; i++) {
	FREE(nodeDataPages[i]);
    }
    FREE(nodeDataPages);
    st_free_table(visitedTable);
    FREE(size);
#if 0
    (void) Cudd_DebugCheck(dd);
    (void) Cudd_CheckKeys(dd);
#endif

    if (subset != NULL) {
#ifdef DD_DEBUG
      if (!Cudd_bddLeq(dd, subset, f)) {
	    fprintf(dd->err, "Wrong subset\n");
	    dd->errorCode = CUDD_INTERNAL_ERROR;
	    return(NULL);
      }
#endif
        cuddDeref(subset);
        return(subset);
    } else {
        return(NULL);
    }
} /* end of cuddSubsetHeavyBranch */


/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/


/**Function********************************************************************

  Synopsis    [Resize the number of pages allocated to store the node data.]

  Description [Resize the number of pages allocated to store the node data
  The procedure  moves the counter to the next page when the end of
  the page is reached and allocates new pages when necessary.]