src/calBdd/calBddVarSubstitute.c File Reference

#include "calInt.h"
Include dependency graph for calBddVarSubstitute.c:

Go to the source code of this file.

Functions

static void CalHashTableSubstituteApply (Cal_BddManager_t *bddManager, CalHashTable_t *hashTable, int lastIndex, CalHashTable_t **reqQueForSubstitute, unsigned short opCode)
static void CalHashTableSubstituteReduce (Cal_BddManager_t *bddManager, CalHashTable_t *hashTable, CalHashTable_t **reqQueForITE, CalHashTable_t *uniqueTableForId, unsigned short opCode)
Cal_Bdd Cal_BddVarSubstitute (Cal_BddManager bddManager, Cal_Bdd fUserBdd)
Cal_Bdd_t CalBddVarSubstitute (Cal_BddManager bddManager, Cal_Bdd_t f, unsigned short opCode, CalAssociation_t *assoc)
int CalOpBddVarSubstitute (Cal_BddManager_t *bddManager, Cal_Bdd_t f, Cal_Bdd_t *resultBddPtr)

Function Documentation

Cal_Bdd Cal_BddVarSubstitute ( Cal_BddManager  bddManager,
Cal_Bdd  fUserBdd 
)

AutomaticEnd Function********************************************************************

Synopsis [Substitute a set of variables by set of another variables.]

Description [Returns a BDD for f using the substitution defined by current variable association. It is assumed that each variable is replaced by another variable. For the substitution of a variable by a function, use Cal_BddSubstitute instead.]

SideEffects [None]

SeeAlso [Cal_BddSubstitute]

Definition at line 93 of file calBddVarSubstitute.c.

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 }

Cal_Bdd_t CalBddVarSubstitute ( Cal_BddManager  bddManager,
Cal_Bdd_t  f,
unsigned short  opCode,
CalAssociation_t *  assoc 
)

Function********************************************************************

Synopsis [Substitute a set of variables by functions]

Description [Returns a BDD for f using the substitution defined by current variable association. Each variable is replaced by its associated BDDs. The substitution is effective simultaneously]

SideEffects [None]

SeeAlso [Cal_BddCompose]

Definition at line 143 of file calBddVarSubstitute.c.

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 }

static void CalHashTableSubstituteApply ( Cal_BddManager_t *  bddManager,
CalHashTable_t *  hashTable,
int  lastIndex,
CalHashTable_t **  reqQueForSubstitute,
unsigned short  opCode 
) [static]

CFile***********************************************************************

FileName [calBddVarSubstitute.c]

PackageName [cal]

Synopsis [Routine for simultaneous substitution of an array of variables with another array of variables.]

Description []

SeeAlso [optional]

Author [Rajeev Ranjan (rajeev@eecs.berkeley.edu) Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) ] Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California. All rights reserved.

Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.

IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]

Revision [

Id
calBddVarSubstitute.c,v 1.2 2002/09/10 00:27:21 fabio Exp

]AutomaticStart

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 236 of file calBddVarSubstitute.c.

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 }

static void CalHashTableSubstituteReduce ( Cal_BddManager_t *  bddManager,
CalHashTable_t *  hashTable,
CalHashTable_t **  reqQueForITE,
CalHashTable_t *  uniqueTableForId,
unsigned short  opCode 
) [static]

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 314 of file calBddVarSubstitute.c.

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 }

int CalOpBddVarSubstitute ( Cal_BddManager_t *  bddManager,
Cal_Bdd_t  f,
Cal_Bdd_t *  resultBddPtr 
)

Function********************************************************************

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 212 of file calBddVarSubstitute.c.

00214 {
00215   if (bddManager->idToIndex[CalBddGetBddId(f)] >
00216       bddManager->currentAssociation->lastBddIndex){ 
00217     *resultBddPtr = f;
00218     return 1;
00219   }
00220   return 0;
00221 }

Generated on Tue Jan 12 13:57:11 2010 for glu-2.2 by  doxygen 1.6.1