abc70930: src/bdd/cudd/cuddRef.c Source File

00001 
00041 #include    "util_hack.h"
00042 #include    "cuddInt.h"
00043 
00044 /*---------------------------------------------------------------------------*/
00045 /* Constant declarations                                                     */
00046 /*---------------------------------------------------------------------------*/
00047 
00048 
00049 /*---------------------------------------------------------------------------*/
00050 /* Stucture declarations                                                     */
00051 /*---------------------------------------------------------------------------*/
00052 
00053 
00054 /*---------------------------------------------------------------------------*/
00055 /* Type declarations                                                         */
00056 /*---------------------------------------------------------------------------*/
00057 
00058 
00059 /*---------------------------------------------------------------------------*/
00060 /* Variable declarations                                                     */
00061 /*---------------------------------------------------------------------------*/
00062 
00063 #ifndef lint
00064 static char rcsid[] DD_UNUSED = "$Id: cuddRef.c,v 1.1.1.1 2003/02/24 22:23:53 wjiang Exp $";
00065 #endif
00066 
00067 /*---------------------------------------------------------------------------*/
00068 /* Macro declarations                                                        */
00069 /*---------------------------------------------------------------------------*/
00070 
00071 
00074 /*---------------------------------------------------------------------------*/
00075 /* Static function prototypes                                                */
00076 /*---------------------------------------------------------------------------*/
00077 
00081 /*---------------------------------------------------------------------------*/
00082 /* Definition of exported functions                                          */
00083 /*---------------------------------------------------------------------------*/
00084 
00097 void
00098 Cudd_Ref(
00099   DdNode * n)
00100 {
00101 
00102     n = Cudd_Regular(n);
00103 
00104     cuddSatInc(n->ref);
00105 
00106 } /* end of Cudd_Ref */
00107 
00108 
00122 void
00123 Cudd_RecursiveDeref(
00124   DdManager * table,
00125   DdNode * n)
00126 {
00127     DdNode *N;
00128     int ord;
00129     DdNodePtr *stack = table->stack;
00130     int SP = 1;
00131 
00132     unsigned int live = table->keys - table->dead;
00133     if (live > table->peakLiveNodes) {
00134         table->peakLiveNodes = live;
00135     }
00136 
00137     N = Cudd_Regular(n);
00138 
00139     do {
00140 #ifdef DD_DEBUG
00141         assert(N->ref != 0);
00142 #endif
00143 
00144         if (N->ref == 1) {
00145             N->ref = 0;
00146             table->dead++;
00147 #ifdef DD_STATS
00148             table->nodesDropped++;
00149 #endif
00150             if (cuddIsConstant(N)) {
00151                 table->constants.dead++;
00152                 N = stack[--SP];
00153             } else {
00154                 ord = table->perm[N->index];
00155                 stack[SP++] = Cudd_Regular(cuddE(N));
00156                 table->subtables[ord].dead++;
00157                 N = cuddT(N);
00158             }
00159         } else {
00160             cuddSatDec(N->ref);
00161             N = stack[--SP];
00162         }
00163     } while (SP != 0);
00164 
00165 } /* end of Cudd_RecursiveDeref */
00166 
00167 
00185 void
00186 Cudd_IterDerefBdd(
00187   DdManager * table,
00188   DdNode * n)
00189 {
00190     DdNode *N;
00191     int ord;
00192     DdNodePtr *stack = table->stack;
00193     int SP = 1;
00194 
00195     unsigned int live = table->keys - table->dead;
00196     if (live > table->peakLiveNodes) {
00197         table->peakLiveNodes = live;
00198     }
00199 
00200     N = Cudd_Regular(n);
00201 
00202     do {
00203 #ifdef DD_DEBUG
00204         assert(N->ref != 0);
00205 #endif
00206 
00207         if (N->ref == 1) {
00208             N->ref = 0;
00209             table->dead++;
00210 #ifdef DD_STATS
00211             table->nodesDropped++;
00212 #endif
00213             ord = table->perm[N->index];
00214             stack[SP++] = Cudd_Regular(cuddE(N));
00215             table->subtables[ord].dead++;
00216             N = cuddT(N);
00217         } else {
00218             cuddSatDec(N->ref);
00219             N = stack[--SP];
00220         }
00221     } while (SP != 0);
00222 
00223 } /* end of Cudd_IterDerefBdd */
00224 
00225 
00242 void
00243 Cudd_DelayedDerefBdd(
00244   DdManager * table,
00245   DdNode * n)
00246 {
00247     DdNode *N;
00248     int ord;
00249     DdNodePtr *stack;
00250     int SP;
00251 
00252     unsigned int live = table->keys - table->dead;
00253     if (live > table->peakLiveNodes) {
00254         table->peakLiveNodes = live;
00255     }
00256 
00257     n = Cudd_Regular(n);
00258 #ifdef DD_DEBUG
00259     assert(n->ref != 0);
00260 #endif
00261 
00262 #ifdef DD_NO_DEATH_ROW
00263     N = n;
00264 #else
00265     if (cuddIsConstant(n) || n->ref > 1) {
00266 #ifdef DD_DEBUG
00267         assert(n->ref != 1 && (!cuddIsConstant(n) || n == DD_ONE(table)));
00268 #endif
00269         cuddSatDec(n->ref);
00270         return;
00271     }
00272 
00273     N = table->deathRow[table->nextDead];
00274 
00275     if (N != NULL) {
00276 #endif
00277 #ifdef DD_DEBUG
00278         assert(!Cudd_IsComplement(N));
00279 #endif
00280         stack = table->stack;
00281         SP = 1;
00282         do {
00283 #ifdef DD_DEBUG
00284             assert(N->ref != 0);
00285 #endif
00286             if (N->ref == 1) {
00287                 N->ref = 0;
00288                 table->dead++;
00289 #ifdef DD_STATS
00290                 table->nodesDropped++;
00291 #endif
00292                 ord = table->perm[N->index];
00293                 stack[SP++] = Cudd_Regular(cuddE(N));
00294                 table->subtables[ord].dead++;
00295                 N = cuddT(N);
00296             } else {
00297                 cuddSatDec(N->ref);
00298                 N = stack[--SP];
00299             }
00300         } while (SP != 0);
00301 #ifndef DD_NO_DEATH_ROW
00302     }
00303     table->deathRow[table->nextDead] = n;
00304 
00305     /* Udate insertion point. */
00306     table->nextDead++;
00307     table->nextDead &= table->deadMask;
00308 #if 0
00309     if (table->nextDead == table->deathRowDepth) {
00310         if (table->deathRowDepth < table->looseUpTo / 2) {
00311             extern void (*MMoutOfMemory)(long);
00312             void (*saveHandler)(long) = MMoutOfMemory;
00313             DdNodePtr *newRow;
00314             MMoutOfMemory = Cudd_OutOfMem;
00315             newRow = REALLOC(DdNodePtr,table->deathRow,2*table->deathRowDepth);
00316             MMoutOfMemory = saveHandler;
00317             if (newRow == NULL) {
00318                 table->nextDead = 0;
00319             } else {
00320                 int i;
00321                 table->memused += table->deathRowDepth;
00322                 i = table->deathRowDepth;
00323                 table->deathRowDepth <<= 1;
00324                 for (; i < table->deathRowDepth; i++) {
00325                     newRow[i] = NULL;
00326                 }
00327                 table->deadMask = table->deathRowDepth - 1;
00328                 table->deathRow = newRow;
00329             }
00330         } else {
00331             table->nextDead = 0;
00332         }
00333     }
00334 #endif
00335 #endif
00336 
00337 } /* end of Cudd_DelayedDerefBdd */
00338 
00339 
00353 void
00354 Cudd_RecursiveDerefZdd(
00355   DdManager * table,
00356   DdNode * n)
00357 {
00358     DdNode *N;
00359     int ord;
00360     DdNodePtr *stack = table->stack;
00361     int SP = 1;
00362 
00363     N = n;
00364 
00365     do {
00366 #ifdef DD_DEBUG
00367         assert(N->ref != 0);
00368 #endif
00369 
00370         cuddSatDec(N->ref);
00371     
00372         if (N->ref == 0) {
00373             table->deadZ++;
00374 #ifdef DD_STATS
00375             table->nodesDropped++;
00376 #endif
00377 #ifdef DD_DEBUG
00378             assert(!cuddIsConstant(N));
00379 #endif
00380             ord = table->permZ[N->index];
00381             stack[SP++] = cuddE(N);
00382             table->subtableZ[ord].dead++;
00383             N = cuddT(N);
00384         } else {
00385             N = stack[--SP];
00386         }
00387     } while (SP != 0);
00388 
00389 } /* end of Cudd_RecursiveDerefZdd */
00390 
00391 
00406 void
00407 Cudd_Deref(
00408   DdNode * node)
00409 {
00410     node = Cudd_Regular(node);
00411     cuddSatDec(node->ref);
00412 
00413 } /* end of Cudd_Deref */
00414 
00415 
00434 int
00435 Cudd_CheckZeroRef(
00436   DdManager * manager)
00437 {
00438     int size;
00439     int i, j;
00440     int remain; /* the expected number of remaining references to one */
00441     DdNodePtr *nodelist;
00442     DdNode *node;
00443     DdNode *sentinel = &(manager->sentinel);
00444     DdSubtable *subtable;
00445     int count = 0;
00446     int index;
00447 
00448 #ifndef DD_NO_DEATH_ROW
00449     cuddClearDeathRow(manager);
00450 #endif
00451 
00452     /* First look at the BDD/ADD subtables. */
00453     remain = 1; /* reference from the manager */
00454     size = manager->size;
00455     remain += 2 * size; /* reference from the BDD projection functions */
00456 
00457     for (i = 0; i < size; i++) {
00458         subtable = &(manager->subtables[i]);
00459         nodelist = subtable->nodelist;
00460         for (j = 0; (unsigned) j < subtable->slots; j++) {
00461             node = nodelist[j];
00462             while (node != sentinel) {
00463                 if (node->ref != 0 && node->ref != DD_MAXREF) {
00464                     index = (int) node->index;
00465                     if (node != manager->vars[index]) {
00466                         count++;
00467                     } else {
00468                         if (node->ref != 1) {
00469                             count++;
00470                         }
00471                     }
00472                 }
00473                 node = node->next;
00474             }
00475         }
00476     }
00477 
00478     /* Then look at the ZDD subtables. */
00479     size = manager->sizeZ;
00480     if (size) /* references from ZDD universe */
00481         remain += 2;
00482 
00483     for (i = 0; i < size; i++) {
00484         subtable = &(manager->subtableZ[i]);
00485         nodelist = subtable->nodelist;
00486         for (j = 0; (unsigned) j < subtable->slots; j++) {
00487             node = nodelist[j];
00488             while (node != NULL) {
00489                 if (node->ref != 0 && node->ref != DD_MAXREF) {
00490                     index = (int) node->index;
00491                     if (node == manager->univ[manager->permZ[index]]) {
00492                         if (node->ref > 2) {
00493                             count++;
00494                         }
00495                     } else {
00496                         count++;
00497                     }
00498                 }
00499                 node = node->next;
00500             }
00501         }
00502     }
00503 
00504     /* Now examine the constant table. Plusinfinity, minusinfinity, and
00505     ** zero are referenced by the manager. One is referenced by the
00506     ** manager, by the ZDD universe, and by all projection functions.
00507     ** All other nodes should have no references.
00508     */
00509     nodelist = manager->constants.nodelist;
00510     for (j = 0; (unsigned) j < manager->constants.slots; j++) {
00511         node = nodelist[j];
00512         while (node != NULL) {
00513             if (node->ref != 0 && node->ref != DD_MAXREF) {
00514                 if (node == manager->one) {
00515                     if ((int) node->ref != remain) {
00516                         count++;
00517                     }
00518                 } else if (node == manager->zero ||
00519                 node == manager->plusinfinity ||
00520                 node == manager->minusinfinity) {
00521                     if (node->ref != 1) {
00522                         count++;
00523                     }
00524                 } else {
00525                     count++;
00526                 }
00527             }
00528             node = node->next;
00529         }
00530     }
00531     return(count);
00532 
00533 } /* end of Cudd_CheckZeroRef */
00534 
00535 
00536 /*---------------------------------------------------------------------------*/
00537 /* Definition of internal functions                                          */
00538 /*---------------------------------------------------------------------------*/
00539 
00540 
00552 void
00553 cuddReclaim(
00554   DdManager * table,
00555   DdNode * n)
00556 {
00557     DdNode *N;
00558     int ord;
00559     DdNodePtr *stack = table->stack;
00560     int SP = 1;
00561     double initialDead = table->dead;
00562 
00563     N = Cudd_Regular(n);
00564 
00565 #ifdef DD_DEBUG
00566     assert(N->ref == 0);
00567 #endif
00568 
00569     do {
00570         if (N->ref == 0) {
00571             N->ref = 1;
00572             table->dead--;
00573             if (cuddIsConstant(N)) {
00574                 table->constants.dead--;
00575                 N = stack[--SP];
00576             } else {
00577                 ord = table->perm[N->index];
00578                 stack[SP++] = Cudd_Regular(cuddE(N));
00579                 table->subtables[ord].dead--;
00580                 N = cuddT(N);
00581             }
00582         } else {
00583             cuddSatInc(N->ref);
00584             N = stack[--SP];
00585         }
00586     } while (SP != 0);
00587 
00588     N = Cudd_Regular(n);
00589     cuddSatDec(N->ref);
00590     table->reclaimed += initialDead - table->dead;
00591 
00592 } /* end of cuddReclaim */
00593 
00594 
00606 void
00607 cuddReclaimZdd(
00608   DdManager * table,
00609   DdNode * n)
00610 {
00611     DdNode *N;
00612     int ord;
00613     DdNodePtr *stack = table->stack;
00614     int SP = 1;
00615 
00616     N = n;
00617 
00618 #ifdef DD_DEBUG
00619     assert(N->ref == 0);
00620 #endif
00621 
00622     do {
00623         cuddSatInc(N->ref);
00624 
00625         if (N->ref == 1) {
00626             table->deadZ--;
00627             table->reclaimed++;
00628 #ifdef DD_DEBUG
00629             assert(!cuddIsConstant(N));
00630 #endif
00631             ord = table->permZ[N->index];
00632             stack[SP++] = cuddE(N);
00633             table->subtableZ[ord].dead--;
00634             N = cuddT(N);
00635         } else {
00636             N = stack[--SP];
00637         }
00638     } while (SP != 0);
00639 
00640     cuddSatDec(n->ref);
00641 
00642 } /* end of cuddReclaimZdd */
00643 
00644 
00656 void
00657 cuddShrinkDeathRow(
00658   DdManager *table)
00659 {
00660 #ifndef DD_NO_DEATH_ROW
00661     int i;
00662 
00663     if (table->deathRowDepth > 3) {
00664         for (i = table->deathRowDepth/4; i < table->deathRowDepth; i++) {
00665             if (table->deathRow[i] == NULL) break;
00666             Cudd_IterDerefBdd(table,table->deathRow[i]);
00667             table->deathRow[i] = NULL;
00668         }
00669         table->deathRowDepth /= 4;
00670         table->deadMask = table->deathRowDepth - 2;
00671         if ((unsigned) table->nextDead > table->deadMask) {
00672             table->nextDead = 0;
00673         }
00674         table->deathRow = REALLOC(DdNodePtr, table->deathRow,
00675                                    table->deathRowDepth);
00676     }
00677 #endif
00678 
00679 } /* end of cuddShrinkDeathRow */
00680 
00681 
00694 void
00695 cuddClearDeathRow(
00696   DdManager *table)
00697 {
00698 #ifndef DD_NO_DEATH_ROW
00699     int i;
00700 
00701     for (i = 0; i < table->deathRowDepth; i++) {
00702         if (table->deathRow[i] == NULL) break;
00703         Cudd_IterDerefBdd(table,table->deathRow[i]);
00704         table->deathRow[i] = NULL;
00705     }
00706 #ifdef DD_DEBUG
00707     for (; i < table->deathRowDepth; i++) {
00708         assert(table->deathRow[i] == NULL);
00709     }
00710 #endif
00711     table->nextDead = 0;
00712 #endif
00713 
00714 } /* end of cuddClearDeathRow */
00715 
00716 
00730 int
00731 cuddIsInDeathRow(
00732   DdManager *dd,
00733   DdNode *f)
00734 {
00735 #ifndef DD_NO_DEATH_ROW
00736     int i;
00737 
00738     for (i = 0; i < dd->deathRowDepth; i++) {
00739         if (f == dd->deathRow[i]) {
00740             return(i);
00741         }
00742     }
00743 #endif
00744 
00745     return(-1);
00746 
00747 } /* end of cuddIsInDeathRow */
00748 
00749 
00761 int
00762 cuddTimesInDeathRow(
00763   DdManager *dd,
00764   DdNode *f)
00765 {
00766     int count = 0;
00767 #ifndef DD_NO_DEATH_ROW
00768     int i;
00769 
00770     for (i = 0; i < dd->deathRowDepth; i++) {
00771         count += f == dd->deathRow[i];
00772     }
00773 #endif
00774 
00775     return(count);
00776 
00777 } /* end of cuddTimesInDeathRow */
00778 
00779 /*---------------------------------------------------------------------------*/
00780 /* Definition of static functions                                            */
00781 /*---------------------------------------------------------------------------*/