📄 cuddexport.c
字号:
/**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.h"#include "cuddInt.h"/*---------------------------------------------------------------------------*//* Constant declarations *//*---------------------------------------------------------------------------*//*---------------------------------------------------------------------------*//* Stucture declarations *//*---------------------------------------------------------------------------*//*---------------------------------------------------------------------------*//* Type declarations *//*---------------------------------------------------------------------------*//*---------------------------------------------------------------------------*//* Variable declarations *//*---------------------------------------------------------------------------*/#ifndef lintstatic 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]******************************************************************************/intCudd_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]******************************************************************************/intCudd_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]******************************************************************************/intCudd_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; }
⌨️ 快捷键说明
复制代码
Ctrl + C
搜索代码
Ctrl + F
全屏模式
F11
切换主题
Ctrl + Shift + D
显示快捷键
?
增大字号
Ctrl + =
减小字号
Ctrl + -