1 /**CFile***********************************************************************
2
3 FileName [cuddZddUtil.c]
4
5 PackageName [cudd]
6
7 Synopsis [Utility functions for ZDDs.]
8
9 Description [External procedures included in this module:
10 <ul>
11 <li> Cudd_zddPrintMinterm()
12 <li> Cudd_zddPrintCover()
13 <li> Cudd_zddPrintDebug()
14 <li> Cudd_zddFirstPath()
15 <li> Cudd_zddNextPath()
16 <li> Cudd_zddCoverPathToString()
17 <li> Cudd_zddDumpDot()
18 </ul>
19 Internal procedures included in this module:
20 <ul>
21 <li> cuddZddP()
22 </ul>
23 Static procedures included in this module:
24 <ul>
25 <li> zp2()
26 <li> zdd_print_minterm_aux()
27 <li> zddPrintCoverAux()
28 </ul>
29 ]
30
31 SeeAlso []
32
33 Author [Hyong-Kyoon Shin, In-Ho Moon, Fabio Somenzi]
34
35 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
36
37 All rights reserved.
38
39 Redistribution and use in source and binary forms, with or without
40 modification, are permitted provided that the following conditions
41 are met:
42
43 Redistributions of source code must retain the above copyright
44 notice, this list of conditions and the following disclaimer.
45
46 Redistributions in binary form must reproduce the above copyright
47 notice, this list of conditions and the following disclaimer in the
48 documentation and/or other materials provided with the distribution.
49
50 Neither the name of the University of Colorado nor the names of its
51 contributors may be used to endorse or promote products derived from
52 this software without specific prior written permission.
53
54 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
55 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
56 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
57 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
58 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
59 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
60 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
61 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
62 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
63 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
64 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
65 POSSIBILITY OF SUCH DAMAGE.]
66
67 ******************************************************************************/
68
69 #include "misc/util/util_hack.h"
70 #include "cuddInt.h"
71
72 ABC_NAMESPACE_IMPL_START
73
74
75
76 /*---------------------------------------------------------------------------*/
77 /* Constant declarations */
78 /*---------------------------------------------------------------------------*/
79
80
81 /*---------------------------------------------------------------------------*/
82 /* Stucture declarations */
83 /*---------------------------------------------------------------------------*/
84
85
86 /*---------------------------------------------------------------------------*/
87 /* Type declarations */
88 /*---------------------------------------------------------------------------*/
89
90
91 /*---------------------------------------------------------------------------*/
92 /* Variable declarations */
93 /*---------------------------------------------------------------------------*/
94
95 #ifndef lint
96 static char rcsid[] DD_UNUSED = "$Id: cuddZddUtil.c,v 1.27 2009/03/08 02:49:02 fabio Exp $";
97 #endif
98
99 /*---------------------------------------------------------------------------*/
100 /* Macro declarations */
101 /*---------------------------------------------------------------------------*/
102
103
104 /**AutomaticStart*************************************************************/
105
106 /*---------------------------------------------------------------------------*/
107 /* Static function prototypes */
108 /*---------------------------------------------------------------------------*/
109
110 static int zp2 (DdManager *zdd, DdNode *f, st__table *t);
111 static void zdd_print_minterm_aux (DdManager *zdd, DdNode *node, int level, int *list);
112 static void zddPrintCoverAux (DdManager *zdd, DdNode *node, int level, int *list);
113
114 /**AutomaticEnd***************************************************************/
115
116
117 /*---------------------------------------------------------------------------*/
118 /* Definition of exported functions */
119 /*---------------------------------------------------------------------------*/
120
121
122 /**Function********************************************************************
123
124 Synopsis [Prints a disjoint sum of product form for a ZDD.]
125
126 Description [Prints a disjoint sum of product form for a ZDD. Returns 1
127 if successful; 0 otherwise.]
128
129 SideEffects [None]
130
131 SeeAlso [Cudd_zddPrintDebug Cudd_zddPrintCover]
132
133 ******************************************************************************/
134 int
Cudd_zddPrintMinterm(DdManager * zdd,DdNode * node)135 Cudd_zddPrintMinterm(
136 DdManager * zdd,
137 DdNode * node)
138 {
139 int i, size;
140 int *list;
141
142 size = (int)zdd->sizeZ;
143 list = ABC_ALLOC(int, size);
144 if (list == NULL) {
145 zdd->errorCode = CUDD_MEMORY_OUT;
146 return(0);
147 }
148 for (i = 0; i < size; i++) list[i] = 3; /* bogus value should disappear */
149 zdd_print_minterm_aux(zdd, node, 0, list);
150 ABC_FREE(list);
151 return(1);
152
153 } /* end of Cudd_zddPrintMinterm */
154
155
156 /**Function********************************************************************
157
158 Synopsis [Prints a sum of products from a ZDD representing a cover.]
159
160 Description [Prints a sum of products from a ZDD representing a cover.
161 Returns 1 if successful; 0 otherwise.]
162
163 SideEffects [None]
164
165 SeeAlso [Cudd_zddPrintMinterm]
166
167 ******************************************************************************/
168 int
Cudd_zddPrintCover(DdManager * zdd,DdNode * node)169 Cudd_zddPrintCover(
170 DdManager * zdd,
171 DdNode * node)
172 {
173 int i, size;
174 int *list;
175
176 size = (int)zdd->sizeZ;
177 if (size % 2 != 0) return(0); /* number of variables should be even */
178 list = ABC_ALLOC(int, size);
179 if (list == NULL) {
180 zdd->errorCode = CUDD_MEMORY_OUT;
181 return(0);
182 }
183 for (i = 0; i < size; i++) list[i] = 3; /* bogus value should disappear */
184 zddPrintCoverAux(zdd, node, 0, list);
185 ABC_FREE(list);
186 return(1);
187
188 } /* end of Cudd_zddPrintCover */
189
190
191 /**Function********************************************************************
192
193 Synopsis [Prints to the standard output a ZDD and its statistics.]
194
195 Description [Prints to the standard output a DD and its statistics.
196 The statistics include the number of nodes and the number of minterms.
197 (The number of minterms is also the number of combinations in the set.)
198 The statistics are printed if pr > 0. Specifically:
199 <ul>
200 <li> pr = 0 : prints nothing
201 <li> pr = 1 : prints counts of nodes and minterms
202 <li> pr = 2 : prints counts + disjoint sum of products
203 <li> pr = 3 : prints counts + list of nodes
204 <li> pr > 3 : prints counts + disjoint sum of products + list of nodes
205 </ul>
206 Returns 1 if successful; 0 otherwise.
207 ]
208
209 SideEffects [None]
210
211 SeeAlso []
212
213 ******************************************************************************/
214 int
Cudd_zddPrintDebug(DdManager * zdd,DdNode * f,int n,int pr)215 Cudd_zddPrintDebug(
216 DdManager * zdd,
217 DdNode * f,
218 int n,
219 int pr)
220 {
221 DdNode *empty = DD_ZERO(zdd);
222 int nodes;
223 double minterms;
224 int retval = 1;
225
226 if (f == empty && pr > 0) {
227 (void) fprintf(zdd->out,": is the empty ZDD\n");
228 (void) fflush(zdd->out);
229 return(1);
230 }
231
232 if (pr > 0) {
233 nodes = Cudd_zddDagSize(f);
234 if (nodes == CUDD_OUT_OF_MEM) retval = 0;
235 minterms = Cudd_zddCountMinterm(zdd, f, n);
236 if (minterms == (double)CUDD_OUT_OF_MEM) retval = 0;
237 (void) fprintf(zdd->out,": %d nodes %g minterms\n",
238 nodes, minterms);
239 if (pr > 2)
240 if (!cuddZddP(zdd, f)) retval = 0;
241 if (pr == 2 || pr > 3) {
242 if (!Cudd_zddPrintMinterm(zdd, f)) retval = 0;
243 (void) fprintf(zdd->out,"\n");
244 }
245 (void) fflush(zdd->out);
246 }
247 return(retval);
248
249 } /* end of Cudd_zddPrintDebug */
250
251
252
253 /**Function********************************************************************
254
255 Synopsis [Finds the first path of a ZDD.]
256
257 Description [Defines an iterator on the paths of a ZDD
258 and finds its first path. Returns a generator that contains the
259 information necessary to continue the enumeration if successful; NULL
260 otherwise.<p>
261 A path is represented as an array of literals, which are integers in
262 {0, 1, 2}; 0 represents an else arc out of a node, 1 represents a then arc
263 out of a node, and 2 stands for the absence of a node.
264 The size of the array equals the number of variables in the manager at
265 the time Cudd_zddFirstCube is called.<p>
266 The paths that end in the empty terminal are not enumerated.]
267
268 SideEffects [The first path is returned as a side effect.]
269
270 SeeAlso [Cudd_zddForeachPath Cudd_zddNextPath Cudd_GenFree
271 Cudd_IsGenEmpty]
272
273 ******************************************************************************/
274 DdGen *
Cudd_zddFirstPath(DdManager * zdd,DdNode * f,int ** path)275 Cudd_zddFirstPath(
276 DdManager * zdd,
277 DdNode * f,
278 int ** path)
279 {
280 DdGen *gen;
281 DdNode *top, *next, *prev;
282 int i;
283 int nvars;
284
285 /* Sanity Check. */
286 if (zdd == NULL || f == NULL) return(NULL);
287
288 /* Allocate generator an initialize it. */
289 gen = ABC_ALLOC(DdGen,1);
290 if (gen == NULL) {
291 zdd->errorCode = CUDD_MEMORY_OUT;
292 return(NULL);
293 }
294
295 gen->manager = zdd;
296 gen->type = CUDD_GEN_ZDD_PATHS;
297 gen->status = CUDD_GEN_EMPTY;
298 gen->gen.cubes.cube = NULL;
299 gen->gen.cubes.value = DD_ZERO_VAL;
300 gen->stack.sp = 0;
301 gen->stack.stack = NULL;
302 gen->node = NULL;
303
304 nvars = zdd->sizeZ;
305 gen->gen.cubes.cube = ABC_ALLOC(int,nvars);
306 if (gen->gen.cubes.cube == NULL) {
307 zdd->errorCode = CUDD_MEMORY_OUT;
308 ABC_FREE(gen);
309 return(NULL);
310 }
311 for (i = 0; i < nvars; i++) gen->gen.cubes.cube[i] = 2;
312
313 /* The maximum stack depth is one plus the number of variables.
314 ** because a path may have nodes at all levels, including the
315 ** constant level.
316 */
317 gen->stack.stack = ABC_ALLOC(DdNodePtr, nvars+1);
318 if (gen->stack.stack == NULL) {
319 zdd->errorCode = CUDD_MEMORY_OUT;
320 ABC_FREE(gen->gen.cubes.cube);
321 ABC_FREE(gen);
322 return(NULL);
323 }
324 for (i = 0; i <= nvars; i++) gen->stack.stack[i] = NULL;
325
326 /* Find the first path of the ZDD. */
327 gen->stack.stack[gen->stack.sp] = f; gen->stack.sp++;
328
329 while (1) {
330 top = gen->stack.stack[gen->stack.sp-1];
331 if (!cuddIsConstant(Cudd_Regular(top))) {
332 /* Take the else branch first. */
333 gen->gen.cubes.cube[Cudd_Regular(top)->index] = 0;
334 next = cuddE(Cudd_Regular(top));
335 gen->stack.stack[gen->stack.sp] = Cudd_Not(next); gen->stack.sp++;
336 } else if (Cudd_Regular(top) == DD_ZERO(zdd)) {
337 /* Backtrack. */
338 while (1) {
339 if (gen->stack.sp == 1) {
340 /* The current node has no predecessor. */
341 gen->status = CUDD_GEN_EMPTY;
342 gen->stack.sp--;
343 goto done;
344 }
345 prev = Cudd_Regular(gen->stack.stack[gen->stack.sp-2]);
346 next = cuddT(prev);
347 if (next != top) { /* follow the then branch next */
348 gen->gen.cubes.cube[prev->index] = 1;
349 gen->stack.stack[gen->stack.sp-1] = next;
350 break;
351 }
352 /* Pop the stack and try again. */
353 gen->gen.cubes.cube[prev->index] = 2;
354 gen->stack.sp--;
355 top = gen->stack.stack[gen->stack.sp-1];
356 }
357 } else {
358 gen->status = CUDD_GEN_NONEMPTY;
359 gen->gen.cubes.value = cuddV(Cudd_Regular(top));
360 goto done;
361 }
362 }
363
364 done:
365 *path = gen->gen.cubes.cube;
366 return(gen);
367
368 } /* end of Cudd_zddFirstPath */
369
370
371 /**Function********************************************************************
372
373 Synopsis [Generates the next path of a ZDD.]
374
375 Description [Generates the next path of a ZDD onset,
376 using generator gen. Returns 0 if the enumeration is completed; 1
377 otherwise.]
378
379 SideEffects [The path is returned as a side effect. The
380 generator is modified.]
381
382 SeeAlso [Cudd_zddForeachPath Cudd_zddFirstPath Cudd_GenFree
383 Cudd_IsGenEmpty]
384
385 ******************************************************************************/
386 int
Cudd_zddNextPath(DdGen * gen,int ** path)387 Cudd_zddNextPath(
388 DdGen * gen,
389 int ** path)
390 {
391 DdNode *top, *next, *prev;
392 DdManager *zdd = gen->manager;
393
394 /* Backtrack from previously reached terminal node. */
395 while (1) {
396 if (gen->stack.sp == 1) {
397 /* The current node has no predecessor. */
398 gen->status = CUDD_GEN_EMPTY;
399 gen->stack.sp--;
400 goto done;
401 }
402 top = gen->stack.stack[gen->stack.sp-1];
403 prev = Cudd_Regular(gen->stack.stack[gen->stack.sp-2]);
404 next = cuddT(prev);
405 if (next != top) { /* follow the then branch next */
406 gen->gen.cubes.cube[prev->index] = 1;
407 gen->stack.stack[gen->stack.sp-1] = next;
408 break;
409 }
410 /* Pop the stack and try again. */
411 gen->gen.cubes.cube[prev->index] = 2;
412 gen->stack.sp--;
413 }
414
415 while (1) {
416 top = gen->stack.stack[gen->stack.sp-1];
417 if (!cuddIsConstant(Cudd_Regular(top))) {
418 /* Take the else branch first. */
419 gen->gen.cubes.cube[Cudd_Regular(top)->index] = 0;
420 next = cuddE(Cudd_Regular(top));
421 gen->stack.stack[gen->stack.sp] = Cudd_Not(next); gen->stack.sp++;
422 } else if (Cudd_Regular(top) == DD_ZERO(zdd)) {
423 /* Backtrack. */
424 while (1) {
425 if (gen->stack.sp == 1) {
426 /* The current node has no predecessor. */
427 gen->status = CUDD_GEN_EMPTY;
428 gen->stack.sp--;
429 goto done;
430 }
431 prev = Cudd_Regular(gen->stack.stack[gen->stack.sp-2]);
432 next = cuddT(prev);
433 if (next != top) { /* follow the then branch next */
434 gen->gen.cubes.cube[prev->index] = 1;
435 gen->stack.stack[gen->stack.sp-1] = next;
436 break;
437 }
438 /* Pop the stack and try again. */
439 gen->gen.cubes.cube[prev->index] = 2;
440 gen->stack.sp--;
441 top = gen->stack.stack[gen->stack.sp-1];
442 }
443 } else {
444 gen->status = CUDD_GEN_NONEMPTY;
445 gen->gen.cubes.value = cuddV(Cudd_Regular(top));
446 goto done;
447 }
448 }
449
450 done:
451 if (gen->status == CUDD_GEN_EMPTY) return(0);
452 *path = gen->gen.cubes.cube;
453 return(1);
454
455 } /* end of Cudd_zddNextPath */
456
457
458 /**Function********************************************************************
459
460 Synopsis [Converts a path of a ZDD representing a cover to a string.]
461
462 Description [Converts a path of a ZDD representing a cover to a
463 string. The string represents an implicant of the cover. The path
464 is typically produced by Cudd_zddForeachPath. Returns a pointer to
465 the string if successful; NULL otherwise. If the str input is NULL,
466 it allocates a new string. The string passed to this function must
467 have enough room for all variables and for the terminator.]
468
469 SideEffects [None]
470
471 SeeAlso [Cudd_zddForeachPath]
472
473 ******************************************************************************/
474 char *
Cudd_zddCoverPathToString(DdManager * zdd,int * path,char * str)475 Cudd_zddCoverPathToString(
476 DdManager *zdd /* DD manager */,
477 int *path /* path of ZDD representing a cover */,
478 char *str /* pointer to string to use if != NULL */
479 )
480 {
481 int nvars = zdd->sizeZ;
482 int i;
483 char *res;
484
485 if (nvars & 1) return(NULL);
486 nvars >>= 1;
487 if (str == NULL) {
488 res = ABC_ALLOC(char, nvars+1);
489 if (res == NULL) return(NULL);
490 } else {
491 res = str;
492 }
493 for (i = 0; i < nvars; i++) {
494 int v = (path[2*i] << 2) | path[2*i+1];
495 switch (v) {
496 case 0:
497 case 2:
498 case 8:
499 case 10:
500 res[i] = '-';
501 break;
502 case 1:
503 case 9:
504 res[i] = '0';
505 break;
506 case 4:
507 case 6:
508 res[i] = '1';
509 break;
510 default:
511 res[i] = '?';
512 }
513 }
514 res[nvars] = 0;
515
516 return(res);
517
518 } /* end of Cudd_zddCoverPathToString */
519
520
521 /**Function********************************************************************
522
523 Synopsis [Writes a dot file representing the argument ZDDs.]
524
525 Description [Writes a file representing the argument ZDDs in a format
526 suitable for the graph drawing program dot.
527 It returns 1 in case of success; 0 otherwise (e.g., out-of-memory,
528 file system full).
529 Cudd_zddDumpDot does not close the file: This is the caller
530 responsibility. Cudd_zddDumpDot uses a minimal unique subset of the
531 hexadecimal address of a node as name for it.
532 If the argument inames is non-null, it is assumed to hold the pointers
533 to the names of the inputs. Similarly for onames.
534 Cudd_zddDumpDot uses the following convention to draw arcs:
535 <ul>
536 <li> solid line: THEN arcs;
537 <li> dashed line: ELSE arcs.
538 </ul>
539 The dot options are chosen so that the drawing fits on a letter-size
540 sheet.
541 ]
542
543 SideEffects [None]
544
545 SeeAlso [Cudd_DumpDot Cudd_zddPrintDebug]
546
547 ******************************************************************************/
548 int
Cudd_zddDumpDot(DdManager * dd,int n,DdNode ** f,char ** inames,char ** onames,FILE * fp)549 Cudd_zddDumpDot(
550 DdManager * dd /* manager */,
551 int n /* number of output nodes to be dumped */,
552 DdNode ** f /* array of output nodes to be dumped */,
553 char ** inames /* array of input names (or NULL) */,
554 char ** onames /* array of output names (or NULL) */,
555 FILE * fp /* pointer to the dump file */)
556 {
557 DdNode *support = NULL;
558 DdNode *scan;
559 int *sorted = NULL;
560 int nvars = dd->sizeZ;
561 st__table *visited = NULL;
562 st__generator *gen;
563 int retval;
564 int i, j;
565 int slots;
566 DdNodePtr *nodelist;
567 long refAddr, diff, mask;
568
569 /* Build a bit array with the support of f. */
570 sorted = ABC_ALLOC(int,nvars);
571 if (sorted == NULL) {
572 dd->errorCode = CUDD_MEMORY_OUT;
573 goto failure;
574 }
575 for (i = 0; i < nvars; i++) sorted[i] = 0;
576
577 /* Take the union of the supports of each output function. */
578 for (i = 0; i < n; i++) {
579 support = Cudd_Support(dd,f[i]);
580 if (support == NULL) goto failure;
581 cuddRef(support);
582 scan = support;
583 while (!cuddIsConstant(scan)) {
584 sorted[scan->index] = 1;
585 scan = cuddT(scan);
586 }
587 Cudd_RecursiveDeref(dd,support);
588 }
589 support = NULL; /* so that we do not try to free it in case of failure */
590
591 /* Initialize symbol table for visited nodes. */
592 visited = st__init_table( st__ptrcmp, st__ptrhash);
593 if (visited == NULL) goto failure;
594
595 /* Collect all the nodes of this DD in the symbol table. */
596 for (i = 0; i < n; i++) {
597 retval = cuddCollectNodes(f[i],visited);
598 if (retval == 0) goto failure;
599 }
600
601 /* Find how many most significant hex digits are identical
602 ** in the addresses of all the nodes. Build a mask based
603 ** on this knowledge, so that digits that carry no information
604 ** will not be printed. This is done in two steps.
605 ** 1. We scan the symbol table to find the bits that differ
606 ** in at least 2 addresses.
607 ** 2. We choose one of the possible masks. There are 8 possible
608 ** masks for 32-bit integer, and 16 possible masks for 64-bit
609 ** integers.
610 */
611
612 /* Find the bits that are different. */
613 refAddr = (long) f[0];
614 diff = 0;
615 gen = st__init_gen(visited);
616 while ( st__gen(gen, (const char **)&scan, NULL)) {
617 diff |= refAddr ^ (long) scan;
618 }
619 st__free_gen(gen);
620
621 /* Choose the mask. */
622 for (i = 0; (unsigned) i < 8 * sizeof(long); i += 4) {
623 mask = (1 << i) - 1;
624 if (diff <= mask) break;
625 }
626
627 /* Write the header and the global attributes. */
628 retval = fprintf(fp,"digraph \"ZDD\" {\n");
629 if (retval == EOF) return(0);
630 retval = fprintf(fp,
631 "size = \"7.5,10\"\ncenter = true;\nedge [dir = none];\n");
632 if (retval == EOF) return(0);
633
634 /* Write the input name subgraph by scanning the support array. */
635 retval = fprintf(fp,"{ node [shape = plaintext];\n");
636 if (retval == EOF) goto failure;
637 retval = fprintf(fp," edge [style = invis];\n");
638 if (retval == EOF) goto failure;
639 /* We use a name ("CONST NODES") with an embedded blank, because
640 ** it is unlikely to appear as an input name.
641 */
642 retval = fprintf(fp," \"CONST NODES\" [style = invis];\n");
643 if (retval == EOF) goto failure;
644 for (i = 0; i < nvars; i++) {
645 if (sorted[dd->invpermZ[i]]) {
646 if (inames == NULL) {
647 retval = fprintf(fp,"\" %d \" -> ", dd->invpermZ[i]);
648 } else {
649 retval = fprintf(fp,"\" %s \" -> ", inames[dd->invpermZ[i]]);
650 }
651 if (retval == EOF) goto failure;
652 }
653 }
654 retval = fprintf(fp,"\"CONST NODES\"; \n}\n");
655 if (retval == EOF) goto failure;
656
657 /* Write the output node subgraph. */
658 retval = fprintf(fp,"{ rank = same; node [shape = box]; edge [style = invis];\n");
659 if (retval == EOF) goto failure;
660 for (i = 0; i < n; i++) {
661 if (onames == NULL) {
662 retval = fprintf(fp,"\"F%d\"", i);
663 } else {
664 retval = fprintf(fp,"\" %s \"", onames[i]);
665 }
666 if (retval == EOF) goto failure;
667 if (i == n - 1) {
668 retval = fprintf(fp,"; }\n");
669 } else {
670 retval = fprintf(fp," -> ");
671 }
672 if (retval == EOF) goto failure;
673 }
674
675 /* Write rank info: All nodes with the same index have the same rank. */
676 for (i = 0; i < nvars; i++) {
677 if (sorted[dd->invpermZ[i]]) {
678 retval = fprintf(fp,"{ rank = same; ");
679 if (retval == EOF) goto failure;
680 if (inames == NULL) {
681 retval = fprintf(fp,"\" %d \";\n", dd->invpermZ[i]);
682 } else {
683 retval = fprintf(fp,"\" %s \";\n", inames[dd->invpermZ[i]]);
684 }
685 if (retval == EOF) goto failure;
686 nodelist = dd->subtableZ[i].nodelist;
687 slots = dd->subtableZ[i].slots;
688 for (j = 0; j < slots; j++) {
689 scan = nodelist[j];
690 while (scan != NULL) {
691 if ( st__is_member(visited,(char *) scan)) {
692 retval = fprintf(fp,"\"%p\";\n", (void *)
693 ((mask & (ptrint) scan) /
694 sizeof(DdNode)));
695 if (retval == EOF) goto failure;
696 }
697 scan = scan->next;
698 }
699 }
700 retval = fprintf(fp,"}\n");
701 if (retval == EOF) goto failure;
702 }
703 }
704
705 /* All constants have the same rank. */
706 retval = fprintf(fp,
707 "{ rank = same; \"CONST NODES\";\n{ node [shape = box]; ");
708 if (retval == EOF) goto failure;
709 nodelist = dd->constants.nodelist;
710 slots = dd->constants.slots;
711 for (j = 0; j < slots; j++) {
712 scan = nodelist[j];
713 while (scan != NULL) {
714 if ( st__is_member(visited,(char *) scan)) {
715 retval = fprintf(fp,"\"%p\";\n", (void *)
716 ((mask & (ptrint) scan) / sizeof(DdNode)));
717 if (retval == EOF) goto failure;
718 }
719 scan = scan->next;
720 }
721 }
722 retval = fprintf(fp,"}\n}\n");
723 if (retval == EOF) goto failure;
724
725 /* Write edge info. */
726 /* Edges from the output nodes. */
727 for (i = 0; i < n; i++) {
728 if (onames == NULL) {
729 retval = fprintf(fp,"\"F%d\"", i);
730 } else {
731 retval = fprintf(fp,"\" %s \"", onames[i]);
732 }
733 if (retval == EOF) goto failure;
734 retval = fprintf(fp," -> \"%p\" [style = solid];\n",
735 (void *) ((mask & (ptrint) f[i]) /
736 sizeof(DdNode)));
737 if (retval == EOF) goto failure;
738 }
739
740 /* Edges from internal nodes. */
741 for (i = 0; i < nvars; i++) {
742 if (sorted[dd->invpermZ[i]]) {
743 nodelist = dd->subtableZ[i].nodelist;
744 slots = dd->subtableZ[i].slots;
745 for (j = 0; j < slots; j++) {
746 scan = nodelist[j];
747 while (scan != NULL) {
748 if ( st__is_member(visited,(char *) scan)) {
749 retval = fprintf(fp,
750 "\"%p\" -> \"%p\";\n",
751 (void *) ((mask & (ptrint) scan) / sizeof(DdNode)),
752 (void *) ((mask & (ptrint) cuddT(scan)) /
753 sizeof(DdNode)));
754 if (retval == EOF) goto failure;
755 retval = fprintf(fp,
756 "\"%p\" -> \"%p\" [style = dashed];\n",
757 (void *) ((mask & (ptrint) scan)
758 / sizeof(DdNode)),
759 (void *) ((mask & (ptrint)
760 cuddE(scan)) /
761 sizeof(DdNode)));
762 if (retval == EOF) goto failure;
763 }
764 scan = scan->next;
765 }
766 }
767 }
768 }
769
770 /* Write constant labels. */
771 nodelist = dd->constants.nodelist;
772 slots = dd->constants.slots;
773 for (j = 0; j < slots; j++) {
774 scan = nodelist[j];
775 while (scan != NULL) {
776 if ( st__is_member(visited,(char *) scan)) {
777 retval = fprintf(fp,"\"%p\" [label = \"%g\"];\n",
778 (void *) ((mask & (ptrint) scan) /
779 sizeof(DdNode)),
780 cuddV(scan));
781 if (retval == EOF) goto failure;
782 }
783 scan = scan->next;
784 }
785 }
786
787 /* Write trailer and return. */
788 retval = fprintf(fp,"}\n");
789 if (retval == EOF) goto failure;
790
791 st__free_table(visited);
792 ABC_FREE(sorted);
793 return(1);
794
795 failure:
796 if (sorted != NULL) ABC_FREE(sorted);
797 if (visited != NULL) st__free_table(visited);
798 return(0);
799
800 } /* end of Cudd_zddDumpBlif */
801
802
803 /*---------------------------------------------------------------------------*/
804 /* Definition of internal functions */
805 /*---------------------------------------------------------------------------*/
806
807
808 /**Function********************************************************************
809
810 Synopsis [Prints a ZDD to the standard output. One line per node is
811 printed.]
812
813 Description [Prints a ZDD to the standard output. One line per node is
814 printed. Returns 1 if successful; 0 otherwise.]
815
816 SideEffects [None]
817
818 SeeAlso [Cudd_zddPrintDebug]
819
820 ******************************************************************************/
821 int
cuddZddP(DdManager * zdd,DdNode * f)822 cuddZddP(
823 DdManager * zdd,
824 DdNode * f)
825 {
826 int retval;
827 st__table *table = st__init_table( st__ptrcmp, st__ptrhash);
828
829 if (table == NULL) return(0);
830
831 retval = zp2(zdd, f, table);
832 st__free_table(table);
833 (void) fputc('\n', zdd->out);
834 return(retval);
835
836 } /* end of cuddZddP */
837
838
839 /*---------------------------------------------------------------------------*/
840 /* Definition of static functions */
841 /*---------------------------------------------------------------------------*/
842
843
844 /**Function********************************************************************
845
846 Synopsis [Performs the recursive step of cuddZddP.]
847
848 Description [Performs the recursive step of cuddZddP. Returns 1 in
849 case of success; 0 otherwise.]
850
851 SideEffects [None]
852
853 SeeAlso []
854
855 ******************************************************************************/
856 static int
zp2(DdManager * zdd,DdNode * f,st__table * t)857 zp2(
858 DdManager * zdd,
859 DdNode * f,
860 st__table * t)
861 {
862 DdNode *n;
863 int T, E;
864 DdNode *base = DD_ONE(zdd);
865
866 if (f == NULL)
867 return(0);
868
869 if (Cudd_IsConstant(f)) {
870 (void)fprintf(zdd->out, "ID = %d\n", (f == base));
871 return(1);
872 }
873 if ( st__is_member(t, (char *)f) == 1)
874 return(1);
875
876 if ( st__insert(t, (char *) f, NULL) == st__OUT_OF_MEM)
877 return(0);
878
879 #if SIZEOF_VOID_P == 8
880 (void) fprintf(zdd->out, "ID = 0x%lx\tindex = %u\tr = %u\t",
881 (ptruint)f / (ptruint) sizeof(DdNode), f->index, f->ref);
882 #else
883 (void) fprintf(zdd->out, "ID = 0x%x\tindex = %hu\tr = %hu\t",
884 (ptruint)f / (ptruint) sizeof(DdNode), f->index, f->ref);
885 #endif
886
887 n = cuddT(f);
888 if (Cudd_IsConstant(n)) {
889 (void) fprintf(zdd->out, "T = %d\t\t", (n == base));
890 T = 1;
891 } else {
892 #if SIZEOF_VOID_P == 8
893 (void) fprintf(zdd->out, "T = 0x%lx\t", (ptruint) n /
894 (ptruint) sizeof(DdNode));
895 #else
896 (void) fprintf(zdd->out, "T = 0x%x\t", (ptruint) n /
897 (ptruint) sizeof(DdNode));
898 #endif
899 T = 0;
900 }
901
902 n = cuddE(f);
903 if (Cudd_IsConstant(n)) {
904 (void) fprintf(zdd->out, "E = %d\n", (n == base));
905 E = 1;
906 } else {
907 #if SIZEOF_VOID_P == 8
908 (void) fprintf(zdd->out, "E = 0x%lx\n", (ptruint) n /
909 (ptruint) sizeof(DdNode));
910 #else
911 (void) fprintf(zdd->out, "E = 0x%x\n", (ptruint) n /
912 (ptruint) sizeof(DdNode));
913 #endif
914 E = 0;
915 }
916
917 if (E == 0)
918 if (zp2(zdd, cuddE(f), t) == 0) return(0);
919 if (T == 0)
920 if (zp2(zdd, cuddT(f), t) == 0) return(0);
921 return(1);
922
923 } /* end of zp2 */
924
925
926 /**Function********************************************************************
927
928 Synopsis [Performs the recursive step of Cudd_zddPrintMinterm.]
929
930 Description []
931
932 SideEffects [None]
933
934 SeeAlso []
935
936 ******************************************************************************/
937 static void
zdd_print_minterm_aux(DdManager * zdd,DdNode * node,int level,int * list)938 zdd_print_minterm_aux(
939 DdManager * zdd /* manager */,
940 DdNode * node /* current node */,
941 int level /* depth in the recursion */,
942 int * list /* current recursion path */)
943 {
944 DdNode *Nv, *Nnv;
945 int i, v;
946 DdNode *base = DD_ONE(zdd);
947
948 if (Cudd_IsConstant(node)) {
949 if (node == base) {
950 /* Check for missing variable. */
951 if (level != zdd->sizeZ) {
952 list[zdd->invpermZ[level]] = 0;
953 zdd_print_minterm_aux(zdd, node, level + 1, list);
954 return;
955 }
956 /* Terminal case: Print one cube based on the current recursion
957 ** path.
958 */
959 for (i = 0; i < zdd->sizeZ; i++) {
960 v = list[i];
961 if (v == 0)
962 (void) fprintf(zdd->out,"0");
963 else if (v == 1)
964 (void) fprintf(zdd->out,"1");
965 else if (v == 3)
966 (void) fprintf(zdd->out,"@"); /* should never happen */
967 else
968 (void) fprintf(zdd->out,"-");
969 }
970 (void) fprintf(zdd->out," 1\n");
971 }
972 } else {
973 /* Check for missing variable. */
974 if (level != cuddIZ(zdd,node->index)) {
975 list[zdd->invpermZ[level]] = 0;
976 zdd_print_minterm_aux(zdd, node, level + 1, list);
977 return;
978 }
979
980 Nnv = cuddE(node);
981 Nv = cuddT(node);
982 if (Nv == Nnv) {
983 list[node->index] = 2;
984 zdd_print_minterm_aux(zdd, Nnv, level + 1, list);
985 return;
986 }
987
988 list[node->index] = 1;
989 zdd_print_minterm_aux(zdd, Nv, level + 1, list);
990 list[node->index] = 0;
991 zdd_print_minterm_aux(zdd, Nnv, level + 1, list);
992 }
993 return;
994
995 } /* end of zdd_print_minterm_aux */
996
997
998 /**Function********************************************************************
999
1000 Synopsis [Performs the recursive step of Cudd_zddPrintCover.]
1001
1002 Description []
1003
1004 SideEffects [None]
1005
1006 SeeAlso []
1007
1008 ******************************************************************************/
1009 static void
zddPrintCoverAux(DdManager * zdd,DdNode * node,int level,int * list)1010 zddPrintCoverAux(
1011 DdManager * zdd /* manager */,
1012 DdNode * node /* current node */,
1013 int level /* depth in the recursion */,
1014 int * list /* current recursion path */)
1015 {
1016 DdNode *Nv, *Nnv;
1017 int i, v;
1018 DdNode *base = DD_ONE(zdd);
1019
1020 if (Cudd_IsConstant(node)) {
1021 if (node == base) {
1022 /* Check for missing variable. */
1023 if (level != zdd->sizeZ) {
1024 list[zdd->invpermZ[level]] = 0;
1025 zddPrintCoverAux(zdd, node, level + 1, list);
1026 return;
1027 }
1028 /* Terminal case: Print one cube based on the current recursion
1029 ** path.
1030 */
1031 for (i = 0; i < zdd->sizeZ; i += 2) {
1032 v = list[i] * 4 + list[i+1];
1033 if (v == 0)
1034 (void) putc('-',zdd->out);
1035 else if (v == 4)
1036 (void) putc('1',zdd->out);
1037 else if (v == 1)
1038 (void) putc('0',zdd->out);
1039 else
1040 (void) putc('@',zdd->out); /* should never happen */
1041 }
1042 (void) fprintf(zdd->out," 1\n");
1043 }
1044 } else {
1045 /* Check for missing variable. */
1046 if (level != cuddIZ(zdd,node->index)) {
1047 list[zdd->invpermZ[level]] = 0;
1048 zddPrintCoverAux(zdd, node, level + 1, list);
1049 return;
1050 }
1051
1052 Nnv = cuddE(node);
1053 Nv = cuddT(node);
1054 if (Nv == Nnv) {
1055 list[node->index] = 2;
1056 zddPrintCoverAux(zdd, Nnv, level + 1, list);
1057 return;
1058 }
1059
1060 list[node->index] = 1;
1061 zddPrintCoverAux(zdd, Nv, level + 1, list);
1062 list[node->index] = 0;
1063 zddPrintCoverAux(zdd, Nnv, level + 1, list);
1064 }
1065 return;
1066
1067 } /* end of zddPrintCoverAux */
1068
1069
1070 ABC_NAMESPACE_IMPL_END
1071
1072