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

00001 
00040 #include "calInt.h"
00041 
00042 /*---------------------------------------------------------------------------*/
00043 /* Constant declarations                                                     */
00044 /*---------------------------------------------------------------------------*/
00045 
00046 /*---------------------------------------------------------------------------*/
00047 /* Type declarations                                                         */
00048 /*---------------------------------------------------------------------------*/
00049 
00050 /*---------------------------------------------------------------------------*/
00051 /* Stucture declarations                                                     */
00052 /*---------------------------------------------------------------------------*/
00053 
00054 
00055 /*---------------------------------------------------------------------------*/
00056 /* Variable declarations                                                     */
00057 /*---------------------------------------------------------------------------*/
00058 
00059 /*---------------------------------------------------------------------------*/
00060 /* Macro declarations                                                        */
00061 /*---------------------------------------------------------------------------*/
00062 
00065 /*---------------------------------------------------------------------------*/
00066 /* Static function prototypes                                                */
00067 /*---------------------------------------------------------------------------*/
00068 
00069 static void CalHashTableSubstituteApply(Cal_BddManager_t * bddManager, CalHashTable_t * hashTable, int lastIndex, CalHashTable_t ** reqQueForSubstitute, unsigned short opCode);
00070 static void CalHashTableSubstituteReduce(Cal_BddManager_t * bddManager, CalHashTable_t * hashTable, CalHashTable_t ** reqQueForITE, CalHashTable_t * uniqueTableForId, unsigned short opCode);
00071 
00074 /*---------------------------------------------------------------------------*/
00075 /* Definition of exported functions                                          */
00076 /*---------------------------------------------------------------------------*/
00077 
00092 Cal_Bdd
00093 Cal_BddVarSubstitute(Cal_BddManager bddManager, Cal_Bdd fUserBdd)
00094 {
00095   CalRequest_t result;
00096   Cal_Bdd userResult;
00097   
00098   if (CalBddPreProcessing(bddManager, 1, fUserBdd)){
00099     Cal_Bdd_t f = CalBddGetInternalBdd(bddManager, fUserBdd);
00100     CalAssociation_t *assoc = bddManager->currentAssociation;
00101     unsigned short opCode;
00102     if (assoc->id == -1){
00103       opCode = bddManager->tempOpCode--;
00104     }
00105     else {
00106       opCode = CAL_OP_VAR_SUBSTITUTE + assoc->id;
00107     }
00108     result = CalBddVarSubstitute(bddManager, f, opCode, assoc);
00109     userResult =  CalBddGetExternalBdd(bddManager, result);
00110     if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){
00111       Cal_BddFree(bddManager, userResult);
00112       Cal_BddManagerGC(bddManager);
00113       return (Cal_Bdd) 0;
00114     }
00115     return userResult;
00116   }
00117   return (Cal_Bdd) 0;
00118 }
00119   
00120 
00121 /*---------------------------------------------------------------------------*/
00122 /* Definition of internal functions                                          */
00123 /*---------------------------------------------------------------------------*/
00124 
00125 /*---------------------------------------------------------------------------*/
00126 /* Definition of static functions                                            */
00127 /*---------------------------------------------------------------------------*/
00128 
00142 Cal_Bdd_t
00143 CalBddVarSubstitute(Cal_BddManager bddManager, Cal_Bdd_t f, unsigned
00144                     short opCode, CalAssociation_t *assoc)
00145 {
00146   CalRequest_t result;
00147   int bddId, bddIndex, lastIndex;
00148   CalHashTable_t *hashTable;
00149   CalHashTable_t *uniqueTableForId;
00150   CalHashTable_t **reqQueForSubstitute = bddManager->reqQue[0];
00151   CalHashTable_t **reqQueForITE = bddManager->reqQue[1]; 
00152   Cal_BddId_t fId = CalBddGetBddId(f);
00153   /*Cal_BddIndex_t fIndex = bddManager->idToIndex[fId];*/
00154   int fIndex = bddManager->idToIndex[fId];
00155   
00156   if (CalOpBddVarSubstitute(bddManager, f, &result)){
00157     return result;
00158   }
00159 
00160   if (CalCacheTableOneLookup(bddManager, f, opCode, &result)){
00161     return result;
00162   }
00163   CalHashTableFindOrAdd(reqQueForSubstitute[fId], f, 
00164     bddManager->bddNull, &result);
00165 
00166   /* ReqQueApply */
00167   lastIndex = assoc->lastBddIndex;
00168   for(bddIndex = fIndex; bddIndex < bddManager->numVars; bddIndex++){
00169     bddId = bddManager->indexToId[bddIndex];
00170     hashTable = reqQueForSubstitute[bddId];
00171     if(hashTable->numEntries){
00172       CalHashTableSubstituteApply(bddManager, hashTable, lastIndex, 
00173                                   reqQueForSubstitute, opCode);
00174     }
00175   }
00176 
00177   /* ReqQueReduce */
00178   for(bddIndex = bddManager->numVars - 1; bddIndex >= fIndex; bddIndex--){
00179     bddId = bddManager->indexToId[bddIndex];
00180     uniqueTableForId = bddManager->uniqueTable[bddId];
00181     hashTable = reqQueForSubstitute[bddId];
00182     if(hashTable->numEntries){
00183       CalHashTableSubstituteReduce(bddManager, hashTable,
00184                                    reqQueForITE, uniqueTableForId,
00185                                    opCode); 
00186     }
00187   }
00188 
00189   CalRequestIsForwardedTo(result);
00190 
00191   /* ReqQueCleanUp */
00192   for(bddId = 1; bddId <= bddManager->numVars; bddId++){
00193     CalHashTableCleanUp(reqQueForSubstitute[bddId]);
00194   }
00195   CalCacheTableTwoFixResultPointers(bddManager);
00196   CalCacheTableOneInsert(bddManager, f, result, opCode, 0);
00197   return result;
00198 }
00199 
00211 int
00212 CalOpBddVarSubstitute(Cal_BddManager_t * bddManager, Cal_Bdd_t  f, Cal_Bdd_t *
00213             resultBddPtr) 
00214 {
00215   if (bddManager->idToIndex[CalBddGetBddId(f)] >
00216       bddManager->currentAssociation->lastBddIndex){ 
00217     *resultBddPtr = f;
00218     return 1;
00219   }
00220   return 0;
00221 }
00222 
00223 
00235 static void
00236 CalHashTableSubstituteApply(
00237   Cal_BddManager_t * bddManager,
00238   CalHashTable_t * hashTable,
00239   int  lastIndex,
00240   CalHashTable_t ** reqQueForSubstitute,
00241   unsigned short opCode)
00242 {
00243   int i, numBins = hashTable->numBins;
00244   CalBddNode_t **bins = hashTable->bins;
00245   CalRequestNode_t *requestNode;
00246   Cal_BddId_t bddId;
00247   /*Cal_BddIndex_t bddIndex;*/
00248   int bddIndex;
00249   Cal_Bdd_t f, fx, fxBar, result;
00250   Cal_Bdd_t nullBdd = bddManager->bddNull;
00251 
00252   for(i = 0; i < numBins; i++){
00253     for(requestNode = bins[i];
00254         requestNode != Cal_Nil(CalRequestNode_t);
00255         requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
00256       /* Process the requestNode */
00257       CalRequestNodeGetF(requestNode, f);
00258       /* Process Left Cofactor */
00259       CalBddGetThenBdd(f, fx);
00260       bddId = CalBddGetBddId(fx);
00261       bddIndex = bddManager->idToIndex[bddId];
00262       if(bddIndex <= lastIndex){
00263           if (CalCacheTableOneLookup(bddManager, fx, opCode, &result)){ 
00264             CalRequestIsForwardedTo(result);
00265           }
00266           else {
00267             CalHashTableFindOrAdd(reqQueForSubstitute[bddId], fx, nullBdd, 
00268                               &result);
00269             CalCacheTableOneInsert(bddManager, fx, result,
00270                                    opCode, 1);
00271           }
00272       }
00273       else{
00274         result = fx;
00275       }
00276       CalBddIcrRefCount(result);
00277       CalRequestNodePutThenRequest(requestNode, result);
00278       /* Process Right Cofactor */
00279       CalBddGetElseBdd(f, fxBar);
00280       bddId = CalBddGetBddId(fxBar);
00281       bddIndex = bddManager->idToIndex[bddId];
00282       if(bddIndex <= lastIndex){
00283           if (CalCacheTableOneLookup(bddManager, fxBar, opCode, &result)){ 
00284             CalRequestIsForwardedTo(result);
00285           }
00286           else {
00287             CalHashTableFindOrAdd(reqQueForSubstitute[bddId], fxBar, nullBdd, 
00288                               &result);
00289             CalCacheTableOneInsert(bddManager, fxBar, result,
00290                                    opCode, 1);
00291           }
00292       }
00293       else{
00294         result = fxBar;
00295       }
00296       CalBddIcrRefCount(result);
00297       CalRequestNodePutElseRequest(requestNode, result);
00298     }
00299   }
00300 }
00301 
00313 static void
00314 CalHashTableSubstituteReduce(
00315   Cal_BddManager_t * bddManager,
00316   CalHashTable_t * hashTable,
00317   CalHashTable_t ** reqQueForITE,
00318   CalHashTable_t * uniqueTableForId,
00319   unsigned short opCode)
00320 {
00321   int i, numBins = hashTable->numBins;
00322   CalBddNode_t **bins = hashTable->bins;
00323   Cal_BddId_t varBddId = hashTable->bddId;
00324   CalNodeManager_t *nodeManager = hashTable->nodeManager;
00325   /*CalRequestNode_t *requestNodeList = hashTable->requestNodeList;*/
00326   CalRequestNode_t *endNode = hashTable->endNode;
00327   CalRequestNode_t *requestNodeListForITE = Cal_Nil(CalRequestNode_t);
00328   CalRequestNode_t *requestNode, *next;
00329   CalBddNode_t *bddNode;
00330   Cal_Bdd_t varBdd;
00331   Cal_Bdd_t thenBdd, elseBdd, result;
00332   Cal_Bdd_t h;
00333   Cal_BddIndex_t resultIndex, varBddIndex;
00334   int minITEindex = bddManager->numVars;
00335   Cal_BddRefCount_t refCount;
00336   int bddId, bddIndex;
00337   CalHashTable_t *hashTableForITE;
00338 
00339   varBddIndex = bddManager->idToIndex[varBddId];
00340   varBdd = bddManager->varBdds[varBddId];
00341   h = bddManager->currentAssociation->varAssociation[varBddId];
00342   if(!CalBddIsBddNull(bddManager, h)){
00343     Cal_BddId_t hId = CalBddGetBddId(h);
00344     Cal_BddIndex_t hIndex = bddManager->idToIndex[hId];
00345     for(i = 0; i < numBins; i++){
00346       for(requestNode = bins[i], bins[i] = Cal_Nil(CalRequestNode_t);
00347           requestNode != Cal_Nil(CalRequestNode_t);
00348           requestNode = next){
00349         next = CalRequestNodeGetNextRequestNode(requestNode);
00350         /* Process the requestNode */
00351         CalRequestNodeGetThenRequest(requestNode, thenBdd);
00352         CalRequestNodeGetElseRequest(requestNode, elseBdd);
00353         CalRequestIsForwardedTo(thenBdd);
00354         CalRequestIsForwardedTo(elseBdd);
00355         if(CalBddIsEqual(thenBdd, elseBdd)){
00356           CalBddNodeGetRefCount(requestNode, refCount);
00357           CalBddAddRefCount(thenBdd, refCount - 2);
00358           CalRequestNodePutThenRequest(requestNode, thenBdd);
00359           CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
00360           endNode->nextBddNode = requestNode;
00361           endNode = requestNode;
00362         }
00363         else{
00364           if(hIndex < CalBddGetBddIndex(bddManager, thenBdd) &&
00365              hIndex < CalBddGetBddIndex(bddManager, elseBdd)){
00366             if(CalUniqueTableForIdLookup(bddManager, bddManager->uniqueTable[hId],
00367                                          thenBdd, elseBdd, &result) == 1){
00368               CalBddDcrRefCount(thenBdd);
00369               CalBddDcrRefCount(elseBdd);
00370               CalBddNodeGetRefCount(requestNode, refCount);
00371               CalBddAddRefCount(result, refCount);
00372               CalRequestNodePutThenRequest(requestNode, result);
00373               CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
00374               endNode->nextBddNode = requestNode;
00375               endNode = requestNode;
00376             }
00377             else if(CalBddIsOutPos(thenBdd)){
00378               /* Get a node from the node manager of h */
00379               CalNodeManager_t *hNodeManager =
00380                   bddManager->nodeManagerArray[hId];
00381               CalNodeManagerInitBddNode(hNodeManager, thenBdd, elseBdd,
00382                                       Cal_Nil(CalBddNode_t), bddNode);
00383               CalBddNodeGetRefCount(requestNode, refCount);
00384               CalBddNodePutRefCount(bddNode, refCount);
00385               CalHashTableAddDirect(bddManager->uniqueTable[hId], bddNode);
00386               bddManager->numNodes++;
00387               bddManager->gcCheck--;
00388               CalRequestNodePutThenRequestId(requestNode, hId);
00389               CalRequestNodePutThenRequestNode(requestNode, bddNode); 
00390               CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
00391               endNode->nextBddNode = requestNode;
00392               endNode = requestNode;
00393             }
00394             else{
00395               /* Get a node from the node manager of h */
00396               CalNodeManager_t *hNodeManager =
00397                   bddManager->nodeManagerArray[hId];
00398               CalBddNot(thenBdd, thenBdd);
00399               CalBddNot(elseBdd, elseBdd);
00400               CalNodeManagerInitBddNode(hNodeManager, thenBdd, elseBdd,
00401                                       Cal_Nil(CalBddNode_t), bddNode);
00402               CalBddNodeGetRefCount(requestNode, refCount);
00403               CalBddNodePutRefCount(bddNode, refCount);
00404               CalHashTableAddDirect(bddManager->uniqueTable[hId], bddNode);
00405               bddManager->numNodes++;
00406               bddManager->gcCheck--;
00407               CalRequestNodePutThenRequestId(requestNode, hId);
00408               CalRequestNodePutThenRequestNode(requestNode,
00409                                                CalBddNodeNot(bddNode));
00410               CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
00411               endNode->nextBddNode = requestNode;
00412               endNode = requestNode;
00413             }
00414           }
00415           else{
00416             CalBddDcrRefCount(thenBdd);
00417             CalBddDcrRefCount(elseBdd);
00418             result = CalOpITE(bddManager, h, thenBdd, elseBdd, reqQueForITE);
00419             if ((resultIndex = bddManager->idToIndex[CalBddGetBddId(result)]) < minITEindex){
00420               minITEindex = resultIndex;
00421             }
00422             CalRequestNodePutThenRequest(requestNode, result);
00423             CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
00424             CalRequestNodePutNextRequestNode(requestNode,
00425                                              requestNodeListForITE);
00426             requestNodeListForITE = requestNode;
00427           }
00428         }
00429       }
00430     }
00431   }
00432   else{
00433     for(i = 0; i < numBins; i++){
00434       for(requestNode = bins[i], bins[i] = Cal_Nil(CalRequestNode_t);
00435           requestNode != Cal_Nil(CalRequestNode_t);
00436           requestNode = next){
00437         next = CalRequestNodeGetNextRequestNode(requestNode);
00438         /* Process the requestNode */
00439         CalRequestNodeGetThenRequest(requestNode, thenBdd);
00440         CalRequestNodeGetElseRequest(requestNode, elseBdd);
00441         CalRequestIsForwardedTo(thenBdd);
00442         CalRequestIsForwardedTo(elseBdd);
00443         if(CalBddIsEqual(thenBdd, elseBdd)){
00444           CalBddNodeGetRefCount(requestNode, refCount);
00445           CalBddAddRefCount(thenBdd, refCount - 2);
00446           CalRequestNodePutThenRequest(requestNode, thenBdd);
00447           CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
00448           endNode->nextBddNode = requestNode;
00449           endNode = requestNode;
00450         }
00451         else{
00452           if(varBddIndex < CalBddGetBddIndex(bddManager, thenBdd) &&
00453              varBddIndex < CalBddGetBddIndex(bddManager, elseBdd)){
00454             if(CalUniqueTableForIdLookup(bddManager, uniqueTableForId,
00455                                          thenBdd, elseBdd, &result) == 1){
00456               CalBddDcrRefCount(thenBdd);
00457               CalBddDcrRefCount(elseBdd);
00458               CalBddNodeGetRefCount(requestNode, refCount);
00459               CalBddAddRefCount(result, refCount);
00460               CalRequestNodePutThenRequest(requestNode, result);
00461               CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
00462               endNode->nextBddNode = requestNode;
00463               endNode = requestNode;
00464             }
00465             else if(CalBddIsOutPos(thenBdd)){
00466               CalRequestNodePutThenRequest(requestNode, thenBdd);
00467               CalRequestNodePutElseRequest(requestNode, elseBdd);
00468               CalHashTableAddDirect(uniqueTableForId, requestNode);
00469               bddManager->numNodes++;
00470               bddManager->gcCheck--;
00471             }
00472             else{
00473               CalBddNot(thenBdd, thenBdd);
00474               CalBddNot(elseBdd, elseBdd);
00475               CalNodeManagerInitBddNode(nodeManager, thenBdd, elseBdd,
00476                                       Cal_Nil(CalBddNode_t), bddNode);
00477               CalBddNodeGetRefCount(requestNode, refCount);
00478               CalBddNodePutRefCount(bddNode, refCount);
00479               CalHashTableAddDirect(uniqueTableForId, bddNode);
00480               bddManager->numNodes++;
00481               bddManager->gcCheck--;
00482               CalRequestNodePutThenRequestId(requestNode, varBddId);
00483               CalRequestNodePutThenRequestNode(requestNode,
00484                                                CalBddNodeNot(bddNode));
00485               CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
00486               endNode->nextBddNode = requestNode;
00487               endNode = requestNode;
00488             }
00489           }
00490           else{
00491             CalBddDcrRefCount(thenBdd);
00492             CalBddDcrRefCount(elseBdd);
00493             result = CalOpITE(bddManager, varBdd, thenBdd, elseBdd, reqQueForITE);
00494             if ((resultIndex = bddManager->idToIndex[CalBddGetBddId(result)]) < minITEindex){
00495               minITEindex = resultIndex;
00496             }
00497             CalRequestNodePutThenRequest(requestNode, result);
00498             CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
00499             CalRequestNodePutNextRequestNode(requestNode,
00500                                              requestNodeListForITE);
00501             requestNodeListForITE = requestNode;
00502           }
00503         }
00504       }
00505     }
00506   }
00507 
00508   /* ITE Apply */
00509   for(bddIndex = minITEindex; bddIndex < bddManager->numVars; bddIndex++){
00510     bddId = bddManager->indexToId[bddIndex];
00511     hashTableForITE = reqQueForITE[bddId];
00512     if(hashTableForITE->numEntries){
00513       CalHashTableITEApply(bddManager, hashTableForITE, reqQueForITE);
00514     }
00515   }
00516   /* ITE Reduce */
00517   for(bddIndex = bddManager->numVars - 1; bddIndex >= minITEindex; bddIndex--){
00518     bddId = bddManager->indexToId[bddIndex];
00519     hashTableForITE = reqQueForITE[bddId];
00520     if(hashTableForITE->numEntries){
00521       CalHashTableReduce(bddManager, hashTableForITE,
00522           bddManager->uniqueTable[bddId]);
00523     }
00524   }
00525     
00526 
00527   for(requestNode = requestNodeListForITE; 
00528       requestNode != Cal_Nil(CalRequestNode_t);
00529       requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
00530     CalRequestNodeGetThenRequest(requestNode, result);
00531     CalBddNodeGetRefCount(requestNode, refCount);
00532     CalRequestIsForwardedTo(result);
00533     CalBddAddRefCount(result, refCount);
00534     CalRequestNodePutThenRequest(requestNode, result);
00535   }
00536 
00537   endNode->nextBddNode = requestNodeListForITE;
00538   hashTable->endNode = endNode;
00539   /* ITE Cleanup */
00540   for(bddId = 1; bddId <= bddManager->numVars; bddId++){
00541     CalHashTableCleanUp(reqQueForITE[bddId]);
00542   }
00543 }
00544