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

00001 
00040 #include "calInt.h"
00041 
00042 /*---------------------------------------------------------------------------*/
00043 /* Constant declarations                                                     */
00044 /*---------------------------------------------------------------------------*/
00045 
00046 /*---------------------------------------------------------------------------*/
00047 /* Type declarations                                                         */
00048 /*---------------------------------------------------------------------------*/
00049 typedef int (*CountFn_t)(Cal_Bdd_t);
00050 
00051 /*---------------------------------------------------------------------------*/
00052 /* Stucture declarations                                                     */
00053 /*---------------------------------------------------------------------------*/
00054 
00055 /*---------------------------------------------------------------------------*/
00056 /* Variable declarations                                                     */
00057 /*---------------------------------------------------------------------------*/
00058 
00059 
00060 /*---------------------------------------------------------------------------*/
00061 /* Macro declarations                                                        */
00062 /*---------------------------------------------------------------------------*/
00063 
00066 /*---------------------------------------------------------------------------*/
00067 /* Static function prototypes                                                */
00068 /*---------------------------------------------------------------------------*/
00069 
00070 static void BddMarkBdd(Cal_Bdd_t f);
00071 static int BddCountNoNodes(Cal_Bdd_t f);
00072 static int BddCountNodes(Cal_Bdd_t f);
00073 static long BddSizeStep(Cal_Bdd_t f, CountFn_t countFn);
00074 static void BddProfileStep(Cal_BddManager_t * bddManager, Cal_Bdd_t f, long * levelCounts, CountFn_t countFn);
00075 static void BddHighestRefStep(Cal_BddManager_t * bddManager, Cal_Bdd_t f, CalHashTable_t * h);
00076 static void BddDominatedStep(Cal_BddManager_t * bddManager, Cal_Bdd_t f, long * funcCounts, CalHashTable_t * h);
00077 
00080 static
00081 int (*(countingFns[]))(Cal_Bdd_t) = 
00082 {
00083   BddCountNoNodes,
00084   BddCountNodes,
00085 };
00086 
00087 /*---------------------------------------------------------------------------*/
00088 /* Definition of exported functions                                          */
00089 /*---------------------------------------------------------------------------*/
00090 
00103 long
00104 Cal_BddSize(Cal_BddManager bddManager, Cal_Bdd fUserBdd, int  negout)
00105 {
00106   Cal_Bdd_t f, g;
00107 
00108   if(CalBddPreProcessing(bddManager, 1, fUserBdd)){
00109     f = CalBddGetInternalBdd(bddManager, fUserBdd);
00110     g =  CalBddOne(bddManager);
00111     CalBddPutMark(g, 0);
00112     BddMarkBdd(f);
00113     return BddSizeStep(f, countingFns[!negout]);
00114   }
00115   return (0l);
00116 }
00117 
00118 
00131 long
00132 Cal_BddSizeMultiple(Cal_BddManager bddManager, Cal_Bdd *fUserBddArray,
00133                     int  negout)
00134 {
00135   long size;
00136   Cal_Bdd_t *f;
00137   Cal_Bdd_t g;
00138   Cal_Bdd_t *fArray;
00139   int i, j;
00140   
00141   if (CalBddArrayPreProcessing(bddManager, fUserBddArray) == 0){
00142     return -1;
00143   }
00144   
00145   for(i = 0; fUserBddArray[i]; ++i);
00146 
00147   fArray = Cal_MemAlloc(Cal_Bdd_t, i+1);
00148   for (j=0; j < i; j++){
00149     fArray[j] = CalBddGetInternalBdd(bddManager,fUserBddArray[j]);
00150   }
00151   fArray[j] = bddManager->bddNull;
00152   
00153   g  =  CalBddOne(bddManager);
00154   CalBddPutMark(g, 0);
00155   for(f = fArray; !CalBddIsBddNull(bddManager, *f); ++f){
00156     BddMarkBdd(*f);
00157   }
00158   size  =  0l;
00159   for(f = fArray; !CalBddIsBddNull(bddManager, *f); ++f){
00160     size +=  BddSizeStep(*f, countingFns[!negout]);
00161   }
00162   Cal_MemFree(fArray);
00163   return size;
00164 }
00165 
00179 void
00180 Cal_BddProfile(Cal_BddManager bddManager, Cal_Bdd fUserBdd,
00181                long * levelCounts, int  negout)
00182 {
00183   Cal_BddIndex_t i;
00184   Cal_Bdd_t f, g;
00185   if(CalBddPreProcessing(bddManager, 1, fUserBdd)){
00186     f = CalBddGetInternalBdd(bddManager, fUserBdd);
00187     for(i = 0; i <=  bddManager->numVars; i++){
00188       levelCounts[i] = 0l;
00189     }
00190     g = CalBddOne(bddManager);
00191     CalBddPutMark(g, 0);
00192     BddMarkBdd(f);
00193     BddProfileStep(bddManager, f, levelCounts, countingFns[!negout]);
00194   }
00195 }
00196 
00197 
00209 void
00210 Cal_BddProfileMultiple(Cal_BddManager bddManager, Cal_Bdd *fUserBddArray,
00211                        long * levelCounts, int  negout)
00212 {
00213   Cal_Bdd_t *f, *fArray;
00214   Cal_Bdd_t g;
00215   int i, j;
00216   
00217   CalBddArrayPreProcessing(bddManager, fUserBddArray);
00218 
00219   for(i = 0; fUserBddArray[i]; ++i);
00220 
00221   fArray = Cal_MemAlloc(Cal_Bdd_t, i+1);
00222   for (j=0; j < i; j++){
00223     fArray[j] = CalBddGetInternalBdd(bddManager,fUserBddArray[j]);
00224   }
00225   fArray[j] = bddManager->bddNull;
00226     
00227   for(i = 0; i <=  bddManager->numVars; i++){
00228     levelCounts[i] = 0l;
00229   }
00230   g = CalBddOne(bddManager);
00231   CalBddPutMark(g, 0);
00232   for(f = fArray; !CalBddIsBddNull(bddManager, *f); ++f){
00233     BddMarkBdd(*f);
00234   }
00235   for(f = fArray; !CalBddIsBddNull(bddManager, *f); ++f){
00236     BddProfileStep(bddManager, *f, levelCounts, countingFns[!negout]);
00237   }
00238   Cal_MemFree(fArray);
00239 }
00240 
00241 
00256 void
00257 Cal_BddFunctionProfile(Cal_BddManager bddManager, Cal_Bdd fUserBdd,
00258                        long * funcCounts) 
00259 {
00260   long i;
00261   Cal_BddIndex_t j;
00262   CalHashTable_t *h;
00263   Cal_Bdd_t f;
00264   
00265   /* The number of subfunctions obtainable by restricting the */
00266   /* variables of index < n is the number of subfunctions whose top */
00267   /* variable has index n plus the number of subfunctions obtainable */
00268   /* by restricting the variables of index < n+1 minus the number of */
00269   /* these latter subfunctions whose highest reference is by a node at */
00270   /* level n. */
00271   /* The strategy will be to start with the number of subfunctions */
00272   /* whose top variable has index n.  We compute the highest level at */
00273   /* which each subfunction is referenced.  Then we work bottom up; at */
00274   /* level n we add in the result from level n+1 and subtract the */
00275   /* number of subfunctions whose highest reference is at level n. */
00276 
00277   Cal_BddProfile(bddManager, fUserBdd, funcCounts, 0);
00278   if(CalBddPreProcessing(bddManager, 1, fUserBdd)){
00279     f = CalBddGetInternalBdd(bddManager, fUserBdd);
00280     /* Encode the profile.  The low bit of a count will be zero for */
00281     /* those levels where f actually has a node. */
00282     for(j = 0; j < bddManager->numVars; ++j){
00283       if(!funcCounts[j]){
00284         funcCounts[j] = 1;
00285       }
00286       else{
00287         funcCounts[j] <<= 1;
00288       }
00289     }
00290     h = CalHashTableOneInit(bddManager, sizeof(int));
00291     /* For each subfunction in f, compute the highest level where it is */
00292     /* referenced.  f itself is conceptually referenced at the highest */
00293     /* possible level, which we represent by -1. */
00294     i =  -1;
00295     CalHashTableOneInsert(h, f, (char *)&i);
00296     BddHighestRefStep(bddManager, f, h);
00297     /* Walk through these results.  For each subfunction, decrement the */
00298     /* count at the highest level where it is referenced. */
00299     BddDominatedStep(bddManager, f, funcCounts, h);
00300     CalHashTableOneQuit(h);
00301     /* Now add each level n+1 result to that of level n. */
00302     for(i = bddManager->numVars-1, j = i+1; i>=  0; --i){
00303       if(funcCounts[i] !=  1){
00304         funcCounts[i] = (funcCounts[i] >> 1) + funcCounts[j];
00305         j = i;
00306       }
00307       else{
00308           funcCounts[i] = 0;
00309       }
00310     }
00311   }
00312 }
00313 
00325 void
00326 Cal_BddFunctionProfileMultiple(Cal_BddManager bddManager, Cal_Bdd
00327                                *fUserBddArray, long * funcCounts)
00328 {
00329   long i;
00330   Cal_BddIndex_t j;
00331   Cal_Bdd_t *f, *fArray;
00332   CalHashTable_t *h;
00333 
00334   CalBddArrayPreProcessing(bddManager, fUserBddArray);
00335 
00336   for(i = 0; fUserBddArray[i]; ++i);
00337 
00338   fArray = Cal_MemAlloc(Cal_Bdd_t, i+1);
00339   for (j=0; j < i; j++){
00340     fArray[j] = CalBddGetInternalBdd(bddManager,fUserBddArray[j]);
00341   }
00342   fArray[j] = bddManager->bddNull;
00343 
00344   /* See cmu_bdd_function_profile for the strategy involved here. */
00345   Cal_BddProfileMultiple(bddManager, fUserBddArray, funcCounts, 0);
00346   for(j = 0; j < bddManager->numVars; ++j){
00347     if(!funcCounts[j]){
00348       funcCounts[j] = 1;
00349     }
00350     else{
00351       funcCounts[j] <<= 1;
00352     }
00353   }
00354   h = CalHashTableOneInit(bddManager, sizeof(int));
00355   for(f = fArray; !CalBddIsBddNull(bddManager, *f); ++f){
00356     BddHighestRefStep(bddManager, *f, h);
00357   }
00358   i = -1;
00359   for(f = fArray; !CalBddIsBddNull(bddManager, *f); ++f){
00360     CalHashTableOneInsert(h, *f, (char *)&i);
00361   }
00362   for(f = fArray; !CalBddIsBddNull(bddManager, *f); ++f){
00363     BddDominatedStep(bddManager, *f, funcCounts, h);
00364   }
00365   CalHashTableOneQuit(h);
00366   for(i = bddManager->numVars-1, j = i+1; i >=  0; --i){
00367     if(funcCounts[i] !=  1){
00368       funcCounts[i] = (funcCounts[i] >> 1) + funcCounts[j];
00369       j = i;
00370     }
00371     else{
00372       funcCounts[i] = 0;
00373     }
00374   }
00375   Cal_MemFree(fArray);
00376 }
00377 
00378 /*---------------------------------------------------------------------------*/
00379 /* Definition of internal functions                                          */
00380 /*---------------------------------------------------------------------------*/
00381 
00382 /*---------------------------------------------------------------------------*/
00383 /* Definition of static functions                                            */
00384 /*---------------------------------------------------------------------------*/
00385 
00386 
00398 static void
00399 BddMarkBdd(Cal_Bdd_t  f)
00400 {
00401   int currMarking, thisMarking;
00402   Cal_Bdd_t thenBdd, elseBdd;
00403 
00404   currMarking = CalBddGetMark(f);
00405   thisMarking = (1 << CalBddIsComplement(f));
00406   if(currMarking & thisMarking){
00407     return;
00408   }
00409   CalBddPutMark(f, currMarking | thisMarking);
00410   if(CalBddIsBddConst(f)){
00411     return;
00412   }
00413   CalBddGetThenBdd(f, thenBdd);
00414   BddMarkBdd(thenBdd);
00415   CalBddGetElseBdd(f, elseBdd);
00416   BddMarkBdd(elseBdd);
00417 }
00418 
00419 
00431 static int
00432 BddCountNoNodes(
00433   Cal_Bdd_t  f)
00434 {
00435   return (CalBddGetMark(f) > 0);
00436 }
00437 
00438 
00450 static int
00451 BddCountNodes(
00452   Cal_Bdd_t  f)
00453 {
00454   int mark;
00455 
00456   mark = CalBddGetMark(f);
00457   return (((mark & 0x1) !=  0) + ((mark & 0x2) !=  0));
00458 }
00459 
00460 
00461 
00473 static long
00474 BddSizeStep(
00475   Cal_Bdd_t  f,
00476   CountFn_t countFn)
00477 {
00478   long result;
00479   Cal_Bdd_t thenBdd, elseBdd;
00480 
00481   if(!CalBddGetMark(f)){
00482     return (0l);
00483   }
00484   result = (*countFn)(f);
00485   if(!CalBddIsBddConst(f)){
00486     CalBddGetThenBdd(f, thenBdd);
00487     CalBddGetElseBdd(f, elseBdd);
00488     result +=
00489         BddSizeStep(thenBdd, countFn) +
00490         BddSizeStep(elseBdd, countFn);
00491   }
00492   CalBddPutMark(f, 0);
00493   return result;
00494 }
00495 
00496 
00497 
00509 static void
00510 BddProfileStep(
00511   Cal_BddManager_t * bddManager,
00512   Cal_Bdd_t  f,
00513   long * levelCounts,
00514   CountFn_t countFn)
00515 {
00516   Cal_Bdd_t thenBdd, elseBdd;
00517   if(!CalBddGetMark(f)){
00518     return;
00519   }
00520   if(CalBddIsBddConst(f)){
00521     levelCounts[bddManager->numVars] += (*countFn)(f);
00522   }
00523   else{
00524     levelCounts[CalBddGetBddIndex(bddManager, f)] += (*countFn)(f);
00525     CalBddGetThenBdd(f, thenBdd);
00526     BddProfileStep(bddManager, thenBdd, levelCounts, countFn);
00527     CalBddGetElseBdd(f, elseBdd);
00528     BddProfileStep(bddManager, elseBdd, levelCounts, countFn);
00529   }
00530   CalBddPutMark(f, 0);
00531 }
00532 
00533 
00534 
00546 static void
00547 BddHighestRefStep(
00548   Cal_BddManager_t * bddManager,
00549   Cal_Bdd_t  f,
00550   CalHashTable_t * h)
00551 {
00552   int fIndex;
00553   Cal_Bdd_t keyBdd;
00554   int *dataPtr;
00555 
00556   if(CalBddIsBddConst(f)){
00557     return;
00558   }
00559   fIndex = CalBddGetBddIndex(bddManager, f);
00560   CalBddGetThenBdd(f, keyBdd);
00561   if(CalHashTableOneLookup(h, keyBdd, (char **)&dataPtr)){
00562     if(*dataPtr > fIndex){
00563       *dataPtr = fIndex;
00564     }
00565   }
00566   else{
00567     CalHashTableOneInsert(h, keyBdd, (char *)&fIndex);
00568     BddHighestRefStep(bddManager, keyBdd, h);
00569   }
00570   CalBddGetElseBdd(f, keyBdd);
00571   if(CalHashTableOneLookup(h, keyBdd, (char **)&dataPtr)){
00572     if(*dataPtr > fIndex){
00573       *dataPtr = fIndex;
00574     }
00575   }
00576   else{
00577     CalHashTableOneInsert(h, keyBdd, (char *)&fIndex);
00578     BddHighestRefStep(bddManager, keyBdd, h);
00579   }
00580 }
00581 
00593 static void
00594 BddDominatedStep(
00595   Cal_BddManager_t * bddManager,
00596   Cal_Bdd_t  f,
00597   long * funcCounts,
00598   CalHashTable_t * h)
00599 {
00600   Cal_Bdd_t thenBdd, elseBdd;
00601   int *dataPtr;
00602 
00603   CalHashTableOneLookup(h, f, (char **)&dataPtr);
00604   if(*dataPtr >=  0)
00605     funcCounts[*dataPtr] -= 2;
00606   if(*dataPtr > -2){
00607     *dataPtr = -2;
00608     if(!CalBddIsBddConst(f)){
00609       CalBddGetThenBdd(f, thenBdd);
00610       BddDominatedStep(bddManager, thenBdd, funcCounts, h);
00611       CalBddGetElseBdd(f, elseBdd);
00612       BddDominatedStep(bddManager, elseBdd, funcCounts, h);
00613     }
00614   }
00615 }
00616 
00617 
00618 
00619 
00620 
00621 
00622 
00623 
00624