abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
cuddExport.c
Go to the documentation of this file.
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
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
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
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
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
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
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
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
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
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
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 
ddDoDumpDaVinci
static int ddDoDumpDaVinci(DdManager *dd, DdNode *f, FILE *fp, st__table *visited, char **names, ptruint mask)
Definition: cuddExport.c:1117
ddDoDumpFactoredForm
static int ddDoDumpFactoredForm(DdManager *dd, DdNode *f, FILE *fp, char **names)
Definition: cuddExport.c:1310
st__free_table
void st__free_table(st__table *table)
Definition: st.c:81
cuddRef
#define cuddRef(n)
Definition: cuddInt.h:584
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdNode
Definition: cudd.h:278
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
st__free_gen
void st__free_gen(st__generator *gen)
Definition: st.c:556
st__insert
int st__insert(st__table *table, const char *key, char *value)
Definition: st.c:171
DdManager::size
int size
Definition: cuddInt.h:361
Cudd_DumpDot
int Cudd_DumpDot(DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp)
Definition: cuddExport.c:344
Cudd_IsConstant
#define Cudd_IsConstant(node)
Definition: cudd.h:352
Cudd_Regular
#define Cudd_Regular(node)
Definition: cudd.h:397
Cudd_DumpBlifBody
int Cudd_DumpBlifBody(DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp, int mv)
Definition: cuddExport.c:252
st__ptrcmp
int st__ptrcmp(const char *, const char *)
Definition: st.c:480
Cudd_DumpBlif
int Cudd_DumpBlif(DdManager *dd, int n, DdNode **f, char **inames, char **onames, char *mname, FILE *fp, int mv)
Definition: cuddExport.c:136
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
DdManager::subtables
DdSubtable * subtables
Definition: cuddInt.h:365
st__is_member
#define st__is_member(table, key)
Definition: st.h:70
ddDoDumpBlif
static int ddDoDumpBlif(DdManager *dd, DdNode *f, FILE *fp, st__table *visited, char **names, int mv)
Definition: cuddExport.c:956
DdNode
struct DdNode DdNode
Definition: cudd.h:270
util_hack.h
cuddV
#define cuddV(node)
Definition: cuddInt.h:668
ptruint
ABC_PTRUINT_T ptruint
Definition: cuddInt.h:261
onames
static const char * onames[]
Definition: testcudd.c:71
st__init_table
st__table * st__init_table(st__compare_func_type compare, st__hash_func_type hash)
Definition: st.c:72
Cudd_IsComplement
#define Cudd_IsComplement(node)
Definition: cudd.h:425
SIZEOF_VOID_P
#define SIZEOF_VOID_P
Definition: cudd.h:78
ptrint
ABC_PTRINT_T ptrint
Definition: cuddInt.h:260
st__table
Definition: st.h:52
DdNode::next
DdNode * next
Definition: cudd.h:281
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
cuddIsConstant
#define cuddIsConstant(node)
Definition: cuddInt.h:620
DdSubtable::nodelist
DdNode ** nodelist
Definition: cuddInt.h:327
Cudd_DumpDaVinci
int Cudd_DumpDaVinci(DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp)
Definition: cuddExport.c:615
cuddT
#define cuddT(node)
Definition: cuddInt.h:636
st__init_gen
st__generator * st__init_gen(st__table *table)
Definition: st.c:486
st__OUT_OF_MEM
#define st__OUT_OF_MEM
Definition: st.h:113
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Cudd_DumpDDcal
int Cudd_DumpDDcal(DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp)
Definition: cuddExport.c:729
ddDoDumpDDcal
static int ddDoDumpDDcal(DdManager *dd, DdNode *f, FILE *fp, st__table *visited, char **names, ptruint mask)
Definition: cuddExport.c:1216
DdNode::index
DdHalfWord index
Definition: cudd.h:279
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
DdSubtable::slots
unsigned int slots
Definition: cuddInt.h:329
cuddE
#define cuddE(node)
Definition: cuddInt.h:652
cuddCollectNodes
int cuddCollectNodes(DdNode *f, st__table *visited)
Definition: cuddUtil.c:2925
assert
#define assert(ex)
Definition: util_old.h:213
Cudd_DumpFactoredForm
int Cudd_DumpFactoredForm(DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp)
Definition: cuddExport.c:889
DdManager::invperm
int * invperm
Definition: cuddInt.h:388
DdManager::constants
DdSubtable constants
Definition: cuddInt.h:367
DD_ONE
#define DD_ONE(dd)
Definition: cuddInt.h:911
DdManager::errorCode
Cudd_ErrorType errorCode
Definition: cuddInt.h:447
st__ptrhash
int st__ptrhash(const char *, int)
Definition: st.c:468
st__gen
int st__gen(st__generator *gen, const char **key_p, char **value_p)
Definition: st.c:502
st__generator
Definition: st.h:64
Cudd_VectorSupport
DdNode * Cudd_VectorSupport(DdManager *dd, DdNode **F, int n)
Definition: cuddUtil.c:908
DD_UNUSED
static ABC_NAMESPACE_IMPL_START char rcsid[] DD_UNUSED
Definition: cuddExport.c:89
DD_ZERO
#define DD_ZERO(dd)
Definition: cuddInt.h:927