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