glu-2.2: src/cuBdd/cuddRef.c Source File

00001 
00068 #include "util.h"
00069 #include "cuddInt.h"
00070 
00071 /*---------------------------------------------------------------------------*/
00072 /* Constant declarations                                                     */
00073 /*---------------------------------------------------------------------------*/
00074 
00075 
00076 /*---------------------------------------------------------------------------*/
00077 /* Stucture declarations                                                     */
00078 /*---------------------------------------------------------------------------*/
00079 
00080 
00081 /*---------------------------------------------------------------------------*/
00082 /* Type declarations                                                         */
00083 /*---------------------------------------------------------------------------*/
00084 
00085 
00086 /*---------------------------------------------------------------------------*/
00087 /* Variable declarations                                                     */
00088 /*---------------------------------------------------------------------------*/
00089 
00090 #ifndef lint
00091 static char rcsid[] DD_UNUSED = "$Id: cuddRef.c,v 1.28 2004/08/13 18:04:50 fabio Exp $";
00092 #endif
00093 
00094 /*---------------------------------------------------------------------------*/
00095 /* Macro declarations                                                        */
00096 /*---------------------------------------------------------------------------*/
00097 
00098 
00101 /*---------------------------------------------------------------------------*/
00102 /* Static function prototypes                                                */
00103 /*---------------------------------------------------------------------------*/
00104 
00108 /*---------------------------------------------------------------------------*/
00109 /* Definition of exported functions                                          */
00110 /*---------------------------------------------------------------------------*/
00111 
00124 void
00125 Cudd_Ref(
00126   DdNode * n)
00127 {
00128 
00129     n = Cudd_Regular(n);
00130 
00131     cuddSatInc(n->ref);
00132 
00133 } /* end of Cudd_Ref */
00134 
00135 
00149 void
00150 Cudd_RecursiveDeref(
00151   DdManager * table,
00152   DdNode * n)
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 */
00193 
00194 
00212 void
00213 Cudd_IterDerefBdd(
00214   DdManager * table,
00215   DdNode * n)
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 */
00251 
00252 
00269 void
00270 Cudd_DelayedDerefBdd(
00271   DdManager * table,
00272   DdNode * n)
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 */
00365 
00366 
00380 void
00381 Cudd_RecursiveDerefZdd(
00382   DdManager * table,
00383   DdNode * n)
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 */
00417 
00418 
00433 void
00434 Cudd_Deref(
00435   DdNode * node)
00436 {
00437     node = Cudd_Regular(node);
00438     cuddSatDec(node->ref);
00439 
00440 } /* end of Cudd_Deref */
00441 
00442 
00461 int
00462 Cudd_CheckZeroRef(
00463   DdManager * manager)
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 */
00561 
00562 
00563 /*---------------------------------------------------------------------------*/
00564 /* Definition of internal functions                                          */
00565 /*---------------------------------------------------------------------------*/
00566 
00567 
00579 void
00580 cuddReclaim(
00581   DdManager * table,
00582   DdNode * n)
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 */
00620 
00621 
00633 void
00634 cuddReclaimZdd(
00635   DdManager * table,
00636   DdNode * n)
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 */
00670 
00671 
00683 void
00684 cuddShrinkDeathRow(
00685   DdManager *table)
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 */
00707 
00708 
00721 void
00722 cuddClearDeathRow(
00723   DdManager *table)
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 */
00742 
00743 
00757 int
00758 cuddIsInDeathRow(
00759   DdManager *dd,
00760   DdNode *f)
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 */
00775 
00776 
00788 int
00789 cuddTimesInDeathRow(
00790   DdManager *dd,
00791   DdNode *f)
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 */
00805 
00806 /*---------------------------------------------------------------------------*/
00807 /* Definition of static functions                                            */
00808 /*---------------------------------------------------------------------------*/