src/calBdd/calReduce.c File Reference

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

Go to the source code of this file.

Functions

static Cal_Bdd_t BddReduceBF (Cal_BddManager_t *bddManager, CalOpProc_t calOpProc, Cal_Bdd_t f, Cal_Bdd_t c)
static Cal_Bdd_t BddCofactorBF (Cal_BddManager_t *bddManager, CalOpProc_t calOpProc, Cal_Bdd_t f, Cal_Bdd_t c)
static void HashTableReduceApply (Cal_BddManager_t *bddManager, CalHashTable_t *hashTable, CalHashTable_t **reduceHashTableArray, CalHashTable_t **orHashTableArray, CalOpProc_t calOpProc)
static void HashTableCofactorApply (Cal_BddManager_t *bddManager, CalHashTable_t *hashTable, CalHashTable_t **cofactorHashTableArray, CalOpProc_t calOpProc)
static void HashTableCofactorReduce (Cal_BddManager_t *bddManager, CalHashTable_t *hashTable, CalHashTable_t *uniqueTableForId)
Cal_Bdd Cal_BddCofactor (Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd cUserBdd)
Cal_Bdd Cal_BddReduce (Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd cUserBdd)
Cal_Bdd Cal_BddBetween (Cal_BddManager bddManager, Cal_Bdd fMinUserBdd, Cal_Bdd fMaxUserBdd)
int CalOpCofactor (Cal_BddManager_t *bddManager, Cal_Bdd_t f, Cal_Bdd_t c, Cal_Bdd_t *resultBddPtr)

Function Documentation

static Cal_Bdd_t BddCofactorBF ( Cal_BddManager_t *  bddManager,
CalOpProc_t  calOpProc,
Cal_Bdd_t  f,
Cal_Bdd_t  c 
) [static]

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 340 of file calReduce.c.

00344 {
00345   Cal_Bdd_t result;
00346   CalHashTable_t  *hashTable;
00347   CalHashTable_t **cofactorHashTableArray = bddManager->reqQue[0];
00348   CalHashTable_t *uniqueTableForId;
00349   
00350 /*Cal_BddIndex_t minIndex;*/
00351   int minIndex;
00352   int bddIndex;
00353   Cal_BddId_t bddId, minId;
00354   
00355   if (CalBddIsBddZero(bddManager, c)){
00356     CalBddWarningMessage("Bdd Cofactor Called with zero care set");
00357     return bddManager->bddOne;
00358   }
00359   
00360   if (calOpProc(bddManager, f, c, &result) == 1){
00361     return result;
00362   }
00363 
00364   CalBddGetMinIdAndMinIndex(bddManager, f, c, minId, minIndex);
00365   CalHashTableFindOrAdd(cofactorHashTableArray[minId], f, c, &result); 
00366   for (bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
00367     bddId = bddManager->indexToId[bddIndex];
00368     hashTable = cofactorHashTableArray[bddId];
00369     if(hashTable->numEntries){
00370       HashTableCofactorApply(bddManager, hashTable, cofactorHashTableArray,
00371                              calOpProc); 
00372     }
00373   }
00374   for(bddIndex = bddManager->numVars - 1; bddIndex >= minIndex; bddIndex--){
00375     bddId = bddManager->indexToId[bddIndex];
00376     uniqueTableForId = bddManager->uniqueTable[bddId];
00377     hashTable = cofactorHashTableArray[bddId];
00378     if(hashTable->numEntries){
00379         HashTableCofactorReduce(bddManager, hashTable, uniqueTableForId);
00380     }
00381   }
00382   CalRequestIsForwardedTo(result);
00383   for (bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
00384     bddId = bddManager->indexToId[bddIndex];
00385     CalHashTableCleanUp(cofactorHashTableArray[bddId]);
00386   }
00387   return result;
00388 }

static Cal_Bdd_t BddReduceBF ( Cal_BddManager_t *  bddManager,
CalOpProc_t  calOpProc,
Cal_Bdd_t  f,
Cal_Bdd_t  c 
) [static]

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

FileName [calReduce.c]

PackageName [cal]

Synopsis [Routines for optimizing a BDD with respect to a don't care set (cofactor and restrict).]

Description []

SeeAlso [None]

Author [Rajeev K. Ranjan (rajeev@eecs.berkeley.edu) and Jagesh V. 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
calReduce.c,v 1.3 2002/09/21 20:39:25 fabio Exp

]AutomaticStart

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 280 of file calReduce.c.

00285 {
00286   Cal_Bdd_t result;
00287   CalHashTable_t  *hashTable;
00288   CalHashTable_t **orHashTableArray = bddManager->reqQue[0];
00289   CalHashTable_t **reduceHashTableArray = bddManager->reqQue[1];
00290   CalHashTable_t *uniqueTableForId;
00291   
00292   /*Cal_BddIndex_t minIndex;*/
00293   int minIndex;
00294   int bddIndex;
00295   Cal_BddId_t bddId, minId;
00296   
00297   
00298   if ((*calOpProc)(bddManager, f, c, &result) == 1){
00299     return result;
00300   }
00301 
00302   CalBddGetMinIdAndMinIndex(bddManager, f, c, minId, minIndex);
00303   CalHashTableFindOrAdd(reduceHashTableArray[minId], f, c, &result); 
00304   for (bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
00305     bddId = bddManager->indexToId[bddIndex];
00306     hashTable = reduceHashTableArray[bddId];
00307     if(hashTable->numEntries){
00308       HashTableReduceApply(bddManager, hashTable, reduceHashTableArray,
00309                            orHashTableArray, CalOpCofactor);
00310     }
00311   }
00312   for(bddIndex = bddManager->numVars - 1; bddIndex >= minIndex; bddIndex--){
00313     bddId = bddManager->indexToId[bddIndex];
00314     uniqueTableForId = bddManager->uniqueTable[bddId];
00315     hashTable = reduceHashTableArray[bddId];
00316     if(hashTable->numEntries){
00317         HashTableCofactorReduce(bddManager, hashTable, uniqueTableForId);
00318     }
00319   }
00320   CalRequestIsForwardedTo(result);
00321   for (bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
00322     bddId = bddManager->indexToId[bddIndex];
00323     CalHashTableCleanUp(reduceHashTableArray[bddId]);
00324   }
00325   return result;
00326 }

Cal_Bdd Cal_BddBetween ( Cal_BddManager  bddManager,
Cal_Bdd  fMinUserBdd,
Cal_Bdd  fMaxUserBdd 
)

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

Synopsis [Returns a minimal BDD whose function contains fMin and is contained in fMax.]

Description [Returns a minimal BDD f which is contains fMin and is contained in fMax ( fMin <= f <= fMax). This operation is typically used in state space searches to simplify the representation for the set of states wich will be expanded at each step (Rk Rk-1' <= f <= Rk).]

SideEffects [None]

SeeAlso [Cal_BddReduce]

Definition at line 185 of file calReduce.c.

00187 {
00188   if (CalBddPreProcessing(bddManager, 2, fMinUserBdd, fMaxUserBdd)){
00189     Cal_Bdd_t fMin = CalBddGetInternalBdd(bddManager, fMinUserBdd);
00190     Cal_Bdd_t fMax = CalBddGetInternalBdd(bddManager, fMaxUserBdd);
00191     Cal_Bdd_t fMaxNot, careSet, result;
00192     Cal_Bdd resultUserBdd;
00193     long fMinSize, fMaxSize, resultSize;
00194 
00195     CalBddNot(fMax, fMaxNot);
00196     careSet = CalBddOpBF(bddManager, CalOpOr, fMin, fMaxNot);
00197     result = BddReduceBF(bddManager, CalOpCofactor, fMin, careSet);
00198     resultUserBdd =  CalBddGetExternalBdd(bddManager, result);
00199     if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){
00200       Cal_BddFree(bddManager, resultUserBdd);
00201       Cal_BddManagerGC(bddManager);
00202       return (Cal_Bdd) 0;
00203     }
00204     fMinSize = Cal_BddSize(bddManager, fMinUserBdd, 1);
00205     fMaxSize = Cal_BddSize(bddManager, fMaxUserBdd, 1);
00206     resultSize = Cal_BddSize(bddManager, resultUserBdd, 1);
00207     if (resultSize < fMinSize){
00208       if (resultSize < fMaxSize){
00209         return resultUserBdd;
00210       }
00211       else {
00212         Cal_BddFree(bddManager, resultUserBdd);
00213         return Cal_BddIdentity(bddManager, fMaxUserBdd);
00214       }
00215     }
00216     Cal_BddFree(bddManager, resultUserBdd);
00217     if (fMinSize < fMaxSize){
00218       return Cal_BddIdentity(bddManager, fMinUserBdd);
00219     }
00220     else{
00221       return Cal_BddIdentity(bddManager, fMaxUserBdd);
00222     }
00223   }
00224   return (Cal_Bdd) 0;
00225 }

Cal_Bdd Cal_BddCofactor ( Cal_BddManager  bddManager,
Cal_Bdd  fUserBdd,
Cal_Bdd  cUserBdd 
)

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

Synopsis [Returns the generalized cofactor of BDD f with respect to BDD c.]

Description [Returns the generalized cofactor of BDD f with respect to BDD c. The constrain operator given by Coudert et al (ICCAD90) is used to find the generalized cofactor.]

SideEffects [None.]

SeeAlso [Cal_BddReduce]

Definition at line 100 of file calReduce.c.

00102 {
00103   Cal_Bdd_t result;
00104   Cal_Bdd userResult;
00105   if (CalBddPreProcessing(bddManager, 2, fUserBdd, cUserBdd)){
00106     Cal_Bdd_t f = CalBddGetInternalBdd(bddManager, fUserBdd);
00107     Cal_Bdd_t c = CalBddGetInternalBdd(bddManager, cUserBdd);
00108     result = BddCofactorBF(bddManager, CalOpCofactor, f, c);
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 Cal_BddReduce ( Cal_BddManager  bddManager,
Cal_Bdd  fUserBdd,
Cal_Bdd  cUserBdd 
)

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

Synopsis [Returns a BDD which agrees with f for all valuations which satisfy c.]

Description [Returns a BDD which agrees with f for all valuations which satisfy c. The result is usually smaller in terms of number of BDD nodes than f. This operation is typically used in state space searches to simplify the representation for the set of states wich will be expanded at each step.]

SideEffects [None]

SeeAlso [Cal_BddCofactor]

Definition at line 138 of file calReduce.c.

00140 {
00141   if (CalBddPreProcessing(bddManager, 2, fUserBdd, cUserBdd)){
00142     Cal_Bdd_t f = CalBddGetInternalBdd(bddManager, fUserBdd);
00143     Cal_Bdd_t c = CalBddGetInternalBdd(bddManager, cUserBdd);
00144     Cal_Bdd_t result;
00145     Cal_Bdd userResult;
00146 
00147     result = BddReduceBF(bddManager, CalOpCofactor, f, c);
00148     userResult =  CalBddGetExternalBdd(bddManager, result);
00149 
00150     if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){
00151       Cal_BddFree(bddManager, userResult);
00152       Cal_BddManagerGC(bddManager);
00153       return (Cal_Bdd) 0;
00154     }
00155     if (Cal_BddSize(bddManager, userResult, 1) <
00156         Cal_BddSize(bddManager, fUserBdd, 1)){
00157       return userResult;
00158     }
00159     else{
00160       Cal_BddFree(bddManager, userResult);
00161       return Cal_BddIdentity(bddManager, fUserBdd);
00162     }
00163   }
00164   return (Cal_Bdd) 0;
00165 }

int CalOpCofactor ( Cal_BddManager_t *  bddManager,
Cal_Bdd_t  f,
Cal_Bdd_t  c,
Cal_Bdd_t *  resultBddPtr 
)

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 243 of file calReduce.c.

00248 {
00249   if (CalBddIsBddConst(c)){
00250     if (CalBddIsBddZero(bddManager, c)){
00251       *resultBddPtr = bddManager->bddNull;
00252     }
00253     else {
00254       *resultBddPtr = f;
00255     }
00256     return 1;
00257   }
00258   if (CalBddIsBddConst(f)){
00259     *resultBddPtr = f;
00260     return 1;
00261   }
00262   return 0;
00263 }

static void HashTableCofactorApply ( Cal_BddManager_t *  bddManager,
CalHashTable_t *  hashTable,
CalHashTable_t **  cofactorHashTableArray,
CalOpProc_t  calOpProc 
) [static]

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 519 of file calReduce.c.

00523 {
00524   int i, numBins = hashTable->numBins;
00525   CalBddNode_t **bins = hashTable->bins;
00526   CalRequestNode_t *requestNode;
00527   Cal_Bdd_t f, c, fx, cx, fxbar, cxbar, result;
00528   Cal_BddId_t bddId, minId;
00529 
00530   for(i = 0; i < numBins; i++){
00531     for(requestNode = bins[i];
00532         requestNode != Cal_Nil(CalRequestNode_t);
00533         requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
00534       CalRequestNodeGetF(requestNode, f);
00535       CalRequestNodeGetG(requestNode, c);
00536       CalBddGetMinId2(bddManager, f, c, minId);
00537       CalBddGetCofactors(f, minId, fx, fxbar);
00538       CalBddGetCofactors(c, minId, cx, cxbar);
00539       if((*calOpProc)(bddManager, fx, cx, &result) == 0){
00540         CalBddGetMinId2(bddManager, fx, cx, bddId);
00541         CalHashTableFindOrAdd(cofactorHashTableArray[bddId], fx, cx, &result);
00542       }
00543       if (CalBddIsBddNull(bddManager, result) == 0){
00544         CalBddIcrRefCount(result);
00545       }
00546       CalRequestNodePutThenRequest(requestNode, result);
00547       if((*calOpProc)(bddManager, fxbar, cxbar, &result) == 0){
00548         CalBddGetMinId2(bddManager, fxbar, cxbar, bddId);
00549         CalHashTableFindOrAdd(cofactorHashTableArray[bddId], fxbar, cxbar,
00550                               &result);
00551       }
00552       if (CalBddIsBddNull(bddManager, result) == 0){
00553           CalBddIcrRefCount(result);
00554       }
00555       CalRequestNodePutElseRequest(requestNode, result);
00556     }
00557   }
00558 }

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

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 572 of file calReduce.c.

00575 {
00576   int i, numBins = hashTable->numBins;
00577   CalBddNode_t **bins = hashTable->bins;
00578   Cal_BddId_t currentBddId = uniqueTableForId->bddId;
00579   CalNodeManager_t *nodeManager = uniqueTableForId->nodeManager;
00580   CalRequestNode_t  *requestNode, *next, *endNode;
00581   CalBddNode_t *bddNode;
00582   Cal_Bdd_t thenBdd, elseBdd, result;
00583   Cal_BddRefCount_t refCount;
00584 
00585   endNode = hashTable->endNode;
00586   for(i = 0; i < numBins; i++){
00587     for(requestNode = bins[i], bins[i] = Cal_Nil(CalRequestNode_t);
00588         requestNode != Cal_Nil(CalRequestNode_t);
00589         requestNode = next){
00590       next = CalRequestNodeGetNextRequestNode(requestNode);
00591       /* Process the requestNode */
00592       CalRequestNodeGetThenRequest(requestNode, thenBdd);
00593       CalRequestNodeGetElseRequest(requestNode, elseBdd);
00594       if (CalBddIsBddNull(bddManager, thenBdd)){
00595         CalRequestIsForwardedTo(elseBdd);
00596         CalBddNodeGetRefCount(requestNode, refCount);
00597         CalBddAddRefCount(elseBdd, refCount - 1);
00598         CalRequestNodePutThenRequest(requestNode, elseBdd);
00599         CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
00600         endNode->nextBddNode = requestNode;
00601         endNode = requestNode;
00602         continue;
00603       }
00604       else if (CalBddIsBddNull(bddManager, elseBdd)){
00605         CalRequestIsForwardedTo(thenBdd);
00606         CalBddNodeGetRefCount(requestNode, refCount);
00607         CalBddAddRefCount(thenBdd, refCount - 1);
00608         CalRequestNodePutThenRequest(requestNode, thenBdd);
00609         CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
00610         endNode->nextBddNode = requestNode;
00611         endNode = requestNode;
00612         continue;
00613       }
00614       CalRequestIsForwardedTo(thenBdd);
00615       CalRequestIsForwardedTo(elseBdd);
00616       if(CalBddIsEqual(thenBdd, elseBdd)){
00617         CalBddNodeGetRefCount(requestNode, refCount);
00618         CalBddAddRefCount(thenBdd, refCount - 2);
00619         CalRequestNodePutThenRequest(requestNode, thenBdd);
00620         CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
00621         endNode->nextBddNode = requestNode;
00622         endNode = requestNode;
00623       }
00624       else if(CalUniqueTableForIdLookup(bddManager, uniqueTableForId,
00625           thenBdd, elseBdd, &result) == 1){
00626         CalBddDcrRefCount(thenBdd);
00627         CalBddDcrRefCount(elseBdd);
00628         CalBddNodeGetRefCount(requestNode, refCount);
00629         CalBddAddRefCount(result, refCount);
00630         CalRequestNodePutThenRequest(requestNode, result);
00631         CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
00632         endNode->nextBddNode = requestNode;
00633         endNode = requestNode;
00634       }
00635       else if(CalBddIsOutPos(thenBdd)){
00636         CalRequestNodePutThenRequest(requestNode, thenBdd);
00637         CalRequestNodePutElseRequest(requestNode, elseBdd);
00638         CalHashTableAddDirect(uniqueTableForId, requestNode);
00639         bddManager->numNodes++;
00640         bddManager->gcCheck--;
00641       }
00642       else{
00643         CalNodeManagerAllocNode(nodeManager, bddNode);
00644         CalBddNodePutThenBddId(bddNode, CalBddGetBddId(thenBdd));
00645         CalBddNodePutThenBddNode(bddNode, CalBddGetBddNodeNot(thenBdd));
00646         CalBddNodePutElseBddId(bddNode, CalBddGetBddId(elseBdd));
00647         CalBddNodePutElseBddNode(bddNode, CalBddGetBddNodeNot(elseBdd));
00648         CalBddNodeGetRefCount(requestNode, refCount);
00649         CalBddNodePutRefCount(bddNode, refCount);
00650         CalHashTableAddDirect(uniqueTableForId, bddNode);
00651         bddManager->numNodes++;
00652         bddManager->gcCheck--;
00653         CalRequestNodePutThenRequestId(requestNode, currentBddId);
00654         CalRequestNodePutThenRequestNode(requestNode, CalBddNodeNot(bddNode));
00655         CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
00656         endNode->nextBddNode = requestNode;
00657         endNode = requestNode;
00658       }
00659     }
00660   }
00661   hashTable->endNode = endNode;
00662 }

static void HashTableReduceApply ( Cal_BddManager_t *  bddManager,
CalHashTable_t *  hashTable,
CalHashTable_t **  reduceHashTableArray,
CalHashTable_t **  orHashTableArray,
CalOpProc_t  calOpProc 
) [static]

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 402 of file calReduce.c.

00407 {
00408   int i, numBins = hashTable->numBins;
00409   CalRequestNode_t *requestNode, *last, *nextRequestNode, *requestNodeList;
00410   Cal_Bdd_t f, c, fx, cx, fxbar, cxbar, result, orResult;
00411   Cal_BddId_t bddId, minId;
00412   /*Cal_BddIndex_t minIndex;*/
00413   int minIndex;
00414   int bddIndex;
00415   CalHashTable_t *orHashTable;
00416   
00417   requestNodeList = Cal_Nil(CalRequestNode_t);
00418   for(i = 0; i < numBins; i++){
00419     last = Cal_Nil(CalRequestNode_t);
00420     for (requestNode =  hashTable->bins[i]; requestNode !=
00421                                                 Cal_Nil(CalRequestNode_t);
00422          requestNode = nextRequestNode){
00423       nextRequestNode = CalRequestNodeGetNextRequestNode(requestNode);  
00424       CalRequestNodeGetF(requestNode, f);
00425       CalRequestNodeGetG(requestNode, c);
00426       CalBddGetMinId2(bddManager, f, c, minId);
00427       CalBddGetCofactors(c, minId, cx, cxbar);
00428       if (CalBddGetBddId(f) != minId){
00429         if (CalOpOr(bddManager, cx, cxbar, &orResult) == 0){
00430           CalBddNormalize(cx, cxbar);
00431           CalBddGetMinId2(bddManager, cx, cxbar, minId);
00432           CalHashTableFindOrAdd(orHashTableArray[minId], cx, cxbar, &orResult);
00433         }
00434         CalRequestNodePutElseRequest(requestNode, orResult);
00435         if (last == Cal_Nil(CalRequestNode_t)){
00436           hashTable->bins[i] = nextRequestNode;
00437         }
00438         else {
00439           CalRequestNodePutNextRequestNode(last, nextRequestNode);
00440         }
00441         CalRequestNodePutNextRequestNode(requestNode, requestNodeList);
00442         requestNodeList = requestNode;
00443       }
00444       else{
00445         last = requestNode;
00446         CalBddGetCofactors(f, minId, fx, fxbar);
00447         if((*calOpProc)(bddManager, fx, cx, &result) == 0){
00448           CalBddGetMinId2(bddManager, fx, cx, bddId);
00449           CalHashTableFindOrAdd(reduceHashTableArray[bddId], fx, cx, &result);
00450         }
00451         if (CalBddIsBddNull(bddManager, result) == 0){
00452           CalBddIcrRefCount(result);
00453         }
00454         CalRequestNodePutThenRequest(requestNode, result);
00455         if((*calOpProc)(bddManager, fxbar, cxbar, &result) == 0){
00456           CalBddGetMinId2(bddManager, fxbar, cxbar, bddId);
00457           CalHashTableFindOrAdd(reduceHashTableArray[bddId], fxbar, cxbar,
00458                                 &result);
00459         }
00460         if (CalBddIsBddNull(bddManager, result) == 0){
00461           CalBddIcrRefCount(result);
00462         }
00463         CalRequestNodePutElseRequest(requestNode, result);
00464       }
00465     }
00466   }
00467   minIndex = bddManager->idToIndex[hashTable->bddId];
00468   for (bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
00469     bddId = bddManager->indexToId[bddIndex];
00470     orHashTable = orHashTableArray[bddId];
00471     if(orHashTable->numEntries){
00472       CalHashTableApply(bddManager, orHashTable, orHashTableArray, CalOpOr);
00473     }
00474   }
00475   
00476   for(bddIndex = bddManager->numVars - 1; bddIndex >= minIndex; bddIndex--){
00477     CalHashTable_t *uniqueTableForId;
00478     bddId = bddManager->indexToId[bddIndex];
00479     uniqueTableForId = bddManager->uniqueTable[bddId];
00480     orHashTable = orHashTableArray[bddId];
00481     if(orHashTable->numEntries){
00482       CalHashTableReduce(bddManager, orHashTable, uniqueTableForId);
00483     }
00484   }
00485   for (requestNode = requestNodeList; requestNode; requestNode =
00486                                                        nextRequestNode){
00487     nextRequestNode = CalRequestNodeGetNextRequestNode(requestNode);
00488     CalRequestNodeGetElseRequest(requestNode, orResult);
00489     CalRequestIsForwardedTo(orResult);
00490     CalRequestNodeGetThenRequest(requestNode, f);
00491     CalBddGetMinId2(bddManager, f, orResult, minId);
00492     CalHashTableFindOrAdd(reduceHashTableArray[minId], f, orResult,
00493                           &result);
00494     CalRequestNodePutThenRequest(requestNode, result);
00495     CalRequestNodePutElseRequest(requestNode, result);
00496     CalBddAddRefCount(result, 2);
00497     CalHashTableAddDirect(hashTable, requestNode);
00498   }
00499   
00500   /* Clean up the orHashTableArray */
00501   for(bddIndex = bddManager->numVars - 1; bddIndex >= minIndex; bddIndex--){
00502     bddId = bddManager->indexToId[bddIndex];
00503     CalHashTableCleanUp(orHashTableArray[bddId]);
00504   }
00505 }

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