cuddref.c

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

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

  Synopsis    [Decreases the reference count of node.]

  Description [Decreases the reference count of node. It is primarily
  used in recursive procedures to decrease the ref count of a result
  node before returning it. This accomplishes the goal of removing the
  protection applied by a previous Cudd_Ref.]

  SideEffects [None]

  SeeAlso     [Cudd_RecursiveDeref Cudd_RecursiveDerefZdd Cudd_Ref]

******************************************************************************/
void
Cudd_Deref(
  DdNode * node)
{
    node = Cudd_Regular(node);
    cuddSatDec(node->ref);

} /* end of Cudd_Deref */


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

  Synopsis [Checks the unique table for nodes with non-zero reference
  counts.]

  Description [Checks the unique table for nodes with non-zero
  reference counts. It is normally called before Cudd_Quit to make sure
  that there are no memory leaks due to missing Cudd_RecursiveDeref's.
  Takes into account that reference counts may saturate and that the
  basic constants and the projection functions are referenced by the
  manager.  Returns the number of nodes with non-zero reference count.
  (Except for the cases mentioned above.)]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
int
Cudd_CheckZeroRef(
  DdManager * manager)
{
    int size;
    int i, j;
    int remain;	/* the expected number of remaining references to one */
    DdNodePtr *nodelist;
    DdNode *node;
    DdNode *sentinel = &(manager->sentinel);
    DdSubtable *subtable;
    int count = 0;
    int index;

#ifndef DD_NO_DEATH_ROW
    cuddClearDeathRow(manager);
#endif

    /* First look at the BDD/ADD subtables. */
    remain = 1; /* reference from the manager */
    size = manager->size;
    remain += 2 * size;	/* reference from the BDD projection functions */

    for (i = 0; i < size; i++) {
	subtable = &(manager->subtables[i]);
	nodelist = subtable->nodelist;
	for (j = 0; (unsigned) j < subtable->slots; j++) {
	    node = nodelist[j];
	    while (node != sentinel) {
		if (node->ref != 0 && node->ref != DD_MAXREF) {
		    index = (int) node->index;
		    if (node != manager->vars[index]) {
			count++;
		    } else {
			if (node->ref != 1) {
			    count++;
			}
		    }
		}
		node = node->next;
	    }
	}
    }

    /* Then look at the ZDD subtables. */
    size = manager->sizeZ;
    if (size) /* references from ZDD universe */
	remain += 2;

    for (i = 0; i < size; i++) {
	subtable = &(manager->subtableZ[i]);
	nodelist = subtable->nodelist;
	for (j = 0; (unsigned) j < subtable->slots; j++) {
	    node = nodelist[j];
	    while (node != NULL) {
		if (node->ref != 0 && node->ref != DD_MAXREF) {
		    index = (int) node->index;
		    if (node == manager->univ[manager->permZ[index]]) {
			if (node->ref > 2) {
			    count++;
			}
		    } else {
			count++;
		    }
		}
		node = node->next;
	    }
	}
    }

    /* Now examine the constant table. Plusinfinity, minusinfinity, and
    ** zero are referenced by the manager. One is referenced by the
    ** manager, by the ZDD universe, and by all projection functions.
    ** All other nodes should have no references.
    */
    nodelist = manager->constants.nodelist;
    for (j = 0; (unsigned) j < manager->constants.slots; j++) {
	node = nodelist[j];
	while (node != NULL) {
	    if (node->ref != 0 && node->ref != DD_MAXREF) {
		if (node == manager->one) {
		    if ((int) node->ref != remain) {
			count++;
		    }
		} else if (node == manager->zero ||
		node == manager->plusinfinity ||
		node == manager->minusinfinity) {
		    if (node->ref != 1) {
			count++;
		    }
		} else {
		    count++;
		}
	    }
	    node = node->next;
	}
    }
    return(count);

} /* end of Cudd_CheckZeroRef */


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


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

  Synopsis    [Brings children of a dead node back.]

  Description []

  SideEffects [None]

  SeeAlso     [cuddReclaimZdd]

******************************************************************************/
void
cuddReclaim(
  DdManager * table,
  DdNode * n)
{
    DdNode *N;
    int ord;
    DdNodePtr *stack = table->stack;
    int SP = 1;
    double initialDead = table->dead;

    N = Cudd_Regular(n);

#ifdef DD_DEBUG
    assert(N->ref == 0);
#endif

    do {
	if (N->ref == 0) {
	    N->ref = 1;
	    table->dead--;
	    if (cuddIsConstant(N)) {
		table->constants.dead--;
		N = stack[--SP];
	    } else {
		ord = table->perm[N->index];
		stack[SP++] = Cudd_Regular(cuddE(N));
		table->subtables[ord].dead--;
		N = cuddT(N);
	    }
	} else {
	    cuddSatInc(N->ref);
	    N = stack[--SP];
	}
    } while (SP != 0);

    N = Cudd_Regular(n);
    cuddSatDec(N->ref);
    table->reclaimed += initialDead - table->dead;

} /* end of cuddReclaim */


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

  Synopsis    [Brings children of a dead ZDD node back.]

  Description []

  SideEffects [None]

  SeeAlso     [cuddReclaim]

******************************************************************************/
void
cuddReclaimZdd(
  DdManager * table,
  DdNode * n)
{
    DdNode *N;
    int ord;
    DdNodePtr *stack = table->stack;
    int SP = 1;

    N = n;

#ifdef DD_DEBUG
    assert(N->ref == 0);
#endif

    do {
	cuddSatInc(N->ref);

	if (N->ref == 1) {
	    table->deadZ--;
	    table->reclaimed++;
#ifdef DD_DEBUG
	    assert(!cuddIsConstant(N));
#endif
	    ord = table->permZ[N->index];
	    stack[SP++] = cuddE(N);
	    table->subtableZ[ord].dead--;
	    N = cuddT(N);
	} else {
	    N = stack[--SP];
	}
    } while (SP != 0);

    cuddSatDec(n->ref);

} /* end of cuddReclaimZdd */


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

  Synopsis    [Shrinks the death row.]

  Description [Shrinks the death row by a factor of four.]

  SideEffects [None]

  SeeAlso     [cuddClearDeathRow]

******************************************************************************/
void
cuddShrinkDeathRow(
  DdManager *table)
{
#ifndef DD_NO_DEATH_ROW
    int i;

    if (table->deathRowDepth > 3) {
	for (i = table->deathRowDepth/4; i < table->deathRowDepth; i++) {
	    if (table->deathRow[i] == NULL) break;
	    Cudd_IterDerefBdd(table,table->deathRow[i]);
	    table->deathRow[i] = NULL;
	}
	table->deathRowDepth /= 4;
	table->deadMask = table->deathRowDepth - 2;
	if ((unsigned) table->nextDead > table->deadMask) {
	    table->nextDead = 0;
	}
	table->deathRow = REALLOC(DdNodePtr, table->deathRow,
				   table->deathRowDepth);
    }
#endif

} /* end of cuddShrinkDeathRow */


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

  Synopsis    [Clears the death row.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_DelayedDerefBdd Cudd_IterDerefBdd Cudd_CheckZeroRef
  cuddGarbageCollect]

******************************************************************************/
void
cuddClearDeathRow(
  DdManager *table)
{
#ifndef DD_NO_DEATH_ROW
    int i;

    for (i = 0; i < table->deathRowDepth; i++) {
	if (table->deathRow[i] == NULL) break;
	Cudd_IterDerefBdd(table,table->deathRow[i]);
	table->deathRow[i] = NULL;
    }
#ifdef DD_DEBUG
    for (; i < table->deathRowDepth; i++) {
	assert(table->deathRow[i] == NULL);
    }
#endif
    table->nextDead = 0;
#endif

} /* end of cuddClearDeathRow */


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

  Synopsis    [Checks whether a node is in the death row.]

  Description [Checks whether a node is in the death row. Returns the
  position of the first occurrence if the node is present; -1
  otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_DelayedDerefBdd cuddClearDeathRow]

******************************************************************************/
int
cuddIsInDeathRow(
  DdManager *dd,
  DdNode *f)
{
#ifndef DD_NO_DEATH_ROW
    int i;

    for (i = 0; i < dd->deathRowDepth; i++) {
	if (f == dd->deathRow[i]) {
	    return(i);
	}
    }
#endif

    return(-1);

} /* end of cuddIsInDeathRow */


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

  Synopsis    [Counts how many times a node is in the death row.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_DelayedDerefBdd cuddClearDeathRow cuddIsInDeathRow]

******************************************************************************/
int
cuddTimesInDeathRow(
  DdManager *dd,
  DdNode *f)
{
    int count = 0;
#ifndef DD_NO_DEATH_ROW
    int i;

    for (i = 0; i < dd->deathRowDepth; i++) {
	count += f == dd->deathRow[i];
    }
#endif

    return(count);

} /* end of cuddTimesInDeathRow */

/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/