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

00001 
00040 #include "calInt.h"
00041 
00042 /*---------------------------------------------------------------------------*/
00043 /* Constant declarations                                                     */
00044 /*---------------------------------------------------------------------------*/
00045 
00046 #define DEFAULT_EXIST_HASH_TABLE_SIZE_INDEX 4
00047 #define DEFAULT_EXIST_HASH_TABLE_SIZE 16
00048 
00049 /*---------------------------------------------------------------------------*/
00050 /* Type declarations                                                         */
00051 /*---------------------------------------------------------------------------*/
00052 
00053 
00054 /*---------------------------------------------------------------------------*/
00055 /* Stucture declarations                                                     */
00056 /*---------------------------------------------------------------------------*/
00057 
00058 
00059 /*---------------------------------------------------------------------------*/
00060 /* Variable declarations                                                     */
00061 /*---------------------------------------------------------------------------*/
00062 
00063 
00064 /*---------------------------------------------------------------------------*/
00065 /* Macro declarations                                                        */
00066 /*---------------------------------------------------------------------------*/
00067 
00068 
00071 /*---------------------------------------------------------------------------*/
00072 /* Static function prototypes                                                */
00073 /*---------------------------------------------------------------------------*/
00074 
00075 static Cal_Bdd_t BddExistsStep(Cal_BddManager_t * bddManager, Cal_Bdd_t f, unsigned short opCode, CalAssociation_t *association);
00076 static Cal_Bdd_t BddRelProdStep(Cal_BddManager_t * bddManager, Cal_Bdd_t f, Cal_Bdd_t g, unsigned short opCode, CalAssociation_t *assoc);
00077 static Cal_Bdd_t BddDFStep(Cal_BddManager_t * bddManager, Cal_Bdd_t f, Cal_Bdd_t g, CalOpProc_t calOpProc, unsigned short opCode);
00078 static void HashTableApply(Cal_BddManager_t * bddManager, CalHashTable_t * hashTable, CalHashTable_t ** reqQueAtPipeDepth, CalOpProc_t calOpProc, unsigned long opCode);
00079 static void HashTableReduce(Cal_BddManager_t * bddManager, CalHashTable_t * hashTable, CalHashTable_t * uniqueTableForId);
00080 static void BddExistsApply(Cal_BddManager_t *bddManager, int quantifying, CalHashTable_t *existHashTable, CalHashTable_t **existHashTableArray, CalOpProc1_t calOpProc, unsigned short opCode, CalAssociation_t *assoc);
00081 static void BddExistsBFAux(Cal_BddManager_t *bddManager, int minIndex, CalHashTable_t **existHashTableArray, CalHashTable_t **orHashTableArray, CalOpProc1_t calOpProc, unsigned short opCode, CalAssociation_t *assoc);
00082 static void BddExistsReduce(Cal_BddManager_t *bddManager, CalHashTable_t *existHashTable, CalHashTable_t **existHashTableArray, CalHashTable_t **orHashTableArray, unsigned short opCode, CalAssociation_t *association);
00083 static Cal_Bdd_t BddExistsBFPlusDF(Cal_BddManager_t *bddManager, Cal_Bdd_t f, unsigned short opCode, CalAssociation_t *association);
00084 static void BddRelProdApply(Cal_BddManager_t *bddManager, int quantifying, CalHashTable_t *relProdHashTable, CalHashTable_t **relProdHashTableArray, CalHashTable_t **andHashTableArray, CalOpProc_t calOpProc, unsigned short opCode, CalAssociation_t *assoc);
00085 static void BddRelProdReduce(Cal_BddManager_t *bddManager, CalHashTable_t *relProdHashTable, CalHashTable_t **relProdHashTableArray, CalHashTable_t **andHashTableArray, CalHashTable_t **orHashTableArray, unsigned short opCode, CalAssociation_t *assoc);
00086 static void BddRelProdBFAux(Cal_BddManager_t *bddManager, int minIndex, CalHashTable_t **relProdHashTableArray, CalHashTable_t **andHashTableArray, CalHashTable_t **orHashTableArray, unsigned short opCode, CalAssociation_t *assoc);
00087 static Cal_Bdd_t BddRelProdBFPlusDF(Cal_BddManager_t * bddManager, Cal_Bdd_t f, Cal_Bdd_t g, unsigned short opCode, CalAssociation_t *association);
00088 
00092 /*---------------------------------------------------------------------------*/
00093 /* Definition of exported functions                                          */
00094 /*---------------------------------------------------------------------------*/
00109 Cal_Bdd
00110 Cal_BddExists(Cal_BddManager bddManager, Cal_Bdd fUserBdd)
00111 {
00112   Cal_Bdd_t result;
00113   Cal_Bdd userResult;
00114 
00115   if (CalBddPreProcessing(bddManager, 1, fUserBdd)){
00116     Cal_Bdd_t f = CalBddGetInternalBdd(bddManager, fUserBdd);
00117     CalAssociation_t *assoc = bddManager->currentAssociation;
00118     unsigned short opCode;
00119     
00120     if (assoc->id == -1){
00121       opCode = bddManager->tempOpCode--;
00122     }
00123     else {
00124       opCode = CAL_OP_QUANT + assoc->id;
00125     }
00126     if (bddManager->numNodes <= CAL_LARGE_BDD){
00127       /* If number of nodes is small, call depth first routine. */
00128       result = BddExistsStep(bddManager, f, opCode, assoc);
00129     }
00130     else {
00131       result = BddExistsBFPlusDF(bddManager, f, opCode, assoc);
00132     }
00133     userResult =  CalBddGetExternalBdd(bddManager, result);
00134     if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){
00135       Cal_BddFree(bddManager, userResult);
00136       Cal_BddManagerGC(bddManager);
00137       return (Cal_Bdd) 0;
00138     }
00139     return userResult;
00140   }
00141   return (Cal_Bdd) 0;
00142 }
00143 
00144 
00158 Cal_Bdd
00159 Cal_BddRelProd(Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd)
00160 {
00161   Cal_Bdd_t result;
00162   Cal_Bdd userResult;
00163   
00164   if (CalBddPreProcessing(bddManager, 2, fUserBdd, gUserBdd)){
00165     Cal_Bdd_t f = CalBddGetInternalBdd(bddManager, fUserBdd);
00166     Cal_Bdd_t g = CalBddGetInternalBdd(bddManager, gUserBdd);
00167     CalAssociation_t *assoc = bddManager->currentAssociation;
00168     unsigned short opCode;
00169     
00170     if (bddManager->currentAssociation->id == -1){
00171       opCode = bddManager->tempOpCode--;
00172       bddManager->tempOpCode--;
00173     }
00174     else {
00175       opCode = CAL_OP_REL_PROD + assoc->id;
00176     }
00177     if (bddManager->numNodes <= CAL_LARGE_BDD){
00178       /* If number of nodes is small, call depth first routine. */
00179       result = BddRelProdStep(bddManager, f, g, opCode, assoc);
00180     }
00181     else {
00182       result = BddRelProdBFPlusDF(bddManager, f, g, opCode, assoc);
00183     }
00184     userResult =  CalBddGetExternalBdd(bddManager, result);
00185     if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){
00186       Cal_BddFree(bddManager, userResult);
00187       Cal_BddManagerGC(bddManager);
00188       return (Cal_Bdd) 0;
00189     }
00190     return userResult;
00191   }
00192   return (Cal_Bdd) 0;
00193 }
00194 
00207 Cal_Bdd
00208 Cal_BddForAll(Cal_BddManager bddManager, Cal_Bdd fUserBdd)
00209 {
00210   Cal_Bdd_t result;
00211   Cal_Bdd userResult;
00212 
00213   if (CalBddPreProcessing(bddManager, 1, fUserBdd)){
00214     Cal_Bdd_t f = CalBddGetInternalBdd(bddManager, fUserBdd);
00215     CalAssociation_t *assoc = bddManager->currentAssociation;
00216     unsigned short opCode;
00217 
00218     CalBddNot(f, f);
00219     if (assoc->id == -1){
00220       opCode = bddManager->tempOpCode--;
00221     }
00222     else {
00223       opCode = CAL_OP_QUANT + assoc->id;
00224     }
00225     if (bddManager->numNodes <= CAL_LARGE_BDD){
00226       /* If number of nodes is small, call depth first routine. */
00227       result = BddExistsStep(bddManager, f, opCode, assoc);
00228     }
00229     else {
00230       result = BddExistsBFPlusDF(bddManager, f, opCode, assoc);
00231     }
00232     CalBddNot(result, result);
00233     userResult =  CalBddGetExternalBdd(bddManager, result);
00234     if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){
00235       Cal_BddFree(bddManager, userResult);
00236       Cal_BddManagerGC(bddManager);
00237       return (Cal_Bdd) 0;
00238     }
00239     return userResult;
00240   }
00241   return (Cal_Bdd) 0;
00242 }
00243 
00244 /*---------------------------------------------------------------------------*/
00245 /* Definition of internal functions                                          */
00246 /*---------------------------------------------------------------------------*/
00247   
00259 int
00260 CalOpExists(Cal_BddManager_t * bddManager, Cal_Bdd_t  f, Cal_Bdd_t *
00261             resultBddPtr) 
00262 {
00263   if (((int)bddManager->idToIndex[CalBddGetBddId(f)]) >
00264       bddManager->currentAssociation->lastBddIndex){ 
00265     *resultBddPtr = f;
00266     return 1;
00267   }
00268   return 0;
00269 }
00270 
00271 
00283 int
00284 CalOpRelProd(Cal_BddManager_t * bddManager, Cal_Bdd_t  f, Cal_Bdd_t  g,
00285              Cal_Bdd_t * resultBddPtr) 
00286 {
00287   if (CalBddIsBddZero(bddManager, f) || CalBddIsBddZero(bddManager, g) ||
00288       CalBddIsComplementEqual(f, g)){
00289     *resultBddPtr = bddManager->bddZero;
00290     return 1;
00291   }
00292   else if (CalBddIsBddOne(bddManager, f) && CalBddIsBddOne(bddManager, g)){
00293     *resultBddPtr = bddManager->bddOne;
00294     return 1;
00295   }
00296   return 0;
00297 }
00298 /*---------------------------------------------------------------------------*/
00299 /* Definition of static functions                                            */
00300 /*---------------------------------------------------------------------------*/
00301 
00313 static Cal_Bdd_t
00314 BddExistsStep(Cal_BddManager_t * bddManager, Cal_Bdd_t  f, unsigned
00315               short opCode, CalAssociation_t *association)
00316 {
00317   Cal_Bdd_t temp1, temp2;
00318   Cal_Bdd_t f1, f2;
00319   Cal_Bdd_t result;
00320   Cal_BddId_t topId;
00321   int quantifying;
00322   
00323   if (((int)CalBddGetBddIndex(bddManager, f)) > association->lastBddIndex){
00324     return f;
00325   }
00326   if (CalCacheTableOneLookup(bddManager, f, opCode, &result)){
00327     return result;
00328   }
00329 
00330   topId = CalBddGetBddId(f);
00331   quantifying = (CalBddIsBddNull(bddManager,
00332                                  association->varAssociation[topId]) ? 0 : 1);
00333   CalBddGetCofactors(f, topId, f1, f2);
00334   temp1 = BddExistsStep(bddManager, f1, opCode, association);
00335   if (quantifying && CalBddIsEqual(temp1, bddManager->bddOne)){
00336     result=temp1;
00337   }
00338   else {
00339     temp2 = BddExistsStep(bddManager, f2, opCode, association);
00340     if (quantifying){
00341       CalBddNot(temp1, temp1);
00342       CalBddNot(temp2, temp2);
00343           result = BddDFStep(bddManager, temp1, temp2, CalOpNand, CAL_OP_NAND);
00344         }
00345     else {
00346       Cal_BddId_t id = CalBddGetBddId(f);
00347       if (CalUniqueTableForIdFindOrAdd(bddManager, bddManager->uniqueTable[id],
00348                                        temp1, temp2, &result) == 0){
00349         CalBddIcrRefCount(temp1);
00350         CalBddIcrRefCount(temp2);
00351       }
00352     }
00353   } 
00354   CalCacheTableOneInsert(bddManager, f, result, opCode, 0);
00355   return (result);
00356 }
00357 
00369 static Cal_Bdd_t
00370 BddRelProdStep(Cal_BddManager_t * bddManager, Cal_Bdd_t  f, Cal_Bdd_t
00371                g, unsigned short opCode, CalAssociation_t *assoc)
00372 {
00373   Cal_BddId_t topId;
00374   Cal_Bdd_t f1, f2, g1, g2;
00375   Cal_Bdd_t temp1, temp2;
00376   Cal_Bdd_t  result;
00377   int quantifying;
00378 
00379   if (CalBddIsBddConst(f) || CalBddIsBddConst(g)){
00380     if (CalBddIsBddZero(bddManager, f) || CalBddIsBddZero(bddManager, g)){
00381       return bddManager->bddZero;
00382     }
00383     if (assoc->id != -1){
00384       opCode = CAL_OP_QUANT+assoc->id;
00385     }
00386     else{
00387       opCode--;
00388     }
00389     if (CalBddIsBddOne(bddManager, f)){
00390       return (BddExistsStep(bddManager, g, opCode, assoc));
00391     }
00392     return (BddExistsStep(bddManager, f, opCode, assoc));
00393   }
00394   if ((((int)CalBddGetBddIndex(bddManager, f)) > assoc->lastBddIndex) &&
00395       (((int)CalBddGetBddIndex(bddManager, g)) > assoc->lastBddIndex)){
00396     result = BddDFStep(bddManager, f, g, CalOpNand, CAL_OP_NAND);
00397     CalBddNot(result, result);
00398     return result;
00399   }
00400   if(CalOpRelProd(bddManager, f, g, &result) == 1){
00401     return result;
00402   }
00403   CalBddNormalize(f, g);
00404   if(CalCacheTableTwoLookup(bddManager, f, g, opCode, &result)){
00405     return result;
00406   }
00407   CalBddGetMinId2(bddManager, f, g, topId);
00408   
00409   quantifying = (CalBddIsBddNull(bddManager, assoc->varAssociation[topId]) ? 0
00410                  : 1);
00411   CalBddGetCofactors(f, topId, f1, f2);
00412   CalBddGetCofactors(g, topId, g1, g2);
00413 
00414   temp1 = BddRelProdStep(bddManager, f1, g1, opCode, assoc);
00415   if (quantifying && CalBddIsBddOne(bddManager, temp1)){
00416     result=temp1;
00417   }
00418   else {
00419     temp2 = BddRelProdStep(bddManager, f2, g2, opCode, assoc);
00420     if (quantifying) {
00421       CalBddNot(temp1, temp1);
00422       CalBddNot(temp2, temp2);
00423           result = BddDFStep(bddManager, temp1, temp2, CalOpNand, CAL_OP_NAND);
00424           /*result = BddDFStep(bddManager, temp1, temp2, CalOpOr, CAL_OP_OR);*/
00425         }
00426     else {
00427       if (CalUniqueTableForIdFindOrAdd(bddManager,
00428                                        bddManager->uniqueTable[topId],
00429                                        temp1, temp2, &result) == 0){
00430         CalBddIcrRefCount(temp1);
00431         CalBddIcrRefCount(temp2);
00432       }
00433     }
00434   }
00435   CalCacheTableTwoInsert(bddManager, f, g, result, opCode, 0);
00436   return (result);
00437 }
00438 
00450 static Cal_Bdd_t
00451 BddDFStep(Cal_BddManager_t * bddManager, Cal_Bdd_t  f, Cal_Bdd_t g,
00452           CalOpProc_t calOpProc, unsigned short opCode)
00453 {
00454   Cal_BddId_t topId;
00455   Cal_Bdd_t temp1, temp2, fx, fxbar, gx, gxbar;
00456   Cal_Bdd_t  result;
00457 
00458   if((*calOpProc)(bddManager, f, g, &result) == 1){
00459     return result;
00460   }
00461   CalBddNormalize(f, g);
00462   if(CalCacheTableTwoLookup(bddManager, f, g, opCode, &result)){
00463     return result;
00464   }
00465   CalBddGetMinId2(bddManager, f, g, topId);
00466   CalBddGetCofactors(f, topId, fx, fxbar);
00467   CalBddGetCofactors(g, topId, gx, gxbar);
00468   temp1 = BddDFStep(bddManager, fx, gx, calOpProc, opCode);
00469   temp2 = BddDFStep(bddManager, fxbar, gxbar, calOpProc, opCode);
00470 
00471   if (CalUniqueTableForIdFindOrAdd(bddManager,
00472                                    bddManager->uniqueTable[topId],
00473                                    temp1, temp2, &result) == 0){
00474     CalBddIcrRefCount(temp1);
00475     CalBddIcrRefCount(temp2);
00476   }
00477   CalCacheTableTwoInsert(bddManager, f, g, result, opCode, 0);
00478   return (result);
00479 }
00491 static void
00492 HashTableApply(Cal_BddManager_t * bddManager, CalHashTable_t * hashTable,
00493                CalHashTable_t ** reqQueAtPipeDepth, CalOpProc_t calOpProc,
00494                unsigned long opCode)  
00495 {
00496   int i, numBins = hashTable->numBins;
00497   CalBddNode_t **bins = hashTable->bins;
00498   CalRequestNode_t *requestNode;
00499   Cal_Bdd_t fx, gx, fxbar, gxbar, result;
00500   Cal_BddId_t bddId;
00501   
00502   for(i = 0; i < numBins; i++){
00503     for(requestNode = bins[i];
00504         requestNode != Cal_Nil(CalRequestNode_t);
00505         requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
00506       CalRequestNodeGetCofactors(bddManager, requestNode, fx, fxbar, gx, gxbar);
00507       CalBddNormalize(fx, gx);
00508       if((*calOpProc)(bddManager, fx, gx, &result) == 0){
00509         if (CalCacheTableTwoLookup(bddManager, fx, gx, opCode, &result) == 0){
00510           CalBddGetMinId2(bddManager, fx, gx, bddId);
00511           CalHashTableFindOrAdd(reqQueAtPipeDepth[bddId], fx, gx, &result);
00512           CalCacheTableTwoInsert(bddManager, fx, gx, result, opCode, 1);
00513         }
00514         else {
00515           CalRequestIsForwardedTo(result);
00516         }
00517       }
00518       CalBddIcrRefCount(result);
00519       CalRequestNodePutThenRequest(requestNode, result);
00520       CalBddNormalize(fxbar, gxbar);
00521       if((*calOpProc)(bddManager, fxbar, gxbar, &result) == 0){
00522         if (CalCacheTableTwoLookup(bddManager, fxbar, gxbar, opCode, &result)
00523             == 0){ 
00524           CalBddGetMinId2(bddManager, fxbar, gxbar, bddId);
00525           CalHashTableFindOrAdd(reqQueAtPipeDepth[bddId], fxbar, gxbar,
00526                                 &result); 
00527           CalCacheTableTwoInsert(bddManager, fxbar, gxbar, result,
00528                                  opCode, 1);
00529         }
00530         else {
00531           CalRequestIsForwardedTo(result);
00532         }
00533       }
00534       CalBddIcrRefCount(result);
00535       CalRequestNodePutElseRequest(requestNode, result);
00536     }
00537   }
00538 }
00539 
00551 static void
00552 HashTableReduce(Cal_BddManager_t * bddManager, CalHashTable_t * hashTable,
00553                 CalHashTable_t * uniqueTableForId)
00554 {
00555   int i, numBins = hashTable->numBins;
00556   CalBddNode_t **bins = hashTable->bins;
00557   Cal_BddId_t currentBddId = uniqueTableForId->bddId;
00558   CalNodeManager_t *nodeManager = uniqueTableForId->nodeManager;
00559   CalRequestNode_t *requestNode, *next;
00560   CalBddNode_t *bddNode, *endNode;
00561   Cal_Bdd_t thenBdd, elseBdd, result;
00562   Cal_BddRefCount_t refCount;
00563 
00564   /*requestNodeList = hashTable->requestNodeList;*/
00565   endNode = hashTable->endNode;
00566   hashTable->numEntries = 0;
00567   for(i = 0; i < numBins; i++){
00568     for(requestNode = bins[i], bins[i] = Cal_Nil(CalRequestNode_t);
00569         requestNode != Cal_Nil(CalRequestNode_t);
00570         requestNode = next){
00571       next = CalRequestNodeGetNextRequestNode(requestNode);
00572       /* Process the requestNode */
00573       CalRequestNodeGetThenRequest(requestNode, thenBdd);
00574       CalRequestNodeGetElseRequest(requestNode, elseBdd);
00575       CalRequestIsForwardedTo(thenBdd);
00576       CalRequestIsForwardedTo(elseBdd);
00577       if(CalBddIsEqual(thenBdd, elseBdd)){
00578         CalBddNodeGetRefCount(requestNode, refCount);
00579         CalBddAddRefCount(thenBdd, refCount - 2);
00580         CalRequestNodePutThenRequest(requestNode, thenBdd);
00581         CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
00582         /*
00583         ** CalRequestNodePutNextRequestNode(requestNode, requestNodeList);
00584         ** requestNodeList = requestNode;
00585         */
00586         /*CalRequestNodePutNextRequestNode(endNode, requestNode);*/
00587         endNode->nextBddNode = requestNode;
00588         endNode = requestNode;
00589       }
00590       else if(CalUniqueTableForIdLookup(bddManager, uniqueTableForId,
00591           thenBdd, elseBdd, &result) == 1){
00592         CalBddDcrRefCount(thenBdd);
00593         CalBddDcrRefCount(elseBdd);
00594         CalBddNodeGetRefCount(requestNode, refCount);
00595         CalBddAddRefCount(result, refCount);
00596         CalRequestNodePutThenRequest(requestNode, result);
00597         CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
00598         /*
00599         ** CalRequestNodePutNextRequestNode(requestNode, requestNodeList);
00600         ** requestNodeList = requestNode;
00601         */
00602         /*CalRequestNodePutNextRequestNode(endNode, requestNode);*/
00603         endNode->nextBddNode = requestNode;
00604         endNode = requestNode;
00605       }
00606       else if(CalBddIsOutPos(thenBdd)){
00607         CalRequestNodePutThenRequest(requestNode, thenBdd);
00608         CalRequestNodePutElseRequest(requestNode, elseBdd);
00609         CalHashTableAddDirect(uniqueTableForId, requestNode);
00610         bddManager->numNodes++;
00611         bddManager->gcCheck--;
00612       }
00613       else{
00614         CalNodeManagerAllocNode(nodeManager, bddNode);
00615         CalBddNodePutThenBddId(bddNode, CalBddGetBddId(thenBdd));
00616         CalBddNodePutThenBddNode(bddNode, CalBddGetBddNodeNot(thenBdd));
00617         CalBddNodePutElseBddId(bddNode, CalBddGetBddId(elseBdd));
00618         CalBddNodePutElseBddNode(bddNode, CalBddGetBddNodeNot(elseBdd));
00619         /*
00620         CalNodeManagerInitBddNode(nodeManager, thenBdd, elseBdd,
00621                                Cal_Nil(CalBddNode_t), bddNode); 
00622                                */
00623         CalBddNodeGetRefCount(requestNode, refCount);
00624         CalBddNodePutRefCount(bddNode, refCount);
00625         CalHashTableAddDirect(uniqueTableForId, bddNode);
00626         bddManager->numNodes++;
00627         bddManager->gcCheck--;
00628         CalRequestNodePutThenRequestId(requestNode, currentBddId);
00629         CalRequestNodePutThenRequestNode(requestNode, CalBddNodeNot(bddNode));
00630         CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
00631         /*
00632         ** CalRequestNodePutNextRequestNode(requestNode, requestNodeList);
00633         ** requestNodeList = requestNode;
00634         */
00635         /*CalRequestNodePutNextRequestNode(endNode, requestNode);*/
00636         endNode->nextBddNode = requestNode;
00637         endNode = requestNode;
00638       }
00639     }
00640   }
00641   /* hashTable->requestNodeList = requestNodeList; */
00642   hashTable->endNode = endNode;
00643 }
00644 
00656 static void
00657 BddExistsApply(Cal_BddManager_t *bddManager, int quantifying,
00658                CalHashTable_t *existHashTable, CalHashTable_t
00659                **existHashTableArray,  CalOpProc1_t calOpProc, 
00660                unsigned short opCode, CalAssociation_t *assoc)  
00661 {
00662   int i, numBins = existHashTable->numBins;
00663   CalBddNode_t **bins = existHashTable->bins;
00664   CalRequestNode_t *requestNode;
00665   Cal_Bdd_t f, fx, fxbar, result, resultBar;
00666   int lastBddIndex = assoc->lastBddIndex; 
00667   
00668   if (quantifying){
00669     for(i = 0; i < numBins; i++){
00670       for(requestNode = bins[i];
00671           requestNode != Cal_Nil(CalRequestNode_t);
00672           requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
00673         CalRequestNodeGetF(requestNode, f);
00674         CalBddGetThenBdd(f, fx);
00675         CalBddGetElseBdd(f, fxbar);
00676       
00677         /*if(calOpProc(bddManager, fx, &result) == 0){*/
00678         if (((int)bddManager->idToIndex[CalBddGetBddId(fx)]) <= lastBddIndex){
00679           if (CalCacheTableOneLookup(bddManager, fx, opCode, &result)){ 
00680             CalRequestIsForwardedTo(result);
00681           }
00682           else {
00683             CalHashTableFindOrAdd(existHashTableArray[CalBddGetBddId(fx)], fx,
00684                                   bddManager->bddOne, &result);
00685             CalCacheTableOneInsert(bddManager, fx, result,
00686                                    opCode, 1);
00687           }
00688         }
00689         else {
00690           result = fx;
00691         }
00692         CalRequestNodePutThenRequest(requestNode, result);
00693         CalRequestNodePutElseRequest(requestNode, fxbar);
00694       }
00695     }
00696   }
00697   else {
00698     for(i = 0; i < numBins; i++){
00699       for(requestNode = bins[i];
00700           requestNode != Cal_Nil(CalRequestNode_t);
00701           requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
00702         CalRequestNodeGetF(requestNode, f);
00703         CalBddGetThenBdd(f, fx);
00704         CalBddGetElseBdd(f, fxbar);
00705       
00706         if (((int)bddManager->idToIndex[CalBddGetBddId(fx)]) <= lastBddIndex){
00707           if (CalCacheTableOneLookup(bddManager, fx, opCode, &result)){ 
00708             CalRequestIsForwardedTo(result);
00709           }
00710           else {
00711             CalHashTableFindOrAdd(existHashTableArray[CalBddGetBddId(fx)], fx,
00712                                   bddManager->bddOne, &result);
00713             CalCacheTableOneInsert(bddManager, fx, result,
00714                                    opCode, 1);
00715           }
00716         }
00717         else {
00718           result = fx;
00719         }
00720         CalRequestNodePutThenRequest(requestNode, result);
00721         CalBddIcrRefCount(result);
00722         /*if(calOpProc(bddManager, fxbar, &resultBar) == 0){*/
00723         if (((int)bddManager->idToIndex[CalBddGetBddId(fxbar)]) <= lastBddIndex){
00724           if (CalCacheTableOneLookup(bddManager, fxbar, opCode,
00725                                        &resultBar)){
00726             CalRequestIsForwardedTo(resultBar);
00727           }
00728           else {
00729             CalHashTableFindOrAdd(existHashTableArray[CalBddGetBddId(fxbar)], fxbar,
00730                                   bddManager->bddOne, &resultBar);
00731             CalCacheTableOneInsert(bddManager, fxbar, resultBar,
00732                                    opCode, 1); 
00733           }
00734         }
00735         else{
00736           resultBar = fxbar;
00737         }
00738         CalBddIcrRefCount(resultBar);
00739         CalRequestNodePutElseRequest(requestNode, resultBar);
00740       }
00741     }
00742   }
00743 }
00744 
00756 static void  
00757 BddExistsBFAux(Cal_BddManager_t *bddManager, int minIndex,
00758                CalHashTable_t **existHashTableArray, CalHashTable_t
00759                **orHashTableArray,  CalOpProc1_t calOpProc, unsigned
00760                short opCode, CalAssociation_t *assoc)   
00761 {
00762   int index;
00763   Cal_BddId_t bddId;
00764   int quantifying;
00765   
00766   /* Apply phase */
00767   for (index = minIndex; index < bddManager->numVars; index++){
00768     bddId = bddManager->indexToId[index];
00769     if (existHashTableArray[bddId]->numEntries){
00770       quantifying = (CalBddIsBddNull(bddManager,
00771                                      assoc->varAssociation[bddId]) ? 0 : 1); 
00772       BddExistsApply(bddManager, quantifying,
00773                      existHashTableArray[bddId], existHashTableArray,
00774                      calOpProc, opCode, assoc);    
00775     }
00776   }
00777   
00778   /* Reduce phase */
00779   for (index = bddManager->numVars-1; index >= minIndex; index--){
00780     bddId = bddManager->indexToId[index];
00781     if (existHashTableArray[bddId]->numEntries){
00782       quantifying = (CalBddIsBddNull(bddManager,
00783                                      assoc->varAssociation[bddId]) ? 0 : 1); 
00784       if (quantifying){
00785         BddExistsReduce(bddManager, existHashTableArray[bddId],
00786                         existHashTableArray, orHashTableArray,
00787                         opCode, assoc);
00788       } 
00789       else {
00790         HashTableReduce(bddManager, existHashTableArray[bddId],
00791                         bddManager->uniqueTable[bddId]);
00792       }
00793     }
00794   }
00795 }
00796 
00808 static void
00809 BddExistsReduce(Cal_BddManager_t *bddManager, CalHashTable_t
00810                 *existHashTable, CalHashTable_t **existHashTableArray,
00811                 CalHashTable_t **orHashTableArray, unsigned short
00812                 opCode, CalAssociation_t *association) 
00813 {
00814   int i, numBins = existHashTable->numBins;
00815   CalBddNode_t **bins = existHashTable->bins;
00816   CalRequestNode_t *requestNode, *next, *requestNodeListAux;
00817   CalBddNode_t *endNode;
00818   
00819   int bddIndex;
00820   /*Cal_BddIndex_t minIndex, elseIndex;*/
00821   int minIndex, elseIndex;
00822   Cal_BddId_t bddId, minId;
00823   Cal_Bdd_t thenBdd, elseBdd, result, orResult;
00824   Cal_BddRefCount_t refCount;
00825   int lastBddIndex = association->lastBddIndex; 
00826   
00827 
00828   /* For those nodes which get processed in the first pass */
00829   /* requestNodeList = existHashTable->requestNodeList; */
00830   endNode = existHashTable->endNode;
00831 
00832   /* For the other ones. This list is merged with the requestNodeList
00833    * after processing is complete.
00834    */
00835   requestNodeListAux = Cal_Nil(CalRequestNode_t);
00836   existHashTable->numEntries = 0;
00837   
00838   minIndex = bddManager->numVars;
00839   
00840   for(i = 0; i < numBins; i++){
00841     for(requestNode = bins[i], bins[i] = Cal_Nil(CalRequestNode_t);
00842         requestNode != Cal_Nil(CalRequestNode_t);
00843         requestNode = next){
00844       next = CalRequestNodeGetNextRequestNode(requestNode);
00845       /* Process the requestNode */
00846       CalRequestNodeGetThenRequest(requestNode, thenBdd);
00847       CalRequestNodeGetElseRequest(requestNode, elseBdd);
00848       CalRequestIsForwardedTo(thenBdd);
00849       CalRequestNodePutThenRequest(requestNode, thenBdd);
00850       if (CalBddIsBddOne(bddManager, thenBdd)){
00851         CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
00852         /*
00853         ** CalRequestNodePutNextRequestNode(requestNode, requestNodeList);
00854         ** requestNodeList = requestNode;
00855         */
00856         /*CalRequestNodePutNextRequestNode(endNode, requestNode);*/
00857         endNode->nextBddNode = requestNode;
00858         endNode = requestNode;
00859         continue;
00860       }
00861       
00862       CalRequestNodePutNextRequestNode(requestNode, requestNodeListAux);
00863       requestNodeListAux = requestNode;
00864 
00865       /*if(CalOpExists(bddManager, elseBdd, &result) == 0){*/
00866       if (((int)bddManager->idToIndex[CalBddGetBddId(elseBdd)]) <= lastBddIndex){
00867         if (CalCacheTableOneLookup(bddManager, elseBdd, opCode,
00868                                    &result)){  
00869           CalRequestIsForwardedTo(result);
00870         }
00871         else{
00872           CalHashTableFindOrAdd(existHashTableArray[CalBddGetBddId(elseBdd)], elseBdd,
00873                                 bddManager->bddOne, &result);
00874           CalCacheTableOneInsert(bddManager, elseBdd, result,
00875                                  opCode, 1);
00876           if (minIndex > (elseIndex = CalBddGetBddIndex(bddManager,
00877                                                         elseBdd))){ 
00878             minIndex = elseIndex;
00879           }
00880         }
00881       }
00882       else{
00883         result = elseBdd;
00884       }
00885       CalRequestNodePutElseRequest(requestNode, result);
00886     }
00887   }
00888   
00889   if (!requestNodeListAux){
00890     /* requestNodeList = requestNodeList; */
00891     existHashTable->endNode = endNode;
00892     return;
00893   }
00894   
00895   BddExistsBFAux(bddManager, minIndex, existHashTableArray,
00896                  orHashTableArray,  CalOpExists, opCode, association); 
00897   minIndex = bddManager->numVars;
00898   for (requestNode = requestNodeListAux; requestNode; requestNode = next){
00899     Cal_Bdd_t thenResult, elseResult;
00900     Cal_BddIndex_t orResultIndex;
00901     
00902     next = CalRequestNodeGetNextRequestNode(requestNode);
00903     CalRequestNodeGetThenRequest(requestNode, thenResult);
00904     CalRequestNodeGetElseRequest(requestNode, elseResult);
00905     CalRequestIsForwardedTo(elseResult);
00906     if (CalOpOr(bddManager, thenResult, elseResult, &orResult) == 0){
00907       CalBddNormalize(thenResult, elseResult);
00908       CalBddNot(thenResult, thenResult);
00909       CalBddNot(elseResult, elseResult);
00910       if (CalCacheTableTwoLookup(bddManager, thenResult,elseResult,
00911                                  CAL_OP_NAND, &orResult)){
00912         CalRequestIsForwardedTo(orResult);
00913       }
00914       else {
00915         CalBddGetMinIdAndMinIndex(bddManager, thenResult, elseResult,
00916                                   minId, orResultIndex);
00917         CalHashTableFindOrAdd(orHashTableArray[minId], thenResult, elseResult,
00918                               &orResult);
00919         CalCacheTableTwoInsert(bddManager, thenResult, elseResult, orResult,
00920                                CAL_OP_NAND, 1);
00921         if (minIndex > orResultIndex) minIndex = orResultIndex;
00922       }
00923     }
00924     CalRequestNodePutThenRequest(requestNode, orResult);
00925   }
00926   
00927 
00928   /* Call "OR" apply and reduce */
00929   for (bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
00930     bddId = bddManager->indexToId[bddIndex];
00931     if(orHashTableArray[bddId]->numEntries){
00932       HashTableApply(bddManager, orHashTableArray[bddId], orHashTableArray,
00933                      CalOpNand, CAL_OP_NAND);
00934     }
00935   }
00936   
00937   for(bddIndex = bddManager->numVars - 1; bddIndex >= minIndex; bddIndex--){
00938     CalHashTable_t *uniqueTableForId;
00939     bddId = bddManager->indexToId[bddIndex];
00940     uniqueTableForId = bddManager->uniqueTable[bddId];
00941     if(orHashTableArray[bddId]->numEntries){
00942       HashTableReduce(bddManager, orHashTableArray[bddId], uniqueTableForId);
00943     }
00944   }
00945   
00946   for (requestNode = requestNodeListAux; requestNode; requestNode = next){
00947     next = CalRequestNodeGetNextRequestNode(requestNode);
00948     CalRequestNodeGetThenRequest(requestNode, result);
00949     CalRequestIsForwardedTo(result);
00950     CalBddNodeGetRefCount(requestNode, refCount);
00951     CalBddAddRefCount(result, refCount);
00952     CalRequestNodePutThenRequest(requestNode, result);
00953     CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
00954     /*
00955     ** CalRequestNodePutNextRequestNode(requestNode, requestNodeList);
00956     ** requestNodeList = requestNode;
00957     */
00958     /*CalRequestNodePutNextRequestNode(endNode, requestNode);*/
00959     endNode->nextBddNode = requestNode;
00960     endNode = requestNode;
00961   }
00962   /*existHashTable->requestNodeList = requestNodeList;*/
00963   existHashTable->endNode = endNode;
00964   
00965 }
00966   
00978 static Cal_Bdd_t
00979 BddExistsBFPlusDF(Cal_BddManager_t *bddManager, Cal_Bdd_t f, unsigned
00980                   short opCode, CalAssociation_t *association)
00981 {
00982   Cal_BddId_t fId = CalBddGetBddId(f);
00983   Cal_BddIndex_t bddIndex;
00984   Cal_BddId_t bddId;
00985   
00986   Cal_BddIndex_t fIndex = bddManager->idToIndex[fId];
00987   CalHashTable_t **orHashTableArray = bddManager->reqQue[4];
00988   CalHashTable_t **existHashTableArray = bddManager->reqQue[5];
00989   Cal_Bdd_t result;
00990   
00991   if (CalOpExists(bddManager, f, &result) == 1){
00992     return result;
00993   }
00994 
00995   if (CalCacheTableOneLookup(bddManager, f, opCode, &result)){
00996     return result;
00997   }
00998   
00999   /*
01000    * Change the size of the exist hash table to min. size 
01001    */
01002   for (bddIndex = fIndex; bddIndex < bddManager->numVars; bddIndex++){
01003     bddId = bddManager->indexToId[bddIndex];
01004     existHashTableArray[bddId]->sizeIndex =
01005         DEFAULT_EXIST_HASH_TABLE_SIZE_INDEX;  
01006     existHashTableArray[bddId]->numBins = DEFAULT_EXIST_HASH_TABLE_SIZE;
01007     Cal_MemFree(existHashTableArray[bddId]->bins);
01008     existHashTableArray[bddId]->bins = Cal_MemAlloc(CalBddNode_t*,
01009                                              DEFAULT_EXIST_HASH_TABLE_SIZE);
01010     memset((char *)existHashTableArray[bddId]->bins, 0,
01011            existHashTableArray[bddId]->numBins*sizeof(CalBddNode_t*));
01012   }
01013   
01014   CalHashTableFindOrAdd(existHashTableArray[fId], f, bddManager->bddOne,
01015                         &result);  
01016 
01017 
01018   BddExistsBFAux(bddManager, fIndex, existHashTableArray, orHashTableArray,
01019                  CalOpExists, opCode, association);  
01020 
01021   CalRequestIsForwardedTo(result);
01022   
01023   CalCacheTableTwoFixResultPointers(bddManager);
01024   CalCacheTableOneInsert(bddManager, f, result, opCode, 0);
01025   for (bddIndex = fIndex; bddIndex < bddManager->numVars; bddIndex++){
01026     bddId = bddManager->indexToId[bddIndex];
01027     CalHashTableCleanUp(existHashTableArray[bddId]);
01028     CalHashTableCleanUp(orHashTableArray[bddId]);
01029   }
01030   return result;
01031 }
01032 
01033   
01045 static void
01046 BddRelProdApply(Cal_BddManager_t *bddManager, int quantifying, CalHashTable_t
01047                 *relProdHashTable, CalHashTable_t **relProdHashTableArray,
01048                 CalHashTable_t **andHashTableArray, CalOpProc_t
01049                 calOpProc, unsigned short opCode, CalAssociation_t *assoc)
01050 {
01051   int i, numBins = relProdHashTable->numBins;
01052   CalBddNode_t **bins = relProdHashTable->bins;
01053   Cal_BddId_t minId;
01054   CalRequestNode_t *requestNode;
01055   Cal_Bdd_t fx, fxbar, gx, gxbar, result, resultBar;
01056   /*Cal_BddIndex_t minIndex;*/
01057   int minIndex;
01058   
01059   for(i = 0; i < numBins; i++){
01060     for(requestNode = bins[i];
01061         requestNode != Cal_Nil(CalRequestNode_t);
01062         requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
01063       CalRequestNodeGetCofactors(bddManager, requestNode, fx, fxbar, gx, gxbar);
01064       CalBddNormalize(fx, gx);
01065       CalBddGetMinIdAndMinIndex(bddManager, fx, gx, minId, minIndex);
01066       if (minIndex > assoc->lastBddIndex){
01067         if (CalOpAnd(bddManager, fx, gx, &result) == 0){
01068           if (CalCacheTableTwoLookup(bddManager, fx, gx, CAL_OP_NAND,
01069                                      &result)){  
01070             CalRequestIsForwardedTo(result);
01071           }
01072           else{
01073             CalHashTableFindOrAdd(andHashTableArray[minId], fx, gx, &result);
01074             CalCacheTableTwoInsert(bddManager, fx, gx, result,
01075                                    CAL_OP_NAND, 1);
01076           }
01077           CalBddNot(result, result);
01078         }
01079       }
01080       else {
01081         if(calOpProc(bddManager, fx, gx, &result) == 0){
01082           if (CalCacheTableTwoLookup(bddManager, fx, gx, opCode,
01083                                      &result)){      
01084             CalRequestIsForwardedTo(result);
01085           }
01086           else {
01087             CalHashTableFindOrAdd(relProdHashTableArray[minId], fx, gx,
01088                                   &result);   
01089             CalCacheTableTwoInsert(bddManager, fx, gx, result, opCode, 1); 
01090           }
01091         }
01092       }
01093       CalRequestNodePutThenRequest(requestNode, result);
01094       if (quantifying){
01095         Cal_Bdd_t elseRequest;
01096         Cal_BddId_t elseRequestId;
01097         CalBddNode_t *elseRequestNode;
01098         
01099         CalBddGetMinId2(bddManager, fxbar, gxbar, elseRequestId);
01100         CalNodeManagerInitBddNode(bddManager->nodeManagerArray[elseRequestId],
01101                                   fxbar, gxbar, Cal_Nil(CalBddNode_t),
01102                                   elseRequestNode);
01103         /*
01104           CalNodeManagerAllocNode(bddManager->nodeManagerArray[elseRequestId],
01105           elseRequestNode);  
01106           CalRequestNodePutF(elseRequestNode, fxbar);
01107           CalRequestNodePutG(elseRequestNode, gxbar);
01108         */
01109         CalRequestPutRequestId(elseRequest, elseRequestId);
01110         CalRequestPutRequestNode(elseRequest, elseRequestNode);
01111         CalRequestNodePutElseRequest(requestNode, elseRequest);
01112       }
01113       else {
01114         CalBddIcrRefCount(result);
01115         CalBddNormalize(fxbar, gxbar);
01116         CalBddGetMinIdAndMinIndex(bddManager, fxbar, gxbar, minId, minIndex);
01117         if (minIndex > assoc->lastBddIndex){
01118           if (CalOpAnd(bddManager, fxbar, gxbar, &resultBar) == 0){
01119             if( CalCacheTableTwoLookup(bddManager, fxbar, gxbar,
01120                                        CAL_OP_NAND, &resultBar)){  
01121               CalRequestIsForwardedTo(resultBar);
01122             }
01123             else{
01124               CalHashTableFindOrAdd(andHashTableArray[minId], fxbar, gxbar,
01125                                     &resultBar); 
01126               CalCacheTableTwoInsert(bddManager, fxbar, gxbar, resultBar,
01127                                      CAL_OP_NAND, 1); 
01128             }
01129             CalBddNot(resultBar, resultBar);
01130           }
01131         }
01132         else {
01133           if(calOpProc(bddManager, fxbar, gxbar, &resultBar) == 0){
01134             if (CalCacheTableTwoLookup(bddManager, fxbar, gxbar, opCode,
01135                                        &resultBar)){   
01136               CalRequestIsForwardedTo(resultBar);
01137             }
01138             else { 
01139               CalHashTableFindOrAdd(relProdHashTableArray[minId],
01140                                     fxbar, gxbar, &resultBar);
01141               CalCacheTableTwoInsert(bddManager, fxbar, gxbar,
01142                                      resultBar, opCode, 1); 
01143             }
01144           }
01145         }
01146         CalBddIcrRefCount(resultBar);
01147         CalRequestNodePutElseRequest(requestNode, resultBar);
01148       }
01149     }
01150   }
01151 }
01163 static void
01164 BddRelProdReduce(Cal_BddManager_t *bddManager, CalHashTable_t
01165                  *relProdHashTable, CalHashTable_t
01166                  **relProdHashTableArray, CalHashTable_t
01167                  **andHashTableArray, CalHashTable_t
01168                  **orHashTableArray, unsigned short opCode,
01169                  CalAssociation_t *assoc)  
01170 {
01171   int i, numBins = relProdHashTable->numBins;
01172   CalBddNode_t **bins = relProdHashTable->bins;
01173   CalRequestNode_t *requestNode, *next, *requestNodeListAux;
01174   CalBddNode_t  *elseRequestNode;
01175   int bddIndex;
01176   /*Cal_BddIndex_t minIndex;*/
01177   int minIndex;
01178   Cal_BddId_t bddId, minId, elseRequestId;
01179   Cal_Bdd_t thenBdd, elseBdd, result, orResult;
01180   Cal_BddRefCount_t refCount;
01181   Cal_Bdd_t fxbar, gxbar;
01182   CalBddNode_t *endNode;
01183   
01184 
01185   /* For those nodes which get processed in the first pass */
01186   /*requestNodeList = relProdHashTable->requestNodeList;*/
01187   endNode = relProdHashTable->endNode;
01188   
01189   /* For the other ones. This list is merged with the requestNodeList
01190    * after processing is complete.
01191    */
01192   requestNodeListAux = Cal_Nil(CalRequestNode_t);
01193   
01194   minIndex = bddManager->numVars;
01195   
01196   for(i = 0; i < numBins; i++){
01197     for(requestNode = bins[i], bins[i] = Cal_Nil(CalRequestNode_t);
01198         requestNode != Cal_Nil(CalRequestNode_t);
01199         requestNode = next){
01200       next = CalRequestNodeGetNextRequestNode(requestNode);
01201       /* Process the requestNode */
01202       CalRequestNodeGetThenRequest(requestNode, thenBdd);
01203       CalRequestIsForwardedTo(thenBdd);
01204       /*CalRequestNodePutThenRequest(requestNode, thenBdd);*/
01205       CalRequestNodeGetElseRequest(requestNode, elseBdd);
01206       CalRequestIsForwardedTo(elseBdd);
01207       CalRequestGetF(elseBdd, fxbar);
01208       CalRequestGetG(elseBdd, gxbar);
01209       
01210       /* Free the else request node because it is not needed */
01211       elseRequestNode = CalRequestNodeGetElseRequestNode(requestNode);
01212       elseRequestId = CalRequestNodeGetElseRequestId(requestNode);
01213       CalNodeManagerFreeNode(bddManager->nodeManagerArray[elseRequestId],
01214                              elseRequestNode);
01215       if (CalBddIsBddOne(bddManager, thenBdd)){
01216         CalRequestNodePutThenRequest(requestNode, bddManager->bddOne);
01217         CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
01218         /*
01219         ** CalRequestNodePutNextRequestNode(requestNode, requestNodeList);
01220         ** requestNodeList = requestNode;
01221         */
01222         /*CalRequestNodePutNextRequestNode(endNode, requestNode);*/
01223         endNode->nextBddNode = requestNode;
01224         endNode = requestNode;
01225         continue;
01226       }
01227       
01228       CalRequestNodePutNextRequestNode(requestNode, requestNodeListAux);
01229       requestNodeListAux = requestNode;
01230 
01231       CalBddGetMinIdAndMinIndex(bddManager, fxbar, gxbar, bddId, bddIndex);
01232       CalBddNormalize(fxbar, gxbar);
01233       if (bddIndex > assoc->lastBddIndex){
01234         if (CalOpAnd(bddManager, fxbar, gxbar, &result) == 0){
01235           if (CalCacheTableTwoLookup(bddManager, fxbar, gxbar,
01236                                      CAL_OP_NAND, &result)){
01237             CalRequestIsForwardedTo(result);
01238           }
01239           else {
01240             CalHashTableFindOrAdd(andHashTableArray[bddId], fxbar,
01241                                   gxbar, &result);
01242             CalCacheTableTwoInsert(bddManager, fxbar, gxbar, result,
01243                                    CAL_OP_NAND, 1);
01244             if (minIndex > bddIndex) minIndex = bddIndex;
01245           }
01246           CalBddNot(result, result);
01247         }
01248       }
01249       else {
01250         if(CalOpRelProd(bddManager, fxbar, gxbar, &result) == 0){
01251           if (CalCacheTableTwoLookup(bddManager, fxbar, gxbar, opCode,
01252                                      &result)){  
01253             CalRequestIsForwardedTo(result);
01254           }
01255           else {
01256             CalHashTableFindOrAdd(relProdHashTableArray[bddId], fxbar, gxbar, 
01257                                   &result);
01258             CalCacheTableTwoInsert(bddManager, fxbar, gxbar, result,
01259                                    opCode, 1); 
01260             if (minIndex > bddIndex) minIndex = bddIndex;
01261           }
01262         }
01263       }
01264       CalRequestNodePutElseRequest(requestNode, result);
01265     }
01266   }
01267 
01268   if (!requestNodeListAux){
01269     /*relProdHashTable->requestNodeList = requestNodeList;*/
01270     relProdHashTable->endNode = endNode;
01271     return;
01272   }
01273   
01274   BddRelProdBFAux(bddManager, minIndex, relProdHashTableArray,
01275                   andHashTableArray, orHashTableArray, opCode, assoc);
01276   
01277   minIndex = bddManager->numVars;
01278   for (requestNode = requestNodeListAux; requestNode; requestNode = next){
01279     Cal_Bdd_t thenResult, elseResult;
01280     Cal_BddIndex_t orResultIndex;
01281     
01282     next = CalRequestNodeGetNextRequestNode(requestNode);
01283     CalRequestNodeGetThenRequest(requestNode, thenResult);
01284     CalRequestNodeGetElseRequest(requestNode, elseResult);
01285     CalRequestIsForwardedTo(elseResult);
01286     CalRequestIsForwardedTo(thenResult);
01287     CalBddNormalize(thenResult, elseResult);
01288     if (CalOpOr(bddManager, thenResult, elseResult, &orResult) == 0){
01289       CalBddNot(thenResult, thenResult);
01290       CalBddNot(elseResult, elseResult);
01291       if (CalCacheTableTwoLookup(bddManager, thenResult, elseResult,
01292                                  CAL_OP_NAND, &orResult)){ 
01293         CalRequestIsForwardedTo(orResult);
01294       }
01295       else {
01296         CalBddGetMinIdAndMinIndex(bddManager, thenResult, elseResult,
01297                                   minId, orResultIndex);
01298         CalHashTableFindOrAdd(orHashTableArray[minId], thenResult, elseResult,
01299                               &orResult);
01300         CalCacheTableTwoInsert(bddManager, thenResult, elseResult, orResult,
01301                                  CAL_OP_NAND, 1); 
01302         if (minIndex > orResultIndex) minIndex = orResultIndex;
01303       }
01304     }
01305     CalRequestNodePutThenRequest(requestNode, orResult);
01306   }
01307 
01308   /* Call "OR" apply and reduce */
01309   for (bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
01310     bddId = bddManager->indexToId[bddIndex];
01311     if(orHashTableArray[bddId]->numEntries){
01312         HashTableApply(bddManager, orHashTableArray[bddId], orHashTableArray,
01313                        CalOpNand, CAL_OP_NAND); 
01314     }
01315   }
01316   
01317   for(bddIndex = bddManager->numVars - 1; bddIndex >= minIndex; bddIndex--){
01318     CalHashTable_t *uniqueTableForId;
01319     bddId = bddManager->indexToId[bddIndex];
01320     uniqueTableForId = bddManager->uniqueTable[bddId];
01321     if(orHashTableArray[bddId]->numEntries){
01322       HashTableReduce(bddManager, orHashTableArray[bddId], uniqueTableForId);
01323     }
01324   }
01325   for (requestNode = requestNodeListAux; requestNode; requestNode = next){
01326     next = CalRequestNodeGetNextRequestNode(requestNode);
01327     CalRequestNodeGetThenRequest(requestNode, result);
01328     CalRequestIsForwardedTo(result);
01329     CalBddNodeGetRefCount(requestNode, refCount);
01330     CalBddAddRefCount(result, refCount);
01331     CalRequestNodePutThenRequest(requestNode, result);
01332     CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
01333     /*
01334     ** CalRequestNodePutNextRequestNode(requestNode, requestNodeList);
01335     ** requestNodeList = requestNode;
01336     */
01337     /*CalRequestNodePutNextRequestNode(endNode, requestNode);*/
01338     endNode->nextBddNode = requestNode;
01339     endNode = requestNode;
01340   }
01341 
01342   /*relProdHashTable->requestNodeList = requestNodeList;*/
01343   relProdHashTable->endNode = endNode;
01344 }
01345 
01357 static void
01358 BddRelProdBFAux(Cal_BddManager_t *bddManager, int minIndex,
01359                 CalHashTable_t **relProdHashTableArray, CalHashTable_t
01360                 **andHashTableArray, CalHashTable_t
01361                 **orHashTableArray, unsigned short opCode,
01362                 CalAssociation_t *assoc)
01363 {
01364   Cal_BddIndex_t bddIndex;
01365   int quantifying;
01366   int index;
01367   Cal_BddId_t bddId;
01368   CalHashTable_t *hashTable;
01369   
01370   for (bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
01371     bddId = bddManager->indexToId[bddIndex];
01372     hashTable = andHashTableArray[bddId];
01373     if(hashTable->numEntries){
01374       HashTableApply(bddManager, hashTable, andHashTableArray, CalOpNand,
01375                      CAL_OP_NAND); 
01376     }
01377     hashTable = relProdHashTableArray[bddId];
01378     if(hashTable->numEntries){
01379       quantifying = (CalBddIsBddNull(bddManager,
01380                                      assoc->varAssociation[bddId]) ? 0 : 1); 
01381       BddRelProdApply(bddManager, quantifying, hashTable,
01382                       relProdHashTableArray, andHashTableArray,
01383                       CalOpRelProd, opCode, assoc); 
01384     }
01385   }
01386 
01387   /* Reduce phase */
01388   for (index = bddManager->numVars-1; index >= minIndex; index--){
01389     CalHashTable_t *uniqueTableForId;
01390     bddId = bddManager->indexToId[index];
01391     uniqueTableForId = bddManager->uniqueTable[bddId];
01392     hashTable = andHashTableArray[bddId];
01393     if(hashTable->numEntries){
01394       HashTableReduce(bddManager, hashTable, uniqueTableForId);
01395     }
01396     if (relProdHashTableArray[bddId]->numEntries){
01397       quantifying = (CalBddIsBddNull(bddManager,
01398                                      assoc->varAssociation[bddId]) ? 0 : 1); 
01399       if (quantifying){
01400         BddRelProdReduce(bddManager, relProdHashTableArray[bddId],
01401                          relProdHashTableArray, andHashTableArray,
01402                          orHashTableArray, opCode, assoc); 
01403       }
01404       else {
01405         HashTableReduce(bddManager, relProdHashTableArray[bddId],
01406                         bddManager->uniqueTable[bddId]);
01407       }
01408     }
01409   }
01410 }
01411 
01423 static Cal_Bdd_t
01424 BddRelProdBFPlusDF(Cal_BddManager_t * bddManager, Cal_Bdd_t  f,
01425                    Cal_Bdd_t  g, unsigned short opCode,
01426                    CalAssociation_t *association)
01427 {
01428   Cal_Bdd_t result;
01429   /*Cal_BddIndex_t minIndex;*/
01430   int  minIndex;
01431   int bddIndex;
01432   CalHashTable_t **andHashTableArray = bddManager->reqQue[3];
01433   CalHashTable_t **relProdHashTableArray = bddManager->reqQue[4];
01434   CalHashTable_t **orHashTableArray = bddManager->reqQue[5];
01435   Cal_BddId_t bddId, minId;
01436 
01437   if(CalOpRelProd(bddManager, f, g, &result) == 1){
01438     return result;
01439   }
01440   CalBddNormalize(f, g);
01441   if(CalCacheTableTwoLookup(bddManager, f, g, opCode, &result)){
01442     return result;
01443   }
01444 
01445   CalBddGetMinIdAndMinIndex(bddManager, f, g, minId, minIndex);
01446 
01447   /*
01448    * Change the size of the exist hash table to min. size 
01449    */
01450   for (bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
01451     bddId = bddManager->indexToId[bddIndex];
01452     relProdHashTableArray[bddId]->sizeIndex =
01453         DEFAULT_EXIST_HASH_TABLE_SIZE_INDEX;  
01454     relProdHashTableArray[bddId]->numBins = DEFAULT_EXIST_HASH_TABLE_SIZE;
01455     Cal_MemFree(relProdHashTableArray[bddId]->bins);
01456     relProdHashTableArray[bddId]->bins = Cal_MemAlloc(CalBddNode_t*,
01457                                              DEFAULT_EXIST_HASH_TABLE_SIZE);
01458     memset((char *)relProdHashTableArray[bddId]->bins, 0,
01459            relProdHashTableArray[bddId]->numBins*sizeof(CalBddNode_t*));
01460   }
01461 
01462   if (minIndex > association->lastBddIndex) {
01463     if (CalOpAnd(bddManager, f, g, &result) == 0){
01464       if (CalCacheTableTwoLookup(bddManager, f, g, CAL_OP_NAND, &result)
01465           == 0){
01466         CalHashTableFindOrAdd(andHashTableArray[minId], f, g, &result);
01467       }
01468       else{
01469         CalCacheTableTwoInsert(bddManager, f, g, result, CAL_OP_NAND,
01470                                1);
01471       }
01472       CalBddNot(result, result);
01473     }
01474   }
01475   else {
01476     CalHashTableFindOrAdd(relProdHashTableArray[minId], f, g, &result); 
01477   }
01478 
01479   BddRelProdBFAux(bddManager, minIndex, relProdHashTableArray,
01480                   andHashTableArray, orHashTableArray, opCode, association); 
01481   CalRequestIsForwardedTo(result);
01482   CalCacheTableTwoFixResultPointers(bddManager);
01483   CalCacheTableTwoInsert(bddManager, f, g, result, opCode, 0);
01484   for (bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
01485     bddId = bddManager->indexToId[bddIndex];
01486     CalHashTableCleanUp(relProdHashTableArray[bddId]);
01487     CalHashTableCleanUp(andHashTableArray[bddId]);
01488     CalHashTableCleanUp(orHashTableArray[bddId]);
01489   }
01490   return result;
01491 }
01492