src/calBdd/calUtil.c File Reference

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

Go to the source code of this file.

Defines

#define CAL_MODULUS1   2147483563
#define CAL_LEQA1   40014
#define CAL_LEQQ1   53668
#define CAL_LEQR1   12211
#define CAL_MODULUS2   2147483399
#define CAL_LEQA2   40692
#define CAL_LEQQ2   52774
#define CAL_LEQR2   3791
#define CAL_STAB_SIZE   64
#define CAL_STAB_DIV   (1 + (CAL_MODULUS1 - 1) / CAL_STAB_SIZE)

Functions

void Cal_ImageDump (Cal_BddManager_t *bddManager, FILE *fp)
void Cal_BddFunctionPrint (Cal_BddManager bddManager, Cal_Bdd userBdd, char *name)
void CalUniqueTablePrint (Cal_BddManager_t *bddManager)
void CalBddFunctionPrint (Cal_BddManager_t *bddManager, Cal_Bdd_t calBdd, char *name)
 while (count)
 if (allValid)
 va_end (ap)
 return (allValid)
int CalBddPostProcessing (Cal_BddManager_t *bddManager)
int CalBddArrayPreProcessing (Cal_BddManager_t *bddManager, Cal_Bdd *userBddArray)
Cal_Bdd_t CalBddGetInternalBdd (Cal_BddManager bddManager, Cal_Bdd userBdd)
Cal_Bdd CalBddGetExternalBdd (Cal_BddManager_t *bddManager, Cal_Bdd_t internalBdd)
void CalBddFatalMessage (char *string)
void CalBddWarningMessage (char *string)
void CalBddNodePrint (CalBddNode_t *bddNode)
void CalBddPrint (Cal_Bdd_t calBdd)
void CalHashTablePrint (CalHashTable_t *hashTable)
void CalHashTableOnePrint (CalHashTable_t *hashTable, int flag)
void CalUtilSRandom (long seed)
long CalUtilRandom (void)

Variables

static long utilRand = 0
static long utilRand2
static long shuffleSelect
static long shuffleTable [CAL_STAB_SIZE]
 allValid = 1

Define Documentation

#define CAL_LEQA1   40014

Definition at line 46 of file calUtil.c.

#define CAL_LEQA2   40692

Definition at line 50 of file calUtil.c.

#define CAL_LEQQ1   53668

Definition at line 47 of file calUtil.c.

#define CAL_LEQQ2   52774

Definition at line 51 of file calUtil.c.

#define CAL_LEQR1   12211

Definition at line 48 of file calUtil.c.

#define CAL_LEQR2   3791

Definition at line 52 of file calUtil.c.

#define CAL_MODULUS1   2147483563

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

FileName [calUtil.c]

PackageName [cal]

Synopsis [Utility functions for the Cal package.]

Description [Utility functions used in the Cal package.]

SeeAlso [optional]

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

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

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

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

Revision [

Id
calUtil.c,v 1.4 2002/09/10 00:10:37 fabio Exp

]

Definition at line 45 of file calUtil.c.

#define CAL_MODULUS2   2147483399

Definition at line 49 of file calUtil.c.

#define CAL_STAB_DIV   (1 + (CAL_MODULUS1 - 1) / CAL_STAB_SIZE)

Definition at line 54 of file calUtil.c.

#define CAL_STAB_SIZE   64

Definition at line 53 of file calUtil.c.

Function Documentation

void Cal_BddFunctionPrint ( Cal_BddManager  bddManager,
Cal_Bdd  userBdd,
char *  name 
)

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

Synopsis [Prints the function implemented by the argument BDD]

Description [Prints the function implemented by the argument BDD]

SideEffects [None]

Definition at line 128 of file calUtil.c.

00130 {
00131   Cal_Bdd_t calBdd;
00132   calBdd = CalBddGetInternalBdd(bddManager, userBdd);
00133   CalBddFunctionPrint(bddManager, calBdd, name);
00134 }

void Cal_ImageDump ( Cal_BddManager_t *  bddManager,
FILE *  fp 
)

AutomaticStart AutomaticEnd

Definition at line 91 of file calUtil.c.

00092 {
00093 
00094   CalPageManager_t *pageManager;
00095   int i, j;
00096   char *segment, c;
00097   int count = NUM_PAGES_PER_SEGMENT * PAGE_SIZE;
00098 
00099   pageManager = bddManager->pageManager1;
00100   for(i = 0; i < pageManager->numSegments; i++){
00101     segment = (char *) pageManager->pageSegmentArray[i];
00102     for(j = 1; j <= count; j++){
00103       c = segment[j];
00104       fprintf(fp, "%c", j%64?c:'\n');
00105     }
00106   }
00107   pageManager = bddManager->pageManager2;
00108   for(i = 0; i < pageManager->numSegments; i++){
00109     segment = (char *) pageManager->pageSegmentArray[i];
00110     for(j = 1; j <= count; j++){
00111       c = segment[j];
00112       fprintf(fp, "%c", j%64?c:'\n');
00113     }
00114   }
00115 }

int CalBddArrayPreProcessing ( Cal_BddManager_t *  bddManager,
Cal_Bdd *  userBddArray 
)

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 330 of file calUtil.c.

00331 {
00332   int i = 0;
00333   Cal_Bdd userBdd;
00334   while ((userBdd = userBddArray[i++])){
00335     if (CalBddPreProcessing(bddManager, 1, userBdd) == 0){
00336       return 0;
00337     }
00338   }
00339   return 1;
00340 }

void CalBddFatalMessage ( char *  string  ) 

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

Name [CalBddFatalMessage]

Synopsis [Prints fatal message and exits.]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 425 of file calUtil.c.

00426 {
00427   (void) fprintf(stderr,"Fatal: %s\n", string);
00428   exit(-1);
00429 }

void CalBddFunctionPrint ( Cal_BddManager_t *  bddManager,
Cal_Bdd_t  calBdd,
char *  name 
)

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

Synopsis [Prints the function implemented by the argument BDD]

Description [Prints the function implemented by the argument BDD]

SideEffects [None]

Definition at line 169 of file calUtil.c.

00172 {
00173   Cal_Bdd_t T,E;
00174   Cal_BddId_t id;
00175   char c;
00176   static int level;
00177 
00178   if(level == 0)printf("%s = ",name);
00179   level++;
00180   printf("( ");
00181   if(CalBddIsBddZero(bddManager, calBdd)){
00182     printf("0 ");
00183   }
00184   else if(CalBddIsBddOne(bddManager, calBdd)){
00185     printf("1 ");
00186   }
00187   else{
00188     id = CalBddGetBddId(calBdd);
00189     c = (char)((int)'a' + id - 1);
00190     printf("%c ", c);
00191     CalBddGetCofactors(calBdd, id, T, E);
00192     CalBddFunctionPrint(bddManager, T, " ");
00193     printf("+ %c' ", c);
00194     CalBddFunctionPrint(bddManager, E, " ");
00195   }
00196   level--;
00197   printf(") ");
00198   if(level == 0)printf("\n");
00199 }

Cal_Bdd CalBddGetExternalBdd ( Cal_BddManager_t *  bddManager,
Cal_Bdd_t  internalBdd 
)

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

Name [CalBddFatalMessage]

Synopsis [Prints fatal message and exits.]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 386 of file calUtil.c.

00387 {
00388   CalHashTable_t *hashTableForUserBdd = bddManager->uniqueTable[0];
00389   Cal_Bdd_t resultBdd;
00390   int found;
00391   
00392   if(CalBddIsOutPos(internalBdd)){
00393     found = CalHashTableFindOrAdd(hashTableForUserBdd, internalBdd,
00394                           bddManager->bddOne, &resultBdd);
00395   }
00396   else {
00397     Cal_Bdd_t internalBddNot;
00398     CalBddNot(internalBdd, internalBddNot);
00399     found = CalHashTableFindOrAdd(hashTableForUserBdd, internalBddNot,
00400                           bddManager->bddOne, &resultBdd);
00401     CalBddNot(resultBdd, resultBdd);
00402   }
00403   if (found == 0){
00404     CalBddIcrRefCount(internalBdd);
00405   }
00406   CalBddIcrRefCount(resultBdd);
00407   return CalBddGetBddNode(resultBdd);
00408 }

Cal_Bdd_t CalBddGetInternalBdd ( Cal_BddManager  bddManager,
Cal_Bdd  userBdd 
)

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

Name [CalBddFatalMessage]

Synopsis [Prints fatal message and exits.]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 357 of file calUtil.c.

00358 {
00359   Cal_Bdd_t resultBdd;
00360   if (CalBddNodeIsOutPos(userBdd)){
00361     CalBddNodeGetThenBdd(userBdd, resultBdd);
00362   }
00363   else {
00364     Cal_Bdd userBddNot = CalBddNodeNot(userBdd);
00365     Cal_Bdd_t internalBdd;
00366         CalBddNodeGetThenBdd(userBddNot,internalBdd);
00367     CalBddNot(internalBdd, resultBdd);
00368   }
00369   return resultBdd;
00370 }

void CalBddNodePrint ( CalBddNode_t *  bddNode  ) 

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 461 of file calUtil.c.

00462 {
00463   int refCount;
00464   CalBddNodeGetRefCount(bddNode, refCount);
00465   printf("Node (%lx) thenBdd(%2d %lx)  elseBdd(%2d %lx) ref_count (%d) next (%lx)\n",
00466          (CalAddress_t)bddNode,
00467          CalBddNodeGetThenBddId(bddNode),
00468          (CalAddress_t) CalBddNodeGetThenBddNode(bddNode), 
00469          CalBddNodeGetElseBddId(bddNode),
00470          (CalAddress_t) CalBddNodeGetElseBddNode(bddNode),
00471          refCount, (CalAddress_t)bddNode->nextBddNode);
00472 }

int CalBddPostProcessing ( Cal_BddManager_t *  bddManager  ) 

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 275 of file calUtil.c.

00276 {
00277   if (bddManager->gcCheck > 0) return CAL_BDD_OK;
00278   bddManager->gcCheck = CAL_GC_CHECK;
00279   if(bddManager->numNodes > bddManager->uniqueTableGCLimit){
00280     long origNodes = bddManager->numNodes;
00281     Cal_BddManagerGC(bddManager);
00282     if ((bddManager->numNodes > bddManager->reorderingThreshold) &&
00283         (3*bddManager->numNodes > 2* bddManager->uniqueTableGCLimit) &&
00284         (bddManager->dynamicReorderingEnableFlag) &&
00285         (bddManager->reorderTechnique != CAL_REORDER_NONE)){
00286       CalCacheTableTwoFlush(bddManager->cacheTable);
00287       if (bddManager->reorderMethod == CAL_REORDER_METHOD_BF){
00288         CalBddReorderAuxBF(bddManager);
00289       }
00290       else{
00291         CalBddReorderAuxDF(bddManager);
00292       }
00293     }
00294     else {
00295       /* Check if we should repack */
00296       Cal_Assert(CalCheckAllValidity(bddManager));
00297       if (bddManager->numNodes <
00298           bddManager->repackAfterGCThreshold*origNodes){
00299         CalRepackNodesAfterGC(bddManager);
00300       }
00301       Cal_Assert(CalCheckAllValidity(bddManager));
00302     }
00303     Cal_BddManagerSetGCLimit(bddManager);
00304     if (bddManager->nodeLimit && (bddManager->numNodes >
00305                                   bddManager->nodeLimit)){ 
00306       CalBddWarningMessage("Overflow: Node Limit Exceeded");
00307       bddManager->overflow = 1;
00308       return CAL_BDD_OVERFLOWED;
00309     }
00310     /*
00311      * Check to see if the cache table needs to be rehashed.
00312      */
00313     CalCacheTableRehash(bddManager);
00314   }
00315   return CAL_BDD_OK;
00316 }

void CalBddPrint ( Cal_Bdd_t  calBdd  ) 

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 487 of file calUtil.c.

00488 {
00489   printf("Id(%2d) node(%lx) ",
00490       CalBddGetBddId(calBdd), (CalAddress_t) CalBddGetBddNode(calBdd));
00491   printf("thenBdd(%2d %lx)  elseBdd(%2d %lx)\n",
00492          CalBddGetThenBddId(calBdd),
00493          (CalAddress_t) CalBddGetThenBddNode(calBdd), 
00494          CalBddGetElseBddId(calBdd),
00495          (CalAddress_t) CalBddGetElseBddNode(calBdd));
00496 }

void CalBddWarningMessage ( char *  string  ) 

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

Name [CalBddWarningMessage]

Synopsis [Prints warning message.]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 444 of file calUtil.c.

00445 {
00446   (void) fprintf(stderr,"Warning: %s\n", string);
00447 }

void CalHashTableOnePrint ( CalHashTable_t *  hashTable,
int  flag 
)

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 575 of file calUtil.c.

00576 {
00577   int i;
00578   CalBddNode_t *ptr, *node;
00579   Cal_Bdd_t keyBdd;
00580 
00581   printf("*************************************************\n");
00582   for(i = 0; i < hashTable->numBins; i++){
00583     ptr = hashTable->bins[i];
00584     while(ptr != Cal_Nil(CalBddNode_t)){
00585       CalBddNodeGetThenBdd(ptr, keyBdd);
00586       node = CalBddNodeGetElseBddNode(ptr);
00587       if(flag == 1){
00588         printf("Key(%d %lx) Value(%f)\n", 
00589             CalBddGetBddId(keyBdd), (CalAddress_t)CalBddGetBddNode(keyBdd), *(double *)node); 
00590       }
00591       else{
00592         printf("Key(%d %lx) Value(%d)\n",
00593             CalBddGetBddId(keyBdd), (CalAddress_t)CalBddGetBddNode(keyBdd),  *(int *)node); 
00594       }
00595       ptr = CalBddNodeGetNextBddNode(ptr);
00596     }
00597   }
00598 }

void CalHashTablePrint ( CalHashTable_t *  hashTable  ) 

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

Synopsis [Prints a hash table.]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 530 of file calUtil.c.

00531 {
00532   int i;
00533   CalBddNode_t *ptr;
00534   Cal_Bdd_t calBdd, T, E;
00535   int refCount, firstFlag;
00536 
00537   printf("HashTable bddId(%d) entries(%ld) bins(%ld) capacity(%ld)\n",
00538          hashTable->bddId, hashTable->numEntries, hashTable->numBins,
00539          hashTable->maxCapacity);
00540   for(i = 0; i < hashTable->numBins; i++){
00541     ptr = hashTable->bins[i];
00542     firstFlag = 1;
00543     while(ptr != Cal_Nil(CalBddNode_t)){
00544       CalBddPutBddNode(calBdd, ptr);
00545       CalBddNodeGetThenBdd(ptr, T);
00546       CalBddNodeGetElseBdd(ptr, E);
00547       if (firstFlag){
00548         printf("\tbin = (%d) ", i);
00549         firstFlag = 0;
00550       }
00551       printf("\t\tbddNode(%lx) ", (CalAddress_t)ptr);
00552       printf("thenId(%d) ", CalBddGetBddId(T)); 
00553       printf("thenBddNode(%lx) ", (CalAddress_t) CalBddGetBddNode(T));
00554       printf("elseId(%d) ", CalBddGetBddId(E)); 
00555       printf("elseBddNode(%lx) ", (unsigned long)CalBddGetBddNode(E));
00556       CalBddGetRefCount(calBdd, refCount);
00557       printf("refCount(%d)\n", refCount);
00558       ptr = CalBddNodeGetNextBddNode(ptr);
00559     }
00560   }
00561 }

void CalUniqueTablePrint ( Cal_BddManager_t *  bddManager  ) 

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 151 of file calUtil.c.

00152 {
00153   int i;
00154   for(i = 0; i <= bddManager->numVars; i++){
00155     CalHashTablePrint(bddManager->uniqueTable[i]);
00156   }
00157 }

long CalUtilRandom ( void   ) 

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

Synopsis [Portable random number generator.]

Description [Portable number generator based on ran2 from "Numerical Recipes in C." It is a long period (> 2 * 10^18) random number generator of L'Ecuyer with Bays-Durham shuffle. Returns a long integer uniformly distributed between 0 and 2147483561 (inclusive of the endpoint values). The random generator can be explicitly initialized by calling CalUtilSRandom. If no explicit initialization is performed, then the seed 1 is assumed.]

SideEffects []

SeeAlso [CalUtilSRandom]

Definition at line 654 of file calUtil.c.

00655 {
00656     int i;      /* index in the shuffle table */
00657     long int w; /* work variable */
00658 
00659     /* utilRand == 0 if the geneartor has not been initialized yet. */
00660     if (utilRand == 0) CalUtilSRandom((long)1);
00661 
00662     /* Compute utilRand = (utilRand * CAL_LEQA1) % CAL_MODULUS1 avoiding
00663     ** overflows by Schrage's method.
00664     */
00665     w          = utilRand / CAL_LEQQ1;
00666     utilRand   = CAL_LEQA1 * (utilRand - w * CAL_LEQQ1) - w * CAL_LEQR1;
00667     utilRand  += (utilRand < 0) * CAL_MODULUS1;
00668 
00669     /* Compute utilRand2 = (utilRand2 * CAL_LEQA2) % CAL_MODULUS2 avoiding
00670     ** overflows by Schrage's method.
00671     */
00672     w          = utilRand2 / CAL_LEQQ2;
00673     utilRand2  = CAL_LEQA2 * (utilRand2 - w * CAL_LEQQ2) - w * CAL_LEQR2;
00674     utilRand2 += (utilRand2 < 0) * CAL_MODULUS2;
00675 
00676     /* utilRand is shuffled with the Bays-Durham algorithm.
00677     ** shuffleSelect and utilRand2 are combined to generate the output.
00678     */
00679 
00680     /* Pick one element from the shuffle table; "i" will be in the range
00681     ** from 0 to CAL_STAB_SIZE-1.
00682     */
00683     i = shuffleSelect / CAL_STAB_DIV;
00684     /* Mix the element of the shuffle table with the current iterate of
00685     ** the second sub-generator, and replace the chosen element of the
00686     ** shuffle table with the current iterate of the first sub-generator.
00687     */
00688     shuffleSelect   = shuffleTable[i] - utilRand2;
00689     shuffleTable[i] = utilRand;
00690     shuffleSelect  += (shuffleSelect < 1) * (CAL_MODULUS1 - 1);
00691     /* Since shuffleSelect != 0, and we want to be able to return 0,
00692     ** here we subtract 1 before returning.
00693     */
00694     return(shuffleSelect - 1);
00695 
00696 } /* end of CalUtilRandom */

void CalUtilSRandom ( long  seed  ) 

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

Synopsis [Initializer for the portable random number generator.]

Description [Initializer for the portable number generator based on ran2 in "Numerical Recipes in C." The input is the seed for the generator. If it is negative, its absolute value is taken as seed. If it is 0, then 1 is taken as seed. The initialized sets up the two recurrences used to generate a long-period stream, and sets up the shuffle table.]

SideEffects [None]

SeeAlso [CalUtilRandom]

Definition at line 617 of file calUtil.c.

00618 {
00619     int i;
00620 
00621     if (seed < 0)       utilRand = -seed;
00622     else if (seed == 0) utilRand = 1;
00623     else                utilRand = seed;
00624     utilRand2 = utilRand;
00625     /* Load the shuffle table (after 11 warm-ups). */
00626     for (i = 0; i < CAL_STAB_SIZE + 11; i++) {
00627         long int w;
00628         w = utilRand / CAL_LEQQ1;
00629         utilRand = CAL_LEQA1 * (utilRand - w * CAL_LEQQ1) - w * CAL_LEQR1;
00630         utilRand += (utilRand < 0) * CAL_MODULUS1;
00631         shuffleTable[i % CAL_STAB_SIZE] = utilRand;
00632     }
00633     shuffleSelect = shuffleTable[1 % CAL_STAB_SIZE];
00634 } /* end of CalUtilSRandom */

if ( allValid   ) 

Definition at line 255 of file calUtil.c.

00255                 {
00256     CalBddPostProcessing(bddManager);
00257   }

return ( allValid   ) 
va_end ( ap   ) 
while ( count   ) 

Definition at line 242 of file calUtil.c.

00242                {
00243     fUserBdd = va_arg(ap, Cal_Bdd);
00244         if (fUserBdd == 0){
00245           allValid=0;
00246     }
00247         else {
00248       f = CalBddGetInternalBdd(bddManager, fUserBdd);
00249       if (CalBddIsRefCountZero(f)){
00250         CalBddFatalMessage("Bdd With Zero Reference Count Used.");
00251       }
00252     }
00253     --count;
00254   }

Variable Documentation

allValid = 1

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

Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 241 of file calUtil.c.

long shuffleSelect [static]

Definition at line 70 of file calUtil.c.

long shuffleTable[CAL_STAB_SIZE] [static]

Definition at line 71 of file calUtil.c.

long utilRand = 0 [static]

Definition at line 68 of file calUtil.c.

long utilRand2 [static]

Definition at line 69 of file calUtil.c.

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