cuddtable.c

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

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

  FileName    [cuddTable.c]

  PackageName [cudd]

  Synopsis    [Unique table management functions.]

  Description [External procedures included in this module:
		<ul>
		<li> Cudd_Prime()
		</ul>
	Internal procedures included in this module:
		<ul>
		<li> cuddAllocNode()
		<li> cuddInitTable()
		<li> cuddFreeTable()
		<li> cuddGarbageCollect()
		<li> cuddGarbageCollectZdd()
		<li> cuddZddGetNode()
		<li> cuddZddGetNodeIVO()
		<li> cuddUniqueInter()
		<li> cuddUniqueInterIVO()
		<li> cuddUniqueInterZdd()
		<li> cuddUniqueConst()
		<li> cuddRehash()
		<li> cuddShrinkSubtable()
		<li> cuddInsertSubtables()
		<li> cuddDestroySubtables()
		<li> cuddResizeTableZdd()
		<li> cuddSlowTableGrowth()
		</ul>
	Static procedures included in this module:
		<ul>
		<li> ddRehashZdd()
		<li> ddResizeTable()
		<li> cuddFindParent()
		<li> cuddOrderedInsert()
		<li> cuddOrderedThread()
		<li> cuddRotateLeft()
		<li> cuddRotateRight()
		<li> cuddDoRebalance()
		<li> cuddCheckCollisionOrdering()
		</ul>]

  SeeAlso     []

  Author      [Fabio Somenzi]

  Copyright   [This file was created at the University of Colorado at
  Boulder.  The University of Colorado at Boulder makes no warranty
  about the suitability of this software for any purpose.  It is
  presented on an AS IS basis.]

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

#include    "util.h"
#include    "cuddInt.h"

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

#ifndef DD_UNSORTED_FREE_LIST
/* Constants for red/black trees. */
#define DD_STACK_SIZE 128
#define DD_RED   0
#define DD_BLACK 1
#define DD_PAGE_SIZE 8192
#define DD_PAGE_MASK ~(DD_PAGE_SIZE - 1)
#define DD_INSERT_COMPARE(x,y) \
	(((ptruint) (x) & DD_PAGE_MASK) - ((ptruint) (y) & DD_PAGE_MASK))
#endif

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

/* This is a hack for when CUDD_VALUE_TYPE is double */
typedef union hack {
    CUDD_VALUE_TYPE value;
    unsigned int bits[2];
} hack;

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

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

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

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


#ifndef DD_UNSORTED_FREE_LIST
/* Macros for red/black trees. */
#define DD_COLOR(p)  ((p)->index)
#define DD_IS_BLACK(p) ((p)->index == DD_BLACK)
#define DD_IS_RED(p) ((p)->index == DD_RED)
#define DD_LEFT(p) cuddT(p)
#define DD_RIGHT(p) cuddE(p)
#define DD_NEXT(p) ((p)->next)
#endif


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

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

static void ddRehashZdd ARGS((DdManager *unique, int i));
static int ddResizeTable ARGS((DdManager *unique, int index));
static int cuddFindParent ARGS((DdManager *table, DdNode *node));
DD_INLINE static void ddFixLimits ARGS((DdManager *unique));
static void cuddOrderedInsert ARGS((DdNodePtr *root, DdNodePtr node));
static DdNode * cuddOrderedThread ARGS((DdNode *root, DdNode *list));
static void cuddRotateLeft ARGS((DdNodePtr *nodeP));
static void cuddRotateRight ARGS((DdNodePtr *nodeP));
static void cuddDoRebalance ARGS((DdNodePtr **stack, int stackN));
static void ddPatchTree ARGS((DdManager *dd, MtrNode *treenode));
#ifdef DD_DEBUG
static int cuddCheckCollisionOrdering ARGS((DdManager *unique, int i, int j));
#endif
static void ddReportRefMess ARGS((DdManager *unique, int i, char *caller));

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


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


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

  Synopsis    [Returns the next prime &gt;= p.]

  Description []

  SideEffects [None]

******************************************************************************/
unsigned int
Cudd_Prime(
  unsigned int  p)
{
    int i,pn;

    p--;
    do {
        p++;
        if (p&1) {
	    pn = 1;
	    i = 3;
	    while ((unsigned) (i * i) <= p) {
		if (p % i == 0) {
		    pn = 0;
		    break;
		}
		i += 2;
	    }
	} else {
	    pn = 0;
	}
    } while (!pn);
    return(p);

} /* end of Cudd_Prime */


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


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

  Synopsis    [Fast storage allocation for DdNodes in the table.]

  Description [Fast storage allocation for DdNodes in the table. The
  first 4 bytes of a chunk contain a pointer to the next block; the
  rest contains DD_MEM_CHUNK spaces for DdNodes.  Returns a pointer to
  a new node if successful; NULL is memory is full.]

  SideEffects [None]

  SeeAlso     [cuddDynamicAllocNode]

******************************************************************************/
DdNode *
cuddAllocNode(
  DdManager * unique)
{
    int i;
    DdNodePtr *mem;
    DdNode *list, *node;
    extern void (*MMoutOfMemory)(long);
    void (*saveHandler)(long);

    if (unique->nextFree == NULL) {	/* free list is empty */
	/* Check for exceeded limits. */
	if ((unique->keys - unique->dead) + (unique->keysZ - unique->deadZ) >
	    unique->maxLive) {
	    unique->errorCode = CUDD_TOO_MANY_NODES;
	    return(NULL);
	}
	if (unique->stash == NULL || unique->memused > unique->maxmemhard) {
	    (void) cuddGarbageCollect(unique,1);
	    mem = NULL;
	}
	if (unique->nextFree == NULL) {
	    if (unique->memused > unique->maxmemhard) {
		unique->errorCode = CUDD_MAX_MEM_EXCEEDED;
		return(NULL);
	    }
	    /* Try to allocate a new block. */
	    saveHandler = MMoutOfMemory;
	    MMoutOfMemory = Cudd_OutOfMem;
	    mem = (DdNodePtr *) ALLOC(DdNode,DD_MEM_CHUNK + 1);
	    MMoutOfMemory = saveHandler;
	    if (mem == NULL) {
		/* No more memory: Try collecting garbage. If this succeeds,
		** we end up with mem still NULL, but unique->nextFree !=
		** NULL. */
		if (cuddGarbageCollect(unique,1) == 0) {
		    /* Last resort: Free the memory stashed away, if there
		    ** any. If this succeeeds, mem != NULL and
		    ** unique->nextFree still NULL. */
		    if (unique->stash != NULL) {
			FREE(unique->stash);
			unique->stash = NULL;
			/* Inhibit resizing of tables. */
			cuddSlowTableGrowth(unique);
			/* Now try again. */
			mem = (DdNodePtr *) ALLOC(DdNode,DD_MEM_CHUNK + 1);
		    }
		    if (mem == NULL) {
			/* Out of luck. Call the default handler to do
			** whatever it specifies for a failed malloc.
			** If this handler returns, then set error code,
			** print warning, and return. */
			(*MMoutOfMemory)(sizeof(DdNode)*(DD_MEM_CHUNK + 1));
			unique->errorCode = CUDD_MEMORY_OUT;
#ifdef DD_VERBOSE
			(void) fprintf(unique->err,
				       "cuddAllocNode: out of memory");
			(void) fprintf(unique->err, "Memory in use = %ld\n",
				       unique->memused);
#endif
			return(NULL);
		    }
		}
	    }
	    if (mem != NULL) {	/* successful allocation; slice memory */
		ptruint offset;
		unique->memused += (DD_MEM_CHUNK + 1) * sizeof(DdNode);
		mem[0] = (DdNodePtr) unique->memoryList;
		unique->memoryList = mem;

		/* Here we rely on the fact that a DdNode is as large
		** as 4 pointers.  */
		offset = (ptruint) mem & (sizeof(DdNode) - 1);
		mem += (sizeof(DdNode) - offset) / sizeof(DdNodePtr);
		assert(((ptruint) mem & (sizeof(DdNode) - 1)) == 0);
		list = (DdNode *) mem;

		i = 1;
		do {
		    list[i - 1].next = &list[i];
		} while (++i < DD_MEM_CHUNK);

		list[DD_MEM_CHUNK-1].next = NULL;

		unique->nextFree = &list[0];
	    }
	}
    }
    unique->allocated++;
    node = unique->nextFree;
    unique->nextFree = node->next;
    return(node);

} /* end of cuddAllocNode */


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

  Synopsis    [Creates and initializes the unique table.]

  Description [Creates and initializes the unique table. Returns a pointer
  to the table if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_Init cuddFreeTable]

******************************************************************************/
DdManager *
cuddInitTable(
  unsigned int numVars  /* Initial number of BDD variables (and subtables) */,
  unsigned int numVarsZ /* Initial number of ZDD variables (and subtables) */,
  unsigned int numSlots /* Initial size of the BDD subtables */,
  unsigned int looseUpTo /* Limit for fast table growth */)
{
    DdManager	*unique = ALLOC(DdManager,1);
    int		i, j;
    DdNodePtr	*nodelist;
    DdNode	*sentinel;
    unsigned int slots;
    int shift;

    if (unique == NULL) {
	return(NULL);
    }
    sentinel = &(unique->sentinel);
    sentinel->ref = 0;
    sentinel->index = 0;
    cuddT(sentinel) = NULL;
    cuddE(sentinel) = NULL;
    sentinel->next = NULL;
    unique->epsilon = DD_EPSILON;
    unique->maxGrowth = DD_MAX_REORDER_GROWTH;
    unique->maxGrowthAlt = 2.0 * DD_MAX_REORDER_GROWTH;
    unique->reordCycle = 0;	/* do not use alternate threshold */
    unique->size = numVars;
    unique->sizeZ = numVarsZ;
    unique->maxSize = ddMax(DD_DEFAULT_RESIZE, numVars);
    unique->maxSizeZ = ddMax(DD_DEFAULT_RESIZE, numVarsZ);

    /* Adjust the requested number of slots to a power of 2. */
    slots = 8;
    while (slots < numSlots) {
	slots <<= 1;
    }
    unique->initSlots = slots;
    shift = sizeof(int) * 8 - cuddComputeFloorLog2(slots);

    unique->slots = (numVars + numVarsZ + 1) * slots;
    unique->keys = 0;
    unique->maxLive = ~0;	/* very large number */
    unique->keysZ = 0;
    unique->dead = 0;
    unique->deadZ = 0;
    unique->gcFrac = DD_GC_FRAC_HI;
    unique->minDead = (unsigned) (DD_GC_FRAC_HI * (double) unique->slots);
    unique->looseUpTo = looseUpTo;
    unique->gcEnabled = 1;
    unique->allocated = 0;
    unique->reclaimed = 0;
    unique->subtables = ALLOC(DdSubtable,unique->maxSize);
    if (unique->subtables == NULL) {
	unique->errorCode = CUDD_MEMORY_OUT;
	return(0);
    }
    unique->subtableZ = ALLOC(DdSubtable,unique->maxSizeZ);
    if (unique->subtableZ == NULL) {
	unique->errorCode = CUDD_MEMORY_OUT;
	return(0);
    }
    unique->perm = ALLOC(int,unique->maxSize);
    if (unique->perm == NULL) {
	unique->errorCode = CUDD_MEMORY_OUT;
	return(0);
    }
    unique->invperm = ALLOC(int,unique->maxSize);
    if (unique->invperm == NULL) {
	unique->errorCode = CUDD_MEMORY_OUT;
	return(0);
    }
    unique->permZ = ALLOC(int,unique->maxSizeZ);
    if (unique->permZ == NULL) {
	unique->errorCode = CUDD_MEMORY_OUT;
	return(0);
    }
    unique->invpermZ = ALLOC(int,unique->maxSizeZ);
    if (unique->invpermZ == NULL) {
	unique->errorCode = CUDD_MEMORY_OUT;
	return(0);
    }
    unique->map = NULL;
    unique->stack = ALLOC(DdNodePtr,ddMax(unique->maxSize,unique->maxSizeZ)+1);
    if (unique->stack == NULL) {
	unique->errorCode = CUDD_MEMORY_OUT;
	return(0);
    }
    unique->stack[0] = NULL; /* to suppress harmless UMR */

#ifndef DD_NO_DEATH_ROW
    unique->deathRowDepth = 1 << cuddComputeFloorLog2(unique->looseUpTo >> 2);
    unique->deathRow = ALLOC(DdNodePtr,unique->deathRowDepth);
    if (unique->deathRow == NULL) {
	unique->errorCode = CUDD_MEMORY_OUT;
	return(0);
    }
    for (i = 0; i < unique->deathRowDepth; i++) {
	unique->deathRow[i] = NULL;
    }
    unique->nextDead = 0;
    unique->deadMask = unique->deathRowDepth - 1;
#endif

    for (i = 0; (unsigned) i < numVars; i++) {
	unique->subtables[i].slots = slots;
	unique->subtables[i].shift = shift;
	unique->subtables[i].keys = 0;
	unique->subtables[i].dead = 0;
	unique->subtables[i].maxKeys = slots * DD_MAX_SUBTABLE_DENSITY;
	unique->subtables[i].bindVar = 0;
	unique->subtables[i].varType = CUDD_VAR_PRIMARY_INPUT;
	unique->subtables[i].pairIndex = 0;
	unique->subtables[i].varHandled = 0;
	unique->subtables[i].varToBeGrouped = CUDD_LAZY_NONE;

	nodelist = unique->subtables[i].nodelist = ALLOC(DdNodePtr,slots);
	if (nodelist == NULL) {
	    unique->errorCode = CUDD_MEMORY_OUT;
	    return(NULL);
	}
	for (j = 0; (unsigned) j < slots; j++) {
	    nodelist[j] = sentinel;
	}
	unique->perm[i] = i;
	unique->invperm[i] = i;
    }
    for (i = 0; (unsigned) i < numVarsZ; i++) {
	unique->subtableZ[i].slots = slots;
	unique->subtableZ[i].shift = shift;
	unique->subtableZ[i].keys = 0;
	unique->subtableZ[i].dead = 0;
	unique->subtableZ[i].maxKeys = slots * DD_MAX_SUBTABLE_DENSITY;
	nodelist = unique->subtableZ[i].nodelist = ALLOC(DdNodePtr,slots);
	if (nodelist == NULL) {
	    unique->errorCode = CUDD_MEMORY_OUT;