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

00001 
00041 #include "calInt.h"
00042 
00043 /*---------------------------------------------------------------------------*/
00044 /* Constant declarations                                                     */
00045 /*---------------------------------------------------------------------------*/
00046 #define MAGIC_COOKIE 0x5e02f795l
00047 #define CAL_BDD_IOERROR 100
00048 
00049 #define TRUE_ENCODING 0xffffff00l
00050 #define FALSE_ENCODING 0xffffff01l
00051 #define POSVAR_ENCODING 0xffffff02l
00052 #define NEGVAR_ENCODING 0xffffff03l
00053 #define POSNODE_ENCODING 0xffffff04l
00054 #define NEGNODE_ENCODING 0xffffff05l
00055 #define NODELABEL_ENCODING 0xffffff06l
00056 #define CONSTANT_ENCODING 0xffffff07l
00057 
00058 /*---------------------------------------------------------------------------*/
00059 /* Type declarations                                                         */
00060 /*---------------------------------------------------------------------------*/
00061 
00062 /*---------------------------------------------------------------------------*/
00063 /* Stucture declarations                                                     */
00064 /*---------------------------------------------------------------------------*/
00065 
00066 /*---------------------------------------------------------------------------*/
00067 /* Variable declarations                                                     */
00068 /*---------------------------------------------------------------------------*/
00069 
00070 
00071 static long indexMask[] = {0xffl, 0xffffl, 0xffffffl};
00072 
00073 /*---------------------------------------------------------------------------*/
00074 /* Macro declarations                                                        */
00075 /*---------------------------------------------------------------------------*/
00076 
00077 
00080 /*---------------------------------------------------------------------------*/
00081 /* Static function prototypes                                                */
00082 /*---------------------------------------------------------------------------*/
00083 
00084 static void Write(Cal_BddManager_t * bddManager, unsigned long n, int bytes, FILE * fp);
00085 static void BddDumpBddStep(Cal_BddManager_t * bddManager, Cal_Bdd_t f, FILE * fp, CalHashTable_t * h, Cal_BddIndex_t * normalizedIndexes, int indexSize, int nodeNumberSize);
00086 static unsigned long Read(int * error, int bytes, FILE * fp);
00087 static Cal_Bdd_t BddUndumpBddStep(Cal_BddManager_t * bddManager, Cal_Bdd_t * vars, FILE * fp, Cal_BddIndex_t numberVars, Cal_Bdd_t * shared, long numberShared, long * sharedSoFar, int indexSize, int nodeNumberSize, int * error);
00088 static int BytesNeeded(long n);
00089 
00092 /*---------------------------------------------------------------------------*/
00093 /* Definition of exported functions                                          */
00094 /*---------------------------------------------------------------------------*/
00120 Cal_Bdd
00121 Cal_BddUndumpBdd(
00122   Cal_BddManager bddManager,
00123   Cal_Bdd * userVars,
00124   FILE * fp,
00125   int * error)
00126 {
00127   long i,j;
00128   Cal_BddIndex_t numberVars;
00129   long numberShared;
00130   int indexSize;
00131   int nodeNumberSize;
00132   Cal_Bdd_t *shared;
00133   long sharedSoFar;
00134   Cal_Bdd_t v;
00135   Cal_Bdd_t result;
00136   Cal_Bdd_t *vars;
00137 
00138   *error = 0;
00139   for(i = 0; userVars[i]; ++i){
00140     if(Cal_BddType(bddManager, userVars[i]) !=  CAL_BDD_TYPE_POSVAR){
00141       CalBddWarningMessage("Cal_BddUndumpBdd: support is not all positive variables"); 
00142       return (Cal_Bdd) 0;
00143     }
00144   }
00145   vars = Cal_MemAlloc(Cal_Bdd_t, i);
00146   for (j=0; j < i; j++){
00147     vars[j] = CalBddGetInternalBdd(bddManager,userVars[j]);
00148   }
00149 
00150   if(Read(error, sizeof(long), fp) !=  MAGIC_COOKIE){
00151     if(!*error){
00152       *error = CAL_BDD_UNDUMP_FORMAT;
00153     }
00154     Cal_MemFree(vars);
00155     return (Cal_Bdd) 0;
00156   }
00157   numberVars = Read(error, sizeof(Cal_BddIndex_t), fp);
00158   if(*error){
00159     Cal_MemFree(vars);
00160     return (Cal_Bdd) 0;
00161   }
00162   if(numberVars !=  i){
00163     *error = CAL_BDD_UNDUMP_FORMAT;
00164     Cal_MemFree(vars);
00165     return (Cal_Bdd) 0;
00166   }
00167   numberShared = Read(error, sizeof(long), fp);
00168   if(*error){
00169     Cal_MemFree(vars);
00170     return (Cal_Bdd) 0;
00171   }
00172   indexSize = BytesNeeded(numberVars+1);
00173   nodeNumberSize = BytesNeeded(numberShared);
00174   if(numberShared < 0){
00175     *error = CAL_BDD_UNDUMP_FORMAT;
00176     Cal_MemFree(vars);
00177     return (Cal_Bdd) 0;
00178   }
00179   shared = Cal_MemAlloc(Cal_Bdd_t, numberShared);
00180   for(i = 0; i < numberShared; ++i){
00181     shared[i] = CalBddNull(bddManager);
00182   }
00183   sharedSoFar = 0;
00184   result = BddUndumpBddStep(bddManager, vars, fp, numberVars, shared,
00185       numberShared, &sharedSoFar, indexSize, nodeNumberSize, error);
00186   Cal_MemFree(vars);
00187   
00188   for(i = 0; i < numberShared; ++i){
00189     v = shared[i];
00190     if(!CalBddIsBddNull(bddManager, v)){
00191       CalBddFree(v);
00192     }
00193   }
00194   if(!*error && sharedSoFar !=  numberShared){
00195     *error = CAL_BDD_UNDUMP_FORMAT;
00196   }
00197   Cal_MemFree(shared);
00198   if(*error){
00199     if(!CalBddIsBddNull(bddManager, result)){
00200       CalBddFree(result);
00201     }
00202     return (Cal_Bdd) 0;
00203   }
00204   /*
00205    * Decrement the reference count of result by 1. Since it has
00206    * already been incremented in BddUndumpBddStep.
00207    */
00208   CalBddDcrRefCount(result);
00209   return CalBddGetExternalBdd(bddManager, result);
00210 }
00211 
00212 
00228 int
00229 Cal_BddDumpBdd(
00230   Cal_BddManager bddManager,
00231   Cal_Bdd  fUserBdd,
00232   Cal_Bdd * userVars,
00233   FILE * fp)
00234 {
00235   long i;
00236   Cal_BddIndex_t *normalizedIndexes;
00237   Cal_BddIndex_t vIndex;
00238   Cal_Bdd_t f;
00239   Cal_BddIndex_t numberVars;
00240   Cal_Bdd *support;
00241   int ok;
00242   CalHashTable_t *h;
00243   int indexSize;
00244   long next;
00245   int nodeNumberSize;
00246 
00247   if(CalBddPreProcessing(bddManager, 1, fUserBdd)){
00248     f = CalBddGetInternalBdd(bddManager, fUserBdd);
00249     for(i = 0; userVars[i]; ++i){
00250       if(Cal_BddType(bddManager, userVars[i]) !=  CAL_BDD_TYPE_POSVAR){
00251         CalBddWarningMessage("Cal_BddDumpBdd: support is not all positive variables");
00252         return (0);
00253       }
00254     }
00255     normalizedIndexes = Cal_MemAlloc(Cal_BddIndex_t, bddManager->numVars);
00256     for(i = 0; i < bddManager->numVars; ++i){
00257       normalizedIndexes[i] = CAL_BDD_CONST_INDEX;
00258     }
00259     for(i = 0; userVars[i]; ++i){
00260       vIndex = Cal_BddGetIfIndex(bddManager, userVars[i]);
00261       if(normalizedIndexes[vIndex] !=  CAL_BDD_CONST_INDEX){
00262         CalBddWarningMessage("Cal_BddDumpBdd: variables duplicated in support");
00263         Cal_MemFree(normalizedIndexes);
00264         return 0;
00265       }
00266       normalizedIndexes[vIndex] = i;
00267     }
00268     numberVars = i;
00269     support = Cal_MemAlloc(Cal_Bdd, bddManager->numVars+1);
00270     Cal_BddSupport(bddManager, fUserBdd, support);
00271     ok = 1;
00272     for(i = 0; ok && support[i]; ++i){
00273       if(normalizedIndexes[Cal_BddGetIfIndex(bddManager, support[i])] == CAL_BDD_CONST_INDEX){
00274         CalBddWarningMessage("Cal_BddDumpBdd: incomplete support specified");
00275         ok = 0;
00276       }
00277     }
00278     if(!ok){
00279       Cal_MemFree(normalizedIndexes);
00280       Cal_MemFree(support);
00281       return 0;
00282     }
00283     Cal_MemFree(support);
00284     /* Everything checked now; barring I/O errors, we should be able to */
00285     /* Write a valid output file. */
00286     f = CalBddGetInternalBdd(bddManager, fUserBdd);
00287     h = CalHashTableOneInit(bddManager, sizeof(long));
00288     indexSize = BytesNeeded(numberVars+1);
00289     CalBddMarkSharedNodes(bddManager, f);
00290     next = 0;
00291     CalBddNumberSharedNodes(bddManager, f, h, &next);
00292     nodeNumberSize = BytesNeeded(next);
00293     Write(bddManager, MAGIC_COOKIE, sizeof(long), fp);
00294     Write(bddManager, (unsigned long)numberVars, sizeof(Cal_BddIndex_t), fp);
00295     Write(bddManager, (unsigned long)next, sizeof(long), fp);
00296     BddDumpBddStep(bddManager, f, fp, h, normalizedIndexes, indexSize, nodeNumberSize);
00297     CalHashTableOneQuit(h);
00298     Cal_MemFree(normalizedIndexes);
00299     return (1);
00300   }
00301   return (0);
00302 }
00303 
00315 static void
00316 Write(
00317   Cal_BddManager_t * bddManager,
00318   unsigned long  n,
00319   int  bytes,
00320   FILE * fp)
00321 {
00322   while(bytes){
00323     if(fputc((char)(n >> (8*(bytes-1)) & 0xff), fp) == EOF){
00324     }
00325     --bytes;
00326   }
00327 }
00328 
00329 
00341 static void
00342 BddDumpBddStep(
00343   Cal_BddManager_t * bddManager,
00344   Cal_Bdd_t  f,
00345   FILE * fp,
00346   CalHashTable_t * h,
00347   Cal_BddIndex_t * normalizedIndexes,
00348   int  indexSize,
00349   int  nodeNumberSize)
00350 {
00351   int negated;
00352   long *number;
00353   Cal_Bdd_t thenBdd, elseBdd;
00354 
00355   switch(CalBddTypeAux(bddManager, f)){
00356   case CAL_BDD_TYPE_ZERO:
00357     Write(bddManager, FALSE_ENCODING, indexSize+1, fp);
00358     break;
00359   case CAL_BDD_TYPE_ONE:
00360     Write(bddManager, TRUE_ENCODING, indexSize+1, fp);
00361     break;
00362   case CAL_BDD_TYPE_CONSTANT:
00363     Write(bddManager, CONSTANT_ENCODING, indexSize+1, fp);
00364 #ifdef JAGESH
00365     Write(bddManager, (unsigned long)BDD_DATA(f)[0], sizeof(long), fp);
00366     Write(bddManager, (unsigned long)BDD_DATA(f)[1], sizeof(long), fp);
00367 #endif
00368     break;
00369   case CAL_BDD_TYPE_POSVAR:
00370     Write(bddManager, POSVAR_ENCODING, indexSize+1, fp);
00371     Write(bddManager,
00372         (unsigned long)normalizedIndexes[CalBddGetBddIndex(bddManager, f)],
00373         indexSize, fp);
00374     break;
00375   case CAL_BDD_TYPE_NEGVAR:
00376     Write(bddManager, NEGVAR_ENCODING, indexSize+1, fp);
00377     Write(bddManager, 
00378         (unsigned long)normalizedIndexes[CalBddGetBddIndex(bddManager, f)],
00379         indexSize, fp);
00380     break;
00381   case CAL_BDD_TYPE_NONTERMINAL:
00382     CalBddNot(f, f);
00383     if(CalHashTableOneLookup(h, f, (char **)0)){
00384       negated  =  1;
00385     }
00386     else{
00387       CalBddNot(f, f);
00388       negated = 0;
00389     }
00390     CalHashTableOneLookup(h, f, (char **)&number);
00391     if(number && *number < 0){
00392           if(negated)
00393             Write(bddManager, NEGNODE_ENCODING, indexSize+1, fp);
00394           else
00395             Write(bddManager, POSNODE_ENCODING, indexSize+1, fp);
00396           Write(bddManager, (unsigned long)(-*number-1), nodeNumberSize, fp);
00397     }
00398     else{
00399       if(number){
00400               Write(bddManager, NODELABEL_ENCODING, indexSize+1, fp);
00401               *number =  -*number-1;
00402       }
00403       Write(bddManager,
00404           (unsigned long)normalizedIndexes[CalBddGetBddIndex(bddManager, f)],
00405           indexSize, fp);
00406       CalBddGetThenBdd(f, thenBdd);
00407       BddDumpBddStep(bddManager, thenBdd, fp, h, normalizedIndexes,
00408           indexSize, nodeNumberSize);
00409       CalBddGetElseBdd(f, elseBdd);
00410       BddDumpBddStep(bddManager, elseBdd, fp, h, normalizedIndexes,
00411           indexSize, nodeNumberSize);
00412     }
00413     break;
00414   default:
00415     CalBddFatalMessage("BddDumpBddStep: unknown type returned by CalBddType");
00416   }
00417 }
00418 
00419 
00420 
00432 static unsigned long
00433 Read(
00434   int * error,
00435   int  bytes,
00436   FILE * fp)
00437 {
00438   int c;
00439   long result;
00440 
00441   result = 0;
00442   if(*error){
00443     return (result);
00444   }
00445   while(bytes){
00446     c = fgetc(fp);
00447     if(c == EOF){
00448       if(ferror(fp)){
00449         *error = CAL_BDD_UNDUMP_IOERROR;
00450       }
00451       else{
00452         *error = CAL_BDD_UNDUMP_EOF;
00453       }
00454       return (0l);
00455     }
00456     result = (result << 8)+c;
00457     --bytes;
00458   } 
00459   return (result);
00460 }
00461 
00462 
00463 
00464 
00476 static Cal_Bdd_t
00477 BddUndumpBddStep(
00478   Cal_BddManager_t * bddManager,
00479   Cal_Bdd_t * vars,
00480   FILE * fp,
00481   Cal_BddIndex_t  numberVars,
00482   Cal_Bdd_t * shared,
00483   long  numberShared,
00484   long * sharedSoFar,
00485   int  indexSize,
00486   int  nodeNumberSize,
00487   int * error)
00488 {
00489   long nodeNumber;
00490   long encoding;
00491   Cal_BddIndex_t i;
00492   CalAddress_t value1, value2;
00493   Cal_Bdd_t v;
00494   Cal_Bdd_t temp1, temp2;
00495   Cal_Bdd_t result;
00496 
00497   i = Read(error, indexSize, fp);
00498   if(*error){
00499     return CalBddNull(bddManager);
00500   }
00501   if(i == indexMask[indexSize-1]){
00502     encoding = 0xffffff00l+Read(error, 1, fp);
00503     if(*error){
00504       return CalBddNull(bddManager);
00505     }
00506     switch(encoding){
00507     case TRUE_ENCODING:
00508       return (CalBddOne(bddManager));
00509     case FALSE_ENCODING:
00510       return (CalBddZero(bddManager));
00511     case CONSTANT_ENCODING:
00512       value1 = Read(error, sizeof(long), fp);
00513       value2 = Read(error, sizeof(long), fp);
00514       if(*error){
00515         return CalBddNull(bddManager);
00516       }
00517       *error = CAL_BDD_UNDUMP_OVERFLOW;
00518       return CalBddNull(bddManager);
00519     case POSVAR_ENCODING:
00520     case NEGVAR_ENCODING:
00521       i = Read(error, indexSize, fp);
00522       if(!*error && i >=  numberVars){
00523         *error = CAL_BDD_UNDUMP_FORMAT;
00524       }
00525       if(*error){
00526         return CalBddNull(bddManager);
00527       }
00528       v = vars[i];
00529       if(encoding == POSVAR_ENCODING){
00530         return (v);
00531       }
00532       else{
00533         CalBddNot(v, v);
00534         return (v);
00535       }
00536     case POSNODE_ENCODING:
00537     case NEGNODE_ENCODING:
00538       nodeNumber = Read(error, nodeNumberSize, fp);
00539       if(!*error && (nodeNumber >=  numberShared ||
00540           CalBddIsBddNull(bddManager, shared[nodeNumber]))){
00541         *error = CAL_BDD_UNDUMP_FORMAT;
00542       }
00543       if(*error){
00544         return CalBddNull(bddManager);
00545       }
00546       v = shared[nodeNumber];
00547       v = CalBddIdentity(bddManager, v);
00548       if(encoding == POSNODE_ENCODING){
00549         return (v);
00550       }
00551       else{
00552         CalBddNot(v, v);
00553         return (v);
00554       }
00555     case NODELABEL_ENCODING:
00556       nodeNumber =  *sharedSoFar;
00557       ++*sharedSoFar;
00558       v = BddUndumpBddStep(bddManager, vars, fp, numberVars, shared,
00559           numberShared, sharedSoFar, indexSize, nodeNumberSize, error);
00560       shared[nodeNumber] = v;
00561       v = CalBddIdentity(bddManager, v);
00562       return (v);
00563     default:
00564       *error = CAL_BDD_UNDUMP_FORMAT;
00565       return CalBddNull(bddManager);
00566     }
00567   }
00568   if(i >= numberVars){
00569     *error = CAL_BDD_UNDUMP_FORMAT;
00570     return CalBddNull(bddManager);
00571   }
00572   temp1 = BddUndumpBddStep(bddManager, vars, fp, numberVars, shared,
00573        numberShared, sharedSoFar, indexSize, nodeNumberSize, error);
00574   temp2 = BddUndumpBddStep(bddManager, vars, fp, numberVars, shared,
00575        numberShared, sharedSoFar, indexSize, nodeNumberSize, error);
00576   if(*error){
00577       CalBddFree(temp1);
00578       return CalBddNull(bddManager);
00579   }
00580   result = CalBddITE(bddManager, vars[i], temp1, temp2);
00581   CalBddFree(temp1);
00582   CalBddFree(temp2);
00583   if(CalBddIsBddNull(bddManager, result)){
00584      *error = CAL_BDD_UNDUMP_OVERFLOW;
00585   }
00586   return (result);
00587 }
00588 
00589 
00590 
00602 static int
00603 BytesNeeded(
00604   long  n)
00605 {
00606   if(n <= 0x100l){
00607     return (1);
00608   }
00609   if(n <= 0x10000l){
00610     return (2);
00611   }
00612   if(n <= 0x1000000l){
00613     return (3);
00614   }
00615   return (4);
00616 }
00617 
00618 
00619 
00620 
00621 
00622 
00623 
00624 
00625 
00626 
00627 
00628