diff options
Diffstat (limited to 'src/bdd/cudd/cuddExport.c')
| -rw-r--r-- | src/bdd/cudd/cuddExport.c | 1289 |
1 files changed, 0 insertions, 1289 deletions
diff --git a/src/bdd/cudd/cuddExport.c b/src/bdd/cudd/cuddExport.c deleted file mode 100644 index d148be42..00000000 --- a/src/bdd/cudd/cuddExport.c +++ /dev/null @@ -1,1289 +0,0 @@ -/**CFile*********************************************************************** - - FileName [cuddExport.c] - - PackageName [cudd] - - Synopsis [Export functions.] - - Description [External procedures included in this module: - <ul> - <li> Cudd_DumpBlif() - <li> Cudd_DumpBlifBody() - <li> Cudd_DumpDot() - <li> Cudd_DumpDaVinci() - <li> Cudd_DumpDDcal() - <li> Cudd_DumpFactoredForm() - </ul> - Internal procedures included in this module: - <ul> - </ul> - Static procedures included in this module: - <ul> - <li> ddDoDumpBlif() - <li> ddDoDumpDaVinci() - <li> ddDoDumpDDcal() - <li> ddDoDumpFactoredForm() - </ul>] - - Author [Fabio Somenzi] - - Copyright [This file was created at the University of Colorado at - Boulder. The University of Colorado at Boulder makes no warranty - about the suitability of this software for any purpose. It is - presented on an AS IS basis.] - -******************************************************************************/ - -#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 */ -/*---------------------------------------------------------------------------*/ - -/**AutomaticStart*************************************************************/ - -/*---------------------------------------------------------------------------*/ -/* 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)); - -/**AutomaticEnd***************************************************************/ - - -/*---------------------------------------------------------------------------*/ -/* Definition of exported functions */ -/*---------------------------------------------------------------------------*/ - - -/**Function******************************************************************** - - Synopsis [Writes a blif file representing the argument BDDs.] - - Description [Writes a blif file representing the argument BDDs as a - network of multiplexers. One multiplexer is written for each BDD - node. It returns 1 in case of success; 0 otherwise (e.g., - out-of-memory, file system full, or an ADD with constants different - from 0 and 1). Cudd_DumpBlif does not close the file: This is the - caller responsibility. Cudd_DumpBlif 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.] - - SideEffects [None] - - SeeAlso [Cudd_DumpBlifBody Cudd_DumpDot Cudd_PrintDebug Cudd_DumpDDcal - Cudd_DumpDaVinci Cudd_DumpFactoredForm] - -******************************************************************************/ -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 */ - - -/**Function******************************************************************** - - Synopsis [Writes a blif body representing the argument BDDs.] - - Description [Writes a blif body representing the argument BDDs as a - network of multiplexers. One multiplexer is written for each BDD - node. It returns 1 in case of success; 0 otherwise (e.g., - out-of-memory, file system full, or an ADD with constants different - from 0 and 1). Cudd_DumpBlif does not close the file: This is the - caller responsibility. Cudd_DumpBlif 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. This function prints out only - .names part.] - - SideEffects [None] - - SeeAlso [Cudd_DumpDot Cudd_PrintDebug Cudd_DumpDDcal - Cudd_DumpDaVinci Cudd_DumpFactoredForm] - -******************************************************************************/ -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 */ - - -/**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: - <ul> - <li> solid line: THEN arcs; - <li> dotted line: complement arcs; - <li> dashed line: regular ELSE arcs. - </ul> - 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_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 */ - - -/**Function******************************************************************** - - Synopsis [Writes a daVinci file representing the argument BDDs.] - - Description [Writes a daVinci file representing the argument BDDs. - It returns 1 in case of success; 0 otherwise (e.g., out-of-memory or - file system full). Cudd_DumpDaVinci does not close the file: This - is the caller responsibility. Cudd_DumpDaVinci 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.] - - SideEffects [None] - - SeeAlso [Cudd_DumpDot Cudd_PrintDebug Cudd_DumpBlif Cudd_DumpDDcal - Cudd_DumpFactoredForm] - -******************************************************************************/ -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 */ - - -/**Function******************************************************************** - - Synopsis [Writes a DDcal file representing the argument BDDs.] - - Description [Writes a DDcal file representing the argument BDDs. - It returns 1 in case of success; 0 otherwise (e.g., out-of-memory or - file system full). Cudd_DumpDDcal does not close the file: This - is the caller responsibility. Cudd_DumpDDcal 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.] - - SideEffects [None] - - SeeAlso [Cudd_DumpDot Cudd_PrintDebug Cudd_DumpBlif Cudd_DumpDaVinci - Cudd_DumpFactoredForm] - -******************************************************************************/ -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 */ - - -/**Function******************************************************************** - - Synopsis [Writes factored forms representing the argument BDDs.] - - Description [Writes factored forms representing the argument BDDs. - The format of the factored form is the one used in the genlib files - for technology mapping in sis. It returns 1 in case of success; 0 - otherwise (e.g., file system full). Cudd_DumpFactoredForm does not - close the file: This is the caller responsibility. Caution must be - exercised because a factored form may be exponentially larger than - the argument BDD. If the argument inames is non-null, it is assumed - to hold the pointers to the names of the inputs. Similarly for - onames.] - - SideEffects [None] - - SeeAlso [Cudd_DumpDot Cudd_PrintDebug Cudd_DumpBlif Cudd_DumpDaVinci - 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 */ -/*---------------------------------------------------------------------------*/ - - -/**Function******************************************************************** - - Synopsis [Performs the recursive step of Cudd_DumpBlif.] - - Description [Performs the recursive step of Cudd_DumpBlif. Traverses - the BDD f and writes a multiplexer-network description to the file - pointed by fp in blif format. f is assumed to be a regular pointer - and ddDoDumpBlif guarantees this assumption in the recursive calls.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -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 */ - - -/**Function******************************************************************** - - Synopsis [Performs the recursive step of Cudd_DumpDaVinci.] - - Description [Performs the recursive step of Cudd_DumpDaVinci. Traverses - the BDD f and writes a term expression to the file - pointed by fp in daVinci format. f is assumed to be a regular pointer - and ddDoDumpDaVinci guarantees this assumption in the recursive calls.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -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 */ - - -/**Function******************************************************************** - - Synopsis [Performs the recursive step of Cudd_DumpDDcal.] - - Description [Performs the recursive step of Cudd_DumpDDcal. Traverses - the BDD f and writes a line for each node to the file - pointed by fp in DDcal format. f is assumed to be a regular pointer - and ddDoDumpDDcal guarantees this assumption in the recursive calls.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -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 */ - - -/**Function******************************************************************** - - Synopsis [Performs the recursive step of Cudd_DumpFactoredForm.] - - Description [Performs the recursive step of - Cudd_DumpFactoredForm. Traverses the BDD f and writes a factored - form for each node to the file pointed by fp in terms of the - factored forms of the children. Constants are propagated, and - absorption is applied. f is assumed to be a regular pointer and - ddDoDumpFActoredForm guarantees this assumption in the recursive - calls.] - - SideEffects [None] - - SeeAlso [Cudd_DumpFactoredForm] - -******************************************************************************/ -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 */ - |