src/bdd/cudd/cuddExport.c

Go to the documentation of this file.

#include "util_hack.h"
#include "cuddInt.h"

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Stucture declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

#ifndef lint
static char rcsid[] DD_UNUSED = "$Id: cuddExport.c,v 1.1.1.1 2003/02/24 22:23:52 wjiang Exp $";
#endif

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

static int ddDoDumpBlif ARGS((DdManager *dd, DdNode *f, FILE *fp, st_table *visited, char **names));
static int ddDoDumpDaVinci ARGS((DdManager *dd, DdNode *f, FILE *fp, st_table *visited, char **names, long mask));
static int ddDoDumpDDcal ARGS((DdManager *dd, DdNode *f, FILE *fp, st_table *visited, char **names, long mask));
static int ddDoDumpFactoredForm ARGS((DdManager *dd, DdNode *f, FILE *fp, char **names));

/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/


int
Cudd_DumpBlif(
  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) */,
  char * mname /* model name (or NULL) */,
  FILE * fp /* pointer to the dump file */)
{
    DdNode      *support = NULL;
    DdNode      *scan;
    int         *sorted = NULL;
    int         nvars = dd->size;
    int         retval;
    int         i;

    /* 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 */

    /* Write the header (.model .inputs .outputs). */
    if (mname == NULL) {
        retval = fprintf(fp,".model DD\n.inputs");
    } else {
        retval = fprintf(fp,".model %s\n.inputs",mname);
    }
    if (retval == EOF) return(0);

    /* Write the input list by scanning the support array. */
    for (i = 0; i < nvars; i++) {
        if (sorted[i]) {
            if (inames == NULL) {
                retval = fprintf(fp," %d", i);
            } else {
                retval = fprintf(fp," %s", inames[i]);
            }
            if (retval == EOF) goto failure;
        }
    }
    FREE(sorted);
    sorted = NULL;

    /* Write the .output line. */
    retval = fprintf(fp,"\n.outputs");
    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;
    }
    retval = fprintf(fp,"\n");
    if (retval == EOF) goto failure;

    retval = Cudd_DumpBlifBody(dd, n, f, inames, onames, fp);
    if (retval == 0) goto failure;

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

    return(1);

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

} /* end of Cudd_DumpBlif */


int
Cudd_DumpBlifBody(
  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 */)
{
    st_table    *visited = NULL;
    int         retval;
    int         i;

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

    /* Call the function that really gets the job done. */
    for (i = 0; i < n; i++) {
        retval = ddDoDumpBlif(dd,Cudd_Regular(f[i]),fp,visited,inames);
        if (retval == 0) goto failure;
    }

    /* To account for the possible complement on the root,
    ** we put either a buffer or an inverter at the output of
    ** the multiplexer representing the top node.
    */
    for (i = 0; i < n; i++) {
        if (onames == NULL) {
            retval = fprintf(fp,
#if SIZEOF_VOID_P == 8
                ".names %lx f%d\n", (unsigned long) f[i] / (unsigned long) sizeof(DdNode), i);
#else
                ".names %x f%d\n", (unsigned) f[i] / (unsigned) sizeof(DdNode), i);
#endif
        } else {
            retval = fprintf(fp,
#if SIZEOF_VOID_P == 8
                ".names %lx %s\n", (unsigned long) f[i] / (unsigned long) sizeof(DdNode), onames[i]);
#else
                ".names %x %s\n", (unsigned) f[i] / (unsigned) sizeof(DdNode), onames[i]);
#endif
        }
        if (retval == EOF) goto failure;
        if (Cudd_IsComplement(f[i])) {
            retval = fprintf(fp,"0 1\n");
        } else {
            retval = fprintf(fp,"1 1\n");
        }
        if (retval == EOF) goto failure;
    }

    st_free_table(visited);
    return(1);

failure:
    if (visited != NULL) st_free_table(visited);
    return(0);

} /* end of Cudd_DumpBlifBody */


int
Cudd_DumpDot(
  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, (char **) &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", (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", (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",
                (mask & (long) f[i]) / sizeof(DdNode));
        } else {
            retval = fprintf(fp," -> \"%lx\" [style = solid];\n",
                (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",
                            (mask & (long) scan) / sizeof(DdNode),
                            (mask & (long) cuddT(scan)) / sizeof(DdNode));
                        if (retval == EOF) goto failure;
                        if (Cudd_IsComplement(cuddE(scan))) {
                            retval = fprintf(fp,
                                "\"%lx\" -> \"%lx\" [style = dotted];\n",
                                (mask & (long) scan) / sizeof(DdNode),
                                (mask & (long) cuddE(scan)) / sizeof(DdNode));
                        } else {
                            retval = fprintf(fp,
                                "\"%lx\" -> \"%lx\" [style = dashed];\n",
                                (mask & (long) scan) / sizeof(DdNode),
                                (mask & (long) cuddE(scan)) / sizeof(DdNode));
                        }
                        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",
                    (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);

} /* end of Cudd_DumpDot */


int
Cudd_DumpDaVinci(
  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;
    st_table    *visited = NULL;
    int         retval;
    int         i;
    st_generator *gen;
    long        refAddr, diff, mask;

    /* 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);
    while (st_gen(gen, (char **) &scan, NULL)) {
        diff |= refAddr ^ (long) scan;
    }
    st_free_gen(gen);

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

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

    retval = fprintf(fp, "[");
    if (retval == EOF) goto failure;
    /* Call the function that really gets the job done. */
    for (i = 0; i < n; i++) {
        if (onames == NULL) {
            retval = fprintf(fp,
                             "l(\"f%d\",n(\"root\",[a(\"OBJECT\",\"f%d\")],",
                             i,i);
        } else {
            retval = fprintf(fp,
                             "l(\"%s\",n(\"root\",[a(\"OBJECT\",\"%s\")],",
                             onames[i], onames[i]);
        }
        if (retval == EOF) goto failure;
        retval = fprintf(fp, "[e(\"edge\",[a(\"EDGECOLOR\",\"%s\"),a(\"_DIR\",\"none\")],",
                         Cudd_IsComplement(f[i]) ? "red" : "blue");
        if (retval == EOF) goto failure;
        retval = ddDoDumpDaVinci(dd,Cudd_Regular(f[i]),fp,visited,inames,mask);
        if (retval == 0) goto failure;
        retval = fprintf(fp, ")]))%s", i == n-1 ? "" : ",");
        if (retval == EOF) goto failure;
    }

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

    st_free_table(visited);
    return(1);

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

} /* end of Cudd_DumpDaVinci */


int
Cudd_DumpDDcal(
  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;
    int         retval;
    int         i;
    st_generator *gen;
    long        refAddr, diff, mask;

    /* 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);
    while (st_gen(gen, (char **) &scan, NULL)) {
        diff |= refAddr ^ (long) scan;
    }
    st_free_gen(gen);

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

    /* 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 */
    for (i = 0; i < nvars; i++) {
        if (sorted[dd->invperm[i]]) {
            if (inames == NULL || inames[dd->invperm[i]] == NULL) {
                retval = fprintf(fp,"v%d", dd->invperm[i]);
            } else {
                retval = fprintf(fp,"%s", inames[dd->invperm[i]]);
            }
            if (retval == EOF) goto failure;
        }
        retval = fprintf(fp,"%s", i == nvars - 1 ? "\n" : " * ");
        if (retval == EOF) goto failure;
    }
    FREE(sorted);
    sorted = NULL;

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

    /* Call the function that really gets the job done. */
    for (i = 0; i < n; i++) {
        retval = ddDoDumpDDcal(dd,Cudd_Regular(f[i]),fp,visited,inames,mask);
        if (retval == 0) goto failure;
        if (onames == NULL) {
            retval = fprintf(fp, "f%d = ", i);
        } else {
            retval = fprintf(fp, "%s = ", onames[i]);
        }
        if (retval == EOF) goto failure;
        retval = fprintf(fp, "n%lx%s\n",
                         ((long) f[i] & mask) / sizeof(DdNode),
                         Cudd_IsComplement(f[i]) ? "'" : "");
        if (retval == EOF) goto failure;
    }

    /* Write trailer and return. */
    retval = fprintf(fp, "[");
    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]);
        }
        retval = fprintf(fp, "%s", i == n-1 ? "" : " ");
        if (retval == EOF) goto failure;
    }
    retval = fprintf(fp, "]\n");
    if (retval == EOF) goto failure;

    st_free_table(visited);
    return(1);

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

} /* end of Cudd_DumpDDcal */


int
Cudd_DumpFactoredForm(
  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 */)
{
    int         retval;
    int         i;

    /* Call the function that really gets the job done. */
    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) return(0);
        if (f[i] == DD_ONE(dd)) {
            retval = fprintf(fp, "CONST1");
            if (retval == EOF) return(0);
        } else if (f[i] == Cudd_Not(DD_ONE(dd)) || f[i] == DD_ZERO(dd)) {
            retval = fprintf(fp, "CONST0");
            if (retval == EOF) return(0);
        } else {
            retval = fprintf(fp, "%s", Cudd_IsComplement(f[i]) ? "!(" : "");
            if (retval == EOF) return(0);
            retval = ddDoDumpFactoredForm(dd,Cudd_Regular(f[i]),fp,inames);
            if (retval == 0) return(0);
            retval = fprintf(fp, "%s", Cudd_IsComplement(f[i]) ? ")" : "");
            if (retval == EOF) return(0);
        }
        retval = fprintf(fp, "%s", i == n-1 ? "" : "\n");
        if (retval == EOF) return(0);
    }

    return(1);

} /* end of Cudd_DumpFactoredForm */


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/


static int
ddDoDumpBlif(
  DdManager * dd,
  DdNode * f,
  FILE * fp,
  st_table * visited,
  char ** names)
{
    DdNode      *T, *E;
    int         retval;

#ifdef DD_DEBUG
    assert(!Cudd_IsComplement(f));
#endif

    /* If already visited, nothing to do. */
    if (st_is_member(visited, (char *) f) == 1)
        return(1);

    /* Check for abnormal condition that should never happen. */
    if (f == NULL)
        return(0);

    /* Mark node as visited. */
    if (st_insert(visited, (char *) f, NULL) == ST_OUT_OF_MEM)
        return(0);

    /* Check for special case: If constant node, generate constant 1. */
    if (f == DD_ONE(dd)) {
#if SIZEOF_VOID_P == 8
        retval = fprintf(fp, ".names %lx\n1\n",(unsigned long) f / (unsigned long) sizeof(DdNode));
#else
        retval = fprintf(fp, ".names %x\n1\n",(unsigned) f / (unsigned) sizeof(DdNode));
#endif
        if (retval == EOF) {
            return(0);
        } else {
            return(1);
        }
    }

    /* Check whether this is an ADD. We deal with 0-1 ADDs, but not
    ** with the general case.
    */
    if (f == DD_ZERO(dd)) {
#if SIZEOF_VOID_P == 8
        retval = fprintf(fp, ".names %lx\n",(unsigned long) f / (unsigned long) sizeof(DdNode));
#else
        retval = fprintf(fp, ".names %x\n",(unsigned) f / (unsigned) sizeof(DdNode));
#endif
        if (retval == EOF) {
            return(0);
        } else {
            return(1);
        }
    }
    if (cuddIsConstant(f))
        return(0);

    /* Recursive calls. */
    T = cuddT(f);
    retval = ddDoDumpBlif(dd,T,fp,visited,names);
    if (retval != 1) return(retval);
    E = Cudd_Regular(cuddE(f));
    retval = ddDoDumpBlif(dd,E,fp,visited,names);
    if (retval != 1) return(retval);

    /* Write multiplexer taking complement arc into account. */
    if (names != NULL) {
        retval = fprintf(fp,".names %s", names[f->index]);
    } else {
        retval = fprintf(fp,".names %d", f->index);
    }
    if (retval == EOF)
        return(0);

#if SIZEOF_VOID_P == 8
    if (Cudd_IsComplement(cuddE(f))) {
        retval = fprintf(fp," %lx %lx %lx\n11- 1\n0-0 1\n",
            (unsigned long) T / (unsigned long) sizeof(DdNode),
            (unsigned long) E / (unsigned long) sizeof(DdNode),
            (unsigned long) f / (unsigned long) sizeof(DdNode));
    } else {
        retval = fprintf(fp," %lx %lx %lx\n11- 1\n0-1 1\n",
            (unsigned long) T / (unsigned long) sizeof(DdNode),
            (unsigned long) E / (unsigned long) sizeof(DdNode),
            (unsigned long) f / (unsigned long) sizeof(DdNode));
    }
#else
    if (Cudd_IsComplement(cuddE(f))) {
        retval = fprintf(fp," %x %x %x\n11- 1\n0-0 1\n",
            (unsigned) T / (unsigned) sizeof(DdNode),
            (unsigned) E / (unsigned) sizeof(DdNode),
            (unsigned) f / (unsigned) sizeof(DdNode));
    } else {
        retval = fprintf(fp," %x %x %x\n11- 1\n0-1 1\n",
            (unsigned) T / (unsigned) sizeof(DdNode),
            (unsigned) E / (unsigned) sizeof(DdNode),
            (unsigned) f / (unsigned) sizeof(DdNode));
    }
#endif
    if (retval == EOF) {
        return(0);
    } else {
        return(1);
    }

} /* end of ddDoDumpBlif */


static int
ddDoDumpDaVinci(
  DdManager * dd,
  DdNode * f,
  FILE * fp,
  st_table * visited,
  char ** names,
  long  mask)
{
    DdNode      *T, *E;
    int         retval;
    long        id;

#ifdef DD_DEBUG
    assert(!Cudd_IsComplement(f));
#endif

    id = ((long) f & mask) / sizeof(DdNode);

    /* If already visited, insert a reference. */
    if (st_is_member(visited, (char *) f) == 1) {
        retval = fprintf(fp,"r(\"%lx\")", id);
        if (retval == EOF) {
            return(0);
        } else {
            return(1);
        }
    }

    /* Check for abnormal condition that should never happen. */
    if (f == NULL)
        return(0);

    /* Mark node as visited. */
    if (st_insert(visited, (char *) f, NULL) == ST_OUT_OF_MEM)
        return(0);

    /* Check for special case: If constant node, generate constant 1. */
    if (Cudd_IsConstant(f)) {
        retval = fprintf(fp, "l(\"%lx\",n(\"constant\",[a(\"OBJECT\",\"%g\")],[]))", id, cuddV(f));
        if (retval == EOF) {
            return(0);
        } else {
            return(1);
        }
    }

    /* Recursive calls. */
    if (names != NULL) {
        retval = fprintf(fp,
                         "l(\"%lx\",n(\"internal\",[a(\"OBJECT\",\"%s\"),",
                         id, names[f->index]);
    } else {
        retval = fprintf(fp,
                         "l(\"%lx\",n(\"internal\",[a(\"OBJECT\",\"%d\"),",
                         id, f->index);
    }
    retval = fprintf(fp, "a(\"_GO\",\"ellipse\")],[e(\"then\",[a(\"EDGECOLOR\",\"blue\"),a(\"_DIR\",\"none\")],");
    if (retval == EOF) return(0);
    T = cuddT(f);
    retval = ddDoDumpDaVinci(dd,T,fp,visited,names,mask);
    if (retval != 1) return(retval);
    retval = fprintf(fp, "),e(\"else\",[a(\"EDGECOLOR\",\"%s\"),a(\"_DIR\",\"none\")],",
                     Cudd_IsComplement(cuddE(f)) ? "red" : "green");
    if (retval == EOF) return(0);
    E = Cudd_Regular(cuddE(f));
    retval = ddDoDumpDaVinci(dd,E,fp,visited,names,mask);
    if (retval != 1) return(retval);

    retval = fprintf(fp,")]))");
    if (retval == EOF) {
        return(0);
    } else {
        return(1);
    }

} /* end of ddDoDumpDaVinci */


static int
ddDoDumpDDcal(
  DdManager * dd,
  DdNode * f,
  FILE * fp,
  st_table * visited,
  char ** names,
  long  mask)
{
    DdNode      *T, *E;
    int         retval;
    long        id, idT, idE;

#ifdef DD_DEBUG
    assert(!Cudd_IsComplement(f));
#endif

    id = ((long) f & mask) / sizeof(DdNode);

    /* If already visited, do nothing. */
    if (st_is_member(visited, (char *) f) == 1) {
        return(1);
    }

    /* Check for abnormal condition that should never happen. */
    if (f == NULL)
        return(0);

    /* Mark node as visited. */
    if (st_insert(visited, (char *) f, NULL) == ST_OUT_OF_MEM)
        return(0);

    /* Check for special case: If constant node, assign constant. */
    if (Cudd_IsConstant(f)) {
        if (f != DD_ONE(dd) && f != DD_ZERO(dd))
            return(0);
        retval = fprintf(fp, "n%lx = %g\n", id, cuddV(f));
        if (retval == EOF) {
            return(0);
        } else {
            return(1);
        }
    }

    /* Recursive calls. */
    T = cuddT(f);
    retval = ddDoDumpDDcal(dd,T,fp,visited,names,mask);
    if (retval != 1) return(retval);
    E = Cudd_Regular(cuddE(f));
    retval = ddDoDumpDDcal(dd,E,fp,visited,names,mask);
    if (retval != 1) return(retval);
    idT = ((long) T & mask) / sizeof(DdNode);
    idE = ((long) E & mask) / sizeof(DdNode);
    if (names != NULL) {
        retval = fprintf(fp, "n%lx = %s * n%lx + %s' * n%lx%s\n",
                         id, names[f->index], idT, names[f->index],
                         idE, Cudd_IsComplement(cuddE(f)) ? "'" : "");
    } else {
        retval = fprintf(fp, "n%lx = v%d * n%lx + v%d' * n%lx%s\n",
                         id, f->index, idT, f->index,
                         idE, Cudd_IsComplement(cuddE(f)) ? "'" : "");
    }
    if (retval == EOF) {
        return(0);
    } else {
        return(1);
    }

} /* end of ddDoDumpDDcal */


static int
ddDoDumpFactoredForm(
  DdManager * dd,
  DdNode * f,
  FILE * fp,
  char ** names)
{
    DdNode      *T, *E;
    int         retval;

#ifdef DD_DEBUG
    assert(!Cudd_IsComplement(f));
    assert(!Cudd_IsConstant(f));
#endif

    /* Check for abnormal condition that should never happen. */
    if (f == NULL)
        return(0);

    /* Recursive calls. */
    T = cuddT(f);
    E = cuddE(f);
    if (T != DD_ZERO(dd)) {
        if (E != DD_ONE(dd)) {
            if (names != NULL) {
                retval = fprintf(fp, "%s", names[f->index]);
            } else {
                retval = fprintf(fp, "x%d", f->index);
            }
            if (retval == EOF) return(0);
        }
        if (T != DD_ONE(dd)) {
            retval = fprintf(fp, "%s(", E != DD_ONE(dd) ? " * " : "");
            if (retval == EOF) return(0);
            retval = ddDoDumpFactoredForm(dd,T,fp,names);
            if (retval != 1) return(retval);
            retval = fprintf(fp, ")");
            if (retval == EOF) return(0);
        }
        if (E == Cudd_Not(DD_ONE(dd)) || E == DD_ZERO(dd)) return(1);
        retval = fprintf(fp, " + ");
        if (retval == EOF) return(0);
    }
    E = Cudd_Regular(E);
    if (T != DD_ONE(dd)) {
        if (names != NULL) {
            retval = fprintf(fp, "!%s", names[f->index]);
        } else {
            retval = fprintf(fp, "!x%d", f->index);
        }
        if (retval == EOF) return(0);
    }
    if (E != DD_ONE(dd)) {
        retval = fprintf(fp, "%s%s(", T != DD_ONE(dd) ? " * " : "",
                         E != cuddE(f) ? "!" : "");
        if (retval == EOF) return(0);
        retval = ddDoDumpFactoredForm(dd,E,fp,names);
        if (retval != 1) return(retval);
        retval = fprintf(fp, ")");
        if (retval == EOF) return(0);
    }
    return(1);

} /* end of ddDoDumpFactoredForm */

---