glu-2.2: src/calBdd/calBddSubstitute.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 void CalHashTableSubstituteApply(Cal_BddManager_t * bddManager, CalHashTable_t * hashTable, int lastIndex, CalHashTable_t ** reqQueForSubstitute);
00071 static void CalHashTableSubstituteReduce(Cal_BddManager_t * bddManager, CalHashTable_t * hashTable, CalHashTable_t ** reqQueForITE, CalHashTable_t * uniqueTableForId);
00072 
00075 /*---------------------------------------------------------------------------*/
00076 /* Definition of exported functions                                          */
00077 /*---------------------------------------------------------------------------*/
00078 
00092 Cal_Bdd
00093 Cal_BddSubstitute(Cal_BddManager bddManager, Cal_Bdd fUserBdd)
00094 {
00095   CalRequest_t result;
00096   int bddId, bddIndex, lastIndex;
00097   CalHashTable_t *hashTable;
00098   CalHashTable_t *uniqueTableForId;
00099   CalHashTable_t **reqQueForSubstitute = bddManager->reqQue[0];
00100   CalHashTable_t **reqQueForITE = bddManager->reqQue[1]; 
00101   Cal_Bdd_t f;
00102   
00103   if (CalBddPreProcessing(bddManager, 1, fUserBdd) == 0){
00104     return (Cal_Bdd) 0;
00105   }
00106   f = CalBddGetInternalBdd(bddManager, fUserBdd);  
00107   if(CalBddIsBddConst(f)){
00108     return CalBddGetExternalBdd(bddManager, f);
00109   }
00110 
00111   CalHashTableFindOrAdd(reqQueForSubstitute[CalBddGetBddId(f)], f, 
00112     bddManager->bddNull, &result);
00113 
00114   /* ReqQueApply */
00115   lastIndex = bddManager->currentAssociation->lastBddIndex;
00116   for(bddIndex = 0; bddIndex < bddManager->numVars; bddIndex++){
00117     bddId = bddManager->indexToId[bddIndex];
00118     hashTable = reqQueForSubstitute[bddId];
00119     if(hashTable->numEntries){
00120       CalHashTableSubstituteApply(bddManager, hashTable, lastIndex, 
00121                                   reqQueForSubstitute);
00122     }
00123   }
00124 
00125   /* ReqQueReduce */
00126   for(bddIndex = bddManager->numVars - 1; bddIndex >= 0; bddIndex--){
00127     bddId = bddManager->indexToId[bddIndex];
00128     uniqueTableForId = bddManager->uniqueTable[bddId];
00129     hashTable = reqQueForSubstitute[bddId];
00130     if(hashTable->numEntries){
00131       CalHashTableSubstituteReduce(bddManager, hashTable,
00132                                    reqQueForITE, uniqueTableForId);
00133     }
00134   }
00135 
00136   CalRequestIsForwardedTo(result);
00137 
00138   /* ReqQueCleanUp */
00139   for(bddId = 1; bddId <= bddManager->numVars; bddId++){
00140     CalHashTableCleanUp(reqQueForSubstitute[bddId]);
00141   }
00142 
00143   return CalBddGetExternalBdd(bddManager, result);
00144 }
00145 
00146 /*---------------------------------------------------------------------------*/
00147 /* Definition of internal functions                                          */
00148 /*---------------------------------------------------------------------------*/
00149 
00150 /*---------------------------------------------------------------------------*/
00151 /* Definition of static functions                                            */
00152 /*---------------------------------------------------------------------------*/
00153 
00165 static void
00166 CalHashTableSubstituteApply(
00167   Cal_BddManager_t * bddManager,
00168   CalHashTable_t * hashTable,
00169   int  lastIndex,
00170   CalHashTable_t ** reqQueForSubstitute)
00171 {
00172   int i, numBins = hashTable->numBins;
00173   CalBddNode_t **bins = hashTable->bins;
00174   CalRequestNode_t *requestNode;
00175   Cal_BddId_t bddId;
00176   /*Cal_BddIndex_t bddIndex;*/
00177   int bddIndex;
00178   Cal_Bdd_t f, calBdd;
00179   Cal_Bdd_t nullBdd = bddManager->bddNull;
00180 
00181   for(i = 0; i < numBins; i++){
00182     for(requestNode = bins[i];
00183         requestNode != Cal_Nil(CalRequestNode_t);
00184         requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
00185       /* Process the requestNode */
00186       CalRequestNodeGetF(requestNode, f);
00187       /* Process Left Cofactor */
00188       CalBddGetThenBdd(f, calBdd);
00189       bddId = CalBddGetBddId(calBdd);
00190       bddIndex = bddManager->idToIndex[bddId];
00191       if(bddIndex <= lastIndex){
00192         CalHashTableFindOrAdd(reqQueForSubstitute[bddId], calBdd, nullBdd, 
00193             &calBdd);
00194       }
00195       CalBddIcrRefCount(calBdd);
00196       CalRequestNodePutThenRequest(requestNode, calBdd);
00197       /* Process Right Cofactor */
00198       CalBddGetElseBdd(f, calBdd);
00199       bddId = CalBddGetBddId(calBdd);
00200       bddIndex = bddManager->idToIndex[bddId];
00201       if(bddIndex <= lastIndex){
00202         CalHashTableFindOrAdd(reqQueForSubstitute[bddId], calBdd, nullBdd, 
00203             &calBdd);
00204       }
00205       CalBddIcrRefCount(calBdd);
00206       CalRequestNodePutElseRequest(requestNode, calBdd);
00207     }
00208   }
00209 }
00210 
00222 static void
00223 CalHashTableSubstituteReduce(
00224   Cal_BddManager_t * bddManager,
00225   CalHashTable_t * hashTable,
00226   CalHashTable_t ** reqQueForITE,
00227   CalHashTable_t * uniqueTableForId)
00228 {
00229   int i, numBins = hashTable->numBins;
00230   CalBddNode_t **bins = hashTable->bins;
00231   Cal_BddId_t varBddId = hashTable->bddId;
00232   CalNodeManager_t *nodeManager = hashTable->nodeManager;
00233   /*CalRequestNode_t *requestNodeList = hashTable->requestNodeList;*/
00234   CalRequestNode_t *endNode = hashTable->endNode;
00235   CalRequestNode_t *requestNodeListForITE = Cal_Nil(CalRequestNode_t);
00236   CalRequestNode_t *requestNode, *next;
00237   CalBddNode_t *bddNode;
00238   Cal_Bdd_t varBdd;
00239   Cal_Bdd_t thenBdd, elseBdd, result;
00240   Cal_Bdd_t h;
00241   Cal_BddIndex_t varBddIndex;
00242   Cal_BddRefCount_t refCount;
00243   int bddId, bddIndex;
00244   CalHashTable_t *hashTableForITE;
00245 
00246   varBddIndex = bddManager->idToIndex[varBddId];
00247   varBdd = bddManager->varBdds[varBddId];
00248   h = bddManager->currentAssociation->varAssociation[varBddId];
00249   if(!CalBddIsBddNull(bddManager, h)){
00250     for(i = 0; i < numBins; i++){
00251       for(requestNode = bins[i], bins[i] = Cal_Nil(CalRequestNode_t);
00252           requestNode != Cal_Nil(CalRequestNode_t);
00253           requestNode = next){
00254         next = CalRequestNodeGetNextRequestNode(requestNode);
00255         /* Process the requestNode */
00256         CalRequestNodeGetThenRequest(requestNode, thenBdd);
00257         CalRequestNodeGetElseRequest(requestNode, elseBdd);
00258         CalRequestIsForwardedTo(thenBdd);
00259         CalRequestIsForwardedTo(elseBdd);
00260         if(CalBddIsEqual(thenBdd, elseBdd)){
00261           CalBddNodeGetRefCount(requestNode, refCount);
00262           CalBddAddRefCount(thenBdd, refCount - 2);
00263           CalRequestNodePutThenRequest(requestNode, thenBdd);
00264           CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
00265           endNode->nextBddNode = requestNode;
00266           endNode = requestNode;
00267         }
00268         else{
00269           CalBddDcrRefCount(thenBdd);
00270           CalBddDcrRefCount(elseBdd);
00271           result = CalOpITE(bddManager, h, thenBdd, elseBdd, reqQueForITE);
00272           CalRequestNodePutThenRequest(requestNode, result);
00273           CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
00274           CalRequestNodePutNextRequestNode(requestNode,
00275               requestNodeListForITE);
00276           requestNodeListForITE = requestNode;
00277         }
00278       }
00279     }
00280   }
00281   else{
00282     for(i = 0; i < numBins; i++){
00283       for(requestNode = bins[i], bins[i] = Cal_Nil(CalRequestNode_t);
00284           requestNode != Cal_Nil(CalRequestNode_t);
00285           requestNode = next){
00286         next = CalRequestNodeGetNextRequestNode(requestNode);
00287         /* Process the requestNode */
00288         CalRequestNodeGetThenRequest(requestNode, thenBdd);
00289         CalRequestNodeGetElseRequest(requestNode, elseBdd);
00290         CalRequestIsForwardedTo(thenBdd);
00291         CalRequestIsForwardedTo(elseBdd);
00292         if(CalBddIsEqual(thenBdd, elseBdd)){
00293           CalBddNodeGetRefCount(requestNode, refCount);
00294           CalBddAddRefCount(thenBdd, refCount - 2);
00295           CalRequestNodePutThenRequest(requestNode, thenBdd);
00296           CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
00297           endNode->nextBddNode = requestNode;
00298           endNode = requestNode;
00299         }
00300         else if(varBddIndex < CalBddGetBddIndex(bddManager, thenBdd) &&
00301             varBddIndex < CalBddGetBddIndex(bddManager, elseBdd)){
00302           if(CalUniqueTableForIdLookup(bddManager, uniqueTableForId,
00303               thenBdd, elseBdd, &result) == 1){
00304             CalBddDcrRefCount(thenBdd);
00305             CalBddDcrRefCount(elseBdd);
00306             CalBddNodeGetRefCount(requestNode, refCount);
00307             CalBddAddRefCount(result, refCount);
00308             CalRequestNodePutThenRequest(requestNode, result);
00309             CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
00310             endNode->nextBddNode = requestNode;
00311             endNode = requestNode;
00312           }
00313           else if(CalBddIsOutPos(thenBdd)){
00314             CalRequestNodePutThenRequest(requestNode, thenBdd);
00315             CalRequestNodePutElseRequest(requestNode, elseBdd);
00316             CalHashTableAddDirect(uniqueTableForId, requestNode);
00317             bddManager->numNodes++;
00318             bddManager->gcCheck--;
00319           }
00320           else{
00321             CalNodeManagerAllocNode(nodeManager, bddNode);
00322             CalBddNodePutThenBddId(bddNode, CalBddGetBddId(thenBdd));
00323             CalBddNodePutThenBddNode(bddNode,
00324                 CalBddGetBddNodeNot(thenBdd));
00325             CalBddNodePutElseBddId(bddNode, CalBddGetBddId(elseBdd));
00326             CalBddNodePutElseBddNode(bddNode,
00327                 CalBddGetBddNodeNot(elseBdd));
00328             CalBddNodeGetRefCount(requestNode, refCount);
00329             CalBddNodePutRefCount(bddNode, refCount);
00330             CalHashTableAddDirect(uniqueTableForId, bddNode);
00331             bddManager->numNodes++;
00332             bddManager->gcCheck--;
00333             CalRequestNodePutThenRequestId(requestNode, varBddId);
00334             CalRequestNodePutThenRequestNode(requestNode,
00335                 CalBddNodeNot(bddNode));
00336             CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
00337             endNode->nextBddNode = requestNode;
00338             endNode = requestNode;
00339           }
00340         }
00341         else{
00342           CalBddDcrRefCount(thenBdd);
00343           CalBddDcrRefCount(elseBdd);
00344           result = CalOpITE(bddManager, varBdd, thenBdd, elseBdd, reqQueForITE);
00345           CalRequestNodePutThenRequest(requestNode, result);
00346           CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
00347           CalRequestNodePutNextRequestNode(requestNode,
00348               requestNodeListForITE);
00349           requestNodeListForITE = requestNode;
00350         }
00351       }
00352     }
00353   }
00354 
00355   /* ITE Apply */
00356   for(bddIndex = 0; bddIndex < bddManager->numVars; bddIndex++){
00357     bddId = bddManager->indexToId[bddIndex];
00358     hashTableForITE = reqQueForITE[bddId];
00359     if(hashTableForITE->numEntries){
00360       CalHashTableITEApply(bddManager, hashTableForITE, reqQueForITE);
00361     }
00362   }
00363   /* ITE Reduce */
00364   for(bddIndex = bddManager->numVars - 1; bddIndex >= 0; bddIndex--){
00365     bddId = bddManager->indexToId[bddIndex];
00366     hashTableForITE = reqQueForITE[bddId];
00367     if(hashTableForITE->numEntries){
00368       CalHashTableReduce(bddManager, hashTableForITE,
00369           bddManager->uniqueTable[bddId]);
00370     }
00371   }
00372     
00373 
00374   /*last = Cal_Nil(CalRequestNode_t);*/
00375   for(requestNode = requestNodeListForITE; 
00376       requestNode != Cal_Nil(CalRequestNode_t);
00377       /*last = requestNode, */
00378       requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
00379     CalRequestNodeGetThenRequest(requestNode, result);
00380     CalBddNodeGetRefCount(requestNode, refCount);
00381     CalRequestIsForwardedTo(result);
00382     CalBddAddRefCount(result, refCount);
00383     CalRequestNodePutThenRequest(requestNode, result);
00384   }
00385 
00386   /*CalBddNodePutNextBddNode(endNode, requestNodeListForITE);*/
00387   endNode->nextBddNode = requestNodeListForITE;
00388   hashTable->endNode = endNode;
00389   
00390   /* ITE Cleanup */
00391   for(bddId = 1; bddId <= bddManager->numVars; bddId++){
00392     CalHashTableCleanUp(reqQueForITE[bddId]);
00393   }
00394 }
00395 
00396 
00397 
00398 
00399 
00400 
00401 
00402 
00403 
00404 
00405 
00406 
00407