source: icGREP/icgrep-devel/cudd-2.5.1/dddmp/dddmpStoreBdd.c @ 4597

Last change on this file since 4597 was 4597, checked in by nmedfort, 4 years ago

Upload of the CUDD library.

File size: 32.2 KB
Line 
1/**CFile**********************************************************************
2
3  FileName     [dddmpStoreBdd.c]
4
5  PackageName  [dddmp]
6
7  Synopsis     [Functions to write BDDs to file.]
8
9  Description  [Functions to write BDDs to file.
10    BDDs are represended on file either in text or binary format under the
11    following rules.  A file contains a forest of BDDs (a vector of
12    Boolean functions).  BDD nodes are numbered with contiguous numbers,
13    from 1 to NNodes (total number of nodes on a file). 0 is not used to
14    allow negative node indexes for complemented edges.  A file contains
15    a header, including information about variables and roots to BDD
16    functions, followed by the list of nodes.  BDD nodes are listed
17    according to their numbering, and in the present implementation
18    numbering follows a post-order strategy, in such a way that a node
19    is never listed before its Then/Else children.
20  ]
21
22  Author       [Gianpiero Cabodi and Stefano Quer]
23
24  Copyright    [
25    Copyright (c) 2004 by Politecnico di Torino.
26    All Rights Reserved. This software is for educational purposes only.
27    Permission is given to academic institutions to use, copy, and modify
28    this software and its documentation provided that this introductory
29    message is not removed, that this software and its documentation is
30    used for the institutions' internal research and educational purposes,
31    and that no monies are exchanged. No guarantee is expressed or implied
32    by the distribution of this code.
33    Send bug-reports and/or questions to:
34    {gianpiero.cabodi,stefano.quer}@polito.it.
35    ]
36
37******************************************************************************/
38
39#include "dddmpInt.h"
40
41/*---------------------------------------------------------------------------*/
42/* Stucture declarations                                                     */
43/*---------------------------------------------------------------------------*/
44
45/*---------------------------------------------------------------------------*/
46/* Type declarations                                                         */
47/*---------------------------------------------------------------------------*/
48
49/*---------------------------------------------------------------------------*/
50/* Variable declarations                                                     */
51/*---------------------------------------------------------------------------*/
52
53/*---------------------------------------------------------------------------*/
54/* Macro declarations                                                        */
55/*---------------------------------------------------------------------------*/
56
57/**AutomaticStart*************************************************************/
58
59/*---------------------------------------------------------------------------*/
60/* Static function prototypes                                                */
61/*---------------------------------------------------------------------------*/
62
63static int NodeStoreRecurBdd(DdManager *ddMgr, DdNode *f, int mode, int *supportids, char **varnames, int *outids, FILE *fp);
64static int NodeTextStoreBdd(DdManager *ddMgr, DdNode *f, int mode, int *supportids, char **varnames, int *outids, FILE *fp, int idf, int vf, int idT, int idE);
65static int NodeBinaryStoreBdd(DdManager *ddMgr, DdNode *f, int mode, int *supportids, char **varnames, int *outids, FILE *fp, int idf, int vf, int idT, int idE, int vT, int vE, DdNode *T, DdNode *E);
66
67/**AutomaticEnd***************************************************************/
68
69/*---------------------------------------------------------------------------*/
70/* Definition of exported functions                                          */
71/*---------------------------------------------------------------------------*/
72
73/**Function********************************************************************
74
75  Synopsis     [Writes a dump file representing the argument BDD.]
76
77  Description  [Dumps the argument BDD to file. Dumping is done through
78    Dddmp_cuddBddArrayStore. A dummy array of 1 BDD root is
79    used for this purpose.
80    ]
81
82  SideEffects  [Nodes are temporarily removed from unique hash. They are
83    re-linked after the store operation in a modified order.
84    ]
85
86  SeeAlso      [Dddmp_cuddBddLoad Dddmp_cuddBddArrayLoad]
87
88******************************************************************************/
89
90int
91Dddmp_cuddBddStore (
92  DdManager *ddMgr           /* IN: DD Manager */,
93  char *ddname               /* IN: DD name (or NULL) */,
94  DdNode *f                  /* IN: BDD root to be stored */,
95  char **varnames            /* IN: array of variable names (or NULL) */,
96  int *auxids                /* IN: array of converted var ids */,
97  int mode                   /* IN: storing mode selector */,
98  Dddmp_VarInfoType varinfo  /* IN: extra info for variables in text mode */,
99  char *fname                /* IN: File name */,
100  FILE *fp                   /* IN: File pointer to the store file */ 
101  )
102{
103  int retValue;
104  DdNode *tmpArray[1];
105
106  tmpArray[0] = f;
107
108  retValue = Dddmp_cuddBddArrayStore (ddMgr,ddname,1,tmpArray,NULL,
109    varnames, auxids, mode, varinfo, fname, fp);
110
111  return (retValue);
112}
113
114/**Function********************************************************************
115
116  Synopsis     [Writes a dump file representing the argument Array of BDDs.]
117
118  Description  [Dumps the argument array of BDDs to file. Dumping is either
119    in text or binary form.  BDDs are stored to the fp (already
120    open) file if not NULL. Otherwise the file whose name is
121    fname is opened in write mode. The header has the same format
122    for both textual and binary dump. Names are allowed for input
123    variables (vnames) and for represented functions (rnames).
124    For sake of generality and because of dynamic variable
125    ordering both variable IDs and permuted IDs are included.
126    New IDs are also supported (auxids). Variables are identified
127    with incremental numbers. according with their positiom in
128    the support set. In text mode, an extra info may be added,
129    chosen among the following options: name, ID, PermID, or an
130    auxiliary id. Since conversion from DD pointers to integers
131    is required, DD nodes are temporarily removed from the unique
132    hash table. This allows the use of the next field to store
133    node IDs.
134   ]
135
136  SideEffects  [Nodes are temporarily removed from the unique hash
137    table. They are re-linked after the store operation in a
138    modified order.
139    ]
140
141  SeeAlso      [Dddmp_cuddBddStore, Dddmp_cuddBddLoad,
142    Dddmp_cuddBddArrayLoad
143    ]
144
145******************************************************************************/
146
147int
148Dddmp_cuddBddArrayStore (
149  DdManager *ddMgr           /* IN: DD Manager */,
150  char *ddname               /* IN: dd name (or NULL) */,
151  int nRoots                 /* IN: number of output BDD roots to be stored */,
152  DdNode **f                 /* IN: array of BDD roots to be stored */,
153  char **rootnames           /* IN: array of root names (or NULL) */,
154  char **varnames            /* IN: array of variable names (or NULL) */,
155  int *auxids                /* IN: array of converted var IDs */,
156  int mode                   /* IN: storing mode selector */,
157  Dddmp_VarInfoType varinfo  /* IN: extra info for variables in text mode */,
158  char *fname                /* IN: File name */,
159  FILE *fp                   /* IN: File pointer to the store file */ 
160  )
161{
162  int retValue;
163
164#ifdef DDDMP_DEBUG
165#ifndef __alpha__ 
166  int retValueBis;
167
168  retValueBis = Cudd_DebugCheck (ddMgr);
169  if (retValueBis == 1) {
170    fprintf (stderr, "Inconsistency Found During BDD Store.\n");
171    fflush (stderr);
172  } else {
173    if (retValueBis == CUDD_OUT_OF_MEM) {
174      fprintf (stderr, "Out of Memory During BDD Store.\n");
175      fflush (stderr);
176    }
177  }
178#endif
179#endif
180
181  retValue = DddmpCuddBddArrayStore (DDDMP_BDD, ddMgr, ddname, nRoots, f,
182    rootnames, varnames, auxids, mode, varinfo, fname, fp);
183
184#ifdef DDDMP_DEBUG
185#ifndef __alpha__ 
186  retValueBis = Cudd_DebugCheck (ddMgr);
187  if (retValueBis == 1) {
188    fprintf (stderr, "Inconsistency Found During BDD Store.\n");
189    fflush (stderr);
190  } else {
191    if (retValueBis == CUDD_OUT_OF_MEM) {
192      fprintf (stderr, "Out of Memory During BDD Store.\n");
193      fflush (stderr);
194    }
195  }
196#endif
197#endif
198
199  return (retValue);
200}
201
202/*---------------------------------------------------------------------------*/
203/* Definition of internal functions                                          */
204/*---------------------------------------------------------------------------*/
205
206/**Function********************************************************************
207
208  Synopsis     [Writes a dump file representing the argument Array of
209    BDDs.
210    ]
211
212  Description  [Dumps the argument array of BDDs to file.
213    Internal function doing inner steps of store for BDDs.
214    ]
215
216  SideEffects  [Nodes are temporarily removed from the unique hash
217    table. They are re-linked after the store operation in a
218    modified order.
219    ]   
220       
221  SeeAlso      [Dddmp_cuddBddStore, Dddmp_cuddBddLoad,
222    Dddmp_cuddBddArrayLoad
223    ]
224
225******************************************************************************/
226
227int
228DddmpCuddBddArrayStore (
229  Dddmp_DecompType ddType   /* IN: Selects the decomp type BDD */,
230  DdManager *ddMgr          /* IN: DD Manager */,
231  char *ddname              /* IN: DD name (or NULL) */,
232  int nRoots                /* IN: number of output BDD roots to be stored */,
233  DdNode **f                /* IN: array of DD roots to be stored */,
234  char **rootnames          /* IN: array of root names (or NULL) */,
235  char **varnames           /* IN: array of variable names (or NULL) */,
236  int *auxids               /* IN: array of converted var IDs */,
237  int mode                  /* IN: storing mode selector */,
238  Dddmp_VarInfoType varinfo /* IN: extra info for variables in text mode */,
239  char *fname               /* IN: File name */,
240  FILE *fp                  /* IN: File pointer to the store file */ 
241  )
242{
243  DdNode *support = NULL;
244  DdNode *scan;
245  int *ids = NULL;
246  int *permids = NULL;
247  int *invpermids = NULL;
248  int *supportids = NULL;
249  int *outids = NULL;
250  char **outvarnames = NULL;
251  int nVars = ddMgr->size;
252  int nnodes;
253  int retValue;
254  int i, var;
255  int fileToClose = 0;
256
257  /*
258   *  Check DD Type
259   */
260
261  Dddmp_CheckAndGotoLabel (ddType==DDDMP_ADD,
262    "Error writing to file: ADD Type.", failure);
263
264  /*
265   *  Check if File needs to be opened in the proper mode.
266   */
267
268  if (fp == NULL) {
269    fp = fopen (fname, "w");
270    Dddmp_CheckAndGotoLabel (fp==NULL, "Error opening file.",
271      failure);
272    fileToClose = 1;
273  }
274
275  /*
276   *  Force binary mode if automatic.
277   */
278
279  switch (mode) {
280    case DDDMP_MODE_TEXT:
281    case DDDMP_MODE_BINARY:
282      break;
283    case DDDMP_MODE_DEFAULT:
284      mode = DDDMP_MODE_BINARY;
285      break;
286    default:
287      mode = DDDMP_MODE_BINARY;
288      break;
289  }
290
291  /*
292   * Alloc vectors for variable IDs, perm IDs and support IDs.
293   *  +1 to include a slot for terminals.
294   */
295
296  ids = DDDMP_ALLOC (int, nVars);
297  Dddmp_CheckAndGotoLabel (ids==NULL, "Error allocating memory.", failure);
298  permids = DDDMP_ALLOC (int, nVars);
299  Dddmp_CheckAndGotoLabel (permids==NULL, "Error allocating memory.", failure);
300  invpermids = DDDMP_ALLOC (int, nVars);
301  Dddmp_CheckAndGotoLabel (invpermids==NULL, "Error allocating memory.",
302    failure);
303  supportids = DDDMP_ALLOC (int, nVars+1);
304  Dddmp_CheckAndGotoLabel (supportids==NULL, "Error allocating memory.",
305    failure);
306   
307  for (i=0; i<nVars; i++) {
308    ids[i] = permids[i] = invpermids[i] = supportids[i] = (-1);
309  }
310  /* StQ */
311  supportids[nVars] = -1;
312 
313  /*
314   *  Take the union of the supports of each output function.
315   *  skip NULL functions.
316   *  Set permids and invpermids of support variables to the proper values.
317   */
318
319  for (i=0; i<nRoots; i++) {
320    if (f[i] == NULL) {
321      continue;
322    }
323    support = Cudd_Support (ddMgr, f[i]);
324    Dddmp_CheckAndGotoLabel (support==NULL, "NULL support returned.",
325      failure);
326    cuddRef (support);
327    scan = support;
328    while (!cuddIsConstant(scan)) {
329      ids[scan->index] = scan->index;
330      permids[scan->index] = ddMgr->perm[scan->index];
331      invpermids[ddMgr->perm[scan->index]] = scan->index;
332      scan = cuddT (scan);
333    }
334    Cudd_RecursiveDeref (ddMgr, support);
335  }
336  /* so that we do not try to free it in case of failure */
337  support = NULL;
338
339  /*
340   *  Set supportids to incremental (shrinked) values following the ordering.
341   */
342
343  for (i=0, var=0; i<nVars; i++) {
344    if (invpermids[i] >= 0) {
345      supportids[invpermids[i]] = var++;
346    }
347  }
348  /* set a dummy id for terminal nodes */
349  supportids[nVars] = var;
350
351  /*
352   *  Select conversion array for extra var info
353   */
354
355  switch (mode) {
356    case DDDMP_MODE_TEXT:
357      switch (varinfo) {
358        case DDDMP_VARIDS:
359          outids = ids;
360          break;
361        case DDDMP_VARPERMIDS:
362          outids = permids;
363          break;
364        case DDDMP_VARAUXIDS:
365          outids = auxids;
366          break;
367        case DDDMP_VARNAMES:
368          outvarnames = varnames;
369          break;
370        case DDDMP_VARDEFAULT:
371          break;
372      }
373      break;
374    case DDDMP_MODE_BINARY:
375      outids = NULL;
376      break;
377  }
378
379  /*
380   *  Number dd nodes and count them (numbering is from 1 to nnodes)
381   */
382
383  nnodes = DddmpNumberBddNodes (ddMgr, f, nRoots);
384
385  /*
386   * Start Header
387   */
388
389#ifdef DDDMP_VERSION
390  retValue = fprintf (fp, ".ver %s\n", DDDMP_VERSION);
391  Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
392    failure);
393#endif
394
395  retValue = fprintf (fp, ".mode %c\n", mode);
396  Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
397    failure);
398
399  if (mode == DDDMP_MODE_TEXT) {
400    retValue = fprintf (fp, ".varinfo %d\n", varinfo);
401    Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
402      failure);
403  }
404
405  if (ddname != NULL) {
406    retValue = fprintf (fp, ".dd %s\n",ddname);
407    Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
408      failure);
409  }
410
411  retValue = fprintf (fp, ".nnodes %d\n", nnodes);
412  Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
413    failure);
414
415  retValue = fprintf (fp, ".nvars %d\n", nVars);
416  Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
417    failure);
418
419  retValue = fprintf (fp, ".nsuppvars %d\n", var);
420  Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
421    failure);
422
423  /*------------  Write the Var Names by scanning the ids array -------------*/
424
425  if (varnames != NULL) {
426
427    retValue = fprintf (fp, ".suppvarnames");
428    Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
429      failure);
430
431    for (i=0; i<nVars; i++) {
432      if (ids[i] >= 0) {
433        if (varnames[ids[i]] == NULL) {
434          (void) fprintf (stderr,
435             "DdStore Warning: null variable name. DUMMY%d generated\n", i);
436          fflush (stderr);
437          varnames[ids[i]] = DDDMP_ALLOC (char, 10);
438          Dddmp_CheckAndGotoLabel (varnames[ids[i]] == NULL,
439            "Error allocating memory.", failure);
440          sprintf (varnames[ids[i]], "DUMMY%d", i);
441        }
442        retValue = fprintf (fp, " %s", varnames[ids[i]]);
443        Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
444          failure);
445      }
446    }
447
448    retValue = fprintf (fp, "\n");
449    Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
450      failure);
451  }
452
453  /*--------- Write the Var SUPPORT Names by scanning the ids array ---------*/
454
455  if (varnames != NULL) {
456    retValue = fprintf (fp, ".orderedvarnames");
457    Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
458      failure);
459
460    for (i=0; i<nVars; i++) {
461      if (varnames[ddMgr->invperm[i]] == NULL) {
462          (void) fprintf (stderr,
463           "DdStore Warning: null variable name. DUMMY%d generated\n", i);
464        fflush (stderr);
465        varnames[ddMgr->invperm[i]] = DDDMP_ALLOC (char, 10);
466        Dddmp_CheckAndGotoLabel (varnames[ddMgr->invperm[i]] == NULL,
467          "Error allocating memory.", failure);
468        sprintf (varnames[ddMgr->invperm[i]], "DUMMY%d", i);
469      }
470
471      retValue = fprintf (fp, " %s", varnames[ddMgr->invperm[i]]);
472      Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
473        failure);
474    }
475
476    retValue = fprintf (fp, "\n");
477    Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
478      failure);
479  }
480
481  /*------------ Write the var ids by scanning the ids array ---------------*/
482
483  retValue = fprintf (fp, ".ids");
484  Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
485    failure);
486
487  for (i=0; i<nVars; i++) {
488    if (ids[i] >= 0) {
489      retValue = fprintf (fp, " %d", i);
490      Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
491        failure);
492    }
493  }
494  retValue = fprintf (fp, "\n");
495  Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
496    failure);
497
498  /*
499   *  Write the var permids by scanning the permids array.
500   */
501
502  retValue = fprintf (fp, ".permids");
503  Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
504    failure);
505  for (i = 0; i < nVars; i++) {
506    if (permids[i] >= 0) {
507      retValue = fprintf (fp, " %d", permids[i]);
508      Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
509        failure);
510    }
511  }
512
513  retValue = fprintf (fp, "\n");
514  Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
515    failure);
516
517  if (auxids != NULL) {
518 
519    /*
520     * Write the var auxids by scanning the ids array.
521     */
522
523    retValue = fprintf (fp, ".auxids");
524    Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
525      failure);
526    for (i = 0; i < nVars; i++) {
527      if (ids[i] >= 0) {
528        retValue = fprintf (fp, " %d", auxids[i]);
529        Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
530          failure);
531      }
532    }
533    retValue = fprintf (fp, "\n");
534    Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
535      failure);
536  }
537
538  /*
539   * Write the roots info.
540   */
541
542  retValue = fprintf (fp, ".nroots %d\n", nRoots);
543  Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
544    failure);
545
546  if (rootnames != NULL) {
547
548    /*
549     * Write the root names.
550     */
551
552    retValue = fprintf (fp, ".rootnames");
553    Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
554      failure);
555
556    for (i = 0; i < nRoots; i++) {
557      if (rootnames[i] == NULL) {
558        (void) fprintf (stderr,
559          "DdStore Warning: null variable name. ROOT%d generated\n",i);
560        fflush (stderr);
561        rootnames[i] = DDDMP_ALLOC(char,10);
562        Dddmp_CheckAndGotoLabel (rootnames[i]==NULL,
563          "Error writing to file.", failure);
564        sprintf(rootnames[ids[i]], "ROOT%d",i);
565      }
566      retValue = fprintf (fp, " %s", rootnames[i]);
567      Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
568        failure);
569    }
570
571    retValue = fprintf (fp, "\n");
572    Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
573      failure);
574  }
575
576  retValue = fprintf (fp, ".rootids");
577  Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
578    failure);
579
580  /*
581   * Write BDD indexes of function roots.
582   * Use negative integers for complemented edges.
583   */
584
585  for (i = 0; i < nRoots; i++) {
586    if (f[i] == NULL) {
587      (void) fprintf (stderr, "DdStore Warning: %d-th root is NULL\n",i);
588      fflush (stderr);
589      retValue = fprintf (fp, " 0");
590    }
591    if (Cudd_IsComplement(f[i])) {
592      retValue = fprintf (fp, " -%d",
593        DddmpReadNodeIndexBdd (Cudd_Regular (f[i])));
594    } else {
595      retValue = fprintf (fp, " %d",
596        DddmpReadNodeIndexBdd (Cudd_Regular (f[i])));
597    }
598    Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
599      failure);
600  }
601
602  retValue = fprintf (fp, "\n");
603  Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
604    failure);
605
606  retValue = fprintf (fp, ".nodes\n");
607  Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
608    failure);
609
610  /*
611   *  END HEADER
612   */
613
614  /*
615   *  Call the function that really gets the job done.
616   */
617
618  for (i = 0; i < nRoots; i++) {
619    if (f[i] != NULL) {
620      retValue = NodeStoreRecurBdd (ddMgr, Cudd_Regular(f[i]),
621        mode, supportids, outvarnames, outids, fp);
622      Dddmp_CheckAndGotoLabel (retValue==DDDMP_FAILURE,
623        "Error writing to file.", failure);
624    }
625  }
626
627  /*
628   *  Write trailer and return.
629   */
630
631  retValue = fprintf (fp, ".end\n");
632  Dddmp_CheckAndGotoLabel (retValue==EOF, "Error writing to file.",
633    failure);
634
635  if (fileToClose) {
636    fclose (fp);
637  }
638
639  DddmpUnnumberBddNodes (ddMgr, f, nRoots);
640  DDDMP_FREE (ids);
641  DDDMP_FREE (permids);
642  DDDMP_FREE (invpermids);
643  DDDMP_FREE (supportids);
644
645  return (DDDMP_SUCCESS);
646
647  failure:
648
649    if (ids != NULL) {
650      DDDMP_FREE (ids);
651    }
652    if (permids != NULL) {
653      DDDMP_FREE (permids);
654    }
655    if (invpermids != NULL) {
656      DDDMP_FREE (invpermids);
657    }
658    if (supportids != NULL) {
659      DDDMP_FREE (supportids);
660    }
661    if (support != NULL) {
662      Cudd_RecursiveDeref (ddMgr, support);
663    }
664   
665    return (DDDMP_FAILURE);
666}
667
668/*---------------------------------------------------------------------------*/
669/* Definition of static functions                                            */
670/*---------------------------------------------------------------------------*/
671
672/**Function********************************************************************
673
674  Synopsis     [Performs the recursive step of Dddmp_bddStore.]
675
676  Description  [Stores a node to file in either test or binary mode.<l>
677    In text mode a node is represented (on a text line basis) as
678    <UL>
679    <LI> node-index \[var-extrainfo\] var-index Then-index Else-index
680    </UL>
681   
682    where all indexes are integer numbers and var-extrainfo
683    (optional redundant field) is either an integer or a string
684    (variable name). Node-index is redundant (due to the node
685    ordering) but we keep it for readability.<p>
686   
687    In binary mode nodes are represented as a sequence of bytes,
688    representing var-index, Then-index, and Else-index in an
689    optimized way. Only the first byte (code) is mandatory.
690    Integer indexes are represented in absolute or relative mode,
691    where relative means offset wrt. a Then/Else node info.
692    Suppose Var(NodeId), Then(NodeId) and Else(NodeId) represent
693    infos about a given node.<p>
694   
695    The generic "NodeId" node is stored as
696
697    <UL>
698    <LI> code-byte
699    <LI> \[var-info\]
700    <LI> \[Then-info\]
701    <LI> \[Else-info\]
702    </UL>
703
704    where code-byte contains bit fields
705
706    <UL>
707    <LI>Unused  : 1 bit
708    <LI>Variable: 2 bits, one of the following codes
709    <UL>
710    <LI>DDDMP_ABSOLUTE_ID   var-info = Var(NodeId) follows
711    <LI>DDDMP_RELATIVE_ID   Var(NodeId) is represented in relative form as
712        var-info = Min(Var(Then(NodeId)),Var(Else(NodeId))) -Var(NodeId)
713    <LI>DDDMP_RELATIVE_1    No var-info follows, because
714        Var(NodeId) = Min(Var(Then(NodeId)),Var(Else(NodeId)))-1
715    <LI>DDDMP_TERMINAL      Node is a terminal, no var info required
716    </UL>
717    <LI>T       : 2 bits, with codes similar to V
718    <UL>
719    <LI>DDDMP_ABSOLUTE_ID   Then-info = Then(NodeId) follows
720    <LI>DDDMP_RELATIVE_ID   Then(NodeId) is represented in relative form as
721          Then-info = Nodeid-Then(NodeId)
722    <LI>DDDMP_RELATIVE_1    No info on Then(NodeId) follows, because
723          Then(NodeId) = NodeId-1
724    <LI>DDDMP_TERMINAL Then Node is a terminal, no info required (for BDDs)
725    </UL>
726    <LI>Ecompl  : 1 bit, if 1 means complemented edge
727    <LI>E       : 2 bits, with codes and meanings as for the Then edge
728    </UL>
729    var-info, Then-info, Else-info (if required) are represented as unsigned
730    integer values on a sufficient set of bytes (MSByte first).
731    ]
732
733  SideEffects  [None]
734
735  SeeAlso      []
736
737******************************************************************************/
738
739static int
740NodeStoreRecurBdd (
741  DdManager *ddMgr  /* IN: DD Manager */,
742  DdNode *f         /* IN: DD node to be stored */,
743  int mode          /* IN: store mode */,
744  int *supportids   /* IN: internal ids for variables */,
745  char **varnames   /* IN: names of variables: to be stored with nodes */,
746  int *outids       /* IN: output ids for variables */,
747  FILE *fp          /* IN: store file */
748  )
749{
750  DdNode *T = NULL;
751  DdNode *E = NULL;
752  int idf = (-1);
753  int idT = (-1);
754  int idE = (-1);
755  int vf = (-1);
756  int vT = (-1);
757  int vE = (-1);
758  int retValue;
759  int nVars;
760
761  nVars = ddMgr->size;
762  T = E = NULL;
763  idf = idT =  idE = (-1);
764
765#ifdef DDDMP_DEBUG
766  assert(!Cudd_IsComplement(f));
767  assert(f!=NULL);
768  assert(supportids!=NULL);
769#endif
770
771  /* If already visited, nothing to do. */
772  if (DddmpVisitedBdd (f)) {
773    return (DDDMP_SUCCESS);
774  }
775
776  /* Mark node as visited. */
777  DddmpSetVisitedBdd (f);
778
779  if (Cudd_IsConstant(f)) {
780    /* Check for special case: don't recur */
781    idf = DddmpReadNodeIndexBdd (f);
782  } else {
783
784#ifdef DDDMP_DEBUG
785    /* BDDs! Only one constant supported */
786    assert (!cuddIsConstant(f));
787#endif
788
789    /*
790     *  Recursive call for Then edge
791     */
792
793    T = cuddT(f);
794#ifdef DDDMP_DEBUG
795    /* ROBDDs! No complemented Then edge */
796    assert (!Cudd_IsComplement(T)); 
797#endif
798    /* recur */
799    retValue = NodeStoreRecurBdd (ddMgr, T, mode, supportids, varnames, outids,
800      fp);
801    if (retValue != DDDMP_SUCCESS) {
802      return (retValue);
803    }
804
805    /*
806     *  Recursive call for Else edge
807     */
808
809    E = Cudd_Regular (cuddE (f));
810    retValue = NodeStoreRecurBdd (ddMgr, E, mode, supportids, varnames, outids,
811      fp);
812    if (retValue != DDDMP_SUCCESS) {
813      return (retValue);
814    }
815
816    /*
817     *  Obtain nodeids and variable ids of f, T, E
818     */
819
820    idf = DddmpReadNodeIndexBdd (f);
821    vf = f->index;
822
823    idT = DddmpReadNodeIndexBdd (T);
824    if (Cudd_IsConstant(T)) {
825      vT = nVars;
826    } else {
827      vT = T->index;
828    }
829
830    idE = DddmpReadNodeIndexBdd (E);
831    if (Cudd_IsConstant(E)) {
832      vE = nVars;
833    } else {
834      vE = E->index;
835    }
836  }
837
838  switch (mode) {
839    case DDDMP_MODE_TEXT:
840      retValue = NodeTextStoreBdd (ddMgr, f, mode, supportids, varnames,
841        outids, fp, idf, vf, idT, idE);
842      break;
843    case DDDMP_MODE_BINARY:
844      retValue = NodeBinaryStoreBdd (ddMgr, f, mode, supportids, varnames,
845        outids, fp, idf, vf, idT, idE, vT, vE, T, E);
846      break;
847    default:
848      return (DDDMP_FAILURE);
849  }
850
851  return (retValue);
852}
853
854/**Function********************************************************************
855
856  Synopsis     [Store One Single Node in Text Format.]
857
858  Description  [Store 1 0 0 for the terminal node.
859    Store id, left child pointer, right pointer for all the other nodes.
860    ]
861
862  SideEffects  [None]
863
864  SeeAlso      [NodeBinaryStoreBdd]
865
866******************************************************************************/
867
868static int
869NodeTextStoreBdd (
870  DdManager *ddMgr  /* IN: DD Manager */,
871  DdNode *f         /* IN: DD node to be stored */,
872  int mode          /* IN: store mode */,
873  int *supportids   /* IN: internal ids for variables */,
874  char **varnames   /* IN: names of variables: to be stored with nodes */,
875  int *outids       /* IN: output ids for variables */,
876  FILE *fp          /* IN: Store file */,
877  int idf           /* IN: index of the current node */,
878  int vf            /* IN: variable of the current node */,
879  int idT           /* IN: index of the Then node */,
880  int idE           /* IN: index of the Else node */
881  )
882{
883  int retValue = EOF;
884
885  /*
886   *  Check for Constant
887   */
888
889  if (Cudd_IsConstant(f)) {
890
891    if (f == Cudd_ReadOne(ddMgr)) {
892      if ((varnames != NULL) || (outids != NULL)) {
893        retValue = fprintf (fp, "%d T 1 0 0\n", idf);
894      } else {
895        retValue = fprintf (fp, "%d 1 0 0\n", idf);
896      }
897
898      if (retValue == EOF) {
899        return (DDDMP_FAILURE);
900      } else {
901        return (DDDMP_SUCCESS);
902      }
903    }
904
905    if (f == Cudd_ReadZero(ddMgr)) {
906      if ((varnames != NULL) || (outids != NULL)) {
907        retValue = fprintf (fp, "%d T 0 0 0\n", idf);
908      } else {
909        retValue = fprintf (fp, "%d 0 0 0\n", idf);
910      }
911
912      if (retValue == EOF) {
913        return (DDDMP_FAILURE);
914      } else {
915        return (DDDMP_SUCCESS);
916      }
917    }
918
919    /*
920     *  A constant node different from 1: an ADD constant
921     */
922
923    Dddmp_CheckAndReturn (((varnames!=NULL)||(outids!=NULL)),
924      "Error writing to file: ADD Type.");
925
926    if (retValue == EOF) {
927      return (DDDMP_FAILURE);
928    } else {
929      return (DDDMP_SUCCESS);
930    }
931  }
932
933  /*
934   *  ... Not A Constant
935   */
936
937  if (Cudd_IsComplement (cuddE(f))) {
938    idE = -idE;
939  }
940
941  if (varnames != NULL) {   
942    retValue = fprintf (fp, "%d %s %d %d %d\n",
943       idf, varnames[vf], supportids[vf], idT, idE);
944
945    if (retValue == EOF) {
946      return (DDDMP_FAILURE);
947    } else {
948      return (DDDMP_SUCCESS);
949    }
950  }
951
952  if (outids != NULL) {   
953    retValue = fprintf (fp, "%d %d %d %d %d\n",
954       idf, outids[vf], supportids[vf], idT, idE);
955
956    if (retValue == EOF) {
957      return (DDDMP_FAILURE);
958    } else {
959      return (DDDMP_SUCCESS);
960    }
961    }
962
963  retValue = fprintf (fp, "%d %d %d %d\n",
964    idf, supportids[vf], idT, idE);
965
966  if (retValue == EOF) {
967    return (DDDMP_FAILURE);
968  } else {
969    return (DDDMP_SUCCESS);
970  }
971}
972
973/**Function********************************************************************
974
975  Synopsis     [Store One Single Node in Binary Format.]
976
977  Description  [Store 1 0 0 for the terminal node.
978    Store id, left child pointer, right pointer for all the other nodes.
979    Store every information as coded binary values.]
980
981  SideEffects  [None]
982
983  SeeAlso      [NodeTextStoreBdd]
984
985******************************************************************************/
986
987static int
988NodeBinaryStoreBdd (
989  DdManager *ddMgr  /* IN: DD Manager */,
990  DdNode *f         /* IN: DD node to be stored */,
991  int mode          /* IN: store mode */,
992  int *supportids   /* IN: internal ids for variables */,
993  char **varnames   /* IN: names of variables: to be stored with nodes */,
994  int *outids       /* IN: output ids for variables */,
995  FILE *fp          /* IN: store file */,
996  int idf           /* IN: index of the node */,
997  int vf            /* IN: variable of the node */,
998  int idT           /* IN: index of the Then node */,
999  int idE           /* IN: index of the Else node */,
1000  int vT            /* IN: variable of the Then node */,
1001  int vE            /* IN: variable of the Else node */,
1002  DdNode *T         /* IN: Then node */,
1003  DdNode *E         /* IN: Else node */
1004  )
1005{
1006  int retValue, diff, var;
1007  struct binary_dd_code code;
1008
1009  /*
1010   *  Check for Constant
1011   */
1012
1013  /* only integer ids used, varnames ignored */
1014  /* Terminal one is coded as DDDMP_TERMINAL, all other fields are 0 */
1015  if (Cudd_IsConstant(f)) {
1016    code.Unused = 0;
1017    code.V = DDDMP_TERMINAL;
1018    code.T = 0;
1019    code.E = 0;
1020    code.Ecompl = 0;
1021    retValue = DddmpWriteCode (fp,code);
1022    if (retValue == EOF) {
1023      return (DDDMP_FAILURE);
1024    } else {
1025      return (DDDMP_SUCCESS);
1026    }
1027  }
1028
1029  /*
1030   * Non terminal: output variable id
1031   */
1032
1033  var = supportids[vf];
1034  diff = (supportids[vT]<supportids[vE]) ? 
1035    (supportids[vT]-var) : (supportids[vE]-var);
1036  code.V = DDDMP_ABSOLUTE_ID;
1037
1038  if (diff <= var) {
1039    if (diff == 1) {
1040      code.V = DDDMP_RELATIVE_1;
1041    } else {
1042      code.V = DDDMP_RELATIVE_ID;
1043      var = diff;
1044    } 
1045  }
1046
1047  if (T == DD_ONE(ddMgr)) {
1048    code.T = DDDMP_TERMINAL;
1049  } else {
1050    /* compute displacement */
1051    diff = idf - idT;
1052    code.T = DDDMP_ABSOLUTE_ID;
1053    if (diff <= idT) {
1054      if (diff == 1) {
1055         code.T = DDDMP_RELATIVE_1;
1056      } else {
1057         code.T = DDDMP_RELATIVE_ID;
1058         idT = diff;
1059      } 
1060    }
1061  }
1062
1063  if (E == DD_ONE(ddMgr)) {
1064    code.E = DDDMP_TERMINAL;
1065  } else {
1066    /* compute displacement */
1067    diff = idf - idE;
1068    code.E = DDDMP_ABSOLUTE_ID;
1069    if (diff <= idE) {
1070      if (diff == 1) {
1071        code.E = DDDMP_RELATIVE_1;
1072      } else {
1073        code.E = DDDMP_RELATIVE_ID;
1074        idE = diff;
1075      } 
1076    }
1077  }
1078
1079  if (Cudd_IsComplement(cuddE(f))) {
1080    code.Ecompl = 1;
1081  } else {
1082    code.Ecompl = 0;
1083  }
1084
1085  retValue = DddmpWriteCode (fp,code);
1086 
1087  if (retValue == EOF) {
1088    return (DDDMP_FAILURE);
1089  }
1090
1091  if ((code.V == DDDMP_ABSOLUTE_ID) || (code.V == DDDMP_RELATIVE_ID)) { 
1092    retValue = DddmpWriteInt (fp, var);
1093    if (retValue == EOF) {
1094      return (DDDMP_FAILURE);
1095    }
1096  }
1097
1098  if ((code.T == DDDMP_ABSOLUTE_ID) || (code.T == DDDMP_RELATIVE_ID)) { 
1099    retValue = DddmpWriteInt(fp,idT);
1100    if (retValue == EOF) {
1101      return (DDDMP_FAILURE);
1102    }
1103  }
1104
1105  if ((code.E == DDDMP_ABSOLUTE_ID) || (code.E == DDDMP_RELATIVE_ID)) { 
1106    retValue = DddmpWriteInt(fp,idE);
1107    if (retValue == EOF) {
1108      return (DDDMP_FAILURE);
1109    }
1110  }
1111
1112  return (retValue);
1113}
1114
Note: See TracBrowser for help on using the repository browser.