src/calBdd/calBddSubstitute.c File Reference

#include "calInt.h"
Include dependency graph for calBddSubstitute.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)
static void CalHashTableSubstituteReduce (Cal_BddManager_t *bddManager, CalHashTable_t *hashTable, CalHashTable_t **reqQueForITE, CalHashTable_t *uniqueTableForId)
Cal_Bdd Cal_BddSubstitute (Cal_BddManager bddManager, Cal_Bdd fUserBdd)

Function Documentation

Cal_Bdd Cal_BddSubstitute ( Cal_BddManager  bddManager,
Cal_Bdd  fUserBdd 
)

AutomaticEnd 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 93 of file calBddSubstitute.c.

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 }

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

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

FileName [calBddSubstitute.c]

PackageName [cal]

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

Description [Routine for simultaneous substitution of an array of variables with an array of functions.]

SeeAlso [optional]

Author [Jagesh Sanghavi (sanghavi@eecs.berkeley.edu) Rajeev Ranjan (rajeev@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
calBddSubstitute.c,v 1.1.1.4 1998/05/04 00:58:54 hsv Exp

]AutomaticStart

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 166 of file calBddSubstitute.c.

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 }

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

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 223 of file calBddSubstitute.c.

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 }

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