src/cuBdd/cuddRef.c File Reference

#include "util.h"
#include "cuddInt.h"
Include dependency graph for cuddRef.c:

Go to the source code of this file.

Functions

void Cudd_Ref (DdNode *n)
void Cudd_RecursiveDeref (DdManager *table, DdNode *n)
void Cudd_IterDerefBdd (DdManager *table, DdNode *n)
void Cudd_DelayedDerefBdd (DdManager *table, DdNode *n)
void Cudd_RecursiveDerefZdd (DdManager *table, DdNode *n)
void Cudd_Deref (DdNode *node)
int Cudd_CheckZeroRef (DdManager *manager)
void cuddReclaim (DdManager *table, DdNode *n)
void cuddReclaimZdd (DdManager *table, DdNode *n)
void cuddShrinkDeathRow (DdManager *table)
void cuddClearDeathRow (DdManager *table)
int cuddIsInDeathRow (DdManager *dd, DdNode *f)
int cuddTimesInDeathRow (DdManager *dd, DdNode *f)

Variables

static char rcsid[] DD_UNUSED = "$Id: cuddRef.c,v 1.28 2004/08/13 18:04:50 fabio Exp $"

Function Documentation

int Cudd_CheckZeroRef ( DdManager *  manager  ) 

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 []

Definition at line 462 of file cuddRef.c.

00464 {
00465     int size;
00466     int i, j;
00467     int remain; /* the expected number of remaining references to one */
00468     DdNodePtr *nodelist;
00469     DdNode *node;
00470     DdNode *sentinel = &(manager->sentinel);
00471     DdSubtable *subtable;
00472     int count = 0;
00473     int index;
00474 
00475 #ifndef DD_NO_DEATH_ROW
00476     cuddClearDeathRow(manager);
00477 #endif
00478 
00479     /* First look at the BDD/ADD subtables. */
00480     remain = 1; /* reference from the manager */
00481     size = manager->size;
00482     remain += 2 * size; /* reference from the BDD projection functions */
00483 
00484     for (i = 0; i < size; i++) {
00485         subtable = &(manager->subtables[i]);
00486         nodelist = subtable->nodelist;
00487         for (j = 0; (unsigned) j < subtable->slots; j++) {
00488             node = nodelist[j];
00489             while (node != sentinel) {
00490                 if (node->ref != 0 && node->ref != DD_MAXREF) {
00491                     index = (int) node->index;
00492                     if (node != manager->vars[index]) {
00493                         count++;
00494                     } else {
00495                         if (node->ref != 1) {
00496                             count++;
00497                         }
00498                     }
00499                 }
00500                 node = node->next;
00501             }
00502         }
00503     }
00504 
00505     /* Then look at the ZDD subtables. */
00506     size = manager->sizeZ;
00507     if (size) /* references from ZDD universe */
00508         remain += 2;
00509 
00510     for (i = 0; i < size; i++) {
00511         subtable = &(manager->subtableZ[i]);
00512         nodelist = subtable->nodelist;
00513         for (j = 0; (unsigned) j < subtable->slots; j++) {
00514             node = nodelist[j];
00515             while (node != NULL) {
00516                 if (node->ref != 0 && node->ref != DD_MAXREF) {
00517                     index = (int) node->index;
00518                     if (node == manager->univ[manager->permZ[index]]) {
00519                         if (node->ref > 2) {
00520                             count++;
00521                         }
00522                     } else {
00523                         count++;
00524                     }
00525                 }
00526                 node = node->next;
00527             }
00528         }
00529     }
00530 
00531     /* Now examine the constant table. Plusinfinity, minusinfinity, and
00532     ** zero are referenced by the manager. One is referenced by the
00533     ** manager, by the ZDD universe, and by all projection functions.
00534     ** All other nodes should have no references.
00535     */
00536     nodelist = manager->constants.nodelist;
00537     for (j = 0; (unsigned) j < manager->constants.slots; j++) {
00538         node = nodelist[j];
00539         while (node != NULL) {
00540             if (node->ref != 0 && node->ref != DD_MAXREF) {
00541                 if (node == manager->one) {
00542                     if ((int) node->ref != remain) {
00543                         count++;
00544                     }
00545                 } else if (node == manager->zero ||
00546                 node == manager->plusinfinity ||
00547                 node == manager->minusinfinity) {
00548                     if (node->ref != 1) {
00549                         count++;
00550                     }
00551                 } else {
00552                     count++;
00553                 }
00554             }
00555             node = node->next;
00556         }
00557     }
00558     return(count);
00559 
00560 } /* end of Cudd_CheckZeroRef */

void Cudd_DelayedDerefBdd ( DdManager *  table,
DdNode *  n 
)

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]

Definition at line 270 of file cuddRef.c.

00273 {
00274     DdNode *N;
00275     int ord;
00276     DdNodePtr *stack;
00277     int SP;
00278 
00279     unsigned int live = table->keys - table->dead;
00280     if (live > table->peakLiveNodes) {
00281         table->peakLiveNodes = live;
00282     }
00283 
00284     n = Cudd_Regular(n);
00285 #ifdef DD_DEBUG
00286     assert(n->ref != 0);
00287 #endif
00288 
00289 #ifdef DD_NO_DEATH_ROW
00290     N = n;
00291 #else
00292     if (cuddIsConstant(n) || n->ref > 1) {
00293 #ifdef DD_DEBUG
00294         assert(n->ref != 1 && (!cuddIsConstant(n) || n == DD_ONE(table)));
00295 #endif
00296         cuddSatDec(n->ref);
00297         return;
00298     }
00299 
00300     N = table->deathRow[table->nextDead];
00301 
00302     if (N != NULL) {
00303 #endif
00304 #ifdef DD_DEBUG
00305         assert(!Cudd_IsComplement(N));
00306 #endif
00307         stack = table->stack;
00308         SP = 1;
00309         do {
00310 #ifdef DD_DEBUG
00311             assert(N->ref != 0);
00312 #endif
00313             if (N->ref == 1) {
00314                 N->ref = 0;
00315                 table->dead++;
00316 #ifdef DD_STATS
00317                 table->nodesDropped++;
00318 #endif
00319                 ord = table->perm[N->index];
00320                 stack[SP++] = Cudd_Regular(cuddE(N));
00321                 table->subtables[ord].dead++;
00322                 N = cuddT(N);
00323             } else {
00324                 cuddSatDec(N->ref);
00325                 N = stack[--SP];
00326             }
00327         } while (SP != 0);
00328 #ifndef DD_NO_DEATH_ROW
00329     }
00330     table->deathRow[table->nextDead] = n;
00331 
00332     /* Udate insertion point. */
00333     table->nextDead++;
00334     table->nextDead &= table->deadMask;
00335 #if 0
00336     if (table->nextDead == table->deathRowDepth) {
00337         if (table->deathRowDepth < table->looseUpTo / 2) {
00338             extern void (*MMoutOfMemory)(long);
00339             void (*saveHandler)(long) = MMoutOfMemory;
00340             DdNodePtr *newRow;
00341             MMoutOfMemory = Cudd_OutOfMem;
00342             newRow = REALLOC(DdNodePtr,table->deathRow,2*table->deathRowDepth);
00343             MMoutOfMemory = saveHandler;
00344             if (newRow == NULL) {
00345                 table->nextDead = 0;
00346             } else {
00347                 int i;
00348                 table->memused += table->deathRowDepth;
00349                 i = table->deathRowDepth;
00350                 table->deathRowDepth <<= 1;
00351                 for (; i < table->deathRowDepth; i++) {
00352                     newRow[i] = NULL;
00353                 }
00354                 table->deadMask = table->deathRowDepth - 1;
00355                 table->deathRow = newRow;
00356             }
00357         } else {
00358             table->nextDead = 0;
00359         }
00360     }
00361 #endif
00362 #endif
00363 
00364 } /* end of Cudd_DelayedDerefBdd */

void Cudd_Deref ( DdNode *  node  ) 

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]

Definition at line 434 of file cuddRef.c.

00436 {
00437     node = Cudd_Regular(node);
00438     cuddSatDec(node->ref);
00439 
00440 } /* end of Cudd_Deref */

void Cudd_IterDerefBdd ( DdManager *  table,
DdNode *  n 
)

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]

Definition at line 213 of file cuddRef.c.

00216 {
00217     DdNode *N;
00218     int ord;
00219     DdNodePtr *stack = table->stack;
00220     int SP = 1;
00221 
00222     unsigned int live = table->keys - table->dead;
00223     if (live > table->peakLiveNodes) {
00224         table->peakLiveNodes = live;
00225     }
00226 
00227     N = Cudd_Regular(n);
00228 
00229     do {
00230 #ifdef DD_DEBUG
00231         assert(N->ref != 0);
00232 #endif
00233 
00234         if (N->ref == 1) {
00235             N->ref = 0;
00236             table->dead++;
00237 #ifdef DD_STATS
00238             table->nodesDropped++;
00239 #endif
00240             ord = table->perm[N->index];
00241             stack[SP++] = Cudd_Regular(cuddE(N));
00242             table->subtables[ord].dead++;
00243             N = cuddT(N);
00244         } else {
00245             cuddSatDec(N->ref);
00246             N = stack[--SP];
00247         }
00248     } while (SP != 0);
00249 
00250 } /* end of Cudd_IterDerefBdd */

void Cudd_RecursiveDeref ( DdManager *  table,
DdNode *  n 
)

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]

Definition at line 150 of file cuddRef.c.

00153 {
00154     DdNode *N;
00155     int ord;
00156     DdNodePtr *stack = table->stack;
00157     int SP = 1;
00158 
00159     unsigned int live = table->keys - table->dead;
00160     if (live > table->peakLiveNodes) {
00161         table->peakLiveNodes = live;
00162     }
00163 
00164     N = Cudd_Regular(n);
00165 
00166     do {
00167 #ifdef DD_DEBUG
00168         assert(N->ref != 0);
00169 #endif
00170 
00171         if (N->ref == 1) {
00172             N->ref = 0;
00173             table->dead++;
00174 #ifdef DD_STATS
00175             table->nodesDropped++;
00176 #endif
00177             if (cuddIsConstant(N)) {
00178                 table->constants.dead++;
00179                 N = stack[--SP];
00180             } else {
00181                 ord = table->perm[N->index];
00182                 stack[SP++] = Cudd_Regular(cuddE(N));
00183                 table->subtables[ord].dead++;
00184                 N = cuddT(N);
00185             }
00186         } else {
00187             cuddSatDec(N->ref);
00188             N = stack[--SP];
00189         }
00190     } while (SP != 0);
00191 
00192 } /* end of Cudd_RecursiveDeref */

void Cudd_RecursiveDerefZdd ( DdManager *  table,
DdNode *  n 
)

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]

Definition at line 381 of file cuddRef.c.

00384 {
00385     DdNode *N;
00386     int ord;
00387     DdNodePtr *stack = table->stack;
00388     int SP = 1;
00389 
00390     N = n;
00391 
00392     do {
00393 #ifdef DD_DEBUG
00394         assert(N->ref != 0);
00395 #endif
00396 
00397         cuddSatDec(N->ref);
00398     
00399         if (N->ref == 0) {
00400             table->deadZ++;
00401 #ifdef DD_STATS
00402             table->nodesDropped++;
00403 #endif
00404 #ifdef DD_DEBUG
00405             assert(!cuddIsConstant(N));
00406 #endif
00407             ord = table->permZ[N->index];
00408             stack[SP++] = cuddE(N);
00409             table->subtableZ[ord].dead++;
00410             N = cuddT(N);
00411         } else {
00412             N = stack[--SP];
00413         }
00414     } while (SP != 0);
00415 
00416 } /* end of Cudd_RecursiveDerefZdd */

void Cudd_Ref ( DdNode *  n  ) 

AutomaticStart AutomaticEnd Function********************************************************************

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

Description []

SideEffects [None]

SeeAlso [Cudd_RecursiveDeref Cudd_Deref]

Definition at line 125 of file cuddRef.c.

00127 {
00128 
00129     n = Cudd_Regular(n);
00130 
00131     cuddSatInc(n->ref);
00132 
00133 } /* end of Cudd_Ref */

void cuddClearDeathRow ( DdManager *  table  ) 

Function********************************************************************

Synopsis [Clears the death row.]

Description []

SideEffects [None]

SeeAlso [Cudd_DelayedDerefBdd Cudd_IterDerefBdd Cudd_CheckZeroRef cuddGarbageCollect]

Definition at line 722 of file cuddRef.c.

00724 {
00725 #ifndef DD_NO_DEATH_ROW
00726     int i;
00727 
00728     for (i = 0; i < table->deathRowDepth; i++) {
00729         if (table->deathRow[i] == NULL) break;
00730         Cudd_IterDerefBdd(table,table->deathRow[i]);
00731         table->deathRow[i] = NULL;
00732     }
00733 #ifdef DD_DEBUG
00734     for (; i < table->deathRowDepth; i++) {
00735         assert(table->deathRow[i] == NULL);
00736     }
00737 #endif
00738     table->nextDead = 0;
00739 #endif
00740 
00741 } /* end of cuddClearDeathRow */

int cuddIsInDeathRow ( DdManager *  dd,
DdNode *  f 
)

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]

Definition at line 758 of file cuddRef.c.

00761 {
00762 #ifndef DD_NO_DEATH_ROW
00763     int i;
00764 
00765     for (i = 0; i < dd->deathRowDepth; i++) {
00766         if (f == dd->deathRow[i]) {
00767             return(i);
00768         }
00769     }
00770 #endif
00771 
00772     return(-1);
00773 
00774 } /* end of cuddIsInDeathRow */

void cuddReclaim ( DdManager *  table,
DdNode *  n 
)

Function********************************************************************

Synopsis [Brings children of a dead node back.]

Description []

SideEffects [None]

SeeAlso [cuddReclaimZdd]

Definition at line 580 of file cuddRef.c.

00583 {
00584     DdNode *N;
00585     int ord;
00586     DdNodePtr *stack = table->stack;
00587     int SP = 1;
00588     double initialDead = table->dead;
00589 
00590     N = Cudd_Regular(n);
00591 
00592 #ifdef DD_DEBUG
00593     assert(N->ref == 0);
00594 #endif
00595 
00596     do {
00597         if (N->ref == 0) {
00598             N->ref = 1;
00599             table->dead--;
00600             if (cuddIsConstant(N)) {
00601                 table->constants.dead--;
00602                 N = stack[--SP];
00603             } else {
00604                 ord = table->perm[N->index];
00605                 stack[SP++] = Cudd_Regular(cuddE(N));
00606                 table->subtables[ord].dead--;
00607                 N = cuddT(N);
00608             }
00609         } else {
00610             cuddSatInc(N->ref);
00611             N = stack[--SP];
00612         }
00613     } while (SP != 0);
00614 
00615     N = Cudd_Regular(n);
00616     cuddSatDec(N->ref);
00617     table->reclaimed += initialDead - table->dead;
00618 
00619 } /* end of cuddReclaim */

void cuddReclaimZdd ( DdManager *  table,
DdNode *  n 
)

Function********************************************************************

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

Description []

SideEffects [None]

SeeAlso [cuddReclaim]

Definition at line 634 of file cuddRef.c.

00637 {
00638     DdNode *N;
00639     int ord;
00640     DdNodePtr *stack = table->stack;
00641     int SP = 1;
00642 
00643     N = n;
00644 
00645 #ifdef DD_DEBUG
00646     assert(N->ref == 0);
00647 #endif
00648 
00649     do {
00650         cuddSatInc(N->ref);
00651 
00652         if (N->ref == 1) {
00653             table->deadZ--;
00654             table->reclaimed++;
00655 #ifdef DD_DEBUG
00656             assert(!cuddIsConstant(N));
00657 #endif
00658             ord = table->permZ[N->index];
00659             stack[SP++] = cuddE(N);
00660             table->subtableZ[ord].dead--;
00661             N = cuddT(N);
00662         } else {
00663             N = stack[--SP];
00664         }
00665     } while (SP != 0);
00666 
00667     cuddSatDec(n->ref);
00668 
00669 } /* end of cuddReclaimZdd */

void cuddShrinkDeathRow ( DdManager *  table  ) 

Function********************************************************************

Synopsis [Shrinks the death row.]

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

SideEffects [None]

SeeAlso [cuddClearDeathRow]

Definition at line 684 of file cuddRef.c.

00686 {
00687 #ifndef DD_NO_DEATH_ROW
00688     int i;
00689 
00690     if (table->deathRowDepth > 3) {
00691         for (i = table->deathRowDepth/4; i < table->deathRowDepth; i++) {
00692             if (table->deathRow[i] == NULL) break;
00693             Cudd_IterDerefBdd(table,table->deathRow[i]);
00694             table->deathRow[i] = NULL;
00695         }
00696         table->deathRowDepth /= 4;
00697         table->deadMask = table->deathRowDepth - 1;
00698         if ((unsigned) table->nextDead > table->deadMask) {
00699             table->nextDead = 0;
00700         }
00701         table->deathRow = REALLOC(DdNodePtr, table->deathRow,
00702                                    table->deathRowDepth);
00703     }
00704 #endif
00705 
00706 } /* end of cuddShrinkDeathRow */

int cuddTimesInDeathRow ( DdManager *  dd,
DdNode *  f 
)

Function********************************************************************

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

Description []

SideEffects [None]

SeeAlso [Cudd_DelayedDerefBdd cuddClearDeathRow cuddIsInDeathRow]

Definition at line 789 of file cuddRef.c.

00792 {
00793     int count = 0;
00794 #ifndef DD_NO_DEATH_ROW
00795     int i;
00796 
00797     for (i = 0; i < dd->deathRowDepth; i++) {
00798         count += f == dd->deathRow[i];
00799     }
00800 #endif
00801 
00802     return(count);
00803 
00804 } /* end of cuddTimesInDeathRow */

Variable Documentation

char rcsid [] DD_UNUSED = "$Id: cuddRef.c,v 1.28 2004/08/13 18:04:50 fabio Exp $" [static]

CFile***********************************************************************

FileName [cuddRef.c]

PackageName [cudd]

Synopsis [Functions that manipulate the reference counts.]

Description [External procedures included in this module:

Internal procedures included in this module:

]

SeeAlso []

Author [Fabio Somenzi]

Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado

All rights reserved.

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.

Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.

Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]

Definition at line 91 of file cuddRef.c.

Generated on Tue Jan 12 13:57:20 2010 for glu-2.2 by  doxygen 1.6.1