cuddtable.c

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

    unique->garbageCollections++;
#ifdef DD_VERBOSE
    (void) fprintf(unique->err,"garbage collecting (%d dead out of %d)...",
    		   unique->deadZ,unique->keysZ);
#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++;
		}
	    }
	}
    }

    /* 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->sizeZ; i++) {
	if (unique->subtableZ[i].dead == 0) continue;
	nodelist = unique->subtableZ[i].nodelist;

	deleted = 0;
	slots = unique->subtableZ[i].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->subtableZ[i].dead) {
	    ddReportRefMess(unique, i, "cuddGarbageCollectZdd");
	}
	totalDeleted += deleted;
	unique->subtableZ[i].keys -= deleted;
	unique->subtableZ[i].dead = 0;
    }

    /* No need to examine the constant table for ZDDs.
    ** If we did we should be careful not to count whatever dead
    ** nodes we found there among the dead ZDD nodes. */
    if ((unsigned) totalDeleted != unique->deadZ) {
	ddReportRefMess(unique, -1, "cuddGarbageCollectZdd");
    }
    unique->keysZ -= totalDeleted;
    unique->deadZ = 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,"ZDD",NULL);
	if (res == 0) return(0);
	hook = hook->next;
    }

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

    return(totalDeleted);

} /* end of cuddGarbageCollectZdd */


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

  Synopsis [Wrapper for cuddUniqueInterZdd.]

  Description [Wrapper for cuddUniqueInterZdd, which applies the ZDD
  reduction rule. Returns a pointer to the result node under normal
  conditions; NULL if reordering occurred or memory was exhausted.]

  SideEffects [None]

  SeeAlso     [cuddUniqueInterZdd]

******************************************************************************/
DdNode *
cuddZddGetNode(
  DdManager * zdd,
  int  id,
  DdNode * T,
  DdNode * E)
{
    DdNode	*node;

    if (T == DD_ZERO(zdd))
	return(E);
    node = cuddUniqueInterZdd(zdd, id, T, E);
    return(node);

} /* end of cuddZddGetNode */


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

  Synopsis [Wrapper for cuddUniqueInterZdd that is independent of variable
  ordering.]

  Description [Wrapper for cuddUniqueInterZdd that is independent of
  variable ordering (IVO). This function does not require parameter
  index to precede the indices of the top nodes of g and h in the
  variable order.  Returns a pointer to the result node under normal
  conditions; NULL if reordering occurred or memory was exhausted.]

  SideEffects [None]

  SeeAlso     [cuddZddGetNode cuddZddIsop]

******************************************************************************/
DdNode *
cuddZddGetNodeIVO(
  DdManager * dd,
  int  index,
  DdNode * g,
  DdNode * h)
{
    DdNode	*f, *r, *t;
    DdNode	*zdd_one = DD_ONE(dd);
    DdNode	*zdd_zero = DD_ZERO(dd);

    f = cuddUniqueInterZdd(dd, index, zdd_one, zdd_zero);
    if (f == NULL) {
	return(NULL);
    }
    cuddRef(f);
    t = cuddZddProduct(dd, f, g);
    if (t == NULL) {
	Cudd_RecursiveDerefZdd(dd, f);
	return(NULL);
    }
    cuddRef(t);
    Cudd_RecursiveDerefZdd(dd, f);
    r = cuddZddUnion(dd, t, h);
    if (r == NULL) {
	Cudd_RecursiveDerefZdd(dd, t);
	return(NULL);
    }
    cuddRef(r);
    Cudd_RecursiveDerefZdd(dd, t);

    cuddDeref(r);
    return(r);

} /* end of cuddZddGetNodeIVO */


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

  Synopsis    [Checks the unique table for the existence of an internal node.]

  Description [Checks the unique table for the existence of an internal
  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.  For a newly
  created node, increments the reference counts of what T and E point
  to.  Returns a pointer to the new node if successful; NULL if memory
  is exhausted or if reordering took place.]

  SideEffects [None]

  SeeAlso     [cuddUniqueInterZdd]

******************************************************************************/
DdNode *
cuddUniqueInter(
  DdManager * unique,
  int  index,
  DdNode * T,
  DdNode * E)
{
    int pos;
    unsigned int level;
    int retval;
    DdNodePtr *nodelist;
    DdNode *looking;
    DdNodePtr *previousP;
    DdSubtable *subtable;
    int gcNumber;

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

    if (index >= unique->size) {
	if (!ddResizeTable(unique,index)) return(NULL);
    }

    level = unique->perm[index];
    subtable = &(unique->subtables[level]);

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

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

    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
    }
    if (T == cuddT(looking) && E == cuddE(looking)) {
	if (looking->ref == 0) {
	    cuddReclaim(unique,looking);
	}
	return(looking);
    }

    /* countDead is 0 if deads should be counted and ~0 if they should not. */
    if (unique->autoDyn &&
    unique->keys - (unique->dead & 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_ReduceHeap(unique,unique->autoMethod,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);
    }

    if (subtable->keys > subtable->maxKeys) {
        if (unique->gcEnabled &&
	    ((unique->dead > unique->minDead) ||
	    ((unique->dead > unique->minDead / 2) &&
	    (subtable->dead > subtable->keys * 0.95)))) { /* too many dead */
	    (void) cuddGarbageCollect(unique,1);
	} else {
	    cuddRehash(unique,(int)level);
	}
	/* Update pointer to insertion point. In the case of rehashing,
	** the slot may have changed. In the case of garbage collection,
	** the predecessor may have been dead. */
	pos = ddHash(T, E, subtable->shift);
	nodelist = subtable->nodelist;
	previousP = &(nodelist[pos]);
	looking = *previousP;

	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
	}
    }

    gcNumber = unique->garbageCollections;
    looking = cuddAllocNode(unique);
    if (looking == NULL) {
	return(NULL);
    }
    unique->keys++;
    subtable->keys++;

    if (gcNumber != unique->garbageCollections) {
	DdNode *looking2;
	pos = ddHash(T, E, subtable->shift);
	nodelist = subtable->nodelist;
	previousP = &(nodelist[pos]);
	looking2 = *previousP;

	while (T < cuddT(looking2)) {
	    previousP = &(looking2->next);
	    looking2 = *previousP;
#ifdef DD_UNIQUE_PROFILE
	    unique->uniqueLinks++;
#endif
	}
	while (T == cuddT(looking2) && E < cuddE(looking2)) {
	    previousP = &(looking2->next);
	    looking2 = *previousP;
#ifdef DD_UNIQUE_PROFILE
	    unique->uniqueLinks++;
#endif
	}
    }
    looking->ref = 0;
    looking->index = index;
    cuddT(looking) = T;
    cuddE(looking) = E;
    looking->next = *previousP;
    *previousP = looking;
    cuddSatInc(T->ref);		/* we know T is a regular pointer */
    cuddRef(E);

#ifdef DD_DEBUG
    cuddCheckCollisionOrdering(unique,level,pos);
#endif

    return(looking);

} /* end of cuddUniqueInter */


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

  Synopsis [Wrapper for cuddUniqueInter that is independent of variable
  ordering.]

  Description [Wrapper for cuddUniqueInter that is independent of
  variable ordering (IVO). This function does not require parameter
  index to precede the indices of the top nodes of T and E in the
  variable order.  Returns a pointer to the result node under normal
  conditions; NULL if reordering occurred or memory was exhausted.]

  SideEffects [None]

  SeeAlso     [cuddUniqueInter Cudd_MakeBddFromZddCover]

******************************************************************************/
DdNode *
cuddUniqueInterIVO(
  DdManager * unique,
  int  index,
  DdNode * T,
  DdNode * E)
{
    DdNode *result;
    DdNode *v;

    v = cuddUniqueInter(unique, index, DD_ONE(unique),
			Cudd_Not(DD_ONE(unique)));
    if (v == NULL)
	return(NULL);
    cuddRef(v);
    result = cuddBddIteRecur(unique, v, T, E);
    Cudd_RecursiveDeref(unique, v);
    return(result);
}


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

  Synopsis    [Checks the unique table for the existence of an internal
  ZDD node.]

  Description [Checks the unique table for the existence of an internal
  ZDD 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.  For a newly
  created node, increments the reference counts of what T and E point
  to.  Returns a pointer to the new node if successful; NULL if memory
  is exhausted or if reordering took place.]

  SideEffects [None]

  SeeAlso     [cuddUniqueInter]

******************************************************************************/
DdNode *
cuddUniqueInterZdd(
  DdManager * unique,
  int  index,
  DdNode * T,
  DdNode * E)
{
    int pos;
    unsigned int level;
    int retval;
    DdNodePtr *nodelist;
    DdNode *looking;
    DdSubtable *subtable;

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

    if (index >= unique->sizeZ) {
	if (!cuddResizeTableZdd(unique,index)) return(NULL);
    }