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

00001 
00041 #include "calInt.h"
00042 
00043 /*---------------------------------------------------------------------------*/
00044 /* Constant declarations                                                     */
00045 /*---------------------------------------------------------------------------*/
00046 
00047 /*---------------------------------------------------------------------------*/
00048 /* Type declarations                                                         */
00049 /*---------------------------------------------------------------------------*/
00050 
00051 /*---------------------------------------------------------------------------*/
00052 /* Stucture declarations                                                     */
00053 /*---------------------------------------------------------------------------*/
00054 
00055 
00056 /*---------------------------------------------------------------------------*/
00057 /* Variable declarations                                                     */
00058 /*---------------------------------------------------------------------------*/
00059 
00060 /*---------------------------------------------------------------------------*/
00061 /* Macro declarations                                                        */
00062 /*---------------------------------------------------------------------------*/
00063 
00066 /*---------------------------------------------------------------------------*/
00067 /* Static function prototypes                                                */
00068 /*---------------------------------------------------------------------------*/
00069 
00070 static Cal_Bdd_t * BddArrayOpBF(Cal_BddManager_t * bddManager, Cal_Bdd_t* bddArray, int numFunction, CalOpProc_t calOpProc);
00071 static Cal_Bdd_t BddMultiwayOp(Cal_BddManager_t * bddManager, Cal_Bdd_t * calBddArray, int numBdds, CalOpProc_t op);
00072 static void BddArrayToRequestNodeListArray(Cal_BddManager_t * bddManager, Cal_Bdd_t * calBddArray, int numBdds);
00073 static int CeilLog2(int number);
00074 
00077 /*---------------------------------------------------------------------------*/
00078 /* Definition of exported functions                                          */
00079 /*---------------------------------------------------------------------------*/
00089 Cal_Bdd
00090 Cal_BddAnd(
00091   Cal_BddManager bddManager,
00092   Cal_Bdd  fUserBdd,
00093   Cal_Bdd  gUserBdd)
00094 {
00095   Cal_Bdd_t result;
00096   Cal_Bdd userResult;
00097   Cal_Bdd_t F, G;
00098 
00099   if (CalBddPreProcessing(bddManager, 2, fUserBdd, gUserBdd)){
00100     F = CalBddGetInternalBdd(bddManager, fUserBdd);
00101     G = CalBddGetInternalBdd(bddManager, gUserBdd);
00102     result = CalBddOpBF(bddManager, CalOpAnd, F, G);
00103   }
00104   else {
00105     return (Cal_Bdd)0;
00106   }
00107   userResult =  CalBddGetExternalBdd(bddManager, result);
00108   if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){
00109     Cal_BddFree(bddManager, userResult);
00110     Cal_BddManagerGC(bddManager);
00111     return (Cal_Bdd) 0;
00112   }
00113   return userResult;
00114 }
00115 
00125 Cal_Bdd
00126 Cal_BddNand(
00127   Cal_BddManager bddManager,
00128   Cal_Bdd fUserBdd,
00129   Cal_Bdd gUserBdd)
00130 {
00131   Cal_Bdd_t result;
00132   Cal_Bdd_t F, G;
00133   Cal_Bdd userResult;
00134   if (CalBddPreProcessing(bddManager, 2, fUserBdd, gUserBdd)){
00135     F = CalBddGetInternalBdd(bddManager, fUserBdd); 
00136     G = CalBddGetInternalBdd(bddManager, gUserBdd); 
00137     result = CalBddOpBF(bddManager, CalOpNand, F, G);
00138   }
00139   else{
00140     return (Cal_Bdd) 0;
00141   }
00142   userResult =  CalBddGetExternalBdd(bddManager, result);
00143   if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){
00144     Cal_BddFree(bddManager, userResult);
00145     Cal_BddManagerGC(bddManager);
00146     return (Cal_Bdd) 0;
00147   }
00148   return userResult;
00149 }
00150 
00160 Cal_Bdd
00161 Cal_BddOr(Cal_BddManager bddManager,
00162           Cal_Bdd fUserBdd,
00163           Cal_Bdd gUserBdd)
00164 {
00165   Cal_Bdd_t result;
00166   Cal_Bdd_t F, G;
00167   Cal_Bdd userResult;
00168   if (CalBddPreProcessing(bddManager, 2, fUserBdd, gUserBdd)){
00169     F = CalBddGetInternalBdd(bddManager, fUserBdd); 
00170     G = CalBddGetInternalBdd(bddManager, gUserBdd); 
00171     result = CalBddOpBF(bddManager, CalOpOr, F, G);
00172   }
00173   else{
00174     return (Cal_Bdd) 0;
00175   }
00176   userResult =  CalBddGetExternalBdd(bddManager, result);
00177   if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){
00178     Cal_BddFree(bddManager, userResult);
00179     Cal_BddManagerGC(bddManager);
00180     return (Cal_Bdd) 0;
00181   }
00182   return userResult;
00183 }
00184 
00194 Cal_Bdd
00195 Cal_BddNor(Cal_BddManager bddManager,
00196            Cal_Bdd fUserBdd,
00197            Cal_Bdd gUserBdd)
00198 {
00199   Cal_Bdd_t result;
00200   Cal_Bdd userResult;
00201   Cal_Bdd_t F, G;
00202   if (CalBddPreProcessing(bddManager, 2, fUserBdd, gUserBdd)){
00203     F = CalBddGetInternalBdd(bddManager, fUserBdd); 
00204     G = CalBddGetInternalBdd(bddManager, gUserBdd); 
00205     result = CalBddOpBF(bddManager, CalOpOr, F, G);
00206     CalBddNot(result, result);
00207   }
00208   else{
00209     return (Cal_Bdd) 0;
00210   }
00211   userResult =  CalBddGetExternalBdd(bddManager, result);
00212   if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){
00213     Cal_BddFree(bddManager, userResult);
00214     Cal_BddManagerGC(bddManager);
00215     return (Cal_Bdd) 0;
00216   }
00217   return userResult;
00218 }
00219 
00229 Cal_Bdd
00230 Cal_BddXor(Cal_BddManager bddManager,
00231            Cal_Bdd fUserBdd,
00232            Cal_Bdd gUserBdd)
00233 {
00234   Cal_Bdd_t result;
00235   Cal_Bdd userResult;
00236   Cal_Bdd_t F, G;
00237   if (CalBddPreProcessing(bddManager, 2, fUserBdd, gUserBdd)){
00238     F = CalBddGetInternalBdd(bddManager, fUserBdd); 
00239     G = CalBddGetInternalBdd(bddManager, gUserBdd); 
00240     result = CalBddOpBF(bddManager, CalOpXor, F, G);
00241   }
00242   else{
00243     return (Cal_Bdd) 0;
00244   }
00245   userResult =  CalBddGetExternalBdd(bddManager, result);
00246   if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){
00247     Cal_BddFree(bddManager, userResult);
00248     Cal_BddManagerGC(bddManager);
00249     return (Cal_Bdd) 0;
00250   }
00251   return userResult;
00252 }
00253 
00263 Cal_Bdd
00264 Cal_BddXnor(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd)
00265 {
00266   Cal_Bdd_t result;
00267   Cal_Bdd userResult;
00268   Cal_Bdd_t F, G;
00269   if (CalBddPreProcessing(bddManager, 2, fUserBdd, gUserBdd)){
00270     F = CalBddGetInternalBdd(bddManager, fUserBdd); 
00271     G = CalBddGetInternalBdd(bddManager, gUserBdd); 
00272     result = CalBddOpBF(bddManager, CalOpXor, F, G);
00273     CalBddNot(result, result);
00274   }
00275   else{
00276     return (Cal_Bdd) 0;
00277   }
00278   userResult =  CalBddGetExternalBdd(bddManager, result);
00279   if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){
00280     Cal_BddFree(bddManager, userResult);
00281     Cal_BddManagerGC(bddManager);
00282     return (Cal_Bdd) 0;
00283   }
00284   return userResult;
00285 }
00286 
00302 Cal_Bdd *
00303 Cal_BddPairwiseAnd(Cal_BddManager bddManager, Cal_Bdd *userBddArray)
00304 {
00305   int i, num;
00306   Cal_Bdd_t *bddArray;
00307   Cal_Bdd_t *resultArray;
00308   Cal_Bdd userBdd;
00309   Cal_Bdd *userResultArray;
00310  
00311   for (num = 0; (userBdd = userBddArray[num]); num++){
00312     if (CalBddPreProcessing(bddManager, 1, userBdd) == 0){
00313       return Cal_Nil(Cal_Bdd);
00314     }
00315   }
00316   if ((num == 0) || (num%2 != 0)){
00317     fprintf(stdout,"Odd number of arguments passed to array AND\n");
00318     return Cal_Nil(Cal_Bdd);
00319   }
00320   bddArray = Cal_MemAlloc(Cal_Bdd_t, num);
00321   for (i = 0; i < num; i++){
00322     bddArray[i] = CalBddGetInternalBdd(bddManager, userBddArray[i]);
00323   }
00324   resultArray =  BddArrayOpBF(bddManager, bddArray, num, CalOpAnd);
00325   userResultArray = Cal_MemAlloc(Cal_Bdd, num/2);
00326   for (i=0; i<num/2; i++){
00327     userResultArray[i] = CalBddGetExternalBdd(bddManager, resultArray[i]);
00328   }
00329   Cal_MemFree(bddArray);
00330   Cal_MemFree(resultArray);
00331   if (CalBddPostProcessing(bddManager)  == CAL_BDD_OVERFLOWED){
00332     for (i=0; i<num/2; i++){
00333       Cal_BddFree(bddManager, userResultArray[i]);
00334       userResultArray[i] = (Cal_Bdd) 0;
00335     }
00336     Cal_BddManagerGC(bddManager);
00337     return userResultArray;
00338   }
00339   return userResultArray;
00340 }
00341 
00357 Cal_Bdd *
00358 Cal_BddPairwiseOr(Cal_BddManager bddManager, Cal_Bdd *userBddArray)
00359 {
00360   int i, num=0;
00361   Cal_Bdd_t *bddArray;
00362   Cal_Bdd_t *resultArray;
00363   Cal_Bdd userBdd;
00364   Cal_Bdd *userResultArray;
00365  
00366   for (num = 0; (userBdd = userBddArray[num]); num++){
00367     if (CalBddPreProcessing(bddManager, 1, userBdd) == 0){
00368       return Cal_Nil(Cal_Bdd);
00369     }
00370   }
00371   if ((num == 0) || (num%2 != 0)){
00372     fprintf(stdout,"Odd number of arguments passed to array OR\n");
00373     return Cal_Nil(Cal_Bdd);
00374   }
00375   bddArray = Cal_MemAlloc(Cal_Bdd_t, num);
00376   for (i = 0; i < num; i++){
00377     bddArray[i] = CalBddGetInternalBdd(bddManager, userBddArray[i]);
00378   }
00379   resultArray =  BddArrayOpBF(bddManager, bddArray, num, CalOpOr);
00380   userResultArray = Cal_MemAlloc(Cal_Bdd, num/2);
00381   for (i=0; i<num/2; i++){
00382     userResultArray[i] = CalBddGetExternalBdd(bddManager, resultArray[i]);
00383   }
00384   Cal_MemFree(bddArray);
00385   Cal_MemFree(resultArray);
00386   return userResultArray;
00387 }
00388 
00404 Cal_Bdd *
00405 Cal_BddPairwiseXor(Cal_BddManager bddManager, Cal_Bdd *userBddArray)
00406 {
00407   int i, num=0;
00408   Cal_Bdd_t *bddArray;
00409   Cal_Bdd_t *resultArray;
00410   Cal_Bdd userBdd;
00411   Cal_Bdd *userResultArray;
00412  
00413   for (num = 0; (userBdd = userBddArray[num]); num++){
00414     if (CalBddPreProcessing(bddManager, 1, userBdd) == 0){
00415       return Cal_Nil(Cal_Bdd);
00416     }
00417   }
00418   if ((num == 0) || (num%2 != 0)){
00419     fprintf(stdout,"Odd number of arguments passed to array OR\n");
00420     return Cal_Nil(Cal_Bdd);
00421   }
00422   bddArray = Cal_MemAlloc(Cal_Bdd_t, num);
00423   for (i = 0; i < num; i++){
00424     bddArray[i] = CalBddGetInternalBdd(bddManager, userBddArray[i]);
00425   }
00426   resultArray =  BddArrayOpBF(bddManager, bddArray, num, CalOpXor);
00427   userResultArray = Cal_MemAlloc(Cal_Bdd, num/2);
00428   for (i=0; i<num/2; i++){
00429     userResultArray[i] = CalBddGetExternalBdd(bddManager, resultArray[i]);
00430   }
00431   Cal_MemFree(bddArray);
00432   Cal_MemFree(resultArray);
00433   return userResultArray;
00434 }
00435 
00436 
00437 
00447 Cal_Bdd
00448 Cal_BddMultiwayAnd(Cal_BddManager bddManager, Cal_Bdd *userBddArray)
00449 {
00450   int i, numBdds = 0;
00451   Cal_Bdd_t result;
00452   Cal_Bdd_t *calBddArray;
00453   Cal_Bdd userBdd;
00454 
00455   for (numBdds  = 0; (userBdd = userBddArray[numBdds]); numBdds++){
00456     if (CalBddPreProcessing(bddManager, 1, userBdd) == 0){
00457       return (Cal_Bdd) 0;
00458     }
00459   }
00460   
00461   if (numBdds == 0){
00462     CalBddWarningMessage("Multiway AND called with 0 length array");
00463     return (Cal_Bdd) 0;
00464   }
00465   else if (numBdds == 1){
00466     return Cal_BddIdentity(bddManager, userBddArray[0]);
00467   }
00468   else{
00469     calBddArray = Cal_MemAlloc(Cal_Bdd_t, numBdds+1);
00470     for (i = 0; i < numBdds; i++){
00471       calBddArray[i] = CalBddGetInternalBdd(bddManager, userBddArray[i]);
00472     }
00473     result = BddMultiwayOp(bddManager, calBddArray, numBdds, CalOpAnd);
00474     Cal_MemFree(calBddArray);
00475   }
00476   return CalBddGetExternalBdd(bddManager, result);
00477 }
00478  
00488 Cal_Bdd
00489 Cal_BddMultiwayOr(Cal_BddManager bddManager, Cal_Bdd *userBddArray)
00490 {
00491   int i, numBdds = 0;
00492   Cal_Bdd_t result;
00493   Cal_Bdd_t *calBddArray;
00494   Cal_Bdd userBdd;
00495 
00496   for (numBdds = 0; (userBdd = userBddArray[numBdds]); numBdds++){
00497     if (CalBddPreProcessing(bddManager, 1, userBdd) == 0){
00498       return (Cal_Bdd) 0;
00499     }
00500   }
00501   
00502   if (numBdds == 0){
00503     CalBddWarningMessage("Multiway OR called with 0 length array");
00504     return (Cal_Bdd) 0;
00505   }
00506   else if (numBdds == 1){
00507     return Cal_BddIdentity(bddManager, userBddArray[0]);
00508   }
00509   else{
00510     calBddArray = Cal_MemAlloc(Cal_Bdd_t, numBdds+1);
00511     for (i = 0; i < numBdds; i++){
00512       calBddArray[i] = CalBddGetInternalBdd(bddManager, userBddArray[i]);
00513     }
00514     result = BddMultiwayOp(bddManager, calBddArray, numBdds, CalOpOr);
00515     Cal_MemFree(calBddArray);
00516   }
00517   return CalBddGetExternalBdd(bddManager, result);
00518 }
00519  
00529 Cal_Bdd
00530 Cal_BddMultiwayXor(Cal_BddManager bddManager, Cal_Bdd *userBddArray)
00531 {
00532   int i, numBdds = 0;
00533   Cal_Bdd_t result;
00534   Cal_Bdd_t *calBddArray;
00535   Cal_Bdd userBdd;
00536 
00537   for (numBdds = 0; (userBdd = userBddArray[numBdds]); numBdds++){
00538     if (CalBddPreProcessing(bddManager, 1, userBdd) == 0){
00539       return (Cal_Bdd) 0;
00540     }
00541   }
00542   
00543   if (numBdds == 0){
00544     CalBddWarningMessage("Multiway OR called with 0 length array");
00545     return (Cal_Bdd) 0;
00546   }
00547   else if (numBdds == 1){
00548     return Cal_BddIdentity(bddManager, userBddArray[0]);
00549   }
00550   else{
00551     calBddArray = Cal_MemAlloc(Cal_Bdd_t, numBdds+1);
00552     for (i = 0; i < numBdds; i++){
00553       calBddArray[i] = CalBddGetInternalBdd(bddManager, userBddArray[i]);
00554     }
00555     result = BddMultiwayOp(bddManager, calBddArray, numBdds, CalOpXor);
00556     Cal_MemFree(calBddArray);
00557   }
00558   return CalBddGetExternalBdd(bddManager, result);
00559 }
00560 
00561 
00562 /*---------------------------------------------------------------------------*/
00563 /* Definition of internal functions                                          */
00564 /*---------------------------------------------------------------------------*/
00565 
00566 
00581 void
00582 CalRequestNodeListArrayOp(Cal_BddManager_t * bddManager,
00583                           CalRequestNode_t ** requestNodeListArray,
00584                           CalOpProc_t calOpProc)
00585 {
00586   CalRequestNode_t *requestNode;
00587   CalRequest_t F, G, result;
00588   int pipeDepth, bddId, bddIndex;
00589   CalHashTable_t **reqQueAtPipeDepth, *hashTable, *uniqueTableForId;
00590   CalHashTable_t ***reqQue = bddManager->reqQue;
00591   
00592   /* ReqQueInsertUsingReqListArray */
00593   for(pipeDepth = 0; pipeDepth < bddManager->depth; pipeDepth++){
00594     reqQueAtPipeDepth = reqQue[pipeDepth];
00595     for(requestNode = requestNodeListArray[pipeDepth];
00596         requestNode != Cal_Nil(CalRequestNode_t);
00597         requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
00598       CalRequestNodeGetF(requestNode, F);
00599       CalRequestIsForwardedTo(F);
00600       CalRequestNodeGetG(requestNode, G);
00601       CalRequestIsForwardedTo(G);
00602       if((*calOpProc)(bddManager, F, G, &result) == 0){
00603         CalBddNormalize(F, G);
00604         CalBddGetMinId2(bddManager, F, G, bddId);
00605         CalHashTableFindOrAdd(reqQueAtPipeDepth[bddId], F, G, &result);
00606       }
00607       CalRequestNodePutThenRequest(requestNode, result);
00608       CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
00609     }
00610   }
00611 
00612   /* ReqQueApply */
00613   for(bddIndex = 0; bddIndex < bddManager->numVars; bddIndex++){
00614     bddId = bddManager->indexToId[bddIndex];
00615     for(pipeDepth = 0; pipeDepth < bddManager->depth; pipeDepth++){
00616       reqQueAtPipeDepth = reqQue[pipeDepth];
00617       hashTable = reqQueAtPipeDepth[bddId];
00618       if(hashTable->numEntries){
00619         CalHashTableApply(bddManager, hashTable, reqQueAtPipeDepth, calOpProc);
00620       }
00621     }
00622   }
00623 
00624 #ifdef COMPUTE_MEMORY_OVERHEAD
00625   {
00626     calNumEntriesAfterApply = 0;
00627     for(bddIndex = 0; bddIndex < bddManager->numVars; bddIndex++){
00628       bddId = bddManager->indexToId[bddIndex];
00629       for(pipeDepth = 0; pipeDepth < bddManager->depth; pipeDepth++){
00630         reqQueAtPipeDepth = reqQue[pipeDepth];
00631         hashTable = reqQueAtPipeDepth[bddId];
00632         calNumEntriesAfterApply += hashTable->numEntries;
00633       }
00634     }
00635   }
00636 #endif
00637 
00638   /* ReqQueReduce */
00639   for(bddIndex = bddManager->numVars - 1; bddIndex >= 0; bddIndex--){
00640     bddId = bddManager->indexToId[bddIndex];
00641     uniqueTableForId = bddManager->uniqueTable[bddId];
00642     for(pipeDepth = 0; pipeDepth < bddManager->depth; pipeDepth++){
00643       hashTable = reqQue[pipeDepth][bddId];
00644       if(hashTable->numEntries){
00645         CalHashTableReduce(bddManager, hashTable, uniqueTableForId);
00646       }
00647     }
00648   }
00649 
00650 #ifdef COMPUTE_MEMORY_OVERHEAD
00651   {
00652     CalRequestNode_t *requestNode;
00653     calNumEntriesAfterReduce = 0;
00654     for(bddIndex = 0; bddIndex < bddManager->numVars; bddIndex++){
00655       CalRequestNode_t *next;
00656       Cal_BddId_t bddId;
00657       bddId = bddManager->indexToId[bddIndex];
00658       for(pipeDepth = 0; pipeDepth < bddManager->depth; pipeDepth++){
00659         hashTable = reqQue[pipeDepth][bddId];
00660         for (requestNode = hashTable->requestNodeList;
00661              requestNode != Cal_Nil(CalRequestNode_t); requestNode = next){
00662           next = CalRequestNodeGetNextRequestNode(requestNode);
00663           calNumEntriesAfterReduce++;
00664         }
00665       }
00666     }
00667     calAfterReduceToAfterApplyNodesRatio =
00668         ((double)calNumEntriesAfterReduce)/((double)calNumEntriesAfterApply); 
00669     calAfterReduceToUniqueTableNodesRatio = 
00670         ((double)calNumEntriesAfterReduce)/((double)bddManager->numNodes);
00671   }
00672 #endif
00673 
00674   /* ReqListArrayReqForward */
00675   for(pipeDepth = 0; pipeDepth < bddManager->depth; pipeDepth++){
00676     for(requestNode = requestNodeListArray[pipeDepth];
00677         requestNode != Cal_Nil(CalRequestNode_t);
00678         requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
00679       CalRequestNodeGetThenRequest(requestNode, result);
00680       CalRequestIsForwardedTo(result);
00681       Cal_Assert(CalBddIsForwarded(result) == 0);
00682       CalRequestNodePutThenRequest(requestNode, result);
00683     }
00684   }
00685 
00686   /* ReqQueCleanUp */
00687   for(pipeDepth = 0; pipeDepth < bddManager->depth; pipeDepth++){
00688     reqQueAtPipeDepth = reqQue[pipeDepth];
00689     for(bddId = 1; bddId <= bddManager->numVars; bddId++){
00690       CalHashTableCleanUp(reqQueAtPipeDepth[bddId]);
00691     }
00692   }
00693 }
00694 
00704 Cal_Bdd_t
00705 CalBddOpBF(
00706   Cal_BddManager_t * bddManager,
00707   CalOpProc_t calOpProc,
00708   Cal_Bdd_t  F,
00709   Cal_Bdd_t  G)
00710 {
00711   Cal_Bdd_t result;
00712   Cal_BddId_t minId, bddId;
00713   /*Cal_BddIndex_t minIndex; Commented out because of the problem on alpha*/ 
00714   int minIndex;
00715   int bddIndex;
00716   CalHashTable_t *hashTable, **hashTableArray, *uniqueTableForId;
00717   
00718   if (calOpProc(bddManager, F, G, &result)){
00719     return result;
00720   }
00721   CalBddGetMinIdAndMinIndex(bddManager, F, G, minId, minIndex);
00722   hashTableArray = bddManager->reqQue[0];
00723   CalHashTableFindOrAdd(hashTableArray[minId], F, G, &result);
00724   
00725   /* ReqQueApply */
00726   for(bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
00727     bddId = bddManager->indexToId[bddIndex];
00728     hashTable = hashTableArray[bddId];
00729     if(hashTable->numEntries){
00730       CalHashTableApply(bddManager, hashTable, hashTableArray, calOpProc);
00731     }
00732   }
00733 #ifdef COMPUTE_MEMORY_OVERHEAD
00734   {
00735     calNumEntriesAfterApply = 0;
00736     for(bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
00737       bddId = bddManager->indexToId[bddIndex];
00738       hashTable = hashTableArray[bddId];
00739       calNumEntriesAfterApply += hashTable->numEntries;
00740     }
00741   }
00742 #endif
00743   /* ReqQueReduce */
00744   for(bddIndex = bddManager->numVars - 1; bddIndex >= minIndex; bddIndex--){
00745     bddId = bddManager->indexToId[bddIndex];
00746     uniqueTableForId = bddManager->uniqueTable[bddId];
00747     hashTable = hashTableArray[bddId];
00748     if(hashTable->numEntries){
00749       CalHashTableReduce(bddManager, hashTable, uniqueTableForId);
00750     }
00751   }
00752   CalRequestIsForwardedTo(result);
00753 
00754 #ifdef COMPUTE_MEMORY_OVERHEAD
00755   {
00756     CalRequestNode_t *requestNode;
00757     calNumEntriesAfterReduce = 0;
00758     for(bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
00759       CalRequestNode_t *next;
00760       Cal_BddId_t bddId;
00761       
00762       bddId = bddManager->indexToId[bddIndex];
00763       hashTable = hashTableArray[bddId];
00764       for (requestNode = hashTable->requestNodeList; requestNode !=
00765                                                          Cal_Nil(CalRequestNode_t);
00766                                                      requestNode = next){
00767         next = CalRequestNodeGetNextRequestNode(requestNode);
00768         calNumEntriesAfterReduce++;
00769       }
00770     }
00771     calAfterReduceToAfterApplyNodesRatio =
00772         ((double)calNumEntriesAfterReduce)/((double)calNumEntriesAfterApply); 
00773     calAfterReduceToUniqueTableNodesRatio = 
00774         ((double)calNumEntriesAfterReduce)/((double)bddManager->numNodes);
00775   }
00776 #endif
00777 
00778   /* Clean up */
00779   for(bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
00780     bddId = bddManager->indexToId[bddIndex];
00781     CalHashTableCleanUp(hashTableArray[bddId]);
00782   }
00783   return result;
00784 }
00785 
00786 
00787 
00788 /*---------------------------------------------------------------------------*/
00789 /* Definition of static functions                                            */
00790 /*---------------------------------------------------------------------------*/
00798 static Cal_Bdd_t *
00799 BddArrayOpBF(Cal_BddManager_t * bddManager, Cal_Bdd_t*  bddArray,
00800                 int numFunction, CalOpProc_t calOpProc)
00801 {
00802   Cal_BddId_t minId, bddId;
00803   /*Cal_BddIndex_t minIndex = 0;*/
00804   int minIndex = 0;
00805   int bddIndex;
00806   CalHashTable_t *hashTable, **hashTableArray, *uniqueTableForId;
00807   Cal_Bdd_t F, G, result;
00808   int numPairs = numFunction/2;
00809   Cal_Bdd_t *resultArray = Cal_MemAlloc(Cal_Bdd_t, numPairs);
00810   int i;
00811   
00812   hashTableArray = bddManager->reqQue[0];
00813   for (i=0; i<numPairs; i++){
00814     F = bddArray[i<<1];
00815     G = bddArray[(i<<1)+1];
00816     if ((*calOpProc)(bddManager, F, G, &result) == 0){
00817       CalBddGetMinIdAndMinIndex(bddManager, F, G, minId, minIndex);
00818       CalHashTableFindOrAdd(hashTableArray[minId], F, G, &result);
00819     }
00820     resultArray[i] = result;
00821   }
00822   
00823   
00824   /* ReqQueApply */
00825   for(bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
00826     bddId = bddManager->indexToId[bddIndex];
00827     hashTable = hashTableArray[bddId];
00828     if(hashTable->numEntries){
00829       CalHashTableApply(bddManager, hashTable, hashTableArray, calOpProc);
00830     }
00831   }
00832 
00833   /* ReqQueReduce */
00834   for(bddIndex = bddManager->numVars - 1; bddIndex >= minIndex; bddIndex--){
00835     bddId = bddManager->indexToId[bddIndex];
00836     uniqueTableForId = bddManager->uniqueTable[bddId];
00837     hashTable = hashTableArray[bddId];
00838     if(hashTable->numEntries){
00839       CalHashTableReduce(bddManager, hashTable, uniqueTableForId);
00840     }
00841   }
00842   for (i=0; i<numPairs; i++){
00843     CalRequestIsForwardedTo(resultArray[i]);
00844   }
00845   /* Clean up */
00846   for(bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
00847     bddId = bddManager->indexToId[bddIndex];
00848     CalHashTableCleanUp(hashTableArray[bddId]);
00849   }
00850   return resultArray;
00851 }
00852 
00862 static Cal_Bdd_t
00863 BddMultiwayOp(Cal_BddManager_t * bddManager, Cal_Bdd_t * calBddArray,
00864               int  numBdds, CalOpProc_t op)
00865 {
00866   int pipeDepth;
00867   CalRequestNode_t *requestNode;
00868   Cal_Bdd_t result;
00869   
00870   BddArrayToRequestNodeListArray(bddManager, calBddArray, numBdds);
00871   CalRequestNodeListArrayOp(bddManager, bddManager->requestNodeListArray, op);
00872   for(pipeDepth = 0; pipeDepth < bddManager->depth-1; pipeDepth++){
00873     CalRequestNode_t *next;
00874     for(requestNode = bddManager->requestNodeListArray[pipeDepth];
00875         requestNode != Cal_Nil(CalRequestNode_t); requestNode = next){
00876       next = CalRequestNodeGetNextRequestNode(requestNode);
00877       CalNodeManagerFreeNode(bddManager->nodeManagerArray[0],
00878                              requestNode);
00879     }
00880     bddManager->requestNodeListArray[pipeDepth] =
00881         Cal_Nil(CalRequestNode_t);
00882   }
00883   requestNode = bddManager->requestNodeListArray[bddManager->depth-1];
00884   bddManager->requestNodeListArray[bddManager->depth-1] =
00885       Cal_Nil(CalRequestNode_t); 
00886   CalRequestNodeGetThenRequest(requestNode, result); 
00887   CalNodeManagerFreeNode(bddManager->nodeManagerArray[0],
00888                          requestNode);
00889   return result;
00890 }
00891 
00892 
00903 static void
00904 BddArrayToRequestNodeListArray(
00905   Cal_BddManager_t * bddManager,
00906   Cal_Bdd_t * calBddArray,
00907   int  numBdds)
00908 {
00909   int i;
00910   Cal_Bdd_t lastBdd;
00911   CalRequestNode_t *even, *odd, *requestNode, *requestNodeList, *head;
00912   
00913   bddManager->depth = CeilLog2(numBdds);
00914   if (bddManager->depth > 10){
00915     CalBddFatalMessage("Don't be stooopid\n, Use lesser depth\n");
00916   }
00917     
00918   if (bddManager->depth > bddManager->maxDepth){
00919     /* Need to reallocate the memory for reqQue and
00920        requestNodeListArray */
00921     int oldMaxDepth = bddManager->maxDepth;
00922     bddManager->maxDepth = bddManager->depth;
00923     
00924     for (i=0; i<bddManager->maxDepth; i++){
00925       bddManager->requestNodeListArray[i] = Cal_Nil(CalRequestNode_t);
00926     }
00927 
00928     bddManager->reqQue = Cal_MemRealloc(CalHashTable_t **, bddManager->reqQue,
00929                                  bddManager->maxDepth);
00930     for (i=oldMaxDepth; i<bddManager->maxDepth; i++){
00931       int j;
00932       bddManager->reqQue[i] = Cal_MemAlloc(CalHashTable_t *, bddManager->maxNumVars+1);
00933       for (j=0; j<bddManager->numVars+1; j++){
00934         bddManager->reqQue[i][j] = CalHashTableInit(bddManager, j);
00935       }
00936     }
00937   }
00938   lastBdd = bddManager->bddNull;
00939   if (numBdds%2 != 0){/* Odd number of Bdd's */
00940     lastBdd = calBddArray[numBdds-1];
00941   }
00942   requestNodeList = bddManager->requestNodeListArray[0];
00943   for (i=0; i<numBdds/2; i++){
00944     CalNodeManagerAllocNode(bddManager->nodeManagerArray[0], requestNode);
00945     CalRequestNodePutF(requestNode, calBddArray[2*i]);
00946     CalRequestNodePutG(requestNode, calBddArray[2*i+1]);
00947     CalRequestNodePutNextRequestNode(requestNode, requestNodeList);
00948     requestNodeList = requestNode;
00949   }
00950   bddManager->requestNodeListArray[0] = requestNodeList;
00951 
00952   for (i=1; i<bddManager->depth; i++){
00953     requestNodeList = bddManager->requestNodeListArray[i];
00954     head = bddManager->requestNodeListArray[i-1];
00955     while ((odd = head) && (even = head->nextBddNode)){
00956       CalNodeManagerAllocNode(bddManager->nodeManagerArray[0], requestNode);
00957       /*
00958        * We don't have to worry about the Id's attached with
00959        * the requestNode or with the then and else part of it.
00960        */
00961       CalRequestNodePutThenRequestNode(requestNode, odd);
00962       CalRequestNodePutElseRequestNode(requestNode, even);
00963       CalRequestNodePutNextRequestNode(requestNode, requestNodeList);
00964       requestNodeList = requestNode;
00965       head = CalRequestNodeGetNextRequestNode(even);
00966     }
00967     if (odd != Cal_Nil(CalRequestNode_t)){/* There is an  odd node at this
00968                                       level */
00969       if (CalBddIsBddNull(bddManager,lastBdd)){ /* There are no odd nodes
00970                                                  * from previous levels, so
00971                                                  * make this an odd node.
00972                                                  */
00973         CalBddPutBddNode(lastBdd, odd);
00974       }
00975       else{ /* There exists an odd node, so make a pair now. */
00976         CalNodeManagerAllocNode(bddManager->nodeManagerArray[0], requestNode);
00977         CalRequestNodePutThenRequestNode(requestNode, odd);
00978         CalRequestNodePutElseRequest(requestNode, lastBdd);
00979         CalRequestNodePutNextRequestNode(requestNode, requestNodeList);
00980         lastBdd = bddManager->bddNull;
00981         requestNodeList = requestNode;
00982       }
00983     }
00984     bddManager->requestNodeListArray[i] = requestNodeList;
00985   }
00986 }
00987 
00988 
00989 
01001 static int
01002 CeilLog2(
01003   int  number)
01004 {
01005   int num, count;
01006   for (num=number, count=0; num > 1; num >>= 1, count++);
01007   if ((1 << count) != number) count++;
01008   return count;
01009 }
01010 
01011 
01012   
01013 
01014 
01015