source: vis_dev/glu-2.1/src/cuBdd/cuddExport.c @ 8

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

src glu
File size: 41.8 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [cuddExport.c]
4
5  PackageName [cudd]
6
7  Synopsis    [Export functions.]
8
9  Description [External procedures included in this module:
10                <ul>
11                <li> Cudd_DumpBlif()
12                <li> Cudd_DumpBlifBody()
13                <li> Cudd_DumpDot()
14                <li> Cudd_DumpDaVinci()
15                <li> Cudd_DumpDDcal()
16                <li> Cudd_DumpFactoredForm()
17                </ul>
18        Internal procedures included in this module:
19                <ul>
20                </ul>
21        Static procedures included in this module:
22                <ul>
23                <li> ddDoDumpBlif()
24                <li> ddDoDumpDaVinci()
25                <li> ddDoDumpDDcal()
26                <li> ddDoDumpFactoredForm()
27                </ul>]
28
29  Author      [Fabio Somenzi]
30
31  Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
32
33  All rights reserved.
34
35  Redistribution and use in source and binary forms, with or without
36  modification, are permitted provided that the following conditions
37  are met:
38
39  Redistributions of source code must retain the above copyright
40  notice, this list of conditions and the following disclaimer.
41
42  Redistributions in binary form must reproduce the above copyright
43  notice, this list of conditions and the following disclaimer in the
44  documentation and/or other materials provided with the distribution.
45
46  Neither the name of the University of Colorado nor the names of its
47  contributors may be used to endorse or promote products derived from
48  this software without specific prior written permission.
49
50  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
51  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
52  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
53  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
54  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
55  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
56  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
57  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
58  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
59  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
60  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
61  POSSIBILITY OF SUCH DAMAGE.]
62
63******************************************************************************/
64
65#include "util.h"
66#include "cuddInt.h"
67
68/*---------------------------------------------------------------------------*/
69/* Constant declarations                                                     */
70/*---------------------------------------------------------------------------*/
71
72/*---------------------------------------------------------------------------*/
73/* Stucture declarations                                                     */
74/*---------------------------------------------------------------------------*/
75
76/*---------------------------------------------------------------------------*/
77/* Type declarations                                                         */
78/*---------------------------------------------------------------------------*/
79
80/*---------------------------------------------------------------------------*/
81/* Variable declarations                                                     */
82/*---------------------------------------------------------------------------*/
83
84#ifndef lint
85static char rcsid[] DD_UNUSED = "$Id: cuddExport.c,v 1.18 2004/08/13 18:04:48 fabio Exp $";
86#endif
87
88/*---------------------------------------------------------------------------*/
89/* Macro declarations                                                        */
90/*---------------------------------------------------------------------------*/
91
92/**AutomaticStart*************************************************************/
93
94/*---------------------------------------------------------------------------*/
95/* Static function prototypes                                                */
96/*---------------------------------------------------------------------------*/
97
98static int ddDoDumpBlif (DdManager *dd, DdNode *f, FILE *fp, st_table *visited, char **names);
99static int ddDoDumpDaVinci (DdManager *dd, DdNode *f, FILE *fp, st_table *visited, char **names, unsigned long mask);
100static int ddDoDumpDDcal (DdManager *dd, DdNode *f, FILE *fp, st_table *visited, char **names, unsigned long mask);
101static int ddDoDumpFactoredForm (DdManager *dd, DdNode *f, FILE *fp, char **names);
102
103/**AutomaticEnd***************************************************************/
104
105
106/*---------------------------------------------------------------------------*/
107/* Definition of exported functions                                          */
108/*---------------------------------------------------------------------------*/
109
110
111/**Function********************************************************************
112
113  Synopsis    [Writes a blif file representing the argument BDDs.]
114
115  Description [Writes a blif file representing the argument BDDs as a
116  network of multiplexers. One multiplexer is written for each BDD
117  node. It returns 1 in case of success; 0 otherwise (e.g.,
118  out-of-memory, file system full, or an ADD with constants different
119  from 0 and 1).  Cudd_DumpBlif does not close the file: This is the
120  caller responsibility. Cudd_DumpBlif uses a minimal unique subset of
121  the hexadecimal address of a node as name for it.  If the argument
122  inames is non-null, it is assumed to hold the pointers to the names
123  of the inputs. Similarly for onames.]
124
125  SideEffects [None]
126
127  SeeAlso     [Cudd_DumpBlifBody Cudd_DumpDot Cudd_PrintDebug Cudd_DumpDDcal
128  Cudd_DumpDaVinci Cudd_DumpFactoredForm]
129
130******************************************************************************/
131int
132Cudd_DumpBlif(
133  DdManager * dd /* manager */,
134  int  n /* number of output nodes to be dumped */,
135  DdNode ** f /* array of output nodes to be dumped */,
136  char ** inames /* array of input names (or NULL) */,
137  char ** onames /* array of output names (or NULL) */,
138  char * mname /* model name (or NULL) */,
139  FILE * fp /* pointer to the dump file */)
140{
141    DdNode      *support = NULL;
142    DdNode      *scan;
143    int         *sorted = NULL;
144    int         nvars = dd->size;
145    int         retval;
146    int         i;
147
148    /* Build a bit array with the support of f. */
149    sorted = ALLOC(int,nvars);
150    if (sorted == NULL) {
151        dd->errorCode = CUDD_MEMORY_OUT;
152        goto failure;
153    }
154    for (i = 0; i < nvars; i++) sorted[i] = 0;
155
156    /* Take the union of the supports of each output function. */
157    support = Cudd_VectorSupport(dd,f,n);
158    if (support == NULL) goto failure;
159    cuddRef(support);
160    scan = support;
161    while (!cuddIsConstant(scan)) {
162        sorted[scan->index] = 1;
163        scan = cuddT(scan);
164    }
165    Cudd_RecursiveDeref(dd,support);
166    support = NULL; /* so that we do not try to free it in case of failure */
167
168    /* Write the header (.model .inputs .outputs). */
169    if (mname == NULL) {
170        retval = fprintf(fp,".model DD\n.inputs");
171    } else {
172        retval = fprintf(fp,".model %s\n.inputs",mname);
173    }
174    if (retval == EOF) return(0);
175
176    /* Write the input list by scanning the support array. */
177    for (i = 0; i < nvars; i++) {
178        if (sorted[i]) {
179            if (inames == NULL) {
180                retval = fprintf(fp," %d", i);
181            } else {
182                retval = fprintf(fp," %s", inames[i]);
183            }
184            if (retval == EOF) goto failure;
185        }
186    }
187    FREE(sorted);
188    sorted = NULL;
189
190    /* Write the .output line. */
191    retval = fprintf(fp,"\n.outputs");
192    if (retval == EOF) goto failure;
193    for (i = 0; i < n; i++) {
194        if (onames == NULL) {
195            retval = fprintf(fp," f%d", i);
196        } else {
197            retval = fprintf(fp," %s", onames[i]);
198        }
199        if (retval == EOF) goto failure;
200    }
201    retval = fprintf(fp,"\n");
202    if (retval == EOF) goto failure;
203
204    retval = Cudd_DumpBlifBody(dd, n, f, inames, onames, fp);
205    if (retval == 0) goto failure;
206
207    /* Write trailer and return. */
208    retval = fprintf(fp,".end\n");
209    if (retval == EOF) goto failure;
210
211    return(1);
212
213failure:
214    if (sorted != NULL) FREE(sorted);
215    if (support != NULL) Cudd_RecursiveDeref(dd,support);
216    return(0);
217
218} /* end of Cudd_DumpBlif */
219
220
221/**Function********************************************************************
222
223  Synopsis    [Writes a blif body representing the argument BDDs.]
224
225  Description [Writes a blif body representing the argument BDDs as a
226  network of multiplexers.  No header (.model, .inputs, and .outputs) and
227  footer (.end) are produced by this function.  One multiplexer is written
228  for each BDD node. It returns 1 in case of success; 0 otherwise (e.g.,
229  out-of-memory, file system full, or an ADD with constants different
230  from 0 and 1).  Cudd_DumpBlifBody does not close the file: This is the
231  caller responsibility. Cudd_DumpBlifBody uses a minimal unique subset of
232  the hexadecimal address of a node as name for it.  If the argument
233  inames is non-null, it is assumed to hold the pointers to the names
234  of the inputs. Similarly for onames. This function prints out only
235  .names part.]
236
237  SideEffects [None]
238
239  SeeAlso     [Cudd_DumpBlif Cudd_DumpDot Cudd_PrintDebug Cudd_DumpDDcal
240  Cudd_DumpDaVinci Cudd_DumpFactoredForm]
241
242******************************************************************************/
243int
244Cudd_DumpBlifBody(
245  DdManager * dd /* manager */,
246  int  n /* number of output nodes to be dumped */,
247  DdNode ** f /* array of output nodes to be dumped */,
248  char ** inames /* array of input names (or NULL) */,
249  char ** onames /* array of output names (or NULL) */,
250  FILE * fp /* pointer to the dump file */)
251{
252    st_table    *visited = NULL;
253    int         retval;
254    int         i;
255
256    /* Initialize symbol table for visited nodes. */
257    visited = st_init_table(st_ptrcmp, st_ptrhash);
258    if (visited == NULL) goto failure;
259
260    /* Call the function that really gets the job done. */
261    for (i = 0; i < n; i++) {
262        retval = ddDoDumpBlif(dd,Cudd_Regular(f[i]),fp,visited,inames);
263        if (retval == 0) goto failure;
264    }
265
266    /* To account for the possible complement on the root,
267    ** we put either a buffer or an inverter at the output of
268    ** the multiplexer representing the top node.
269    */
270    for (i = 0; i < n; i++) {
271        if (onames == NULL) {
272            retval = fprintf(fp,
273#if SIZEOF_VOID_P == 8
274                ".names %lx f%d\n", (unsigned long) f[i] / (unsigned long) sizeof(DdNode), i);
275#else
276                ".names %x f%d\n", (unsigned) f[i] / (unsigned) sizeof(DdNode), i);
277#endif
278        } else {
279            retval = fprintf(fp,
280#if SIZEOF_VOID_P == 8
281                ".names %lx %s\n", (unsigned long) f[i] / (unsigned long) sizeof(DdNode), onames[i]);
282#else
283                ".names %x %s\n", (unsigned) f[i] / (unsigned) sizeof(DdNode), onames[i]);
284#endif
285        }
286        if (retval == EOF) goto failure;
287        if (Cudd_IsComplement(f[i])) {
288            retval = fprintf(fp,"0 1\n");
289        } else {
290            retval = fprintf(fp,"1 1\n");
291        }
292        if (retval == EOF) goto failure;
293    }
294
295    st_free_table(visited);
296    return(1);
297
298failure:
299    if (visited != NULL) st_free_table(visited);
300    return(0);
301
302} /* end of Cudd_DumpBlifBody */
303
304
305/**Function********************************************************************
306
307  Synopsis    [Writes a dot file representing the argument DDs.]
308
309  Description [Writes a file representing the argument DDs in a format
310  suitable for the graph drawing program dot.
311  It returns 1 in case of success; 0 otherwise (e.g., out-of-memory,
312  file system full).
313  Cudd_DumpDot does not close the file: This is the caller
314  responsibility. Cudd_DumpDot uses a minimal unique subset of the
315  hexadecimal address of a node as name for it.
316  If the argument inames is non-null, it is assumed to hold the pointers
317  to the names of the inputs. Similarly for onames.
318  Cudd_DumpDot uses the following convention to draw arcs:
319    <ul>
320    <li> solid line: THEN arcs;
321    <li> dotted line: complement arcs;
322    <li> dashed line: regular ELSE arcs.
323    </ul>
324  The dot options are chosen so that the drawing fits on a letter-size
325  sheet.
326  ]
327
328  SideEffects [None]
329
330  SeeAlso     [Cudd_DumpBlif Cudd_PrintDebug Cudd_DumpDDcal
331  Cudd_DumpDaVinci Cudd_DumpFactoredForm]
332
333******************************************************************************/
334int
335Cudd_DumpDot(
336  DdManager * dd /* manager */,
337  int  n /* number of output nodes to be dumped */,
338  DdNode ** f /* array of output nodes to be dumped */,
339  char ** inames /* array of input names (or NULL) */,
340  char ** onames /* array of output names (or NULL) */,
341  FILE * fp /* pointer to the dump file */)
342{
343    DdNode      *support = NULL;
344    DdNode      *scan;
345    int         *sorted = NULL;
346    int         nvars = dd->size;
347    st_table    *visited = NULL;
348    st_generator *gen = NULL;
349    int         retval;
350    int         i, j;
351    int         slots;
352    DdNodePtr   *nodelist;
353    long        refAddr, diff, mask;
354
355    /* Build a bit array with the support of f. */
356    sorted = ALLOC(int,nvars);
357    if (sorted == NULL) {
358        dd->errorCode = CUDD_MEMORY_OUT;
359        goto failure;
360    }
361    for (i = 0; i < nvars; i++) sorted[i] = 0;
362
363    /* Take the union of the supports of each output function. */
364    support = Cudd_VectorSupport(dd,f,n);
365    if (support == NULL) goto failure;
366    cuddRef(support);
367    scan = support;
368    while (!cuddIsConstant(scan)) {
369        sorted[scan->index] = 1;
370        scan = cuddT(scan);
371    }
372    Cudd_RecursiveDeref(dd,support);
373    support = NULL; /* so that we do not try to free it in case of failure */
374
375    /* Initialize symbol table for visited nodes. */
376    visited = st_init_table(st_ptrcmp, st_ptrhash);
377    if (visited == NULL) goto failure;
378
379    /* Collect all the nodes of this DD in the symbol table. */
380    for (i = 0; i < n; i++) {
381        retval = cuddCollectNodes(Cudd_Regular(f[i]),visited);
382        if (retval == 0) goto failure;
383    }
384
385    /* Find how many most significant hex digits are identical
386    ** in the addresses of all the nodes. Build a mask based
387    ** on this knowledge, so that digits that carry no information
388    ** will not be printed. This is done in two steps.
389    **  1. We scan the symbol table to find the bits that differ
390    **     in at least 2 addresses.
391    **  2. We choose one of the possible masks. There are 8 possible
392    **     masks for 32-bit integer, and 16 possible masks for 64-bit
393    **     integers.
394    */
395
396    /* Find the bits that are different. */
397    refAddr = (long) Cudd_Regular(f[0]);
398    diff = 0;
399    gen = st_init_gen(visited);
400    if (gen == NULL) goto failure;
401    while (st_gen(gen, &scan, NULL)) {
402        diff |= refAddr ^ (long) scan;
403    }
404    st_free_gen(gen); gen = NULL;
405
406    /* Choose the mask. */
407    for (i = 0; (unsigned) i < 8 * sizeof(long); i += 4) {
408        mask = (1 << i) - 1;
409        if (diff <= mask) break;
410    }
411
412    /* Write the header and the global attributes. */
413    retval = fprintf(fp,"digraph \"DD\" {\n");
414    if (retval == EOF) return(0);
415    retval = fprintf(fp,
416        "size = \"7.5,10\"\ncenter = true;\nedge [dir = none];\n");
417    if (retval == EOF) return(0);
418
419    /* Write the input name subgraph by scanning the support array. */
420    retval = fprintf(fp,"{ node [shape = plaintext];\n");
421    if (retval == EOF) goto failure;
422    retval = fprintf(fp,"  edge [style = invis];\n");
423    if (retval == EOF) goto failure;
424    /* We use a name ("CONST NODES") with an embedded blank, because
425    ** it is unlikely to appear as an input name.
426    */
427    retval = fprintf(fp,"  \"CONST NODES\" [style = invis];\n");
428    if (retval == EOF) goto failure;
429    for (i = 0; i < nvars; i++) {
430        if (sorted[dd->invperm[i]]) {
431            if (inames == NULL || inames[dd->invperm[i]] == NULL) {
432                retval = fprintf(fp,"\" %d \" -> ", dd->invperm[i]);
433            } else {
434                retval = fprintf(fp,"\" %s \" -> ", inames[dd->invperm[i]]);
435            }
436            if (retval == EOF) goto failure;
437        }
438    }
439    retval = fprintf(fp,"\"CONST NODES\"; \n}\n");
440    if (retval == EOF) goto failure;
441
442    /* Write the output node subgraph. */
443    retval = fprintf(fp,"{ rank = same; node [shape = box]; edge [style = invis];\n");
444    if (retval == EOF) goto failure;
445    for (i = 0; i < n; i++) {
446        if (onames == NULL) {
447            retval = fprintf(fp,"\"F%d\"", i);
448        } else {
449            retval = fprintf(fp,"\"  %s  \"", onames[i]);
450        }
451        if (retval == EOF) goto failure;
452        if (i == n - 1) {
453            retval = fprintf(fp,"; }\n");
454        } else {
455            retval = fprintf(fp," -> ");
456        }
457        if (retval == EOF) goto failure;
458    }
459
460    /* Write rank info: All nodes with the same index have the same rank. */
461    for (i = 0; i < nvars; i++) {
462        if (sorted[dd->invperm[i]]) {
463            retval = fprintf(fp,"{ rank = same; ");
464            if (retval == EOF) goto failure;
465            if (inames == NULL || inames[dd->invperm[i]] == NULL) {
466                retval = fprintf(fp,"\" %d \";\n", dd->invperm[i]);
467            } else {
468                retval = fprintf(fp,"\" %s \";\n", inames[dd->invperm[i]]);
469            }
470            if (retval == EOF) goto failure;
471            nodelist = dd->subtables[i].nodelist;
472            slots = dd->subtables[i].slots;
473            for (j = 0; j < slots; j++) {
474                scan = nodelist[j];
475                while (scan != NULL) {
476                    if (st_is_member(visited,(char *) scan)) {
477                        retval = fprintf(fp,"\"%lx\";\n",
478                            (unsigned long) ((mask & (long) scan) /
479                            sizeof(DdNode)));
480                        if (retval == EOF) goto failure;
481                    }
482                    scan = scan->next;
483                }
484            }
485            retval = fprintf(fp,"}\n");
486            if (retval == EOF) goto failure;
487        }
488    }
489
490    /* All constants have the same rank. */
491    retval = fprintf(fp,
492        "{ rank = same; \"CONST NODES\";\n{ node [shape = box]; ");
493    if (retval == EOF) goto failure;
494    nodelist = dd->constants.nodelist;
495    slots = dd->constants.slots;
496    for (j = 0; j < slots; j++) {
497        scan = nodelist[j];
498        while (scan != NULL) {
499            if (st_is_member(visited,(char *) scan)) {
500                retval = fprintf(fp,"\"%lx\";\n",
501                    (unsigned long) ((mask & (long) scan) / sizeof(DdNode)));
502                if (retval == EOF) goto failure;
503            }
504            scan = scan->next;
505        }
506    }
507    retval = fprintf(fp,"}\n}\n");
508    if (retval == EOF) goto failure;
509
510    /* Write edge info. */
511    /* Edges from the output nodes. */
512    for (i = 0; i < n; i++) {
513        if (onames == NULL) {
514            retval = fprintf(fp,"\"F%d\"", i);
515        } else {
516            retval = fprintf(fp,"\"  %s  \"", onames[i]);
517        }
518        if (retval == EOF) goto failure;
519        /* Account for the possible complement on the root. */
520        if (Cudd_IsComplement(f[i])) {
521            retval = fprintf(fp," -> \"%lx\" [style = dotted];\n",
522                (unsigned long) ((mask & (long) f[i]) / sizeof(DdNode)));
523        } else {
524            retval = fprintf(fp," -> \"%lx\" [style = solid];\n",
525                (unsigned long) ((mask & (long) f[i]) / sizeof(DdNode)));
526        }
527        if (retval == EOF) goto failure;
528    }
529
530    /* Edges from internal nodes. */
531    for (i = 0; i < nvars; i++) {
532        if (sorted[dd->invperm[i]]) {
533            nodelist = dd->subtables[i].nodelist;
534            slots = dd->subtables[i].slots;
535            for (j = 0; j < slots; j++) {
536                scan = nodelist[j];
537                while (scan != NULL) {
538                    if (st_is_member(visited,(char *) scan)) {
539                        retval = fprintf(fp,
540                            "\"%lx\" -> \"%lx\";\n",
541                            (unsigned long) ((mask & (long) scan) /
542                            sizeof(DdNode)),
543                            (unsigned long) ((mask & (long) cuddT(scan)) /
544                            sizeof(DdNode)));
545                        if (retval == EOF) goto failure;
546                        if (Cudd_IsComplement(cuddE(scan))) {
547                            retval = fprintf(fp,
548                                "\"%lx\" -> \"%lx\" [style = dotted];\n",
549                                (unsigned long) ((mask & (long) scan) /
550                                sizeof(DdNode)),
551                                (unsigned long) ((mask & (long) cuddE(scan)) /
552                                sizeof(DdNode)));
553                        } else {
554                            retval = fprintf(fp,
555                                "\"%lx\" -> \"%lx\" [style = dashed];\n",
556                                (unsigned long) ((mask & (long) scan) /
557                                sizeof(DdNode)),
558                                (unsigned long) ((mask & (long) cuddE(scan)) /
559                                sizeof(DdNode)));
560                        }
561                        if (retval == EOF) goto failure;
562                    }
563                    scan = scan->next;
564                }
565            }
566        }
567    }
568
569    /* Write constant labels. */
570    nodelist = dd->constants.nodelist;
571    slots = dd->constants.slots;
572    for (j = 0; j < slots; j++) {
573        scan = nodelist[j];
574        while (scan != NULL) {
575            if (st_is_member(visited,(char *) scan)) {
576                retval = fprintf(fp,"\"%lx\" [label = \"%g\"];\n",
577                    (unsigned long) ((mask & (long) scan) / sizeof(DdNode)),
578                    cuddV(scan));
579                if (retval == EOF) goto failure;
580            }
581            scan = scan->next;
582        }
583    }
584
585    /* Write trailer and return. */
586    retval = fprintf(fp,"}\n");
587    if (retval == EOF) goto failure;
588
589    st_free_table(visited);
590    FREE(sorted);
591    return(1);
592
593failure:
594    if (sorted != NULL) FREE(sorted);
595    if (support != NULL) Cudd_RecursiveDeref(dd,support);
596    if (visited != NULL) st_free_table(visited);
597    return(0);
598
599} /* end of Cudd_DumpDot */
600
601
602/**Function********************************************************************
603
604  Synopsis    [Writes a daVinci file representing the argument BDDs.]
605
606  Description [Writes a daVinci file representing the argument BDDs.
607  It returns 1 in case of success; 0 otherwise (e.g., out-of-memory or
608  file system full).  Cudd_DumpDaVinci does not close the file: This
609  is the caller responsibility. Cudd_DumpDaVinci uses a minimal unique
610  subset of the hexadecimal address of a node as name for it.  If the
611  argument inames is non-null, it is assumed to hold the pointers to
612  the names of the inputs. Similarly for onames.]
613
614  SideEffects [None]
615
616  SeeAlso     [Cudd_DumpDot Cudd_PrintDebug Cudd_DumpBlif Cudd_DumpDDcal
617  Cudd_DumpFactoredForm]
618
619******************************************************************************/
620int
621Cudd_DumpDaVinci(
622  DdManager * dd /* manager */,
623  int  n /* number of output nodes to be dumped */,
624  DdNode ** f /* array of output nodes to be dumped */,
625  char ** inames /* array of input names (or NULL) */,
626  char ** onames /* array of output names (or NULL) */,
627  FILE * fp /* pointer to the dump file */)
628{
629    DdNode        *support = NULL;
630    DdNode        *scan;
631    st_table      *visited = NULL;
632    int           retval;
633    int           i;
634    st_generator  *gen;
635    unsigned long refAddr, diff, mask;
636
637    /* Initialize symbol table for visited nodes. */
638    visited = st_init_table(st_ptrcmp, st_ptrhash);
639    if (visited == NULL) goto failure;
640
641    /* Collect all the nodes of this DD in the symbol table. */
642    for (i = 0; i < n; i++) {
643        retval = cuddCollectNodes(Cudd_Regular(f[i]),visited);
644        if (retval == 0) goto failure;
645    }
646
647    /* Find how many most significant hex digits are identical
648    ** in the addresses of all the nodes. Build a mask based
649    ** on this knowledge, so that digits that carry no information
650    ** will not be printed. This is done in two steps.
651    **  1. We scan the symbol table to find the bits that differ
652    **     in at least 2 addresses.
653    **  2. We choose one of the possible masks. There are 8 possible
654    **     masks for 32-bit integer, and 16 possible masks for 64-bit
655    **     integers.
656    */
657
658    /* Find the bits that are different. */
659    refAddr = (unsigned long) Cudd_Regular(f[0]);
660    diff = 0;
661    gen = st_init_gen(visited);
662    while (st_gen(gen, &scan, NULL)) {
663        diff |= refAddr ^ (unsigned long) scan;
664    }
665    st_free_gen(gen);
666
667    /* Choose the mask. */
668    for (i = 0; (unsigned) i < 8 * sizeof(long unsigned); i += 4) {
669        mask = (1 << i) - 1;
670        if (diff <= mask) break;
671    }
672    st_free_table(visited);
673
674    /* Initialize symbol table for visited nodes. */
675    visited = st_init_table(st_ptrcmp, st_ptrhash);
676    if (visited == NULL) goto failure;
677
678    retval = fprintf(fp, "[");
679    if (retval == EOF) goto failure;
680    /* Call the function that really gets the job done. */
681    for (i = 0; i < n; i++) {
682        if (onames == NULL) {
683            retval = fprintf(fp,
684                             "l(\"f%d\",n(\"root\",[a(\"OBJECT\",\"f%d\")],",
685                             i,i);
686        } else {
687            retval = fprintf(fp,
688                             "l(\"%s\",n(\"root\",[a(\"OBJECT\",\"%s\")],",
689                             onames[i], onames[i]);
690        }
691        if (retval == EOF) goto failure;
692        retval = fprintf(fp, "[e(\"edge\",[a(\"EDGECOLOR\",\"%s\"),a(\"_DIR\",\"none\")],",
693                         Cudd_IsComplement(f[i]) ? "red" : "blue");
694        if (retval == EOF) goto failure;
695        retval = ddDoDumpDaVinci(dd,Cudd_Regular(f[i]),fp,visited,inames,mask);
696        if (retval == 0) goto failure;
697        retval = fprintf(fp, ")]))%s", i == n-1 ? "" : ",");
698        if (retval == EOF) goto failure;
699    }
700
701    /* Write trailer and return. */
702    retval = fprintf(fp, "]\n");
703    if (retval == EOF) goto failure;
704
705    st_free_table(visited);
706    return(1);
707
708failure:
709    if (support != NULL) Cudd_RecursiveDeref(dd,support);
710    if (visited != NULL) st_free_table(visited);
711    return(0);
712
713} /* end of Cudd_DumpDaVinci */
714
715
716/**Function********************************************************************
717
718  Synopsis    [Writes a DDcal file representing the argument BDDs.]
719
720  Description [Writes a DDcal file representing the argument BDDs.
721  It returns 1 in case of success; 0 otherwise (e.g., out-of-memory or
722  file system full).  Cudd_DumpDDcal does not close the file: This
723  is the caller responsibility. Cudd_DumpDDcal uses a minimal unique
724  subset of the hexadecimal address of a node as name for it.  If the
725  argument inames is non-null, it is assumed to hold the pointers to
726  the names of the inputs. Similarly for onames.]
727
728  SideEffects [None]
729
730  SeeAlso     [Cudd_DumpDot Cudd_PrintDebug Cudd_DumpBlif Cudd_DumpDaVinci
731  Cudd_DumpFactoredForm]
732
733******************************************************************************/
734int
735Cudd_DumpDDcal(
736  DdManager * dd /* manager */,
737  int  n /* number of output nodes to be dumped */,
738  DdNode ** f /* array of output nodes to be dumped */,
739  char ** inames /* array of input names (or NULL) */,
740  char ** onames /* array of output names (or NULL) */,
741  FILE * fp /* pointer to the dump file */)
742{
743    DdNode        *support = NULL;
744    DdNode        *scan;
745    int           *sorted = NULL;
746    int           nvars = dd->size;
747    st_table      *visited = NULL;
748    int           retval;
749    int           i;
750    st_generator  *gen;
751    unsigned long refAddr, diff, mask;
752
753    /* Initialize symbol table for visited nodes. */
754    visited = st_init_table(st_ptrcmp, st_ptrhash);
755    if (visited == NULL) goto failure;
756
757    /* Collect all the nodes of this DD in the symbol table. */
758    for (i = 0; i < n; i++) {
759        retval = cuddCollectNodes(Cudd_Regular(f[i]),visited);
760        if (retval == 0) goto failure;
761    }
762
763    /* Find how many most significant hex digits are identical
764    ** in the addresses of all the nodes. Build a mask based
765    ** on this knowledge, so that digits that carry no information
766    ** will not be printed. This is done in two steps.
767    **  1. We scan the symbol table to find the bits that differ
768    **     in at least 2 addresses.
769    **  2. We choose one of the possible masks. There are 8 possible
770    **     masks for 32-bit integer, and 16 possible masks for 64-bit
771    **     integers.
772    */
773
774    /* Find the bits that are different. */
775    refAddr = (unsigned long) Cudd_Regular(f[0]);
776    diff = 0;
777    gen = st_init_gen(visited);
778    while (st_gen(gen, &scan, NULL)) {
779        diff |= refAddr ^ (unsigned long) scan;
780    }
781    st_free_gen(gen);
782
783    /* Choose the mask. */
784    for (i = 0; (unsigned) i < 8 * sizeof(unsigned long); i += 4) {
785        mask = (1 << i) - 1;
786        if (diff <= mask) break;
787    }
788    st_free_table(visited);
789
790    /* Build a bit array with the support of f. */
791    sorted = ALLOC(int,nvars);
792    if (sorted == NULL) {
793        dd->errorCode = CUDD_MEMORY_OUT;
794        goto failure;
795    }
796    for (i = 0; i < nvars; i++) sorted[i] = 0;
797
798    /* Take the union of the supports of each output function. */
799    support = Cudd_VectorSupport(dd,f,n);
800    if (support == NULL) goto failure;
801    cuddRef(support);
802    scan = support;
803    while (!cuddIsConstant(scan)) {
804        sorted[scan->index] = 1;
805        scan = cuddT(scan);
806    }
807    Cudd_RecursiveDeref(dd,support);
808    support = NULL; /* so that we do not try to free it in case of failure */
809    for (i = 0; i < nvars; i++) {
810        if (sorted[dd->invperm[i]]) {
811            if (inames == NULL || inames[dd->invperm[i]] == NULL) {
812                retval = fprintf(fp,"v%d", dd->invperm[i]);
813            } else {
814                retval = fprintf(fp,"%s", inames[dd->invperm[i]]);
815            }
816            if (retval == EOF) goto failure;
817        }
818        retval = fprintf(fp,"%s", i == nvars - 1 ? "\n" : " * ");
819        if (retval == EOF) goto failure;
820    }
821    FREE(sorted);
822    sorted = NULL;
823
824    /* Initialize symbol table for visited nodes. */
825    visited = st_init_table(st_ptrcmp, st_ptrhash);
826    if (visited == NULL) goto failure;
827
828    /* Call the function that really gets the job done. */
829    for (i = 0; i < n; i++) {
830        retval = ddDoDumpDDcal(dd,Cudd_Regular(f[i]),fp,visited,inames,mask);
831        if (retval == 0) goto failure;
832        if (onames == NULL) {
833            retval = fprintf(fp, "f%d = ", i);
834        } else {
835            retval = fprintf(fp, "%s = ", onames[i]);
836        }
837        if (retval == EOF) goto failure;
838        retval = fprintf(fp, "n%lx%s\n",
839                         ((unsigned long) f[i] & mask) /
840                         (unsigned long) sizeof(DdNode),
841                         Cudd_IsComplement(f[i]) ? "'" : "");
842        if (retval == EOF) goto failure;
843    }
844
845    /* Write trailer and return. */
846    retval = fprintf(fp, "[");
847    if (retval == EOF) goto failure;
848    for (i = 0; i < n; i++) {
849        if (onames == NULL) {
850            retval = fprintf(fp, "f%d", i);
851        } else {
852            retval = fprintf(fp, "%s", onames[i]);
853        }
854        retval = fprintf(fp, "%s", i == n-1 ? "" : " ");
855        if (retval == EOF) goto failure;
856    }
857    retval = fprintf(fp, "]\n");
858    if (retval == EOF) goto failure;
859
860    st_free_table(visited);
861    return(1);
862
863failure:
864    if (sorted != NULL) FREE(sorted);
865    if (support != NULL) Cudd_RecursiveDeref(dd,support);
866    if (visited != NULL) st_free_table(visited);
867    return(0);
868
869} /* end of Cudd_DumpDDcal */
870
871
872/**Function********************************************************************
873
874  Synopsis    [Writes factored forms representing the argument BDDs.]
875
876  Description [Writes factored forms representing the argument BDDs.
877  The format of the factored form is the one used in the genlib files
878  for technology mapping in sis.  It returns 1 in case of success; 0
879  otherwise (e.g., file system full).  Cudd_DumpFactoredForm does not
880  close the file: This is the caller responsibility. Caution must be
881  exercised because a factored form may be exponentially larger than
882  the argument BDD.  If the argument inames is non-null, it is assumed
883  to hold the pointers to the names of the inputs. Similarly for
884  onames.]
885
886  SideEffects [None]
887
888  SeeAlso     [Cudd_DumpDot Cudd_PrintDebug Cudd_DumpBlif Cudd_DumpDaVinci
889  Cudd_DumpDDcal]
890
891******************************************************************************/
892int
893Cudd_DumpFactoredForm(
894  DdManager * dd /* manager */,
895  int  n /* number of output nodes to be dumped */,
896  DdNode ** f /* array of output nodes to be dumped */,
897  char ** inames /* array of input names (or NULL) */,
898  char ** onames /* array of output names (or NULL) */,
899  FILE * fp /* pointer to the dump file */)
900{
901    int         retval;
902    int         i;
903
904    /* Call the function that really gets the job done. */
905    for (i = 0; i < n; i++) {
906        if (onames == NULL) {
907            retval = fprintf(fp, "f%d = ", i);
908        } else {
909            retval = fprintf(fp, "%s = ", onames[i]);
910        }
911        if (retval == EOF) return(0);
912        if (f[i] == DD_ONE(dd)) {
913            retval = fprintf(fp, "CONST1");
914            if (retval == EOF) return(0);
915        } else if (f[i] == Cudd_Not(DD_ONE(dd)) || f[i] == DD_ZERO(dd)) {
916            retval = fprintf(fp, "CONST0");
917            if (retval == EOF) return(0);
918        } else {
919            retval = fprintf(fp, "%s", Cudd_IsComplement(f[i]) ? "!(" : "");
920            if (retval == EOF) return(0);
921            retval = ddDoDumpFactoredForm(dd,Cudd_Regular(f[i]),fp,inames);
922            if (retval == 0) return(0);
923            retval = fprintf(fp, "%s", Cudd_IsComplement(f[i]) ? ")" : "");
924            if (retval == EOF) return(0);
925        }
926        retval = fprintf(fp, "%s", i == n-1 ? "" : "\n");
927        if (retval == EOF) return(0);
928    }
929
930    return(1);
931
932} /* end of Cudd_DumpFactoredForm */
933
934
935/*---------------------------------------------------------------------------*/
936/* Definition of internal functions                                          */
937/*---------------------------------------------------------------------------*/
938
939
940/*---------------------------------------------------------------------------*/
941/* Definition of static functions                                            */
942/*---------------------------------------------------------------------------*/
943
944
945/**Function********************************************************************
946
947  Synopsis    [Performs the recursive step of Cudd_DumpBlif.]
948
949  Description [Performs the recursive step of Cudd_DumpBlif. Traverses
950  the BDD f and writes a multiplexer-network description to the file
951  pointed by fp in blif format. f is assumed to be a regular pointer
952  and ddDoDumpBlif guarantees this assumption in the recursive calls.]
953
954  SideEffects [None]
955
956  SeeAlso     []
957
958******************************************************************************/
959static int
960ddDoDumpBlif(
961  DdManager * dd,
962  DdNode * f,
963  FILE * fp,
964  st_table * visited,
965  char ** names)
966{
967    DdNode      *T, *E;
968    int         retval;
969
970#ifdef DD_DEBUG
971    assert(!Cudd_IsComplement(f));
972#endif
973
974    /* If already visited, nothing to do. */
975    if (st_is_member(visited, (char *) f) == 1)
976        return(1);
977
978    /* Check for abnormal condition that should never happen. */
979    if (f == NULL)
980        return(0);
981
982    /* Mark node as visited. */
983    if (st_insert(visited, (char *) f, NULL) == ST_OUT_OF_MEM)
984        return(0);
985
986    /* Check for special case: If constant node, generate constant 1. */
987    if (f == DD_ONE(dd)) {
988#if SIZEOF_VOID_P == 8
989        retval = fprintf(fp, ".names %lx\n1\n",(unsigned long) f / (unsigned long) sizeof(DdNode));
990#else
991        retval = fprintf(fp, ".names %x\n1\n",(unsigned) f / (unsigned) sizeof(DdNode));
992#endif
993        if (retval == EOF) {
994            return(0);
995        } else {
996            return(1);
997        }
998    }
999
1000    /* Check whether this is an ADD. We deal with 0-1 ADDs, but not
1001    ** with the general case.
1002    */
1003    if (f == DD_ZERO(dd)) {
1004#if SIZEOF_VOID_P == 8
1005        retval = fprintf(fp, ".names %lx\n",(unsigned long) f / (unsigned long) sizeof(DdNode));
1006#else
1007        retval = fprintf(fp, ".names %x\n",(unsigned) f / (unsigned) sizeof(DdNode));
1008#endif
1009        if (retval == EOF) {
1010            return(0);
1011        } else {
1012            return(1);
1013        }
1014    }
1015    if (cuddIsConstant(f))
1016        return(0);
1017
1018    /* Recursive calls. */
1019    T = cuddT(f);
1020    retval = ddDoDumpBlif(dd,T,fp,visited,names);
1021    if (retval != 1) return(retval);
1022    E = Cudd_Regular(cuddE(f));
1023    retval = ddDoDumpBlif(dd,E,fp,visited,names);
1024    if (retval != 1) return(retval);
1025
1026    /* Write multiplexer taking complement arc into account. */
1027    if (names != NULL) {
1028        retval = fprintf(fp,".names %s", names[f->index]);
1029    } else {
1030        retval = fprintf(fp,".names %d", f->index);
1031    }
1032    if (retval == EOF)
1033        return(0);
1034
1035#if SIZEOF_VOID_P == 8
1036    if (Cudd_IsComplement(cuddE(f))) {
1037        retval = fprintf(fp," %lx %lx %lx\n11- 1\n0-0 1\n",
1038            (unsigned long) T / (unsigned long) sizeof(DdNode),
1039            (unsigned long) E / (unsigned long) sizeof(DdNode),
1040            (unsigned long) f / (unsigned long) sizeof(DdNode));
1041    } else {
1042        retval = fprintf(fp," %lx %lx %lx\n11- 1\n0-1 1\n",
1043            (unsigned long) T / (unsigned long) sizeof(DdNode),
1044            (unsigned long) E / (unsigned long) sizeof(DdNode),
1045            (unsigned long) f / (unsigned long) sizeof(DdNode));
1046    }
1047#else
1048    if (Cudd_IsComplement(cuddE(f))) {
1049        retval = fprintf(fp," %x %x %x\n11- 1\n0-0 1\n",
1050            (unsigned) T / (unsigned) sizeof(DdNode),
1051            (unsigned) E / (unsigned) sizeof(DdNode),
1052            (unsigned) f / (unsigned) sizeof(DdNode));
1053    } else {
1054        retval = fprintf(fp," %x %x %x\n11- 1\n0-1 1\n",
1055            (unsigned) T / (unsigned) sizeof(DdNode),
1056            (unsigned) E / (unsigned) sizeof(DdNode),
1057            (unsigned) f / (unsigned) sizeof(DdNode));
1058    }
1059#endif
1060    if (retval == EOF) {
1061        return(0);
1062    } else {
1063        return(1);
1064    }
1065
1066} /* end of ddDoDumpBlif */
1067
1068
1069/**Function********************************************************************
1070
1071  Synopsis    [Performs the recursive step of Cudd_DumpDaVinci.]
1072
1073  Description [Performs the recursive step of Cudd_DumpDaVinci. Traverses
1074  the BDD f and writes a term expression to the file
1075  pointed by fp in daVinci format. f is assumed to be a regular pointer
1076  and ddDoDumpDaVinci guarantees this assumption in the recursive calls.]
1077
1078  SideEffects [None]
1079
1080  SeeAlso     []
1081
1082******************************************************************************/
1083static int
1084ddDoDumpDaVinci(
1085  DdManager * dd,
1086  DdNode * f,
1087  FILE * fp,
1088  st_table * visited,
1089  char ** names,
1090  unsigned long mask)
1091{
1092    DdNode        *T, *E;
1093    int           retval;
1094    unsigned long id;
1095
1096#ifdef DD_DEBUG
1097    assert(!Cudd_IsComplement(f));
1098#endif
1099
1100    id = ((unsigned long) f & mask) / sizeof(DdNode);
1101
1102    /* If already visited, insert a reference. */
1103    if (st_is_member(visited, (char *) f) == 1) {
1104        retval = fprintf(fp,"r(\"%lx\")", id);
1105        if (retval == EOF) {
1106            return(0);
1107        } else {
1108            return(1);
1109        }
1110    }
1111
1112    /* Check for abnormal condition that should never happen. */
1113    if (f == NULL)
1114        return(0);
1115
1116    /* Mark node as visited. */
1117    if (st_insert(visited, (char *) f, NULL) == ST_OUT_OF_MEM)
1118        return(0);
1119
1120    /* Check for special case: If constant node, generate constant 1. */
1121    if (Cudd_IsConstant(f)) {
1122        retval = fprintf(fp, "l(\"%lx\",n(\"constant\",[a(\"OBJECT\",\"%g\")],[]))", id, cuddV(f));
1123        if (retval == EOF) {
1124            return(0);
1125        } else {
1126            return(1);
1127        }
1128    }
1129
1130    /* Recursive calls. */
1131    if (names != NULL) {
1132        retval = fprintf(fp,
1133                         "l(\"%lx\",n(\"internal\",[a(\"OBJECT\",\"%s\"),",
1134                         id, names[f->index]);
1135    } else {
1136        retval = fprintf(fp,
1137                         "l(\"%lx\",n(\"internal\",[a(\"OBJECT\",\"%d\"),",
1138                         id, f->index);
1139    }
1140    retval = fprintf(fp, "a(\"_GO\",\"ellipse\")],[e(\"then\",[a(\"EDGECOLOR\",\"blue\"),a(\"_DIR\",\"none\")],");
1141    if (retval == EOF) return(0);
1142    T = cuddT(f);
1143    retval = ddDoDumpDaVinci(dd,T,fp,visited,names,mask);
1144    if (retval != 1) return(retval);
1145    retval = fprintf(fp, "),e(\"else\",[a(\"EDGECOLOR\",\"%s\"),a(\"_DIR\",\"none\")],",
1146                     Cudd_IsComplement(cuddE(f)) ? "red" : "green");
1147    if (retval == EOF) return(0);
1148    E = Cudd_Regular(cuddE(f));
1149    retval = ddDoDumpDaVinci(dd,E,fp,visited,names,mask);
1150    if (retval != 1) return(retval);
1151
1152    retval = fprintf(fp,")]))");
1153    if (retval == EOF) {
1154        return(0);
1155    } else {
1156        return(1);
1157    }
1158
1159} /* end of ddDoDumpDaVinci */
1160
1161
1162/**Function********************************************************************
1163
1164  Synopsis    [Performs the recursive step of Cudd_DumpDDcal.]
1165
1166  Description [Performs the recursive step of Cudd_DumpDDcal. Traverses
1167  the BDD f and writes a line for each node to the file
1168  pointed by fp in DDcal format. f is assumed to be a regular pointer
1169  and ddDoDumpDDcal guarantees this assumption in the recursive calls.]
1170
1171  SideEffects [None]
1172
1173  SeeAlso     []
1174
1175******************************************************************************/
1176static int
1177ddDoDumpDDcal(
1178  DdManager * dd,
1179  DdNode * f,
1180  FILE * fp,
1181  st_table * visited,
1182  char ** names,
1183  unsigned long mask)
1184{
1185    DdNode        *T, *E;
1186    int           retval;
1187    unsigned long id, idT, idE;
1188
1189#ifdef DD_DEBUG
1190    assert(!Cudd_IsComplement(f));
1191#endif
1192
1193    id = ((unsigned long) f & mask) / sizeof(DdNode);
1194
1195    /* If already visited, do nothing. */
1196    if (st_is_member(visited, (char *) f) == 1) {
1197        return(1);
1198    }
1199
1200    /* Check for abnormal condition that should never happen. */
1201    if (f == NULL)
1202        return(0);
1203
1204    /* Mark node as visited. */
1205    if (st_insert(visited, (char *) f, NULL) == ST_OUT_OF_MEM)
1206        return(0);
1207
1208    /* Check for special case: If constant node, assign constant. */
1209    if (Cudd_IsConstant(f)) {
1210        if (f != DD_ONE(dd) && f != DD_ZERO(dd))
1211            return(0);
1212        retval = fprintf(fp, "n%lx = %g\n", id, cuddV(f));
1213        if (retval == EOF) {
1214            return(0);
1215        } else {
1216            return(1);
1217        }
1218    }
1219
1220    /* Recursive calls. */
1221    T = cuddT(f);
1222    retval = ddDoDumpDDcal(dd,T,fp,visited,names,mask);
1223    if (retval != 1) return(retval);
1224    E = Cudd_Regular(cuddE(f));
1225    retval = ddDoDumpDDcal(dd,E,fp,visited,names,mask);
1226    if (retval != 1) return(retval);
1227    idT = ((unsigned long) T & mask) / sizeof(DdNode);
1228    idE = ((unsigned long) E & mask) / sizeof(DdNode);
1229    if (names != NULL) {
1230        retval = fprintf(fp, "n%lx = %s * n%lx + %s' * n%lx%s\n",
1231                         id, names[f->index], idT, names[f->index],
1232                         idE, Cudd_IsComplement(cuddE(f)) ? "'" : "");
1233    } else {
1234        retval = fprintf(fp, "n%lx = v%d * n%lx + v%d' * n%lx%s\n",
1235                         id, f->index, idT, f->index,
1236                         idE, Cudd_IsComplement(cuddE(f)) ? "'" : "");
1237    }
1238    if (retval == EOF) {
1239        return(0);
1240    } else {
1241        return(1);
1242    }
1243
1244} /* end of ddDoDumpDDcal */
1245
1246
1247/**Function********************************************************************
1248
1249  Synopsis    [Performs the recursive step of Cudd_DumpFactoredForm.]
1250
1251  Description [Performs the recursive step of
1252  Cudd_DumpFactoredForm. Traverses the BDD f and writes a factored
1253  form for each node to the file pointed by fp in terms of the
1254  factored forms of the children. Constants are propagated, and
1255  absorption is applied.  f is assumed to be a regular pointer and
1256  ddDoDumpFActoredForm guarantees this assumption in the recursive
1257  calls.]
1258
1259  SideEffects [None]
1260
1261  SeeAlso     [Cudd_DumpFactoredForm]
1262
1263******************************************************************************/
1264static int
1265ddDoDumpFactoredForm(
1266  DdManager * dd,
1267  DdNode * f,
1268  FILE * fp,
1269  char ** names)
1270{
1271    DdNode      *T, *E;
1272    int         retval;
1273
1274#ifdef DD_DEBUG
1275    assert(!Cudd_IsComplement(f));
1276    assert(!Cudd_IsConstant(f));
1277#endif
1278
1279    /* Check for abnormal condition that should never happen. */
1280    if (f == NULL)
1281        return(0);
1282
1283    /* Recursive calls. */
1284    T = cuddT(f);
1285    E = cuddE(f);
1286    if (T != DD_ZERO(dd)) {
1287        if (E != DD_ONE(dd)) {
1288            if (names != NULL) {
1289                retval = fprintf(fp, "%s", names[f->index]);
1290            } else {
1291                retval = fprintf(fp, "x%d", f->index);
1292            }
1293            if (retval == EOF) return(0);
1294        }
1295        if (T != DD_ONE(dd)) {
1296            retval = fprintf(fp, "%s(", E != DD_ONE(dd) ? " * " : "");
1297            if (retval == EOF) return(0);
1298            retval = ddDoDumpFactoredForm(dd,T,fp,names);
1299            if (retval != 1) return(retval);
1300            retval = fprintf(fp, ")");
1301            if (retval == EOF) return(0);
1302        }
1303        if (E == Cudd_Not(DD_ONE(dd)) || E == DD_ZERO(dd)) return(1);
1304        retval = fprintf(fp, " + ");
1305        if (retval == EOF) return(0);
1306    }
1307    E = Cudd_Regular(E);
1308    if (T != DD_ONE(dd)) {
1309        if (names != NULL) {
1310            retval = fprintf(fp, "!%s", names[f->index]);
1311        } else {
1312            retval = fprintf(fp, "!x%d", f->index);
1313        }
1314        if (retval == EOF) return(0);
1315    }
1316    if (E != DD_ONE(dd)) {
1317        retval = fprintf(fp, "%s%s(", T != DD_ONE(dd) ? " * " : "",
1318                         E != cuddE(f) ? "!" : "");
1319        if (retval == EOF) return(0);
1320        retval = ddDoDumpFactoredForm(dd,E,fp,names);
1321        if (retval != 1) return(retval);
1322        retval = fprintf(fp, ")");
1323        if (retval == EOF) return(0);
1324    }
1325    return(1);
1326
1327} /* end of ddDoDumpFactoredForm */
1328
Note: See TracBrowser for help on using the repository browser.