summaryrefslogtreecommitdiffstats
path: root/src/bdd/cudd/cuddRef.c
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2007-09-30 08:01:00 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2007-09-30 08:01:00 -0700
commite54d9691616b9a0326e2fdb3156bb4eeb8abfcd7 (patch)
treede3ffe87c3e17950351e3b7d97fa18318bd5ea9a /src/bdd/cudd/cuddRef.c
parent7d7e60f2dc84393cd4c5db22d2eaf7b1fb1a79b2 (diff)
downloadabc-e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7.tar.gz
abc-e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7.tar.bz2
abc-e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7.zip
Version abc70930
Diffstat (limited to 'src/bdd/cudd/cuddRef.c')
-rw-r--r--src/bdd/cudd/cuddRef.c781
1 files changed, 0 insertions, 781 deletions
diff --git a/src/bdd/cudd/cuddRef.c b/src/bdd/cudd/cuddRef.c
deleted file mode 100644
index a9241f3d..00000000
--- a/src/bdd/cudd/cuddRef.c
+++ /dev/null
@@ -1,781 +0,0 @@
-/**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_hack.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 */
-
-
-/**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 */
-/*---------------------------------------------------------------------------*/