cuddtable.c

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

    level = unique->permZ[index];
    subtable = &(unique->subtableZ[level]);

#ifdef DD_DEBUG
    assert(level < (unsigned) cuddIZ(unique,T->index));
    assert(level < (unsigned) cuddIZ(unique,Cudd_Regular(E)->index));
#endif

    if (subtable->keys > subtable->maxKeys) {
        if (unique->gcEnabled && ((unique->deadZ > unique->minDead) ||
	(10 * subtable->dead > 9 * subtable->keys))) { 	/* too many dead */
	    (void) cuddGarbageCollectZdd(unique,1);
	} else {
	    ddRehashZdd(unique,(int)level);
	}
    }

    pos = ddHash(T, E, subtable->shift);
    nodelist = subtable->nodelist;
    looking = nodelist[pos];

    while (looking != NULL) {
        if (cuddT(looking) == T && cuddE(looking) == E) {
	    if (looking->ref == 0) {
		cuddReclaimZdd(unique,looking);
	    }
	    return(looking);
	}
	looking = looking->next;
#ifdef DD_UNIQUE_PROFILE
	unique->uniqueLinks++;
#endif
    }

    /* countDead is 0 if deads should be counted and ~0 if they should not. */
    if (unique->autoDynZ &&
    unique->keysZ - (unique->deadZ & unique->countDead) >= unique->nextDyn) {
#ifdef DD_DEBUG
	retval = Cudd_DebugCheck(unique);
	if (retval != 0) return(NULL);
	retval = Cudd_CheckKeys(unique);
	if (retval != 0) return(NULL);
#endif
	retval = Cudd_zddReduceHeap(unique,unique->autoMethodZ,10); /* 10 = whatever */
	if (retval == 0) unique->reordered = 2;
#ifdef DD_DEBUG
	retval = Cudd_DebugCheck(unique);
	if (retval != 0) unique->reordered = 2;
	retval = Cudd_CheckKeys(unique);
	if (retval != 0) unique->reordered = 2;
#endif
	return(NULL);
    }

    unique->keysZ++;
    subtable->keys++;

    looking = cuddAllocNode(unique);
    if (looking == NULL) return(NULL);
    looking->ref = 0;
    looking->index = index;
    cuddT(looking) = T;
    cuddE(looking) = E;
    looking->next = nodelist[pos];
    nodelist[pos] = looking;
    cuddRef(T);
    cuddRef(E);

    return(looking);

} /* end of cuddUniqueInterZdd */


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

  Synopsis    [Checks the unique table for the existence of a constant node.]

  Description [Checks the unique table for the existence of a constant node.
  If it does not exist, it creates a new one.  Does not
  modify the reference count of whatever is returned.  A newly created
  internal node comes back with a reference count 0.  Returns a
  pointer to the new node.]

  SideEffects [None]

******************************************************************************/
DdNode *
cuddUniqueConst(
  DdManager * unique,
  CUDD_VALUE_TYPE  value)
{
    int pos;
    DdNodePtr *nodelist;
    DdNode *looking;
    hack split;

#ifdef DD_UNIQUE_PROFILE
    unique->uniqueLookUps++;
#endif

    if (unique->constants.keys > unique->constants.maxKeys) {
        if (unique->gcEnabled && ((unique->dead > unique->minDead) ||
	(10 * unique->constants.dead > 9 * unique->constants.keys))) { 	/* too many dead */
	    (void) cuddGarbageCollect(unique,1);
	} else {
	    cuddRehash(unique,CUDD_CONST_INDEX);
	}
    }

    cuddAdjust(value); /* for the case of crippled infinities */

    if (ddAbs(value) < unique->epsilon) {
	value = 0.0;
    }
    split.value = value;

    pos = ddHash(split.bits[0], split.bits[1], unique->constants.shift);
    nodelist = unique->constants.nodelist;
    looking = nodelist[pos];

    /* Here we compare values both for equality and for difference less
     * than epsilon. The first comparison is required when values are
     * infinite, since Infinity - Infinity is NaN and NaN < X is 0 for
     * every X.
     */
    while (looking != NULL) {
        if (looking->type.value == value ||
	ddEqualVal(looking->type.value,value,unique->epsilon)) {
	    if (looking->ref == 0) {
		cuddReclaim(unique,looking);
	    }
	    return(looking);
	}
	looking = looking->next;
#ifdef DD_UNIQUE_PROFILE
	unique->uniqueLinks++;
#endif
    }

    unique->keys++;
    unique->constants.keys++;

    looking = cuddAllocNode(unique);
    if (looking == NULL) return(NULL);
    looking->ref = 0;
    looking->index = CUDD_CONST_INDEX;
    looking->type.value = value;
    looking->next = nodelist[pos];
    nodelist[pos] = looking;

    return(looking);

} /* end of cuddUniqueConst */


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

  Synopsis    [Rehashes a unique subtable.]

  Description [Doubles the size of a unique subtable and rehashes its
  contents.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
void
cuddRehash(
  DdManager * unique,
  int i)
{
    unsigned int slots, oldslots;
    int shift, oldshift;
    int j, pos;
    DdNodePtr *nodelist, *oldnodelist;
    DdNode *node, *next;
    DdNode *sentinel = &(unique->sentinel);
    hack split;
    extern void (*MMoutOfMemory)(long);
    void (*saveHandler)(long);

    if (unique->gcFrac == DD_GC_FRAC_HI && unique->slots > unique->looseUpTo) {
	unique->gcFrac = DD_GC_FRAC_LO;
	unique->minDead = (unsigned) (DD_GC_FRAC_LO * (double) unique->slots);
#ifdef DD_VERBOSE
	(void) fprintf(unique->err,"GC fraction = %.2f\t", DD_GC_FRAC_LO);
	(void) fprintf(unique->err,"minDead = %d\n", unique->minDead);
#endif
    }

    if (unique->gcFrac != DD_GC_FRAC_MIN && unique->memused > unique->maxmem) {
	unique->gcFrac = DD_GC_FRAC_MIN;
	unique->minDead = (unsigned) (DD_GC_FRAC_MIN * (double) unique->slots);
#ifdef DD_VERBOSE
	(void) fprintf(unique->err,"GC fraction = %.2f\t", DD_GC_FRAC_MIN);
	(void) fprintf(unique->err,"minDead = %d\n", unique->minDead);
#endif
	cuddShrinkDeathRow(unique);
	if (cuddGarbageCollect(unique,1) > 0) return;
    }

    if (i != CUDD_CONST_INDEX) {
	oldslots = unique->subtables[i].slots;
	oldshift = unique->subtables[i].shift;
	oldnodelist = unique->subtables[i].nodelist;

	/* Compute the new size of the subtable. */
	slots = oldslots << 1;
	shift = oldshift - 1;

	saveHandler = MMoutOfMemory;
	MMoutOfMemory = Cudd_OutOfMem;
	nodelist = ALLOC(DdNodePtr, slots);
	MMoutOfMemory = saveHandler;
	if (nodelist == NULL) {
	    (void) fprintf(unique->err,
			   "Unable to resize subtable %d for lack of memory\n",
			   i);
	    /* Prevent frequent resizing attempts. */
	    (void) cuddGarbageCollect(unique,1);
	    if (unique->stash != NULL) {
		FREE(unique->stash);
		unique->stash = NULL;
		/* Inhibit resizing of tables. */
		cuddSlowTableGrowth(unique);
	    }
	    return;
	}
	unique->subtables[i].nodelist = nodelist;
	unique->subtables[i].slots = slots;
	unique->subtables[i].shift = shift;
	unique->subtables[i].maxKeys = slots * DD_MAX_SUBTABLE_DENSITY;

	/* Move the nodes from the old table to the new table.
	** This code depends on the type of hash function.
	** It assumes that the effect of doubling the size of the table
	** is to retain one more bit of the 32-bit hash value.
	** The additional bit is the LSB. */
	for (j = 0; (unsigned) j < oldslots; j++) {
	    DdNodePtr *evenP, *oddP;
	    node = oldnodelist[j];
	    evenP = &(nodelist[j<<1]);
	    oddP = &(nodelist[(j<<1)+1]);
	    while (node != sentinel) {
		next = node->next;
		pos = ddHash(cuddT(node), cuddE(node), shift);
		if (pos & 1) {
		    *oddP = node;
		    oddP = &(node->next);
		} else {
		    *evenP = node;
		    evenP = &(node->next);
		}
		node = next;
	    }
	    *evenP = *oddP = sentinel;
	}
	FREE(oldnodelist);

#ifdef DD_VERBOSE
	(void) fprintf(unique->err,
		       "rehashing layer %d: keys %d dead %d new size %d\n",
		       i, unique->subtables[i].keys,
		       unique->subtables[i].dead, slots);
#endif
    } else {
	oldslots = unique->constants.slots;
	oldshift = unique->constants.shift;
	oldnodelist = unique->constants.nodelist;

	/* The constant subtable is never subjected to reordering.
	** Therefore, when it is resized, it is because it has just
	** reached the maximum load. We can safely just double the size,
	** with no need for the loop we use for the other tables.
	*/
	slots = oldslots << 1;
	shift = oldshift - 1;
	saveHandler = MMoutOfMemory;
	MMoutOfMemory = Cudd_OutOfMem;
	nodelist = ALLOC(DdNodePtr, slots);
	MMoutOfMemory = saveHandler;
	if (nodelist == NULL) {
	    int j;
	    (void) fprintf(unique->err,
			   "Unable to resize constant subtable for lack of memory\n");
	    (void) cuddGarbageCollect(unique,1);
	    for (j = 0; j < unique->size; j++) {
		unique->subtables[j].maxKeys <<= 1;
	    }
	    unique->constants.maxKeys <<= 1;
	    return;
	}
	unique->constants.slots = slots;
	unique->constants.shift = shift;
	unique->constants.maxKeys = slots * DD_MAX_SUBTABLE_DENSITY;
	unique->constants.nodelist = nodelist;
	for (j = 0; (unsigned) j < slots; j++) {
	    nodelist[j] = NULL;
	}
	for (j = 0; (unsigned) j < oldslots; j++) {
	    node = oldnodelist[j];
	    while (node != NULL) {
		next = node->next;
		split.value = cuddV(node);
		pos = ddHash(split.bits[0], split.bits[1], shift);
		node->next = nodelist[pos];
		nodelist[pos] = node;
		node = next;
	    }
	}
	FREE(oldnodelist);

#ifdef DD_VERBOSE
	(void) fprintf(unique->err,
		       "rehashing constants: keys %d dead %d new size %d\n",
		       unique->constants.keys,unique->constants.dead,slots);
#endif
    }

    /* Update global data */

    unique->memused += (slots - oldslots) * sizeof(DdNodePtr);
    unique->slots += (slots - oldslots);
    ddFixLimits(unique);

} /* end of cuddRehash */


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

  Synopsis    [Shrinks a subtable.]

  Description [Shrinks a subtable.]

  SideEffects [None]

  SeeAlso     [cuddRehash]

******************************************************************************/
void
cuddShrinkSubtable(
  DdManager *unique,
  int i)
{
    int j;
    int shift, posn;
    DdNodePtr *nodelist, *oldnodelist;
    DdNode *node, *next;
    DdNode *sentinel = &(unique->sentinel);
    unsigned int slots, oldslots;
    extern void (*MMoutOfMemory)(long);
    void (*saveHandler)(long);

    oldnodelist = unique->subtables[i].nodelist;
    oldslots = unique->subtables[i].slots;
    slots = oldslots >> 1;
    saveHandler = MMoutOfMemory;
    MMoutOfMemory = Cudd_OutOfMem;
    nodelist = ALLOC(DdNodePtr, slots);
    MMoutOfMemory = saveHandler;
    if (nodelist == NULL) {
	return;
    }
    unique->subtables[i].nodelist = nodelist;
    unique->subtables[i].slots = slots;
    unique->subtables[i].shift++;
    unique->subtables[i].maxKeys = slots * DD_MAX_SUBTABLE_DENSITY;
#ifdef DD_VERBOSE
    (void) fprintf(unique->err,
		   "shrunk layer %d (%d keys) from %d to %d slots\n",
		   i, unique->subtables[i].keys, oldslots, slots);
#endif

    for (j = 0; (unsigned) j < slots; j++) {
	nodelist[j] = sentinel;
    }
    shift = unique->subtables[i].shift;
    for (j = 0; (unsigned) j < oldslots; j++) {
	node = oldnodelist[j];
	while (node != sentinel) {
	    DdNode *looking, *T, *E;
	    DdNodePtr *previousP;
	    next = node->next;
	    posn = ddHash(cuddT(node), cuddE(node), shift);
	    previousP = &(nodelist[posn]);
	    looking = *previousP;
	    T = cuddT(node);
	    E = cuddE(node);
	    while (T < cuddT(looking)) {
		previousP = &(looking->next);
		looking = *previousP;
#ifdef DD_UNIQUE_PROFILE
		unique->uniqueLinks++;
#endif
	    }
	    while (T == cuddT(looking) && E < cuddE(looking)) {
		previousP = &(looking->next);
		looking = *previousP;
#ifdef DD_UNIQUE_PROFILE
		unique->uniqueLinks++;
#endif
	    }
	    node->next = *previousP;
	    *previousP = node;
	    node = next;
	}
    }
    FREE(oldnodelist);

    unique->memused += ((long) slots - (long) oldslots) * sizeof(DdNode *);
    unique->slots += slots - oldslots;
    unique->minDead = (unsigned) (unique->gcFrac * (double) unique->slots);
    unique->cacheSlack = (int)
	ddMin(unique->maxCacheHard,DD_MAX_CACHE_TO_SLOTS_RATIO * unique->slots)
	- 2 * (int) unique->cacheSlots;

} /* end of cuddShrinkSubtable */


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

  Synopsis [Inserts n new subtables in a unique table at level.]

  Description [Inserts n new subtables in a unique table at level.
  The number n should be positive, and level should be an existing level.
  Returns 1 if successful; 0 otherwise.]

  SideEffects [None]

  SeeAlso     [cuddDestroySubtables]

******************************************************************************/
int
cuddInsertSubtables(
  DdManager * unique,
  int  n,
  int  level)
{
    DdSubtable *newsubtables;