glu-2.2: src/calBdd/calHashTable.c Source File

00001 
00038 #include "calInt.h"
00039 
00040 /*---------------------------------------------------------------------------*/
00041 /* Constant declarations                                                     */
00042 /*---------------------------------------------------------------------------*/
00043 
00044 
00045 /*---------------------------------------------------------------------------*/
00046 /* Type declarations                                                         */
00047 /*---------------------------------------------------------------------------*/
00048 
00049 
00050 /*---------------------------------------------------------------------------*/
00051 /* Stucture declarations                                                     */
00052 /*---------------------------------------------------------------------------*/
00053 
00054 
00055 /*---------------------------------------------------------------------------*/
00056 /* Variable declarations                                                     */
00057 /*---------------------------------------------------------------------------*/
00058 
00059 /*---------------------------------------------------------------------------*/
00060 /* Macro declarations                                                        */
00061 /*---------------------------------------------------------------------------*/
00062 
00065 /*---------------------------------------------------------------------------*/
00066 /* Static function prototypes                                                */
00067 /*---------------------------------------------------------------------------*/
00068 
00069 static int CeilLog2(int number);
00070 
00074 /*---------------------------------------------------------------------------*/
00075 /* Definition of exported functions                                          */
00076 /*---------------------------------------------------------------------------*/
00077 
00078 
00079 /*---------------------------------------------------------------------------*/
00080 /* Definition of internal functions                                          */
00081 /*---------------------------------------------------------------------------*/
00082 
00094 CalHashTable_t *
00095 CalHashTableInit(Cal_BddManager_t *bddManager, Cal_BddId_t  bddId)
00096 {
00097   CalHashTable_t *hashTable;
00098 
00099   hashTable = Cal_MemAlloc(CalHashTable_t, 1);
00100   /*hashTable = CAL_BDD_NEW_REC(bddManager, CalHashTable_t);*/
00101   if(hashTable == Cal_Nil(CalHashTable_t)){
00102     CalBddFatalMessage("out of memory");
00103   }
00104   hashTable->sizeIndex = HASH_TABLE_DEFAULT_SIZE_INDEX;
00105   hashTable->numBins = TABLE_SIZE(hashTable->sizeIndex);
00106   hashTable->maxCapacity = hashTable->numBins*HASH_TABLE_DEFAULT_MAX_DENSITY;
00107   hashTable->bins = Cal_MemAlloc(CalBddNode_t *, hashTable->numBins);
00108   if(hashTable->bins == Cal_Nil(CalBddNode_t *)){
00109     CalBddFatalMessage("out of memory");
00110   }
00111   memset((char *)hashTable->bins, 0,
00112          hashTable->numBins*sizeof(CalBddNode_t *)); 
00113   hashTable->bddId = bddId;
00114   hashTable->nodeManager = bddManager->nodeManagerArray[bddId];
00115   hashTable->requestNodeList = Cal_Nil(CalRequestNode_t);
00116   memset((char *)(&(hashTable->startNode)), 0, sizeof(CalBddNode_t));
00117   hashTable->endNode = &(hashTable->startNode);
00118   hashTable->numEntries = 0;
00119   return hashTable;
00120 }
00121 
00122 
00134 int
00135 CalHashTableQuit(Cal_BddManager_t *bddManager, CalHashTable_t * hashTable)
00136 {
00137   if(hashTable == Cal_Nil(CalHashTable_t))return 1;
00138   /*
00139   for(i = 0; i < hashTable->numBins; i++){
00140     ptr = hashTable->bins[i];
00141     while(ptr != Cal_Nil(CalBddNode_t)){
00142       next = CalBddNodeGetNextBddNode(ptr);
00143       CalNodeManagerFreeNode(hashTable->nodeManager, ptr);
00144       ptr = next;
00145     }
00146   }
00147   There is no need to free the nodes individually. They will be taken
00148   care of by the PageManagerQuit.
00149   We need to make sure that this function is called only during the global quitting.
00150   If it need be called at some intermediate point, we need to free the BDD nodes 
00151   appropriately.
00152   */
00153   
00154   Cal_MemFree(hashTable->bins);
00155   Cal_MemFree(hashTable);
00156   /*CAL_BDD_FREE_REC(bddManager, hashTable, CalHashTable_t);*/
00157   return 0;
00158 }
00159 
00160 
00161 
00173 void
00174 CalHashTableAddDirect(CalHashTable_t * hashTable, CalBddNode_t * bddNode)
00175 {
00176   int hashValue;
00177   CalBddNode_t *thenBddNode, *elseBddNode;
00178 
00179   hashTable->numEntries++;
00180   if(hashTable->numEntries >= hashTable->maxCapacity){
00181     CalHashTableRehash(hashTable, 1);
00182   }
00183   thenBddNode = CalBddNodeGetThenBddNode(bddNode);
00184   elseBddNode = CalBddNodeGetElseBddNode(bddNode);
00185   hashValue = CalDoHash2(thenBddNode, elseBddNode, hashTable);
00186   CalBddNodePutNextBddNode(bddNode, hashTable->bins[hashValue]);
00187   hashTable->bins[hashValue] = bddNode;
00188 }
00189 
00190 
00202 int
00203 CalHashTableFindOrAdd(CalHashTable_t * hashTable,
00204                       Cal_Bdd_t  thenBdd,
00205                       Cal_Bdd_t  elseBdd,
00206                       Cal_Bdd_t * bddPtr)
00207 {
00208   CalBddNode_t *ptr;
00209   Cal_Bdd_t tmpBdd;
00210   int hashValue;
00211   
00212   hashValue = CalDoHash2(CalBddGetBddNode(thenBdd), 
00213       CalBddGetBddNode(elseBdd), hashTable);
00214   ptr = hashTable->bins[hashValue];
00215   while(ptr != Cal_Nil(CalBddNode_t)){
00216     CalBddNodeGetThenBdd(ptr, tmpBdd);
00217     if(CalBddIsEqual(thenBdd, tmpBdd)){
00218       CalBddNodeGetElseBdd(ptr, tmpBdd);
00219       if(CalBddIsEqual(elseBdd, tmpBdd)){
00220         CalBddPutBddId(*bddPtr, hashTable->bddId);
00221         CalBddPutBddNode(*bddPtr, ptr);
00222         return 1;
00223       }
00224     }
00225     ptr = CalBddNodeGetNextBddNode(ptr);
00226   }
00227   hashTable->numEntries++;
00228   if(hashTable->numEntries > hashTable->maxCapacity){
00229     CalHashTableRehash(hashTable,1);
00230     hashValue = CalDoHash2(CalBddGetBddNode(thenBdd),
00231         CalBddGetBddNode(elseBdd), hashTable);
00232   }
00233   CalNodeManagerInitBddNode(hashTable->nodeManager, thenBdd, elseBdd, 
00234       hashTable->bins[hashValue], ptr);
00235   hashTable->bins[hashValue] = ptr;
00236   CalBddPutBddId(*bddPtr, hashTable->bddId);
00237   CalBddPutBddNode(*bddPtr, ptr);
00238   return 0;
00239 }
00240 
00252 int
00253 CalHashTableAddDirectAux(CalHashTable_t * hashTable, Cal_Bdd_t
00254                          thenBdd, Cal_Bdd_t  elseBdd, Cal_Bdd_t *
00255                          bddPtr) 
00256 {
00257   CalBddNode_t *ptr;
00258   int hashValue;
00259   
00260   hashTable->numEntries++;
00261   if(hashTable->numEntries >= hashTable->maxCapacity){
00262     CalHashTableRehash(hashTable, 1);
00263   }
00264   hashValue = CalDoHash2(CalBddGetBddNode(thenBdd), CalBddGetBddNode(elseBdd),
00265                          hashTable); 
00266   CalNodeManagerInitBddNode(hashTable->nodeManager, thenBdd, elseBdd, 
00267       hashTable->bins[hashValue], ptr);
00268   hashTable->bins[hashValue] = ptr;
00269   CalBddPutBddId(*bddPtr, hashTable->bddId);
00270   CalBddPutBddNode(*bddPtr, ptr);
00271   return 0;
00272 }
00273 
00285 void
00286 CalHashTableCleanUp(CalHashTable_t * hashTable)
00287 {
00288   CalNodeManager_t *nodeManager;
00289 
00290   nodeManager = hashTable->nodeManager;
00291   hashTable->endNode->nextBddNode = nodeManager->freeNodeList;
00292   nodeManager->freeNodeList = hashTable->startNode.nextBddNode;
00293   hashTable->endNode = &(hashTable->startNode);
00294   hashTable->numEntries = 0;
00295   hashTable->startNode.nextBddNode = NULL;
00296   Cal_Assert(!(hashTable->requestNodeList));
00297   hashTable->requestNodeList = Cal_Nil(CalRequestNode_t);
00298   return;
00299 }
00300 
00301 
00313 int
00314 CalHashTableLookup(
00315   CalHashTable_t * hashTable,
00316   Cal_Bdd_t  thenBdd,
00317   Cal_Bdd_t  elseBdd,
00318   Cal_Bdd_t * bddPtr)
00319 {
00320   CalBddNode_t *ptr;
00321   Cal_Bdd_t tmpBdd;
00322   int hashValue;
00323   
00324   hashValue = CalDoHash2(CalBddGetBddNode(thenBdd),
00325       CalBddGetBddNode(elseBdd), hashTable);
00326   ptr = hashTable->bins[hashValue];
00327   while(ptr != Cal_Nil(CalBddNode_t)){
00328     CalBddNodeGetThenBdd(ptr, tmpBdd);
00329     if(CalBddIsEqual(thenBdd, tmpBdd)){
00330       CalBddNodeGetElseBdd(ptr, tmpBdd);
00331       if(CalBddIsEqual(elseBdd, tmpBdd)){
00332         CalBddPutBddId(*bddPtr, hashTable->bddId);
00333         CalBddPutBddNode(*bddPtr, ptr);
00334         return 1;
00335       }
00336     }
00337     ptr = CalBddNodeGetNextBddNode(ptr);
00338   }
00339   return 0;
00340 }
00341 
00353 void
00354 CalHashTableDelete(CalHashTable_t * hashTable, CalBddNode_t * bddNode)
00355 {
00356   int hashValue;
00357   Cal_Bdd_t thenBdd, elseBdd;
00358   CalBddNode_t  *ptr, *last;
00359 
00360   CalBddNodeGetThenBdd(bddNode, thenBdd);
00361   CalBddNodeGetElseBdd(bddNode, elseBdd);
00362   hashValue =
00363       CalDoHash2(CalBddGetBddNode(thenBdd), CalBddGetBddNode(elseBdd), hashTable);
00364 
00365   last = Cal_Nil(CalBddNode_t);
00366   ptr = hashTable->bins[hashValue];
00367   while(ptr != Cal_Nil(CalBddNode_t)){
00368     if(ptr == bddNode){
00369       if(last == Cal_Nil(CalBddNode_t)){
00370         hashTable->bins[hashValue] = CalBddNodeGetNextBddNode(ptr);
00371       }
00372       else{
00373         CalBddNodePutNextBddNode(last, CalBddNodeGetNextBddNode(ptr));
00374       }
00375       hashTable->numEntries--;
00376       CalNodeManagerFreeNode(hashTable->nodeManager, ptr);
00377       return;
00378     }
00379     last = ptr;
00380     ptr = CalBddNodeGetNextBddNode(ptr);
00381   }
00382   CalBddWarningMessage("Trying to delete a non-existent node\n");
00383 }
00384 
00385 
00397 int
00398 CalUniqueTableForIdLookup(
00399   Cal_BddManager_t * bddManager,
00400   CalHashTable_t * hashTable,
00401   Cal_Bdd_t  thenBdd,
00402   Cal_Bdd_t  elseBdd,
00403   Cal_Bdd_t * bddPtr)
00404 {
00405   CalBddNode_t *ptr;
00406   Cal_Bdd_t tmpBdd;
00407   int hashValue;
00408   
00409   hashValue = CalDoHash2(CalBddGetBddNode(thenBdd),
00410       CalBddGetBddNode(elseBdd), hashTable);
00411   ptr = hashTable->bins[hashValue];
00412   if(CalBddIsOutPos(thenBdd)){
00413     while(ptr != Cal_Nil(CalBddNode_t)){
00414       CalBddNodeGetThenBdd(ptr, tmpBdd);
00415       if(CalBddIsEqual(thenBdd, tmpBdd)){
00416         CalBddNodeGetElseBdd(ptr, tmpBdd);
00417         if(CalBddIsEqual(elseBdd, tmpBdd)){
00418           CalBddPutBddId(*bddPtr, hashTable->bddId);
00419           CalBddPutBddNode(*bddPtr, ptr);
00420           return 1;
00421         }
00422       }
00423       ptr = CalBddNodeGetNextBddNode(ptr);
00424     }
00425   }
00426   else{
00427     CalBddNot(thenBdd, thenBdd);
00428     CalBddNot(elseBdd, elseBdd);
00429     while(ptr != Cal_Nil(CalBddNode_t)){
00430       CalBddNodeGetThenBdd(ptr, tmpBdd);
00431       if(CalBddIsEqual(thenBdd, tmpBdd)){
00432         CalBddNodeGetElseBdd(ptr, tmpBdd);
00433         if(CalBddIsEqual(elseBdd, tmpBdd)){
00434           CalBddPutBddId(*bddPtr, hashTable->bddId);
00435           CalBddPutBddNode(*bddPtr, CalBddNodeNot(ptr));
00436           return 1;
00437         }
00438       }
00439       ptr = CalBddNodeGetNextBddNode(ptr);
00440     }
00441   }
00442   return 0;
00443 }
00444 
00445 
00458 int
00459 CalUniqueTableForIdFindOrAdd(
00460   Cal_BddManager_t * bddManager,
00461   CalHashTable_t * hashTable,
00462   Cal_Bdd_t  thenBdd,
00463   Cal_Bdd_t  elseBdd,
00464   Cal_Bdd_t * bddPtr)
00465 {
00466   int found = 0; 
00467   if (CalBddIsEqual(thenBdd, elseBdd)){
00468     *bddPtr = thenBdd;
00469     found = 1;
00470   }
00471   else if(CalBddIsOutPos(thenBdd)){
00472     found = CalHashTableFindOrAdd(hashTable, thenBdd, elseBdd, bddPtr);
00473   }
00474   else{
00475     CalBddNot(thenBdd, thenBdd);
00476     CalBddNot(elseBdd, elseBdd);
00477     found = CalHashTableFindOrAdd(hashTable, thenBdd, elseBdd, bddPtr);
00478     CalBddNot(*bddPtr, *bddPtr);
00479   }
00480   if (!found) bddManager->numNodes++;
00481   return found;
00482 }
00483 
00484 
00497 void
00498 CalHashTableRehash(CalHashTable_t *hashTable,int grow)
00499 {
00500   CalBddNode_t *ptr, *next;
00501   CalBddNode_t **oldBins = hashTable->bins;
00502   int i, hashValue;
00503   int oldNumBins = hashTable->numBins;
00504 
00505   if(grow){
00506     hashTable->sizeIndex++;
00507   }
00508   else{
00509     if (hashTable->sizeIndex <= HASH_TABLE_DEFAULT_SIZE_INDEX){/* No need to rehash */
00510       return;
00511     }
00512     hashTable->sizeIndex--;
00513   }
00514 
00515   hashTable->numBins = TABLE_SIZE(hashTable->sizeIndex);
00516   hashTable->maxCapacity = hashTable->numBins * HASH_TABLE_DEFAULT_MAX_DENSITY;
00517   hashTable->bins = Cal_MemAlloc(CalBddNode_t *, hashTable->numBins);
00518   if(hashTable->bins == Cal_Nil(CalBddNode_t *)){
00519     CalBddFatalMessage("out of memory");
00520   }
00521   /*
00522   for(i = 0; i < hashTable->numBins; i++){
00523     hashTable->bins[i] = Cal_Nil(CalBddNode_t);
00524   }
00525   */
00526   memset((char *)hashTable->bins, 0,
00527          hashTable->numBins*sizeof(CalBddNode_t *));
00528 
00529   for(i = 0; i < oldNumBins; i++){
00530     ptr = oldBins[i];
00531     while(ptr != Cal_Nil(CalBddNode_t)){
00532       next = CalBddNodeGetNextBddNode(ptr);
00533       hashValue = CalDoHash2(CalBddNodeGetThenBddNode(ptr),
00534           CalBddNodeGetElseBddNode(ptr), hashTable);
00535       CalBddNodePutNextBddNode(ptr, hashTable->bins[hashValue]);
00536       hashTable->bins[hashValue] = ptr;
00537       ptr = next;
00538     }
00539   }
00540   Cal_MemFree(oldBins);
00541 }
00542 
00554 void
00555 CalUniqueTableForIdRehashNode(CalHashTable_t *hashTable, CalBddNode_t *bddNode,
00556                               CalBddNode_t *thenBddNode,
00557                               CalBddNode_t *elseBddNode)
00558 
00559 {
00560   CalBddNode_t *nextBddNode;
00561   CalBddNode_t *ptr;
00562   int found;
00563   int hashValue;
00564   int oldHashValue;
00565   Cal_Bdd_t thenBdd;
00566 
00567   oldHashValue = CalDoHash2(thenBddNode, elseBddNode, hashTable);
00568   hashValue = CalDoHash2(CalBddNodeGetThenBddNode(bddNode),
00569                          CalBddNodeGetElseBddNode(bddNode),
00570                          hashTable);
00571   CalBddNodeGetThenBdd(bddNode, thenBdd);
00572   if (CalBddIsComplement(thenBdd)) {
00573     CalBddFatalMessage("Complement edge on then pointer");
00574   }
00575   if (oldHashValue == hashValue) {
00576     return;
00577   }
00578 
00579   found = 0;
00580   ptr = hashTable->bins[oldHashValue];
00581   if ((ptr != Cal_Nil(CalBddNode_t)) && (ptr == bddNode)) {
00582     hashTable->bins[oldHashValue] = CalBddNodeGetNextBddNode(bddNode);
00583     found = 1;
00584   } else {
00585     while (ptr != Cal_Nil(CalBddNode_t)) {
00586       nextBddNode = CalBddNodeGetNextBddNode(ptr);
00587       if (nextBddNode == bddNode) {
00588         CalBddNodePutNextBddNode(ptr, CalBddNodeGetNextBddNode(bddNode));
00589         found = 1;
00590         break;
00591       }
00592       ptr = nextBddNode;
00593     }
00594   }
00595 
00596   if (!found) {
00597     CalBddFatalMessage("Node not found in the unique table");
00598   } else {
00599     CalBddNodePutNextBddNode(bddNode, hashTable->bins[hashValue]);
00600     hashTable->bins[hashValue] = bddNode;
00601   }
00602 }
00603 
00616 unsigned long
00617 CalBddUniqueTableNumLockedNodes(Cal_BddManager_t *bddManager,
00618                                 CalHashTable_t *uniqueTableForId)
00619 {
00620   CalBddNode_t *bddNode;
00621   long i;
00622   unsigned long numLockedNodes = 0;
00623   
00624   for(i=0; i<uniqueTableForId->numBins; i++){
00625     bddNode = uniqueTableForId->bins[i];
00626     while (bddNode){
00627       numLockedNodes += CalBddNodeIsRefCountMax(bddNode);
00628       bddNode = CalBddNodeGetNextBddNode(bddNode);
00629     }
00630   }
00631   return numLockedNodes;
00632 }
00633 
00645 void
00646 CalPackNodes(Cal_BddManager_t *bddManager)
00647 {
00648   int index, id;
00649   
00650   for (index = bddManager->numVars-1; index >= 0; index--){
00651     id = bddManager->indexToId[index];
00652     CalBddPackNodesForSingleId(bddManager, id);
00653   }
00654 }
00655 
00667 void
00668 CalBddPackNodesForSingleId(Cal_BddManager_t *bddManager,
00669                            Cal_BddId_t id)
00670 {
00671   /* Need to copy the one for "AfterReorder" and suitably modify. */
00672 }
00673 
00692 void
00693 CalBddPackNodesAfterReorderForSingleId(Cal_BddManager_t *bddManager,
00694                                        int fixForwardedNodesFlag,
00695                                        int bestIndex, 
00696                                        int bottomIndex) 
00697 {
00698   /* We need to pack the nodes for this id and fix the cofactors of
00699      the upper indices.
00700      */
00701   CalBddNode_t *node, *nextBddNode, *dupNode, **oldBins;
00702   CalBddNode_t *thenBddNode, *elseBddNode, *bddNode;
00703   Cal_Bdd_t thenBdd;
00704   CalAddress_t *page;
00705   int id = bddManager->indexToId[bestIndex];
00706   CalNodeManager_t *nodeManager = bddManager->nodeManagerArray[id];
00707   CalAddress_t **oldPageList = nodeManager->pageList;
00708   int oldNumPages = nodeManager->numPages;
00709   CalHashTable_t *uniqueTableForId = bddManager->uniqueTable[id];
00710   int numPagesRequired, newSizeIndex, index, i;
00711   long oldNumBins, hashValue;
00712   
00713   
00714 #ifdef _CAL_VERBOSE
00715   fprintf(stdout,"Repacking id %3d\n", id);
00716 #endif
00717   
00718 
00719   nodeManager->freeNodeList = Cal_Nil(CalBddNode_t);
00720   nodeManager->numPages = 0;
00721   numPagesRequired = uniqueTableForId->numEntries/NUM_NODES_PER_PAGE;
00722   nodeManager->maxNumPages =
00723       2*(numPagesRequired ? numPagesRequired : 1);
00724 
00725   nodeManager->pageList = Cal_MemAlloc(CalAddress_t *,
00726                                        nodeManager->maxNumPages); 
00727   
00728   oldBins = uniqueTableForId->bins;
00729   oldNumBins = uniqueTableForId->numBins;
00730   /* Create the new set of bins */
00731   newSizeIndex =
00732       CeilLog2(uniqueTableForId->numEntries/HASH_TABLE_DEFAULT_MAX_DENSITY);
00733 
00734   if (newSizeIndex < HASH_TABLE_DEFAULT_SIZE_INDEX){
00735     newSizeIndex = HASH_TABLE_DEFAULT_SIZE_INDEX;
00736   }
00737 
00738   uniqueTableForId->sizeIndex = newSizeIndex;
00739   uniqueTableForId->numBins =  TABLE_SIZE(uniqueTableForId->sizeIndex);
00740   uniqueTableForId->maxCapacity =
00741       uniqueTableForId->numBins * HASH_TABLE_DEFAULT_MAX_DENSITY; 
00742 
00743   uniqueTableForId->bins = Cal_MemAlloc(CalBddNode_t *,
00744                                         uniqueTableForId->numBins); 
00745   if(uniqueTableForId->bins == Cal_Nil(CalBddNode_t *)){
00746     CalBddFatalMessage("out of memory");
00747   }
00748 
00749   memset((char *)uniqueTableForId->bins, 0, 
00750         uniqueTableForId->numBins*sizeof(CalBddNode_t *)); 
00751 
00752   for (i = 0; i < oldNumBins; i++){
00753     node = oldBins[i];
00754     while (node){
00755       nextBddNode = CalBddNodeGetNextBddNode(node);
00756       CalNodeManagerCreateAndDupBddNode(nodeManager, node, dupNode);
00757       thenBddNode = CalBddNodeGetThenBddNode(dupNode);
00758       elseBddNode = CalBddNodeGetElseBddNode(dupNode);
00759       hashValue = CalDoHash2(thenBddNode, elseBddNode, uniqueTableForId);
00760       CalBddNodePutNextBddNode(dupNode, uniqueTableForId->bins[hashValue]);
00761       uniqueTableForId->bins[hashValue] = dupNode;
00762       CalBddNodePutThenBddNode(node, dupNode);
00763       CalBddNodePutThenBddId(node, id);
00764       CalBddNodePutElseBddNode(node, FORWARD_FLAG);
00765       node = nextBddNode;
00766       Cal_Assert(!(CalBddNodeIsRefCountZero(dupNode)));
00767     }
00768   }
00769   
00770   if (fixForwardedNodesFlag){
00771       CalBddNode_t *requestNodeList =
00772           bddManager->uniqueTable[id]->startNode.nextBddNode;  
00773       for (bddNode = requestNodeList; bddNode; bddNode = nextBddNode){
00774         Cal_Assert(CalBddNodeIsForwarded(bddNode));
00775         nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00776         CalBddNodeGetThenBdd(bddNode, thenBdd);
00777         if (CalBddGetBddId(thenBdd) == id){
00778           if (CalBddIsForwarded(thenBdd)) {
00779             CalBddForward(thenBdd);
00780             Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
00781             CalBddNodePutThenBdd(bddNode, thenBdd);
00782           }
00783         }
00784         Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
00785       }
00786       for (index = bestIndex+1; index <= bottomIndex; index++){   
00787       int varId = bddManager->indexToId[index];
00788       requestNodeList =
00789           bddManager->uniqueTable[varId]->startNode.nextBddNode;   
00790       for (bddNode = requestNodeList; bddNode; bddNode = nextBddNode){
00791         Cal_Assert(CalBddNodeIsForwarded(bddNode));
00792         nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00793         CalBddNodeGetThenBdd(bddNode, thenBdd);
00794         if (CalBddIsForwarded(thenBdd)) {
00795           CalBddForward(thenBdd);
00796           Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
00797           CalBddNodePutThenBdd(bddNode, thenBdd);
00798         }
00799         Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
00800       }
00801     }
00802   }
00803   
00804 /* Traverse the upper indices fixing the cofactors */
00805   for (index = bestIndex-1; index >= 0; index--){
00806     CalBddReorderFixCofactors(bddManager,
00807                            bddManager->indexToId[index]); 
00808   }
00809 
00810   if (bddManager->pipelineState == CREATE){
00811     /* There are some results computed in pipeline */
00812     CalBddReorderFixProvisionalNodes(bddManager);
00813   }
00814   
00815   /* Fix the user BDDs */
00816   CalBddReorderFixUserBddPtrs(bddManager);
00817 
00818   CalBddIsForwardedTo(bddManager->varBdds[id]);
00819 
00820   /* Fix the association */
00821   CalReorderAssociationFix(bddManager);
00822   
00823   /* Free the old bins */
00824   Cal_MemFree(oldBins);
00825 
00826   uniqueTableForId->endNode = &(uniqueTableForId->startNode);
00827   uniqueTableForId->startNode.nextBddNode = NULL;
00828   if (fixForwardedNodesFlag){
00829     CalBddReorderReclaimForwardedNodes(bddManager, bestIndex+1,
00830                                     bottomIndex);
00831   }
00832   /* Free the old pages */
00833   for (i = 0; i < oldNumPages; i++){
00834     page = oldPageList[i]; 
00835     CalPageManagerFreePage(nodeManager->pageManager, page);
00836   }
00837   Cal_MemFree(oldPageList);
00838   Cal_Assert(CalCheckAllValidity(bddManager));
00839 }
00840 
00852 void
00853 CalBddPackNodesForMultipleIds(Cal_BddManager_t *bddManager,
00854                               Cal_BddId_t beginId, int numLevels)
00855 {
00856   /* We need to pack the nodes for this id and fix the cofactors of
00857      the upper indices.
00858      */
00859   int index = bddManager->idToIndex[beginId];
00860   int level, id;
00861   long i, j;
00862   CalBddNode_t *node, *nextBddNode, *dupNode, *thenBddNode;
00863   CalBddNode_t *elseBddNode, **oldBins;
00864   Cal_Bdd_t thenBdd, elseBdd;
00865   CalNodeManager_t *nodeManager;
00866   CalHashTable_t *uniqueTableForId;
00867   int someRepackingDone = 0;
00868   long oldNumBins, hashValue;
00869   int newSizeIndex;
00870 
00871 
00872   CalAddress_t *page, ***oldPageListArray, **oldPageList;
00873   int *oldNumPagesArray;
00874   int numPagesRequired;
00875   
00876   oldPageListArray = Cal_MemAlloc(CalAddress_t **, numLevels);
00877 
00878   oldNumPagesArray = Cal_MemAlloc(int, numLevels);
00879   
00880   for (level = numLevels-1; level >= 0; level--){
00881     id = bddManager->indexToId[index+level];
00882     oldNumPagesArray[level] = 0;
00883     oldPageListArray[level] = Cal_Nil(CalAddress_t *);
00884     if (CalBddIdNeedsRepacking(bddManager, id)){
00885       nodeManager = bddManager->nodeManagerArray[id];
00886       uniqueTableForId = bddManager->uniqueTable[id];
00887       oldPageListArray[level] = nodeManager->pageList;
00888       oldNumPagesArray[level] = nodeManager->numPages;
00889       nodeManager->freeNodeList = Cal_Nil(CalBddNode_t);
00890       nodeManager->numPages = 0;
00891       numPagesRequired = uniqueTableForId->numEntries/NUM_NODES_PER_PAGE;
00892       nodeManager->maxNumPages =
00893           2*(numPagesRequired ? numPagesRequired : 1);
00894       nodeManager->pageList = Cal_MemAlloc(CalAddress_t *,
00895                                            nodeManager->maxNumPages); 
00896       oldBins = uniqueTableForId->bins;
00897       oldNumBins = uniqueTableForId->numBins;
00898       /* Create the new set of bins */
00899       newSizeIndex =
00900           CeilLog2(uniqueTableForId->numEntries /
00901                    HASH_TABLE_DEFAULT_MAX_DENSITY);  
00902       if (newSizeIndex < HASH_TABLE_DEFAULT_SIZE_INDEX){
00903         newSizeIndex = HASH_TABLE_DEFAULT_SIZE_INDEX;
00904       }
00905       uniqueTableForId->sizeIndex = newSizeIndex;
00906       uniqueTableForId->numBins =  TABLE_SIZE(uniqueTableForId->sizeIndex);
00907       uniqueTableForId->maxCapacity =
00908           uniqueTableForId->numBins * HASH_TABLE_DEFAULT_MAX_DENSITY; 
00909       
00910       uniqueTableForId->bins = Cal_MemAlloc(CalBddNode_t *,
00911                                             uniqueTableForId->numBins); 
00912       if(uniqueTableForId->bins == Cal_Nil(CalBddNode_t *)){
00913         CalBddFatalMessage("out of memory");
00914       }
00915       memset((char *)uniqueTableForId->bins, 0, 
00916             uniqueTableForId->numBins*sizeof(CalBddNode_t *)); 
00917       
00918       for (i = 0; i < oldNumBins; i++){
00919         node = oldBins[i];
00920         while (node){
00921           nextBddNode = CalBddNodeGetNextBddNode(node);
00922           CalBddNodeGetThenBdd(node, thenBdd);
00923           CalBddNodeGetElseBdd(node, elseBdd);
00924           if (CalBddIsForwarded(thenBdd)){
00925             CalBddForward(thenBdd);
00926             CalBddNodePutThenBdd(node, thenBdd);
00927           }
00928           if (CalBddIsForwarded(elseBdd)){
00929             CalBddForward(elseBdd);
00930             CalBddNodePutElseBdd(node, elseBdd);
00931           }
00932           CalNodeManagerCreateAndDupBddNode(nodeManager, node, dupNode);
00933           thenBddNode = CalBddNodeGetThenBddNode(dupNode);
00934           elseBddNode = CalBddNodeGetElseBddNode(dupNode);
00935           hashValue = CalDoHash2(thenBddNode, elseBddNode, uniqueTableForId);
00936           CalBddNodePutNextBddNode(dupNode, uniqueTableForId->bins[hashValue]);
00937           uniqueTableForId->bins[hashValue] = dupNode;
00938           CalBddNodePutThenBddNode(node, dupNode);
00939           CalBddNodePutThenBddId(node, id);
00940           CalBddNodePutElseBddNode(node, FORWARD_FLAG);
00941           node = nextBddNode;
00942           Cal_Assert(!(CalBddNodeIsRefCountZero(dupNode)));
00943         }
00944       }
00945 
00946 #ifdef __FOO__
00947       /*fprintf(stdout,"Repacking id = %d, index = %d\n", id, index+level);*/
00948       /* First put all the nodes in that list */
00949       nodeList = Cal_Nil(CalBddNode_t);
00950       for (i = 0; i < uniqueTableForId->numBins; i++){
00951         node = uniqueTableForId->bins[i];
00952         while (node){
00953           nextBddNode = CalBddNodeGetNextBddNode(node);
00954           /* The "then" and "else" pointers could be forwarded */
00955           CalBddNodeGetThenBdd(node, thenBdd);
00956           CalBddNodeGetElseBdd(node, elseBdd);
00957           if (CalBddIsForwarded(thenBdd)){
00958             CalBddForward(thenBdd);
00959             CalBddNodePutThenBdd(node, thenBdd);
00960           }
00961           if (CalBddIsForwarded(elseBdd)){
00962             CalBddForward(elseBdd);
00963             CalBddNodePutElseBdd(node, elseBdd);
00964           }
00965           CalBddNodePutNextBddNode(node, nodeList);
00966           nodeList = node;
00967           node = nextBddNode;
00968         }
00969         uniqueTableForId->bins[i] = Cal_Nil(CalBddNode_t);
00970       }
00971       uniqueTableForId->numEntries = 0;
00972       
00973       for (node = nodeList; node; node = nextBddNode){
00974         nextBddNode = CalBddNodeGetNextBddNode(node);
00975         CalNodeManagerCreateAndDupBddNode(nodeManager, node, dupNode);
00976         /* Hash the dupNode */
00977         CalHashTableAddDirect(uniqueTableForId, dupNode);
00978         /* Make the original node a forwarding node */
00979         CalBddNodePutThenBddNode(node, dupNode);
00980         CalBddNodePutThenBddId(node, id);
00981         CalBddNodePutElseBddNode(node, FORWARD_FLAG);
00982       }
00983 #endif
00984       someRepackingDone = 1;
00985     }
00986     else if (someRepackingDone){ /* Still need to fix the cofactors */
00987       CalBddReorderFixCofactors(bddManager, id);
00988     }
00989   }
00990   
00991 
00992   /* Traverse the upper indices fixing the cofactors */
00993   for (i = index-1; i >= 0; i--){
00994     CalBddReorderFixCofactors(bddManager,
00995                               bddManager->indexToId[i]);
00996   }
00997 
00998   /* Fix the user BDDs */
00999   CalBddReorderFixUserBddPtrs(bddManager);
01000   if (bddManager->pipelineState == CREATE){
01001     /* There are some results computed in pipeline */
01002     CalBddReorderFixProvisionalNodes(bddManager);
01003   }
01004   /* Fix Cache Tables */
01005   (void)CalCacheTableTwoRepackUpdate(bddManager->cacheTable);
01006   
01007   for (level = numLevels - 1 ; level >= 0; level--){
01008     id = bddManager->indexToId[index+level];
01009     /* Update varBdd field of bdd manager */
01010     CalBddIsForwardedTo(bddManager->varBdds[id]);
01011     /* Fix associations */
01012     CalVarAssociationRepackUpdate(bddManager, id);
01013     /* Free the old pages */
01014     nodeManager = bddManager->nodeManagerArray[id];
01015     oldPageList = oldPageListArray[level];
01016     for (j = 0; j < oldNumPagesArray[level]; j++){
01017       page = oldPageList[j]; 
01018       CalPageManagerFreePage(nodeManager->pageManager, page);
01019     }
01020     if ((unsigned long)oldPageList) Cal_MemFree(oldPageList);
01021   }
01022   Cal_MemFree(oldPageListArray);
01023   Cal_MemFree(oldNumPagesArray);
01024 }
01025 
01026 /*---------------------------------------------------------------------------*/
01027 /* Definition of static functions                                            */
01028 /*---------------------------------------------------------------------------*/
01040 static int
01041 CeilLog2(
01042   int  number)
01043 {
01044   int num, count;
01045   for (num=number, count=0; num > 1; num >>= 1, count++);
01046   if ((1 << count) != number) count++;
01047   return count;
01048 }