glu-2.2: src/calBdd/calUtil.c Source File

00001 
00039 #include "calInt.h"
00040 
00041 /*---------------------------------------------------------------------------*/
00042 /* Constant declarations                                                     */
00043 /*---------------------------------------------------------------------------*/
00044 /* Random generator constants. */
00045 #define CAL_MODULUS1 2147483563
00046 #define CAL_LEQA1 40014
00047 #define CAL_LEQQ1 53668
00048 #define CAL_LEQR1 12211
00049 #define CAL_MODULUS2 2147483399
00050 #define CAL_LEQA2 40692
00051 #define CAL_LEQQ2 52774
00052 #define CAL_LEQR2 3791
00053 #define CAL_STAB_SIZE 64
00054 #define CAL_STAB_DIV (1 + (CAL_MODULUS1 - 1) / CAL_STAB_SIZE)
00055 
00056 /*---------------------------------------------------------------------------*/
00057 /* Type declarations                                                         */
00058 /*---------------------------------------------------------------------------*/
00059 
00060 
00061 /*---------------------------------------------------------------------------*/
00062 /* Stucture declarations                                                     */
00063 /*---------------------------------------------------------------------------*/
00064 
00065 /*---------------------------------------------------------------------------*/
00066 /* Variable declarations                                                     */
00067 /*---------------------------------------------------------------------------*/
00068 static long utilRand = 0;
00069 static long utilRand2;
00070 static long shuffleSelect;
00071 static long shuffleTable[CAL_STAB_SIZE];
00072 
00073 /*---------------------------------------------------------------------------*/
00074 /* Macro declarations                                                        */
00075 /*---------------------------------------------------------------------------*/
00076 
00077 
00080 /*---------------------------------------------------------------------------*/
00081 /* Static function prototypes                                                */
00082 /*---------------------------------------------------------------------------*/
00083 
00084 
00087 /*---------------------------------------------------------------------------*/
00088 /* Definition of exported functions                                          */
00089 /*---------------------------------------------------------------------------*/
00090 void
00091 Cal_ImageDump(Cal_BddManager_t *bddManager, FILE *fp)
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 }
00116 
00117 
00127 void
00128 Cal_BddFunctionPrint(Cal_BddManager bddManager, Cal_Bdd  userBdd,
00129                      char *name)
00130 {
00131   Cal_Bdd_t calBdd;
00132   calBdd = CalBddGetInternalBdd(bddManager, userBdd);
00133   CalBddFunctionPrint(bddManager, calBdd, name);
00134 }
00135 
00136 /*---------------------------------------------------------------------------*/
00137 /* Definition of internal functions                                          */
00138 /*---------------------------------------------------------------------------*/
00150 void
00151 CalUniqueTablePrint(Cal_BddManager_t *bddManager)
00152 {
00153   int i;
00154   for(i = 0; i <= bddManager->numVars; i++){
00155     CalHashTablePrint(bddManager->uniqueTable[i]);
00156   }
00157 }
00158 
00168 void
00169 CalBddFunctionPrint(Cal_BddManager_t * bddManager,
00170                     Cal_Bdd_t  calBdd,
00171                     char * name)
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 }
00200 
00212 #if HAVE_STDARG_H
00213 int
00214 CalBddPreProcessing(Cal_BddManager_t *bddManager, int count, ...)
00215 {
00216   int allValid;
00217   va_list ap;
00218   Cal_Bdd fUserBdd;
00219   Cal_Bdd_t f;
00220   
00221   va_start(ap, count);
00222 #else
00223 #  if HAVE_VARARGS_H
00224 int
00225 CalBddPreProcessing(va_alist)
00226 va_dcl
00227 {
00228   int allValid;
00229   va_list ap;
00230   Cal_Bdd *fUserBdd;
00231   int count;
00232   Cal_BddManager_t *bddManager;
00233   Cal_Bdd_t f;
00234   
00235   va_start(ap);
00236   bddManager = va_arg(ap, Cal_BddManager_t *);
00237   count = va_arg(ap, int);
00238 #  endif
00239 #endif  
00240 
00241   allValid=1;
00242   while (count){
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   }
00255   if (allValid) {
00256     CalBddPostProcessing(bddManager);
00257   }
00258   va_end(ap);
00259   return (allValid);
00260 }
00261 
00262 
00274 int
00275 CalBddPostProcessing(Cal_BddManager_t *bddManager)
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 }
00317 
00329 int
00330 CalBddArrayPreProcessing(Cal_BddManager_t *bddManager, Cal_Bdd *userBddArray) 
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 }
00341     
00342                        
00356 Cal_Bdd_t
00357 CalBddGetInternalBdd(Cal_BddManager bddManager, Cal_Bdd userBdd)
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 }
00371 
00385 Cal_Bdd
00386 CalBddGetExternalBdd(Cal_BddManager_t *bddManager, Cal_Bdd_t internalBdd)
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 }
00409 
00410 
00424 void
00425 CalBddFatalMessage(char *string)
00426 {
00427   (void) fprintf(stderr,"Fatal: %s\n", string);
00428   exit(-1);
00429 }
00443 void
00444 CalBddWarningMessage(char *string)
00445 {
00446   (void) fprintf(stderr,"Warning: %s\n", string);
00447 }
00448 
00460 void
00461 CalBddNodePrint(CalBddNode_t *bddNode)
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 }
00473 
00486 void
00487 CalBddPrint(Cal_Bdd_t calBdd)
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 }
00497 
00498 #ifdef TEST_CALBDDNODE
00499 main(int argc, char **argv)
00500 {
00501   CalBddNode_t *bddNode, *thenBddNode, *elseBddNode;
00502 
00503   bddNode = Cal_MemAlloc(CalBddNode_t, 1);
00504   thenBddNode = Cal_MemAlloc(CalBddNode_t, 1);
00505   elseBddNode = Cal_MemAlloc(CalBddNode_t, 1);
00506 
00507   CalBddNodePutThenBddId(bddNode, 1);
00508   CalBddNodePutThenBddNode(bddNode, thenBddNode);
00509   CalBddNodePutElseBddId(bddNode, 2);
00510   CalBddNodePutElseBddNode(bddNode, elseBddNode);
00511 
00512   printf("then( 1 %x) else( 2 %x)\n", thenBddNode, elseBddNode);
00513   CalBddNodePrint(bddNode);
00514 }
00515 #endif
00516 
00517 
00529 void
00530 CalHashTablePrint(CalHashTable_t *hashTable)
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 }
00562 
00574 void
00575 CalHashTableOnePrint(CalHashTable_t *hashTable, int flag)
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 }
00599 
00616 void
00617 CalUtilSRandom(long seed)
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 */
00635 
00653 long
00654 CalUtilRandom(void)
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 */
00697 
00698