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