source: icGREP/icgrep-devel/cudd-2.5.1/dddmp/dddmpStoreMisc.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: 47.6 KB
Line 
1/**CFile**********************************************************************
2
3  FileName     [dddmpStoreMisc.c]
4
5  PackageName  [dddmp]
6
7  Synopsis     [Functions to write out bdds to file in prefixed
8    and in Blif form.]
9
10  Description  [Functions to write out bdds to file.
11    BDDs are represended on file in text format.
12    Each node is stored as a multiplexer in a prefix notation format for
13    the prefix notation file or in PLA format for the blif file.
14  ]
15
16  Author       [Gianpiero Cabodi and Stefano Quer]
17
18  Copyright    [
19    Copyright (c) 2004 by Politecnico di Torino.
20    All Rights Reserved. This software is for educational purposes only.
21    Permission is given to academic institutions to use, copy, and modify
22    this software and its documentation provided that this introductory
23    message is not removed, that this software and its documentation is
24    used for the institutions' internal research and educational purposes,
25    and that no monies are exchanged. No guarantee is expressed or implied
26    by the distribution of this code.
27    Send bug-reports and/or questions to:
28    {gianpiero.cabodi,stefano.quer}@polito.it.
29    ]
30
31******************************************************************************/
32
33#include "dddmpInt.h"
34
35/*---------------------------------------------------------------------------*/
36/* Stucture declarations                                                     */
37/*---------------------------------------------------------------------------*/
38
39/*---------------------------------------------------------------------------*/
40/* Type declarations                                                         */
41/*---------------------------------------------------------------------------*/
42
43/*---------------------------------------------------------------------------*/
44/* Variable declarations                                                     */
45/*---------------------------------------------------------------------------*/
46
47/*---------------------------------------------------------------------------*/
48/* Macro declarations                                                        */
49/*---------------------------------------------------------------------------*/
50
51/**AutomaticStart*************************************************************/
52
53/*---------------------------------------------------------------------------*/
54/* Static function prototypes                                                */
55/*---------------------------------------------------------------------------*/
56
57static int DddmpCuddDdArrayStorePrefix(DdManager *ddMgr, int n, DdNode **f, char **inputNames, char **outputNames, char *modelName, FILE *fp);
58static int DddmpCuddDdArrayStorePrefixBody(DdManager *ddMgr, int n, DdNode **f, char **inputNames, char **outputNames, FILE *fp);
59static int DddmpCuddDdArrayStorePrefixStep(DdManager * ddMgr, DdNode * f, FILE * fp, st_table * visited, char ** names);
60static int DddmpCuddDdArrayStoreBlif(DdManager *ddMgr, int n, DdNode **f, char **inputNames, char **outputNames, char *modelName, FILE *fp);
61static int DddmpCuddDdArrayStoreBlifBody(DdManager *ddMgr, int n, DdNode **f, char **inputNames, char **outputNames, FILE *fp);
62static int DddmpCuddDdArrayStoreBlifStep(DdManager *ddMgr, DdNode *f, FILE *fp, st_table *visited, char **names);
63static int DddmpCuddDdArrayStoreSmv(DdManager *ddMgr, int n, DdNode **f, char **inputNames, char **outputNames, char *modelName, FILE *fp);
64static int DddmpCuddDdArrayStoreSmvBody(DdManager *ddMgr, int n, DdNode **f, char **inputNames, char **outputNames, FILE *fp);
65static int DddmpCuddDdArrayStoreSmvStep(DdManager * ddMgr, DdNode * f, FILE * fp, st_table * visited, char ** names);
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 in
76    a prefix notation.]
77
78  Description  [Dumps the argument BDD to file.
79    Dumping is done through Dddmp_cuddBddArrayStorePrefix.
80    A dummy array of 1 BDD root is used for this purpose.
81    ]
82
83  SideEffects  []
84
85  SeeAlso      [Dddmp_cuddBddStore]
86
87******************************************************************************/
88
89int
90Dddmp_cuddBddStorePrefix (
91  DdManager *ddMgr     /* IN: DD Manager */,
92  int nRoots           /* IN: Number of BDD roots */,
93  DdNode *f            /* IN: BDD root to be stored */,
94  char **inputNames    /* IN: Array of variable names */,
95  char **outputNames   /* IN: Array of root names */,
96  char *modelName      /* IN: Model Name */,
97  char *fileName       /* IN: File name */,
98  FILE *fp             /* IN: File pointer to the store file */
99  )
100{
101  int retValue;
102  DdNode *tmpArray[1];
103
104  tmpArray[0] = f;
105
106  retValue = Dddmp_cuddBddArrayStorePrefix (ddMgr, 1, tmpArray,
107    inputNames, outputNames, modelName, fileName, fp);
108
109  return (retValue);
110}
111
112/**Function********************************************************************
113
114  Synopsis     [Writes a dump file representing the argument BDD in
115    a prefix notation.]
116
117  Description  [Dumps the argument BDD to file.
118    Dumping is done through Dddmp_cuddBddArrayStorePrefix.
119    A dummy array of 1 BDD root is used for this purpose.
120    ]
121
122  SideEffects  []
123
124  SeeAlso      [Dddmp_cuddBddArrayStore]
125
126******************************************************************************/
127
128int
129Dddmp_cuddBddArrayStorePrefix (
130  DdManager *ddMgr       /* IN: DD Manager */,
131  int nroots             /* IN: number of output BDD roots to be stored */,
132  DdNode **f             /* IN: array of BDD roots to be stored */,
133  char **inputNames      /* IN: array of variable names (or NULL) */,
134  char **outputNames     /* IN: array of root names (or NULL) */,
135  char *modelName        /* IN: Model Name */,
136  char *fname            /* IN: File name */,
137  FILE *fp               /* IN: File pointer to the store file */
138  )
139{
140  int retValue;
141  int fileToClose = 0;
142
143#ifdef DDDMP_DEBUG
144#ifndef __alpha__ 
145  int retValueBis;
146
147  retValueBis = Cudd_DebugCheck (ddMgr);
148  if (retValueBis == 1) {
149    fprintf (stderr, "Inconsistency Found During BDD Store.\n");
150    fflush (stderr);
151  } else {
152    if (retValueBis == CUDD_OUT_OF_MEM) {
153      fprintf (stderr, "Out of Memory During BDD Store.\n");
154      fflush (stderr);
155    }
156  }
157#endif
158#endif
159
160  /*
161   *  Check if File needs to be opened in the proper mode.
162   */
163
164  if (fp == NULL) {
165    fp = fopen (fname, "w");
166    Dddmp_CheckAndGotoLabel (fp==NULL, "Error opening file.",
167      failure);
168    fileToClose = 1;
169  }
170
171  retValue = DddmpCuddDdArrayStorePrefix (ddMgr, nroots, f,
172    inputNames, outputNames, modelName, fp);
173
174  if (fileToClose) {
175    fclose (fp);
176  }
177
178#ifdef DDDMP_DEBUG
179#ifndef __alpha__ 
180  retValueBis = Cudd_DebugCheck (ddMgr);
181  if (retValueBis == 1) {
182    fprintf (stderr, "Inconsistency Found During BDD Store.\n");
183    fflush (stderr);
184  } else {
185    if (retValueBis == CUDD_OUT_OF_MEM) {
186      fprintf (stderr, "Out of Memory During BDD Store.\n");
187      fflush (stderr);
188    }
189  }
190#endif
191#endif
192
193  return (retValue);
194
195  failure:
196    return (DDDMP_FAILURE);
197}
198
199/**Function********************************************************************
200
201  Synopsis     [Writes a dump file representing the argument BDD in
202    a Blif/Exlif notation.]
203
204  Description  [Dumps the argument BDD to file.
205    Dumping is done through Dddmp_cuddBddArrayStoreBlif.
206    A dummy array of 1 BDD root is used for this purpose.
207    ]
208
209  SideEffects  []
210
211  SeeAlso      [Dddmp_cuddBddStorePrefix]
212
213******************************************************************************/
214
215int
216Dddmp_cuddBddStoreBlif (
217  DdManager *ddMgr     /* IN: DD Manager */,
218  int nRoots           /* IN: Number of BDD roots */,
219  DdNode *f            /* IN: BDD root to be stored */,
220  char **inputNames    /* IN: Array of variable names */,
221  char **outputNames   /* IN: Array of root names */,
222  char *modelName      /* IN: Model Name */,
223  char *fileName       /* IN: File name */,
224  FILE *fp             /* IN: File pointer to the store file */
225  )
226{
227  int retValue;
228  DdNode *tmpArray[1];
229
230  tmpArray[0] = f;
231
232  retValue = Dddmp_cuddBddArrayStoreBlif (ddMgr, 1, tmpArray,
233    inputNames, outputNames, modelName, fileName, fp);
234
235  return (retValue);
236}
237
238/**Function********************************************************************
239
240  Synopsis     [Writes a dump file representing the argument BDD in
241    a Blif/Exlif notation.]
242
243  Description  [Dumps the argument BDD to file.
244    Dumping is done through Dddmp_cuddBddArrayStoreBLif.
245    A dummy array of 1 BDD root is used for this purpose.
246    ]
247
248  SideEffects  []
249
250  SeeAlso      [Dddmp_cuddBddArrayStorePrefix]
251
252******************************************************************************/
253
254int
255Dddmp_cuddBddArrayStoreBlif (
256  DdManager *ddMgr       /* IN: DD Manager */,
257  int nroots             /* IN: number of output BDD roots to be stored */,
258  DdNode **f             /* IN: array of BDD roots to be stored */,
259  char **inputNames      /* IN: array of variable names (or NULL) */,
260  char **outputNames     /* IN: array of root names (or NULL) */,
261  char *modelName        /* IN: Model Name */,
262  char *fname            /* IN: File name */,
263  FILE *fp               /* IN: File pointer to the store file */
264  )
265{
266  int retValue;
267  int fileToClose = 0;
268
269#ifdef DDDMP_DEBUG
270#ifndef __alpha__ 
271  int retValueBis;
272
273  retValueBis = Cudd_DebugCheck (ddMgr);
274  if (retValueBis == 1) {
275    fprintf (stderr, "Inconsistency Found During BDD Store.\n");
276    fflush (stderr);
277  } else {
278    if (retValueBis == CUDD_OUT_OF_MEM) {
279      fprintf (stderr, "Out of Memory During BDD Store.\n");
280      fflush (stderr);
281    }
282  }
283#endif
284#endif
285
286  /*
287   *  Check if File needs to be opened in the proper mode.
288   */
289
290  if (fp == NULL) {
291    fp = fopen (fname, "w");
292    Dddmp_CheckAndGotoLabel (fp==NULL, "Error opening file.",
293      failure);
294    fileToClose = 1;
295  }
296
297  retValue = DddmpCuddDdArrayStoreBlif (ddMgr, nroots, f,
298    inputNames, outputNames, modelName, fp);
299
300  if (fileToClose) {
301    fclose (fp);
302  }
303
304#ifdef DDDMP_DEBUG
305#ifndef __alpha__ 
306  retValueBis = Cudd_DebugCheck (ddMgr);
307  if (retValueBis == 1) {
308    fprintf (stderr, "Inconsistency Found During BDD Store.\n");
309    fflush (stderr);
310  } else {
311    if (retValueBis == CUDD_OUT_OF_MEM) {
312      fprintf (stderr, "Out of Memory During BDD Store.\n");
313      fflush (stderr);
314    }
315  }
316#endif
317#endif
318
319  return (retValue);
320
321  failure:
322    return (DDDMP_FAILURE);
323}
324
325/**Function********************************************************************
326
327  Synopsis     [Writes a dump file representing the argument BDD in
328    a prefix notation.]
329
330  Description  [Dumps the argument BDD to file.
331    Dumping is done through Dddmp_cuddBddArrayStorePrefix.
332    A dummy array of 1 BDD root is used for this purpose.
333    ]
334
335  SideEffects  []
336
337  SeeAlso      [Dddmp_cuddBddStore]
338
339******************************************************************************/
340
341int
342Dddmp_cuddBddStoreSmv (
343  DdManager *ddMgr     /* IN: DD Manager */,
344  int nRoots           /* IN: Number of BDD roots */,
345  DdNode *f            /* IN: BDD root to be stored */,
346  char **inputNames    /* IN: Array of variable names */,
347  char **outputNames   /* IN: Array of root names */,
348  char *modelName      /* IN: Model Name */,
349  char *fileName       /* IN: File name */,
350  FILE *fp             /* IN: File pointer to the store file */
351  )
352{
353  int retValue;
354  DdNode *tmpArray[1];
355
356  tmpArray[0] = f;
357
358  retValue = Dddmp_cuddBddArrayStoreSmv (ddMgr, 1, tmpArray,
359    inputNames, outputNames, modelName, fileName, fp);
360
361  return (retValue);
362}
363
364/**Function********************************************************************
365
366  Synopsis     [Writes a dump file representing the argument BDD in
367    a prefix notation.]
368
369  Description  [Dumps the argument BDD to file.
370    Dumping is done through Dddmp_cuddBddArrayStorePrefix.
371    A dummy array of 1 BDD root is used for this purpose.
372    ]
373
374  SideEffects  []
375
376  SeeAlso      [Dddmp_cuddBddArrayStore]
377
378******************************************************************************/
379
380int
381Dddmp_cuddBddArrayStoreSmv (
382  DdManager *ddMgr       /* IN: DD Manager */,
383  int nroots             /* IN: number of output BDD roots to be stored */,
384  DdNode **f             /* IN: array of BDD roots to be stored */,
385  char **inputNames      /* IN: array of variable names (or NULL) */,
386  char **outputNames     /* IN: array of root names (or NULL) */,
387  char *modelName        /* IN: Model Name */,
388  char *fname            /* IN: File name */,
389  FILE *fp               /* IN: File pointer to the store file */
390  )
391{
392  int retValue;
393  int fileToClose = 0;
394
395#ifdef DDDMP_DEBUG
396#ifndef __alpha__ 
397  int retValueBis;
398
399  retValueBis = Cudd_DebugCheck (ddMgr);
400  if (retValueBis == 1) {
401    fprintf (stderr, "Inconsistency Found During BDD Store.\n");
402    fflush (stderr);
403  } else {
404    if (retValueBis == CUDD_OUT_OF_MEM) {
405      fprintf (stderr, "Out of Memory During BDD Store.\n");
406      fflush (stderr);
407    }
408  }
409#endif
410#endif
411
412  /*
413   *  Check if File needs to be opened in the proper mode.
414   */
415
416  if (fp == NULL) {
417    fp = fopen (fname, "w");
418    Dddmp_CheckAndGotoLabel (fp==NULL, "Error opening file.",
419      failure);
420    fileToClose = 1;
421  }
422
423  retValue = DddmpCuddDdArrayStoreSmv (ddMgr, nroots, f,
424    inputNames, outputNames, modelName, fp);
425
426  if (fileToClose) {
427    fclose (fp);
428  }
429
430#ifdef DDDMP_DEBUG
431#ifndef __alpha__ 
432  retValueBis = Cudd_DebugCheck (ddMgr);
433  if (retValueBis == 1) {
434    fprintf (stderr, "Inconsistency Found During BDD Store.\n");
435    fflush (stderr);
436  } else {
437    if (retValueBis == CUDD_OUT_OF_MEM) {
438      fprintf (stderr, "Out of Memory During BDD Store.\n");
439      fflush (stderr);
440    }
441  }
442#endif
443#endif
444
445  return (retValue);
446
447  failure:
448    return (DDDMP_FAILURE);
449}
450
451/*---------------------------------------------------------------------------*/
452/* Definition of static functions                                            */
453/*---------------------------------------------------------------------------*/
454
455/**Function********************************************************************
456
457  Synopsis     [Internal function to writes a dump file representing the
458    argument BDD in a prefix notation.]
459
460  Description  [One multiplexer is written for each BDD node.
461    It returns 1 in case of success; 0 otherwise (e.g., out-of-memory, file
462    system full, or an ADD with constants different from 0 and 1).
463    It does not close the file: This is the caller responsibility.
464    It uses a minimal unique subset of the hexadecimal address of a node as
465    name for it.
466    If the argument inputNames is non-null, it is assumed to hold the
467    pointers to the names of the inputs. Similarly for outputNames.
468    For each BDD node of function f, variable v, then child T, and else
469    child E it stores:
470    f = v * T + v' * E
471    that is
472    (OR f (AND v T) (AND (NOT v) E))
473    If E is a complemented child this results in the following
474    (OR f (AND v T) (AND (NOT v) (NOT E)))
475    Comments (COMMENT) are added at the beginning of the description to
476    describe inputs and outputs of the design.
477    A buffer (BUF) is add on the output to cope with complemented functions.
478    ]
479
480  SideEffects [None]
481
482  SeeAlso     [DddmpCuddDdArrayStoreBlif]
483
484******************************************************************************/
485
486static int
487DddmpCuddDdArrayStorePrefix (
488  DdManager *ddMgr    /* IN: Manager */,
489  int n               /* IN: Number of output nodes to be dumped */,
490  DdNode **f          /* IN: Array of output nodes to be dumped */,
491  char **inputNames   /* IN: Array of input names (or NULL) */,
492  char **outputNames  /* IN: Array of output names (or NULL) */,
493  char *modelName     /* IN: Model name (or NULL) */,
494  FILE *fp            /* IN: Pointer to the dump file */
495  )
496{
497  DdNode *support = NULL;
498  DdNode *scan;
499  int *sorted = NULL;
500  int nVars = ddMgr->size;
501  int retValue;
502  int i;
503
504  /* Build a bit array with the support of f. */
505  sorted = ALLOC(int, nVars);
506  if (sorted == NULL) {
507    ddMgr->errorCode = CUDD_MEMORY_OUT;
508    Dddmp_CheckAndGotoLabel (1, "Allocation Error.", failure);
509  }
510  for (i = 0; i < nVars; i++) {
511    sorted[i] = 0;
512  }
513
514  /* Take the union of the supports of each output function. */
515  support = Cudd_VectorSupport(ddMgr,f,n);
516  Dddmp_CheckAndGotoLabel (support==NULL,
517    "Error in function Cudd_VectorSupport.", failure);
518  cuddRef(support);
519  scan = support;
520  while (!cuddIsConstant(scan)) {
521    sorted[scan->index] = 1;
522    scan = cuddT(scan);
523  }
524  Cudd_RecursiveDeref(ddMgr,support);
525  /* so that we do not try to free it in case of failure */
526  support = NULL;
527
528  /* Write the header (.model .inputs .outputs). */
529  if (modelName == NULL) {
530    retValue = fprintf (fp, "(COMMENT - model name: Unknown )\n");
531  } else {
532    retValue = fprintf (fp, "(COMMENT - model name: %s )\n", modelName);
533  }
534  if (retValue == EOF) {
535    return(0);
536  }
537
538  retValue = fprintf(fp, "(COMMENT - input names: ");
539  if (retValue == EOF) {
540    return(0);
541  }
542  /* Write the input list by scanning the support array. */
543  for (i = 0; i < nVars; i++) {
544    if (sorted[i]) {
545      if (inputNames == NULL) {
546        retValue = fprintf(fp," inNode%d", i);
547      } else {
548        retValue = fprintf(fp," %s", inputNames[i]);
549      }
550      Dddmp_CheckAndGotoLabel (retValue==EOF,
551        "Error during file store.", failure);
552    }
553  }
554  FREE(sorted);
555  sorted = NULL;
556  retValue = fprintf(fp, " )\n");
557  if (retValue == EOF) {
558    return(0);
559  }
560
561  /* Write the .output line. */
562  retValue = fprintf(fp,"(COMMENT - output names: ");
563  if (retValue == EOF) {
564    return(0);
565  }
566  for (i = 0; i < n; i++) {
567    if (outputNames == NULL) {
568      retValue = fprintf (fp," outNode%d", i);
569    } else {
570      retValue = fprintf (fp," %s", outputNames[i]);
571    }
572    Dddmp_CheckAndGotoLabel (retValue==EOF,
573      "Error during file store.", failure);
574  } 
575  retValue = fprintf(fp, " )\n");
576  Dddmp_CheckAndGotoLabel (retValue==EOF,
577    "Error during file store.", failure);
578
579  retValue = DddmpCuddDdArrayStorePrefixBody (ddMgr, n, f, inputNames,
580    outputNames, fp);
581  Dddmp_CheckAndGotoLabel (retValue==0,
582    "Error in function DddmpCuddDdArrayStorePrefixBody.", failure);
583
584  return(1);
585
586failure:
587    if (sorted != NULL) {
588      FREE(sorted);
589    }
590    if (support != NULL) {
591      Cudd_RecursiveDeref(ddMgr,support);
592    }
593    return(0);
594}
595
596/**Function********************************************************************
597
598  Synopsis     [Internal function to writes a dump file representing the
599    argument BDD in a prefix notation. Writes the body of the file.]
600
601  Description  [One multiplexer is written for each BDD node.
602    It returns 1 in case of success; 0 otherwise (e.g., out-of-memory, file
603    system full, or an ADD with constants different from 0 and 1).
604    It does not close the file: This is the caller responsibility.
605    It uses a minimal unique subset of the hexadecimal address of a node as
606    name for it.
607    If the argument inputNames is non-null, it is assumed to hold the
608    pointers to the names of the inputs. Similarly for outputNames.
609    For each BDD node of function f, variable v, then child T, and else
610    child E it stores:
611    f = v * T + v' * E
612    that is
613    (OR f (AND v T) (AND (NOT v) E))
614    If E is a complemented child this results in the following
615    (OR f (AND v T) (AND (NOT v) (NOT E)))
616    ]
617
618  SideEffects [None]
619
620  SeeAlso     [DddmpCuddDdArrayStoreBlif]
621
622******************************************************************************/
623
624static int
625DddmpCuddDdArrayStorePrefixBody (
626  DdManager *ddMgr      /* IN: Manager */,
627  int n                 /* IN: Number of output nodes to be dumped */,
628  DdNode **f            /* IN: Array of output nodes to be dumped */,
629  char **inputNames     /* IN: Array of input names (or NULL) */,
630  char **outputNames    /* IN: Array of output names (or NULL) */,
631  FILE *fp              /* IN: Pointer to the dump file */
632  )
633{
634  st_table *visited = NULL;
635  int retValue;
636  int i;
637
638  /* Initialize symbol table for visited nodes. */
639  visited = st_init_table(st_ptrcmp, st_ptrhash);
640  Dddmp_CheckAndGotoLabel (visited==NULL,
641    "Error if function st_init_table.", failure);
642
643  /* Call the function that really gets the job done. */
644  for (i = 0; i < n; i++) {
645    retValue = DddmpCuddDdArrayStorePrefixStep (ddMgr, Cudd_Regular(f[i]),
646      fp, visited, inputNames);
647    Dddmp_CheckAndGotoLabel (retValue==0,
648      "Error if function DddmpCuddDdArrayStorePrefixStep.", failure);
649  }
650
651  /* To account for the possible complement on the root,
652   ** we put either a buffer or an inverter at the output of
653   ** the multiplexer representing the top node.
654   */
655  for (i=0; i<n; i++) {
656    if (outputNames == NULL) {
657      retValue = fprintf (fp,  "(BUF outNode%d ", i);
658    } else {
659      retValue = fprintf (fp,  "(BUF %s ", outputNames[i]);
660    }
661    Dddmp_CheckAndGotoLabel (retValue==EOF,
662      "Error during file store.", failure);
663
664    if (Cudd_IsComplement(f[i])) {
665#if SIZEOF_VOID_P == 8
666      retValue = fprintf (fp, "(NOT node%lx))\n",
667        (unsigned long) f[i] / (unsigned long) sizeof(DdNode));
668#else
669      retValue = fprintf (fp, "(NOT node%x))\n",
670        (unsigned) f[i] / (unsigned) sizeof(DdNode));
671#endif
672    } else {
673#if SIZEOF_VOID_P == 8
674      retValue = fprintf (fp, "node%lx)\n",
675        (unsigned long) f[i] / (unsigned long) sizeof(DdNode));
676#else
677      retValue = fprintf (fp, "node%x)\n",
678        (unsigned) f[i] / (unsigned) sizeof(DdNode));
679#endif
680    }
681    Dddmp_CheckAndGotoLabel (retValue==EOF,
682      "Error during file store.", failure);
683  }
684
685  st_free_table (visited);
686
687  return(1);
688
689failure:
690    if (visited != NULL) st_free_table(visited);
691    return(0);
692
693}
694
695/**Function********************************************************************
696
697  Synopsis    [Performs the recursive step of
698    DddmpCuddDdArrayStorePrefixBody.]
699
700  Description [Performs the recursive step of
701    DddmpCuddDdArrayStorePrefixBody.
702    Traverses the BDD f and writes a multiplexer-network description to the
703    file pointed by fp.
704    For each BDD node of function f, variable v, then child T, and else
705    child E it stores:
706    f = v * T + v' * E
707    that is
708    (OR f (AND v T) (AND (NOT v) E))
709    If E is a complemented child this results in the following
710    (OR f (AND v T) (AND (NOT v) (NOT E)))
711    f is assumed to be a regular pointer and the function guarantees this
712    assumption in the recursive calls.
713    ]
714
715  SideEffects [None]
716
717  SeeAlso     []
718
719******************************************************************************/
720
721static int
722DddmpCuddDdArrayStorePrefixStep (
723  DdManager * ddMgr,
724  DdNode * f,
725  FILE * fp,
726  st_table * visited,
727  char ** names
728  )
729{
730  DdNode *T, *E;
731  int retValue;
732
733#ifdef DDDMP_DEBUG
734  assert(!Cudd_IsComplement(f));
735#endif
736
737  /* If already visited, nothing to do. */
738  if (st_is_member(visited, (char *) f) == 1) {
739    return(1);
740  }
741
742  /* Check for abnormal condition that should never happen. */
743  if (f == NULL) {
744    return(0);
745  }
746
747  /* Mark node as visited. */
748  if (st_insert(visited, (char *) f, NULL) == ST_OUT_OF_MEM) {
749    return(0);
750  }
751
752  /* Check for special case: If constant node, generate constant 1. */
753  if (f == DD_ONE (ddMgr)) {
754#if SIZEOF_VOID_P == 8
755    retValue = fprintf (fp,
756      "(OR node%lx vss vdd)\n",
757      (unsigned long) f / (unsigned long) sizeof(DdNode));
758#else
759    retValue = fprintf (fp,
760      "(OR node%x vss vdd)\n",
761      (unsigned) f / (unsigned) sizeof(DdNode));
762#endif
763    if (retValue == EOF) {
764       return(0);
765    } else {
766       return(1);
767    }
768  }
769
770  /*
771   *  Check whether this is an ADD. We deal with 0-1 ADDs, but not
772   *  with the general case.
773   */
774
775  if (f == DD_ZERO(ddMgr)) {
776#if SIZEOF_VOID_P == 8
777    retValue = fprintf (fp,
778      "(AND node%lx vss vdd)\n",
779       (unsigned long) f / (unsigned long) sizeof(DdNode));
780#else
781    retValue = fprintf (fp,
782      "(AND node%x vss vdd)\n",
783      (unsigned) f / (unsigned) sizeof(DdNode));
784#endif
785   if (retValue == EOF) {
786     return(0);
787   } else {
788     return(1);
789   }
790  }
791
792  if (cuddIsConstant(f)) {
793    return(0);
794  }
795
796  /* Recursive calls. */
797  T = cuddT(f);
798  retValue = DddmpCuddDdArrayStorePrefixStep (ddMgr,T,fp,visited,names);
799  if (retValue != 1) {
800    return(retValue);
801  }
802  E = Cudd_Regular(cuddE(f));
803  retValue = DddmpCuddDdArrayStorePrefixStep (ddMgr,E,fp,visited,names);
804  if (retValue != 1) {
805    return(retValue);
806  }
807
808  /* Write multiplexer taking complement arc into account. */
809#if SIZEOF_VOID_P == 8
810  retValue = fprintf (fp, "(OR node%lx (AND ",
811    (unsigned long) f / (unsigned long) sizeof(DdNode));
812#else
813  retValue = fprintf (fp, "(OR node%x (AND ",
814    (unsigned) f / (unsigned) sizeof(DdNode));
815#endif
816  if (retValue == EOF) {
817    return(0);
818  }
819
820  if (names != NULL) {
821    retValue = fprintf(fp, "%s ", names[f->index]);
822  } else {
823    retValue = fprintf(fp, "inNode%d ", f->index);
824  }
825  if (retValue == EOF) {
826    return(0);
827  }
828
829#if SIZEOF_VOID_P == 8
830  retValue = fprintf (fp, "node%lx) (AND (NOT ",
831    (unsigned long) T / (unsigned long) sizeof(DdNode));
832#else
833  retValue = fprintf (fp, "node%x) (AND (NOT ",
834    (unsigned) T / (unsigned) sizeof(DdNode));
835#endif
836  if (retValue == EOF) {
837    return(0);
838  }
839
840  if (names != NULL) {
841    retValue = fprintf (fp, "%s", names[f->index]);
842  } else {
843    retValue = fprintf (fp, "inNode%d", f->index);
844  }
845  if (retValue == EOF) {
846    return(0);
847  }
848
849#if SIZEOF_VOID_P == 8
850  if (Cudd_IsComplement(cuddE(f))) {
851    retValue = fprintf (fp, ") (NOT node%lx)))\n",
852      (unsigned long) E / (unsigned long) sizeof(DdNode));
853  } else {
854    retValue = fprintf (fp, ") node%lx))\n",
855      (unsigned long) E / (unsigned long) sizeof(DdNode));
856  }
857#else
858  if (Cudd_IsComplement(cuddE(f))) {
859    retValue = fprintf (fp, ") (NOT node%x)))\n",
860      (unsigned) E / (unsigned) sizeof(DdNode));
861  } else {
862    retValue = fprintf (fp, ") node%x))\n",
863      (unsigned) E / (unsigned) sizeof(DdNode));
864  }
865#endif
866
867  if (retValue == EOF) {
868    return(0);
869  } else {
870    return(1);
871  }
872}
873
874/**Function********************************************************************
875
876  Synopsis    [Writes a blif file representing the argument BDDs.]
877
878  Description [Writes a blif file representing the argument BDDs as a
879    network of multiplexers. One multiplexer is written for each BDD
880    node. It returns 1 in case of success; 0 otherwise (e.g.,
881    out-of-memory, file system full, or an ADD with constants different
882    from 0 and 1).
883    DddmpCuddDdArrayStoreBlif does not close the file: This is the
884    caller responsibility.
885    DddmpCuddDdArrayStoreBlif uses a minimal unique subset of
886    the hexadecimal address of a node as name for it.  If the argument
887    inames is non-null, it is assumed to hold the pointers to the names
888    of the inputs. Similarly for outputNames.
889    It prefixes the string "NODE" to each nome to have "regular" names
890    for each elements.
891    ]
892
893  SideEffects [None]
894
895  SeeAlso     [DddmpCuddDdArrayStoreBlifBody,Cudd_DumpBlif]
896
897******************************************************************************/
898
899static int
900DddmpCuddDdArrayStoreBlif (
901  DdManager *ddMgr    /* IN: Manager */,
902  int n               /* IN: Number of output nodes to be dumped */,
903  DdNode **f          /* IN: Array of output nodes to be dumped */,
904  char **inputNames   /* IN: Array of input names (or NULL) */,
905  char **outputNames  /* IN: Array of output names (or NULL) */,
906  char *modelName     /* IN: Model name (or NULL) */,
907  FILE *fp            /* IN: Pointer to the dump file */
908  )
909{
910  DdNode *support = NULL;
911  DdNode *scan;
912  int *sorted = NULL;
913  int nVars = ddMgr->size;
914  int retValue;
915  int i;
916
917  /* Build a bit array with the support of f. */
918  sorted = ALLOC (int, nVars);
919  if (sorted == NULL) {
920    ddMgr->errorCode = CUDD_MEMORY_OUT;
921    Dddmp_CheckAndGotoLabel (1, "Allocation Error.", failure);
922  }
923  for (i = 0; i < nVars; i++) {
924    sorted[i] = 0;
925  }
926
927  /* Take the union of the supports of each output function. */
928  support = Cudd_VectorSupport(ddMgr,f,n);
929  Dddmp_CheckAndGotoLabel (support==NULL,
930    "Error in function Cudd_VectorSupport.", failure);
931  cuddRef(support);
932  scan = support;
933  while (!cuddIsConstant(scan)) {
934    sorted[scan->index] = 1;
935    scan = cuddT(scan);
936  }
937  Cudd_RecursiveDeref(ddMgr,support);
938  support = NULL;
939  /* so that we do not try to free it in case of failure */
940
941  /* Write the header (.model .inputs .outputs). */
942  if (modelName == NULL) {
943    retValue = fprintf(fp,".model DD\n.inputs");
944  } else {
945    retValue = fprintf(fp,".model %s\n.inputs", modelName);
946  }
947  if (retValue == EOF) {
948    return(0);
949  }
950
951  /* Write the input list by scanning the support array. */
952  for (i = 0; i < nVars; i++) {
953    if (sorted[i]) {
954      if (inputNames == NULL || (inputNames[i] == NULL)) {
955        retValue = fprintf(fp," inNode%d", i);
956      } else {
957        retValue = fprintf(fp," %s", inputNames[i]);
958      }
959      Dddmp_CheckAndGotoLabel (retValue==EOF,
960        "Error during file store.", failure);
961    }
962  }
963  FREE(sorted);
964  sorted = NULL;
965
966  /* Write the .output line. */
967  retValue = fprintf(fp,"\n.outputs");
968  Dddmp_CheckAndGotoLabel (retValue==EOF,
969    "Error during file store.", failure);
970  for (i = 0; i < n; i++) {
971    if (outputNames == NULL || (outputNames[i] == NULL)) {
972      retValue = fprintf(fp," outNode%d", i);
973    } else {
974      retValue = fprintf(fp," %s", outputNames[i]);
975    }
976    Dddmp_CheckAndGotoLabel (retValue==EOF,
977      "Error during file store.", failure);
978  }
979  retValue = fprintf(fp,"\n");
980  Dddmp_CheckAndGotoLabel (retValue==EOF,
981    "Error during file store.", failure);
982
983  retValue = DddmpCuddDdArrayStoreBlifBody(ddMgr, n, f, inputNames,
984    outputNames, fp);
985  Dddmp_CheckAndGotoLabel (retValue==0,
986    "Error if function DddmpCuddDdArrayStoreBlifBody.", failure);
987
988  /* Write trailer and return. */
989  retValue = fprintf (fp, ".end\n");
990  Dddmp_CheckAndGotoLabel (retValue==EOF,
991    "Error during file store.", failure);
992
993  return(1);
994
995failure:
996  if (sorted != NULL) {
997    FREE(sorted);
998  }
999  if (support != NULL) {
1000    Cudd_RecursiveDeref(ddMgr,support);
1001  }
1002
1003  return(0);
1004}
1005
1006
1007/**Function********************************************************************
1008
1009  Synopsis    [Writes a blif body representing the argument BDDs.]
1010
1011  Description [Writes a blif body representing the argument BDDs as a
1012    network of multiplexers. One multiplexer is written for each BDD
1013    node. It returns 1 in case of success; 0 otherwise (e.g.,
1014    out-of-memory, file system full, or an ADD with constants different
1015    from 0 and 1).
1016    DddmpCuddDdArrayStoreBlif does not close the file: This is the
1017    caller responsibility.
1018    DddmpCuddDdArrayStoreBlif uses a minimal unique subset of
1019    the hexadecimal address of a node as name for it.  If the argument
1020    inputNames is non-null, it is assumed to hold the pointers to the names
1021    of the inputs. Similarly for outputNames. This function prints out only
1022    .names part.
1023  ]
1024
1025  SideEffects [None]
1026
1027  SeeAlso     []
1028
1029******************************************************************************/
1030
1031static int
1032DddmpCuddDdArrayStoreBlifBody (
1033  DdManager *ddMgr      /* IN: Manager */,
1034  int n                 /* IN: Number of output nodes to be dumped */,
1035  DdNode **f            /* IN: Array of output nodes to be dumped */,
1036  char **inputNames     /* IN: Array of input names (or NULL) */,
1037  char **outputNames    /* IN: Array of output names (or NULL) */,
1038  FILE *fp              /* IN: Pointer to the dump file */
1039  )
1040{
1041  st_table *visited = NULL;
1042  int retValue;
1043  int i;
1044
1045  /* Initialize symbol table for visited nodes. */
1046  visited = st_init_table(st_ptrcmp, st_ptrhash);
1047  Dddmp_CheckAndGotoLabel (visited==NULL,
1048    "Error if function st_init_table.", failure);
1049
1050  /* Call the function that really gets the job done. */
1051  for (i = 0; i < n; i++) {
1052    retValue = DddmpCuddDdArrayStoreBlifStep (ddMgr, Cudd_Regular(f[i]),
1053      fp, visited, inputNames);
1054    Dddmp_CheckAndGotoLabel (retValue==0,
1055      "Error if function DddmpCuddDdArrayStoreBlifStep.", failure);
1056  }
1057
1058  /*
1059   *  To account for the possible complement on the root,
1060   *  we put either a buffer or an inverter at the output of
1061   *  the multiplexer representing the top node.
1062   */
1063
1064  for (i = 0; i < n; i++) {
1065    if (outputNames == NULL) {
1066      retValue = fprintf(fp,
1067#if SIZEOF_VOID_P == 8
1068        ".names node%lx outNode%d\n",
1069        (unsigned long) f[i] / (unsigned long) sizeof(DdNode), i);
1070#else
1071        ".names node%x outNode%d\n",
1072        (unsigned) f[i] / (unsigned) sizeof(DdNode), i);
1073#endif
1074    } else {
1075      retValue = fprintf(fp,
1076#if SIZEOF_VOID_P == 8
1077        ".names node%lx %s\n",
1078        (unsigned long) f[i] / (unsigned long) sizeof(DdNode), outputNames[i]);
1079#else
1080        ".names node%x %s\n",
1081        (unsigned) f[i] / (unsigned) sizeof(DdNode), outputNames[i]);
1082#endif
1083    }
1084    Dddmp_CheckAndGotoLabel (retValue==EOF,
1085      "Error during file store.", failure);
1086    if (Cudd_IsComplement(f[i])) {
1087      retValue = fprintf(fp,"0 1\n");
1088    } else {
1089      retValue = fprintf(fp,"1 1\n");
1090    }
1091    Dddmp_CheckAndGotoLabel (retValue==EOF,
1092      "Error during file store.", failure);
1093  }
1094
1095  st_free_table(visited);
1096  return(1);
1097
1098failure:
1099  if (visited != NULL) {
1100    st_free_table(visited);
1101  }
1102  return(0);
1103}
1104
1105/**Function********************************************************************
1106
1107  Synopsis    [Performs the recursive step of DddmpCuddDdArrayStoreBlif.]
1108
1109  Description [Performs the recursive step of DddmpCuddDdArrayStoreBlif.
1110    Traverses the BDD f and writes a multiplexer-network description to
1111    the file pointed by fp in blif format.
1112    f is assumed to be a regular pointer and DddmpCuddDdArrayStoreBlifStep
1113    guarantees this assumption in the recursive calls.
1114    ]
1115
1116  SideEffects [None]
1117
1118  SeeAlso     []
1119
1120******************************************************************************/
1121
1122static int
1123DddmpCuddDdArrayStoreBlifStep (
1124  DdManager *ddMgr,
1125  DdNode *f,
1126  FILE *fp,
1127  st_table *visited,
1128  char **names
1129  )
1130{
1131  DdNode *T, *E;
1132  int retValue;
1133
1134#ifdef DDDMP_DEBUG
1135  assert(!Cudd_IsComplement(f));
1136#endif
1137
1138  /* If already visited, nothing to do. */
1139  if (st_is_member(visited, (char *) f) == 1) {
1140    return(1);
1141  }
1142
1143  /* Check for abnormal condition that should never happen. */
1144  if (f == NULL) {
1145    return(0);
1146  }
1147
1148  /* Mark node as visited. */
1149  if (st_insert(visited, (char *) f, NULL) == ST_OUT_OF_MEM) {
1150    return(0);
1151  }
1152
1153  /* Check for special case: If constant node, generate constant 1. */
1154  if (f == DD_ONE(ddMgr)) {
1155#if SIZEOF_VOID_P == 8
1156    retValue = fprintf(fp, ".names node%lx\n1\n",
1157      (unsigned long) f / (unsigned long) sizeof(DdNode));
1158#else
1159    retValue = fprintf(fp, ".names node%x\n1\n",
1160      (unsigned) f / (unsigned) sizeof(DdNode));
1161#endif
1162     if (retValue == EOF) {
1163       return(0);
1164     } else {
1165       return(1);
1166    }
1167  }
1168
1169  /* Check whether this is an ADD. We deal with 0-1 ADDs, but not
1170  ** with the general case.
1171  */
1172  if (f == DD_ZERO(ddMgr)) {
1173#if SIZEOF_VOID_P == 8
1174    retValue = fprintf(fp, ".names node%lx\n",
1175      (unsigned long) f / (unsigned long) sizeof(DdNode));
1176#else
1177    retValue = fprintf(fp, ".names node%x\n",
1178      (unsigned) f / (unsigned) sizeof(DdNode));
1179#endif
1180    if (retValue == EOF) {
1181      return(0);
1182    } else {
1183      return(1);
1184    }
1185  }
1186  if (cuddIsConstant(f)) {
1187    return(0);
1188  }
1189
1190  /* Recursive calls. */
1191  T = cuddT(f);
1192  retValue = DddmpCuddDdArrayStoreBlifStep(ddMgr,T,fp,visited,names);
1193  if (retValue != 1) return(retValue);
1194  E = Cudd_Regular(cuddE(f));
1195  retValue = DddmpCuddDdArrayStoreBlifStep(ddMgr,E,fp,visited,names);
1196  if (retValue != 1) return(retValue);
1197
1198  /* Write multiplexer taking complement arc into account. */
1199  if (names != NULL) {
1200    retValue = fprintf(fp,".names %s", names[f->index]);
1201  } else {
1202    retValue = fprintf(fp,".names inNode%d", f->index);
1203  }
1204  if (retValue == EOF) {
1205    return(0);
1206  }
1207
1208#if SIZEOF_VOID_P == 8
1209  if (Cudd_IsComplement(cuddE(f))) {
1210    retValue = fprintf(fp," node%lx node%lx node%lx\n11- 1\n0-0 1\n",
1211      (unsigned long) T / (unsigned long) sizeof(DdNode),
1212      (unsigned long) E / (unsigned long) sizeof(DdNode),
1213      (unsigned long) f / (unsigned long) sizeof(DdNode));
1214  } else {
1215    retValue = fprintf(fp," node%lx node%lx node%lx\n11- 1\n0-1 1\n",
1216      (unsigned long) T / (unsigned long) sizeof(DdNode),
1217      (unsigned long) E / (unsigned long) sizeof(DdNode),
1218      (unsigned long) f / (unsigned long) sizeof(DdNode));
1219  }
1220#else
1221  if (Cudd_IsComplement(cuddE(f))) {
1222    retValue = fprintf(fp," node%x node%x node%x\n11- 1\n0-0 1\n",
1223      (unsigned) T / (unsigned) sizeof(DdNode),
1224      (unsigned) E / (unsigned) sizeof(DdNode),
1225      (unsigned) f / (unsigned) sizeof(DdNode));
1226  } else {
1227    retValue = fprintf(fp," node%x node%x node%x\n11- 1\n0-1 1\n",
1228      (unsigned) T / (unsigned) sizeof(DdNode),
1229      (unsigned) E / (unsigned) sizeof(DdNode),
1230      (unsigned) f / (unsigned) sizeof(DdNode));
1231  }
1232#endif
1233  if (retValue == EOF) {
1234    return(0);
1235  } else {
1236    return(1);
1237  }
1238}
1239
1240/**Function********************************************************************
1241
1242  Synopsis     [Internal function to writes a dump file representing the
1243    argument BDD in a SMV notation.]
1244
1245  Description  [One multiplexer is written for each BDD node.
1246    It returns 1 in case of success; 0 otherwise (e.g., out-of-memory, file
1247    system full, or an ADD with constants different from 0 and 1).
1248    It does not close the file: This is the caller responsibility.
1249    It uses a minimal unique subset of the hexadecimal address of a node as
1250    name for it.
1251    If the argument inputNames is non-null, it is assumed to hold the
1252    pointers to the names of the inputs. Similarly for outputNames.
1253    For each BDD node of function f, variable v, then child T, and else
1254    child E it stores:
1255    f = v * T + v' * E
1256    that is
1257    (OR f (AND v T) (AND (NOT v) E))
1258    If E is a complemented child this results in the following
1259    (OR f (AND v T) (AND (NOT v) (NOT E)))
1260    Comments (COMMENT) are added at the beginning of the description to
1261    describe inputs and outputs of the design.
1262    A buffer (BUF) is add on the output to cope with complemented functions.
1263    ]
1264
1265  SideEffects [None]
1266
1267  SeeAlso     [DddmpCuddDdArrayStoreBlif]
1268
1269******************************************************************************/
1270
1271static int
1272DddmpCuddDdArrayStoreSmv (
1273  DdManager *ddMgr    /* IN: Manager */,
1274  int n               /* IN: Number of output nodes to be dumped */,
1275  DdNode **f          /* IN: Array of output nodes to be dumped */,
1276  char **inputNames   /* IN: Array of input names (or NULL) */,
1277  char **outputNames  /* IN: Array of output names (or NULL) */,
1278  char *modelName     /* IN: Model name (or NULL) */,
1279  FILE *fp            /* IN: Pointer to the dump file */
1280  )
1281{
1282  DdNode *support = NULL;
1283  DdNode *scan;
1284  int *sorted = NULL;
1285  int nVars = ddMgr->size;
1286  int retValue;
1287  int i;
1288
1289  /* Build a bit array with the support of f. */
1290  sorted = ALLOC(int, nVars);
1291  if (sorted == NULL) {
1292    ddMgr->errorCode = CUDD_MEMORY_OUT;
1293    Dddmp_CheckAndGotoLabel (1, "Allocation Error.", failure);
1294  }
1295  for (i = 0; i < nVars; i++) {
1296    sorted[i] = 0;
1297  }
1298
1299  /* Take the union of the supports of each output function. */
1300  support = Cudd_VectorSupport(ddMgr,f,n);
1301  Dddmp_CheckAndGotoLabel (support==NULL,
1302    "Error in function Cudd_VectorSupport.", failure);
1303  cuddRef(support);
1304  scan = support;
1305  while (!cuddIsConstant(scan)) {
1306    sorted[scan->index] = 1;
1307    scan = cuddT(scan);
1308  }
1309  Cudd_RecursiveDeref(ddMgr,support);
1310  /* so that we do not try to free it in case of failure */
1311  support = NULL;
1312
1313  /* Write the header */
1314  if (modelName == NULL) {
1315    retValue = fprintf (fp, "MODULE main -- Unknown\n");
1316  } else {
1317    retValue = fprintf (fp, "MODULE main -- %s\n", modelName);
1318  }
1319  if (retValue == EOF) {
1320    return(0);
1321  }
1322
1323  retValue = fprintf(fp, "IVAR\n");
1324  if (retValue == EOF) {
1325    return(0);
1326  }
1327
1328  /* Write the input list by scanning the support array. */
1329  for (i=0; i<nVars; i++) {
1330    if (sorted[i]) {
1331      if (inputNames == NULL) {
1332        retValue = fprintf (fp, " inNode%d : boolean;\n", i);
1333      } else {
1334        retValue = fprintf (fp, " %s : boolean;\n", inputNames[i]);
1335      }
1336      Dddmp_CheckAndGotoLabel (retValue==EOF,
1337        "Error during file store.", failure);
1338    }
1339  }
1340  FREE(sorted);
1341  sorted = NULL;
1342
1343  retValue = fprintf (fp, "\nDEFINE\n");
1344
1345  retValue = DddmpCuddDdArrayStoreSmvBody (ddMgr, n, f, inputNames,
1346    outputNames, fp);
1347  Dddmp_CheckAndGotoLabel (retValue==0,
1348    "Error in function DddmpCuddDdArrayStoreSmvBody.", failure);
1349
1350  return(1);
1351
1352failure:
1353    if (sorted != NULL) {
1354      FREE(sorted);
1355    }
1356    if (support != NULL) {
1357      Cudd_RecursiveDeref(ddMgr,support);
1358    }
1359    return(0);
1360}
1361
1362/**Function********************************************************************
1363
1364  Synopsis     [Internal function to writes a dump file representing the
1365    argument BDD in a SMV notation. Writes the body of the file.]
1366
1367  Description  [One multiplexer is written for each BDD node.
1368    It returns 1 in case of success; 0 otherwise (e.g., out-of-memory, file
1369    system full, or an ADD with constants different from 0 and 1).
1370    It does not close the file: This is the caller responsibility.
1371    It uses a minimal unique subset of the hexadecimal address of a node as
1372    name for it.
1373    If the argument inputNames is non-null, it is assumed to hold the
1374    pointers to the names of the inputs. Similarly for outputNames.
1375    For each BDD node of function f, variable v, then child T, and else
1376    child E it stores:
1377    f = v * T + v' * E
1378    that is
1379    (OR f (AND v T) (AND (NOT v) E))
1380    If E is a complemented child this results in the following
1381    (OR f (AND v T) (AND (NOT v) (NOT E)))
1382    ]
1383
1384  SideEffects [None]
1385
1386  SeeAlso     [DddmpCuddDdArrayStoreBlif]
1387
1388******************************************************************************/
1389
1390static int
1391DddmpCuddDdArrayStoreSmvBody (
1392  DdManager *ddMgr      /* IN: Manager */,
1393  int n                 /* IN: Number of output nodes to be dumped */,
1394  DdNode **f            /* IN: Array of output nodes to be dumped */,
1395  char **inputNames     /* IN: Array of input names (or NULL) */,
1396  char **outputNames    /* IN: Array of output names (or NULL) */,
1397  FILE *fp              /* IN: Pointer to the dump file */
1398  )
1399{
1400  st_table *visited = NULL;
1401  int retValue;
1402  int i;
1403
1404  /* Initialize symbol table for visited nodes. */
1405  visited = st_init_table(st_ptrcmp, st_ptrhash);
1406  Dddmp_CheckAndGotoLabel (visited==NULL,
1407    "Error if function st_init_table.", failure);
1408
1409  /* Call the function that really gets the job done. */
1410  for (i = 0; i < n; i++) {
1411    retValue = DddmpCuddDdArrayStoreSmvStep (ddMgr, Cudd_Regular(f[i]),
1412      fp, visited, inputNames);
1413    Dddmp_CheckAndGotoLabel (retValue==0,
1414      "Error if function DddmpCuddDdArrayStoreSmvStep.", failure);
1415  }
1416
1417  /*
1418   *  To account for the possible complement on the root,
1419   *  we put either a buffer or an inverter at the output of
1420   *  the multiplexer representing the top node.
1421   */
1422
1423  for (i=0; i<n; i++) {
1424    if (outputNames == NULL) {
1425      retValue = fprintf (fp,  "outNode%d := ", i);
1426    } else {
1427      retValue = fprintf (fp,  "%s := ", outputNames[i]);
1428    }
1429    Dddmp_CheckAndGotoLabel (retValue==EOF,
1430      "Error during file store.", failure);
1431
1432    if (Cudd_IsComplement(f[i])) {
1433#if SIZEOF_VOID_P == 8
1434      retValue = fprintf (fp, "!node%lx\n",
1435        (unsigned long) f[i] / (unsigned long) sizeof(DdNode));
1436#else
1437      retValue = fprintf (fp, "!node%x\n",
1438        (unsigned) f[i] / (unsigned) sizeof(DdNode));
1439#endif
1440    } else {
1441#if SIZEOF_VOID_P == 8
1442      retValue = fprintf (fp, "node%lx\n",
1443        (unsigned long) f[i] / (unsigned long) sizeof(DdNode));
1444#else
1445      retValue = fprintf (fp, "node%x\n",
1446        (unsigned) f[i] / (unsigned) sizeof(DdNode));
1447#endif
1448    }
1449    Dddmp_CheckAndGotoLabel (retValue==EOF,
1450      "Error during file store.", failure);
1451  }
1452
1453  st_free_table (visited);
1454
1455  return(1);
1456
1457failure:
1458    if (visited != NULL) st_free_table(visited);
1459    return(0);
1460
1461}
1462
1463/**Function********************************************************************
1464
1465  Synopsis    [Performs the recursive step of
1466    DddmpCuddDdArrayStoreSmvBody.]
1467
1468  Description [Performs the recursive step of
1469    DddmpCuddDdArrayStoreSmvBody.
1470    Traverses the BDD f and writes a multiplexer-network description to the
1471    file pointed by fp.
1472    For each BDD node of function f, variable v, then child T, and else
1473    child E it stores:
1474    f = v * T + v' * E
1475    that is
1476    (OR f (AND v T) (AND (NOT v) E))
1477    If E is a complemented child this results in the following
1478    (OR f (AND v T) (AND (NOT v) (NOT E)))
1479    f is assumed to be a regular pointer and the function guarantees this
1480    assumption in the recursive calls.
1481    ]
1482
1483  SideEffects [None]
1484
1485  SeeAlso     []
1486
1487******************************************************************************/
1488
1489static int
1490DddmpCuddDdArrayStoreSmvStep (
1491  DdManager * ddMgr,
1492  DdNode * f,
1493  FILE * fp,
1494  st_table * visited,
1495  char ** names
1496  )
1497{
1498  DdNode *T, *E;
1499  int retValue;
1500
1501#ifdef DDDMP_DEBUG
1502  assert(!Cudd_IsComplement(f));
1503#endif
1504
1505  /* If already visited, nothing to do. */
1506  if (st_is_member(visited, (char *) f) == 1) {
1507    return(1);
1508  }
1509
1510  /* Check for abnormal condition that should never happen. */
1511  if (f == NULL) {
1512    return(0);
1513  }
1514
1515  /* Mark node as visited. */
1516  if (st_insert(visited, (char *) f, NULL) == ST_OUT_OF_MEM) {
1517    return(0);
1518  }
1519
1520  /* Check for special case: If constant node, generate constant 1. */
1521  if (f == DD_ONE (ddMgr)) {
1522#if SIZEOF_VOID_P == 8
1523    retValue = fprintf (fp,
1524      "node%lx := 1;\n",
1525      (unsigned long) f / (unsigned long) sizeof(DdNode));
1526#else
1527    retValue = fprintf (fp,
1528      "node%x := 1;\n",
1529      (unsigned) f / (unsigned) sizeof(DdNode));
1530#endif
1531    if (retValue == EOF) {
1532       return(0);
1533    } else {
1534       return(1);
1535    }
1536  }
1537
1538  /*
1539   *  Check whether this is an ADD. We deal with 0-1 ADDs, but not
1540   *  with the general case.
1541   */
1542
1543  if (f == DD_ZERO(ddMgr)) {
1544#if SIZEOF_VOID_P == 8
1545    retValue = fprintf (fp,
1546      "node%lx := 0;\n",
1547       (unsigned long) f / (unsigned long) sizeof(DdNode));
1548#else
1549    retValue = fprintf (fp,
1550      "node%x := 0;\n",
1551      (unsigned) f / (unsigned) sizeof(DdNode));
1552#endif
1553   if (retValue == EOF) {
1554     return(0);
1555   } else {
1556     return(1);
1557   }
1558  }
1559
1560  if (cuddIsConstant(f)) {
1561    return(0);
1562  }
1563
1564  /* Recursive calls. */
1565  T = cuddT(f);
1566  retValue = DddmpCuddDdArrayStoreSmvStep (ddMgr,T,fp,visited,names);
1567  if (retValue != 1) {
1568    return(retValue);
1569  }
1570  E = Cudd_Regular(cuddE(f));
1571  retValue = DddmpCuddDdArrayStoreSmvStep (ddMgr,E,fp,visited,names);
1572  if (retValue != 1) {
1573    return(retValue);
1574  }
1575
1576  /* Write multiplexer taking complement arc into account. */
1577#if SIZEOF_VOID_P == 8
1578  retValue = fprintf (fp, "node%lx := ",
1579    (unsigned long) f / (unsigned long) sizeof(DdNode));
1580#else
1581  retValue = fprintf (fp, "node%x := ",
1582    (unsigned) f / (unsigned) sizeof(DdNode));
1583#endif
1584  if (retValue == EOF) {
1585    return(0);
1586  }
1587
1588  if (names != NULL) {
1589    retValue = fprintf(fp, "%s ", names[f->index]);
1590  } else {
1591    retValue = fprintf(fp, "inNode%d ", f->index);
1592  }
1593  if (retValue == EOF) {
1594    return(0);
1595  }
1596
1597#if SIZEOF_VOID_P == 8
1598  retValue = fprintf (fp, "& node%lx | ",
1599    (unsigned long) T / (unsigned long) sizeof(DdNode));
1600#else
1601  retValue = fprintf (fp, "& node%x | ",
1602    (unsigned) T / (unsigned) sizeof(DdNode));
1603#endif
1604  if (retValue == EOF) {
1605    return(0);
1606  }
1607
1608  if (names != NULL) {
1609    retValue = fprintf (fp, "!%s ", names[f->index]);
1610  } else {
1611    retValue = fprintf (fp, "!inNode%d ", f->index);
1612  }
1613  if (retValue == EOF) {
1614    return(0);
1615  }
1616
1617#if SIZEOF_VOID_P == 8
1618  if (Cudd_IsComplement(cuddE(f))) {
1619    retValue = fprintf (fp, "& !node%lx\n",
1620      (unsigned long) E / (unsigned long) sizeof(DdNode));
1621  } else {
1622    retValue = fprintf (fp, "& node%lx\n",
1623      (unsigned long) E / (unsigned long) sizeof(DdNode));
1624  }
1625#else
1626  if (Cudd_IsComplement(cuddE(f))) {
1627    retValue = fprintf (fp, "& !node%x\n",
1628      (unsigned) E / (unsigned) sizeof(DdNode));
1629  } else {
1630    retValue = fprintf (fp, "& node%x\n",
1631      (unsigned) E / (unsigned) sizeof(DdNode));
1632  }
1633#endif
1634
1635  if (retValue == EOF) {
1636    return(0);
1637  } else {
1638    return(1);
1639  }
1640}
1641
Note: See TracBrowser for help on using the repository browser.