glu-2.2: src/cmuBdd/bdddump.c Source File

00001 /* BDD library dump/undump routines */
00002 
00003 
00004 #include "bddint.h"
00005 
00006 
00007 #define MAGIC_COOKIE 0x5e02f795l
00008 #define BDD_IOERROR 100
00009 
00010 
00011 #define TRUE_ENCODING 0xffffff00l
00012 #define FALSE_ENCODING 0xffffff01l
00013 #define POSVAR_ENCODING 0xffffff02l
00014 #define NEGVAR_ENCODING 0xffffff03l
00015 #define POSNODE_ENCODING 0xffffff04l
00016 #define NEGNODE_ENCODING 0xffffff05l
00017 #define NODELABEL_ENCODING 0xffffff06l
00018 #define CONSTANT_ENCODING 0xffffff07l
00019 
00020 
00021 static
00022 int
00023 bytes_needed(long n)
00024 {
00025   if (n <= 0x100l)
00026     return (1);
00027   if (n <= 0x10000l)
00028     return (2);
00029   if (n <= 0x1000000l)
00030     return (3);
00031   return (4);
00032 }
00033 
00034 
00035 static
00036 void
00037 write(cmu_bdd_manager bddm, unsigned long n, int bytes, FILE *fp)
00038 {
00039   while (bytes)
00040     {
00041       if (fputc((char)(n >> (8*(bytes-1)) & 0xff), fp) == EOF)
00042         longjmp(bddm->abort.context, BDD_IOERROR);
00043       --bytes;
00044     }
00045 }
00046 
00047 
00048 static
00049 void
00050 cmu_bdd_dump_bdd_step(cmu_bdd_manager bddm,
00051                   bdd f,
00052                   FILE *fp,
00053                   hash_table h,
00054                   bdd_index_type *normalized_indexes,
00055                   int index_size,
00056                   int node_number_size)
00057 {
00058   int negated;
00059   long *number;
00060 
00061   BDD_SETUP(f);
00062   switch (cmu_bdd_type_aux(bddm, f))
00063     {
00064     case BDD_TYPE_ZERO:
00065       write(bddm, FALSE_ENCODING, index_size+1, fp);
00066       break;
00067     case BDD_TYPE_ONE:
00068       write(bddm, TRUE_ENCODING, index_size+1, fp);
00069       break;
00070     case BDD_TYPE_CONSTANT:
00071       write(bddm, CONSTANT_ENCODING, index_size+1, fp);
00072       write(bddm, (unsigned long)BDD_DATA(f)[0], sizeof(long), fp);
00073       write(bddm, (unsigned long)BDD_DATA(f)[1], sizeof(long), fp);
00074       break;
00075     case BDD_TYPE_POSVAR:
00076       write(bddm, POSVAR_ENCODING, index_size+1, fp);
00077       write(bddm, (unsigned long)normalized_indexes[BDD_INDEX(bddm, f)], index_size, fp);
00078       break;
00079     case BDD_TYPE_NEGVAR:
00080       write(bddm, NEGVAR_ENCODING, index_size+1, fp);
00081       write(bddm, (unsigned long)normalized_indexes[BDD_INDEX(bddm, f)], index_size, fp);
00082       break;
00083     case BDD_TYPE_NONTERMINAL:
00084       if (bdd_lookup_in_hash_table(h, BDD_NOT(f)))
00085         {
00086           f=BDD_NOT(f);
00087           negated=1;
00088         }
00089       else
00090         negated=0;
00091       number=(long *)bdd_lookup_in_hash_table(h, f);
00092       if (number && *number < 0)
00093         {
00094           if (negated)
00095             write(bddm, NEGNODE_ENCODING, index_size+1, fp);
00096           else
00097             write(bddm, POSNODE_ENCODING, index_size+1, fp);
00098           write(bddm, (unsigned long)(-*number-1), node_number_size, fp);
00099         }
00100       else
00101         {
00102           if (number)
00103             {
00104               write(bddm, NODELABEL_ENCODING, index_size+1, fp);
00105               *number= -*number-1;
00106             }
00107           write(bddm, (unsigned long)normalized_indexes[BDD_INDEX(bddm, f)], index_size, fp);
00108           cmu_bdd_dump_bdd_step(bddm, BDD_THEN(f), fp, h, normalized_indexes, index_size, node_number_size);
00109           cmu_bdd_dump_bdd_step(bddm, BDD_ELSE(f), fp, h, normalized_indexes, index_size, node_number_size);
00110         }
00111       break;
00112     default:
00113       cmu_bdd_fatal("cmu_bdd_dump_bdd_step: unknown type returned by cmu_bdd_type");
00114     }
00115 }
00116 
00117 
00118 int
00119 cmu_bdd_dump_bdd(cmu_bdd_manager bddm, bdd f, bdd *vars, FILE *fp)
00120 {
00121   long i;
00122   bdd_index_type *normalized_indexes;
00123   bdd_index_type v_index;
00124   bdd var;
00125   bdd_index_type number_vars;
00126   bdd *support;
00127   int ok;
00128   hash_table h;
00129   int index_size;
00130   long next;
00131   int node_number_size;
00132 
00133   if (bdd_check_arguments(1, f))
00134     {
00135       for (i=0; vars[i]; ++i)
00136         if (cmu_bdd_type(bddm, vars[i]) != BDD_TYPE_POSVAR)
00137           {
00138             cmu_bdd_warning("cmu_bdd_dump_bdd: support is not all positive variables");
00139             return (0);
00140           }
00141       normalized_indexes=(bdd_index_type *)mem_get_block((SIZE_T)(bddm->vars*sizeof(bdd_index_type)));
00142       for (i=0; i < bddm->vars; ++i)
00143         normalized_indexes[i]=BDD_MAX_INDEX;
00144       for (i=0; (var=vars[i]); ++i)
00145         {
00146           BDD_SETUP(var);
00147           v_index=BDD_INDEX(bddm, var);
00148           if (normalized_indexes[v_index] != BDD_MAX_INDEX)
00149             {
00150               cmu_bdd_warning("cmu_bdd_dump_bdd: variables duplicated in support");
00151               mem_free_block((pointer)normalized_indexes);
00152               return (0);
00153             }
00154           normalized_indexes[v_index]=i;
00155         }
00156       number_vars=i;
00157       support=(bdd *)mem_get_block((SIZE_T)((bddm->vars+1)*sizeof(bdd)));
00158       cmu_bdd_support(bddm, f, support);
00159       ok=1;
00160       for (i=0; ok && (var=support[i]); ++i)
00161         {
00162           BDD_SETUP(var);
00163           if (normalized_indexes[BDD_INDEX(bddm, var)] == BDD_MAX_INDEX)
00164             {
00165               cmu_bdd_warning("cmu_bdd_dump_bdd: incomplete support specified");
00166               ok=0;
00167             }
00168         }
00169       if (!ok)
00170         {
00171           mem_free_block((pointer)normalized_indexes);
00172           mem_free_block((pointer)support);
00173           return (0);
00174         }
00175       mem_free_block((pointer)support);
00176       /* Everything checked now; barring I/O errors, we should be able to */
00177       /* write a valid output file. */
00178       h=bdd_new_hash_table(bddm, sizeof(long));
00179       FIREWALL1(bddm,
00180                 if (retcode == BDD_IOERROR)
00181                   {
00182                     cmu_bdd_free_hash_table(h);
00183                     mem_free_block((pointer)normalized_indexes);
00184                     return (0);
00185                   }
00186                 else
00187                   cmu_bdd_fatal("cmu_bdd_dump_bdd: got unexpected retcode");
00188                 );
00189       index_size=bytes_needed(number_vars+1);
00190       bdd_mark_shared_nodes(bddm, f);
00191       next=0;
00192       bdd_number_shared_nodes(bddm, f, h, &next);
00193       node_number_size=bytes_needed(next);
00194       write(bddm, MAGIC_COOKIE, sizeof(long), fp);
00195       write(bddm, (unsigned long)number_vars, sizeof(bdd_index_type), fp);
00196       write(bddm, (unsigned long)next, sizeof(long), fp);
00197       cmu_bdd_dump_bdd_step(bddm, f, fp, h, normalized_indexes, index_size, node_number_size);
00198       cmu_bdd_free_hash_table(h);
00199       mem_free_block((pointer)normalized_indexes);
00200       return (1);
00201     }
00202   return (0);
00203 }
00204 
00205 
00206 static
00207 unsigned long
00208 read(int *error, int bytes, FILE *fp)
00209 {
00210   int c;
00211   long result;
00212 
00213   result=0;
00214   if (*error)
00215     return (result);
00216   while (bytes)
00217     {
00218       c=fgetc(fp);
00219       if (c == EOF)
00220         {
00221           if (ferror(fp))
00222             *error=BDD_UNDUMP_IOERROR;
00223           else
00224             *error=BDD_UNDUMP_EOF;
00225           return (0l);
00226         }
00227       result=(result << 8)+c;
00228       --bytes;
00229     }
00230   return (result);
00231 }
00232 
00233 
00234 static long index_mask[]={0xffl, 0xffffl, 0xffffffl};
00235 
00236 
00237 static
00238 bdd
00239 cmu_bdd_undump_bdd_step(cmu_bdd_manager bddm,
00240                     bdd *vars,
00241                     FILE *fp,
00242                     bdd_index_type number_vars,
00243                     bdd *shared,
00244                     long number_shared,
00245                     long *shared_so_far,
00246                     int index_size,
00247                     int node_number_size,
00248                     int *error)
00249 {
00250   long node_number;
00251   long encoding;
00252   bdd_index_type i;
00253   INT_PTR value1, value2;
00254   bdd v;
00255   bdd temp1, temp2;
00256   bdd result;
00257 
00258   i=read(error, index_size, fp);
00259   if (*error)
00260     return ((bdd)0);
00261   if (i == index_mask[index_size-1])
00262     {
00263       encoding=0xffffff00l+read(error, 1, fp);
00264       if (*error)
00265         return ((bdd)0);
00266       switch (encoding)
00267         {
00268         case TRUE_ENCODING:
00269           return (BDD_ONE(bddm));
00270         case FALSE_ENCODING:
00271           return (BDD_ZERO(bddm));
00272         case CONSTANT_ENCODING:
00273           value1=read(error, sizeof(long), fp);
00274           value2=read(error, sizeof(long), fp);
00275           if (*error)
00276             return ((bdd)0);
00277           if ((result=cmu_mtbdd_get_terminal(bddm, value1, value2)))
00278             return (result);
00279           *error=BDD_UNDUMP_OVERFLOW;
00280           return ((bdd)0);
00281         case POSVAR_ENCODING:
00282         case NEGVAR_ENCODING:
00283           i=read(error, index_size, fp);
00284           if (!*error && i >= number_vars)
00285             *error=BDD_UNDUMP_FORMAT;
00286           if (*error)
00287             return ((bdd)0);
00288           v=vars[i];
00289           if (encoding == POSVAR_ENCODING)
00290             return (v);
00291           else
00292             return (BDD_NOT(v));
00293         case POSNODE_ENCODING:
00294         case NEGNODE_ENCODING:
00295           node_number=read(error, node_number_size, fp);
00296           if (!*error && (node_number >= number_shared || !shared[node_number]))
00297             *error=BDD_UNDUMP_FORMAT;
00298           if (*error)
00299             return ((bdd)0);
00300           v=shared[node_number];
00301           v=cmu_bdd_identity(bddm, v);
00302           if (encoding == POSNODE_ENCODING)
00303             return (v);
00304           else
00305             return (BDD_NOT(v));
00306         case NODELABEL_ENCODING:
00307           node_number= *shared_so_far;
00308           ++*shared_so_far;
00309           v=cmu_bdd_undump_bdd_step(bddm, vars, fp, number_vars, shared, number_shared,
00310                                 shared_so_far, index_size, node_number_size, error);
00311           shared[node_number]=v;
00312           v=cmu_bdd_identity(bddm, v);
00313           return (v);
00314         default:
00315           *error=BDD_UNDUMP_FORMAT;
00316           return ((bdd)0);
00317         }
00318     }
00319   if (i >= number_vars)
00320     {
00321       *error=BDD_UNDUMP_FORMAT;
00322       return ((bdd)0);
00323     }
00324   temp1=cmu_bdd_undump_bdd_step(bddm, vars, fp, number_vars, shared, number_shared,
00325                             shared_so_far, index_size, node_number_size, error);
00326   temp2=cmu_bdd_undump_bdd_step(bddm, vars, fp, number_vars, shared, number_shared,
00327                             shared_so_far, index_size, node_number_size, error);
00328   if (*error)
00329     {
00330       cmu_bdd_free(bddm, temp1);
00331       return ((bdd)0);
00332     }
00333   result=cmu_bdd_ite(bddm, vars[i], temp1, temp2);
00334   cmu_bdd_free(bddm, temp1);
00335   cmu_bdd_free(bddm, temp2);
00336   if (!result)
00337     *error=BDD_UNDUMP_OVERFLOW;
00338   return (result);
00339 }
00340 
00341 
00342 bdd
00343 cmu_bdd_undump_bdd(cmu_bdd_manager bddm, bdd *vars, FILE *fp, int *error)
00344 {
00345   long i;
00346   bdd_index_type number_vars;
00347   long number_shared;
00348   int index_size;
00349   int node_number_size;
00350   bdd *shared;
00351   long shared_so_far;
00352   bdd v;
00353   bdd result;
00354 
00355   *error=0;
00356   for (i=0; vars[i]; ++i)
00357     if (cmu_bdd_type(bddm, vars[i]) != BDD_TYPE_POSVAR)
00358       {
00359         cmu_bdd_warning("cmu_bdd_undump_bdd: support is not all positive variables");
00360         return ((bdd)0);
00361       }
00362   if (read(error, sizeof(long), fp) != MAGIC_COOKIE)
00363     {
00364       if (!*error)
00365         *error=BDD_UNDUMP_FORMAT;
00366       return ((bdd)0);
00367     }
00368   number_vars=read(error, sizeof(bdd_index_type), fp);
00369   if (*error)
00370     return ((bdd)0);
00371   if (number_vars != i)
00372     {
00373       *error=BDD_UNDUMP_FORMAT;
00374       return ((bdd)0);
00375     }
00376   number_shared=read(error, sizeof(long), fp);
00377   if (*error)
00378     return ((bdd)0);
00379   index_size=bytes_needed(number_vars+1);
00380   node_number_size=bytes_needed(number_shared);
00381   if (number_shared < 0)
00382     {
00383       *error=BDD_UNDUMP_FORMAT;
00384       return ((bdd)0);
00385     }
00386   shared=(bdd *)mem_get_block((SIZE_T)(number_shared*sizeof(bdd)));
00387   for (i=0; i < number_shared; ++i)
00388     shared[i]=0;
00389   shared_so_far=0;
00390   result=cmu_bdd_undump_bdd_step(bddm, vars, fp, number_vars, shared, number_shared,
00391                              &shared_so_far, index_size, node_number_size, error);
00392   for (i=0; i < number_shared; ++i)
00393     if ((v=shared[i]))
00394       cmu_bdd_free(bddm, v);
00395   if (!*error && shared_so_far != number_shared)
00396     *error=BDD_UNDUMP_FORMAT;
00397   mem_free_block((pointer)shared);
00398   if (*error)
00399     {
00400       if (result)
00401         cmu_bdd_free(bddm, result);
00402       return ((bdd)0);
00403     }
00404   return (result);
00405 }