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

00001 
00046 #include "calInt.h"
00047 
00048 /*---------------------------------------------------------------------------*/
00049 /* Constant declarations                                                     */
00050 /*---------------------------------------------------------------------------*/
00051 
00052 /*---------------------------------------------------------------------------*/
00053 /* Type declarations                                                         */
00054 /*---------------------------------------------------------------------------*/
00055 
00056 /*---------------------------------------------------------------------------*/
00057 /* Stucture declarations                                                     */
00058 /*---------------------------------------------------------------------------*/
00059 
00060 /*---------------------------------------------------------------------------*/
00061 /* Variable declarations                                                     */
00062 /*---------------------------------------------------------------------------*/
00063 static   CalNodeManager_t *nodeManager; 
00064 static   int freeListId;
00065 
00066 
00067 /*---------------------------------------------------------------------------*/
00068 /* Macro declarations                                                        */
00069 /*---------------------------------------------------------------------------*/
00070 /* These macros are needed because we are dealing with a new data
00071    structures of the BDD nodes */
00072 
00073 #define BddNodeIcrRefCount(f)                   \
00074 {                                               \
00075   CalBddNode_t *_bddNode = CAL_BDD_POINTER(f);  \
00076   if (_bddNode->elseBddId < CAL_MAX_REF_COUNT){ \
00077     _bddNode->elseBddId++;                      \
00078   }                                             \
00079 }
00080 
00081 #define BddNodeDcrRefCount(f) \
00082 { \
00083   CalBddNode_t *_bddNode = CAL_BDD_POINTER(f); \
00084   if ((_bddNode->elseBddId < CAL_MAX_REF_COUNT) && (_bddNode->elseBddId)){ \
00085     _bddNode->elseBddId--; \
00086   } \
00087   else if (_bddNode->elseBddId == 0){ \
00088     CalBddWarningMessage("Trying to decrement reference count below zero"); \
00089   } \
00090 }
00091 
00092 #define BddGetCofactors(bddManager, f, id, fThen, fElse)                \
00093 {                                                                       \
00094   CalBddNode_t *_bddNode = CAL_BDD_POINTER(f);                          \
00095   Cal_Assert(bddManager->idToIndex[_bddNode->thenBddId] <=              \
00096              bddManager->idToIndex[id]);                                \
00097   if (bddManager->idToIndex[_bddNode->thenBddId] ==                     \
00098       bddManager->idToIndex[id]){                                       \
00099     fThen = _bddNode->thenBddNode;                                      \
00100     fElse = _bddNode->elseBddNode;                                      \
00101   }                                                                     \
00102   else{                                                                 \
00103     fThen = fElse = f;                                                  \
00104   }                                                                     \
00105 }
00106 
00107 #define BddNodeGetThenBddNode(bddNode)                    \
00108 ((CalBddNode_t*) ((CalAddress_t)                          \
00109                   (CAL_BDD_POINTER(bddNode)->thenBddNode) \
00110                   ^ (CAL_TAG0(bddNode))))
00111 
00112 #define BddNodeGetElseBddNode(bddNode)                    \
00113 ((CalBddNode_t*) ((CalAddress_t)                          \
00114                   (CAL_BDD_POINTER(bddNode)->elseBddNode) \
00115                   ^ (CAL_TAG0(bddNode))))
00116   
00117     
00118     
00121 /*---------------------------------------------------------------------------*/
00122 /* Static function prototypes                                                */
00123 /*---------------------------------------------------------------------------*/
00124 
00125 static int UniqueTableForIdFindOrAdd(Cal_BddManager_t * bddManager, CalHashTable_t * hashTable, CalBddNode_t *thenBdd, CalBddNode_t *elseBdd, CalBddNode_t **bddPtr);
00126 static void HashTableAddDirect(CalHashTable_t * hashTable, CalBddNode_t *bddNode);
00127 static int HashTableFindOrAdd(Cal_BddManager_t *bddManager, CalHashTable_t *hashTable, CalBddNode_t *thenBdd, CalBddNode_t *elseBdd, CalBddNode_t **bddPtr);
00128 static void BddConvertDataStruct(Cal_BddManager_t *bddManager);
00129 static void BddConvertDataStructBack(Cal_BddManager_t *bddManager);
00130 static void BddReallocateNodes(Cal_BddManager_t *bddManager);
00131 static void BddExchangeAux(Cal_BddManager_t *bddManager, CalBddNode_t *f, int id, int nextId);
00132 static int CheckValidityOfNodes(Cal_BddManager_t *bddManager, long id);
00133 static void SweepVarTable(Cal_BddManager_t *bddManager, long id);
00134 static void BddExchange(Cal_BddManager_t *bddManager, long id);
00135 static void BddExchangeVarBlocks(Cal_BddManager_t *bddManager, Cal_Block parent, long blockIndex);
00136 static int BddReorderWindow2(Cal_BddManager_t *bddManager, Cal_Block block, long i);
00137 static int BddReorderWindow3(Cal_BddManager_t *bddManager, Cal_Block block, long i);
00138 static void BddReorderStableWindow3Aux(Cal_BddManager_t *bddManager, Cal_Block block, char *levels);
00139 static void BddReorderStableWindow3(Cal_BddManager_t *bddManager);
00140 static void BddSiftBlock(Cal_BddManager_t *bddManager, Cal_Block block, long startPosition, double maxSizeFactor);
00141 static void BddReorderSiftAux(Cal_BddManager_t *bddManager, Cal_Block block, Cal_Block *toSift, double maxSizeFactor);
00142 static void BddReorderSift(Cal_BddManager_t *bddManager, double maxSizeFactor);
00143 static int CeilLog2(int number);
00144 
00147 /*---------------------------------------------------------------------------*/
00148 /* Definition of exported functions                                          */
00149 /*---------------------------------------------------------------------------*/
00150 
00162 void
00163 CalBddReorderAuxDF(Cal_BddManager_t *bddManager)
00164 {
00165   CalHashTableGC(bddManager, bddManager->uniqueTable[0]);
00166   /*Cal_BddManagerGC(bddManager);Cal_Assert(CalCheckAllValidity(bddManager));*/
00167   /* If we want to check the validity, we need to garbage collect */
00168   CalInitInteract(bddManager); /* Initialize the interaction matrix
00169                                   before changing the data structure */
00170   nodeManager = CalNodeManagerInit(bddManager->pageManager2);
00171   freeListId = 1;
00172 #ifdef _CAL_QUANTIFY_
00173   quantify_start_recording_data();
00174 #endif
00175   BddConvertDataStruct(bddManager);
00176   if (bddManager->reorderTechnique == CAL_REORDER_WINDOW){
00177     BddReorderStableWindow3(bddManager);
00178   }
00179   else {
00180     BddReorderSift(bddManager, bddManager->maxSiftingGrowth);
00181   }
00182   BddReallocateNodes(bddManager);
00183   BddConvertDataStructBack(bddManager);
00184 #ifdef _CAL_QUANTIFY_
00185   quantify_stop_recording_data();
00186 #endif
00187   nodeManager->numPages = 0; /* Since these pages have already been
00188                                 freed */
00189   CalNodeManagerQuit(nodeManager);
00190   Cal_Assert(CalCheckAllValidity(bddManager));
00191   Cal_MemFree(bddManager->interact);
00192   bddManager->numReorderings++;
00193 }
00194 
00195 
00196 /*---------------------------------------------------------------------------*/
00197 /* Definition of internal functions                                          */
00198 /*---------------------------------------------------------------------------*/
00199 /*---------------------------------------------------------------------------*/
00200 /* Definition of static functions                                          */
00201 /*---------------------------------------------------------------------------*/
00202 static void
00203 NodeManagerAllocNode(Cal_BddManager_t *bddManager, CalBddNode_t **nodePtr) 
00204 {
00205   /* First check the free list of bddManager */
00206   if (nodeManager->freeNodeList){
00207     *nodePtr = nodeManager->freeNodeList;
00208     nodeManager->freeNodeList =
00209         ((CalBddNode_t *)(*nodePtr))->nextBddNode;
00210   }
00211   else{
00212     if (freeListId < bddManager->numVars){
00213       /* Find the next id with free list */
00214       for (; freeListId <= bddManager->numVars; freeListId++){
00215         CalNodeManager_t *nodeManagerForId =
00216             bddManager->nodeManagerArray[freeListId]; 
00217         if (nodeManagerForId->freeNodeList){
00218           *nodePtr = nodeManagerForId->freeNodeList;
00219           nodeManagerForId->freeNodeList = (CalBddNode_t *)0;
00220           nodeManager->freeNodeList =
00221               ((CalBddNode_t *)(*nodePtr))->nextBddNode;
00222           break;
00223         }
00224       }
00225     }
00226   }
00227   if (!(*nodePtr)){
00228     /* Create a new page */
00229     CalBddNode_t *_freeNodeList, *_nextNode, *_node;                        
00230     _freeNodeList =                                                         
00231         (CalBddNode_t *)CalPageManagerAllocPage(nodeManager->pageManager);  
00232     for(_node = _freeNodeList + NUM_NODES_PER_PAGE - 1, _nextNode =0;       
00233         _node != _freeNodeList; _nextNode = _node--){                       
00234       _node->nextBddNode = _nextNode;                                       
00235     }                                                                       
00236     nodeManager->freeNodeList = _freeNodeList + 1;                          
00237     *nodePtr = _node;
00238     if (nodeManager->numPages == nodeManager->maxNumPages){             
00239       nodeManager->maxNumPages *= 2;                                      
00240       nodeManager->pageList =                                            
00241           Cal_MemRealloc(CalAddress_t *, nodeManager->pageList, 
00242                          nodeManager->maxNumPages);                       
00243     }                                                                       
00244     nodeManager->pageList[nodeManager->numPages++] =
00245         (CalAddress_t *)_freeNodeList;     
00246   }
00247 }
00248 
00261 static int
00262 UniqueTableForIdFindOrAdd(Cal_BddManager_t * bddManager,
00263                           CalHashTable_t * hashTable,
00264                           CalBddNode_t *thenBdd,
00265                           CalBddNode_t *elseBdd,
00266                           CalBddNode_t **bddPtr)
00267 {
00268   int found = 0; 
00269   if (thenBdd == elseBdd){
00270     *bddPtr = thenBdd;
00271     found = 1;
00272   }
00273   else if(CalBddNodeIsOutPos(thenBdd)){
00274     found = HashTableFindOrAdd(bddManager, hashTable, thenBdd, elseBdd, bddPtr);
00275   }
00276   else{
00277     found = HashTableFindOrAdd(bddManager, hashTable,
00278                                CalBddNodeNot(thenBdd),
00279                                CalBddNodeNot(elseBdd), bddPtr); 
00280     *bddPtr = CalBddNodeNot(*bddPtr);
00281   }
00282   if (!found) bddManager->numNodes++;
00283   return found;
00284 }
00285 
00297 static void
00298 HashTableAddDirect(CalHashTable_t * hashTable, CalBddNode_t *bddNode)
00299 {
00300   int hashValue;
00301   CalBddNode_t *thenBddNode, *elseBddNode;
00302 
00303   hashTable->numEntries++;
00304   if(hashTable->numEntries >= hashTable->maxCapacity){
00305     CalHashTableRehash(hashTable, 1);
00306   }
00307   thenBddNode = bddNode->thenBddNode;
00308   Cal_Assert(CalBddNodeIsOutPos(thenBddNode));
00309   elseBddNode = bddNode->elseBddNode;
00310   hashValue = CalDoHash2(thenBddNode, elseBddNode, hashTable);
00311   bddNode->nextBddNode = hashTable->bins[hashValue];
00312   hashTable->bins[hashValue] = bddNode;
00313 }
00314 
00315 
00327 static int
00328 HashTableFindOrAdd(Cal_BddManager_t *bddManager, CalHashTable_t
00329                    *hashTable,  CalBddNode_t *thenBdd,
00330                    CalBddNode_t *elseBdd, CalBddNode_t **bddPtr) 
00331 {
00332   CalBddNode_t *ptr;
00333   int hashValue;
00334   
00335   Cal_Assert(CalBddNodeIsOutPos(thenBdd));
00336   hashValue = CalDoHash2(thenBdd, elseBdd, hashTable);
00337   for (ptr = hashTable->bins[hashValue]; ptr; ptr = ptr->nextBddNode){
00338     if ((ptr->thenBddNode == thenBdd) &&
00339         (ptr->elseBddNode == elseBdd)){
00340       *bddPtr = ptr;
00341       return 1;
00342     }
00343   }
00344   hashTable->numEntries++;
00345   if(hashTable->numEntries > hashTable->maxCapacity){
00346     CalHashTableRehash(hashTable,1);
00347     hashValue = CalDoHash2(thenBdd, elseBdd, hashTable);
00348   }
00349 
00350   NodeManagerAllocNode(bddManager, &ptr);
00351 
00352   ptr->thenBddNode = thenBdd;
00353   ptr->elseBddNode = elseBdd;
00354   ptr->nextBddNode = hashTable->bins[hashValue];
00355   ptr->thenBddId = hashTable->bddId;
00356   ptr->elseBddId = 0;
00357   hashTable->bins[hashValue] = ptr;
00358   *bddPtr = ptr;
00359   return 0;
00360 }
00361 
00362 
00375 static void
00376 BddConvertDataStruct(Cal_BddManager_t *bddManager)
00377 {
00378   CalBddNode_t *bddNode, *thenBddNode, *elseBddNode,
00379       *next = Cal_Nil(CalBddNode_t); 
00380   CalBddNode_t *last;
00381   long numBins;
00382   int i, refCount, id, index;
00383   long oldNumEntries;
00384   CalHashTable_t *uniqueTableForId;
00385 
00386   if (bddManager->numPeakNodes < bddManager->numNodes){
00387     bddManager->numPeakNodes = bddManager->numNodes;
00388   }
00389 
00390   for(index = 0; index < bddManager->numVars; index++){
00391     id = bddManager->indexToId[index];
00392     uniqueTableForId = bddManager->uniqueTable[id];
00393     oldNumEntries = uniqueTableForId->numEntries;
00394     numBins = uniqueTableForId->numBins;
00395     for(i = 0; i < numBins; i++){
00396       last = NULL;
00397       bddNode = uniqueTableForId->bins[i];
00398       while(bddNode != Cal_Nil(CalBddNode_t)){
00399         next = CalBddNodeGetNextBddNode(bddNode);
00400         CalBddNodeGetRefCount(bddNode, refCount);
00401         thenBddNode = CalBddNodeGetThenBddNode(bddNode);
00402         elseBddNode = CalBddNodeGetElseBddNode(bddNode);
00403         if(refCount == 0){
00404           if (last == NULL){
00405             uniqueTableForId->bins[i] = next;
00406           }
00407           else{
00408             last->nextBddNode = next;
00409           }
00410           CalBddNodeDcrRefCount(CAL_BDD_POINTER(thenBddNode));
00411           CalBddNodeDcrRefCount(CAL_BDD_POINTER(elseBddNode));
00412           CalNodeManagerFreeNode(nodeManager, bddNode);
00413           uniqueTableForId->numEntries--;
00414         }
00415         else {
00416           bddNode->thenBddId = id;
00417           bddNode->elseBddId = refCount;
00418           bddNode->nextBddNode = next;
00419           bddNode->thenBddNode = thenBddNode;
00420           bddNode->elseBddNode = elseBddNode;
00421           last = bddNode; 
00422         }
00423         bddNode = next;
00424       }
00425     }
00426     if ((uniqueTableForId->numBins > uniqueTableForId->numEntries) &&
00427         (uniqueTableForId->sizeIndex > HASH_TABLE_DEFAULT_SIZE_INDEX)){
00428       CalHashTableRehash(uniqueTableForId, 0);
00429     }
00430     bddManager->numNodes -= oldNumEntries - uniqueTableForId->numEntries;
00431     bddManager->numNodesFreed += oldNumEntries - uniqueTableForId->numEntries;
00432   }
00433   id = 0;
00434   uniqueTableForId = bddManager->uniqueTable[id];
00435   numBins = uniqueTableForId->numBins;
00436   for(i = 0; i < numBins; i++){
00437     bddNode = uniqueTableForId->bins[i];
00438     while(bddNode != Cal_Nil(CalBddNode_t)){
00439       next = CalBddNodeGetNextBddNode(bddNode);
00440       CalBddNodeGetRefCount(bddNode, refCount);
00441       Cal_Assert(refCount);
00442       thenBddNode = CalBddNodeGetThenBddNode(bddNode);
00443       elseBddNode = CalBddNodeGetElseBddNode(bddNode);
00444       bddNode->thenBddId = id;
00445       bddNode->elseBddId = refCount;
00446       bddNode->nextBddNode = next;
00447       bddNode->thenBddNode = thenBddNode;
00448       bddNode->elseBddNode = elseBddNode;
00449       bddNode = next;
00450     }
00451   }
00452   bddNode = bddManager->bddOne.bddNode;
00453   CalBddNodeGetRefCount(bddNode, refCount);
00454   Cal_Assert(refCount);
00455   thenBddNode = CalBddNodeGetThenBddNode(bddNode);
00456   elseBddNode = CalBddNodeGetElseBddNode(bddNode);
00457   bddNode->thenBddId = id;
00458   bddNode->elseBddId = refCount;
00459   bddNode->nextBddNode = next;
00460   bddNode->thenBddNode = thenBddNode;
00461   bddNode->elseBddNode = elseBddNode;
00462 }
00463 
00464 
00477 static void
00478 BddConvertDataStructBack(Cal_BddManager_t *bddManager)
00479 {
00480   Cal_Bdd_t thenBdd, elseBdd;
00481   
00482   CalBddNode_t *bddNode, *nextBddNode, **bins;
00483   long numBins;
00484   int i, id, index;
00485   CalHashTable_t *uniqueTableForId;
00486   uniqueTableForId = bddManager->uniqueTable[0];
00487   numBins = uniqueTableForId->numBins;
00488   bins = uniqueTableForId->bins;
00489   for(i = 0; i < numBins; i++) {
00490     for(bddNode = bins[i];
00491         bddNode != Cal_Nil(CalBddNode_t);
00492         bddNode = nextBddNode) {
00493       nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00494       CalBddNodePutRefCount(bddNode, bddNode->elseBddId);
00495       bddNode->thenBddId = CAL_BDD_POINTER(bddNode->thenBddNode)->thenBddId;
00496       bddNode->elseBddId = CAL_BDD_POINTER(bddNode->elseBddNode)->thenBddId;
00497     }
00498   }
00499   for(index = 0; index < bddManager->numVars; index++){
00500     id = bddManager->indexToId[index];
00501     uniqueTableForId = bddManager->uniqueTable[id];
00502     numBins = uniqueTableForId->numBins;
00503     bins = uniqueTableForId->bins;
00504     for(i = 0; i < numBins; i++) {
00505       for(bddNode = bins[i];
00506           bddNode != Cal_Nil(CalBddNode_t);
00507           bddNode = nextBddNode) {
00508         nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00509         CalBddNodePutRefCount(bddNode, bddNode->elseBddId);
00510         bddNode->thenBddId = CAL_BDD_POINTER(bddNode->thenBddNode)->thenBddId;
00511         bddNode->elseBddId = CAL_BDD_POINTER(bddNode->elseBddNode)->thenBddId;
00512       Cal_Assert(!CalBddNodeIsForwarded(bddNode));
00513       Cal_Assert(!CalBddNodeIsRefCountZero(bddNode));
00514       CalBddNodeGetThenBdd(bddNode, thenBdd);
00515       CalBddNodeGetElseBdd(bddNode, elseBdd);
00516       Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
00517       Cal_Assert(CalBddIsForwarded(elseBdd) == 0);
00518       }
00519     }
00520   }
00521   bddNode = bddManager->bddOne.bddNode;
00522   CalBddNodePutRefCount(bddNode, bddNode->elseBddId);
00523   bddNode->thenBddId = 0;
00524   bddNode->elseBddId = 0;
00525 }
00526 
00527 #ifdef _FOO_
00528 
00539 static void
00540 BddReallocateNodesInPlace(Cal_BddManager_t *bddManager)
00541 {
00542   Cal_Address_t  *pageSegment;
00543   CalPageManager_t *pageManager;
00544   CalHashTable_t *uniqueTable;
00545   CalNodeManager_t *nodeManager;
00546   int index, id, i, pageCounter, numUsefulSegments, segmentCounter;
00547   
00548   /* Initialize and set up few things */
00549   pageManager = bddManager->pageManager;
00550   uniqueTable = bddManager->uniqueTable;
00551   for (id = 1; id <= bddManager->numVars; id++){
00552     numPagesRequired =
00553         uniqueTable[id]->numEntries/NUM_NODES_PER_PAGE+1;
00554     nodeManager = uniqueTable[id]->nodeManager;
00555     /* Clear out the page list of the node manager */
00556     for (i=0; i<nodeManager->maxNumPages; i++){
00557       nodeManager->pageList[i] = 0;
00558     }
00559     nodeManager->freeNodeList = (CalBddNode_t *)0;
00560     nodeManager->numPages = numPagesRequired;
00561     Cal_Assert(nodeManager->maxNumPages >= numPagesRequired);
00562     for (i = 0; i<numPagesRequired; i++){
00563       if (++pageCounter ==
00564               pageManager->numPagesArray[segmentCounter]){
00565         pageCounter = 0;
00566         segmentCounter++;
00567         pageSegment = pageManager->pageSegmentArray[segmentCounter];
00568       }
00569       nodeManager->pageList[i] = pageSegment[pageCounter];
00570     }
00571   }
00572   numUsefulSegments = segmentCounter+1;
00573   numUsefulPagesInLastSegment = pageCounter+1;
00574   
00575   /* Traverse all the nodes belonging in each page */
00576   /* Put the destination addresses in the next pointer */
00577   for (numSegment=0; numSegment < pageManager->numSegments; 
00578        numSegment++){
00579     for (numPage = 0, page = pageManager->pageSegmentArray[numSegment]; 
00580          numPage < pageManager->numPagesArray[numSegment];
00581          page += PAGE_SIZE, numPage++){
00582       for (bddNode = (CalBddNode_t*) page, numNode = 0;
00583            numNode < NUM_NODES_PER_PAGE; numNode++, bddNode += 1){
00584         /* If the node is not useful, continue */
00585         if (bddNode->elseBddId == 0) continue; 
00586         /* Find out the destination address */
00587         bddId = bddNode->thenBddId;
00588         nodeCounter[bddId]++;
00589         if (nodeCounter[bddId] == NUM_NODES_PER_PAGE){
00590           pageCounter[bddId]++;
00591           nodePointerArray[bddId] =
00592               pageListArray[bddId][pageCounter[bddId]];
00593           nodeCounter[bddId] = 0;
00594         }
00595         bddNode->nextBddNode = nodePointerArray[bddId];
00596         nodePointerArray[bddId] += 1;
00597       }
00598     }
00599   }
00600   /* Traverse all the nodes belonging in each page */
00601   /* Update the contents */
00602   for (numSegment=0; numSegment < pageManager->totalNumSegments; 
00603        numSegment++){
00604     for (numPage = 0, page = pageManager->pageSegmentArray[numSegment]; 
00605          numPage < pageManager->numPagesArray[numSegment];
00606          page += PAGE_SIZE, numPage++){
00607       for (bddNode = (CalBddNode_t*) page, numNode = 0;
00608            numNode < NUM_NODES_PER_PAGE; numNode++, bddNode += 1){
00609         /* If the node is not useful, continue */
00610         if (bddNode->elseBddId == 0) continue; 
00611         /* If the node has been visited, continue */
00612         if ((CalAddress_t)bddNode->nextBddNode & 01) continue;
00613         /* If the nodes is supposed to remain at the same place,
00614            update the then and else pointers and continue */
00615         if (((CalAddress_t) bddNode->nextBddNode &~01) ==
00616             ((CalAddress_t) bddNode & ~01)){
00617           CalBddNodeUpdatebddNode(bddNode);
00618           continue;
00619         }
00620         origNode = bddNode; /* Remember the address */
00621         /* Update the contents */
00622         thenBddNode = bddNode->thenBddNode;
00623         elseBddNode = bddNode->elseBddNode;
00624         thenBddId = bddNode->thenBddId;
00625         elseBddId = bddNode->elseBddId;
00626         do{
00627           thenBddNode = UpdateThenBddNode(thenBddNode);
00628           elseBddNode = UpdateElseBddNode(elseBddNode);
00629           destinationNode = bddNode->nextBddNode;
00630           /* Mark the node visited */
00631           bddNode->nextBddNode = (CalBddNode_t *)
00632               ((CalAddress_t)bddNode->nextBddNode | 01);
00633           thenBddNode2 = destinationNode->thenBddNode;
00634           elseBddNode2 = destinationNode->elseBddNode;
00635           thenBddId2 = destinationNode->thenBddId;
00636           elseBddId2 = destinationNode->elseBddId;
00637           destinationNode->thenBddNode = thenBddNode;
00638           destinationNode->elseBddNode = elseBddNode;
00639           destinationNode->thenBddId = thenBddId;
00640           destinationNode->elseBddId = elseBddId;
00641           bddNode = destinationNode;
00642           thenBddNode = thenBddNode2;
00643           elseBddNode = elseBddNode2;
00644           thenBddId = thenBddId2;
00645           elseBddId = elseBddId2;
00646         } while ((elseBddId != 0) && (bddNode != origNode) &&
00647                  !((CalAddress_t)(bddNode->nextBddNode) & 01));
00648       }
00649     }
00650   }
00651   /* Fix the handles to the nodes being moved */
00652   for (id = 1; id <= bddManager->numVars; id++){
00653     /* Fix the varBdd array */
00654   }
00655 /* Need to update the handles to the nodes being moved */
00656   if (bddManager->pipelineState == CREATE){
00657     /* There are some results computed in pipeline */
00658     CalBddReorderFixProvisionalNodesAfterReallocation(bddManager);
00659   }
00660   
00661   /* Fix the user BDDs */
00662   CalBddReorderFixUserBddPtrsAfterReallocation(bddManager);
00663 
00664   /* Fix the association */
00665   CalReorderAssociationFixAfterReallocation(bddManager);
00666 
00667   Cal_Assert(CalCheckAssoc(bddManager));
00668   
00669 
00670   /* Update the next pointers */
00671   /* Since the pages for the ids are distributed in the uniform
00672      manner, we can scan the pages on id by id basis without any
00673      disadvantage */
00674   for (id = 1; id <= bddManager->numVars; id++){
00675     nodeManager = uniqueTable[id]->nodeManager;
00676     freeNodeList = Cal_Nil(CalBddNode_t);
00677     for (i=0; i<nodeManager->numPages; i++){
00678       page = nodeManager->pageList[i];
00679       for (bddNode = (CalBddNode_t*) page, numNode = 0;
00680            numNode < NUM_NODES_PER_PAGE; numNode++, bddNode += 1){
00681         /* If the node is not useful, put it in the free list */
00682         if ((bddNode->elseBddId == 0) || (bddNode->elseBddNode == 0)){
00683           bddNode->nextBddNode = freeNodeList;
00684           freeNodeList = bddNode;
00685         }
00686       }
00687     }
00688     nodeManager->freeNodeList = freeNodeList;
00689   }
00690   /* We should put the unused pages in the free page list */
00691   pageSegment = pageManager->pageSegmentArray[numUsefulSegments-1];
00692   for (pageCounter = numUsefulPagesInLastSegment;
00693        pageCounter < pageSegment->numPages ; pageCounter++){
00694     CalPageManagerFreePage(pageManager, pageSegment[pageCounter]);
00695   }
00696   /* We have to free up the unnecessary page segments;*/
00697   for (i = numUsefulSegments; i < pageManager->numSegments; i++){
00698     free(pageManager->pageSegmentArray[i]);
00699     pageManager->pageSegmentArray[i] = 0;
00700   }
00701   pageManager->numSegments = numUsefulSegments;
00702 }
00714 void
00715 CalAlignCollisionChains(Cal_BddManager_t *bddManager)
00716 {
00717   /* First find out the pages corresponding to each variable */
00718   Cal_Address_t ***pageListArray = Cal_MemAlloc(Cal_Address_t **,
00719                                                 bddManager->numVars+1);
00720   for (id = 1; id <= bddManager->numVars; id++){
00721     nodeManager = bddManager->nodeManagerArray[id];
00722     numPages = nodeManager->numPages;
00723     pageListArray[id] = Cal_MemAlloc(Cal_Address_t *, numPages);
00724     for (i=0; i<numPages; i++){
00725       pageListArray[id][i] = nodeManager->pageList[i];
00726     }
00727   }
00728     
00729   /* Bottom up traversal */
00730   for (index = bddManager->numVars-1; index >= 0; index--){
00731     id = bddManager->indexToId[index];
00732     uniqueTableForId = bddManager->uniqueTable[id];
00733     nodeManager = uniqueTableForId->nodeManager;
00734     /* Calculate the collision lengths */
00735     collisionLengthArray = CalculateCollisionLength(uniqueTableForId);
00736     /* Initialize the bins */
00737     bins = uniqueTableForId->bins;
00738     numBins = uniqueTableForId->numBins;
00739     numNodes = 0;
00740     pageNum = 0;
00741     for (i=0; i<numBins; i++){
00742       numNodes += collisionLengthArray[i];
00743       if (numNodes < NUM_NODES_PER_PAGE){
00744         nodePointer[i] += collisionLengthArray[i];
00745       }
00746       else if (numNodes == NUM_NODES_PER_PAGE){
00747         nodePointer[i] = pageListArray[id][++pageNum];
00748         numNodes = 0;
00749       }
00750       else {
00751         /* put the rest of the nodes from this page in a free list */
00752         nodePointer[i]->nextBddNode = nodeManager->freeNodeList;
00753         nodeManager->freeNodeList = nodePointer;
00754         nodePointer[i] = pageListArray[id][++pageNum]+collisionLengthArray[i];
00755         numNodes = collisionLengthArray[i];
00756       }
00757     }
00758   }
00759 }
00760 #endif
00761 
00773 static void
00774 BddReallocateNodes(Cal_BddManager_t *bddManager)
00775 {
00776   int i;
00777   int index;
00778   CalNodeManager_t *nodeManager;
00779   CalPageManager_t *pageManager;
00780   int numSegments;
00781   CalAddress_t **pageSegmentArray;
00782   
00783   pageManager = bddManager->pageManager2;
00784   numSegments = pageManager->numSegments;
00785   pageSegmentArray = pageManager->pageSegmentArray;
00786   
00787   /* Reinitialize the page manager */
00788   pageManager->totalNumPages = 0;
00789   pageManager->numSegments = 0;
00790   pageManager->maxNumSegments = MAX_NUM_SEGMENTS;
00791   pageManager->pageSegmentArray 
00792       = Cal_MemAlloc(CalAddress_t *, pageManager->maxNumSegments);
00793   pageManager->freePageList = Cal_Nil(CalAddress_t);
00794   
00795   /* Do a bottom up traversal */
00796 
00797   for (index = bddManager->numVars-1; index >= 0; index--){
00798     int id;
00799     CalHashTable_t *uniqueTableForId;
00800     int numPagesRequired, newSizeIndex;
00801     CalBddNode_t *bddNode, *dupNode, *thenNode, *elseNode, **oldBins;
00802     long hashValue, oldNumBins;
00803     
00804     id = bddManager->indexToId[index];
00805     uniqueTableForId = bddManager->uniqueTable[id];
00806     nodeManager = bddManager->nodeManagerArray[id];
00807     oldBins = uniqueTableForId->bins;
00808     oldNumBins = uniqueTableForId->numBins;
00809     nodeManager->freeNodeList = Cal_Nil(CalBddNode_t);
00810     nodeManager->numPages = 0;
00811     numPagesRequired =
00812         uniqueTableForId->numEntries/NUM_NODES_PER_PAGE;
00813     nodeManager->maxNumPages =
00814         2*(numPagesRequired ? numPagesRequired : 1);
00815     Cal_MemFree(nodeManager->pageList);
00816     nodeManager->pageList = Cal_MemAlloc(CalAddress_t *,
00817                                          nodeManager->maxNumPages); 
00818     /* Create the new set of bins */
00819     newSizeIndex =
00820         CeilLog2(uniqueTableForId->numEntries/HASH_TABLE_DEFAULT_MAX_DENSITY);
00821     if (newSizeIndex < HASH_TABLE_DEFAULT_SIZE_INDEX){
00822       newSizeIndex = HASH_TABLE_DEFAULT_SIZE_INDEX;
00823     }
00824     uniqueTableForId->sizeIndex = newSizeIndex;
00825     uniqueTableForId->numBins =  TABLE_SIZE(uniqueTableForId->sizeIndex);
00826     uniqueTableForId->maxCapacity =
00827         uniqueTableForId->numBins * HASH_TABLE_DEFAULT_MAX_DENSITY; 
00828     
00829     uniqueTableForId->bins = Cal_MemAlloc(CalBddNode_t *,
00830                                           uniqueTableForId->numBins); 
00831     memset((char *)uniqueTableForId->bins, 0, 
00832            uniqueTableForId->numBins*sizeof(CalBddNode_t *)); 
00833     for (i=0; i<oldNumBins; i++){
00834       for (bddNode = oldBins[i]; bddNode; bddNode = bddNode->nextBddNode){ 
00835         CalNodeManagerAllocNode(nodeManager, dupNode);
00836         thenNode = bddNode->thenBddNode;
00837         CalBddNodeIsForwardedTo(thenNode);
00838         Cal_Assert(thenNode);
00839         Cal_Assert(!CalBddNodeIsForwarded(thenNode));
00840         elseNode = bddNode->elseBddNode;
00841         CalBddNodeIsForwardedTo(elseNode);
00842         Cal_Assert(elseNode);
00843         Cal_Assert(!CalBddNodeIsForwarded(CAL_BDD_POINTER(elseNode)));
00844         Cal_Assert(bddManager->idToIndex[bddNode->thenBddId] <
00845                    bddManager->idToIndex[thenNode->thenBddId]); 
00846         Cal_Assert(bddManager->idToIndex[bddNode->thenBddId] <
00847                    bddManager->idToIndex[CAL_BDD_POINTER(elseNode)->thenBddId]);
00848         dupNode->thenBddNode = thenNode;
00849         dupNode->elseBddNode = elseNode;
00850         dupNode->thenBddId = bddNode->thenBddId;
00851         dupNode->elseBddId = bddNode->elseBddId;
00852         hashValue = CalDoHash2(thenNode, elseNode, uniqueTableForId);
00853         dupNode->nextBddNode = uniqueTableForId->bins[hashValue];
00854         uniqueTableForId->bins[hashValue] = dupNode;
00855         bddNode->thenBddNode = dupNode;
00856         bddNode->elseBddNode = (CalBddNode_t *)0;
00857         bddNode->thenBddId = id;
00858         Cal_Assert(bddManager->idToIndex[dupNode->thenBddId] <
00859                    bddManager->idToIndex[thenNode->thenBddId]); 
00860         Cal_Assert(bddManager->idToIndex[dupNode->thenBddId] <
00861                    bddManager->idToIndex[CAL_BDD_POINTER(elseNode)->thenBddId]);
00862       }
00863     }
00864     Cal_MemFree(oldBins);
00865     CalBddIsForwardedTo(bddManager->varBdds[id]);
00866   }
00867 
00868   if (bddManager->pipelineState == CREATE){
00869     /* There are some results computed in pipeline */
00870     CalBddReorderFixProvisionalNodes(bddManager);
00871   }
00872   
00873   /* Fix the user BDDs */
00874   CalBddReorderFixUserBddPtrs(bddManager);
00875 
00876   /* Fix the association */
00877   CalReorderAssociationFix(bddManager);
00878 
00879   Cal_Assert(CalCheckAssoc(bddManager));
00880   
00881   /* Free the page manager related stuff*/
00882   for(i = 0; i < numSegments; i++){
00883     free(pageSegmentArray[i]);
00884   }
00885   Cal_MemFree(pageSegmentArray);
00886 }
00887 
00888 
00900 static void
00901 BddExchangeAux(Cal_BddManager_t *bddManager, CalBddNode_t *f,
00902                int id, int nextId)
00903 {
00904   CalBddNode_t *f0, *f1;
00905   CalBddNode_t *f00, *f01, *f10, *f11;
00906   CalBddNode_t *newF0, *newF1;
00907   int f0Found, f1Found;
00908   int fIndex;
00909   
00910   f0 = f->elseBddNode;
00911   f1 = f->thenBddNode;
00912 
00913   if (CAL_BDD_POINTER(f0)->thenBddId == nextId){
00914     f00 = BddNodeGetElseBddNode(f0);
00915     f01 = BddNodeGetThenBddNode(f0);
00916   }
00917   else {
00918     f00 = f01 = f0;
00919   }
00920   if (CAL_BDD_POINTER(f1)->thenBddId == nextId){
00921     f10 = BddNodeGetElseBddNode(f1);
00922     f11 = BddNodeGetThenBddNode(f1);
00923   }
00924   else {
00925     f10 = f11 = f1;
00926   }
00927   
00928   if (f00 == f10){
00929     newF0 = f00;
00930     f0Found = 1;
00931   }
00932   else{
00933     f0Found = UniqueTableForIdFindOrAdd(bddManager,
00934                                         bddManager->uniqueTable[id], f10,
00935                                         f00, &newF0);
00936   }
00937   BddNodeIcrRefCount(newF0);
00938   if (f01 == f11){
00939     newF1 = f11;
00940     f1Found = 1;
00941   }
00942   else{
00943     f1Found = UniqueTableForIdFindOrAdd(bddManager,
00944                                         bddManager->uniqueTable[id], f11,
00945                                         f01, &newF1);
00946   }
00947   BddNodeIcrRefCount(newF1);
00948 
00949   f->thenBddId = nextId;
00950   f->elseBddNode = newF0;
00951   f->thenBddNode = newF1;
00952 
00953   fIndex = bddManager->idToIndex[id];
00954   Cal_Assert(fIndex <
00955              bddManager->idToIndex[CAL_BDD_POINTER(f00)->thenBddId]);
00956   Cal_Assert(fIndex <
00957              bddManager->idToIndex[CAL_BDD_POINTER(f10)->thenBddId]);
00958   Cal_Assert(fIndex <
00959              bddManager->idToIndex[CAL_BDD_POINTER(f01)->thenBddId]);
00960   Cal_Assert(fIndex <
00961              bddManager->idToIndex[CAL_BDD_POINTER(f11)->thenBddId]);
00962   Cal_Assert(CAL_BDD_POINTER(f00)->thenBddId != nextId);
00963   Cal_Assert(CAL_BDD_POINTER(f01)->thenBddId != nextId);
00964   Cal_Assert(CAL_BDD_POINTER(f10)->thenBddId != nextId);
00965   Cal_Assert(CAL_BDD_POINTER(f11)->thenBddId != nextId);
00966   
00967   if (!f0Found){
00968     BddNodeIcrRefCount(f00);
00969     BddNodeIcrRefCount(f10);
00970   }
00971 
00972   if (!f1Found){
00973     BddNodeIcrRefCount(f01);
00974     BddNodeIcrRefCount(f11);
00975   }
00976 
00977   BddNodeDcrRefCount(f0);
00978   BddNodeDcrRefCount(f1);
00979 }
00980 
00992 static int
00993 CheckValidityOfNodes(Cal_BddManager_t *bddManager, long id)
00994 {
00995 #ifndef NDEBUG
00996   CalHashTable_t *table = bddManager->uniqueTable[id];
00997   int i;
00998   CalBddNode_t *bddNode;
00999   int index = bddManager->idToIndex[id];
01000   for(i = 0; i < table->numBins; ++i){
01001     for (bddNode = table->bins[i]; bddNode; bddNode = bddNode->nextBddNode){
01002       int thenIndex = bddManager->idToIndex[bddNode->thenBddNode->thenBddId];
01003       int elseIndex =
01004         bddManager->idToIndex[CAL_BDD_POINTER(bddNode->elseBddNode)->thenBddId]; 
01005       assert((thenIndex > index) && (elseIndex > index));
01006     }
01007   }
01008 #endif
01009   return 1;
01010 }
01011 
01023 static void
01024 SweepVarTable(Cal_BddManager_t *bddManager, long id)
01025 {
01026   CalHashTable_t *table = bddManager->uniqueTable[id];
01027   long numNodesFreed, oldNumEntries;
01028   CalBddNode_t **ptr, *bddNode;
01029   int i;
01030   
01031   oldNumEntries = table->numEntries;
01032   for(i = 0; i < table->numBins; ++i){
01033     for (ptr = &table->bins[i], bddNode = *ptr; bddNode;
01034          bddNode = *ptr){
01035       if (bddNode->elseBddId == 0){
01036         *ptr = bddNode->nextBddNode;
01037         CalNodeManagerFreeNode(nodeManager, bddNode);
01038         BddNodeDcrRefCount(bddNode->thenBddNode);
01039         BddNodeDcrRefCount(bddNode->elseBddNode);
01040         table->numEntries--;
01041       }
01042       else{
01043         ptr = &bddNode->nextBddNode;
01044       }
01045     }
01046   }
01047   numNodesFreed = oldNumEntries - table->numEntries;
01048   bddManager->numNodes -= numNodesFreed;
01049   bddManager->numNodesFreed += numNodesFreed;
01050 }
01051 
01052 
01064 static void
01065 BddExchange(Cal_BddManager_t *bddManager, long id)
01066 {
01067   Cal_BddId_t  nextId;
01068   CalBddNode_t **ptr, *bddNode, *nodeList;
01069   CalHashTable_t *table, *nextTable;
01070   Cal_BddIndex_t index, nextIndex;
01071   int i;
01072   CalBddNode_t  *f1, *f2;
01073   CalAssociation_t *p;
01074   CalNodeManager_t *nodeManager;
01075   
01076   index = bddManager->idToIndex[id];
01077   nextIndex = index+1;
01078   nextId = bddManager->indexToId[nextIndex];
01079 
01080   if (CalTestInteract(bddManager, id, nextId)){
01081     bddManager->numSwaps++;
01082     nodeManager = bddManager->nodeManagerArray[id];
01083     table = bddManager->uniqueTable[id];
01084     nextTable = bddManager->uniqueTable[nextId];
01085     nodeList = (CalBddNode_t*)0;
01086     for(i = 0; i < table->numBins; i++){
01087       for (ptr = &table->bins[i], bddNode = *ptr; bddNode;
01088            bddNode = *ptr){
01089         Cal_Assert(bddNode->elseBddId != 0);
01090         f1 = bddNode->elseBddNode;
01091         f2 = bddNode->thenBddNode;
01092         if ((CAL_BDD_POINTER(f1)->thenBddId != nextId) &&
01093             (CAL_BDD_POINTER(f2)->thenBddId != nextId)){ 
01094           ptr = &bddNode->nextBddNode;
01095         }
01096         else{
01097           *ptr = bddNode->nextBddNode;
01098           bddNode->nextBddNode = nodeList;
01099           nodeList = bddNode;
01100         }
01101       }
01102     }
01103     for (bddNode = nodeList; bddNode ; bddNode = nodeList){
01104       BddExchangeAux(bddManager, bddNode, id, nextId);
01105       nodeList = bddNode->nextBddNode;
01106       HashTableAddDirect(nextTable, bddNode);
01107       table->numEntries--;
01108     }
01109     SweepVarTable(bddManager, nextId);
01110   }
01111   else {
01112     bddManager->numTrivialSwaps++;
01113   }
01114   
01115   CalFixupAssoc(bddManager, id, nextId, bddManager->tempAssociation);
01116   for(p = bddManager->associationList; p; p = p->next){
01117     CalFixupAssoc(bddManager, id, nextId, p);
01118   }
01119 
01120   bddManager->idToIndex[id] = nextIndex;
01121   bddManager->idToIndex[nextId] = index;
01122   bddManager->indexToId[index] = nextId;
01123   bddManager->indexToId[nextIndex] = id;
01124 
01125   Cal_Assert(CheckValidityOfNodes(bddManager, id));
01126   Cal_Assert(CheckValidityOfNodes(bddManager, nextId));
01127   Cal_Assert(CalCheckAssoc(bddManager));
01128 #ifdef _CAL_VERBOSE
01129   /*fprintf(stdout,"Variable order after swap:\n");*/
01130   for (i=0; i<bddManager->numVars; i++){
01131     fprintf(stdout, "%3d ", bddManager->indexToId[i]);
01132   }
01133   fprintf(stdout, "%8d\n", bddManager->numNodes);
01134 #endif
01135 }
01136 
01137 
01149 static void
01150 BddExchangeVarBlocks(Cal_BddManager_t *bddManager, Cal_Block parent,
01151                      long blockIndex)
01152 {
01153   Cal_Block b1, b2, temp;
01154   long i, j, k, l, firstBlockWidth, secondBlockWidth;
01155 
01156   b1 = parent->children[blockIndex];
01157   b2 = parent->children[blockIndex+1];
01158   /* This slides the blocks past each other in a kind of interleaving */
01159   /* fashion. */
01160   firstBlockWidth = b1->lastIndex - b1->firstIndex;
01161   secondBlockWidth = b2->lastIndex - b2->firstIndex;
01162   
01163   for (i=0; i <= firstBlockWidth + secondBlockWidth; i++){
01164     j = i - firstBlockWidth;
01165     if (j < 0) j=0;
01166     k = ((i > secondBlockWidth) ? secondBlockWidth : i);
01167     while (j <= k) {
01168           l = b2->firstIndex + j - i + j;
01169           BddExchange(bddManager, bddManager->indexToId[l-1]);
01170           ++j;
01171         }
01172   }
01173   CalBddBlockDelta(b1, secondBlockWidth+1);
01174   CalBddBlockDelta(b2, -(firstBlockWidth+1));
01175   temp = parent->children[blockIndex];
01176   parent->children[blockIndex] = parent->children[blockIndex+1];
01177   parent->children[blockIndex+1] = temp;
01178 }
01179 
01191 static int
01192 BddReorderWindow2(Cal_BddManager_t *bddManager, Cal_Block block, long i)
01193 {
01194   long size, bestSize;
01195 
01196   /* 1 2 */
01197   bestSize = bddManager->numNodes;
01198   BddExchangeVarBlocks(bddManager, block, i);
01199   /* 2 1 */
01200   size = bddManager->numNodes;
01201   if (size < bestSize) return (1);
01202   BddExchangeVarBlocks(bddManager, block, i);
01203   return (0);
01204 }
01205 
01206 
01218 static int
01219 BddReorderWindow3(Cal_BddManager_t *bddManager, Cal_Block block, long i)
01220 {
01221   int best;
01222   long size, bestSize;
01223   long origSize;
01224   
01225   origSize = bddManager->numNodes;
01226   best = 0;
01227   /* 1 2 3 */
01228   bestSize = bddManager->numNodes;
01229   BddExchangeVarBlocks(bddManager, block, i);
01230   /* 2 1 3 */
01231   size=bddManager->numNodes;
01232   if (size < bestSize) {
01233     best=1;
01234     bestSize=size;
01235   }
01236   BddExchangeVarBlocks(bddManager, block, i+1);
01237   /* 2 3 1 */
01238   size=bddManager->numNodes;
01239   if (size < bestSize) {
01240     best=2;
01241     bestSize=size;
01242   }
01243   BddExchangeVarBlocks(bddManager, block, i);
01244   /* 3 2 1 */
01245   size=bddManager->numNodes;
01246   if (size <= bestSize) {
01247     best=3;
01248     bestSize=size;
01249   }
01250   BddExchangeVarBlocks(bddManager, block, i+1);
01251   /* 3 1 2 */
01252   size=bddManager->numNodes;
01253   if (size <= bestSize) {
01254     best=4;
01255     bestSize=size;
01256   }
01257   BddExchangeVarBlocks(bddManager, block, i);
01258   /* 1 3 2 */
01259   size=bddManager->numNodes;
01260   if (size <= bestSize) {
01261     best=5;
01262     bestSize=size;
01263   }
01264   switch (best){
01265       case 0:
01266         BddExchangeVarBlocks(bddManager, block, i+1);
01267         break;
01268       case 1:
01269         BddExchangeVarBlocks(bddManager, block, i+1);
01270         BddExchangeVarBlocks(bddManager, block, i);
01271         break;
01272       case 2:
01273         BddExchangeVarBlocks(bddManager, block, i+1);
01274         BddExchangeVarBlocks(bddManager, block, i);
01275         BddExchangeVarBlocks(bddManager, block, i+1);
01276         break;
01277       case 3:
01278         BddExchangeVarBlocks(bddManager, block, i);
01279         BddExchangeVarBlocks(bddManager, block, i+1);
01280         break;
01281       case 4:
01282         BddExchangeVarBlocks(bddManager, block, i);
01283         break;
01284       case 5:
01285         break;
01286   }
01287   return ((best > 0) && (origSize > bestSize));
01288 }
01289 
01301 static void
01302 BddReorderStableWindow3Aux(Cal_BddManager_t *bddManager, Cal_Block block,
01303                            char *levels) 
01304 {
01305   long i;
01306   int moved;
01307   int anySwapped;
01308 
01309   if (block->reorderable) {
01310     for (i=0; i < block->numChildren-1; ++i) levels[i]=1;
01311     do {
01312           anySwapped=0;
01313           for (i=0; i < block->numChildren-1; i++){
01314             if (levels[i]){
01315 #ifdef _CAL_VERBOSE
01316           fprintf(stdout,"Moving block %3d -- %3d\n",
01317                   bddManager->indexToId[block->children[i]-> firstIndex],
01318                   bddManager->indexToId[block->children[i]->lastIndex]);
01319           fflush(stdout);
01320           for (j=0; j<bddManager->numVars; j++){
01321             fprintf(stdout, "%3d ", bddManager->indexToId[j]);
01322           }
01323           fprintf(stdout, "%8d\n", bddManager->numNodes);
01324 #endif
01325           if (i < block->numChildren-2){
01326             moved = BddReorderWindow3(bddManager, block, i);
01327           }
01328           else{
01329             moved = BddReorderWindow2(bddManager, block, i);
01330           }
01331           if (moved){
01332                     if (i > 0) {
01333               levels[i-1]=1;
01334               if (i > 1)
01335                 levels[i-2]=1;
01336             }
01337                     levels[i]=1;
01338                     levels[i+1]=1;
01339                     if (i < block->numChildren-2){
01340               levels[i+2]=1;
01341               if (i < block->numChildren-3) {
01342                             levels[i+3]=1;
01343                             if (i < block->numChildren-4) levels[i+4]=1;
01344                           }
01345             }
01346                     anySwapped=1;
01347           }
01348           else levels[i]=0;
01349         }
01350       }
01351     } while (anySwapped);
01352   }
01353   for (i=0; i < block->numChildren; ++i){
01354     BddReorderStableWindow3Aux(bddManager, block->children[i], levels);
01355   }
01356 }
01357 
01369 static void
01370 BddReorderStableWindow3(Cal_BddManager_t *bddManager)
01371 {
01372   char *levels;
01373   levels =  Cal_MemAlloc(char, bddManager->numVars);
01374   bddManager->numSwaps = 0;
01375   BddReorderStableWindow3Aux(bddManager, bddManager->superBlock, levels);
01376   Cal_MemFree(levels);
01377 }
01378 
01390 static void
01391 BddSiftBlock(Cal_BddManager_t *bddManager, Cal_Block block, long
01392              startPosition, double maxSizeFactor)
01393 {
01394   long startSize;
01395   long bestSize;
01396   long bestPosition;
01397   long currentSize;
01398   long currentPosition;
01399   long maxSize;
01400   
01401   startSize = bddManager->numNodes;
01402   bestSize = startSize;
01403   bestPosition = startPosition;
01404   currentSize = startSize;
01405   currentPosition = startPosition;
01406   maxSize = maxSizeFactor*startSize;
01407   if (bddManager->nodeLimit && maxSize > bddManager->nodeLimit)
01408     maxSize = bddManager->nodeLimit;
01409 
01410   /* Need to do optimization here */
01411   if (startPosition > (block->numChildren >> 1)){
01412     while (currentPosition < block->numChildren-1 && currentSize <= maxSize){
01413       BddExchangeVarBlocks(bddManager, block, currentPosition);
01414       ++currentPosition;
01415       currentSize = bddManager->numNodes;
01416       if (currentSize < bestSize){
01417         bestSize = currentSize;
01418         bestPosition=currentPosition;
01419       }
01420     }
01421     while (currentPosition != startPosition){
01422       --currentPosition;
01423       BddExchangeVarBlocks(bddManager, block, currentPosition);
01424     }
01425     currentSize = startSize;
01426     while (currentPosition && currentSize <= maxSize){
01427       --currentPosition;
01428       BddExchangeVarBlocks(bddManager, block, currentPosition);
01429       currentSize = bddManager->numNodes;
01430       if (currentSize <= bestSize){
01431         bestSize = currentSize;
01432         bestPosition = currentPosition;
01433       }
01434     }
01435     while (currentPosition != bestPosition){
01436       BddExchangeVarBlocks(bddManager, block, currentPosition);
01437       ++currentPosition;
01438     }
01439   }
01440   else{
01441     while (currentPosition && currentSize <= maxSize){
01442       --currentPosition;
01443       BddExchangeVarBlocks(bddManager, block, currentPosition);
01444       currentSize = bddManager->numNodes;
01445       if (currentSize < bestSize){
01446         bestSize = currentSize;
01447         bestPosition = currentPosition;
01448       }
01449     }
01450     while (currentPosition != startPosition){
01451       BddExchangeVarBlocks(bddManager, block, currentPosition);
01452       ++currentPosition;
01453     }
01454     currentSize = startSize;
01455     while (currentPosition < block->numChildren-1 && currentSize <= maxSize){
01456       BddExchangeVarBlocks(bddManager, block, currentPosition);
01457       currentSize = bddManager->numNodes;
01458       ++currentPosition;
01459       if (currentSize <= bestSize){
01460         bestSize = currentSize;
01461         bestPosition = currentPosition;
01462       }
01463     }
01464     while (currentPosition != bestPosition){
01465       --currentPosition;
01466       BddExchangeVarBlocks(bddManager, block, currentPosition);
01467     }
01468   }
01469 }
01470 
01471 
01472 
01482 static void
01483 BddReorderSiftAux(Cal_BddManager_t *bddManager, Cal_Block block,
01484                      Cal_Block *toSift, double maxSizeFactor) 
01485 {
01486   long i, j, k;
01487   long width;
01488   long maxWidth;
01489   long widest;
01490   long numVarsShifted = 0;
01491   bddManager->numSwaps = 0;
01492   if (block->reorderable) {
01493     for (i=0; i < block->numChildren; ++i){
01494       toSift[i] = block->children[i];
01495     }
01496     while (i &&
01497            (numVarsShifted <=
01498             bddManager->maxNumVarsSiftedPerReordering) &&
01499            (bddManager->numSwaps <=
01500             bddManager->maxNumSwapsPerReordering)){ 
01501           i--;
01502       numVarsShifted++;
01503           maxWidth = 0;
01504           widest = 0;
01505           for (j=0; j <= i; ++j) {
01506         for (width=0, k=toSift[j]->firstIndex; k <= toSift[j]->lastIndex; ++k){
01507           width +=
01508               bddManager->uniqueTable[bddManager->indexToId[k]]->numEntries; 
01509         }
01510         width /= toSift[j]->lastIndex - toSift[j]->firstIndex+1;
01511         if (width > maxWidth) {
01512                   maxWidth = width;
01513                   widest = j;
01514                 }
01515       }
01516           if (maxWidth > 1) {
01517         for (j=0; block->children[j] != toSift[widest]; ++j);
01518 #ifdef _CAL_VERBOSE
01519         fprintf(stdout,"Moving block %3d -- %3d\n",
01520                 bddManager->indexToId[block->children[j]-> firstIndex],
01521                 bddManager->indexToId[block->children[j]->lastIndex]);
01522         fflush(stdout);
01523         for (l=0; l<bddManager->numVars; l++){
01524           fprintf(stdout, "%3d ", bddManager->indexToId[l]);
01525         }
01526         fprintf(stdout, "%8d\n", bddManager->numNodes);
01527 #endif
01528         BddSiftBlock(bddManager, block, j, maxSizeFactor);
01529         toSift[widest] = toSift[i];
01530       }
01531           else {
01532         break;
01533       }
01534         }
01535   }
01536   for (i=0; i < block->numChildren; ++i)
01537     BddReorderSiftAux(bddManager, block->children[i], toSift,
01538                       maxSizeFactor);  
01539 }
01540 
01552 static void
01553 BddReorderSift(Cal_BddManager_t *bddManager, double maxSizeFactor)
01554 {
01555   Cal_Block *toSift;
01556 
01557   toSift = Cal_MemAlloc(Cal_Block, bddManager->numVars);
01558   BddReorderSiftAux(bddManager, bddManager->superBlock, toSift,
01559                        maxSizeFactor); 
01560   Cal_MemFree(toSift);
01561 }
01562 
01563 
01564 
01565 
01577 static int
01578 CeilLog2(int  number)
01579 {
01580   int num, count;
01581   for (num=number, count=0; num > 1; num >>= 1, count++);
01582   if ((1 << count) != number) count++;
01583   return count;
01584 }