cuddref.c

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

/**CFile***********************************************************************

  FileName    [cuddRef.c]

  PackageName [cudd]

  Synopsis    [Functions that manipulate the reference counts.]

  Description [External procedures included in this module:
		    <ul>
		    <li> Cudd_Ref()
		    <li> Cudd_RecursiveDeref()
		    <li> Cudd_IterDerefBdd()
		    <li> Cudd_DelayedDerefBdd()
		    <li> Cudd_RecursiveDerefZdd()
		    <li> Cudd_Deref()
		    <li> Cudd_CheckZeroRef()
		    </ul>
	       Internal procedures included in this module:
		    <ul>
		    <li> cuddReclaim()
		    <li> cuddReclaimZdd()
		    <li> cuddClearDeathRow()
		    <li> cuddShrinkDeathRow()
		    <li> cuddIsInDeathRow()
		    <li> cuddTimesInDeathRow()
		    </ul>
	      ]

  SeeAlso     []

  Author      [Fabio Somenzi]

  Copyright [ This file was created at the University of Colorado at
  Boulder.  The University of Colorado at Boulder makes no warranty
  about the suitability of this software for any purpose.  It is
  presented on an AS IS basis.]

******************************************************************************/

#include    "util.h"
#include    "cuddInt.h"

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Stucture declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

#ifndef lint
static char rcsid[] DD_UNUSED = "$Id: cuddRef.c,v 1.1.1.1 2003/02/24 22:23:53 wjiang Exp $";
#endif

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/


/**AutomaticStart*************************************************************/

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

/**AutomaticEnd***************************************************************/


/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/

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

  Synopsis [Increases the reference count of a node, if it is not
  saturated.]

  Description []

  SideEffects [None]

  SeeAlso     [Cudd_RecursiveDeref Cudd_Deref]

******************************************************************************/
void
Cudd_Ref(
  DdNode * n)
{

    n = Cudd_Regular(n);

    cuddSatInc(n->ref);

} /* end of Cudd_Ref */


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

  Synopsis    [Decreases the reference count of node n.]

  Description [Decreases the reference count of node n. If n dies,
  recursively decreases the reference counts of its children.  It is
  used to dispose of a DD that is no longer needed.]

  SideEffects [None]

  SeeAlso     [Cudd_Deref Cudd_Ref Cudd_RecursiveDerefZdd]

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

    unsigned int live = table->keys - table->dead;
    if (live > table->peakLiveNodes) {
	table->peakLiveNodes = live;
    }

    N = Cudd_Regular(n);

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

	if (N->ref == 1) {
	    N->ref = 0;
	    table->dead++;
#ifdef DD_STATS
	    table->nodesDropped++;
#endif
	    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 {
	    cuddSatDec(N->ref);
	    N = stack[--SP];
	}
    } while (SP != 0);

} /* end of Cudd_RecursiveDeref */


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

  Synopsis    [Decreases the reference count of BDD node n.]

  Description [Decreases the reference count of node n. If n dies,
  recursively decreases the reference counts of its children.  It is
  used to dispose of a BDD that is no longer needed. It is more
  efficient than Cudd_RecursiveDeref, but it cannot be used on
  ADDs. The greater efficiency comes from being able to assume that no
  constant node will ever die as a result of a call to this
  procedure.]

  SideEffects [None]

  SeeAlso     [Cudd_RecursiveDeref Cudd_DelayedDerefBdd]

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

    unsigned int live = table->keys - table->dead;
    if (live > table->peakLiveNodes) {
	table->peakLiveNodes = live;
    }

    N = Cudd_Regular(n);

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

	if (N->ref == 1) {
	    N->ref = 0;
	    table->dead++;
#ifdef DD_STATS
	    table->nodesDropped++;
#endif
	    ord = table->perm[N->index];
	    stack[SP++] = Cudd_Regular(cuddE(N));
	    table->subtables[ord].dead++;
	    N = cuddT(N);
	} else {
	    cuddSatDec(N->ref);
	    N = stack[--SP];
	}
    } while (SP != 0);

} /* end of Cudd_IterDerefBdd */


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

  Synopsis    [Decreases the reference count of BDD node n.]

  Description [Enqueues node n for later dereferencing. If the queue
  is full decreases the reference count of the oldest node N to make
  room for n. If N dies, recursively decreases the reference counts of
  its children.  It is used to dispose of a BDD that is currently not
  needed, but may be useful again in the near future. The dereferencing
  proper is done as in Cudd_IterDerefBdd.]

  SideEffects [None]

  SeeAlso     [Cudd_RecursiveDeref Cudd_IterDerefBdd]

******************************************************************************/
void
Cudd_DelayedDerefBdd(
  DdManager * table,
  DdNode * n)
{
    DdNode *N;
    int ord;
    DdNodePtr *stack;
    int SP;

    unsigned int live = table->keys - table->dead;
    if (live > table->peakLiveNodes) {
	table->peakLiveNodes = live;
    }

    n = Cudd_Regular(n);
#ifdef DD_DEBUG
    assert(n->ref != 0);
#endif

#ifdef DD_NO_DEATH_ROW
    N = n;
#else
    if (cuddIsConstant(n) || n->ref > 1) {
#ifdef DD_DEBUG
	assert(n->ref != 1 && (!cuddIsConstant(n) || n == DD_ONE(table)));
#endif
	cuddSatDec(n->ref);
	return;
    }

    N = table->deathRow[table->nextDead];

    if (N != NULL) {
#endif
#ifdef DD_DEBUG
	assert(!Cudd_IsComplement(N));
#endif
	stack = table->stack;
	SP = 1;
	do {
#ifdef DD_DEBUG
	    assert(N->ref != 0);
#endif
	    if (N->ref == 1) {
		N->ref = 0;
		table->dead++;
#ifdef DD_STATS
		table->nodesDropped++;
#endif
		ord = table->perm[N->index];
		stack[SP++] = Cudd_Regular(cuddE(N));
		table->subtables[ord].dead++;
		N = cuddT(N);
	    } else {
		cuddSatDec(N->ref);
		N = stack[--SP];
	    }
	} while (SP != 0);
#ifndef DD_NO_DEATH_ROW
    }
    table->deathRow[table->nextDead] = n;

    /* Udate insertion point. */
    table->nextDead++;
    table->nextDead &= table->deadMask;
#if 0
    if (table->nextDead == table->deathRowDepth) {
	if (table->deathRowDepth < table->looseUpTo / 2) {
	    extern void (*MMoutOfMemory)(long);
	    void (*saveHandler)(long) = MMoutOfMemory;
	    DdNodePtr *newRow;
	    MMoutOfMemory = Cudd_OutOfMem;
	    newRow = REALLOC(DdNodePtr,table->deathRow,2*table->deathRowDepth);
	    MMoutOfMemory = saveHandler;
	    if (newRow == NULL) {
		table->nextDead = 0;
	    } else {
		int i;
		table->memused += table->deathRowDepth;
		i = table->deathRowDepth;
		table->deathRowDepth <<= 1;
		for (; i < table->deathRowDepth; i++) {
		    newRow[i] = NULL;
		}
		table->deadMask = table->deathRowDepth - 1;
		table->deathRow = newRow;
	    }
	} else {
	    table->nextDead = 0;
	}
    }
#endif
#endif

} /* end of Cudd_DelayedDerefBdd */


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

  Synopsis    [Decreases the reference count of ZDD node n.]

  Description [Decreases the reference count of ZDD node n. If n dies,
  recursively decreases the reference counts of its children.  It is
  used to dispose of a ZDD that is no longer needed.]

  SideEffects [None]

  SeeAlso     [Cudd_Deref Cudd_Ref Cudd_RecursiveDeref]

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

    N = n;

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

	cuddSatDec(N->ref);
    
	if (N->ref == 0) {
	    table->deadZ++;
#ifdef DD_STATS
	    table->nodesDropped++;
#endif
#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);

} /* end of Cudd_RecursiveDerefZdd */