cuddtable.c

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

    DdNodePtr *newnodelist;
    DdNodePtr *newvars;
    DdNode *sentinel = &(unique->sentinel);
    int oldsize,newsize;
    int i,j,index,reorderSave;
    unsigned int numSlots = unique->initSlots;
    int *newperm, *newinvperm, *newmap;
    DdNode *one, *zero;

#ifdef DD_DEBUG
    assert(n > 0 && level < unique->size);
#endif

    oldsize = unique->size;
    /* Easy case: there is still room in the current table. */
    if (oldsize + n <= unique->maxSize) {
	/* Shift the tables at and below level. */
	for (i = oldsize - 1; i >= level; i--) {
	    unique->subtables[i+n].slots    = unique->subtables[i].slots;
	    unique->subtables[i+n].shift    = unique->subtables[i].shift;
	    unique->subtables[i+n].keys     = unique->subtables[i].keys;
	    unique->subtables[i+n].maxKeys  = unique->subtables[i].maxKeys;
	    unique->subtables[i+n].dead     = unique->subtables[i].dead;
	    unique->subtables[i+n].nodelist = unique->subtables[i].nodelist;
	    unique->subtables[i+n].bindVar  = unique->subtables[i].bindVar;
	    unique->subtables[i+n].varType  = unique->subtables[i].varType;
	    unique->subtables[i+n].pairIndex  = unique->subtables[i].pairIndex;
	    unique->subtables[i+n].varHandled = unique->subtables[i].varHandled;
	    unique->subtables[i+n].varToBeGrouped =
		unique->subtables[i].varToBeGrouped;

	    index                           = unique->invperm[i];
	    unique->invperm[i+n]            = index;
	    unique->perm[index]            += n;
	}
	/* Create new subtables. */
	for (i = 0; i < n; i++) {
	    unique->subtables[level+i].slots = numSlots;
	    unique->subtables[level+i].shift = sizeof(int) * 8 -
		cuddComputeFloorLog2(numSlots);
	    unique->subtables[level+i].keys = 0;
	    unique->subtables[level+i].maxKeys = numSlots * DD_MAX_SUBTABLE_DENSITY;
	    unique->subtables[level+i].dead = 0;
	    unique->subtables[level+i].bindVar = 0;
	    unique->subtables[level+i].varType = CUDD_VAR_PRIMARY_INPUT;
	    unique->subtables[level+i].pairIndex = 0;
	    unique->subtables[level+i].varHandled = 0;
	    unique->subtables[level+i].varToBeGrouped = CUDD_LAZY_NONE;

	    unique->perm[oldsize+i] = level + i;
	    unique->invperm[level+i] = oldsize + i;
	    newnodelist = unique->subtables[level+i].nodelist =
		ALLOC(DdNodePtr, numSlots);
	    if (newnodelist == NULL) {
		unique->errorCode = CUDD_MEMORY_OUT;
		return(0);
	    }
	    for (j = 0; j < numSlots; j++) {
		newnodelist[j] = sentinel;
	    }
	}
	if (unique->map != NULL) {
	    for (i = 0; i < n; i++) {
		unique->map[oldsize+i] = oldsize + i;
	    }
	}
    } else {
	/* The current table is too small: we need to allocate a new,
	** larger one; move all old subtables, and initialize the new
	** subtables.
	*/
	newsize = oldsize + n + DD_DEFAULT_RESIZE;
#ifdef DD_VERBOSE
	(void) fprintf(unique->err,
		       "Increasing the table size from %d to %d\n",
	    unique->maxSize, newsize);
#endif
	/* Allocate memory for new arrays (except nodelists). */
	newsubtables = ALLOC(DdSubtable,newsize);
	if (newsubtables == NULL) {
	    unique->errorCode = CUDD_MEMORY_OUT;
	    return(0);
	}
	newvars = ALLOC(DdNodePtr,newsize);
	if (newvars == NULL) {
	    unique->errorCode = CUDD_MEMORY_OUT;
	    FREE(newsubtables);
	    return(0);
	}
	newperm = ALLOC(int,newsize);
	if (newperm == NULL) {
	    unique->errorCode = CUDD_MEMORY_OUT;
	    FREE(newsubtables);
	    FREE(newvars);
	    return(0);
	}
	newinvperm = ALLOC(int,newsize);
	if (newinvperm == NULL) {
	    unique->errorCode = CUDD_MEMORY_OUT;
	    FREE(newsubtables);
	    FREE(newvars);
	    FREE(newperm);
	    return(0);
	}
	if (unique->map != NULL) {
	    newmap = ALLOC(int,newsize);
	    if (newmap == NULL) {
		unique->errorCode = CUDD_MEMORY_OUT;
		FREE(newsubtables);
		FREE(newvars);
		FREE(newperm);
		FREE(newinvperm);
		return(0);
	    }
	    unique->memused += (newsize - unique->maxSize) * sizeof(int);
	}
	unique->memused += (newsize - unique->maxSize) * ((numSlots+1) *
	    sizeof(DdNode *) + 2 * sizeof(int) + sizeof(DdSubtable));
	/* Copy levels before insertion points from old tables. */
	for (i = 0; i < level; i++) {
	    newsubtables[i].slots = unique->subtables[i].slots;
	    newsubtables[i].shift = unique->subtables[i].shift;
	    newsubtables[i].keys = unique->subtables[i].keys;
	    newsubtables[i].maxKeys = unique->subtables[i].maxKeys;
	    newsubtables[i].dead = unique->subtables[i].dead;
	    newsubtables[i].nodelist = unique->subtables[i].nodelist;
	    newsubtables[i].bindVar = unique->subtables[i].bindVar;
	    newsubtables[i].varType = unique->subtables[i].varType;
	    newsubtables[i].pairIndex = unique->subtables[i].pairIndex;
	    newsubtables[i].varHandled = unique->subtables[i].varHandled;
	    newsubtables[i].varToBeGrouped = unique->subtables[i].varToBeGrouped;

	    newvars[i] = unique->vars[i];
	    newperm[i] = unique->perm[i];
	    newinvperm[i] = unique->invperm[i];
	}
	/* Finish initializing permutation for new table to old one. */
	for (i = level; i < oldsize; i++) {
	    newperm[i] = unique->perm[i];
	}
	/* Initialize new levels. */
	for (i = level; i < level + n; i++) {
	    newsubtables[i].slots = numSlots;
	    newsubtables[i].shift = sizeof(int) * 8 -
		cuddComputeFloorLog2(numSlots);
	    newsubtables[i].keys = 0;
	    newsubtables[i].maxKeys = numSlots * DD_MAX_SUBTABLE_DENSITY;
	    newsubtables[i].dead = 0;
	    newsubtables[i].bindVar = 0;
	    newsubtables[i].varType = CUDD_VAR_PRIMARY_INPUT;
	    newsubtables[i].pairIndex = 0;
	    newsubtables[i].varHandled = 0;
	    newsubtables[i].varToBeGrouped = CUDD_LAZY_NONE;

	    newperm[oldsize + i - level] = i;
	    newinvperm[i] = oldsize + i - level;
	    newnodelist = newsubtables[i].nodelist = ALLOC(DdNodePtr, numSlots);
	    if (newnodelist == NULL) {
		/* We are going to leak some memory.  We should clean up. */
		unique->errorCode = CUDD_MEMORY_OUT;
		return(0);
	    }
	    for (j = 0; j < numSlots; j++) {
		newnodelist[j] = sentinel;
	    }
	}
	/* Copy the old tables for levels past the insertion point. */
	for (i = level; i < oldsize; i++) {
	    newsubtables[i+n].slots    = unique->subtables[i].slots;
	    newsubtables[i+n].shift    = unique->subtables[i].shift;
	    newsubtables[i+n].keys     = unique->subtables[i].keys;
	    newsubtables[i+n].maxKeys  = unique->subtables[i].maxKeys;
	    newsubtables[i+n].dead     = unique->subtables[i].dead;
	    newsubtables[i+n].nodelist = unique->subtables[i].nodelist;
	    newsubtables[i+n].bindVar  = unique->subtables[i].bindVar;
	    newsubtables[i+n].varType  = unique->subtables[i].varType;
	    newsubtables[i+n].pairIndex  = unique->subtables[i].pairIndex;
	    newsubtables[i+n].varHandled  = unique->subtables[i].varHandled;
	    newsubtables[i+n].varToBeGrouped  =
		unique->subtables[i].varToBeGrouped;

	    newvars[i]                 = unique->vars[i];
	    index                      = unique->invperm[i];
	    newinvperm[i+n]            = index;
	    newperm[index]            += n;
	}
	/* Update the map. */
	if (unique->map != NULL) {
	    for (i = 0; i < oldsize; i++) {
		newmap[i] = unique->map[i];
	    }
	    for (i = oldsize; i < oldsize + n; i++) {
		newmap[i] = i;
	    }
	    FREE(unique->map);
	    unique->map = newmap;
	}
	/* Install the new tables and free the old ones. */
	FREE(unique->subtables);
	unique->subtables = newsubtables;
	unique->maxSize = newsize;
	FREE(unique->vars);
	unique->vars = newvars;
	FREE(unique->perm);
	unique->perm = newperm;
	FREE(unique->invperm);
	unique->invperm = newinvperm;
	/* Update the stack for iterative procedures. */
	if (newsize > unique->maxSizeZ) {
	    FREE(unique->stack);
	    unique->stack = ALLOC(DdNodePtr,newsize + 1);
	    if (unique->stack == NULL) {
		unique->errorCode = CUDD_MEMORY_OUT;
		return(0);
	    }
	    unique->stack[0] = NULL; /* to suppress harmless UMR */
	    unique->memused +=
		(newsize - ddMax(unique->maxSize,unique->maxSizeZ))
		* sizeof(DdNode *);
	}
    }
    /* Update manager parameters to account for the new subtables. */
    unique->slots += n * numSlots;
    ddFixLimits(unique);
    unique->size += n;

    /* Now that the table is in a coherent state, create the new
    ** projection functions. We need to temporarily disable reordering,
    ** because we cannot reorder without projection functions in place.
    **/
    one = unique->one;
    zero = Cudd_Not(one);

    reorderSave = unique->autoDyn;
    unique->autoDyn = 0;
    for (i = oldsize; i < oldsize + n; i++) {
	unique->vars[i] = cuddUniqueInter(unique,i,one,zero);
	if (unique->vars[i] == NULL) {
	    unique->autoDyn = reorderSave;
	    /* Shift everything back so table remains coherent. */
	    for (j = oldsize; j < i; j++) {
		Cudd_IterDerefBdd(unique,unique->vars[j]);
		cuddDeallocNode(unique,unique->vars[j]);
		unique->vars[j] = NULL;
	    }
	    for (j = level; j < oldsize; j++) {
		unique->subtables[j].slots    = unique->subtables[j+n].slots;
		unique->subtables[j].slots    = unique->subtables[j+n].slots;
		unique->subtables[j].shift    = unique->subtables[j+n].shift;
		unique->subtables[j].keys     = unique->subtables[j+n].keys;
		unique->subtables[j].maxKeys  =
		    unique->subtables[j+n].maxKeys;
		unique->subtables[j].dead     = unique->subtables[j+n].dead;
		FREE(unique->subtables[j].nodelist);
		unique->subtables[j].nodelist =
		    unique->subtables[j+n].nodelist;
		unique->subtables[j+n].nodelist = NULL;
		unique->subtables[j].bindVar  =
		    unique->subtables[j+n].bindVar;
		unique->subtables[j].varType  =
		    unique->subtables[j+n].varType;
		unique->subtables[j].pairIndex =
		    unique->subtables[j+n].pairIndex;
		unique->subtables[j].varHandled =
		    unique->subtables[j+n].varHandled;
		unique->subtables[j].varToBeGrouped =
		    unique->subtables[j+n].varToBeGrouped;
		index                         = unique->invperm[j+n];
		unique->invperm[j]            = index;
		unique->perm[index]          -= n;
	    }
	    unique->size = oldsize;
	    unique->slots -= n * numSlots;
	    ddFixLimits(unique);
	    (void) Cudd_DebugCheck(unique);
	    return(0);
	}
	cuddRef(unique->vars[i]);
    }
    if (unique->tree != NULL) {
	unique->tree->size += n;
	unique->tree->index = unique->invperm[0];
	ddPatchTree(unique,unique->tree);
    }
    unique->autoDyn = reorderSave;

    return(1);

} /* end of cuddInsertSubtables */


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

  Synopsis [Destroys the n most recently created subtables in a unique table.]

  Description [Destroys the n most recently created subtables in a unique
  table.  n should be positive. The subtables should not contain any live
  nodes, except the (isolated) projection function. The projection
  functions are freed.  Returns 1 if successful; 0 otherwise.]

  SideEffects [The variable map used for fast variable substitution is
  destroyed if it exists. In this case the cache is also cleared.]

  SeeAlso     [cuddInsertSubtables Cudd_SetVarMap]

******************************************************************************/
int
cuddDestroySubtables(
  DdManager * unique,
  int  n)
{
    DdSubtable *subtables;
    DdNodePtr *nodelist;
    DdNodePtr *vars;
    int firstIndex, lastIndex;
    int index, level, newlevel;
    int lowestLevel;
    int shift;
    int found;

    /* Sanity check and set up. */
    if (n <= 0) return(0);
    if (n > unique->size) n = unique->size;

    subtables = unique->subtables;
    vars = unique->vars;
    firstIndex = unique->size - n;
    lastIndex  = unique->size;

    /* Check for nodes labeled by the variables being destroyed
    ** that may still be in use.  It is allowed to destroy a variable
    ** only if there are no such nodes. Also, find the lowest level
    ** among the variables being destroyed. This will make further
    ** processing more efficient.
    */
    lowestLevel = unique->size;
    for (index = firstIndex; index < lastIndex; index++) {
	level = unique->perm[index];
	if (level < lowestLevel) lowestLevel = level;
	nodelist = subtables[level].nodelist;
	if (subtables[level].keys - subtables[level].dead != 1) return(0);
	/* The projection function should be isolated. If the ref count
	** is 1, everything is OK. If the ref count is saturated, then
	** we need to make sure that there are no nodes pointing to it.
	** As for the external references, we assume the application is
	** responsible for them.
	*/
	if (vars[index]->ref != 1) {
	    if (vars[index]->ref != DD_MAXREF) return(0);
	    found = cuddFindParent(unique,vars[index]);
	    if (found) {
		return(0);
	    } else {
		vars[index]->ref = 1;
	    }
	}
	Cudd_RecursiveDeref(unique,vars[index]);
    }

    /* Collect garbage, because we cannot afford having dead nodes pointing
    ** to the dead nodes in the subtables being destroyed.
    */
    (void) cuddGarbageCollect(unique,1);

    /* Here we know we can destroy our subtables. */
    for (index = firstIndex; index < lastIndex; index++) {
	level = unique->perm[index];
	nodelist = subtables[level].nodelist;
#ifdef DD_DEBUG
	assert(subtables[level].keys == 0);
#endif
	FREE(nodelist);
	unique->memused -= sizeof(DdNodePtr) * subtables[level].slots;
	unique->slots -= subtables[level].slots;
	unique->dead -= subtables[level].dead;
    }

    /* Here all subtables to be destroyed have their keys field == 0 and
    ** their hash tables have been freed.
    ** We now scan the subtables from level lowestLevel + 1 to level size - 1,
    ** shifting the subtables as required. We keep a running count of
    ** how many subtables have been moved, so that we know by how many
    ** positions each subtable should be shifted.
    */
    shift = 1;
    for (level = lowestLevel + 1; level < unique->size; level++) {
	if (subtables[level].keys == 0) {
	    shift++;
	    continue;
	}
	newlevel = level - shift;
	subtables[newlevel].slots = subtables[level].slots;
	subtables[newlevel].shift = subtables[level].shift;
	subtables[newlevel].keys = subtables[level].keys;
	subtables[newlevel].maxKeys = subtables[level].maxKeys;
	subtables[newlevel].dead = subtables[level].dead;
	subtables[newlevel].nodelist = subtables[level].nodelist;
	index = unique->invperm[level];
	unique->perm[index] = newlevel;
	unique->invperm[newlevel]  = index;
	subtables[newlevel].bindVar = subtables[level].bindVar;
	subtables[newlevel].varType = subtables[level].varType;
	subtables[newlevel].pairIndex = subtables[level].pairIndex;
	subtables[newlevel].varHandled = subtables[level].varHandled;
	subtables[newlevel].varToBeGrouped = subtables[level].varToBeGrouped;
    }
    /* Destroy the map. If a surviving variable is
    ** mapped to a dying variable, and the map were used again,
    ** an out-of-bounds access to unique->vars would result. */
    if (unique->map != NULL) {
	cuddCacheFlush(unique);
	FREE(unique->map);
	unique->map = NULL;
    }

    unique->minDead = (unsigned) (unique->gcFrac * (double) unique->slots);
    unique->size -= n;

    return(1);

} /* end of cuddDestroySubtables */


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

  Synopsis [Increases the number of ZDD subtables in a unique table so
  that it meets or exceeds index.]

  Description [Increases the number of ZDD subtables in a unique table so
  that it meets or exceeds index.  When new ZDD variables are created, it
  is possible to preserve the functions unchanged, or it is possible to
  preserve the covers unchanged, but not both. cuddResizeTableZdd preserves
  the covers.  Returns 1 if successful; 0 otherwise.]

  SideEffects [None]

  SeeAlso     [ddResizeTable]

******************************************************************************/
int
cuddResizeTableZd