src/calBdd/calBddOp.c File Reference

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

Go to the source code of this file.

Functions

static Cal_Bdd_t * BddArrayOpBF (Cal_BddManager_t *bddManager, Cal_Bdd_t *bddArray, int numFunction, CalOpProc_t calOpProc)
static Cal_Bdd_t BddMultiwayOp (Cal_BddManager_t *bddManager, Cal_Bdd_t *calBddArray, int numBdds, CalOpProc_t op)
static void BddArrayToRequestNodeListArray (Cal_BddManager_t *bddManager, Cal_Bdd_t *calBddArray, int numBdds)
static int CeilLog2 (int number)
Cal_Bdd Cal_BddAnd (Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd)
Cal_Bdd Cal_BddNand (Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd)
Cal_Bdd Cal_BddOr (Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd)
Cal_Bdd Cal_BddNor (Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd)
Cal_Bdd Cal_BddXor (Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd)
Cal_Bdd Cal_BddXnor (Cal_BddManager bddManager, Cal_Bdd fUserBdd, Cal_Bdd gUserBdd)
Cal_Bdd * Cal_BddPairwiseAnd (Cal_BddManager bddManager, Cal_Bdd *userBddArray)
Cal_Bdd * Cal_BddPairwiseOr (Cal_BddManager bddManager, Cal_Bdd *userBddArray)
Cal_Bdd * Cal_BddPairwiseXor (Cal_BddManager bddManager, Cal_Bdd *userBddArray)
Cal_Bdd Cal_BddMultiwayAnd (Cal_BddManager bddManager, Cal_Bdd *userBddArray)
Cal_Bdd Cal_BddMultiwayOr (Cal_BddManager bddManager, Cal_Bdd *userBddArray)
Cal_Bdd Cal_BddMultiwayXor (Cal_BddManager bddManager, Cal_Bdd *userBddArray)
void CalRequestNodeListArrayOp (Cal_BddManager_t *bddManager, CalRequestNode_t **requestNodeListArray, CalOpProc_t calOpProc)
Cal_Bdd_t CalBddOpBF (Cal_BddManager_t *bddManager, CalOpProc_t calOpProc, Cal_Bdd_t F, Cal_Bdd_t G)

Function Documentation

static Cal_Bdd_t * BddArrayOpBF ( Cal_BddManager_t *  bddManager,
Cal_Bdd_t *  bddArray,
int  numFunction,
CalOpProc_t  calOpProc 
) [static]

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

FileName [calBddOp.c]

PackageName [cal]

Synopsis [Routines for performing simple boolean operations on a pair of BDDs or on an array of pair of BDDs or on an array of BDDs.]

Description [The "cal" specific routines are "Cal_BddPairwiseAnd/Or", "Cal_BddMultiwayAnd/Or".]

SeeAlso [optional]

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

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

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

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

Revision [

Id
calBddOp.c,v 1.1.1.3 1998/05/04 00:58:52 hsv Exp

]AutomaticStart

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

Synopsis [Internal common routine for Cal_BddPairwiseAnd and Cal_BddPairwiseOr]

SideEffects [None]

Definition at line 799 of file calBddOp.c.

00801 {
00802   Cal_BddId_t minId, bddId;
00803   /*Cal_BddIndex_t minIndex = 0;*/
00804   int minIndex = 0;
00805   int bddIndex;
00806   CalHashTable_t *hashTable, **hashTableArray, *uniqueTableForId;
00807   Cal_Bdd_t F, G, result;
00808   int numPairs = numFunction/2;
00809   Cal_Bdd_t *resultArray = Cal_MemAlloc(Cal_Bdd_t, numPairs);
00810   int i;
00811   
00812   hashTableArray = bddManager->reqQue[0];
00813   for (i=0; i<numPairs; i++){
00814     F = bddArray[i<<1];
00815     G = bddArray[(i<<1)+1];
00816     if ((*calOpProc)(bddManager, F, G, &result) == 0){
00817       CalBddGetMinIdAndMinIndex(bddManager, F, G, minId, minIndex);
00818       CalHashTableFindOrAdd(hashTableArray[minId], F, G, &result);
00819     }
00820     resultArray[i] = result;
00821   }
00822   
00823   
00824   /* ReqQueApply */
00825   for(bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
00826     bddId = bddManager->indexToId[bddIndex];
00827     hashTable = hashTableArray[bddId];
00828     if(hashTable->numEntries){
00829       CalHashTableApply(bddManager, hashTable, hashTableArray, calOpProc);
00830     }
00831   }
00832 
00833   /* ReqQueReduce */
00834   for(bddIndex = bddManager->numVars - 1; bddIndex >= minIndex; bddIndex--){
00835     bddId = bddManager->indexToId[bddIndex];
00836     uniqueTableForId = bddManager->uniqueTable[bddId];
00837     hashTable = hashTableArray[bddId];
00838     if(hashTable->numEntries){
00839       CalHashTableReduce(bddManager, hashTable, uniqueTableForId);
00840     }
00841   }
00842   for (i=0; i<numPairs; i++){
00843     CalRequestIsForwardedTo(resultArray[i]);
00844   }
00845   /* Clean up */
00846   for(bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
00847     bddId = bddManager->indexToId[bddIndex];
00848     CalHashTableCleanUp(hashTableArray[bddId]);
00849   }
00850   return resultArray;
00851 }

static void BddArrayToRequestNodeListArray ( Cal_BddManager_t *  bddManager,
Cal_Bdd_t *  calBddArray,
int  numBdds 
) [static]

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

Synopsis [Converts an array of BDDs to a list of requests representing BDD pairs]

Description [Converts an array of BDDs to a list of requests representing BDD]

SideEffects [None]

Definition at line 904 of file calBddOp.c.

00908 {
00909   int i;
00910   Cal_Bdd_t lastBdd;
00911   CalRequestNode_t *even, *odd, *requestNode, *requestNodeList, *head;
00912   
00913   bddManager->depth = CeilLog2(numBdds);
00914   if (bddManager->depth > 10){
00915     CalBddFatalMessage("Don't be stooopid\n, Use lesser depth\n");
00916   }
00917     
00918   if (bddManager->depth > bddManager->maxDepth){
00919     /* Need to reallocate the memory for reqQue and
00920        requestNodeListArray */
00921     int oldMaxDepth = bddManager->maxDepth;
00922     bddManager->maxDepth = bddManager->depth;
00923     
00924     for (i=0; i<bddManager->maxDepth; i++){
00925       bddManager->requestNodeListArray[i] = Cal_Nil(CalRequestNode_t);
00926     }
00927 
00928     bddManager->reqQue = Cal_MemRealloc(CalHashTable_t **, bddManager->reqQue,
00929                                  bddManager->maxDepth);
00930     for (i=oldMaxDepth; i<bddManager->maxDepth; i++){
00931       int j;
00932       bddManager->reqQue[i] = Cal_MemAlloc(CalHashTable_t *, bddManager->maxNumVars+1);
00933       for (j=0; j<bddManager->numVars+1; j++){
00934         bddManager->reqQue[i][j] = CalHashTableInit(bddManager, j);
00935       }
00936     }
00937   }
00938   lastBdd = bddManager->bddNull;
00939   if (numBdds%2 != 0){/* Odd number of Bdd's */
00940     lastBdd = calBddArray[numBdds-1];
00941   }
00942   requestNodeList = bddManager->requestNodeListArray[0];
00943   for (i=0; i<numBdds/2; i++){
00944     CalNodeManagerAllocNode(bddManager->nodeManagerArray[0], requestNode);
00945     CalRequestNodePutF(requestNode, calBddArray[2*i]);
00946     CalRequestNodePutG(requestNode, calBddArray[2*i+1]);
00947     CalRequestNodePutNextRequestNode(requestNode, requestNodeList);
00948     requestNodeList = requestNode;
00949   }
00950   bddManager->requestNodeListArray[0] = requestNodeList;
00951 
00952   for (i=1; i<bddManager->depth; i++){
00953     requestNodeList = bddManager->requestNodeListArray[i];
00954     head = bddManager->requestNodeListArray[i-1];
00955     while ((odd = head) && (even = head->nextBddNode)){
00956       CalNodeManagerAllocNode(bddManager->nodeManagerArray[0], requestNode);
00957       /*
00958        * We don't have to worry about the Id's attached with
00959        * the requestNode or with the then and else part of it.
00960        */
00961       CalRequestNodePutThenRequestNode(requestNode, odd);
00962       CalRequestNodePutElseRequestNode(requestNode, even);
00963       CalRequestNodePutNextRequestNode(requestNode, requestNodeList);
00964       requestNodeList = requestNode;
00965       head = CalRequestNodeGetNextRequestNode(even);
00966     }
00967     if (odd != Cal_Nil(CalRequestNode_t)){/* There is an  odd node at this
00968                                       level */
00969       if (CalBddIsBddNull(bddManager,lastBdd)){ /* There are no odd nodes
00970                                                  * from previous levels, so
00971                                                  * make this an odd node.
00972                                                  */
00973         CalBddPutBddNode(lastBdd, odd);
00974       }
00975       else{ /* There exists an odd node, so make a pair now. */
00976         CalNodeManagerAllocNode(bddManager->nodeManagerArray[0], requestNode);
00977         CalRequestNodePutThenRequestNode(requestNode, odd);
00978         CalRequestNodePutElseRequest(requestNode, lastBdd);
00979         CalRequestNodePutNextRequestNode(requestNode, requestNodeList);
00980         lastBdd = bddManager->bddNull;
00981         requestNodeList = requestNode;
00982       }
00983     }
00984     bddManager->requestNodeListArray[i] = requestNodeList;
00985   }
00986 }

static Cal_Bdd_t BddMultiwayOp ( Cal_BddManager_t *  bddManager,
Cal_Bdd_t *  calBddArray,
int  numBdds,
CalOpProc_t  op 
) [static]

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

Synopsis [Internal routine for multiway operations]

Description [Internal routine for multiway operations]

SideEffects [None]

Definition at line 863 of file calBddOp.c.

00865 {
00866   int pipeDepth;
00867   CalRequestNode_t *requestNode;
00868   Cal_Bdd_t result;
00869   
00870   BddArrayToRequestNodeListArray(bddManager, calBddArray, numBdds);
00871   CalRequestNodeListArrayOp(bddManager, bddManager->requestNodeListArray, op);
00872   for(pipeDepth = 0; pipeDepth < bddManager->depth-1; pipeDepth++){
00873     CalRequestNode_t *next;
00874     for(requestNode = bddManager->requestNodeListArray[pipeDepth];
00875         requestNode != Cal_Nil(CalRequestNode_t); requestNode = next){
00876       next = CalRequestNodeGetNextRequestNode(requestNode);
00877       CalNodeManagerFreeNode(bddManager->nodeManagerArray[0],
00878                              requestNode);
00879     }
00880     bddManager->requestNodeListArray[pipeDepth] =
00881         Cal_Nil(CalRequestNode_t);
00882   }
00883   requestNode = bddManager->requestNodeListArray[bddManager->depth-1];
00884   bddManager->requestNodeListArray[bddManager->depth-1] =
00885       Cal_Nil(CalRequestNode_t); 
00886   CalRequestNodeGetThenRequest(requestNode, result); 
00887   CalNodeManagerFreeNode(bddManager->nodeManagerArray[0],
00888                          requestNode);
00889   return result;
00890 }

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

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

Synopsis [Returns the BDD for logical AND of argument BDDs]

Description [Returns the BDD for logical AND of f and g]

SideEffects [None]

Definition at line 90 of file calBddOp.c.

00094 {
00095   Cal_Bdd_t result;
00096   Cal_Bdd userResult;
00097   Cal_Bdd_t F, G;
00098 
00099   if (CalBddPreProcessing(bddManager, 2, fUserBdd, gUserBdd)){
00100     F = CalBddGetInternalBdd(bddManager, fUserBdd);
00101     G = CalBddGetInternalBdd(bddManager, gUserBdd);
00102     result = CalBddOpBF(bddManager, CalOpAnd, F, G);
00103   }
00104   else {
00105     return (Cal_Bdd)0;
00106   }
00107   userResult =  CalBddGetExternalBdd(bddManager, result);
00108   if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){
00109     Cal_BddFree(bddManager, userResult);
00110     Cal_BddManagerGC(bddManager);
00111     return (Cal_Bdd) 0;
00112   }
00113   return userResult;
00114 }

Cal_Bdd Cal_BddMultiwayAnd ( Cal_BddManager  bddManager,
Cal_Bdd *  userBddArray 
)

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

Synopsis [Returns the BDD for logical AND of argument BDDs]

Description [Returns the BDD for logical AND of set of BDDs in the bddArray]

SideEffects [None]

Definition at line 448 of file calBddOp.c.

00449 {
00450   int i, numBdds = 0;
00451   Cal_Bdd_t result;
00452   Cal_Bdd_t *calBddArray;
00453   Cal_Bdd userBdd;
00454 
00455   for (numBdds  = 0; (userBdd = userBddArray[numBdds]); numBdds++){
00456     if (CalBddPreProcessing(bddManager, 1, userBdd) == 0){
00457       return (Cal_Bdd) 0;
00458     }
00459   }
00460   
00461   if (numBdds == 0){
00462     CalBddWarningMessage("Multiway AND called with 0 length array");
00463     return (Cal_Bdd) 0;
00464   }
00465   else if (numBdds == 1){
00466     return Cal_BddIdentity(bddManager, userBddArray[0]);
00467   }
00468   else{
00469     calBddArray = Cal_MemAlloc(Cal_Bdd_t, numBdds+1);
00470     for (i = 0; i < numBdds; i++){
00471       calBddArray[i] = CalBddGetInternalBdd(bddManager, userBddArray[i]);
00472     }
00473     result = BddMultiwayOp(bddManager, calBddArray, numBdds, CalOpAnd);
00474     Cal_MemFree(calBddArray);
00475   }
00476   return CalBddGetExternalBdd(bddManager, result);
00477 }

Cal_Bdd Cal_BddMultiwayOr ( Cal_BddManager  bddManager,
Cal_Bdd *  userBddArray 
)

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

Synopsis [Returns the BDD for logical OR of argument BDDs]

Description [Returns the BDD for logical OR of set of BDDs in the bddArray]

SideEffects [None]

Definition at line 489 of file calBddOp.c.

00490 {
00491   int i, numBdds = 0;
00492   Cal_Bdd_t result;
00493   Cal_Bdd_t *calBddArray;
00494   Cal_Bdd userBdd;
00495 
00496   for (numBdds = 0; (userBdd = userBddArray[numBdds]); numBdds++){
00497     if (CalBddPreProcessing(bddManager, 1, userBdd) == 0){
00498       return (Cal_Bdd) 0;
00499     }
00500   }
00501   
00502   if (numBdds == 0){
00503     CalBddWarningMessage("Multiway OR called with 0 length array");
00504     return (Cal_Bdd) 0;
00505   }
00506   else if (numBdds == 1){
00507     return Cal_BddIdentity(bddManager, userBddArray[0]);
00508   }
00509   else{
00510     calBddArray = Cal_MemAlloc(Cal_Bdd_t, numBdds+1);
00511     for (i = 0; i < numBdds; i++){
00512       calBddArray[i] = CalBddGetInternalBdd(bddManager, userBddArray[i]);
00513     }
00514     result = BddMultiwayOp(bddManager, calBddArray, numBdds, CalOpOr);
00515     Cal_MemFree(calBddArray);
00516   }
00517   return CalBddGetExternalBdd(bddManager, result);
00518 }

Cal_Bdd Cal_BddMultiwayXor ( Cal_BddManager  bddManager,
Cal_Bdd *  userBddArray 
)

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

Synopsis [Returns the BDD for logical XOR of argument BDDs]

Description [Returns the BDD for logical XOR of set of BDDs in the bddArray]

SideEffects [None]

Definition at line 530 of file calBddOp.c.

00531 {
00532   int i, numBdds = 0;
00533   Cal_Bdd_t result;
00534   Cal_Bdd_t *calBddArray;
00535   Cal_Bdd userBdd;
00536 
00537   for (numBdds = 0; (userBdd = userBddArray[numBdds]); numBdds++){
00538     if (CalBddPreProcessing(bddManager, 1, userBdd) == 0){
00539       return (Cal_Bdd) 0;
00540     }
00541   }
00542   
00543   if (numBdds == 0){
00544     CalBddWarningMessage("Multiway OR called with 0 length array");
00545     return (Cal_Bdd) 0;
00546   }
00547   else if (numBdds == 1){
00548     return Cal_BddIdentity(bddManager, userBddArray[0]);
00549   }
00550   else{
00551     calBddArray = Cal_MemAlloc(Cal_Bdd_t, numBdds+1);
00552     for (i = 0; i < numBdds; i++){
00553       calBddArray[i] = CalBddGetInternalBdd(bddManager, userBddArray[i]);
00554     }
00555     result = BddMultiwayOp(bddManager, calBddArray, numBdds, CalOpXor);
00556     Cal_MemFree(calBddArray);
00557   }
00558   return CalBddGetExternalBdd(bddManager, result);
00559 }

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

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

Synopsis [Returns the BDD for logical NAND of argument BDDs]

Description [Returns the BDD for logical NAND of f and g]

SideEffects [None]

Definition at line 126 of file calBddOp.c.

00130 {
00131   Cal_Bdd_t result;
00132   Cal_Bdd_t F, G;
00133   Cal_Bdd userResult;
00134   if (CalBddPreProcessing(bddManager, 2, fUserBdd, gUserBdd)){
00135     F = CalBddGetInternalBdd(bddManager, fUserBdd); 
00136     G = CalBddGetInternalBdd(bddManager, gUserBdd); 
00137     result = CalBddOpBF(bddManager, CalOpNand, F, G);
00138   }
00139   else{
00140     return (Cal_Bdd) 0;
00141   }
00142   userResult =  CalBddGetExternalBdd(bddManager, result);
00143   if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){
00144     Cal_BddFree(bddManager, userResult);
00145     Cal_BddManagerGC(bddManager);
00146     return (Cal_Bdd) 0;
00147   }
00148   return userResult;
00149 }

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

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

Synopsis [Returns the BDD for logical NOR of argument BDDs]

Description [Returns the BDD for logical NOR of f and g]

SideEffects [None]

Definition at line 195 of file calBddOp.c.

00198 {
00199   Cal_Bdd_t result;
00200   Cal_Bdd userResult;
00201   Cal_Bdd_t F, G;
00202   if (CalBddPreProcessing(bddManager, 2, fUserBdd, gUserBdd)){
00203     F = CalBddGetInternalBdd(bddManager, fUserBdd); 
00204     G = CalBddGetInternalBdd(bddManager, gUserBdd); 
00205     result = CalBddOpBF(bddManager, CalOpOr, F, G);
00206     CalBddNot(result, result);
00207   }
00208   else{
00209     return (Cal_Bdd) 0;
00210   }
00211   userResult =  CalBddGetExternalBdd(bddManager, result);
00212   if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){
00213     Cal_BddFree(bddManager, userResult);
00214     Cal_BddManagerGC(bddManager);
00215     return (Cal_Bdd) 0;
00216   }
00217   return userResult;
00218 }

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

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

Synopsis [Returns the BDD for logical OR of argument BDDs]

Description [Returns the BDD for logical OR of f and g]

SideEffects [None]

Definition at line 161 of file calBddOp.c.

00164 {
00165   Cal_Bdd_t result;
00166   Cal_Bdd_t F, G;
00167   Cal_Bdd userResult;
00168   if (CalBddPreProcessing(bddManager, 2, fUserBdd, gUserBdd)){
00169     F = CalBddGetInternalBdd(bddManager, fUserBdd); 
00170     G = CalBddGetInternalBdd(bddManager, gUserBdd); 
00171     result = CalBddOpBF(bddManager, CalOpOr, F, G);
00172   }
00173   else{
00174     return (Cal_Bdd) 0;
00175   }
00176   userResult =  CalBddGetExternalBdd(bddManager, result);
00177   if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){
00178     Cal_BddFree(bddManager, userResult);
00179     Cal_BddManagerGC(bddManager);
00180     return (Cal_Bdd) 0;
00181   }
00182   return userResult;
00183 }

Cal_Bdd* Cal_BddPairwiseAnd ( Cal_BddManager  bddManager,
Cal_Bdd *  userBddArray 
)

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

Synopsis [Returns an array of BDDs obtained by logical AND of BDD pairs specified by an BDD array in which a BDD at an even location is paired with a BDD at an odd location of the array]

Description [Returns an array of BDDs obtained by logical AND of BDD pairs specified by an BDD array in which a BDD at an even location is paired with a BDD at an odd location of the array]

SideEffects [None]

SeeAlso [Cal_BddPairwiseOr]

Definition at line 303 of file calBddOp.c.

00304 {
00305   int i, num;
00306   Cal_Bdd_t *bddArray;
00307   Cal_Bdd_t *resultArray;
00308   Cal_Bdd userBdd;
00309   Cal_Bdd *userResultArray;
00310  
00311   for (num = 0; (userBdd = userBddArray[num]); num++){
00312     if (CalBddPreProcessing(bddManager, 1, userBdd) == 0){
00313       return Cal_Nil(Cal_Bdd);
00314     }
00315   }
00316   if ((num == 0) || (num%2 != 0)){
00317     fprintf(stdout,"Odd number of arguments passed to array AND\n");
00318     return Cal_Nil(Cal_Bdd);
00319   }
00320   bddArray = Cal_MemAlloc(Cal_Bdd_t, num);
00321   for (i = 0; i < num; i++){
00322     bddArray[i] = CalBddGetInternalBdd(bddManager, userBddArray[i]);
00323   }
00324   resultArray =  BddArrayOpBF(bddManager, bddArray, num, CalOpAnd);
00325   userResultArray = Cal_MemAlloc(Cal_Bdd, num/2);
00326   for (i=0; i<num/2; i++){
00327     userResultArray[i] = CalBddGetExternalBdd(bddManager, resultArray[i]);
00328   }
00329   Cal_MemFree(bddArray);
00330   Cal_MemFree(resultArray);
00331   if (CalBddPostProcessing(bddManager)  == CAL_BDD_OVERFLOWED){
00332     for (i=0; i<num/2; i++){
00333       Cal_BddFree(bddManager, userResultArray[i]);
00334       userResultArray[i] = (Cal_Bdd) 0;
00335     }
00336     Cal_BddManagerGC(bddManager);
00337     return userResultArray;
00338   }
00339   return userResultArray;
00340 }

Cal_Bdd* Cal_BddPairwiseOr ( Cal_BddManager  bddManager,
Cal_Bdd *  userBddArray 
)

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

Synopsis [Returns an array of BDDs obtained by logical OR of BDD pairs specified by an BDD array in which a BDD at an even location is paired with a BDD at an odd location of the array]

Description [Returns an array of BDDs obtained by logical OR of BDD pairs specified by an BDD array in which a BDD at an even location is paired with a BDD at an odd location of the array]

SideEffects [None]

SeeAlso [Cal_BddPairwiseAnd]

Definition at line 358 of file calBddOp.c.

00359 {
00360   int i, num=0;
00361   Cal_Bdd_t *bddArray;
00362   Cal_Bdd_t *resultArray;
00363   Cal_Bdd userBdd;
00364   Cal_Bdd *userResultArray;
00365  
00366   for (num = 0; (userBdd = userBddArray[num]); num++){
00367     if (CalBddPreProcessing(bddManager, 1, userBdd) == 0){
00368       return Cal_Nil(Cal_Bdd);
00369     }
00370   }
00371   if ((num == 0) || (num%2 != 0)){
00372     fprintf(stdout,"Odd number of arguments passed to array OR\n");
00373     return Cal_Nil(Cal_Bdd);
00374   }
00375   bddArray = Cal_MemAlloc(Cal_Bdd_t, num);
00376   for (i = 0; i < num; i++){
00377     bddArray[i] = CalBddGetInternalBdd(bddManager, userBddArray[i]);
00378   }
00379   resultArray =  BddArrayOpBF(bddManager, bddArray, num, CalOpOr);
00380   userResultArray = Cal_MemAlloc(Cal_Bdd, num/2);
00381   for (i=0; i<num/2; i++){
00382     userResultArray[i] = CalBddGetExternalBdd(bddManager, resultArray[i]);
00383   }
00384   Cal_MemFree(bddArray);
00385   Cal_MemFree(resultArray);
00386   return userResultArray;
00387 }

Cal_Bdd* Cal_BddPairwiseXor ( Cal_BddManager  bddManager,
Cal_Bdd *  userBddArray 
)

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

Synopsis [Returns an array of BDDs obtained by logical XOR of BDD pairs specified by an BDD array in which a BDD at an even location is paired with a BDD at an odd location of the array]

Description [Returns an array of BDDs obtained by logical XOR of BDD pairs specified by an BDD array in which a BDD at an even location is paired with a BDD at an odd location of the array]

SideEffects [None]

SeeAlso [Cal_BddPairwiseAnd]

Definition at line 405 of file calBddOp.c.

00406 {
00407   int i, num=0;
00408   Cal_Bdd_t *bddArray;
00409   Cal_Bdd_t *resultArray;
00410   Cal_Bdd userBdd;
00411   Cal_Bdd *userResultArray;
00412  
00413   for (num = 0; (userBdd = userBddArray[num]); num++){
00414     if (CalBddPreProcessing(bddManager, 1, userBdd) == 0){
00415       return Cal_Nil(Cal_Bdd);
00416     }
00417   }
00418   if ((num == 0) || (num%2 != 0)){
00419     fprintf(stdout,"Odd number of arguments passed to array OR\n");
00420     return Cal_Nil(Cal_Bdd);
00421   }
00422   bddArray = Cal_MemAlloc(Cal_Bdd_t, num);
00423   for (i = 0; i < num; i++){
00424     bddArray[i] = CalBddGetInternalBdd(bddManager, userBddArray[i]);
00425   }
00426   resultArray =  BddArrayOpBF(bddManager, bddArray, num, CalOpXor);
00427   userResultArray = Cal_MemAlloc(Cal_Bdd, num/2);
00428   for (i=0; i<num/2; i++){
00429     userResultArray[i] = CalBddGetExternalBdd(bddManager, resultArray[i]);
00430   }
00431   Cal_MemFree(bddArray);
00432   Cal_MemFree(resultArray);
00433   return userResultArray;
00434 }

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

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

Synopsis [Returns the BDD for logical exclusive NOR of argument BDDs]

Description [Returns the BDD for logical exclusive NOR of f and g]

SideEffects [None]

Definition at line 264 of file calBddOp.c.

00265 {
00266   Cal_Bdd_t result;
00267   Cal_Bdd userResult;
00268   Cal_Bdd_t F, G;
00269   if (CalBddPreProcessing(bddManager, 2, fUserBdd, gUserBdd)){
00270     F = CalBddGetInternalBdd(bddManager, fUserBdd); 
00271     G = CalBddGetInternalBdd(bddManager, gUserBdd); 
00272     result = CalBddOpBF(bddManager, CalOpXor, F, G);
00273     CalBddNot(result, result);
00274   }
00275   else{
00276     return (Cal_Bdd) 0;
00277   }
00278   userResult =  CalBddGetExternalBdd(bddManager, result);
00279   if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){
00280     Cal_BddFree(bddManager, userResult);
00281     Cal_BddManagerGC(bddManager);
00282     return (Cal_Bdd) 0;
00283   }
00284   return userResult;
00285 }

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

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

Synopsis [Returns the BDD for logical exclusive OR of argument BDDs]

Description [Returns the BDD for logical exclusive OR of f and g]

SideEffects [None]

Definition at line 230 of file calBddOp.c.

00233 {
00234   Cal_Bdd_t result;
00235   Cal_Bdd userResult;
00236   Cal_Bdd_t F, G;
00237   if (CalBddPreProcessing(bddManager, 2, fUserBdd, gUserBdd)){
00238     F = CalBddGetInternalBdd(bddManager, fUserBdd); 
00239     G = CalBddGetInternalBdd(bddManager, gUserBdd); 
00240     result = CalBddOpBF(bddManager, CalOpXor, F, G);
00241   }
00242   else{
00243     return (Cal_Bdd) 0;
00244   }
00245   userResult =  CalBddGetExternalBdd(bddManager, result);
00246   if (CalBddPostProcessing(bddManager) == CAL_BDD_OVERFLOWED){
00247     Cal_BddFree(bddManager, userResult);
00248     Cal_BddManagerGC(bddManager);
00249     return (Cal_Bdd) 0;
00250   }
00251   return userResult;
00252 }

Cal_Bdd_t CalBddOpBF ( Cal_BddManager_t *  bddManager,
CalOpProc_t  calOpProc,
Cal_Bdd_t  F,
Cal_Bdd_t  G 
)

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

Synopsis [Internal routine to compute a logical operation on a pair of BDDs]

Description [Internal routine to compute a logical operation on a pair of BDDs]

SideEffects [None]

Definition at line 705 of file calBddOp.c.

00710 {
00711   Cal_Bdd_t result;
00712   Cal_BddId_t minId, bddId;
00713   /*Cal_BddIndex_t minIndex; Commented out because of the problem on alpha*/ 
00714   int minIndex;
00715   int bddIndex;
00716   CalHashTable_t *hashTable, **hashTableArray, *uniqueTableForId;
00717   
00718   if (calOpProc(bddManager, F, G, &result)){
00719     return result;
00720   }
00721   CalBddGetMinIdAndMinIndex(bddManager, F, G, minId, minIndex);
00722   hashTableArray = bddManager->reqQue[0];
00723   CalHashTableFindOrAdd(hashTableArray[minId], F, G, &result);
00724   
00725   /* ReqQueApply */
00726   for(bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
00727     bddId = bddManager->indexToId[bddIndex];
00728     hashTable = hashTableArray[bddId];
00729     if(hashTable->numEntries){
00730       CalHashTableApply(bddManager, hashTable, hashTableArray, calOpProc);
00731     }
00732   }
00733 #ifdef COMPUTE_MEMORY_OVERHEAD
00734   {
00735     calNumEntriesAfterApply = 0;
00736     for(bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
00737       bddId = bddManager->indexToId[bddIndex];
00738       hashTable = hashTableArray[bddId];
00739       calNumEntriesAfterApply += hashTable->numEntries;
00740     }
00741   }
00742 #endif
00743   /* ReqQueReduce */
00744   for(bddIndex = bddManager->numVars - 1; bddIndex >= minIndex; bddIndex--){
00745     bddId = bddManager->indexToId[bddIndex];
00746     uniqueTableForId = bddManager->uniqueTable[bddId];
00747     hashTable = hashTableArray[bddId];
00748     if(hashTable->numEntries){
00749       CalHashTableReduce(bddManager, hashTable, uniqueTableForId);
00750     }
00751   }
00752   CalRequestIsForwardedTo(result);
00753 
00754 #ifdef COMPUTE_MEMORY_OVERHEAD
00755   {
00756     CalRequestNode_t *requestNode;
00757     calNumEntriesAfterReduce = 0;
00758     for(bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
00759       CalRequestNode_t *next;
00760       Cal_BddId_t bddId;
00761       
00762       bddId = bddManager->indexToId[bddIndex];
00763       hashTable = hashTableArray[bddId];
00764       for (requestNode = hashTable->requestNodeList; requestNode !=
00765                                                          Cal_Nil(CalRequestNode_t);
00766                                                      requestNode = next){
00767         next = CalRequestNodeGetNextRequestNode(requestNode);
00768         calNumEntriesAfterReduce++;
00769       }
00770     }
00771     calAfterReduceToAfterApplyNodesRatio =
00772         ((double)calNumEntriesAfterReduce)/((double)calNumEntriesAfterApply); 
00773     calAfterReduceToUniqueTableNodesRatio = 
00774         ((double)calNumEntriesAfterReduce)/((double)bddManager->numNodes);
00775   }
00776 #endif
00777 
00778   /* Clean up */
00779   for(bddIndex = minIndex; bddIndex < bddManager->numVars; bddIndex++){
00780     bddId = bddManager->indexToId[bddIndex];
00781     CalHashTableCleanUp(hashTableArray[bddId]);
00782   }
00783   return result;
00784 }

void CalRequestNodeListArrayOp ( Cal_BddManager_t *  bddManager,
CalRequestNode_t **  requestNodeListArray,
CalOpProc_t  calOpProc 
)

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

Synopsis [Computes result BDDs for an array of lists, each entry of which is pair of pointers, each of which points to a operand BDD or an entry in another list with a smaller array index]

Description [Computes result BDDs for an array of lists, each entry of which is pair of pointers, each of which points to a operand BDD or an entry in another list with a smaller array index]

SideEffects [ThenBDD pointer of an entry is over written by the result BDD and ElseBDD pointer is marked using FORWARD_FLAG]

Definition at line 582 of file calBddOp.c.

00585 {
00586   CalRequestNode_t *requestNode;
00587   CalRequest_t F, G, result;
00588   int pipeDepth, bddId, bddIndex;
00589   CalHashTable_t **reqQueAtPipeDepth, *hashTable, *uniqueTableForId;
00590   CalHashTable_t ***reqQue = bddManager->reqQue;
00591   
00592   /* ReqQueInsertUsingReqListArray */
00593   for(pipeDepth = 0; pipeDepth < bddManager->depth; pipeDepth++){
00594     reqQueAtPipeDepth = reqQue[pipeDepth];
00595     for(requestNode = requestNodeListArray[pipeDepth];
00596         requestNode != Cal_Nil(CalRequestNode_t);
00597         requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
00598       CalRequestNodeGetF(requestNode, F);
00599       CalRequestIsForwardedTo(F);
00600       CalRequestNodeGetG(requestNode, G);
00601       CalRequestIsForwardedTo(G);
00602       if((*calOpProc)(bddManager, F, G, &result) == 0){
00603         CalBddNormalize(F, G);
00604         CalBddGetMinId2(bddManager, F, G, bddId);
00605         CalHashTableFindOrAdd(reqQueAtPipeDepth[bddId], F, G, &result);
00606       }
00607       CalRequestNodePutThenRequest(requestNode, result);
00608       CalRequestNodePutElseRequestNode(requestNode, FORWARD_FLAG);
00609     }
00610   }
00611 
00612   /* ReqQueApply */
00613   for(bddIndex = 0; bddIndex < bddManager->numVars; bddIndex++){
00614     bddId = bddManager->indexToId[bddIndex];
00615     for(pipeDepth = 0; pipeDepth < bddManager->depth; pipeDepth++){
00616       reqQueAtPipeDepth = reqQue[pipeDepth];
00617       hashTable = reqQueAtPipeDepth[bddId];
00618       if(hashTable->numEntries){
00619         CalHashTableApply(bddManager, hashTable, reqQueAtPipeDepth, calOpProc);
00620       }
00621     }
00622   }
00623 
00624 #ifdef COMPUTE_MEMORY_OVERHEAD
00625   {
00626     calNumEntriesAfterApply = 0;
00627     for(bddIndex = 0; bddIndex < bddManager->numVars; bddIndex++){
00628       bddId = bddManager->indexToId[bddIndex];
00629       for(pipeDepth = 0; pipeDepth < bddManager->depth; pipeDepth++){
00630         reqQueAtPipeDepth = reqQue[pipeDepth];
00631         hashTable = reqQueAtPipeDepth[bddId];
00632         calNumEntriesAfterApply += hashTable->numEntries;
00633       }
00634     }
00635   }
00636 #endif
00637 
00638   /* ReqQueReduce */
00639   for(bddIndex = bddManager->numVars - 1; bddIndex >= 0; bddIndex--){
00640     bddId = bddManager->indexToId[bddIndex];
00641     uniqueTableForId = bddManager->uniqueTable[bddId];
00642     for(pipeDepth = 0; pipeDepth < bddManager->depth; pipeDepth++){
00643       hashTable = reqQue[pipeDepth][bddId];
00644       if(hashTable->numEntries){
00645         CalHashTableReduce(bddManager, hashTable, uniqueTableForId);
00646       }
00647     }
00648   }
00649 
00650 #ifdef COMPUTE_MEMORY_OVERHEAD
00651   {
00652     CalRequestNode_t *requestNode;
00653     calNumEntriesAfterReduce = 0;
00654     for(bddIndex = 0; bddIndex < bddManager->numVars; bddIndex++){
00655       CalRequestNode_t *next;
00656       Cal_BddId_t bddId;
00657       bddId = bddManager->indexToId[bddIndex];
00658       for(pipeDepth = 0; pipeDepth < bddManager->depth; pipeDepth++){
00659         hashTable = reqQue[pipeDepth][bddId];
00660         for (requestNode = hashTable->requestNodeList;
00661              requestNode != Cal_Nil(CalRequestNode_t); requestNode = next){
00662           next = CalRequestNodeGetNextRequestNode(requestNode);
00663           calNumEntriesAfterReduce++;
00664         }
00665       }
00666     }
00667     calAfterReduceToAfterApplyNodesRatio =
00668         ((double)calNumEntriesAfterReduce)/((double)calNumEntriesAfterApply); 
00669     calAfterReduceToUniqueTableNodesRatio = 
00670         ((double)calNumEntriesAfterReduce)/((double)bddManager->numNodes);
00671   }
00672 #endif
00673 
00674   /* ReqListArrayReqForward */
00675   for(pipeDepth = 0; pipeDepth < bddManager->depth; pipeDepth++){
00676     for(requestNode = requestNodeListArray[pipeDepth];
00677         requestNode != Cal_Nil(CalRequestNode_t);
00678         requestNode = CalRequestNodeGetNextRequestNode(requestNode)){
00679       CalRequestNodeGetThenRequest(requestNode, result);
00680       CalRequestIsForwardedTo(result);
00681       Cal_Assert(CalBddIsForwarded(result) == 0);
00682       CalRequestNodePutThenRequest(requestNode, result);
00683     }
00684   }
00685 
00686   /* ReqQueCleanUp */
00687   for(pipeDepth = 0; pipeDepth < bddManager->depth; pipeDepth++){
00688     reqQueAtPipeDepth = reqQue[pipeDepth];
00689     for(bddId = 1; bddId <= bddManager->numVars; bddId++){
00690       CalHashTableCleanUp(reqQueAtPipeDepth[bddId]);
00691     }
00692   }
00693 }

static int CeilLog2 ( int  number  )  [static]

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

Synopsis [Returns the smallest integer greater than or equal to log2 of a number]

Description [Returns the smallest integer greater than or equal to log2 of a number (The assumption is that the number is >= 1)]

SideEffects [None]

Definition at line 1002 of file calBddOp.c.

01004 {
01005   int num, count;
01006   for (num=number, count=0; num > 1; num >>= 1, count++);
01007   if ((1 << count) != number) count++;
01008   return count;
01009 }

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