cuddexport.c is missing a good Dot File Tree Dump...

[tezozomoc]

There is no good dot tree dump for cudd... I wrote this one several years ago...

Please include the following function to cuddexport.c

in the cudd.h file include the following.. .
function declaration...
extern int Cudd_DumpDotTree (DdManager *dd, int n, DdNode **f, char **inames, char **onames, FILE *fp);

in the file cuddexport.c add the following function...

/Function******************************************************************

Synopsis [Writes a dot file representing the argument DDs.]

Description [Writes a file representing the argument DDs in a format
suitable for the graph drawing program dot.
It returns 1 in case of success; 0 otherwise (e.g., out-of-memory,
file system full).
Cudd_DumpDot does not close the file: This is the caller
responsibility. Cudd_DumpDot uses a minimal unique subset of the
hexadecimal address of a node as name for it.
If the argument inames is non-null, it is assumed to hold the pointers
to the names of the inputs. Similarly for onames.
Cudd_DumpDot uses the following convention to draw arcs:

• solid line: THEN arcs;
  
• dotted line: complement arcs;
  
• dashed line: regular ELSE arcs.
  

The dot options are chosen so that the drawing fits on a letter-size
sheet.
]

SideEffects [None]

SeeAlso [Cudd_DumpBlif Cudd_PrintDebug Cudd_DumpDDcal
Cudd_DumpDaVinci Cudd_DumpFactoredForm]

*****************************************************************************/
int
Cudd_DumpDotTree(
DdManager * dd / manager /,
int n / number of output nodes to be dumped /,
DdNode ** f / array of output nodes to be dumped /,
char ** inames / array of input names (or NULL) /,
char ** onames / array of output names (or NULL) /,
FILE * fp / pointer to the dump file */)
{
DdNode *support = NULL;
DdNode *scan;
int *sorted = NULL;
int nvars = dd->size;
st_table *visited = NULL;
st_generator *gen = NULL;
int retval;
int i, j;
int slots;
DdNodePtr *nodelist;
long refAddr, diff, mask;

/* Build a bit array with the support of f. */
sorted = ALLOC(int,nvars);
if (sorted == NULL) {
dd->errorCode = CUDD_MEMORY_OUT;
goto failure;
}
for (i = 0; i < nvars; i++) sorted[i] = 0;

/* Take the union of the supports of each output function. */
support = Cudd_VectorSupport(dd,f,n);
if (support == NULL) goto failure;
cuddRef(support);
scan = support;
while (!cuddIsConstant(scan)) {
sorted[scan->index] = 1;
scan = cuddT(scan);
}
Cudd_RecursiveDeref(dd,support);
support = NULL; /* so that we do not try to free it in case of failure */

/* Initialize symbol table for visited nodes. */
visited = st_init_table(st_ptrcmp, st_ptrhash);
if (visited == NULL) goto failure;

/* Collect all the nodes of this DD in the symbol table. */
for (i = 0; i < n; i++) {
retval = cuddCollectNodes(Cudd_Regular(f[i]),visited);
if (retval == 0) goto failure;
}

/* Find how many most significant hex digits are identical
** in the addresses of all the nodes. Build a mask based
** on this knowledge, so that digits that carry no information
** will not be printed. This is done in two steps.
**  1. We scan the symbol table to find the bits that differ
**     in at least 2 addresses.
**  2. We choose one of the possible masks. There are 8 possible
**     masks for 32-bit integer, and 16 possible masks for 64-bit
**     integers.
*/

/* Find the bits that are different. */
refAddr = (long) Cudd_Regular(f[0]);
diff = 0;
gen = st_init_gen(visited);
if (gen == NULL) goto failure;
while (st_gen(gen, &scan, NULL)) {
diff |= refAddr ^ (long) scan;
}
st_free_gen(gen); gen = NULL;

/* Choose the mask. */
for (i = 0; (unsigned) i < 8 * sizeof(long); i += 4) {
mask = (1 << i) - 1;
if (diff <= mask) break;
}

/* Write the header and the global attributes. */
retval = fprintf(fp,"digraph \"DD\" {\n");
if (retval == EOF) return(0);
retval = fprintf(fp,
"size = \"7.5,10\"\ncenter = true;\nedge [dir = none];\n");
if (retval == EOF) return(0);

/* Write the input name subgraph by scanning the support array. */
retval = fprintf(fp,"{ node [shape = plaintext];\n");
if (retval == EOF) goto failure;
retval = fprintf(fp,"  edge [style = invis];\n");
if (retval == EOF) goto failure;
/* We use a name ("CONST NODES") with an embedded blank, because
** it is unlikely to appear as an input name.
*/
retval = fprintf(fp,"  \"CONST NODES\" [style = invis];\n");
if (retval == EOF) goto failure;
for (i = 0; i < nvars; i++) {
    if (sorted[dd->invperm[i]]) {
    if (inames == NULL || inames[dd->invperm[i]] == NULL) {
	retval = fprintf(fp,"\" %d \" -> ", dd->invperm[i]);
    } else {
	retval = fprintf(fp,"\" %s \" -> ", inames[dd->invperm[i]]);
    }
        if (retval == EOF) goto failure;
    }
}
retval = fprintf(fp,"\"CONST NODES\"; \n}\n");
if (retval == EOF) goto failure;

/* Write the output node subgraph. */
retval = fprintf(fp,"{ rank = same; node [shape = box]; edge [style = invis];\n");
if (retval == EOF) goto failure;
for (i = 0; i < n; i++) {
if (onames == NULL) {
    retval = fprintf(fp,"\"F%d\"", i);
} else {
    retval = fprintf(fp,"\"  %s  \"", onames[i]);
}
if (retval == EOF) goto failure;
if (i == n - 1) {
    retval = fprintf(fp,"; }\n");
} else {
    retval = fprintf(fp," -> ");
}
if (retval == EOF) goto failure;
}

/* Write rank info: All nodes with the same index have the same rank. */
for (i = 0; i < nvars; i++) {
    if (sorted[dd->invperm[i]]) {
    retval = fprintf(fp,"{ rank = same; ");
    if (retval == EOF) goto failure;
    if (inames == NULL || inames[dd->invperm[i]] == NULL) {
	retval = fprintf(fp,"\" %d \";\n", dd->invperm[i]);
    } else {
	retval = fprintf(fp,"\" %s \";\n", inames[dd->invperm[i]]);
    }
        if (retval == EOF) goto failure;
    nodelist = dd->subtables[i].nodelist;
    slots = dd->subtables[i].slots;
    for (j = 0; j < slots; j++) {
	scan = nodelist[j];
	while (scan != NULL) {
	    if (st_is_member(visited,(char *) scan)) {
		retval = fprintf(fp,"\"%lx\";\n",
		    (unsigned long) ((mask & (long) scan) /
		    sizeof(DdNode)));
		if (retval == EOF) goto failure;
	    }
	    scan = scan->next;
	}
    }
    retval = fprintf(fp,"}\n");
    if (retval == EOF) goto failure;
}
}

/* All constants have the same rank. */
retval = fprintf(fp,
"{ rank = same; \"CONST NODES\";\n{ node [shape = box]; ");
if (retval == EOF) goto failure;
nodelist = dd->constants.nodelist;
slots = dd->constants.slots;
for (j = 0; j < slots; j++) {
scan = nodelist[j];
while (scan != NULL) {
    if (st_is_member(visited,(char *) scan)) {
	retval = fprintf(fp,"\"%lx\";\n",
	    (unsigned long) ((mask & (long) scan) / sizeof(DdNode)));
	if (retval == EOF) goto failure;
    }
    scan = scan->next;
}
}
retval = fprintf(fp,"}\n}\n");
if (retval == EOF) goto failure;

/* Write edge info. */
/* Edges from the output nodes. */
for (i = 0; i < n; i++) {
if (onames == NULL) {
    retval = fprintf(fp,"\"F%d\"", i);
} else {
    retval = fprintf(fp,"\"  %s  \"", onames[i]);
}
if (retval == EOF) goto failure;
/* Account for the possible complement on the root. */
if (Cudd_IsComplement(f[i])) {
    retval = fprintf(fp," -> \"%lx\" [style = dotted];\n",
	(unsigned long) ((mask & (long) f[i]) / sizeof(DdNode)));
} else {
    retval = fprintf(fp," -> \"%lx\" [style = solid];\n",
	(unsigned long) ((mask & (long) f[i]) / sizeof(DdNode)));
}
if (retval == EOF) goto failure;
}

/* Edges from internal nodes. */
for (i = 0; i < nvars; i++) {
    if (sorted[dd->invperm[i]]) {
    nodelist = dd->subtables[i].nodelist;
    slots = dd->subtables[i].slots;
    for (j = 0; j < slots; j++) {
	scan = nodelist[j];
	while (scan != NULL) {
	    if (st_is_member(visited,(char *) scan)) {
		retval = fprintf(fp,
		    "\"%lx\" -> \"%lx\";\n",
		    (unsigned long) ((mask & (long) scan) /
		    sizeof(DdNode)),
		    (unsigned long) ((mask & (long) cuddT(scan)) /
		    sizeof(DdNode)));
		if (retval == EOF) goto failure;

                    unsigned long parent = 0U;
		if (Cudd_IsComplement(cuddE(scan)))
                    {
		    retval = fprintf(fp,
			"\"%lx\" -> \"FAIL\" [style = dotted];\n",
			(unsigned long) ((mask & (long) scan) /
			sizeof(DdNode)),
			(unsigned long) ((mask & (long) cuddE(scan)) /
			sizeof(DdNode)));
                    }
                    else
                    {
		    retval = fprintf(fp,
			"\"%lx\" -> \"%lx\" [style = dashed];\n",
			(unsigned long) ((mask & (long) scan) /
			sizeof(DdNode)),
			(unsigned long) ((mask & (long) cuddE(scan)) /
			sizeof(DdNode)));
                    }
                    #ifdef ORIG
		if (Cudd_IsComplement(cuddE(scan))) {
		    retval = fprintf(fp,
			"\"%lx\" -> \"%lx\" [style = dotted];\n",
			(unsigned long) ((mask & (long) scan) /
			sizeof(DdNode)),
			(unsigned long) ((mask & (long) cuddE(scan)) /
			sizeof(DdNode)));
		} else {
		    retval = fprintf(fp,
			"\"%lx\" -> \"%lx\" [style = dashed];\n",
			(unsigned long) ((mask & (long) scan) /
			sizeof(DdNode)),
			(unsigned long) ((mask & (long) cuddE(scan)) /
			sizeof(DdNode)));
		}
                    #endif
		if (retval == EOF) goto failure;
	    }
	    scan = scan->next;
	}
    }
}
}

/* Write constant labels. */
nodelist = dd->constants.nodelist;
slots = dd->constants.slots;
for (j = 0; j < slots; j++) {
scan = nodelist[j];
while (scan != NULL) {
    if (st_is_member(visited,(char *) scan)) {
	retval = fprintf(fp,"\"%lx\" [label = \"%g\"];\n",
	    (unsigned long) ((mask & (long) scan) / sizeof(DdNode)),
	    cuddV(scan));
	if (retval == EOF) goto failure;
    }
    scan = scan->next;
}
}

/* Write trailer and return. */
retval = fprintf(fp,"}\n");
if (retval == EOF) goto failure;

st_free_table(visited);
FREE(sorted);
return(1);

failure:
if (sorted != NULL) FREE(sorted);
if (support != NULL) Cudd_RecursiveDeref(dd,support);
if (visited != NULL) st_free_table(visited);
return(0);

}

[ivmai]

Hi.
I'm not a maintainer (nor developer) of cudd. Please contact the author.
Anyway you can make a pull request (I won't merge or close it) to let others use your fix.