source: vis_dev/glu-2.3/src/cuBdd/cuddExport.c @ 104

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

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