source: vis_dev/glu-2.3/src/cmuBdd/bdddump.c @ 31

Last change on this file since 31 was 13, checked in by cecile, 13 years ago

library glu 2.3
File size: 9.9 KB
Line 
1/* BDD library dump/undump routines */
2
3
4#include "bddint.h"
5
6
7#define MAGIC_COOKIE 0x5e02f795l
8#define BDD_IOERROR 100
9
10
11#define TRUE_ENCODING 0xffffff00l
12#define FALSE_ENCODING 0xffffff01l
13#define POSVAR_ENCODING 0xffffff02l
14#define NEGVAR_ENCODING 0xffffff03l
15#define POSNODE_ENCODING 0xffffff04l
16#define NEGNODE_ENCODING 0xffffff05l
17#define NODELABEL_ENCODING 0xffffff06l
18#define CONSTANT_ENCODING 0xffffff07l
19
20
21static
22int
23bytes_needed(long n)
24{
25  if (n <= 0x100l)
26    return (1);
27  if (n <= 0x10000l)
28    return (2);
29  if (n <= 0x1000000l)
30    return (3);
31  return (4);
32}
33
34
35static
36void
37write(cmu_bdd_manager bddm, unsigned long n, int bytes, FILE *fp)
38{
39  while (bytes)
40    {
41      if (fputc((char)(n >> (8*(bytes-1)) & 0xff), fp) == EOF)
42        longjmp(bddm->abort.context, BDD_IOERROR);
43      --bytes;
44    }
45}
46
47
48static
49void
50cmu_bdd_dump_bdd_step(cmu_bdd_manager bddm,
51                  bdd f,
52                  FILE *fp,
53                  hash_table h,
54                  bdd_index_type *normalized_indexes,
55                  int index_size,
56                  int node_number_size)
57{
58  int negated;
59  long *number;
60
61  BDD_SETUP(f);
62  switch (cmu_bdd_type_aux(bddm, f))
63    {
64    case BDD_TYPE_ZERO:
65      write(bddm, FALSE_ENCODING, index_size+1, fp);
66      break;
67    case BDD_TYPE_ONE:
68      write(bddm, TRUE_ENCODING, index_size+1, fp);
69      break;
70    case BDD_TYPE_CONSTANT:
71      write(bddm, CONSTANT_ENCODING, index_size+1, fp);
72      write(bddm, (unsigned long)BDD_DATA(f)[0], sizeof(long), fp);
73      write(bddm, (unsigned long)BDD_DATA(f)[1], sizeof(long), fp);
74      break;
75    case BDD_TYPE_POSVAR:
76      write(bddm, POSVAR_ENCODING, index_size+1, fp);
77      write(bddm, (unsigned long)normalized_indexes[BDD_INDEX(bddm, f)], index_size, fp);
78      break;
79    case BDD_TYPE_NEGVAR:
80      write(bddm, NEGVAR_ENCODING, index_size+1, fp);
81      write(bddm, (unsigned long)normalized_indexes[BDD_INDEX(bddm, f)], index_size, fp);
82      break;
83    case BDD_TYPE_NONTERMINAL:
84      if (bdd_lookup_in_hash_table(h, BDD_NOT(f)))
85        {
86          f=BDD_NOT(f);
87          negated=1;
88        }
89      else
90        negated=0;
91      number=(long *)bdd_lookup_in_hash_table(h, f);
92      if (number && *number < 0)
93        {
94          if (negated)
95            write(bddm, NEGNODE_ENCODING, index_size+1, fp);
96          else
97            write(bddm, POSNODE_ENCODING, index_size+1, fp);
98          write(bddm, (unsigned long)(-*number-1), node_number_size, fp);
99        }
100      else
101        {
102          if (number)
103            {
104              write(bddm, NODELABEL_ENCODING, index_size+1, fp);
105              *number= -*number-1;
106            }
107          write(bddm, (unsigned long)normalized_indexes[BDD_INDEX(bddm, f)], index_size, fp);
108          cmu_bdd_dump_bdd_step(bddm, BDD_THEN(f), fp, h, normalized_indexes, index_size, node_number_size);
109          cmu_bdd_dump_bdd_step(bddm, BDD_ELSE(f), fp, h, normalized_indexes, index_size, node_number_size);
110        }
111      break;
112    default:
113      cmu_bdd_fatal("cmu_bdd_dump_bdd_step: unknown type returned by cmu_bdd_type");
114    }
115}
116
117
118int
119cmu_bdd_dump_bdd(cmu_bdd_manager bddm, bdd f, bdd *vars, FILE *fp)
120{
121  long i;
122  bdd_index_type *normalized_indexes;
123  bdd_index_type v_index;
124  bdd var;
125  bdd_index_type number_vars;
126  bdd *support;
127  int ok;
128  hash_table h;
129  int index_size;
130  long next;
131  int node_number_size;
132
133  if (bdd_check_arguments(1, f))
134    {
135      for (i=0; vars[i]; ++i)
136        if (cmu_bdd_type(bddm, vars[i]) != BDD_TYPE_POSVAR)
137          {
138            cmu_bdd_warning("cmu_bdd_dump_bdd: support is not all positive variables");
139            return (0);
140          }
141      normalized_indexes=(bdd_index_type *)mem_get_block((SIZE_T)(bddm->vars*sizeof(bdd_index_type)));
142      for (i=0; i < bddm->vars; ++i)
143        normalized_indexes[i]=BDD_MAX_INDEX;
144      for (i=0; (var=vars[i]); ++i)
145        {
146          BDD_SETUP(var);
147          v_index=BDD_INDEX(bddm, var);
148          if (normalized_indexes[v_index] != BDD_MAX_INDEX)
149            {
150              cmu_bdd_warning("cmu_bdd_dump_bdd: variables duplicated in support");
151              mem_free_block((pointer)normalized_indexes);
152              return (0);
153            }
154          normalized_indexes[v_index]=i;
155        }
156      number_vars=i;
157      support=(bdd *)mem_get_block((SIZE_T)((bddm->vars+1)*sizeof(bdd)));
158      cmu_bdd_support(bddm, f, support);
159      ok=1;
160      for (i=0; ok && (var=support[i]); ++i)
161        {
162          BDD_SETUP(var);
163          if (normalized_indexes[BDD_INDEX(bddm, var)] == BDD_MAX_INDEX)
164            {
165              cmu_bdd_warning("cmu_bdd_dump_bdd: incomplete support specified");
166              ok=0;
167            }
168        }
169      if (!ok)
170        {
171          mem_free_block((pointer)normalized_indexes);
172          mem_free_block((pointer)support);
173          return (0);
174        }
175      mem_free_block((pointer)support);
176      /* Everything checked now; barring I/O errors, we should be able to */
177      /* write a valid output file. */
178      h=bdd_new_hash_table(bddm, sizeof(long));
179      FIREWALL1(bddm,
180                if (retcode == BDD_IOERROR)
181                  {
182                    cmu_bdd_free_hash_table(h);
183                    mem_free_block((pointer)normalized_indexes);
184                    return (0);
185                  }
186                else
187                  cmu_bdd_fatal("cmu_bdd_dump_bdd: got unexpected retcode");
188                );
189      index_size=bytes_needed(number_vars+1);
190      bdd_mark_shared_nodes(bddm, f);
191      next=0;
192      bdd_number_shared_nodes(bddm, f, h, &next);
193      node_number_size=bytes_needed(next);
194      write(bddm, MAGIC_COOKIE, sizeof(long), fp);
195      write(bddm, (unsigned long)number_vars, sizeof(bdd_index_type), fp);
196      write(bddm, (unsigned long)next, sizeof(long), fp);
197      cmu_bdd_dump_bdd_step(bddm, f, fp, h, normalized_indexes, index_size, node_number_size);
198      cmu_bdd_free_hash_table(h);
199      mem_free_block((pointer)normalized_indexes);
200      return (1);
201    }
202  return (0);
203}
204
205
206static
207unsigned long
208read(int *error, int bytes, FILE *fp)
209{
210  int c;
211  long result;
212
213  result=0;
214  if (*error)
215    return (result);
216  while (bytes)
217    {
218      c=fgetc(fp);
219      if (c == EOF)
220        {
221          if (ferror(fp))
222            *error=BDD_UNDUMP_IOERROR;
223          else
224            *error=BDD_UNDUMP_EOF;
225          return (0l);
226        }
227      result=(result << 8)+c;
228      --bytes;
229    }
230  return (result);
231}
232
233
234static long index_mask[]={0xffl, 0xffffl, 0xffffffl};
235
236
237static
238bdd
239cmu_bdd_undump_bdd_step(cmu_bdd_manager bddm,
240                    bdd *vars,
241                    FILE *fp,
242                    bdd_index_type number_vars,
243                    bdd *shared,
244                    long number_shared,
245                    long *shared_so_far,
246                    int index_size,
247                    int node_number_size,
248                    int *error)
249{
250  long node_number;
251  long encoding;
252  bdd_index_type i;
253  INT_PTR value1, value2;
254  bdd v;
255  bdd temp1, temp2;
256  bdd result;
257
258  i=read(error, index_size, fp);
259  if (*error)
260    return ((bdd)0);
261  if (i == index_mask[index_size-1])
262    {
263      encoding=0xffffff00l+read(error, 1, fp);
264      if (*error)
265        return ((bdd)0);
266      switch (encoding)
267        {
268        case TRUE_ENCODING:
269          return (BDD_ONE(bddm));
270        case FALSE_ENCODING:
271          return (BDD_ZERO(bddm));
272        case CONSTANT_ENCODING:
273          value1=read(error, sizeof(long), fp);
274          value2=read(error, sizeof(long), fp);
275          if (*error)
276            return ((bdd)0);
277          if ((result=cmu_mtbdd_get_terminal(bddm, value1, value2)))
278            return (result);
279          *error=BDD_UNDUMP_OVERFLOW;
280          return ((bdd)0);
281        case POSVAR_ENCODING:
282        case NEGVAR_ENCODING:
283          i=read(error, index_size, fp);
284          if (!*error && i >= number_vars)
285            *error=BDD_UNDUMP_FORMAT;
286          if (*error)
287            return ((bdd)0);
288          v=vars[i];
289          if (encoding == POSVAR_ENCODING)
290            return (v);
291          else
292            return (BDD_NOT(v));
293        case POSNODE_ENCODING:
294        case NEGNODE_ENCODING:
295          node_number=read(error, node_number_size, fp);
296          if (!*error && (node_number >= number_shared || !shared[node_number]))
297            *error=BDD_UNDUMP_FORMAT;
298          if (*error)
299            return ((bdd)0);
300          v=shared[node_number];
301          v=cmu_bdd_identity(bddm, v);
302          if (encoding == POSNODE_ENCODING)
303            return (v);
304          else
305            return (BDD_NOT(v));
306        case NODELABEL_ENCODING:
307          node_number= *shared_so_far;
308          ++*shared_so_far;
309          v=cmu_bdd_undump_bdd_step(bddm, vars, fp, number_vars, shared, number_shared,
310                                shared_so_far, index_size, node_number_size, error);
311          shared[node_number]=v;
312          v=cmu_bdd_identity(bddm, v);
313          return (v);
314        default:
315          *error=BDD_UNDUMP_FORMAT;
316          return ((bdd)0);
317        }
318    }
319  if (i >= number_vars)
320    {
321      *error=BDD_UNDUMP_FORMAT;
322      return ((bdd)0);
323    }
324  temp1=cmu_bdd_undump_bdd_step(bddm, vars, fp, number_vars, shared, number_shared,
325                            shared_so_far, index_size, node_number_size, error);
326  temp2=cmu_bdd_undump_bdd_step(bddm, vars, fp, number_vars, shared, number_shared,
327                            shared_so_far, index_size, node_number_size, error);
328  if (*error)
329    {
330      cmu_bdd_free(bddm, temp1);
331      return ((bdd)0);
332    }
333  result=cmu_bdd_ite(bddm, vars[i], temp1, temp2);
334  cmu_bdd_free(bddm, temp1);
335  cmu_bdd_free(bddm, temp2);
336  if (!result)
337    *error=BDD_UNDUMP_OVERFLOW;
338  return (result);
339}
340
341
342bdd
343cmu_bdd_undump_bdd(cmu_bdd_manager bddm, bdd *vars, FILE *fp, int *error)
344{
345  long i;
346  bdd_index_type number_vars;
347  long number_shared;
348  int index_size;
349  int node_number_size;
350  bdd *shared;
351  long shared_so_far;
352  bdd v;
353  bdd result;
354
355  *error=0;
356  for (i=0; vars[i]; ++i)
357    if (cmu_bdd_type(bddm, vars[i]) != BDD_TYPE_POSVAR)
358      {
359        cmu_bdd_warning("cmu_bdd_undump_bdd: support is not all positive variables");
360        return ((bdd)0);
361      }
362  if (read(error, sizeof(long), fp) != MAGIC_COOKIE)
363    {
364      if (!*error)
365        *error=BDD_UNDUMP_FORMAT;
366      return ((bdd)0);
367    }
368  number_vars=read(error, sizeof(bdd_index_type), fp);
369  if (*error)
370    return ((bdd)0);
371  if (number_vars != i)
372    {
373      *error=BDD_UNDUMP_FORMAT;
374      return ((bdd)0);
375    }
376  number_shared=read(error, sizeof(long), fp);
377  if (*error)
378    return ((bdd)0);
379  index_size=bytes_needed(number_vars+1);
380  node_number_size=bytes_needed(number_shared);
381  if (number_shared < 0)
382    {
383      *error=BDD_UNDUMP_FORMAT;
384      return ((bdd)0);
385    }
386  shared=(bdd *)mem_get_block((SIZE_T)(number_shared*sizeof(bdd)));
387  for (i=0; i < number_shared; ++i)
388    shared[i]=0;
389  shared_so_far=0;
390  result=cmu_bdd_undump_bdd_step(bddm, vars, fp, number_vars, shared, number_shared,
391                             &shared_so_far, index_size, node_number_size, error);
392  for (i=0; i < number_shared; ++i)
393    if ((v=shared[i]))
394      cmu_bdd_free(bddm, v);
395  if (!*error && shared_so_far != number_shared)
396    *error=BDD_UNDUMP_FORMAT;
397  mem_free_block((pointer)shared);
398  if (*error)
399    {
400      if (result)
401        cmu_bdd_free(bddm, result);
402      return ((bdd)0);
403    }
404  return (result);
405}
Note: See TracBrowser for help on using the repository browser.