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

00001 
00045 #include "calInt.h"
00046 
00047 /*---------------------------------------------------------------------------*/
00048 /* Constant declarations                                                     */
00049 /*---------------------------------------------------------------------------*/
00050 
00051 /*---------------------------------------------------------------------------*/
00052 /* Type declarations                                                         */
00053 /*---------------------------------------------------------------------------*/
00054 
00055 /*---------------------------------------------------------------------------*/
00056 /* Stucture declarations                                                     */
00057 /*---------------------------------------------------------------------------*/
00058 
00059 /*---------------------------------------------------------------------------*/
00060 /* Variable declarations                                                     */
00061 /*---------------------------------------------------------------------------*/
00062 
00063 /*---------------------------------------------------------------------------*/
00064 /* Macro declarations                                                        */
00065 /*---------------------------------------------------------------------------*/
00066 
00069 /*---------------------------------------------------------------------------*/
00070 /* Static function prototypes                                                */
00071 /*---------------------------------------------------------------------------*/
00072 
00073 static void BddReorderFixForwardingNodes(Cal_BddManager bddManager, Cal_BddId_t id);
00074 static void BddReorderFixAndFreeForwardingNodes(Cal_BddManager bddManager, Cal_BddId_t id, int numLevels);
00075 static void BddReorderSwapVarIndex(Cal_BddManager_t * bddManager, int varIndex, int forwardCheckFlag);
00076 static int CofactorFixAndReclaimForwardedNodes(Cal_BddManager_t *bddManager, int cofactorCheckStartIndex, int cofactorCheckEndIndex, int reclaimStartIndex, int reclaimEndIndex);
00077 static void BddReorderFreeNodes(Cal_BddManager_t * bddManager, int varId);
00078 #ifdef _CAL_VERBOSE
00079 static void PrintBddProfileAfterReorder(Cal_BddManager_t *bddManager);
00080 #endif
00081 static void BddReorderVarSift(Cal_BddManager bddManager, double maxSizeFactor);
00082 static int BddReorderSiftToBestPos(Cal_BddManager_t * bddManager, int varStartIndex, double maxSizeFactor);
00083 static void BddSiftPerfromPhaseIV(Cal_BddManager_t *bddManager, int varStartIndex, int bestIndex, int bottomMostSwapIndex);
00084 static void BddReorderVarWindow(Cal_BddManager bddManager, char *levels);
00085 static int BddReorderWindow2(Cal_BddManager bddManager, long index, int directionFlag);
00086 static int BddReorderWindow3(Cal_BddManager bddManager, long index, int directionFlag);
00087 
00090 /*---------------------------------------------------------------------------*/
00091 /* Definition of exported functions                                          */
00092 /*---------------------------------------------------------------------------*/
00093 /*---------------------------------------------------------------------------*/
00094 /* Definition of internal functions                                          */
00095 /*---------------------------------------------------------------------------*/
00107 void
00108 CalBddReorderAuxBF(Cal_BddManager_t * bddManager)
00109 {
00110   Cal_Assert(CalCheckAllValidity(bddManager));
00111   CalInitInteract(bddManager);
00112 #ifdef _CAL_QUANTIFY_
00113   quantify_start_recording_data();
00114 #endif
00115   if (bddManager->reorderTechnique == CAL_REORDER_WINDOW){
00116     char *levels = Cal_MemAlloc(char, bddManager->numVars);
00117     BddReorderVarWindow(bddManager, levels);
00118     Cal_MemFree(levels);
00119   }
00120   else {
00121     BddReorderVarSift(bddManager, bddManager->maxSiftingGrowth);
00122   }
00123 #ifdef _CAL_QUANTIFY_
00124   quantify_stop_recording_data();
00125 #endif
00126   Cal_Assert(CalCheckAllValidity(bddManager));
00127   Cal_MemFree(bddManager->interact);
00128   bddManager->numReorderings++;
00129 }
00130 
00131 /*---------------------------------------------------------------------------*/
00132 /* Definition of static functions                                          */
00133 /*---------------------------------------------------------------------------*/
00134 
00149 static void
00150 BddReorderFixForwardingNodes(Cal_BddManager bddManager,
00151                              Cal_BddId_t id) 
00152 {
00153   CalHashTable_t *uniqueTableForId =
00154       bddManager->uniqueTable[id];
00155   CalBddNode_t *bddNode, *nextBddNode;
00156   Cal_Bdd_t thenBdd;
00157   
00158   /* These are the forwarding nodes. */
00159   CalBddNode_t *requestNodeList =
00160       uniqueTableForId->startNode.nextBddNode;
00161   for (bddNode = requestNodeList; bddNode; bddNode = nextBddNode){
00162     nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00163     CalBddNodeGetThenBdd(bddNode, thenBdd);
00164     if (CalBddIsForwarded(thenBdd)) {
00165       CalBddForward(thenBdd);
00166       CalBddNodePutThenBdd(bddNode, thenBdd);
00167     }
00168     else {
00169       /* there should not be anymore double forwarding */
00170       break;
00171     }
00172     Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
00173   }
00174   /* Adjust the list */
00175   uniqueTableForId->endNode->nextBddNode =
00176       uniqueTableForId->startNode.nextBddNode;
00177   uniqueTableForId->startNode.nextBddNode = bddNode;
00178 }
00179 
00192 static void
00193 BddReorderFixAndFreeForwardingNodes(Cal_BddManager bddManager,
00194                                     Cal_BddId_t id, int numLevels)
00195 {
00196   CalHashTable_t *uniqueTableForId;
00197   Cal_BddIndex_t index = bddManager->idToIndex[id];
00198   CalBddNode_t *nextBddNode, *bddNode, *endNode;
00199   Cal_Bdd_t thenBdd;
00200   CalNodeManager_t *nodeManager;
00201   int i;
00202   
00203   /* Fixing */
00204   for (i=numLevels-1; i >= 0; i--){
00205     uniqueTableForId =
00206         bddManager->uniqueTable[bddManager->indexToId[index+i]];
00207     for (bddNode = uniqueTableForId->startNode.nextBddNode; bddNode;
00208          bddNode = nextBddNode){ 
00209       nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00210       CalBddNodeGetThenBdd(bddNode, thenBdd);
00211       if (CalBddIsForwarded(thenBdd)){
00212         do{
00213           CalBddMark(thenBdd);
00214           CalBddForward(thenBdd);
00215         } while (CalBddIsForwarded(thenBdd));
00216         CalBddNodePutThenBdd(bddNode, thenBdd); 
00217       }
00218       Cal_Assert(CalBddIsForwarded(thenBdd) == 0);
00219     }
00220   }
00221   /* Freeing */
00222   for (i=numLevels-1; i >= 0; i--){
00223     uniqueTableForId =
00224         bddManager->uniqueTable[bddManager->indexToId[index+i]];
00225     endNode = &(uniqueTableForId->startNode);
00226     for (bddNode = uniqueTableForId->startNode.nextBddNode; bddNode;
00227          bddNode = nextBddNode){ 
00228       nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00229       CalBddNodeGetThenBdd(bddNode, thenBdd);
00230       if (CalBddIsMarked(thenBdd)){
00231         do{
00232           /* Free the node */
00233           nodeManager = bddManager->nodeManagerArray[CalBddGetBddId(thenBdd)];
00234           CalNodeManagerFreeNode(nodeManager, CalBddGetBddNode(thenBdd));
00235           bddManager->numForwardedNodes--;
00236         } while (CalBddIsMarked(thenBdd));
00237       }
00238       else{
00239         endNode->nextBddNode = bddNode;
00240         endNode = bddNode;
00241       }
00242     }
00243     uniqueTableForId->endNode = endNode;
00244   }
00245 }
00246 
00258 static void
00259 BddReorderSwapVarIndex(Cal_BddManager_t * bddManager, int varIndex,
00260                        int forwardCheckFlag)
00261 {
00262   int thenVarIndex;
00263   int elseVarIndex;
00264   int varId;
00265   int nextVarId;
00266   int i;
00267   int numBins;
00268   int refCount;
00269   int f0Found;
00270   int f1Found;
00271   CalHashTable_t *uniqueTableForId;
00272   CalHashTable_t *nextUniqueTableForId;
00273   CalBddNode_t **bins;
00274   CalBddNode_t *bddNode, *startNode;
00275   CalBddNode_t *nextBddNode, *processingNodeList;
00276   CalBddNode_t *prevBddNode = Cal_Nil(CalBddNode_t);
00277   Cal_Bdd_t newF;
00278   Cal_Bdd_t f0;
00279   Cal_Bdd_t f1;
00280   Cal_Bdd_t newF0;
00281   Cal_Bdd_t newF1;
00282   Cal_Bdd_t f00;
00283   Cal_Bdd_t f01;
00284   Cal_Bdd_t f10;
00285   Cal_Bdd_t f11;
00286   CalAssociation_t *assoc;
00287   
00288   varId = bddManager->indexToId[varIndex];
00289   nextVarId = bddManager->indexToId[varIndex + 1];
00290   
00291   if (CalTestInteract(bddManager, varId, nextVarId)){
00292   bddManager->numSwaps++;
00293 #ifdef _CAL_VERBOSE
00294   /*fprintf(stdout," %3d(%3d) going down,  %3d(%3d) going up\n",
00295           varId, varIndex, nextVarId, varIndex+1);*/
00296 #endif
00297   uniqueTableForId = bddManager->uniqueTable[varId];
00298   nextUniqueTableForId = bddManager->uniqueTable[nextVarId];
00299   
00300   /*uniqueTableForId->requestNodeList = Cal_Nil(CalBddNode_t);*/
00301   processingNodeList = Cal_Nil(CalBddNode_t);
00302   numBins = uniqueTableForId->numBins;
00303   bins = uniqueTableForId->bins;
00304   if (forwardCheckFlag){
00305     for(i = 0; i < numBins; ++i) {
00306       prevBddNode = Cal_Nil(CalBddNode_t);
00307       for(bddNode = bins[i];
00308           bddNode != Cal_Nil(CalBddNode_t);
00309           bddNode = nextBddNode) {
00310         /*
00311          * Process one bddNode at a time
00312          */
00313         nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00314         /* The node should not be forwarded */
00315         Cal_Assert(CalBddNodeIsForwarded(bddNode) == 0);
00316         /*
00317         ** We don't know for sure if the reference count of the node
00318         ** could be 0. Let us use the assertion at this point.
00319         */
00320         Cal_Assert(CalBddNodeIsRefCountZero(bddNode) == 0);
00321         /*
00322         ** If ever the above assetion fails, or if we can convince
00323         ** ourselves that the reference count could be zero, we need
00324         ** to uncomment the following code.
00325         */
00326         /*
00327         if (CalBddNodeIsRefCountZero(bddNode)){
00328           thenBddNode = CAL_BDD_POINTER(CalBddNodeGetThenBddNode(bddNode));
00329           elseBddNode = CAL_BDD_POINTER(CalBddNodeGetElseBddNode(bddNode));
00330           CalBddNodeDcrRefCount(thenBddNode);
00331           CalBddNodeDcrRefCount(elseBddNode);
00332           if (prevBddNode){
00333             CalBddNodePutNextBddNode(prevBddNode, nextBddNode);
00334           }
00335           else{
00336             bins[i] = nextBddNode;
00337           }
00338           uniqueTableForId->numEntries--;
00339           bddManager->numNodes--;
00340           bddManager->numNodesFreed++;
00341           CalNodeManagerFreeNode(uniqueTableForId->nodeManager, bddNode);
00342           continue;
00343         }
00344         */
00345         CalBddNodeGetElseBdd(bddNode, f0);
00346         CalBddNodeGetThenBdd(bddNode, f1);
00347         
00348         if (CalBddIsForwarded(f1)) {
00349           CalBddForward(f1);
00350           CalBddNodePutThenBdd(bddNode, f1);
00351         }
00352         Cal_Assert(CalBddIsForwarded(f1) == 0);
00353         
00354         if (CalBddIsForwarded(f0)) {
00355           CalBddForward(f0);
00356           CalBddNodePutElseBdd(bddNode, f0); 
00357         }
00358         Cal_Assert(CalBddIsForwarded(f0) == 0);
00359         /*
00360         ** Get the index of f0 and f1 and create newF0 and newF1 if necessary
00361         */
00362         elseVarIndex = CalBddNodeGetElseBddIndex(bddManager, bddNode);
00363         thenVarIndex = CalBddNodeGetThenBddIndex(bddManager, bddNode);
00364         
00365         if ((elseVarIndex > (varIndex + 1))
00366             && (thenVarIndex > (varIndex + 1))) { 
00367           prevBddNode = bddNode;
00368           Cal_Assert(CalDoHash2(CalBddGetBddNode(f1),
00369                                 CalBddGetBddNode(f0), 
00370                                 uniqueTableForId) == i);
00371           continue;
00372         }
00373   
00374         /* This node is going to be forwared */
00375         CalBddNodePutNextBddNode(bddNode, processingNodeList);
00376         processingNodeList = bddNode;
00377         
00378         /* Update the unique table appropriately */
00379         if (prevBddNode){
00380           CalBddNodePutNextBddNode(prevBddNode, nextBddNode);
00381         }
00382         else{
00383           bins[i] = nextBddNode;
00384         } 
00385         uniqueTableForId->numEntries--;
00386         bddManager->numNodes--;
00387       }
00388     }
00389   }
00390   else{
00391     for(i = 0; i < numBins; i++) {
00392       prevBddNode = Cal_Nil(CalBddNode_t);
00393       for(bddNode = bins[i];
00394           bddNode != Cal_Nil(CalBddNode_t);
00395           bddNode = nextBddNode) {
00396         /*
00397          * Process one bddNode at a time
00398          */
00399         nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00400         /* The node should not be forwarded */
00401         Cal_Assert(CalBddNodeIsForwarded(bddNode) == 0);
00402 
00403         /*
00404         ** We don't know for sure if the reference count of the node
00405         ** could be 0. Let us use the assertion at this point.
00406         */
00407         Cal_Assert(CalBddNodeIsRefCountZero(bddNode) == 0);
00408         /*
00409         ** If ever the above assetion fails, or if we can convince
00410         ** ourselves that the reference count could be zero, we need
00411         ** to uncomment the following code.
00412         */
00413         /*
00414         if (CalBddNodeIsRefCountZero(bddNode)){
00415           thenBddNode = CAL_BDD_POINTER(CalBddNodeGetThenBddNode(bddNode));
00416           elseBddNode = CAL_BDD_POINTER(CalBddNodeGetElseBddNode(bddNode));
00417           CalBddNodeDcrRefCount(thenBddNode);
00418           CalBddNodeDcrRefCount(elseBddNode);
00419           if (prevBddNode){
00420             CalBddNodePutNextBddNode(prevBddNode, nextBddNode);
00421           }
00422           else{
00423             bins[i] = nextBddNode;
00424           }
00425           uniqueTableForId->numEntries--;
00426           bddManager->numNodes--;
00427           bddManager->numNodesFreed++;
00428           CalNodeManagerFreeNode(uniqueTableForId->nodeManager, bddNode);
00429           continue;
00430         }
00431         */
00432         CalBddNodeGetThenBdd(bddNode, f1);
00433         Cal_Assert(CalBddIsForwarded(f1) == 0);
00434         CalBddNodeGetElseBdd(bddNode, f0);
00435         Cal_Assert(CalBddIsForwarded(f0) == 0);
00436         /*
00437         ** Get the index of f0 and f1 and create newF0 and newF1 if necessary
00438         */
00439 
00440         elseVarIndex = CalBddNodeGetElseBddIndex(bddManager, bddNode);
00441         thenVarIndex = CalBddNodeGetThenBddIndex(bddManager, bddNode);
00442         
00443         if ((elseVarIndex > (varIndex + 1))
00444             && (thenVarIndex > (varIndex + 1))) { 
00445           prevBddNode = bddNode;
00446           continue;
00447         }
00448   
00449         /* This node is going to be forwared */
00450         CalBddNodePutNextBddNode(bddNode, processingNodeList);
00451         processingNodeList = bddNode;
00452         
00453         /* Update the unique table appropriately */
00454         if (prevBddNode){
00455           CalBddNodePutNextBddNode(prevBddNode, nextBddNode);
00456         }
00457         else{
00458           bins[i] = nextBddNode;
00459         } 
00460         uniqueTableForId->numEntries--;
00461         bddManager->numNodes--;
00462       }
00463     }
00464   }
00465   bddNode = processingNodeList;
00466   /*endNode = uniqueTableForId->endNode;*/
00467   startNode = uniqueTableForId->startNode.nextBddNode;
00468   while (bddNode != Cal_Nil(CalBddNode_t)) {
00469     nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00470 
00471     /*
00472      * Get the index of f0 and f1 and create newF0 and newF1 if necessary
00473      */
00474 
00475     CalBddNodeGetElseBdd(bddNode, f0);
00476     CalBddNodeGetThenBdd(bddNode, f1);
00477     elseVarIndex = CalBddNodeGetElseBddIndex(bddManager, bddNode);
00478     thenVarIndex = CalBddNodeGetThenBddIndex(bddManager, bddNode);
00479 
00480     if (elseVarIndex > (varIndex + 1)) {
00481       f00 = f0;
00482       f01 = f0;
00483       CalBddGetElseBdd(f1, f10);
00484       CalBddGetThenBdd(f1, f11);
00485     } else if (thenVarIndex > (varIndex + 1)) {
00486       f10 = f1;
00487       f11 = f1;
00488       CalBddGetElseBdd(f0, f00);
00489       CalBddGetThenBdd(f0, f01);
00490     }else{
00491       CalBddGetElseBdd(f1, f10);
00492       CalBddGetThenBdd(f1, f11);
00493       CalBddGetElseBdd(f0, f00);
00494       CalBddGetThenBdd(f0, f01);
00495     }
00496     Cal_Assert(CalBddIsForwarded(f10) == 0);
00497     Cal_Assert(CalBddIsForwarded(f11) == 0);
00498     Cal_Assert(CalBddIsForwarded(f00) == 0);
00499     Cal_Assert(CalBddIsForwarded(f01) == 0);
00500 
00501     if (CalBddIsEqual(f10,f00)) {
00502       newF0 = f00;
00503       f0Found = 1;
00504     }
00505     else {
00506       f0Found = CalUniqueTableForIdFindOrAdd(bddManager, uniqueTableForId, f10,
00507                                              f00, &newF0);
00508     }
00509     CalBddIcrRefCount(newF0);
00510     if (CalBddIsEqual(f11, f01)) {
00511       newF1 = f01;
00512       f1Found = 1;
00513     }
00514     else {
00515       f1Found = CalUniqueTableForIdFindOrAdd(bddManager, uniqueTableForId, f11,
00516                                              f01, &newF1);
00517     }
00518     CalBddIcrRefCount(newF1);
00519 
00520     if (!f0Found){
00521       CalBddIcrRefCount(f10);
00522       CalBddIcrRefCount(f00);
00523     }
00524 
00525     if (!f1Found){
00526       CalBddIcrRefCount(f11);
00527       CalBddIcrRefCount(f01);
00528     }
00529 
00530     CalBddDcrRefCount(f0);
00531     CalBddDcrRefCount(f1);
00532     /*
00533      * Create the new node for f. It cannot exist before, since at
00534      * least one of newF0 and newF1 must be dependent on currentIndex.
00535      * Otherwise, f00 == f10 and f01 == f11 (redundant nodes).
00536      */
00537     CalHashTableAddDirectAux(nextUniqueTableForId, newF1, newF0, &newF);
00538     bddManager->numNodes++;
00539     CalBddNodePutThenBdd(bddNode, newF);
00540     CalBddNodePutElseBddNode(bddNode, FORWARD_FLAG);
00541     bddManager->numForwardedNodes++;
00542     CalBddNodeGetRefCount(bddNode, refCount);
00543     CalBddAddRefCount(newF, refCount);
00544     Cal_Assert(!CalBddIsRefCountZero(newF));
00545     /* Put it in the forwarded list of the unique table */
00546     /*
00547     endNode->nextBddNode = bddNode;
00548     endNode = bddNode;
00549     */
00550     bddNode->nextBddNode = startNode;
00551     startNode = bddNode;
00552     
00553     bddNode = nextBddNode;
00554   }
00555   /*uniqueTableForId->endNode = endNode;*/
00556   uniqueTableForId->startNode.nextBddNode = startNode;
00557 
00558   BddReorderFreeNodes(bddManager, nextVarId);
00559   
00560   }
00561   else{
00562     bddManager->numTrivialSwaps++;
00563   }
00564   
00565   CalFixupAssoc(bddManager, varId, nextVarId, bddManager->tempAssociation);
00566   for(assoc = bddManager->associationList; assoc; assoc = assoc->next){
00567     CalFixupAssoc(bddManager, varId, nextVarId, assoc);
00568   }
00569 
00570   bddManager->idToIndex[varId] = varIndex + 1;
00571   bddManager->idToIndex[nextVarId] = varIndex;
00572   bddManager->indexToId[varIndex] = nextVarId;
00573   bddManager->indexToId[varIndex + 1] = varId;
00574 
00575   Cal_Assert(CalCheckAssoc(bddManager));
00576 
00577 #ifdef _CAL_VERBOSE
00578   /*fprintf(stdout,"Variable order after swap:\n");*/
00579   for (i=0; i<bddManager->numVars; i++){
00580     fprintf(stdout, "%3d ", bddManager->indexToId[i]);
00581   }
00582   fprintf(stdout, "%8d\n", bddManager->numNodes);
00583 #endif
00584 }
00585 
00597 static int
00598 CofactorFixAndReclaimForwardedNodes(Cal_BddManager_t *bddManager, int
00599                                        cofactorCheckStartIndex, int
00600                                        cofactorCheckEndIndex, int
00601                                        reclaimStartIndex, int reclaimEndIndex)
00602 {
00603   int index, varId;
00604   /* Clean up : Need to fix the cofactors of userBDDs and the
00605      indices above the varStartIndex only. */
00606   if (bddManager->pipelineState == CREATE){
00607     /* There are some results computed in pipeline */
00608     CalBddReorderFixProvisionalNodes(bddManager);
00609   }
00610   CalBddReorderFixUserBddPtrs(bddManager);
00611   CalReorderAssociationFix(bddManager);
00612   for (index = cofactorCheckStartIndex;
00613        index <= cofactorCheckEndIndex; index++){ 
00614     varId = bddManager->indexToId[index];
00615     CalBddReorderFixCofactors(bddManager, varId);
00616   }
00617   CalBddReorderReclaimForwardedNodes(bddManager, reclaimStartIndex,
00618                                      reclaimEndIndex);
00619   Cal_Assert(CalCheckAllValidity(bddManager));
00620   return 0;
00621 }
00622 
00634 static void
00635 BddReorderFreeNodes(Cal_BddManager_t * bddManager, int varId)
00636 {
00637   CalBddNode_t *prevNode, *bddNode, *nextBddNode;
00638   CalBddNode_t *elseBddNode;
00639   CalBddNode_t *thenBddNode;
00640   CalHashTable_t *uniqueTableForId;
00641   CalBddNode_t **bins;
00642   int numBins;
00643   int i;
00644   long oldNumEntries, numNodesFreed;
00645 
00646   uniqueTableForId = bddManager->uniqueTable[varId];
00647   bins = uniqueTableForId->bins;
00648   numBins = uniqueTableForId->numBins;
00649   oldNumEntries = uniqueTableForId->numEntries;
00650 
00651   if (bddManager->numPeakNodes < (bddManager->numNodes +
00652                                   bddManager->numForwardedNodes)){
00653     bddManager->numPeakNodes = bddManager->numNodes +
00654         bddManager->numForwardedNodes ;
00655   }
00656   
00657   for(i = 0; i < numBins; i++){
00658     prevNode = NULL;
00659     bddNode = bins[i];
00660     while(bddNode != Cal_Nil(CalBddNode_t)){
00661       nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00662       Cal_Assert(CalBddNodeIsForwarded(bddNode) == 0);
00663       if(CalBddNodeIsRefCountZero(bddNode)){
00664         thenBddNode = CAL_BDD_POINTER(CalBddNodeGetThenBddNode(bddNode));
00665         elseBddNode = CAL_BDD_POINTER(CalBddNodeGetElseBddNode(bddNode));
00666         Cal_Assert(CalBddNodeIsForwarded(thenBddNode) == 0);
00667         Cal_Assert(CalBddNodeIsForwarded(elseBddNode) == 0);
00668         CalBddNodeDcrRefCount(thenBddNode);
00669         CalBddNodeDcrRefCount(elseBddNode);
00670         if (prevNode == NULL) {
00671           bins[i] = nextBddNode;
00672         } else {
00673           CalBddNodePutNextBddNode(prevNode, nextBddNode);
00674         }
00675         CalNodeManagerFreeNode(uniqueTableForId->nodeManager, bddNode);
00676         uniqueTableForId->numEntries--;
00677       } else {
00678         prevNode = bddNode;
00679       }
00680       bddNode = nextBddNode;
00681     }
00682   }
00683   numNodesFreed = oldNumEntries - uniqueTableForId->numEntries;
00684   bddManager->numNodes -= numNodesFreed;
00685   bddManager->numNodesFreed += numNodesFreed;
00686 }
00687 
00688 #ifdef _CAL_VERBOSE
00689 
00701 static void
00702 PrintBddProfileAfterReorder(Cal_BddManager_t *bddManager)
00703 {
00704     int i, index, numBins, j;
00705     CalHashTable_t *uniqueTableForId;
00706     CalBddNode_t *bddNode, *nextBddNode;
00707     char *levels = Cal_MemAlloc(char, bddManager->numVars+1);
00708     CalBddNode_t *requestNodeList;
00709     Cal_Bdd_t thenBdd, elseBdd;
00710     
00711   /* Now traverse all the nodes in order */
00712     for (index = 0; index < bddManager->numVars; index++){
00713       fprintf(stdout,"**** %3d ****\n", bddManager->indexToId[index]);  
00714       uniqueTableForId = bddManager->uniqueTable[bddManager->indexToId[index]];
00715       numBins = uniqueTableForId->numBins;
00716       for (i=1; i<=bddManager->numVars; i++) {
00717           levels[i] = 0;
00718       }
00719       j = 0;
00720       for (i = 0; i < numBins; i++){
00721           for (bddNode = uniqueTableForId->bins[i]; bddNode;
00722                bddNode = nextBddNode){
00723               nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00724               CalBddNodeGetThenBdd(bddNode, thenBdd);
00725               CalBddNodeGetElseBdd(bddNode, elseBdd);
00726               if (CalBddIsForwarded(thenBdd) ||
00727                   CalBddIsForwarded(elseBdd)){                       
00728                 j++;
00729               }
00730               if (CalBddIsForwarded(thenBdd)) {                      
00731                   levels[CalBddGetThenBddId(thenBdd)]++;
00732               }
00733               if (CalBddIsForwarded(elseBdd)) {                      
00734                   levels[CalBddGetThenBddId(elseBdd)]++;
00735               }
00736           }
00737       }
00738       fprintf(stdout,"\tCofactors (%3d): ", j);
00739       for (i=1; i<=bddManager->numVars; i++){
00740           if (levels[i]) {
00741               fprintf(stdout,"%3d->%3d ", i, levels[i]);
00742           }
00743       }
00744       fprintf(stdout,"\n");
00745       for (i=1; i<=bddManager->numVars; i++) {
00746           levels[i] = 0;
00747       }
00748       j = 0;
00749       requestNodeList = uniqueTableForId->startNode.nextBddNode;
00750       for (bddNode = requestNodeList; bddNode; bddNode = nextBddNode){
00751           Cal_Assert(CalBddNodeIsForwarded(bddNode));
00752           nextBddNode = CalBddNodeGetNextBddNode(bddNode);
00753           CalBddNodeGetThenBdd(bddNode, thenBdd);
00754           Cal_Assert(!CalBddIsForwarded(thenBdd));
00755           levels[CalBddGetBddId(thenBdd)]++;
00756           j++;
00757       }
00758       fprintf(stdout,"\tForwarded nodes (%3d): ", j);
00759       for (i=1; i<=bddManager->numVars; i++){
00760           if (levels[i]) {
00761               fprintf(stdout,"%3d->%3d ", i, levels[i]);
00762           }
00763       }
00764       fprintf(stdout,"\n");
00765     }
00766     Cal_MemFree(levels);
00767 }
00768 #endif
00769 
00779 static void
00780 BddReorderVarSift(Cal_BddManager bddManager, double maxSizeFactor)
00781 {
00782   int i,j;
00783   int mostNodesId = -1;
00784   long mostNodes, varNodes;
00785   int *idArray;
00786   long numVarsShifted = 0;
00787   bddManager->numSwaps = 0;
00788   
00789   idArray = Cal_MemAlloc(int, bddManager->numVars);
00790   for (i = 0; i < bddManager->numVars; i++) {
00791     idArray[i] = bddManager->indexToId[i];
00792   }
00793 
00794   while (i &&
00795          (numVarsShifted <=
00796           bddManager->maxNumVarsSiftedPerReordering) &&
00797          (bddManager->numSwaps <=
00798           bddManager->maxNumSwapsPerReordering)){ 
00799     i--;
00800     numVarsShifted++;
00801 /*
00802  * Find var with the most number of nodes and do sifting on it.
00803  * idArray is used to make sure that a var is not sifted more than
00804  * once.
00805  */
00806     mostNodes = 0;
00807     for (j = 0; j <= i; j++){
00808       varNodes = bddManager->uniqueTable[idArray[j]]->numEntries;
00809       if (varNodes > mostNodes) {
00810         mostNodes = varNodes;
00811         mostNodesId = j;
00812       }
00813     }
00814  
00815     if (mostNodes <= 1) { /* I can put a different stopping criterion */
00816       /*
00817        * Most number of nodes among the vars not sifted yet is 0. Stop.
00818        */
00819       break;
00820     }
00821 
00822     BddReorderSiftToBestPos(bddManager,
00823                             bddManager->idToIndex[idArray[mostNodesId]],
00824                             maxSizeFactor); 
00825     Cal_Assert(CalCheckAllValidity(bddManager));
00826     idArray[mostNodesId] = idArray[i];
00827   }
00828 
00829   Cal_MemFree(idArray);
00830 }
00831 
00832 
00844 static int
00845 BddReorderSiftToBestPos(Cal_BddManager_t * bddManager, int
00846                         varStartIndex, double maxSizeFactor)
00847 {
00848   long curSize;
00849   long bestSize;
00850   int bestIndex;
00851   int varCurIndex;
00852   int varId, i;
00853   int lastIndex = bddManager->numVars - 1;
00854   int numVars = bddManager->numVars;
00855   long startSize = bddManager->numNodes;
00856   long maxSize =  startSize * maxSizeFactor;
00857   int origId = bddManager->indexToId[varStartIndex];
00858 
00859   int topMostSwapIndex = 0; /* the variable has been swapped upto this
00860                                index */
00861   int bottomMostSwapIndex = lastIndex; /* the variable has been
00862                                           swapped upto this index */
00863 
00864   int swapFlag = 0; /* If a swap has taken place after last cleaning
00865                        up */
00866                        
00867   
00868   curSize = bestSize = bddManager->numNodes;
00869   bestIndex = varStartIndex;
00870 
00871 #ifdef _CAL_VERBOSE
00872   for (i=0; i<bddManager->numVars; i++){
00873     fprintf(stdout, "%3d ", bddManager->indexToId[i]);
00874   }
00875   fprintf(stdout, "%8d\n", bddManager->numNodes);
00876 #endif
00877   
00878   /*
00879   ** If varStartIndex > numVars/2, do: Down, Up, Down.
00880   ** If varStartIndex < numVars/2, do: Up, Down, Up
00881   ** Followed by a cleanup phase in either case.
00882   */
00883   
00884   if (varStartIndex >= (numVars >> 1)){
00885     /* Phase I: Downward swap, no forwarding check. */
00886     varCurIndex = varStartIndex;
00887     while (varCurIndex < lastIndex) {
00888       BddReorderSwapVarIndex(bddManager, varCurIndex, 0);
00889       swapFlag = 1;
00890       if (bddManager->numForwardedNodes > bddManager->maxForwardedNodes){
00891         CofactorFixAndReclaimForwardedNodes(bddManager, 0,
00892                                                varCurIndex-1,
00893                                                varCurIndex+1,
00894                                                varCurIndex+1); 
00895         swapFlag = 0;
00896       }
00897       varCurIndex++;
00898       curSize = bddManager->numNodes;
00899       /*if (curSize > maxSize){*/
00900       if (curSize >= (bestSize << 1)){
00901         bottomMostSwapIndex = varCurIndex;
00902         break;
00903       }
00904       if (curSize < bestSize) {
00905         bestSize = curSize;
00906         bestIndex = varCurIndex;
00907       }
00908     }
00909     
00910     /* Phase II : Two parts */
00911     /*
00912     ** Part One: Upward swap until varStartIndex. Fix cofactors and
00913     ** fix double pointers. 
00914     */
00915     
00916     while (varCurIndex > varStartIndex) {
00917       varCurIndex--;
00918       BddReorderSwapVarIndex(bddManager, varCurIndex, 1);
00919       swapFlag = 1;
00920       varId = bddManager->indexToId[varCurIndex];
00921       BddReorderFixForwardingNodes(bddManager, varId);
00922       if (bddManager->numForwardedNodes > bddManager->maxForwardedNodes){
00923         CofactorFixAndReclaimForwardedNodes(bddManager, 0,
00924                                                varCurIndex-1,
00925                                                varCurIndex,
00926                                                bottomMostSwapIndex); 
00927         swapFlag = 0;
00928       }
00929     }
00930     curSize = startSize;
00931     
00932     /*
00933     ** Part two: Upward swap all the way to the top. Fix cofactors.
00934     */
00935     while (varCurIndex > 0) {
00936       varCurIndex--;
00937       BddReorderSwapVarIndex(bddManager, varCurIndex, 1);
00938       swapFlag = 1;
00939       curSize = bddManager->numNodes;
00940       if (bddManager->numForwardedNodes > bddManager->maxForwardedNodes){
00941         CofactorFixAndReclaimForwardedNodes(bddManager, 0,
00942                                                varCurIndex-1,
00943                                                varCurIndex,
00944                                                bottomMostSwapIndex); 
00945         swapFlag = 0;
00946       }
00947       if (curSize > maxSize){
00948         topMostSwapIndex = varCurIndex;
00949         break;
00950       }
00951       if (curSize <= bestSize) {
00952         bestSize = curSize;
00953         bestIndex = varCurIndex;
00954       }
00955     }
00956 
00957     if (swapFlag){
00958       /* Fix user BDD pointers and reclaim forwarding nodes */
00959       if (bddManager->pipelineState == CREATE){
00960         /* There are some results computed in pipeline */
00961         CalBddReorderFixProvisionalNodes(bddManager);
00962       }
00963       CalBddReorderFixUserBddPtrs(bddManager);
00964       CalReorderAssociationFix(bddManager);
00965       
00966       /* The upward swapping might have stopped short */
00967       for (i = 0; i < topMostSwapIndex; i++){
00968         varId = bddManager->indexToId[i];
00969         CalBddReorderFixCofactors(bddManager, varId);
00970       }
00971       
00972       CalBddReorderReclaimForwardedNodes(bddManager, topMostSwapIndex,
00973                                          bottomMostSwapIndex);
00974       swapFlag = 0;
00975     }
00976     
00977     Cal_Assert(CalCheckAllValidity(bddManager));
00978     
00979     /* Phase III : Swap to the min position */
00980 
00981     while (varCurIndex < bestIndex) {
00982       BddReorderSwapVarIndex(bddManager, varCurIndex, 0); 
00983       swapFlag = 1;
00984       if (bddManager->numForwardedNodes > bddManager->maxForwardedNodes){
00985         CofactorFixAndReclaimForwardedNodes(bddManager, 0,
00986                                                varCurIndex-1,
00987                                                varCurIndex+1,
00988                                                varCurIndex+1); 
00989         swapFlag = 0;
00990       }
00991       varCurIndex++;
00992     }
00993   }
00994   else{
00995     /* Phase I: Upward swap, fix cofactors. */
00996     varCurIndex = varStartIndex;
00997     while (varCurIndex > 0) {
00998       varCurIndex--;
00999       BddReorderSwapVarIndex(bddManager, varCurIndex, 1);
01000       swapFlag = 1;
01001       curSize = bddManager->numNodes;
01002       if (bddManager->numForwardedNodes > bddManager->maxForwardedNodes){
01003         CofactorFixAndReclaimForwardedNodes(bddManager, 0,
01004                                                varCurIndex-1,
01005                                                varCurIndex+1,
01006                                                varStartIndex); 
01007         swapFlag = 0;
01008       }
01009       if (curSize > maxSize){
01010         topMostSwapIndex = varCurIndex;
01011         break;
01012       }
01013       if (curSize < bestSize) {
01014         bestSize = curSize;
01015         bestIndex = varCurIndex;
01016       }
01017     }
01018     
01019     if (swapFlag){
01020       /* Fix user BDD pointers and reclaim forwarding nodes */
01021       if (bddManager->pipelineState == CREATE){
01022         /* There are some results computed in pipeline */
01023         CalBddReorderFixProvisionalNodes(bddManager);
01024       }
01025       CalBddReorderFixUserBddPtrs(bddManager);
01026       CalReorderAssociationFix(bddManager);
01027       /* The upward swapping might have stopped short */
01028       for (i = 0; i < topMostSwapIndex; i++){
01029         varId = bddManager->indexToId[i];
01030         CalBddReorderFixCofactors(bddManager, varId);
01031       }
01032       CalBddReorderReclaimForwardedNodes(bddManager, topMostSwapIndex,
01033                                          varStartIndex);
01034       swapFlag = 0;
01035     }
01036     
01037     Cal_Assert(CalCheckAllValidity(bddManager));
01038 
01039     /* Phase II : Move all the way down : two parts */
01040 
01041     /* Swap it to the original position, no cofactor fixing, fix
01042        double pointers of the variable moving up.*/
01043     while (varCurIndex < varStartIndex){
01044       BddReorderSwapVarIndex(bddManager, varCurIndex, 0);
01045       swapFlag = 1;
01046       if (bddManager->numForwardedNodes > bddManager->maxForwardedNodes){
01047         CofactorFixAndReclaimForwardedNodes(bddManager, 0,
01048                                                varCurIndex-1,
01049                                                varCurIndex+1,
01050                                                varCurIndex+1); 
01051         swapFlag = 0;
01052       }
01053       varCurIndex++;
01054     }
01055     /* Swap to the bottom */
01056     while (varCurIndex < lastIndex){
01057       BddReorderSwapVarIndex(bddManager, varCurIndex, 0);
01058       swapFlag = 1;
01059       if (bddManager->numForwardedNodes > bddManager->maxForwardedNodes){
01060         CofactorFixAndReclaimForwardedNodes(bddManager, 0,
01061                                                varCurIndex-1,
01062                                                varCurIndex+1,
01063                                                varCurIndex+1); 
01064         swapFlag = 0;
01065       }
01066       varCurIndex++;
01067       curSize = bddManager->numNodes;
01068       /* if (curSize > maxSize){ */
01069       if (curSize >= (bestSize << 1)){
01070         bottomMostSwapIndex = varCurIndex;
01071         break;
01072       }
01073       if (curSize <= bestSize) {
01074         bestSize = curSize;
01075         bestIndex = varCurIndex;
01076       }
01077     }
01078 
01079     /* Phase III : Move up to the best position */
01080     while (varCurIndex > bestIndex){
01081       varCurIndex--;
01082       BddReorderSwapVarIndex(bddManager, varCurIndex, 1);
01083       swapFlag = 1;
01084       varId = bddManager->indexToId[varCurIndex];
01085       BddReorderFixForwardingNodes(bddManager, varId);
01086       if (bddManager->numForwardedNodes > bddManager->maxForwardedNodes){
01087         CofactorFixAndReclaimForwardedNodes(bddManager, 0, varCurIndex-1,
01088                                                varCurIndex,
01089                                                bottomMostSwapIndex); 
01090         swapFlag = 0;
01091       }
01092     }
01093   } /* End of else clause (varStartIndex < numVars/2) */
01094 
01095 #ifdef _CAL_VERBOSE
01096   PrintBddProfileAfterReorder(bddManager);
01097 #endif
01098   
01099   if (CalBddIdNeedsRepacking(bddManager, origId)){
01100     if (swapFlag){
01101       if (varStartIndex >= (numVars >> 1)){
01102         CalBddPackNodesAfterReorderForSingleId(bddManager, 0,
01103                                                bestIndex, bestIndex); 
01104       }
01105       /*
01106       else if (bestIndex >= (numVars >> 1)){
01107         int i;
01108         int nodeCounter = 0;
01109         for (i=bestIndex; i<numVars; i++){
01110           nodeCounter +=
01111               bddManager->uniqueTable[bddManager->indexToId[i]]->numEntries;
01112         }
01113         if ((bddManager->numNodes - nodeCounter) >
01114             bddManager->numForwardedNodes){
01115             BddPackNodesAfterReorderForSingleId(bddManager, 1, bestIndex,
01116                                                  bottomMostSwapIndex);
01117         }
01118         else {
01119           BddSiftPerfromPhaseIV(bddManager, varStartIndex, bestIndex,
01120                                 bottomMostSwapIndex);
01121           BddPackNodesAfterReorderForSingleId(bddManager, 0,
01122                                                  bestIndex, bestIndex); 
01123         }
01124       }
01125       */
01126       else {
01127         /* Clean up - phase IV */
01128         BddSiftPerfromPhaseIV(bddManager, varStartIndex, bestIndex,
01129                               bottomMostSwapIndex);
01130         CalBddPackNodesAfterReorderForSingleId(bddManager, 0,
01131                                                bestIndex, bestIndex); 
01132       }
01133     }
01134     else {
01135       CalBddPackNodesAfterReorderForSingleId(bddManager, 0, bestIndex,
01136                                              bestIndex); 
01137     }
01138   }
01139   else if (swapFlag) {
01140     /* clean up - phase IV */
01141     BddSiftPerfromPhaseIV(bddManager, varStartIndex, bestIndex,
01142                           bottomMostSwapIndex);
01143   }
01144   Cal_Assert(CalCheckAllValidity(bddManager));
01145   
01146 #ifdef _CAL_VERBOSE
01147   printf("ID = %3d SI = %3d EI = %3d Nodes = %7d\n", origId,
01148          varStartIndex, bestIndex, bddManager->numNodes);
01149 #endif
01150   return bestIndex;
01151 }
01152 
01153   
01165 static void
01166 BddSiftPerfromPhaseIV(Cal_BddManager_t *bddManager, int varStartIndex,
01167                       int bestIndex, int bottomMostSwapIndex)
01168 {
01169   int varCurIndex, varId;
01170   
01171 
01172 /* We need to perform phase IV */
01173   varCurIndex = bestIndex-1;
01174   while (varCurIndex >= 0) {
01175     varId = bddManager->indexToId[varCurIndex];
01176     CalBddReorderFixCofactors(bddManager, varId);
01177     varCurIndex--;
01178   }
01179   if (bddManager->pipelineState == CREATE){
01180     /* There are some results computed in pipeline */
01181     CalBddReorderFixProvisionalNodes(bddManager);
01182   }
01183   CalBddReorderFixUserBddPtrs(bddManager);
01184   CalReorderAssociationFix(bddManager);
01185   if (varStartIndex >= (bddManager->numVars >> 1)){
01186     CalBddReorderReclaimForwardedNodes(bddManager, bestIndex, bestIndex);
01187   }
01188   else {
01189     CalBddReorderReclaimForwardedNodes(bddManager, bestIndex,
01190                                        bottomMostSwapIndex); 
01191   }
01192 }
01193 
01194 
01206 static void
01207 BddReorderVarWindow(Cal_BddManager bddManager, char *levels)
01208 {
01209   long i;
01210   int moved;
01211   int anySwapped;
01212   int even;
01213   int lastIndex = bddManager->numVars-1;
01214   
01215 #ifdef _CAL_VERBOSE
01216   for (i=0; i<bddManager->numVars; i++){
01217     fprintf(stdout, "%3d ", bddManager->indexToId[i]);
01218   }
01219   fprintf(stdout, "%8d\n", bddManager->numNodes);
01220 #endif
01221   for (i=0; i < bddManager->numVars-1; i++) levels[i]=1;
01222   even = 1;
01223   do {
01224     anySwapped=0;
01225     if (even){
01226       /*fprintf(stdout, "Downward Swap\n");*/
01227       for (i=0; i < bddManager->numVars-1; i++){
01228         if (levels[i]) {
01229           if (i < bddManager->numVars-2) {
01230             moved = BddReorderWindow3(bddManager, i, 0);
01231             if (bddManager->numForwardedNodes >
01232                 bddManager->maxForwardedNodes){   
01233               CofactorFixAndReclaimForwardedNodes(bddManager, 0,
01234                                                      i-1, 0, i+2);
01235               CalBddPackNodesForMultipleIds(bddManager,
01236                                          bddManager->indexToId[i], 3);
01237             }
01238           }
01239           else {
01240             moved = BddReorderWindow2(bddManager, i, 0);
01241           }
01242           if (moved){
01243             if (i > 0) {
01244               levels[i-1]=1;
01245               if (i > 1) levels[i-2]=1;
01246             }
01247             levels[i]=1;
01248             levels[i+1]=1;
01249             if (i < bddManager->numVars-2) {
01250               levels[i+2]=1;
01251               if (i < bddManager->numVars-3) {
01252                 levels[i+3]=1;
01253                 if (i < bddManager->numVars-4) levels[i+4]=1;
01254               }
01255             }
01256             anySwapped=1;
01257           }
01258           else {
01259             levels[i]=0;
01260           }
01261         }
01262       }
01263       /* new code added */
01264       for (i = bddManager->numVars-1; i >= 0; i--){
01265         CalBddReorderFixCofactors(bddManager, bddManager->indexToId[i]);
01266       }
01267       CalBddReorderFixUserBddPtrs(bddManager);
01268       if (bddManager->pipelineState == CREATE){
01269         /* There are some results computed in pipeline */
01270         CalBddReorderFixProvisionalNodes(bddManager);
01271       }
01272       CalReorderAssociationFix(bddManager);
01273       CalBddReorderReclaimForwardedNodes(bddManager, 0, lastIndex);
01274       /*even = 0;*/
01275     }
01276     else{
01277       /*fprintf(stdout, "Upward Swap\n");*/
01278       for (i=bddManager->numVars-1; i > 0; i--){
01279           /*
01280            * Fix the then and else cofactors. We need to fix it, even
01281            * if this level is not supposed to be moved.
01282            */
01283         if (i > 1) {
01284           CalBddReorderFixCofactors(bddManager,
01285                                  bddManager->indexToId[i-2]); 
01286         }
01287         else {
01288           CalBddReorderFixCofactors(bddManager,
01289                                  bddManager->indexToId[i-1]); 
01290         }
01291         if (levels[i]) {
01292           if (i > 1) {
01293             moved = BddReorderWindow3(bddManager, i-2, 1);
01294             if (bddManager->numForwardedNodes >
01295                 bddManager->maxForwardedNodes){ 
01296               CofactorFixAndReclaimForwardedNodes(bddManager, 0,
01297                                                   i-3, 0,
01298                                                   lastIndex); 
01299               CalBddPackNodesForMultipleIds(bddManager,
01300                                             bddManager->indexToId[i-2], 3);
01301             }
01302           }
01303           else {
01304             moved = BddReorderWindow2(bddManager, i-1, 1);
01305           }
01306           if (moved){
01307             if (i < bddManager->numVars-1) {
01308               levels[i+1]=1;
01309               if (i < bddManager->numVars-2) {
01310                 levels[i+2]=1;
01311                 if (i < bddManager->numVars-3) {
01312                   levels[i+3]=1;
01313                   if (i < bddManager->numVars-4) {
01314                     levels[i+4]=1;
01315                   }
01316                 }
01317               }
01318             }
01319             levels[i]=1;
01320             levels[i-1]=1;
01321             if (i > 1) {
01322               levels[i-2]=1;
01323             }
01324             anySwapped=1;
01325           }
01326           else {
01327             levels[i]=0;
01328           }
01329         }
01330       }
01331       even = 1;
01332       CalBddReorderFixUserBddPtrs(bddManager);
01333       if (bddManager->pipelineState == CREATE){
01334         /* There are some results computed in pipeline */
01335         CalBddReorderFixProvisionalNodes(bddManager);
01336       }
01337       CalReorderAssociationFix(bddManager);
01338       CalBddReorderReclaimForwardedNodes(bddManager, 0, lastIndex);
01339     }
01340   }
01341   while (anySwapped);
01342   if (!even){ /* Need to do pointer fixing */
01343     for (i = bddManager->numVars-1; i >= 0; i--){
01344       CalBddReorderFixCofactors(bddManager, bddManager->indexToId[i]);
01345     }
01346     CalBddReorderFixUserBddPtrs(bddManager);
01347     if (bddManager->pipelineState == CREATE){
01348       /* There are some results computed in pipeline */
01349       CalBddReorderFixProvisionalNodes(bddManager);
01350     }
01351     CalReorderAssociationFix(bddManager);
01352     CalBddReorderReclaimForwardedNodes(bddManager, 0, lastIndex);
01353   }
01354   Cal_Assert(CalCheckAllValidity(bddManager));
01355 }
01356 
01368 static int
01369 BddReorderWindow2(Cal_BddManager bddManager, long index, int directionFlag)
01370 {
01371   long curSize, startSize;
01372 
01373   startSize = bddManager->numNodes;
01374   BddReorderSwapVarIndex(bddManager, index, 0);
01375   curSize = bddManager->numNodes;
01376   if (curSize > startSize){
01377     BddReorderSwapVarIndex(bddManager, index, 0);
01378   }
01379   if (directionFlag){/* Upward window swap */
01380     BddReorderFixAndFreeForwardingNodes(bddManager,
01381                                         bddManager->indexToId[index],
01382                                         bddManager->numVars-index); 
01383   }
01384   else{
01385     BddReorderFixAndFreeForwardingNodes(bddManager,
01386                                         bddManager->indexToId[index], 2);
01387   }
01388   Cal_Assert(CalCheckValidityOfNodesForWindow(bddManager, index, 2));
01389   return (curSize < startSize);
01390 }
01391 
01403 static int
01404 BddReorderWindow3(Cal_BddManager bddManager, long index, int directionFlag)
01405 {
01406   int best;
01407   long curSize, bestSize;
01408   long origSize = bddManager->numNodes;
01409   
01410   /* 1 2 3 */
01411   best = 0;
01412   bestSize = bddManager->numNodes;
01413   BddReorderSwapVarIndex(bddManager, index, 0); 
01414   /* 2 1 3 */
01415   curSize = bddManager->numNodes;
01416   if (curSize < bestSize){
01417     best = 1;
01418     bestSize = curSize;
01419   }
01420   BddReorderSwapVarIndex(bddManager, index+1, 0);
01421   /* 2 3 1 */
01422   curSize = bddManager->numNodes;
01423   if (curSize < bestSize){
01424     best = 2;
01425     bestSize = curSize;
01426   }
01427   BddReorderSwapVarIndex(bddManager, index, 1);
01428   /* 3 2 1 */
01429   curSize = bddManager->numNodes;
01430   if (curSize <= bestSize){
01431     best = 3;
01432     bestSize = curSize;
01433   }
01434   BddReorderSwapVarIndex(bddManager, index+1, 0);
01435   /* 3 1 2 */
01436   curSize = bddManager->numNodes;
01437   if (curSize <= bestSize){
01438     best = 4;
01439     bestSize = curSize;
01440   }
01441   BddReorderSwapVarIndex(bddManager, index, 1);
01442   /* 1 3 2 */
01443   curSize = bddManager->numNodes;
01444   if (curSize <= bestSize){
01445     best = 5;
01446     bestSize = curSize;
01447   }
01448   switch (best) {
01449     case 0:
01450       BddReorderSwapVarIndex(bddManager, index+1, 0);
01451       break;
01452     case 1:
01453       BddReorderSwapVarIndex(bddManager, index+1, 0);
01454       BddReorderSwapVarIndex(bddManager, index, 1);
01455       break;
01456     case 2:
01457       BddReorderSwapVarIndex(bddManager, index, 0);
01458       BddReorderSwapVarIndex(bddManager, index+1, 0);
01459       BddReorderSwapVarIndex(bddManager, index, 1);
01460       break;
01461     case 3:
01462       BddReorderSwapVarIndex(bddManager, index, 0);
01463       BddReorderSwapVarIndex(bddManager, index+1, 0);
01464       break;
01465     case 4:
01466       BddReorderSwapVarIndex(bddManager, index, 0);
01467       break;
01468     case 5:
01469       break;
01470   }
01471   if ((best == 0) || (best == 3)){
01472     CalBddReorderFixCofactors(bddManager, bddManager->indexToId[index]);
01473   }
01474   if (directionFlag){/* Upward window swap */
01475     BddReorderFixAndFreeForwardingNodes(bddManager,
01476                                         bddManager->indexToId[index],
01477                                         bddManager->numVars-index); 
01478   }
01479   else{
01480     BddReorderFixAndFreeForwardingNodes(bddManager,
01481                                         bddManager->indexToId[index], 3);
01482   }
01483   Cal_Assert(CalCheckValidityOfNodesForWindow(bddManager, index, 3));
01484   return ((best > 0) && (origSize > bestSize));
01485 }
01486