src/calBdd/calQuant.c File Reference

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

Go to the source code of this file.

Defines

#define DEFAULT_EXIST_HASH_TABLE_SIZE_INDEX   4
#define DEFAULT_EXIST_HASH_TABLE_SIZE   16

Functions

static Cal_Bdd_t BddExistsStep (Cal_BddManager_t *bddManager, Cal_Bdd_t f, unsigned short opCode, CalAssociation_t *association)
static Cal_Bdd_t BddRelProdStep (Cal_BddManager_t *bddManager, Cal_Bdd_t f, Cal_Bdd_t g, unsigned short opCode, CalAssociation_t *assoc)
static Cal_Bdd_t BddDFStep (Cal_BddManager_t *bddManager, Cal_Bdd_t f, Cal_Bdd_t g, CalOpProc_t calOpProc, unsigned short opCode)
static void HashTableApply (Cal_BddManager_t *bddManager, CalHashTable_t *hashTable, CalHashTable_t **reqQueAtPipeDepth, CalOpProc_t calOpProc, unsigned long opCode)
static void HashTableReduce (Cal_BddManager_t *bddManager, CalHashTable_t *hashTable, CalHashTable_t *uniqueTableForId)
static void BddExistsApply (Cal_BddManager_t *bddManager, int quantifying, CalHashTable_t *existHashTable, CalHashTable_t **existHashTableArray, CalOpProc1_t calOpProc, unsigned short opCode, CalAssociation_t *assoc)
static void BddExistsBFAux (Cal_BddManager_t *bddManager, int minIndex, CalHashTable_t **existHashTableArray, CalHashTable_t **orHashTableArray, CalOpProc1_t calOpProc, unsigned short opCode, CalAssociation_t *assoc)
static void BddExistsReduce (Cal_BddManager_t *bddManager, CalHashTable_t *existHashTable, CalHashTable_t **existHashTableArray, CalHashTable_t **orHashTableArray, unsigned short opCode, CalAssociation_t *association)
static Cal_Bdd_t BddExistsBFPlusDF (Cal_BddManager_t *bddManager, Cal_Bdd_t f, unsigned short opCode, CalAssociation_t *association)
static void BddRelProdApply (Cal_BddManager_t *bddManager, int quantifying, CalHashTable_t *relProdHashTable, CalHashTable_t **relProdHashTableArray, CalHashTable_t **andHashTableArray, CalOpProc_t calOpProc, unsigned short opCode, CalAssociation_t *assoc)
static void BddRelProdReduce (Cal_BddManager_t *bddManager, CalHashTable_t *relProdHashTable, CalHashTable_t **relProdHashTableArray, CalHashTable_t **andHashTableArray, CalHashTable_t **orHashTableArray, unsigned short opCode, CalAssociation_t *assoc)
static void BddRelProdBFAux (Cal_BddManager_t *bddManager, int minIndex, CalHashTable_t **relProdHashTableArray, CalHashTable_t **andHashTableArray, CalHashTable_t **orHashTableArray, unsigned short opCode, CalAssociation_t *assoc)
static Cal_Bdd_t BddRelProdBFPlusDF (Cal_BddManager_t *bddManager, Cal_Bdd_t f, Cal_Bdd_t g, unsigned short opCode, CalAssociation_t *association)
Cal_Bdd Cal_BddExists (Cal_BddManager bddManager, Cal_Bdd fUserBdd)
Cal_Bdd Cal_BddRelProd (Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd)
Cal_Bdd Cal_BddForAll (Cal_BddManager bddManager, Cal_Bdd fUserBdd)
int CalOpExists (Cal_BddManager_t *bddManager, Cal_Bdd_t f, Cal_Bdd_t *resultBddPtr)
int CalOpRelProd (Cal_BddManager_t *bddManager, Cal_Bdd_t f, Cal_Bdd_t g, Cal_Bdd_t *resultBddPtr)

Define Documentation

#define DEFAULT_EXIST_HASH_TABLE_SIZE   16

Definition at line 47 of file calQuant.c.

#define DEFAULT_EXIST_HASH_TABLE_SIZE_INDEX   4

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

FileName [calQuant.c]

PackageName [cal]

Synopsis [Routines for existential/universal quantification and relational product.]

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
calQuant.c,v 1.1.1.4 1998/05/04 00:59:02 hsv Exp

]

Definition at line 46 of file calQuant.c.

Function Documentation

static Cal_Bdd_t BddDFStep ( Cal_BddManager_t *  bddManager,
Cal_Bdd_t  f,
Cal_Bdd_t  g,
CalOpProc_t  calOpProc,
unsigned short  opCode 
) [static]

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 451 of file calQuant.c.

00453 {
00454   Cal_BddId_t topId;
00455   Cal_Bdd_t temp1, temp2, fx, fxbar, gx, gxbar;
00456   Cal_Bdd_t  result;
00457 
00458   if((*calOpProc)(bddManager, f, g, &result) == 1){
00459     return result;
00460   }
00461   CalBddNormalize(f, g);
00462   if(CalCacheTableTwoLookup(bddManager, f, g, opCode, &result)){
00463     return result;
00464   }
00465   CalBddGetMinId2(bddManager, f, g, topId);
00466   CalBddGetCofactors(f, topId, fx, fxbar);
00467   CalBddGetCofactors(g, topId, gx, gxbar);
00468   temp1 = BddDFStep(bddManager, fx, gx, calOpProc, opCode);
00469   temp2 = BddDFStep(bddManager, fxbar, gxbar, calOpProc, opCode);
00470 
00471   if (CalUniqueTableForIdFindOrAdd(bddManager,
00472                                    bddManager->uniqueTable[topId],
00473                                    temp1, temp2, &result) == 0){
00474     CalBddIcrRefCount(temp1);
00475     CalBddIcrRefCount(temp2);
00476   }
00477   CalCacheTableTwoInsert(bddManager, f, g, result, opCode, 0);
00478   return (result);
00479 }

static void BddExistsApply ( Cal_BddManager_t *  bddManager,
int  quantifying,
CalHashTable_t *  existHashTable,
CalHashTable_t **  existHashTableArray,
CalOpProc1_t  calOpProc,
unsigned short  opCode,
CalAssociation_t *  assoc 
) [static]

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 657 of file calQuant.c.

00661 {
00662   int i, numBins = existHashTable->numBins;
00663   CalBddNode_t **bins = existHashTable->bins;
00664   CalRequestNode_t *requestNode;
00665   Cal_Bdd_t f, fx, fxbar, result, resultBar;
00666   int lastBddIndex = assoc->lastBddIndex; 
00667   
00668   if (quantifying){
00669     for(i = 0; i < numBins; i++){
00670       for(requestNode = bins[i];
00671           requestNode != Cal_Nil(CalRequestNode_t);
00672           requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
00673         CalRequestNodeGetF(requestNode, f);
00674         CalBddGetThenBdd(f, fx);
00675         CalBddGetElseBdd(f, fxbar);
00676       
00677         /*if(calOpProc(bddManager, fx, &result) == 0){*/
00678         if (((int)bddManager->idToIndex[CalBddGetBddId(fx)]) <= lastBddIndex){
00679           if (CalCacheTableOneLookup(bddManager, fx, opCode, &result)){ 
00680             CalRequestIsForwardedTo(result);
00681           }
00682           else {
00683             CalHashTableFindOrAdd(existHashTableArray[CalBddGetBddId(fx)], fx,
00684                                   bddManager->bddOne, &result);
00685             CalCacheTableOneInsert(bddManager, fx, result,
00686                                    opCode, 1);
00687           }
00688         }
00689         else {
00690           result = fx;
00691         }
00692         CalRequestNodePutThenRequest(requestNode, result);
00693         CalRequestNodePutElseRequest(requestNode, fxbar);
00694       }
00695     }
00696   }
00697   else {
00698     for(i = 0; i < numBins; i++){
00699       for(requestNode = bins[i];
00700           requestNode != Cal_Nil(CalRequestNode_t);
00701           requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
00702         CalRequestNodeGetF(requestNode, f);
00703         CalBddGetThenBdd(f, fx);
00704         CalBddGetElseBdd(f, fxbar);
00705       
00706         if (((int)bddManager->idToIndex[CalBddGetBddId(fx)]) <= lastBddIndex){
00707           if (CalCacheTableOneLookup(bddManager, fx, opCode, &result)){ 
00708             CalRequestIsForwardedTo(result);
00709           }
00710           else {
00711             CalHashTableFindOrAdd(existHashTableArray[CalBddGetBddId(fx)], fx,
00712                                   bddManager->bddOne, &result);
00713             CalCacheTableOneInsert(bddManager, fx, result,
00714                                    opCode, 1);
00715           }
00716         }
00717         else {
00718           result = fx;
00719         }
00720         CalRequestNodePutThenRequest(requestNode, result);
00721         CalBddIcrRefCount(result);
00722         /*if(calOpProc(bddManager, fxbar, &resultBar) == 0){*/
00723         if (((int)bddManager->idToIndex[CalBddGetBddId(fxbar)]) <= lastBddIndex){
00724           if (CalCacheTableOneLookup(bddManager, fxbar, opCode,
00725                                        &resultBar)){
00726             CalRequestIsForwardedTo(resultBar);
00727           }
00728           else {
00729             CalHashTableFindOrAdd(existHashTableArray[CalBddGetBddId(fxbar)], fxbar,
00730                                   bddManager->bddOne, &resultBar);
00731             CalCacheTableOneInsert(bddManager, fxbar, resultBar,
00732                                    opCode, 1); 
00733           }
00734         }
00735         else{
00736           resultBar = fxbar;
00737         }
00738         CalBddIcrRefCount(resultBar);
00739         CalRequestNodePutElseRequest(requestNode, resultBar);
00740       }
00741     }
00742   }
00743 }

static void BddExistsBFAux ( Cal_BddManager_t *  bddManager,
int  minIndex,
CalHashTable_t **  existHashTableArray,
CalHashTable_t **  orHashTableArray,
CalOpProc1_t  calOpProc,
unsigned short  opCode,
CalAssociation_t *  assoc 
) [static]

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 757 of file calQuant.c.

00761 {
00762   int index;
00763   Cal_BddId_t bddId;
00764   int quantifying;
00765   
00766   /* Apply phase */
00767   for (index = minIndex; index < bddManager->numVars; index++){
00768     bddId = bddManager->indexToId[index];
00769     if (existHashTableArray[bddId]->numEntries){
00770       quantifying = (CalBddIsBddNull(bddManager,
00771                                      assoc->varAssociation[bddId]) ? 0 : 1); 
00772       BddExistsApply(bddManager, quantifying,
00773                      existHashTableArray[bddId], existHashTableArray,
00774                      calOpProc, opCode, assoc);    
00775     }
00776   }
00777   
00778   /* Reduce phase */
00779   for (index = bddManager->numVars-1; index >= minIndex; index--){
00780     bddId = bddManager->indexToId[index];
00781     if (existHashTableArray[bddId]->numEntries){
00782       quantifying = (CalBddIsBddNull(bddManager,
00783                                      assoc->varAssociation[bddId]) ? 0 : 1); 
00784       if (quantifying){
00785         BddExistsReduce(bddManager, existHashTableArray[bddId],
00786                         existHashTableArray, orHashTableArray,
00787                         opCode, assoc);
00788       } 
00789       else {
00790         HashTableReduce(bddManager, existHashTableArray[bddId],
00791                         bddManager->uniqueTable[bddId]);
00792       }
00793     }
00794   }
00795 }

static Cal_Bdd_t BddExistsBFPlusDF ( Cal_BddManager_t *  bddManager,
Cal_Bdd_t  f,
unsigned short  opCode,
CalAssociation_t *  association 
) [static]

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 979 of file calQuant.c.

00981 {
00982   Cal_BddId_t fId = CalBddGetBddId(f);
00983   Cal_BddIndex_t bddIndex;
00984   Cal_BddId_t bddId;
00985   
00986   Cal_BddIndex_t fIndex = bddManager->idToIndex[fId];
00987   CalHashTable_t **orHashTableArray = bddManager->reqQue[4];
00988   CalHashTable_t **existHashTableArray = bddManager->reqQue[5];
00989   Cal_Bdd_t result;
00990   
00991   if (CalOpExists(bddManager, f, &result) == 1){
00992     return result;
00993   }
00994 
00995   if (CalCacheTableOneLookup(bddManager, f, opCode, &result)){
00996     return result;
00997   }
00998   
00999   /*
01000    * Change the size of the exist hash table to min. size 
01001    */
01002   for (bddIndex = fIndex; bddIndex < bddManager->numVars; bddIndex++){
01003     bddId = bddManager->indexToId[bddIndex];
01004     existHashTableArray[bddId]->sizeIndex =
01005         DEFAULT_EXIST_HASH_TABLE_SIZE_INDEX;  
01006     existHashTableArray[bddId]->numBins = DEFAULT_EXIST_HASH_TABLE_SIZE;
01007     Cal_MemFree(existHashTableArray[bddId]->bins);
01008     existHashTableArray[bddId]->bins = Cal_MemAlloc(CalBddNode_t*,
01009                                              DEFAULT_EXIST_HASH_TABLE_SIZE);
01010     memset((char *)existHashTableArray[bddId]->bins, 0,
01011            existHashTableArray[bddId]->numBins*sizeof(CalBddNode_t*));
01012   }
01013   
01014   CalHashTableFindOrAdd(existHashTableArray[fId], f, bddManager->bddOne,
01015                         &result);  
01016 
01017 
01018   BddExistsBFAux(bddManager, fIndex, existHashTableArray, orHashTableArray,
01019                  CalOpExists, opCode, association);  
01020 
01021   CalRequestIsForwardedTo(result);
01022   
01023   CalCacheTableTwoFixResultPointers(bddManager);
01024   CalCacheTableOneInsert(bddManager, f, result, opCode, 0);
01025   for (bddIndex = fIndex; bddIndex < bddManager->numVars; bddIndex++){
01026     bddId = bddManager->indexToId[bddIndex];
01027     CalHashTableCleanUp(existHashTableArray[bddId]);
01028     CalHashTableCleanUp(orHashTableArray[bddId]);
01029   }
01030   return result;
01031 }

static void BddExistsReduce ( Cal_BddManager_t *  bddManager,
CalHashTable_t *  existHashTable,
CalHashTable_t **  existHashTableArray,
CalHashTable_t **  orHashTableArray,
unsigned short  opCode,
CalAssociation_t *  association 
) [static]

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 809 of file calQuant.c.

00813 {
00814   int i, numBins = existHashTable->numBins;
00815   CalBddNode_t **bins = existHashTable->bins;
00816   CalRequestNode_t *requestNode, *next, *requestNodeListAux;
00817   CalBddNode_t *endNode;
00818   
00819   int bddIndex;
00820   /*Cal_BddIndex_t minIndex, elseIndex;*/
00821   int minIndex, elseIndex;
00822   Cal_BddId_t bddId, minId;
00823   Cal_Bdd_t thenBdd, elseBdd, result, orResult;
00824   Cal_BddRefCount_t refCount;
00825   int lastBddIndex = association->lastBddIndex; 
00826   
00827 
00828   /* For those nodes which get processed in the first pass */
00829   /* requestNodeList = existHashTable->requestNodeList; */
00830   endNode = existHashTable->endNode;
00831 
00832   /* For the other ones. This list is merged with the requestNodeList
00833    * after processing is complete.
00834    */
00835   requestNodeListAux = Cal_Nil(CalRequestNode_t);
00836   existHashTable->numEntries = 0;
00837   
00838   minIndex = bddManager->numVars;
00839   
00840   for(i = 0; i < numBins; i++){
00841     for(requestNode = bins[i], bins[i] = Cal_Nil(CalRequestNode_t);
00842         requestNode != Cal_Nil(CalRequestNode_t);
00843         requestNode = next){
00844       next = CalRequestNodeGetNextRequestNode(requestNode);
00845       /* Process the requestNode */
00846       CalRequestNodeGetThenRequest(requestNode, thenBdd);
00847       CalRequestNodeGetElseRequest(requestNode, elseBdd);
00848       CalRequestIsForwardedTo(thenBdd);
00849       CalRequestNodePutThenRequest(requestNode, thenBdd);
00850       if (CalBddIsBddOne(bddManager, thenBdd)){
00851         CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
00852         /*
00853         ** CalRequestNodePutNextRequestNode(requestNode, requestNodeList);
00854         ** requestNodeList = requestNode;
00855         */
00856         /*CalRequestNodePutNextRequestNode(endNode, requestNode);*/
00857         endNode->nextBddNode = requestNode;
00858         endNode = requestNode;
00859         continue;
00860       }
00861       
00862       CalRequestNodePutNextRequestNode(requestNode, requestNodeListAux);
00863       requestNodeListAux = requestNode;
00864 
00865       /*if(CalOpExists(bddManager, elseBdd, &result) == 0){*/
00866       if (((int)bddManager->idToIndex[CalBddGetBddId(elseBdd)]) <= lastBddIndex){
00867         if (CalCacheTableOneLookup(bddManager, elseBdd, opCode,
00868                                    &result)){  
00869           CalRequestIsForwardedTo(result);
00870         }
00871         else{
00872           CalHashTableFindOrAdd(existHashTableArray[CalBddGetBddId(elseBdd)], elseBdd,
00873                                 bddManager->bddOne, &result);
00874           CalCacheTableOneInsert(bddManager, elseBdd, result,
00875                                  opCode, 1);
00876           if (minIndex > (elseIndex = CalBddGetBddIndex(bddManager,
00877                                                         elseBdd))){ 
00878             minIndex = elseIndex;
00879           }
00880         }
00881       }
00882       else{
00883         result = elseBdd;
00884       }
00885       CalRequestNodePutElseRequest(requestNode, result);
00886     }
00887   }
00888   
00889   if (!requestNodeListAux){
00890     /* requestNodeList = requestNodeList; */
00891     existHashTable->endNode = endNode;
00892     return;
00893   }
00894   
00895   BddExistsBFAux(bddManager, minIndex, existHashTableArray,
00896                  orHashTableArray,  CalOpExists, opCode, association); 
00897   minIndex = bddManager->numVars;
00898   for (requestNode = requestNodeListAux; requestNode; requestNode = next){
00899     Cal_Bdd_t thenResult, elseResult;
00900     Cal_BddIndex_t orResultIndex;
00901     
00902     next = CalRequestNodeGetNextRequestNode(requestNode);
00903     CalRequestNodeGetThenRequest(requestNode, thenResult);
00904     CalRequestNodeGetElseRequest(requestNode, elseResult);
00905     CalRequestIsForwardedTo(elseResult);
00906     if (CalOpOr(bddManager, thenResult, elseResult, &orResult) == 0){
00907       CalBddNormalize(thenResult, elseResult);
00908       CalBddNot(thenResult, thenResult);
00909       CalBddNot(elseResult, elseResult);
00910       if (CalCacheTableTwoLookup(bddManager, thenResult,elseResult,
00911                                  CAL_OP_NAND, &orResult)){
00912         CalRequestIsForwardedTo(orResult);
00913       }
00914       else {
00915         CalBddGetMinIdAndMinIndex(bddManager, thenResult, elseResult,
00916                                   minId, orResultIndex);
00917         CalHashTableFindOrAdd(orHashTableArray[minId], thenResult, elseResult,
00918                               &orResult);
00919         CalCacheTableTwoInsert(bddManager, thenResult, elseResult, orResult,
00920                                CAL_OP_NAND, 1);
00921         if (minIndex > orResultIndex) minIndex = orResultIndex;
00922       }
00923     }
00924     CalRequestNodePutThenRequest(requestNode, orResult);
00925   }
00926   
00927 
00928   /* Call "OR" apply and reduce */
00929   for (bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
00930     bddId = bddManager->indexToId[bddIndex];
00931     if(orHashTableArray[bddId]->numEntries){
00932       HashTableApply(bddManager, orHashTableArray[bddId], orHashTableArray,
00933                      CalOpNand, CAL_OP_NAND);
00934     }
00935   }
00936   
00937   for(bddIndex = bddManager->numVars - 1; bddIndex >= minIndex; bddIndex--){
00938     CalHashTable_t *uniqueTableForId;
00939     bddId = bddManager->indexToId[bddIndex];
00940     uniqueTableForId = bddManager->uniqueTable[bddId];
00941     if(orHashTableArray[bddId]->numEntries){
00942       HashTableReduce(bddManager, orHashTableArray[bddId], uniqueTableForId);
00943     }
00944   }
00945   
00946   for (requestNode = requestNodeListAux; requestNode; requestNode = next){
00947     next = CalRequestNodeGetNextRequestNode(requestNode);
00948     CalRequestNodeGetThenRequest(requestNode, result);
00949     CalRequestIsForwardedTo(result);
00950     CalBddNodeGetRefCount(requestNode, refCount);
00951     CalBddAddRefCount(result, refCount);
00952     CalRequestNodePutThenRequest(requestNode, result);
00953     CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
00954     /*
00955     ** CalRequestNodePutNextRequestNode(requestNode, requestNodeList);
00956     ** requestNodeList = requestNode;
00957     */
00958     /*CalRequestNodePutNextRequestNode(endNode, requestNode);*/
00959     endNode->nextBddNode = requestNode;
00960     endNode = requestNode;
00961   }
00962   /*existHashTable->requestNodeList = requestNodeList;*/
00963   existHashTable->endNode = endNode;
00964   
00965 }

static Cal_Bdd_t BddExistsStep ( Cal_BddManager_t *  bddManager,
Cal_Bdd_t  f,
unsigned short  opCode,
CalAssociation_t *  association 
) [static]

AutomaticStart

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 314 of file calQuant.c.

00316 {
00317   Cal_Bdd_t temp1, temp2;
00318   Cal_Bdd_t f1, f2;
00319   Cal_Bdd_t result;
00320   Cal_BddId_t topId;
00321   int quantifying;
00322   
00323   if (((int)CalBddGetBddIndex(bddManager, f)) > association->lastBddIndex){
00324     return f;
00325   }
00326   if (CalCacheTableOneLookup(bddManager, f, opCode, &result)){
00327     return result;
00328   }
00329 
00330   topId = CalBddGetBddId(f);
00331   quantifying = (CalBddIsBddNull(bddManager,
00332                                  association->varAssociation[topId]) ? 0 : 1);
00333   CalBddGetCofactors(f, topId, f1, f2);
00334   temp1 = BddExistsStep(bddManager, f1, opCode, association);
00335   if (quantifying && CalBddIsEqual(temp1, bddManager->bddOne)){
00336     result=temp1;
00337   }
00338   else {
00339     temp2 = BddExistsStep(bddManager, f2, opCode, association);
00340     if (quantifying){
00341       CalBddNot(temp1, temp1);
00342       CalBddNot(temp2, temp2);
00343           result = BddDFStep(bddManager, temp1, temp2, CalOpNand, CAL_OP_NAND);
00344         }
00345     else {
00346       Cal_BddId_t id = CalBddGetBddId(f);
00347       if (CalUniqueTableForIdFindOrAdd(bddManager, bddManager->uniqueTable[id],
00348                                        temp1, temp2, &result) == 0){
00349         CalBddIcrRefCount(temp1);
00350         CalBddIcrRefCount(temp2);
00351       }
00352     }
00353   } 
00354   CalCacheTableOneInsert(bddManager, f, result, opCode, 0);
00355   return (result);
00356 }

static void BddRelProdApply ( Cal_BddManager_t *  bddManager,
int  quantifying,
CalHashTable_t *  relProdHashTable,
CalHashTable_t **  relProdHashTableArray,
CalHashTable_t **  andHashTableArray,
CalOpProc_t  calOpProc,
unsigned short  opCode,
CalAssociation_t *  assoc 
) [static]

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 1046 of file calQuant.c.

01050 {
01051   int i, numBins = relProdHashTable->numBins;
01052   CalBddNode_t **bins = relProdHashTable->bins;
01053   Cal_BddId_t minId;
01054   CalRequestNode_t *requestNode;
01055   Cal_Bdd_t fx, fxbar, gx, gxbar, result, resultBar;
01056   /*Cal_BddIndex_t minIndex;*/
01057   int minIndex;
01058   
01059   for(i = 0; i < numBins; i++){
01060     for(requestNode = bins[i];
01061         requestNode != Cal_Nil(CalRequestNode_t);
01062         requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
01063       CalRequestNodeGetCofactors(bddManager, requestNode, fx, fxbar, gx, gxbar);
01064       CalBddNormalize(fx, gx);
01065       CalBddGetMinIdAndMinIndex(bddManager, fx, gx, minId, minIndex);
01066       if (minIndex > assoc->lastBddIndex){
01067         if (CalOpAnd(bddManager, fx, gx, &result) == 0){
01068           if (CalCacheTableTwoLookup(bddManager, fx, gx, CAL_OP_NAND,
01069                                      &result)){  
01070             CalRequestIsForwardedTo(result);
01071           }
01072           else{
01073             CalHashTableFindOrAdd(andHashTableArray[minId], fx, gx, &result);
01074             CalCacheTableTwoInsert(bddManager, fx, gx, result,
01075                                    CAL_OP_NAND, 1);
01076           }
01077           CalBddNot(result, result);
01078         }
01079       }
01080       else {
01081         if(calOpProc(bddManager, fx, gx, &result) == 0){
01082           if (CalCacheTableTwoLookup(bddManager, fx, gx, opCode,
01083                                      &result)){      
01084             CalRequestIsForwardedTo(result);
01085           }
01086           else {
01087             CalHashTableFindOrAdd(relProdHashTableArray[minId], fx, gx,
01088                                   &result);   
01089             CalCacheTableTwoInsert(bddManager, fx, gx, result, opCode, 1); 
01090           }
01091         }
01092       }
01093       CalRequestNodePutThenRequest(requestNode, result);
01094       if (quantifying){
01095         Cal_Bdd_t elseRequest;
01096         Cal_BddId_t elseRequestId;
01097         CalBddNode_t *elseRequestNode;
01098         
01099         CalBddGetMinId2(bddManager, fxbar, gxbar, elseRequestId);
01100         CalNodeManagerInitBddNode(bddManager->nodeManagerArray[elseRequestId],
01101                                   fxbar, gxbar, Cal_Nil(CalBddNode_t),
01102                                   elseRequestNode);
01103         /*
01104           CalNodeManagerAllocNode(bddManager->nodeManagerArray[elseRequestId],
01105           elseRequestNode);  
01106           CalRequestNodePutF(elseRequestNode, fxbar);
01107           CalRequestNodePutG(elseRequestNode, gxbar);
01108         */
01109         CalRequestPutRequestId(elseRequest, elseRequestId);
01110         CalRequestPutRequestNode(elseRequest, elseRequestNode);
01111         CalRequestNodePutElseRequest(requestNode, elseRequest);
01112       }
01113       else {
01114         CalBddIcrRefCount(result);
01115         CalBddNormalize(fxbar, gxbar);
01116         CalBddGetMinIdAndMinIndex(bddManager, fxbar, gxbar, minId, minIndex);
01117         if (minIndex > assoc->lastBddIndex){
01118           if (CalOpAnd(bddManager, fxbar, gxbar, &resultBar) == 0){
01119             if( CalCacheTableTwoLookup(bddManager, fxbar, gxbar,
01120                                        CAL_OP_NAND, &resultBar)){  
01121               CalRequestIsForwardedTo(resultBar);
01122             }
01123             else{
01124               CalHashTableFindOrAdd(andHashTableArray[minId], fxbar, gxbar,
01125                                     &resultBar); 
01126               CalCacheTableTwoInsert(bddManager, fxbar, gxbar, resultBar,
01127                                      CAL_OP_NAND, 1); 
01128             }
01129             CalBddNot(resultBar, resultBar);
01130           }
01131         }
01132         else {
01133           if(calOpProc(bddManager, fxbar, gxbar, &resultBar) == 0){
01134             if (CalCacheTableTwoLookup(bddManager, fxbar, gxbar, opCode,
01135                                        &resultBar)){   
01136               CalRequestIsForwardedTo(resultBar);
01137             }
01138             else { 
01139               CalHashTableFindOrAdd(relProdHashTableArray[minId],
01140                                     fxbar, gxbar, &resultBar);
01141               CalCacheTableTwoInsert(bddManager, fxbar, gxbar,
01142                                      resultBar, opCode, 1); 
01143             }
01144           }
01145         }
01146         CalBddIcrRefCount(resultBar);
01147         CalRequestNodePutElseRequest(requestNode, resultBar);
01148       }
01149     }
01150   }
01151 }

static void BddRelProdBFAux ( Cal_BddManager_t *  bddManager,
int  minIndex,
CalHashTable_t **  relProdHashTableArray,
CalHashTable_t **  andHashTableArray,
CalHashTable_t **  orHashTableArray,
unsigned short  opCode,
CalAssociation_t *  assoc 
) [static]

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 1358 of file calQuant.c.

01363 {
01364   Cal_BddIndex_t bddIndex;
01365   int quantifying;
01366   int index;
01367   Cal_BddId_t bddId;
01368   CalHashTable_t *hashTable;
01369   
01370   for (bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
01371     bddId = bddManager->indexToId[bddIndex];
01372     hashTable = andHashTableArray[bddId];
01373     if(hashTable->numEntries){
01374       HashTableApply(bddManager, hashTable, andHashTableArray, CalOpNand,
01375                      CAL_OP_NAND); 
01376     }
01377     hashTable = relProdHashTableArray[bddId];
01378     if(hashTable->numEntries){
01379       quantifying = (CalBddIsBddNull(bddManager,
01380                                      assoc->varAssociation[bddId]) ? 0 : 1); 
01381       BddRelProdApply(bddManager, quantifying, hashTable,
01382                       relProdHashTableArray, andHashTableArray,
01383                       CalOpRelProd, opCode, assoc); 
01384     }
01385   }
01386 
01387   /* Reduce phase */
01388   for (index = bddManager->numVars-1; index >= minIndex; index--){
01389     CalHashTable_t *uniqueTableForId;
01390     bddId = bddManager->indexToId[index];
01391     uniqueTableForId = bddManager->uniqueTable[bddId];
01392     hashTable = andHashTableArray[bddId];
01393     if(hashTable->numEntries){
01394       HashTableReduce(bddManager, hashTable, uniqueTableForId);
01395     }
01396     if (relProdHashTableArray[bddId]->numEntries){
01397       quantifying = (CalBddIsBddNull(bddManager,
01398                                      assoc->varAssociation[bddId]) ? 0 : 1); 
01399       if (quantifying){
01400         BddRelProdReduce(bddManager, relProdHashTableArray[bddId],
01401                          relProdHashTableArray, andHashTableArray,
01402                          orHashTableArray, opCode, assoc); 
01403       }
01404       else {
01405         HashTableReduce(bddManager, relProdHashTableArray[bddId],
01406                         bddManager->uniqueTable[bddId]);
01407       }
01408     }
01409   }
01410 }

static Cal_Bdd_t BddRelProdBFPlusDF ( Cal_BddManager_t *  bddManager,
Cal_Bdd_t  f,
Cal_Bdd_t  g,
unsigned short  opCode,
CalAssociation_t *  association 
) [static]

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 1424 of file calQuant.c.

01427 {
01428   Cal_Bdd_t result;
01429   /*Cal_BddIndex_t minIndex;*/
01430   int  minIndex;
01431   int bddIndex;
01432   CalHashTable_t **andHashTableArray = bddManager->reqQue[3];
01433   CalHashTable_t **relProdHashTableArray = bddManager->reqQue[4];
01434   CalHashTable_t **orHashTableArray = bddManager->reqQue[5];
01435   Cal_BddId_t bddId, minId;
01436 
01437   if(CalOpRelProd(bddManager, f, g, &result) == 1){
01438     return result;
01439   }
01440   CalBddNormalize(f, g);
01441   if(CalCacheTableTwoLookup(bddManager, f, g, opCode, &result)){
01442     return result;
01443   }
01444 
01445   CalBddGetMinIdAndMinIndex(bddManager, f, g, minId, minIndex);
01446 
01447   /*
01448    * Change the size of the exist hash table to min. size 
01449    */
01450   for (bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
01451     bddId = bddManager->indexToId[bddIndex];
01452     relProdHashTableArray[bddId]->sizeIndex =
01453         DEFAULT_EXIST_HASH_TABLE_SIZE_INDEX;  
01454     relProdHashTableArray[bddId]->numBins = DEFAULT_EXIST_HASH_TABLE_SIZE;
01455     Cal_MemFree(relProdHashTableArray[bddId]->bins);
01456     relProdHashTableArray[bddId]->bins = Cal_MemAlloc(CalBddNode_t*,
01457                                              DEFAULT_EXIST_HASH_TABLE_SIZE);
01458     memset((char *)relProdHashTableArray[bddId]->bins, 0,
01459            relProdHashTableArray[bddId]->numBins*sizeof(CalBddNode_t*));
01460   }
01461 
01462   if (minIndex > association->lastBddIndex) {
01463     if (CalOpAnd(bddManager, f, g, &result) == 0){
01464       if (CalCacheTableTwoLookup(bddManager, f, g, CAL_OP_NAND, &result)
01465           == 0){
01466         CalHashTableFindOrAdd(andHashTableArray[minId], f, g, &result);
01467       }
01468       else{
01469         CalCacheTableTwoInsert(bddManager, f, g, result, CAL_OP_NAND,
01470                                1);
01471       }
01472       CalBddNot(result, result);
01473     }
01474   }
01475   else {
01476     CalHashTableFindOrAdd(relProdHashTableArray[minId], f, g, &result); 
01477   }
01478 
01479   BddRelProdBFAux(bddManager, minIndex, relProdHashTableArray,
01480                   andHashTableArray, orHashTableArray, opCode, association); 
01481   CalRequestIsForwardedTo(result);
01482   CalCacheTableTwoFixResultPointers(bddManager);
01483   CalCacheTableTwoInsert(bddManager, f, g, result, opCode, 0);
01484   for (bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
01485     bddId = bddManager->indexToId[bddIndex];
01486     CalHashTableCleanUp(relProdHashTableArray[bddId]);
01487     CalHashTableCleanUp(andHashTableArray[bddId]);
01488     CalHashTableCleanUp(orHashTableArray[bddId]);
01489   }
01490   return result;
01491 }

static void BddRelProdReduce ( Cal_BddManager_t *  bddManager,
CalHashTable_t *  relProdHashTable,
CalHashTable_t **  relProdHashTableArray,
CalHashTable_t **  andHashTableArray,
CalHashTable_t **  orHashTableArray,
unsigned short  opCode,
CalAssociation_t *  assoc 
) [static]

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 1164 of file calQuant.c.

01170 {
01171   int i, numBins = relProdHashTable->numBins;
01172   CalBddNode_t **bins = relProdHashTable->bins;
01173   CalRequestNode_t *requestNode, *next, *requestNodeListAux;
01174   CalBddNode_t  *elseRequestNode;
01175   int bddIndex;
01176   /*Cal_BddIndex_t minIndex;*/
01177   int minIndex;
01178   Cal_BddId_t bddId, minId, elseRequestId;
01179   Cal_Bdd_t thenBdd, elseBdd, result, orResult;
01180   Cal_BddRefCount_t refCount;
01181   Cal_Bdd_t fxbar, gxbar;
01182   CalBddNode_t *endNode;
01183   
01184 
01185   /* For those nodes which get processed in the first pass */
01186   /*requestNodeList = relProdHashTable->requestNodeList;*/
01187   endNode = relProdHashTable->endNode;
01188   
01189   /* For the other ones. This list is merged with the requestNodeList
01190    * after processing is complete.
01191    */
01192   requestNodeListAux = Cal_Nil(CalRequestNode_t);
01193   
01194   minIndex = bddManager->numVars;
01195   
01196   for(i = 0; i < numBins; i++){
01197     for(requestNode = bins[i], bins[i] = Cal_Nil(CalRequestNode_t);
01198         requestNode != Cal_Nil(CalRequestNode_t);
01199         requestNode = next){
01200       next = CalRequestNodeGetNextRequestNode(requestNode);
01201       /* Process the requestNode */
01202       CalRequestNodeGetThenRequest(requestNode, thenBdd);
01203       CalRequestIsForwardedTo(thenBdd);
01204       /*CalRequestNodePutThenRequest(requestNode, thenBdd);*/
01205       CalRequestNodeGetElseRequest(requestNode, elseBdd);
01206       CalRequestIsForwardedTo(elseBdd);
01207       CalRequestGetF(elseBdd, fxbar);
01208       CalRequestGetG(elseBdd, gxbar);
01209       
01210       /* Free the else request node because it is not needed */
01211       elseRequestNode = CalRequestNodeGetElseRequestNode(requestNode);
01212       elseRequestId = CalRequestNodeGetElseRequestId(requestNode);
01213       CalNodeManagerFreeNode(bddManager->nodeManagerArray[elseRequestId],
01214                              elseRequestNode);
01215       if (CalBddIsBddOne(bddManager, thenBdd)){
01216         CalRequestNodePutThenRequest(requestNode, bddManager->bddOne);
01217         CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
01218         /*
01219         ** CalRequestNodePutNextRequestNode(requestNode, requestNodeList);
01220         ** requestNodeList = requestNode;
01221         */
01222         /*CalRequestNodePutNextRequestNode(endNode, requestNode);*/
01223         endNode->nextBddNode = requestNode;
01224         endNode = requestNode;
01225         continue;
01226       }
01227       
01228       CalRequestNodePutNextRequestNode(requestNode, requestNodeListAux);
01229       requestNodeListAux = requestNode;
01230 
01231       CalBddGetMinIdAndMinIndex(bddManager, fxbar, gxbar, bddId, bddIndex);
01232       CalBddNormalize(fxbar, gxbar);
01233       if (bddIndex > assoc->lastBddIndex){
01234         if (CalOpAnd(bddManager, fxbar, gxbar, &result) == 0){
01235           if (CalCacheTableTwoLookup(bddManager, fxbar, gxbar,
01236                                      CAL_OP_NAND, &result)){
01237             CalRequestIsForwardedTo(result);
01238           }
01239           else {
01240             CalHashTableFindOrAdd(andHashTableArray[bddId], fxbar,
01241                                   gxbar, &result);
01242             CalCacheTableTwoInsert(bddManager, fxbar, gxbar, result,
01243                                    CAL_OP_NAND, 1);
01244             if (minIndex > bddIndex) minIndex = bddIndex;
01245           }
01246           CalBddNot(result, result);
01247         }
01248       }
01249       else {
01250         if(CalOpRelProd(bddManager, fxbar, gxbar, &result) == 0){
01251           if (CalCacheTableTwoLookup(bddManager, fxbar, gxbar, opCode,
01252                                      &result)){  
01253             CalRequestIsForwardedTo(result);
01254           }
01255           else {
01256             CalHashTableFindOrAdd(relProdHashTableArray[bddId], fxbar, gxbar, 
01257                                   &result);
01258             CalCacheTableTwoInsert(bddManager, fxbar, gxbar, result,
01259                                    opCode, 1); 
01260             if (minIndex > bddIndex) minIndex = bddIndex;
01261           }
01262         }
01263       }
01264       CalRequestNodePutElseRequest(requestNode, result);
01265     }
01266   }
01267 
01268   if (!requestNodeListAux){
01269     /*relProdHashTable->requestNodeList = requestNodeList;*/
01270     relProdHashTable->endNode = endNode;
01271     return;
01272   }
01273   
01274   BddRelProdBFAux(bddManager, minIndex, relProdHashTableArray,
01275                   andHashTableArray, orHashTableArray, opCode, assoc);
01276   
01277   minIndex = bddManager->numVars;
01278   for (requestNode = requestNodeListAux; requestNode; requestNode = next){
01279     Cal_Bdd_t thenResult, elseResult;
01280     Cal_BddIndex_t orResultIndex;
01281     
01282     next = CalRequestNodeGetNextRequestNode(requestNode);
01283     CalRequestNodeGetThenRequest(requestNode, thenResult);
01284     CalRequestNodeGetElseRequest(requestNode, elseResult);
01285     CalRequestIsForwardedTo(elseResult);
01286     CalRequestIsForwardedTo(thenResult);
01287     CalBddNormalize(thenResult, elseResult);
01288     if (CalOpOr(bddManager, thenResult, elseResult, &orResult) == 0){
01289       CalBddNot(thenResult, thenResult);
01290       CalBddNot(elseResult, elseResult);
01291       if (CalCacheTableTwoLookup(bddManager, thenResult, elseResult,
01292                                  CAL_OP_NAND, &orResult)){ 
01293         CalRequestIsForwardedTo(orResult);
01294       }
01295       else {
01296         CalBddGetMinIdAndMinIndex(bddManager, thenResult, elseResult,
01297                                   minId, orResultIndex);
01298         CalHashTableFindOrAdd(orHashTableArray[minId], thenResult, elseResult,
01299                               &orResult);
01300         CalCacheTableTwoInsert(bddManager, thenResult, elseResult, orResult,
01301                                  CAL_OP_NAND, 1); 
01302         if (minIndex > orResultIndex) minIndex = orResultIndex;
01303       }
01304     }
01305     CalRequestNodePutThenRequest(requestNode, orResult);
01306   }
01307 
01308   /* Call "OR" apply and reduce */
01309   for (bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
01310     bddId = bddManager->indexToId[bddIndex];
01311     if(orHashTableArray[bddId]->numEntries){
01312         HashTableApply(bddManager, orHashTableArray[bddId], orHashTableArray,
01313                        CalOpNand, CAL_OP_NAND); 
01314     }
01315   }
01316   
01317   for(bddIndex = bddManager->numVars - 1; bddIndex >= minIndex; bddIndex--){
01318     CalHashTable_t *uniqueTableForId;
01319     bddId = bddManager->indexToId[bddIndex];
01320     uniqueTableForId = bddManager->uniqueTable[bddId];
01321     if(orHashTableArray[bddId]->numEntries){
01322       HashTableReduce(bddManager, orHashTableArray[bddId], uniqueTableForId);
01323     }
01324   }
01325   for (requestNode = requestNodeListAux; requestNode; requestNode = next){
01326     next = CalRequestNodeGetNextRequestNode(requestNode);
01327     CalRequestNodeGetThenRequest(requestNode, result);
01328     CalRequestIsForwardedTo(result);
01329     CalBddNodeGetRefCount(requestNode, refCount);
01330     CalBddAddRefCount(result, refCount);
01331     CalRequestNodePutThenRequest(requestNode, result);
01332     CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
01333     /*
01334     ** CalRequestNodePutNextRequestNode(requestNode, requestNodeList);
01335     ** requestNodeList = requestNode;
01336     */
01337     /*CalRequestNodePutNextRequestNode(endNode, requestNode);*/
01338     endNode->nextBddNode = requestNode;
01339     endNode = requestNode;
01340   }
01341 
01342   /*relProdHashTable->requestNodeList = requestNodeList;*/
01343   relProdHashTable->endNode = endNode;
01344 }

static Cal_Bdd_t BddRelProdStep ( Cal_BddManager_t *  bddManager,
Cal_Bdd_t  f,
Cal_Bdd_t  g,
unsigned short  opCode,
CalAssociation_t *  assoc 
) [static]

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 370 of file calQuant.c.

00372 {
00373   Cal_BddId_t topId;
00374   Cal_Bdd_t f1, f2, g1, g2;
00375   Cal_Bdd_t temp1, temp2;
00376   Cal_Bdd_t  result;
00377   int quantifying;
00378 
00379   if (CalBddIsBddConst(f) || CalBddIsBddConst(g)){
00380     if (CalBddIsBddZero(bddManager, f) || CalBddIsBddZero(bddManager, g)){
00381       return bddManager->bddZero;
00382     }
00383     if (assoc->id != -1){
00384       opCode = CAL_OP_QUANT+assoc->id;
00385     }
00386     else{
00387       opCode--;
00388     }
00389     if (CalBddIsBddOne(bddManager, f)){
00390       return (BddExistsStep(bddManager, g, opCode, assoc));
00391     }
00392     return (BddExistsStep(bddManager, f, opCode, assoc));
00393   }
00394   if ((((int)CalBddGetBddIndex(bddManager, f)) > assoc->lastBddIndex) &&
00395       (((int)CalBddGetBddIndex(bddManager, g)) > assoc->lastBddIndex)){
00396     result = BddDFStep(bddManager, f, g, CalOpNand, CAL_OP_NAND);
00397     CalBddNot(result, result);
00398     return result;
00399   }
00400   if(CalOpRelProd(bddManager, f, g, &result) == 1){
00401     return result;
00402   }
00403   CalBddNormalize(f, g);
00404   if(CalCacheTableTwoLookup(bddManager, f, g, opCode, &result)){
00405     return result;
00406   }
00407   CalBddGetMinId2(bddManager, f, g, topId);
00408   
00409   quantifying = (CalBddIsBddNull(bddManager, assoc->varAssociation[topId]) ? 0
00410                  : 1);
00411   CalBddGetCofactors(f, topId, f1, f2);
00412   CalBddGetCofactors(g, topId, g1, g2);
00413 
00414   temp1 = BddRelProdStep(bddManager, f1, g1, opCode, assoc);
00415   if (quantifying && CalBddIsBddOne(bddManager, temp1)){
00416     result=temp1;
00417   }
00418   else {
00419     temp2 = BddRelProdStep(bddManager, f2, g2, opCode, assoc);
00420     if (quantifying) {
00421       CalBddNot(temp1, temp1);
00422       CalBddNot(temp2, temp2);
00423           result = BddDFStep(bddManager, temp1, temp2, CalOpNand, CAL_OP_NAND);
00424           /*result = BddDFStep(bddManager, temp1, temp2, CalOpOr, CAL_OP_OR);*/
00425         }
00426     else {
00427       if (CalUniqueTableForIdFindOrAdd(bddManager,
00428                                        bddManager->uniqueTable[topId],
00429                                        temp1, temp2, &result) == 0){
00430         CalBddIcrRefCount(temp1);
00431         CalBddIcrRefCount(temp2);
00432       }
00433     }
00434   }
00435   CalCacheTableTwoInsert(bddManager, f, g, result, opCode, 0);
00436   return (result);
00437 }

Cal_Bdd Cal_BddExists ( Cal_BddManager  bddManager,
Cal_Bdd  fUserBdd 
)

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

Synopsis [Returns the result of existentially quantifying some variables from the given BDD.]

Description [Returns the BDD for f with all the variables that are paired with something in the current variable association existentially quantified out.]

SideEffects [None.]

SeeAlso [Cal_BddRelProd]

Definition at line 110 of file calQuant.c.

00111 {
00112   Cal_Bdd_t result;
00113   Cal_Bdd userResult;
00114 
00115   if (CalBddPreProcessing(bddManager, 1, fUserBdd)){
00116     Cal_Bdd_t f = CalBddGetInternalBdd(bddManager, fUserBdd);
00117     CalAssociation_t *assoc = bddManager->currentAssociation;
00118     unsigned short opCode;
00119     
00120     if (assoc->id == -1){
00121       opCode = bddManager->tempOpCode--;
00122     }
00123     else {
00124       opCode = CAL_OP_QUANT + assoc->id;
00125     }
00126     if (bddManager->numNodes <= CAL_LARGE_BDD){
00127       /* If number of nodes is small, call depth first routine. */
00128       result = BddExistsStep(bddManager, f, opCode, assoc);
00129     }
00130     else {
00131       result = BddExistsBFPlusDF(bddManager, f, opCode, assoc);
00132     }
00133     userResult =  CalBddGetExternalBdd(bddManager, result);
00134     if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){
00135       Cal_BddFree(bddManager, userResult);
00136       Cal_BddManagerGC(bddManager);
00137       return (Cal_Bdd) 0;
00138     }
00139     return userResult;
00140   }
00141   return (Cal_Bdd) 0;
00142 }

Cal_Bdd Cal_BddForAll ( Cal_BddManager  bddManager,
Cal_Bdd  fUserBdd 
)

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

Synopsis [Returns the result of universally quantifying some variables from the given BDD.]

Description [Returns the BDD for f with all the variables that are paired with something in the current variable association universally quantified out.]

SideEffects [None.]

Definition at line 208 of file calQuant.c.

00209 {
00210   Cal_Bdd_t result;
00211   Cal_Bdd userResult;
00212 
00213   if (CalBddPreProcessing(bddManager, 1, fUserBdd)){
00214     Cal_Bdd_t f = CalBddGetInternalBdd(bddManager, fUserBdd);
00215     CalAssociation_t *assoc = bddManager->currentAssociation;
00216     unsigned short opCode;
00217 
00218     CalBddNot(f, f);
00219     if (assoc->id == -1){
00220       opCode = bddManager->tempOpCode--;
00221     }
00222     else {
00223       opCode = CAL_OP_QUANT + assoc->id;
00224     }
00225     if (bddManager->numNodes <= CAL_LARGE_BDD){
00226       /* If number of nodes is small, call depth first routine. */
00227       result = BddExistsStep(bddManager, f, opCode, assoc);
00228     }
00229     else {
00230       result = BddExistsBFPlusDF(bddManager, f, opCode, assoc);
00231     }
00232     CalBddNot(result, result);
00233     userResult =  CalBddGetExternalBdd(bddManager, result);
00234     if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){
00235       Cal_BddFree(bddManager, userResult);
00236       Cal_BddManagerGC(bddManager);
00237       return (Cal_Bdd) 0;
00238     }
00239     return userResult;
00240   }
00241   return (Cal_Bdd) 0;
00242 }

Cal_Bdd Cal_BddRelProd ( Cal_BddManager  bddManager,
Cal_Bdd  fUserBdd,
Cal_Bdd  gUserBdd 
)

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

Synopsis [Returns the result of taking the logical AND of the argument BDDs and existentially quantifying some variables from the product.]

Description [Returns the BDD for the logical AND of f and g with all the variables that are paired with something in the current variable association existentially quantified out.]

SideEffects [None.]

Definition at line 159 of file calQuant.c.

00160 {
00161   Cal_Bdd_t result;
00162   Cal_Bdd userResult;
00163   
00164   if (CalBddPreProcessing(bddManager, 2, fUserBdd, gUserBdd)){
00165     Cal_Bdd_t f = CalBddGetInternalBdd(bddManager, fUserBdd);
00166     Cal_Bdd_t g = CalBddGetInternalBdd(bddManager, gUserBdd);
00167     CalAssociation_t *assoc = bddManager->currentAssociation;
00168     unsigned short opCode;
00169     
00170     if (bddManager->currentAssociation->id == -1){
00171       opCode = bddManager->tempOpCode--;
00172       bddManager->tempOpCode--;
00173     }
00174     else {
00175       opCode = CAL_OP_REL_PROD + assoc->id;
00176     }
00177     if (bddManager->numNodes <= CAL_LARGE_BDD){
00178       /* If number of nodes is small, call depth first routine. */
00179       result = BddRelProdStep(bddManager, f, g, opCode, assoc);
00180     }
00181     else {
00182       result = BddRelProdBFPlusDF(bddManager, f, g, opCode, assoc);
00183     }
00184     userResult =  CalBddGetExternalBdd(bddManager, result);
00185     if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){
00186       Cal_BddFree(bddManager, userResult);
00187       Cal_BddManagerGC(bddManager);
00188       return (Cal_Bdd) 0;
00189     }
00190     return userResult;
00191   }
00192   return (Cal_Bdd) 0;
00193 }

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

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 260 of file calQuant.c.

00262 {
00263   if (((int)bddManager->idToIndex[CalBddGetBddId(f)]) >
00264       bddManager->currentAssociation->lastBddIndex){ 
00265     *resultBddPtr = f;
00266     return 1;
00267   }
00268   return 0;
00269 }

int CalOpRelProd ( Cal_BddManager_t *  bddManager,
Cal_Bdd_t  f,
Cal_Bdd_t  g,
Cal_Bdd_t *  resultBddPtr 
)

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 284 of file calQuant.c.

00286 {
00287   if (CalBddIsBddZero(bddManager, f) || CalBddIsBddZero(bddManager, g) ||
00288       CalBddIsComplementEqual(f, g)){
00289     *resultBddPtr = bddManager->bddZero;
00290     return 1;
00291   }
00292   else if (CalBddIsBddOne(bddManager, f) && CalBddIsBddOne(bddManager, g)){
00293     *resultBddPtr = bddManager->bddOne;
00294     return 1;
00295   }
00296   return 0;
00297 }

static void HashTableApply ( Cal_BddManager_t *  bddManager,
CalHashTable_t *  hashTable,
CalHashTable_t **  reqQueAtPipeDepth,
CalOpProc_t  calOpProc,
unsigned long  opCode 
) [static]

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 492 of file calQuant.c.

00495 {
00496   int i, numBins = hashTable->numBins;
00497   CalBddNode_t **bins = hashTable->bins;
00498   CalRequestNode_t *requestNode;
00499   Cal_Bdd_t fx, gx, fxbar, gxbar, result;
00500   Cal_BddId_t bddId;
00501   
00502   for(i = 0; i < numBins; i++){
00503     for(requestNode = bins[i];
00504         requestNode != Cal_Nil(CalRequestNode_t);
00505         requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
00506       CalRequestNodeGetCofactors(bddManager, requestNode, fx, fxbar, gx, gxbar);
00507       CalBddNormalize(fx, gx);
00508       if((*calOpProc)(bddManager, fx, gx, &result) == 0){
00509         if (CalCacheTableTwoLookup(bddManager, fx, gx, opCode, &result) == 0){
00510           CalBddGetMinId2(bddManager, fx, gx, bddId);
00511           CalHashTableFindOrAdd(reqQueAtPipeDepth[bddId], fx, gx, &result);
00512           CalCacheTableTwoInsert(bddManager, fx, gx, result, opCode, 1);
00513         }
00514         else {
00515           CalRequestIsForwardedTo(result);
00516         }
00517       }
00518       CalBddIcrRefCount(result);
00519       CalRequestNodePutThenRequest(requestNode, result);
00520       CalBddNormalize(fxbar, gxbar);
00521       if((*calOpProc)(bddManager, fxbar, gxbar, &result) == 0){
00522         if (CalCacheTableTwoLookup(bddManager, fxbar, gxbar, opCode, &result)
00523             == 0){ 
00524           CalBddGetMinId2(bddManager, fxbar, gxbar, bddId);
00525           CalHashTableFindOrAdd(reqQueAtPipeDepth[bddId], fxbar, gxbar,
00526                                 &result); 
00527           CalCacheTableTwoInsert(bddManager, fxbar, gxbar, result,
00528                                  opCode, 1);
00529         }
00530         else {
00531           CalRequestIsForwardedTo(result);
00532         }
00533       }
00534       CalBddIcrRefCount(result);
00535       CalRequestNodePutElseRequest(requestNode, result);
00536     }
00537   }
00538 }

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

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 552 of file calQuant.c.

00554 {
00555   int i, numBins = hashTable->numBins;
00556   CalBddNode_t **bins = hashTable->bins;
00557   Cal_BddId_t currentBddId = uniqueTableForId->bddId;
00558   CalNodeManager_t *nodeManager = uniqueTableForId->nodeManager;
00559   CalRequestNode_t *requestNode, *next;
00560   CalBddNode_t *bddNode, *endNode;
00561   Cal_Bdd_t thenBdd, elseBdd, result;
00562   Cal_BddRefCount_t refCount;
00563 
00564   /*requestNodeList = hashTable->requestNodeList;*/
00565   endNode = hashTable->endNode;
00566   hashTable->numEntries = 0;
00567   for(i = 0; i < numBins; i++){
00568     for(requestNode = bins[i], bins[i] = Cal_Nil(CalRequestNode_t);
00569         requestNode != Cal_Nil(CalRequestNode_t);
00570         requestNode = next){
00571       next = CalRequestNodeGetNextRequestNode(requestNode);
00572       /* Process the requestNode */
00573       CalRequestNodeGetThenRequest(requestNode, thenBdd);
00574       CalRequestNodeGetElseRequest(requestNode, elseBdd);
00575       CalRequestIsForwardedTo(thenBdd);
00576       CalRequestIsForwardedTo(elseBdd);
00577       if(CalBddIsEqual(thenBdd, elseBdd)){
00578         CalBddNodeGetRefCount(requestNode, refCount);
00579         CalBddAddRefCount(thenBdd, refCount - 2);
00580         CalRequestNodePutThenRequest(requestNode, thenBdd);
00581         CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
00582         /*
00583         ** CalRequestNodePutNextRequestNode(requestNode, requestNodeList);
00584         ** requestNodeList = requestNode;
00585         */
00586         /*CalRequestNodePutNextRequestNode(endNode, requestNode);*/
00587         endNode->nextBddNode = requestNode;
00588         endNode = requestNode;
00589       }
00590       else if(CalUniqueTableForIdLookup(bddManager, uniqueTableForId,
00591           thenBdd, elseBdd, &result) == 1){
00592         CalBddDcrRefCount(thenBdd);
00593         CalBddDcrRefCount(elseBdd);
00594         CalBddNodeGetRefCount(requestNode, refCount);
00595         CalBddAddRefCount(result, refCount);
00596         CalRequestNodePutThenRequest(requestNode, result);
00597         CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
00598         /*
00599         ** CalRequestNodePutNextRequestNode(requestNode, requestNodeList);
00600         ** requestNodeList = requestNode;
00601         */
00602         /*CalRequestNodePutNextRequestNode(endNode, requestNode);*/
00603         endNode->nextBddNode = requestNode;
00604         endNode = requestNode;
00605       }
00606       else if(CalBddIsOutPos(thenBdd)){
00607         CalRequestNodePutThenRequest(requestNode, thenBdd);
00608         CalRequestNodePutElseRequest(requestNode, elseBdd);
00609         CalHashTableAddDirect(uniqueTableForId, requestNode);
00610         bddManager->numNodes++;
00611         bddManager->gcCheck--;
00612       }
00613       else{
00614         CalNodeManagerAllocNode(nodeManager, bddNode);
00615         CalBddNodePutThenBddId(bddNode, CalBddGetBddId(thenBdd));
00616         CalBddNodePutThenBddNode(bddNode, CalBddGetBddNodeNot(thenBdd));
00617         CalBddNodePutElseBddId(bddNode, CalBddGetBddId(elseBdd));
00618         CalBddNodePutElseBddNode(bddNode, CalBddGetBddNodeNot(elseBdd));
00619         /*
00620         CalNodeManagerInitBddNode(nodeManager, thenBdd, elseBdd,
00621                                Cal_Nil(CalBddNode_t), bddNode); 
00622                                */
00623         CalBddNodeGetRefCount(requestNode, refCount);
00624         CalBddNodePutRefCount(bddNode, refCount);
00625         CalHashTableAddDirect(uniqueTableForId, bddNode);
00626         bddManager->numNodes++;
00627         bddManager->gcCheck--;
00628         CalRequestNodePutThenRequestId(requestNode, currentBddId);
00629         CalRequestNodePutThenRequestNode(requestNode, CalBddNodeNot(bddNode));
00630         CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
00631         /*
00632         ** CalRequestNodePutNextRequestNode(requestNode, requestNodeList);
00633         ** requestNodeList = requestNode;
00634         */
00635         /*CalRequestNodePutNextRequestNode(endNode, requestNode);*/
00636         endNode->nextBddNode = requestNode;
00637         endNode = requestNode;
00638       }
00639     }
00640   }
00641   /* hashTable->requestNodeList = requestNodeList; */
00642   hashTable->endNode = endNode;
00643 }

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