source: vis_dev/glu-2.3/src/calBdd/calDump.c @ 27

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

library glu 2.3
File size: 18.1 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [calDump.c]
4
5  PackageName [cal]
6
7  Synopsis    [BDD library dump/undump routines]
8             
9
10  Description [ ]
11
12  SeeAlso     [optional]
13
14  Author      [Jagesh Sanghavi (sanghavi@eecs.berkeley.edu)
15               Rajeev Ranjan   (rajeev@eecs.berkeley.edu)
16               Originally written by David Long.
17              ]
18
19  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
20  All rights reserved.
21
22  Permission is hereby granted, without written agreement and without license
23  or royalty fees, to use, copy, modify, and distribute this software and its
24  documentation for any purpose, provided that the above copyright notice and
25  the following two paragraphs appear in all copies of this software.
26
27  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
28  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
29  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
30  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
31
32  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
33  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
34  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
35  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
36  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
37
38  Revision    [$Id: calDump.c,v 1.1.1.3 1998/05/04 00:58:56 hsv Exp $]
39
40******************************************************************************/
41#include "calInt.h"
42
43/*---------------------------------------------------------------------------*/
44/* Constant declarations                                                     */
45/*---------------------------------------------------------------------------*/
46#define MAGIC_COOKIE 0x5e02f795l
47#define CAL_BDD_IOERROR 100
48
49#define TRUE_ENCODING 0xffffff00l
50#define FALSE_ENCODING 0xffffff01l
51#define POSVAR_ENCODING 0xffffff02l
52#define NEGVAR_ENCODING 0xffffff03l
53#define POSNODE_ENCODING 0xffffff04l
54#define NEGNODE_ENCODING 0xffffff05l
55#define NODELABEL_ENCODING 0xffffff06l
56#define CONSTANT_ENCODING 0xffffff07l
57
58/*---------------------------------------------------------------------------*/
59/* Type declarations                                                         */
60/*---------------------------------------------------------------------------*/
61
62/*---------------------------------------------------------------------------*/
63/* Stucture declarations                                                     */
64/*---------------------------------------------------------------------------*/
65
66/*---------------------------------------------------------------------------*/
67/* Variable declarations                                                     */
68/*---------------------------------------------------------------------------*/
69
70
71static long indexMask[] = {0xffl, 0xffffl, 0xffffffl};
72
73/*---------------------------------------------------------------------------*/
74/* Macro declarations                                                        */
75/*---------------------------------------------------------------------------*/
76
77
78/**AutomaticStart*************************************************************/
79
80/*---------------------------------------------------------------------------*/
81/* Static function prototypes                                                */
82/*---------------------------------------------------------------------------*/
83
84static void Write(Cal_BddManager_t * bddManager, unsigned long n, int bytes, FILE * fp);
85static void BddDumpBddStep(Cal_BddManager_t * bddManager, Cal_Bdd_t f, FILE * fp, CalHashTable_t * h, Cal_BddIndex_t * normalizedIndexes, int indexSize, int nodeNumberSize);
86static unsigned long Read(int * error, int bytes, FILE * fp);
87static 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);
88static int BytesNeeded(long n);
89
90/**AutomaticEnd***************************************************************/
91
92/*---------------------------------------------------------------------------*/
93/* Definition of exported functions                                          */
94/*---------------------------------------------------------------------------*/
95/**Function********************************************************************
96
97  Synopsis    [Reads a BDD from a file]
98
99  Description [Loads an encoded description of a BDD from the file given by
100  fp. The argument vars should be a null terminated array of variables that will
101  become the support of the BDD. As in Cal_BddDumpBdd, these need not be in
102  the order of increasing index. If the same array of variables in used in
103  dumping and undumping, the BDD returned will be equal to the one that was
104  dumped. More generally, if array v1 is used when dumping, and the array v2
105  is used when undumping, the BDD returned will be equal to the original BDD
106  with the ith variable in v2 substituted for the ith variable in v1 for all i.
107  Null BDD is returned in the operation fails for reason (node limit reached,
108  I/O error, invalid file format, etc.). In this case, an error code is stored
109  in error. the code will be one of the following.
110  CAL_BDD_UNDUMP_FORMAT Invalid file format
111  CAL_BDD_UNDUMP_OVERFLOW Node limit exceeded
112  CAL_BDD_UNDUMP_IOERROR File I/O error
113  CAL_BDD_UNDUMP_EOF Unexpected EOF]
114
115  SideEffects [required]
116
117  SeeAlso     [optional]
118
119******************************************************************************/
120Cal_Bdd
121Cal_BddUndumpBdd(
122  Cal_BddManager bddManager,
123  Cal_Bdd * userVars,
124  FILE * fp,
125  int * error)
126{
127  long i,j;
128  Cal_BddIndex_t numberVars;
129  long numberShared;
130  int indexSize;
131  int nodeNumberSize;
132  Cal_Bdd_t *shared;
133  long sharedSoFar;
134  Cal_Bdd_t v;
135  Cal_Bdd_t result;
136  Cal_Bdd_t *vars;
137
138  *error = 0;
139  for(i = 0; userVars[i]; ++i){
140    if(Cal_BddType(bddManager, userVars[i]) !=  CAL_BDD_TYPE_POSVAR){
141      CalBddWarningMessage("Cal_BddUndumpBdd: support is not all positive variables"); 
142      return (Cal_Bdd) 0;
143    }
144  }
145  vars = Cal_MemAlloc(Cal_Bdd_t, i);
146  for (j=0; j < i; j++){
147    vars[j] = CalBddGetInternalBdd(bddManager,userVars[j]);
148  }
149
150  if(Read(error, sizeof(long), fp) !=  MAGIC_COOKIE){
151    if(!*error){
152      *error = CAL_BDD_UNDUMP_FORMAT;
153    }
154    Cal_MemFree(vars);
155    return (Cal_Bdd) 0;
156  }
157  numberVars = Read(error, sizeof(Cal_BddIndex_t), fp);
158  if(*error){
159    Cal_MemFree(vars);
160    return (Cal_Bdd) 0;
161  }
162  if(numberVars !=  i){
163    *error = CAL_BDD_UNDUMP_FORMAT;
164    Cal_MemFree(vars);
165    return (Cal_Bdd) 0;
166  }
167  numberShared = Read(error, sizeof(long), fp);
168  if(*error){
169    Cal_MemFree(vars);
170    return (Cal_Bdd) 0;
171  }
172  indexSize = BytesNeeded(numberVars+1);
173  nodeNumberSize = BytesNeeded(numberShared);
174  if(numberShared < 0){
175    *error = CAL_BDD_UNDUMP_FORMAT;
176    Cal_MemFree(vars);
177    return (Cal_Bdd) 0;
178  }
179  shared = Cal_MemAlloc(Cal_Bdd_t, numberShared);
180  for(i = 0; i < numberShared; ++i){
181    shared[i] = CalBddNull(bddManager);
182  }
183  sharedSoFar = 0;
184  result = BddUndumpBddStep(bddManager, vars, fp, numberVars, shared,
185      numberShared, &sharedSoFar, indexSize, nodeNumberSize, error);
186  Cal_MemFree(vars);
187 
188  for(i = 0; i < numberShared; ++i){
189    v = shared[i];
190    if(!CalBddIsBddNull(bddManager, v)){
191      CalBddFree(v);
192    }
193  }
194  if(!*error && sharedSoFar !=  numberShared){
195    *error = CAL_BDD_UNDUMP_FORMAT;
196  }
197  Cal_MemFree(shared);
198  if(*error){
199    if(!CalBddIsBddNull(bddManager, result)){
200      CalBddFree(result);
201    }
202    return (Cal_Bdd) 0;
203  }
204  /*
205   * Decrement the reference count of result by 1. Since it has
206   * already been incremented in BddUndumpBddStep.
207   */
208  CalBddDcrRefCount(result);
209  return CalBddGetExternalBdd(bddManager, result);
210}
211
212
213/**Function********************************************************************
214
215  Synopsis    [Write a BDD to a file]
216
217  Description [Writes an encoded description of the BDD to the file given by fp.
218  The argument vars should be a null-terminated array of variables that include
219  the support of f .  These variables need not be in order of increasing index.
220  The function returns a nonzero value if f was written to the file successfully.
221  ]
222
223  SideEffects [required]
224
225  SeeAlso     [optional]
226
227******************************************************************************/
228int
229Cal_BddDumpBdd(
230  Cal_BddManager bddManager,
231  Cal_Bdd  fUserBdd,
232  Cal_Bdd * userVars,
233  FILE * fp)
234{
235  long i;
236  Cal_BddIndex_t *normalizedIndexes;
237  Cal_BddIndex_t vIndex;
238  Cal_Bdd_t f;
239  Cal_BddIndex_t numberVars;
240  Cal_Bdd *support;
241  int ok;
242  CalHashTable_t *h;
243  int indexSize;
244  long next;
245  int nodeNumberSize;
246
247  if(CalBddPreProcessing(bddManager, 1, fUserBdd)){
248    f = CalBddGetInternalBdd(bddManager, fUserBdd);
249    for(i = 0; userVars[i]; ++i){
250      if(Cal_BddType(bddManager, userVars[i]) !=  CAL_BDD_TYPE_POSVAR){
251        CalBddWarningMessage("Cal_BddDumpBdd: support is not all positive variables");
252        return (0);
253      }
254    }
255    normalizedIndexes = Cal_MemAlloc(Cal_BddIndex_t, bddManager->numVars);
256    for(i = 0; i < bddManager->numVars; ++i){
257      normalizedIndexes[i] = CAL_BDD_CONST_INDEX;
258    }
259    for(i = 0; userVars[i]; ++i){
260      vIndex = Cal_BddGetIfIndex(bddManager, userVars[i]);
261      if(normalizedIndexes[vIndex] !=  CAL_BDD_CONST_INDEX){
262        CalBddWarningMessage("Cal_BddDumpBdd: variables duplicated in support");
263        Cal_MemFree(normalizedIndexes);
264        return 0;
265      }
266      normalizedIndexes[vIndex] = i;
267    }
268    numberVars = i;
269    support = Cal_MemAlloc(Cal_Bdd, bddManager->numVars+1);
270    Cal_BddSupport(bddManager, fUserBdd, support);
271    ok = 1;
272    for(i = 0; ok && support[i]; ++i){
273      if(normalizedIndexes[Cal_BddGetIfIndex(bddManager, support[i])] == CAL_BDD_CONST_INDEX){
274        CalBddWarningMessage("Cal_BddDumpBdd: incomplete support specified");
275        ok = 0;
276      }
277    }
278    if(!ok){
279      Cal_MemFree(normalizedIndexes);
280      Cal_MemFree(support);
281      return 0;
282    }
283    Cal_MemFree(support);
284    /* Everything checked now; barring I/O errors, we should be able to */
285    /* Write a valid output file. */
286    f = CalBddGetInternalBdd(bddManager, fUserBdd);
287    h = CalHashTableOneInit(bddManager, sizeof(long));
288    indexSize = BytesNeeded(numberVars+1);
289    CalBddMarkSharedNodes(bddManager, f);
290    next = 0;
291    CalBddNumberSharedNodes(bddManager, f, h, &next);
292    nodeNumberSize = BytesNeeded(next);
293    Write(bddManager, MAGIC_COOKIE, sizeof(long), fp);
294    Write(bddManager, (unsigned long)numberVars, sizeof(Cal_BddIndex_t), fp);
295    Write(bddManager, (unsigned long)next, sizeof(long), fp);
296    BddDumpBddStep(bddManager, f, fp, h, normalizedIndexes, indexSize, nodeNumberSize);
297    CalHashTableOneQuit(h);
298    Cal_MemFree(normalizedIndexes);
299    return (1);
300  }
301  return (0);
302}
303
304/**Function********************************************************************
305
306  Synopsis    []
307
308  Description [optional]
309
310  SideEffects [required]
311
312  SeeAlso     [optional]
313
314******************************************************************************/
315static void
316Write(
317  Cal_BddManager_t * bddManager,
318  unsigned long  n,
319  int  bytes,
320  FILE * fp)
321{
322  while(bytes){
323    if(fputc((char)(n >> (8*(bytes-1)) & 0xff), fp) == EOF){
324    }
325    --bytes;
326  }
327}
328
329
330/**Function********************************************************************
331
332  Synopsis    []
333
334  Description [optional]
335
336  SideEffects [required]
337
338  SeeAlso     [optional]
339
340******************************************************************************/
341static void
342BddDumpBddStep(
343  Cal_BddManager_t * bddManager,
344  Cal_Bdd_t  f,
345  FILE * fp,
346  CalHashTable_t * h,
347  Cal_BddIndex_t * normalizedIndexes,
348  int  indexSize,
349  int  nodeNumberSize)
350{
351  int negated;
352  long *number;
353  Cal_Bdd_t thenBdd, elseBdd;
354
355  switch(CalBddTypeAux(bddManager, f)){
356  case CAL_BDD_TYPE_ZERO:
357    Write(bddManager, FALSE_ENCODING, indexSize+1, fp);
358    break;
359  case CAL_BDD_TYPE_ONE:
360    Write(bddManager, TRUE_ENCODING, indexSize+1, fp);
361    break;
362  case CAL_BDD_TYPE_CONSTANT:
363    Write(bddManager, CONSTANT_ENCODING, indexSize+1, fp);
364#ifdef JAGESH
365    Write(bddManager, (unsigned long)BDD_DATA(f)[0], sizeof(long), fp);
366    Write(bddManager, (unsigned long)BDD_DATA(f)[1], sizeof(long), fp);
367#endif
368    break;
369  case CAL_BDD_TYPE_POSVAR:
370    Write(bddManager, POSVAR_ENCODING, indexSize+1, fp);
371    Write(bddManager,
372        (unsigned long)normalizedIndexes[CalBddGetBddIndex(bddManager, f)],
373        indexSize, fp);
374    break;
375  case CAL_BDD_TYPE_NEGVAR:
376    Write(bddManager, NEGVAR_ENCODING, indexSize+1, fp);
377    Write(bddManager, 
378        (unsigned long)normalizedIndexes[CalBddGetBddIndex(bddManager, f)],
379        indexSize, fp);
380    break;
381  case CAL_BDD_TYPE_NONTERMINAL:
382    CalBddNot(f, f);
383    if(CalHashTableOneLookup(h, f, (char **)0)){
384      negated  =  1;
385    }
386    else{
387      CalBddNot(f, f);
388      negated = 0;
389    }
390    CalHashTableOneLookup(h, f, (char **)&number);
391    if(number && *number < 0){
392          if(negated)
393            Write(bddManager, NEGNODE_ENCODING, indexSize+1, fp);
394          else
395            Write(bddManager, POSNODE_ENCODING, indexSize+1, fp);
396          Write(bddManager, (unsigned long)(-*number-1), nodeNumberSize, fp);
397    }
398    else{
399      if(number){
400              Write(bddManager, NODELABEL_ENCODING, indexSize+1, fp);
401              *number =  -*number-1;
402      }
403      Write(bddManager,
404          (unsigned long)normalizedIndexes[CalBddGetBddIndex(bddManager, f)],
405          indexSize, fp);
406      CalBddGetThenBdd(f, thenBdd);
407      BddDumpBddStep(bddManager, thenBdd, fp, h, normalizedIndexes,
408          indexSize, nodeNumberSize);
409      CalBddGetElseBdd(f, elseBdd);
410      BddDumpBddStep(bddManager, elseBdd, fp, h, normalizedIndexes,
411          indexSize, nodeNumberSize);
412    }
413    break;
414  default:
415    CalBddFatalMessage("BddDumpBddStep: unknown type returned by CalBddType");
416  }
417}
418
419
420
421/**Function********************************************************************
422
423  Synopsis    []
424
425  Description [optional]
426
427  SideEffects [required]
428
429  SeeAlso     [optional]
430
431******************************************************************************/
432static unsigned long
433Read(
434  int * error,
435  int  bytes,
436  FILE * fp)
437{
438  int c;
439  long result;
440
441  result = 0;
442  if(*error){
443    return (result);
444  }
445  while(bytes){
446    c = fgetc(fp);
447    if(c == EOF){
448      if(ferror(fp)){
449        *error = CAL_BDD_UNDUMP_IOERROR;
450      }
451      else{
452        *error = CAL_BDD_UNDUMP_EOF;
453      }
454      return (0l);
455    }
456    result = (result << 8)+c;
457    --bytes;
458  } 
459  return (result);
460}
461
462
463
464
465/**Function********************************************************************
466
467  Synopsis    []
468
469  Description [optional]
470
471  SideEffects [required]
472
473  SeeAlso     [optional]
474
475******************************************************************************/
476static Cal_Bdd_t
477BddUndumpBddStep(
478  Cal_BddManager_t * bddManager,
479  Cal_Bdd_t * vars,
480  FILE * fp,
481  Cal_BddIndex_t  numberVars,
482  Cal_Bdd_t * shared,
483  long  numberShared,
484  long * sharedSoFar,
485  int  indexSize,
486  int  nodeNumberSize,
487  int * error)
488{
489  long nodeNumber;
490  long encoding;
491  Cal_BddIndex_t i;
492  CalAddress_t value1, value2;
493  Cal_Bdd_t v;
494  Cal_Bdd_t temp1, temp2;
495  Cal_Bdd_t result;
496
497  i = Read(error, indexSize, fp);
498  if(*error){
499    return CalBddNull(bddManager);
500  }
501  if(i == indexMask[indexSize-1]){
502    encoding = 0xffffff00l+Read(error, 1, fp);
503    if(*error){
504      return CalBddNull(bddManager);
505    }
506    switch(encoding){
507    case TRUE_ENCODING:
508      return (CalBddOne(bddManager));
509    case FALSE_ENCODING:
510      return (CalBddZero(bddManager));
511    case CONSTANT_ENCODING:
512      value1 = Read(error, sizeof(long), fp);
513      value2 = Read(error, sizeof(long), fp);
514      if(*error){
515        return CalBddNull(bddManager);
516      }
517      *error = CAL_BDD_UNDUMP_OVERFLOW;
518      return CalBddNull(bddManager);
519    case POSVAR_ENCODING:
520    case NEGVAR_ENCODING:
521      i = Read(error, indexSize, fp);
522      if(!*error && i >=  numberVars){
523        *error = CAL_BDD_UNDUMP_FORMAT;
524      }
525      if(*error){
526        return CalBddNull(bddManager);
527      }
528      v = vars[i];
529      if(encoding == POSVAR_ENCODING){
530        return (v);
531      }
532      else{
533        CalBddNot(v, v);
534        return (v);
535      }
536    case POSNODE_ENCODING:
537    case NEGNODE_ENCODING:
538      nodeNumber = Read(error, nodeNumberSize, fp);
539      if(!*error && (nodeNumber >=  numberShared ||
540          CalBddIsBddNull(bddManager, shared[nodeNumber]))){
541        *error = CAL_BDD_UNDUMP_FORMAT;
542      }
543      if(*error){
544        return CalBddNull(bddManager);
545      }
546      v = shared[nodeNumber];
547      v = CalBddIdentity(bddManager, v);
548      if(encoding == POSNODE_ENCODING){
549        return (v);
550      }
551      else{
552        CalBddNot(v, v);
553        return (v);
554      }
555    case NODELABEL_ENCODING:
556      nodeNumber =  *sharedSoFar;
557      ++*sharedSoFar;
558      v = BddUndumpBddStep(bddManager, vars, fp, numberVars, shared,
559          numberShared, sharedSoFar, indexSize, nodeNumberSize, error);
560      shared[nodeNumber] = v;
561      v = CalBddIdentity(bddManager, v);
562      return (v);
563    default:
564      *error = CAL_BDD_UNDUMP_FORMAT;
565      return CalBddNull(bddManager);
566    }
567  }
568  if(i >= numberVars){
569    *error = CAL_BDD_UNDUMP_FORMAT;
570    return CalBddNull(bddManager);
571  }
572  temp1 = BddUndumpBddStep(bddManager, vars, fp, numberVars, shared,
573       numberShared, sharedSoFar, indexSize, nodeNumberSize, error);
574  temp2 = BddUndumpBddStep(bddManager, vars, fp, numberVars, shared,
575       numberShared, sharedSoFar, indexSize, nodeNumberSize, error);
576  if(*error){
577      CalBddFree(temp1);
578      return CalBddNull(bddManager);
579  }
580  result = CalBddITE(bddManager, vars[i], temp1, temp2);
581  CalBddFree(temp1);
582  CalBddFree(temp2);
583  if(CalBddIsBddNull(bddManager, result)){
584     *error = CAL_BDD_UNDUMP_OVERFLOW;
585  }
586  return (result);
587}
588
589
590
591/**Function********************************************************************
592
593  Synopsis    []
594
595  Description [optional]
596
597  SideEffects [required]
598
599  SeeAlso     [optional]
600
601******************************************************************************/
602static int
603BytesNeeded(
604  long  n)
605{
606  if(n <= 0x100l){
607    return (1);
608  }
609  if(n <= 0x10000l){
610    return (2);
611  }
612  if(n <= 0x1000000l){
613    return (3);
614  }
615  return (4);
616}
617
618
619
620
621
622
623
624
625
626
627
628
Note: See TracBrowser for help on using the repository browser.