cuddtable.c

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

	    return(NULL);
	}
	for (j = 0; (unsigned) j < slots; j++) {
	    nodelist[j] = NULL;
	}
	unique->permZ[i] = i;
	unique->invpermZ[i] = i;
    }
    unique->constants.slots = slots;
    unique->constants.shift = shift;
    unique->constants.keys = 0;
    unique->constants.dead = 0;
    unique->constants.maxKeys = slots * DD_MAX_SUBTABLE_DENSITY;
    nodelist = unique->constants.nodelist = ALLOC(DdNodePtr,slots);
    if (nodelist == NULL) {
	unique->errorCode = CUDD_MEMORY_OUT;
	return(NULL);
    }
    for (j = 0; (unsigned) j < slots; j++) {
	nodelist[j] = NULL;
    }

    unique->memoryList = NULL;
    unique->nextFree = NULL;

    unique->memused = sizeof(DdManager) + (unique->maxSize + unique->maxSizeZ)
	* (sizeof(DdSubtable) + 2 * sizeof(int)) + (numVars + 1) *
	slots * sizeof(DdNodePtr) +
	(ddMax(unique->maxSize,unique->maxSizeZ) + 1) * sizeof(DdNodePtr);
#ifndef DD_NO_DEATH_ROW
    unique->memused += unique->deathRowDepth * sizeof(DdNodePtr);
#endif

    /* Initialize fields concerned with automatic dynamic reordering */
    unique->reorderings = 0;
    unique->autoDyn = 0;	/* initially disabled */
    unique->autoDynZ = 0;	/* initially disabled */
    unique->realign = 0;	/* initially disabled */
    unique->realignZ = 0;	/* initially disabled */
    unique->reordered = 0;
    unique->autoMethod = CUDD_REORDER_SIFT;
    unique->autoMethodZ = CUDD_REORDER_SIFT;
    unique->nextDyn = DD_FIRST_REORDER;
    unique->countDead = ~0;
    unique->siftMaxVar = DD_SIFT_MAX_VAR;
    unique->siftMaxSwap = DD_SIFT_MAX_SWAPS;
    unique->tree = NULL;
    unique->treeZ = NULL;
    unique->groupcheck = CUDD_GROUP_CHECK7;
    unique->recomb = DD_DEFAULT_RECOMB;
    unique->symmviolation = 0;
    unique->arcviolation = 0;
    unique->populationSize = 0;
    unique->numberXovers = 0;
    unique->linear = NULL;
    unique->linearSize = 0;

    /* Initialize ZDD universe. */
    unique->univ = (DdNodePtr *)NULL;

    /* Initialize auxiliary fields. */
    unique->localCaches = NULL;
    unique->preGCHook = NULL;
    unique->postGCHook = NULL;
    unique->preReorderingHook = NULL;
    unique->postReorderingHook = NULL;
    unique->out = stdout;
    unique->err = stderr;
    unique->errorCode = CUDD_NO_ERROR;

    /* Initialize statistical counters. */
    unique->maxmemhard = (long) ((~ (unsigned long) 0) >> 1);
    unique->garbageCollections = 0;
    unique->GCTime = 0;
    unique->reordTime = 0;
#ifdef DD_STATS
    unique->nodesDropped = 0;
    unique->nodesFreed = 0;
#endif
    unique->peakLiveNodes = 0;
#ifdef DD_UNIQUE_PROFILE
    unique->uniqueLookUps = 0;
    unique->uniqueLinks = 0;
#endif
#ifdef DD_COUNT
    unique->recursiveCalls = 0;
    unique->swapSteps = 0;
#ifdef DD_STATS
    unique->nextSample = 250000;
#endif
#endif

    return(unique);

} /* end of cuddInitTable */


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

  Synopsis    [Frees the resources associated to a unique table.]

  Description []

  SideEffects [None]

  SeeAlso     [cuddInitTable]

******************************************************************************/
void
cuddFreeTable(
  DdManager * unique)
{
    DdNodePtr *next;
    DdNodePtr *memlist = unique->memoryList;
    int i;

    if (unique->univ != NULL) cuddZddFreeUniv(unique);
    while (memlist != NULL) {
        next = (DdNodePtr *) memlist[0];	/* link to next block */
	FREE(memlist);
	memlist = next;
    }
    unique->nextFree = NULL;
    unique->memoryList = NULL;

    for (i = 0; i < unique->size; i++) {
	FREE(unique->subtables[i].nodelist);
    }
    for (i = 0; i < unique->sizeZ; i++) {
	FREE(unique->subtableZ[i].nodelist);
    }
    FREE(unique->constants.nodelist);
    FREE(unique->subtables);
    FREE(unique->subtableZ);
    FREE(unique->acache);
    FREE(unique->perm);
    FREE(unique->permZ);
    FREE(unique->invperm);
    FREE(unique->invpermZ);
    FREE(unique->vars);
    if (unique->map != NULL) FREE(unique->map);
    FREE(unique->stack);
#ifndef DD_NO_DEATH_ROW
    FREE(unique->deathRow);
#endif
    if (unique->tree != NULL) Mtr_FreeTree(unique->tree);
    if (unique->treeZ != NULL) Mtr_FreeTree(unique->treeZ);
    if (unique->linear != NULL) FREE(unique->linear);
    while (unique->preGCHook != NULL)
	Cudd_RemoveHook(unique,unique->preGCHook->f,CUDD_PRE_GC_HOOK);
    while (unique->postGCHook != NULL)
	Cudd_RemoveHook(unique,unique->postGCHook->f,CUDD_POST_GC_HOOK);
    while (unique->preReorderingHook != NULL)
	Cudd_RemoveHook(unique,unique->preReorderingHook->f,
			CUDD_PRE_REORDERING_HOOK);
    while (unique->postReorderingHook != NULL)
	Cudd_RemoveHook(unique,unique->postReorderingHook->f,
			CUDD_POST_REORDERING_HOOK);
    FREE(unique);

} /* end of cuddFreeTable */


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

  Synopsis    [Performs garbage collection on a unique table.]

  Description [Performs garbage collection on a unique table.
  If clearCache is 0, the cache is not cleared. This should only be
  specified if the cache has been cleared right before calling
  cuddGarbageCollect. (As in the case of dynamic reordering.)
  Returns the total number of deleted nodes.]

  SideEffects [None]

  SeeAlso     [cuddGarbageCollectZdd]

******************************************************************************/
int
cuddGarbageCollect(
  DdManager * unique,
  int  clearCache)
{
    DdHook	*hook;
    DdCache	*cache = unique->cache;
    DdNode	*sentinel = &(unique->sentinel);
    DdNodePtr	*nodelist;
    int		i, j, deleted, totalDeleted;
    DdCache	*c;
    DdNode	*node,*next;
    DdNodePtr	*lastP;
    int		slots;
    long	localTime;
#ifndef DD_UNSORTED_FREE_LIST
    DdNodePtr	tree;
#endif

#ifndef DD_NO_DEATH_ROW
    cuddClearDeathRow(unique);
#endif

    hook = unique->preGCHook;
    while (hook != NULL) {
	int res = (hook->f)(unique,"BDD",NULL);
	if (res == 0) return(0);
	hook = hook->next;
    }

    if (unique->dead == 0) {
	hook = unique->postGCHook;
	while (hook != NULL) {
	    int res = (hook->f)(unique,"BDD",NULL);
	    if (res == 0) return(0);
	    hook = hook->next;
	}
        return(0);
    }

    /* If many nodes are being reclaimed, we want to resize the tables
    ** more aggressively, to reduce the frequency of garbage collection.
    */
    if (clearCache && unique->gcFrac == DD_GC_FRAC_LO &&
	unique->slots <= unique->looseUpTo && unique->stash != NULL) {
	unique->minDead = (unsigned) (DD_GC_FRAC_HI * (double) unique->slots);
#ifdef DD_VERBOSE
	(void) fprintf(unique->err,"GC fraction = %.2f\t", DD_GC_FRAC_HI);
	(void) fprintf(unique->err,"minDead = %d\n", unique->minDead);
#endif
	unique->gcFrac = DD_GC_FRAC_HI;
	return(0);
    }

    localTime = util_cpu_time();

    unique->garbageCollections++;
#ifdef DD_VERBOSE
    (void) fprintf(unique->err,
		   "garbage collecting (%d dead out of %d, min %d)...",
    		   unique->dead, unique->keys, unique->minDead);
#endif

    /* Remove references to garbage collected nodes from the cache. */
    if (clearCache) {
	slots = unique->cacheSlots;
	for (i = 0; i < slots; i++) {
	    c = &cache[i];
	    if (c->data != NULL) {
		if (cuddClean(c->f)->ref == 0 ||
		cuddClean(c->g)->ref == 0 ||
		(((ptruint)c->f & 0x2) && Cudd_Regular(c->h)->ref == 0) ||
		(c->data != DD_NON_CONSTANT &&
		Cudd_Regular(c->data)->ref == 0)) {
		    c->data = NULL;
		    unique->cachedeletions++;
		}
	    }
	}
	cuddLocalCacheClearDead(unique);
    }

    /* Now return dead nodes to free list. Count them for sanity check. */
    totalDeleted = 0;
#ifndef DD_UNSORTED_FREE_LIST
    tree = NULL;
#endif

    for (i = 0; i < unique->size; i++) {
	if (unique->subtables[i].dead == 0) continue;
	nodelist = unique->subtables[i].nodelist;

	deleted = 0;
	slots = unique->subtables[i].slots;
	for (j = 0; j < slots; j++) {
	    lastP = &(nodelist[j]);
	    node = *lastP;
	    while (node != sentinel) {
		next = node->next;
		if (node->ref == 0) {
		    deleted++;
#ifndef DD_UNSORTED_FREE_LIST
#ifdef __osf__
#pragma pointer_size save
#pragma pointer_size short
#endif
		    cuddOrderedInsert(&tree,node);
#ifdef __osf__
#pragma pointer_size restore
#endif
#else
		    cuddDeallocNode(unique,node);
#endif
		} else {
		    *lastP = node;
		    lastP = &(node->next);
		}
		node = next;
	    }
	    *lastP = sentinel;
	}
	if ((unsigned) deleted != unique->subtables[i].dead) {
	    ddReportRefMess(unique, i, "cuddGarbageCollect");
	}
	totalDeleted += deleted;
	unique->subtables[i].keys -= deleted;
	unique->subtables[i].dead = 0;
    }
    if (unique->constants.dead != 0) {
	nodelist = unique->constants.nodelist;
	deleted = 0;
	slots = unique->constants.slots;
	for (j = 0; j < slots; j++) {
	    lastP = &(nodelist[j]);
	    node = *lastP;
	    while (node != NULL) {
		next = node->next;
		if (node->ref == 0) {
		    deleted++;
#ifndef DD_UNSORTED_FREE_LIST
#ifdef __osf__
#pragma pointer_size save
#pragma pointer_size short
#endif
		    cuddOrderedInsert(&tree,node);
#ifdef __osf__
#pragma pointer_size restore
#endif
#else
		    cuddDeallocNode(unique,node);
#endif
		} else {
		    *lastP = node;
		    lastP = &(node->next);
		}	    
		node = next;
	    }
	    *lastP = NULL;
	}
	if ((unsigned) deleted != unique->constants.dead) {
	    ddReportRefMess(unique, CUDD_CONST_INDEX, "cuddGarbageCollect");
	}
	totalDeleted += deleted;
	unique->constants.keys -= deleted;
	unique->constants.dead = 0;
    }
    if ((unsigned) totalDeleted != unique->dead) {
	ddReportRefMess(unique, -1, "cuddGarbageCollect");
    }
    unique->keys -= totalDeleted;
    unique->dead = 0;
#ifdef DD_STATS
    unique->nodesFreed += (double) totalDeleted;
#endif

#ifndef DD_UNSORTED_FREE_LIST
    unique->nextFree = cuddOrderedThread(tree,unique->nextFree);
#endif

    unique->GCTime += util_cpu_time() - localTime;

    hook = unique->postGCHook;
    while (hook != NULL) {
	int res = (hook->f)(unique,"BDD",NULL);
	if (res == 0) return(0);
	hook = hook->next;
    }

#ifdef DD_VERBOSE
    (void) fprintf(unique->err," done\n");
#endif

    return(totalDeleted);

} /* end of cuddGarbageCollect */


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

  Synopsis    [Performs garbage collection on a ZDD unique table.]

  Description [Performs garbage collection on a ZDD unique table.
  If clearCache is 0, the cache is not cleared. This should only be
  specified if the cache has been cleared right before calling
  cuddGarbageCollectZdd. (As in the case of dynamic reordering.)
  Returns the total number of deleted nodes.]

  SideEffects [None]

  SeeAlso     [cuddGarbageCollect]

******************************************************************************/
int
cuddGarbageCollectZdd(
  DdManager * unique,
  int  clearCache)
{
    DdHook	*hook;
    DdCache	*cache = unique->cache;
    DdNodePtr	*nodelist;
    int		i, j, deleted, totalDeleted;
    DdCache	*c;
    DdNode	*node,*next;
    DdNodePtr	*lastP;
    int		slots;
    long	localTime;
#ifndef DD_UNSORTED_FREE_LIST
    DdNodePtr	tree;
#endif

    hook = unique->preGCHook;
    while (hook != NULL) {
	int res = (hook->f)(unique,"ZDD",NULL);
	if (res == 0) return(0);
	hook = hook->next;
    }

    if (unique->deadZ == 0) {
	hook = unique->postGCHook;
	while (hook != NULL) {
	    int res = (hook->f)(unique,"ZDD",NULL);
	    if (res == 0) return(0);
	    hook = hook->next;
	}
        return(0);
    }

    /* If many nodes are being reclaimed, we want to resize the tables
    ** more aggressively, to reduce the frequency of garbage collection.
    */
    if (clearCache && unique->slots <= unique->looseUpTo) {
	unique->minDead = (unsigned) (DD_GC_FRAC_HI * (double) unique->slots);
#ifdef DD_VERBOSE
	if (unique->gcFrac == DD_GC_FRAC_LO) {
	    (void) fprintf(unique->err,"GC fraction = %.2f\t",
			   DD_GC_FRAC_HI);
	    (void) fprintf(unique->err,"minDead = %d\n", unique->minDead);
	}
#endif
	unique->gcFrac = DD_GC_FRAC_HI;
    }

    localTime = util_cpu_time();