diff options
Diffstat (limited to 'src/bdd/cudd/cuddExport.c')
| -rw-r--r-- | src/bdd/cudd/cuddExport.c | 873 |
1 files changed, 488 insertions, 385 deletions
diff --git a/src/bdd/cudd/cuddExport.c b/src/bdd/cudd/cuddExport.c index cccf2465..255baabf 100644 --- a/src/bdd/cudd/cuddExport.c +++ b/src/bdd/cudd/cuddExport.c @@ -7,31 +7,58 @@ 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>] + <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.] + Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado + + All rights reserved. + + Redistribution and use in source and binary forms, with or without + modification, are permitted provided that the following conditions + are met: + + Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in the + documentation and/or other materials provided with the distribution. + + Neither the name of the University of Colorado nor the names of its + contributors may be used to endorse or promote products derived from + this software without specific prior written permission. + + THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS + "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT + LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS + FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE + COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, + INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, + BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; + LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT + LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN + ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE + POSSIBILITY OF SUCH DAMAGE.] ******************************************************************************/ @@ -41,6 +68,7 @@ ABC_NAMESPACE_IMPL_START + /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ @@ -58,7 +86,7 @@ ABC_NAMESPACE_IMPL_START /*---------------------------------------------------------------------------*/ #ifndef lint -static char rcsid[] DD_UNUSED = "$Id: cuddExport.c,v 1.1.1.1 2003/02/24 22:23:52 wjiang Exp $"; +static char rcsid[] DD_UNUSED = "$Id: cuddExport.c,v 1.22 2009/03/08 02:49:02 fabio Exp $"; #endif /*---------------------------------------------------------------------------*/ @@ -71,10 +99,10 @@ static char rcsid[] DD_UNUSED = "$Id: cuddExport.c,v 1.1.1.1 2003/02/24 22:23:52 /* 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)); +static int ddDoDumpBlif (DdManager *dd, DdNode *f, FILE *fp, st_table *visited, char **names, int mv); +static int ddDoDumpDaVinci (DdManager *dd, DdNode *f, FILE *fp, st_table *visited, char **names, ptruint mask); +static int ddDoDumpDDcal (DdManager *dd, DdNode *f, FILE *fp, st_table *visited, char **names, ptruint mask); +static int ddDoDumpFactoredForm (DdManager *dd, DdNode *f, FILE *fp, char **names); /**AutomaticEnd***************************************************************/ @@ -112,20 +140,21 @@ Cudd_DumpBlif( 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 */) + FILE * fp /* pointer to the dump file */, + int mv /* 0: blif, 1: blif-MV */) { - DdNode *support = NULL; - DdNode *scan; - int *sorted = NULL; - int nvars = dd->size; - int retval; - int i; + 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 = ABC_ALLOC(int,nvars); if (sorted == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - goto failure; + dd->errorCode = CUDD_MEMORY_OUT; + goto failure; } for (i = 0; i < nvars; i++) sorted[i] = 0; @@ -135,28 +164,31 @@ Cudd_DumpBlif( cuddRef(support); scan = support; while (!cuddIsConstant(scan)) { - sorted[scan->index] = 1; - scan = cuddT(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"); + retval = fprintf(fp,".model DD\n.inputs"); } else { - retval = fprintf(fp,".model %s\n.inputs",mname); + retval = fprintf(fp,".model %s\n.inputs",mname); + } + if (retval == EOF) { + ABC_FREE(sorted); + return(0); } - 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 (inames == NULL) { + retval = fprintf(fp," %d", i); + } else { + retval = fprintf(fp," %s", inames[i]); + } if (retval == EOF) goto failure; } } @@ -167,17 +199,17 @@ Cudd_DumpBlif( 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; + 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); + retval = Cudd_DumpBlifBody(dd, n, f, inames, onames, fp, mv); if (retval == 0) goto failure; /* Write trailer and return. */ @@ -199,11 +231,12 @@ failure: 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., + network of multiplexers. No header (.model, .inputs, and .outputs) and + footer (.end) are produced by this function. 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 + from 0 and 1). Cudd_DumpBlifBody does not close the file: This is the + caller responsibility. Cudd_DumpBlifBody 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 @@ -211,7 +244,7 @@ failure: SideEffects [None] - SeeAlso [Cudd_DumpDot Cudd_PrintDebug Cudd_DumpDDcal + SeeAlso [Cudd_DumpBlif Cudd_DumpDot Cudd_PrintDebug Cudd_DumpDDcal Cudd_DumpDaVinci Cudd_DumpFactoredForm] ******************************************************************************/ @@ -222,11 +255,12 @@ Cudd_DumpBlifBody( 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 */) + FILE * fp /* pointer to the dump file */, + int mv /* 0: blif, 1: blif-MV */) { st_table *visited = NULL; - int retval; - int i; + int retval; + int i; /* Initialize symbol table for visited nodes. */ visited = st_init_table(st_ptrcmp, st_ptrhash); @@ -234,8 +268,8 @@ Cudd_DumpBlifBody( /* 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; + retval = ddDoDumpBlif(dd,Cudd_Regular(f[i]),fp,visited,inames,mv); + if (retval == 0) goto failure; } /* To account for the possible complement on the root, @@ -243,28 +277,28 @@ Cudd_DumpBlifBody( ** the multiplexer representing the top node. */ for (i = 0; i < n; i++) { - if (onames == NULL) { - retval = fprintf(fp, + 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); + ".names %lx f%d\n", (ptruint) f[i] / (ptruint) sizeof(DdNode), i); #else - ".names %x f%d\n", (unsigned) f[i] / (unsigned) sizeof(DdNode), i); + ".names %x f%d\n", (ptruint) f[i] / (ptruint) sizeof(DdNode), i); #endif - } else { - retval = fprintf(fp, + } else { + retval = fprintf(fp, #if SIZEOF_VOID_P == 8 - ".names %lx %s\n", (unsigned long) f[i] / (unsigned long) sizeof(DdNode), onames[i]); + ".names %lx %s\n", (ptruint) f[i] / (ptruint) sizeof(DdNode), onames[i]); #else - ".names %x %s\n", (unsigned) f[i] / (unsigned) sizeof(DdNode), onames[i]); + ".names %x %s\n", (ptruint) f[i] / (ptruint) 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; + } + if (retval == EOF) goto failure; + if (Cudd_IsComplement(f[i])) { + retval = fprintf(fp,"%s0 1\n", mv ? ".def 0\n" : ""); + } else { + retval = fprintf(fp,"%s1 1\n", mv ? ".def 0\n" : ""); + } + if (retval == EOF) goto failure; } st_free_table(visited); @@ -315,23 +349,23 @@ Cudd_DumpDot( 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; + 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; + int retval; + int i, j; + int slots; + DdNodePtr *nodelist; + long refAddr, diff, mask; /* Build a bit array with the support of f. */ sorted = ABC_ALLOC(int,nvars); if (sorted == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - goto failure; + dd->errorCode = CUDD_MEMORY_OUT; + goto failure; } for (i = 0; i < nvars; i++) sorted[i] = 0; @@ -341,8 +375,8 @@ Cudd_DumpDot( cuddRef(support); scan = support; while (!cuddIsConstant(scan)) { - sorted[scan->index] = 1; - scan = cuddT(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 */ @@ -353,8 +387,8 @@ Cudd_DumpDot( /* 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; + retval = cuddCollectNodes(Cudd_Regular(f[i]),visited); + if (retval == 0) goto failure; } /* Find how many most significant hex digits are identical @@ -373,22 +407,22 @@ Cudd_DumpDot( diff = 0; gen = st_init_gen(visited); if (gen == NULL) goto failure; - while (st_gen(gen, (const char **) &scan, NULL)) { - diff |= refAddr ^ (long) scan; + while (st_gen(gen, (const 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; + 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"); + "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. */ @@ -403,11 +437,11 @@ Cudd_DumpDot( 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 (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; } } @@ -418,63 +452,66 @@ Cudd_DumpDot( 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; + 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]]); - } + retval = fprintf(fp,"{ rank = same; "); 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 (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,"\"%p\";\n", + (void *) ((mask & (ptrint) scan) / + sizeof(DdNode))); + if (retval == EOF) goto failure; + } + scan = scan->next; + } } - scan = scan->next; - } + retval = fprintf(fp,"}\n"); + if (retval == EOF) goto failure; } - 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]; "); + "{ 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 = nodelist[j]; + while (scan != NULL) { + if (st_is_member(visited,(char *) scan)) { + retval = fprintf(fp,"\"%p\";\n", + (void *) ((mask & (ptrint) scan) / sizeof(DdNode))); + if (retval == EOF) goto failure; + } + scan = scan->next; } - scan = scan->next; - } } retval = fprintf(fp,"}\n}\n"); if (retval == EOF) goto failure; @@ -482,69 +519,76 @@ Cudd_DumpDot( /* 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; + 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," -> \"%p\" [style = dotted];\n", + (void *) ((mask & (ptrint) f[i]) / sizeof(DdNode))); + } else { + retval = fprintf(fp," -> \"%p\" [style = solid];\n", + (void *) ((mask & (ptrint) 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; + 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, + "\"%p\" -> \"%p\";\n", + (void *) ((mask & (ptrint) scan) / + sizeof(DdNode)), + (void *) ((mask & (ptrint) cuddT(scan)) / + sizeof(DdNode))); + if (retval == EOF) goto failure; + if (Cudd_IsComplement(cuddE(scan))) { + retval = fprintf(fp, + "\"%p\" -> \"%p\" [style = dotted];\n", + (void *) ((mask & (ptrint) scan) / + sizeof(DdNode)), + (void *) ((mask & (ptrint) cuddE(scan)) / + sizeof(DdNode))); + } else { + retval = fprintf(fp, + "\"%p\" -> \"%p\" [style = dashed];\n", + (void *) ((mask & (ptrint) scan) / + sizeof(DdNode)), + (void *) ((mask & (ptrint) cuddE(scan)) / + sizeof(DdNode))); + } + if (retval == EOF) goto failure; + } + scan = scan->next; + } } - 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 = nodelist[j]; + while (scan != NULL) { + if (st_is_member(visited,(char *) scan)) { + retval = fprintf(fp,"\"%p\" [label = \"%g\"];\n", + (void *) ((mask & (ptrint) scan) / sizeof(DdNode)), + cuddV(scan)); + if (retval == EOF) goto failure; + } + scan = scan->next; } - scan = scan->next; - } } /* Write trailer and return. */ @@ -591,13 +635,13 @@ Cudd_DumpDaVinci( 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; + DdNode *support = NULL; + DdNode *scan; + st_table *visited = NULL; + int retval; + int i; + st_generator *gen; + ptruint refAddr, diff, mask; /* Initialize symbol table for visited nodes. */ visited = st_init_table(st_ptrcmp, st_ptrhash); @@ -605,8 +649,8 @@ Cudd_DumpDaVinci( /* 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; + retval = cuddCollectNodes(Cudd_Regular(f[i]),visited); + if (retval == 0) goto failure; } /* Find how many most significant hex digits are identical @@ -621,18 +665,18 @@ Cudd_DumpDaVinci( */ /* Find the bits that are different. */ - refAddr = (long) Cudd_Regular(f[0]); + refAddr = (ptruint) Cudd_Regular(f[0]); diff = 0; gen = st_init_gen(visited); - while (st_gen(gen, (const char **) &scan, NULL)) { - diff |= refAddr ^ (long) scan; + while (st_gen(gen, (const char **)&scan, NULL)) { + diff |= refAddr ^ (ptruint) 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; + for (i = 0; (unsigned) i < 8 * sizeof(ptruint); i += 4) { + mask = (1 << i) - 1; + if (diff <= mask) break; } st_free_table(visited); @@ -644,23 +688,23 @@ Cudd_DumpDaVinci( 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; + 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. */ @@ -705,15 +749,15 @@ Cudd_DumpDDcal( 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; + DdNode *support = NULL; + DdNode *scan; + int *sorted = NULL; + int nvars = dd->size; + st_table *visited = NULL; + int retval; + int i; + st_generator *gen; + ptruint refAddr, diff, mask; /* Initialize symbol table for visited nodes. */ visited = st_init_table(st_ptrcmp, st_ptrhash); @@ -721,8 +765,8 @@ Cudd_DumpDDcal( /* 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; + retval = cuddCollectNodes(Cudd_Regular(f[i]),visited); + if (retval == 0) goto failure; } /* Find how many most significant hex digits are identical @@ -737,26 +781,26 @@ Cudd_DumpDDcal( */ /* Find the bits that are different. */ - refAddr = (long) Cudd_Regular(f[0]); + refAddr = (ptruint) Cudd_Regular(f[0]); diff = 0; gen = st_init_gen(visited); - while (st_gen(gen, (const char **) &scan, NULL)) { - diff |= refAddr ^ (long) scan; + while (st_gen(gen, (const char **)&scan, NULL)) { + diff |= refAddr ^ (ptruint) 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; + for (i = 0; (unsigned) i < 8 * sizeof(ptruint); i += 4) { + mask = (1 << i) - 1; + if (diff <= mask) break; } st_free_table(visited); /* Build a bit array with the support of f. */ sorted = ABC_ALLOC(int,nvars); if (sorted == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - goto failure; + dd->errorCode = CUDD_MEMORY_OUT; + goto failure; } for (i = 0; i < nvars; i++) sorted[i] = 0; @@ -766,22 +810,22 @@ Cudd_DumpDDcal( cuddRef(support); scan = support; while (!cuddIsConstant(scan)) { - sorted[scan->index] = 1; - scan = cuddT(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 (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; + retval = fprintf(fp,"%s", i == nvars - 1 ? "\n" : " * "); + if (retval == EOF) goto failure; } ABC_FREE(sorted); sorted = NULL; @@ -792,31 +836,32 @@ Cudd_DumpDDcal( /* 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; + 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%p%s\n", + (void *) (((ptruint) f[i] & mask) / + (ptruint) 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; + 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; @@ -862,34 +907,34 @@ Cudd_DumpFactoredForm( char ** onames /* array of output names (or NULL) */, FILE * fp /* pointer to the dump file */) { - int retval; - int i; + 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 (onames == NULL) { + retval = fprintf(fp, "f%d = ", i); + } else { + retval = fprintf(fp, "%s = ", onames[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 (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); } - retval = fprintf(fp, "%s", i == n-1 ? "" : "\n"); - if (retval == EOF) return(0); - } return(1); @@ -926,10 +971,11 @@ ddDoDumpBlif( DdNode * f, FILE * fp, st_table * visited, - char ** names) + char ** names, + int mv) { - DdNode *T, *E; - int retval; + DdNode *T, *E; + int retval; #ifdef DD_DEBUG assert(!Cudd_IsComplement(f)); @@ -950,9 +996,9 @@ ddDoDumpBlif( /* 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)); + retval = fprintf(fp, ".names %lx\n1\n",(ptruint) f / (ptruint) sizeof(DdNode)); #else - retval = fprintf(fp, ".names %x\n1\n",(unsigned) f / (unsigned) sizeof(DdNode)); + retval = fprintf(fp, ".names %x\n1\n",(ptruint) f / (ptruint) sizeof(DdNode)); #endif if (retval == EOF) { return(0); @@ -966,9 +1012,13 @@ ddDoDumpBlif( */ if (f == DD_ZERO(dd)) { #if SIZEOF_VOID_P == 8 - retval = fprintf(fp, ".names %lx\n",(unsigned long) f / (unsigned long) sizeof(DdNode)); + retval = fprintf(fp, ".names %lx\n%s", + (ptruint) f / (ptruint) sizeof(DdNode), + mv ? "0\n" : ""); #else - retval = fprintf(fp, ".names %x\n",(unsigned) f / (unsigned) sizeof(DdNode)); + retval = fprintf(fp, ".names %x\n%s", + (ptruint) f / (ptruint) sizeof(DdNode), + mv ? "0\n" : ""); #endif if (retval == EOF) { return(0); @@ -977,48 +1027,80 @@ ddDoDumpBlif( } } if (cuddIsConstant(f)) - return(0); + return(0); /* Recursive calls. */ T = cuddT(f); - retval = ddDoDumpBlif(dd,T,fp,visited,names); + retval = ddDoDumpBlif(dd,T,fp,visited,names,mv); if (retval != 1) return(retval); E = Cudd_Regular(cuddE(f)); - retval = ddDoDumpBlif(dd,E,fp,visited,names); + retval = ddDoDumpBlif(dd,E,fp,visited,names,mv); if (retval != 1) return(retval); /* Write multiplexer taking complement arc into account. */ if (names != NULL) { - retval = fprintf(fp,".names %s", names[f->index]); + retval = fprintf(fp,".names %s", names[f->index]); } else { - retval = fprintf(fp,".names %d", f->index); +#if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4 + retval = fprintf(fp,".names %u", f->index); +#else + retval = fprintf(fp,".names %hu", f->index); +#endif } if (retval == EOF) - return(0); + 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)); + if (mv) { + if (Cudd_IsComplement(cuddE(f))) { + retval = fprintf(fp," %lx %lx %lx\n.def 0\n1 1 - 1\n0 - 0 1\n", + (ptruint) T / (ptruint) sizeof(DdNode), + (ptruint) E / (ptruint) sizeof(DdNode), + (ptruint) f / (ptruint) sizeof(DdNode)); + } else { + retval = fprintf(fp," %lx %lx %lx\n.def 0\n1 1 - 1\n0 - 1 1\n", + (ptruint) T / (ptruint) sizeof(DdNode), + (ptruint) E / (ptruint) sizeof(DdNode), + (ptruint) f / (ptruint) 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)); + if (Cudd_IsComplement(cuddE(f))) { + retval = fprintf(fp," %lx %lx %lx\n11- 1\n0-0 1\n", + (ptruint) T / (ptruint) sizeof(DdNode), + (ptruint) E / (ptruint) sizeof(DdNode), + (ptruint) f / (ptruint) sizeof(DdNode)); + } else { + retval = fprintf(fp," %lx %lx %lx\n11- 1\n0-1 1\n", + (ptruint) T / (ptruint) sizeof(DdNode), + (ptruint) E / (ptruint) sizeof(DdNode), + (ptruint) f / (ptruint) 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)); + if (mv) { + if (Cudd_IsComplement(cuddE(f))) { + retval = fprintf(fp," %x %x %x\n.def 0\n1 1 - 1\n0 - 0 1\n", + (ptruint) T / (ptruint) sizeof(DdNode), + (ptruint) E / (ptruint) sizeof(DdNode), + (ptruint) f / (ptruint) sizeof(DdNode)); + } else { + retval = fprintf(fp," %x %x %x\n.def 0\n1 1 - 1\n0 - 1 1\n", + (ptruint) T / (ptruint) sizeof(DdNode), + (ptruint) E / (ptruint) sizeof(DdNode), + (ptruint) f / (ptruint) 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)); + if (Cudd_IsComplement(cuddE(f))) { + retval = fprintf(fp," %x %x %x\n11- 1\n0-0 1\n", + (ptruint) T / (ptruint) sizeof(DdNode), + (ptruint) E / (ptruint) sizeof(DdNode), + (ptruint) f / (ptruint) sizeof(DdNode)); + } else { + retval = fprintf(fp," %x %x %x\n11- 1\n0-1 1\n", + (ptruint) T / (ptruint) sizeof(DdNode), + (ptruint) E / (ptruint) sizeof(DdNode), + (ptruint) f / (ptruint) sizeof(DdNode)); + } } #endif if (retval == EOF) { @@ -1051,21 +1133,21 @@ ddDoDumpDaVinci( FILE * fp, st_table * visited, char ** names, - long mask) + ptruint mask) { - DdNode *T, *E; - int retval; - long id; + DdNode *T, *E; + int retval; + ptruint id; #ifdef DD_DEBUG assert(!Cudd_IsComplement(f)); #endif - id = ((long) f & mask) / sizeof(DdNode); + id = ((ptruint) f & mask) / sizeof(DdNode); /* If already visited, insert a reference. */ if (st_is_member(visited, (char *) f) == 1) { - retval = fprintf(fp,"r(\"%lx\")", id); + retval = fprintf(fp,"r(\"%p\")", (void *) id); if (retval == EOF) { return(0); } else { @@ -1083,7 +1165,9 @@ ddDoDumpDaVinci( /* 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)); + retval = fprintf(fp, + "l(\"%p\",n(\"constant\",[a(\"OBJECT\",\"%g\")],[]))", + (void *) id, cuddV(f)); if (retval == EOF) { return(0); } else { @@ -1093,13 +1177,17 @@ ddDoDumpDaVinci( /* Recursive calls. */ if (names != NULL) { - retval = fprintf(fp, - "l(\"%lx\",n(\"internal\",[a(\"OBJECT\",\"%s\"),", - id, names[f->index]); + retval = fprintf(fp, + "l(\"%p\",n(\"internal\",[a(\"OBJECT\",\"%s\"),", + (void *) id, names[f->index]); } else { - retval = fprintf(fp, - "l(\"%lx\",n(\"internal\",[a(\"OBJECT\",\"%d\"),", - id, f->index); + retval = fprintf(fp, +#if SIZEOF_VOID_P == 8 + "l(\"%p\",n(\"internal\",[a(\"OBJECT\",\"%u\"),", +#else + "l(\"%p\",n(\"internal\",[a(\"OBJECT\",\"%hu\"),", +#endif + (void *) id, f->index); } retval = fprintf(fp, "a(\"_GO\",\"ellipse\")],[e(\"then\",[a(\"EDGECOLOR\",\"blue\"),a(\"_DIR\",\"none\")],"); if (retval == EOF) return(0); @@ -1107,7 +1195,7 @@ ddDoDumpDaVinci( 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"); + Cudd_IsComplement(cuddE(f)) ? "red" : "green"); if (retval == EOF) return(0); E = Cudd_Regular(cuddE(f)); retval = ddDoDumpDaVinci(dd,E,fp,visited,names,mask); @@ -1144,21 +1232,21 @@ ddDoDumpDDcal( FILE * fp, st_table * visited, char ** names, - long mask) + ptruint mask) { - DdNode *T, *E; - int retval; - long id, idT, idE; + DdNode *T, *E; + int retval; + ptruint id, idT, idE; #ifdef DD_DEBUG assert(!Cudd_IsComplement(f)); #endif - id = ((long) f & mask) / sizeof(DdNode); + id = ((ptruint) f & mask) / sizeof(DdNode); /* If already visited, do nothing. */ if (st_is_member(visited, (char *) f) == 1) { - return(1); + return(1); } /* Check for abnormal condition that should never happen. */ @@ -1171,9 +1259,9 @@ ddDoDumpDDcal( /* 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 (f != DD_ONE(dd) && f != DD_ZERO(dd)) + return(0); + retval = fprintf(fp, "n%p = %g\n", (void *) id, cuddV(f)); if (retval == EOF) { return(0); } else { @@ -1188,16 +1276,22 @@ ddDoDumpDDcal( 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); + idT = ((ptruint) T & mask) / sizeof(DdNode); + idE = ((ptruint) 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)) ? "'" : ""); + retval = fprintf(fp, "n%p = %s * n%p + %s' * n%p%s\n", + (void *) id, names[f->index], + (void *) idT, names[f->index], + (void *) 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 SIZEOF_VOID_P == 8 + retval = fprintf(fp, "n%p = v%u * n%p + v%u' * n%p%s\n", +#else + retval = fprintf(fp, "n%p = v%hu * n%p + v%hu' * n%p%s\n", +#endif + (void *) id, f->index, + (void *) idT, f->index, + (void *) idE, Cudd_IsComplement(cuddE(f)) ? "'" : ""); } if (retval == EOF) { return(0); @@ -1232,8 +1326,8 @@ ddDoDumpFactoredForm( FILE * fp, char ** names) { - DdNode *T, *E; - int retval; + DdNode *T, *E; + int retval; #ifdef DD_DEBUG assert(!Cudd_IsComplement(f)); @@ -1248,47 +1342,56 @@ ddDoDumpFactoredForm( T = cuddT(f); E = cuddE(f); if (T != DD_ZERO(dd)) { - if (E != DD_ONE(dd)) { + if (E != DD_ONE(dd)) { + if (names != NULL) { + retval = fprintf(fp, "%s", names[f->index]); + } else { +#if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4 + retval = fprintf(fp, "x%u", f->index); +#else + retval = fprintf(fp, "x%hu", f->index); +#endif + } + 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]); + retval = fprintf(fp, "!%s", names[f->index]); } else { - retval = fprintf(fp, "x%d", f->index); +#if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4 + retval = fprintf(fp, "!x%u", f->index); +#else + retval = fprintf(fp, "!x%hu", f->index); +#endif } if (retval == EOF) return(0); } - if (T != DD_ONE(dd)) { - retval = fprintf(fp, "%s(", E != DD_ONE(dd) ? " * " : ""); + 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,T,fp,names); + retval = ddDoDumpFactoredForm(dd,E,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 */ + ABC_NAMESPACE_IMPL_END |