summaryrefslogtreecommitdiffstats
path: root/src/bdd/cudd/cuddZddUtil.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/bdd/cudd/cuddZddUtil.c')
-rw-r--r--src/bdd/cudd/cuddZddUtil.c1021
1 files changed, 1021 insertions, 0 deletions
diff --git a/src/bdd/cudd/cuddZddUtil.c b/src/bdd/cudd/cuddZddUtil.c
new file mode 100644
index 00000000..616d16d4
--- /dev/null
+++ b/src/bdd/cudd/cuddZddUtil.c
@@ -0,0 +1,1021 @@
+/**CFile***********************************************************************
+
+ FileName [cuddZddUtil.c]
+
+ PackageName [cudd]
+
+ Synopsis [Utility functions for ZDDs.]
+
+ Description [External procedures included in this module:
+ <ul>
+ <li> Cudd_zddPrintMinterm()
+ <li> Cudd_zddPrintCover()
+ <li> Cudd_zddPrintDebug()
+ <li> Cudd_zddDumpDot()
+ </ul>
+ Internal procedures included in this module:
+ <ul>
+ <li> cuddZddP()
+ </ul>
+ Static procedures included in this module:
+ <ul>
+ <li> zp2()
+ <li> zdd_print_minterm_aux()
+ </ul>
+ ]
+
+ SeeAlso []
+
+ Author [Hyong-Kyoon Shin, In-Ho Moon]
+
+ 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: cuddZddUtil.c,v 1.1.1.1 2003/02/24 22:23:54 wjiang Exp $";
+#endif
+
+/*---------------------------------------------------------------------------*/
+/* Macro declarations */
+/*---------------------------------------------------------------------------*/
+
+
+/**AutomaticStart*************************************************************/
+
+/*---------------------------------------------------------------------------*/
+/* Static function prototypes */
+/*---------------------------------------------------------------------------*/
+
+static int zp2 ARGS((DdManager *zdd, DdNode *f, st_table *t));
+static void zdd_print_minterm_aux ARGS((DdManager *zdd, DdNode *node, int level, int *list));
+static void zddPrintCoverAux ARGS((DdManager *zdd, DdNode *node, int level, int *list));
+
+/**AutomaticEnd***************************************************************/
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of exported functions */
+/*---------------------------------------------------------------------------*/
+
+
+/**Function********************************************************************
+
+ Synopsis [Prints a disjoint sum of product form for a ZDD.]
+
+ Description [Prints a disjoint sum of product form for a ZDD. Returns 1
+ if successful; 0 otherwise.]
+
+ SideEffects [None]
+
+ SeeAlso [Cudd_zddPrintDebug Cudd_zddPrintCover]
+
+******************************************************************************/
+int
+Cudd_zddPrintMinterm(
+ DdManager * zdd,
+ DdNode * node)
+{
+ int i, size;
+ int *list;
+
+ size = (int)zdd->sizeZ;
+ list = ALLOC(int, size);
+ if (list == NULL) {
+ zdd->errorCode = CUDD_MEMORY_OUT;
+ return(0);
+ }
+ for (i = 0; i < size; i++) list[i] = 3; /* bogus value should disappear */
+ zdd_print_minterm_aux(zdd, node, 0, list);
+ FREE(list);
+ return(1);
+
+} /* end of Cudd_zddPrintMinterm */
+
+
+/**Function********************************************************************
+
+ Synopsis [Prints a sum of products from a ZDD representing a cover.]
+
+ Description [Prints a sum of products from a ZDD representing a cover.
+ Returns 1 if successful; 0 otherwise.]
+
+ SideEffects [None]
+
+ SeeAlso [Cudd_zddPrintMinterm]
+
+******************************************************************************/
+int
+Cudd_zddPrintCover(
+ DdManager * zdd,
+ DdNode * node)
+{
+ int i, size;
+ int *list;
+
+ size = (int)zdd->sizeZ;
+ if (size % 2 != 0) return(0); /* number of variables should be even */
+ list = ALLOC(int, size);
+ if (list == NULL) {
+ zdd->errorCode = CUDD_MEMORY_OUT;
+ return(0);
+ }
+ for (i = 0; i < size; i++) list[i] = 3; /* bogus value should disappear */
+ zddPrintCoverAux(zdd, node, 0, list);
+ FREE(list);
+ return(1);
+
+} /* end of Cudd_zddPrintCover */
+
+
+/**Function********************************************************************
+
+ Synopsis [Prints to the standard output a ZDD and its statistics.]
+
+ Description [Prints to the standard output a DD and its statistics.
+ The statistics include the number of nodes and the number of minterms.
+ (The number of minterms is also the number of combinations in the set.)
+ The statistics are printed if pr &gt; 0. Specifically:
+ <ul>
+ <li> pr = 0 : prints nothing
+ <li> pr = 1 : prints counts of nodes and minterms
+ <li> pr = 2 : prints counts + disjoint sum of products
+ <li> pr = 3 : prints counts + list of nodes
+ <li> pr &gt; 3 : prints counts + disjoint sum of products + list of nodes
+ </ul>
+ Returns 1 if successful; 0 otherwise.
+ ]
+
+ SideEffects [None]
+
+ SeeAlso []
+
+******************************************************************************/
+int
+Cudd_zddPrintDebug(
+ DdManager * zdd,
+ DdNode * f,
+ int n,
+ int pr)
+{
+ DdNode *empty = DD_ZERO(zdd);
+ int nodes;
+ double minterms;
+ int retval = 1;
+
+ if (f == empty && pr > 0) {
+ (void) fprintf(zdd->out,": is the empty ZDD\n");
+ (void) fflush(zdd->out);
+ return(1);
+ }
+
+ if (pr > 0) {
+ nodes = Cudd_zddDagSize(f);
+ if (nodes == CUDD_OUT_OF_MEM) retval = 0;
+ minterms = Cudd_zddCountMinterm(zdd, f, n);
+ if (minterms == (double)CUDD_OUT_OF_MEM) retval = 0;
+ (void) fprintf(zdd->out,": %d nodes %g minterms\n",
+ nodes, minterms);
+ if (pr > 2)
+ if (!cuddZddP(zdd, f)) retval = 0;
+ if (pr == 2 || pr > 3) {
+ if (!Cudd_zddPrintMinterm(zdd, f)) retval = 0;
+ (void) fprintf(zdd->out,"\n");
+ }
+ (void) fflush(zdd->out);
+ }
+ return(retval);
+
+} /* end of Cudd_zddPrintDebug */
+
+
+
+/**Function********************************************************************
+
+ Synopsis [Finds the first path of a ZDD.]
+
+ Description [Defines an iterator on the paths of a ZDD
+ and finds its first path. Returns a generator that contains the
+ information necessary to continue the enumeration if successful; NULL
+ otherwise.<p>
+ A path is represented as an array of literals, which are integers in
+ {0, 1, 2}; 0 represents an else arc out of a node, 1 represents a then arc
+ out of a node, and 2 stands for the absence of a node.
+ The size of the array equals the number of variables in the manager at
+ the time Cudd_zddFirstCube is called.<p>
+ The paths that end in the empty terminal are not enumerated.]
+
+ SideEffects [The first path is returned as a side effect.]
+
+ SeeAlso [Cudd_zddForeachPath Cudd_zddNextPath Cudd_GenFree
+ Cudd_IsGenEmpty]
+
+******************************************************************************/
+DdGen *
+Cudd_zddFirstPath(
+ DdManager * zdd,
+ DdNode * f,
+ int ** path)
+{
+ DdGen *gen;
+ DdNode *top, *next, *prev;
+ int i;
+ int nvars;
+
+ /* Sanity Check. */
+ if (zdd == NULL || f == NULL) return(NULL);
+
+ /* Allocate generator an initialize it. */
+ gen = ALLOC(DdGen,1);
+ if (gen == NULL) {
+ zdd->errorCode = CUDD_MEMORY_OUT;
+ return(NULL);
+ }
+
+ gen->manager = zdd;
+ gen->type = CUDD_GEN_ZDD_PATHS;
+ gen->status = CUDD_GEN_EMPTY;
+ gen->gen.cubes.cube = NULL;
+ gen->gen.cubes.value = DD_ZERO_VAL;
+ gen->stack.sp = 0;
+ gen->stack.stack = NULL;
+ gen->node = NULL;
+
+ nvars = zdd->sizeZ;
+ gen->gen.cubes.cube = ALLOC(int,nvars);
+ if (gen->gen.cubes.cube == NULL) {
+ zdd->errorCode = CUDD_MEMORY_OUT;
+ FREE(gen);
+ return(NULL);
+ }
+ for (i = 0; i < nvars; i++) gen->gen.cubes.cube[i] = 2;
+
+ /* The maximum stack depth is one plus the number of variables.
+ ** because a path may have nodes at all levels, including the
+ ** constant level.
+ */
+ gen->stack.stack = ALLOC(DdNode *, nvars+1);
+ if (gen->stack.stack == NULL) {
+ zdd->errorCode = CUDD_MEMORY_OUT;
+ FREE(gen->gen.cubes.cube);
+ FREE(gen);
+ return(NULL);
+ }
+ for (i = 0; i <= nvars; i++) gen->stack.stack[i] = NULL;
+
+ /* Find the first path of the ZDD. */
+ gen->stack.stack[gen->stack.sp] = f; gen->stack.sp++;
+
+ while (1) {
+ top = gen->stack.stack[gen->stack.sp-1];
+ if (!cuddIsConstant(top)) {
+ /* Take the else branch first. */
+ gen->gen.cubes.cube[top->index] = 0;
+ next = cuddE(top);
+ gen->stack.stack[gen->stack.sp] = next; gen->stack.sp++;
+ } else if (top == DD_ZERO(zdd)) {
+ /* Backtrack. */
+ while (1) {
+ if (gen->stack.sp == 1) {
+ /* The current node has no predecessor. */
+ gen->status = CUDD_GEN_EMPTY;
+ gen->stack.sp--;
+ goto done;
+ }
+ prev = gen->stack.stack[gen->stack.sp-2];
+ next = cuddT(prev);
+ if (next != top) { /* follow the then branch next */
+ gen->gen.cubes.cube[prev->index] = 1;
+ gen->stack.stack[gen->stack.sp-1] = next;
+ break;
+ }
+ /* Pop the stack and try again. */
+ gen->gen.cubes.cube[prev->index] = 2;
+ gen->stack.sp--;
+ top = gen->stack.stack[gen->stack.sp-1];
+ }
+ } else {
+ gen->status = CUDD_GEN_NONEMPTY;
+ gen->gen.cubes.value = cuddV(top);
+ goto done;
+ }
+ }
+
+done:
+ *path = gen->gen.cubes.cube;
+ return(gen);
+
+} /* end of Cudd_zddFirstPath */
+
+
+/**Function********************************************************************
+
+ Synopsis [Generates the next path of a ZDD.]
+
+ Description [Generates the next path of a ZDD onset,
+ using generator gen. Returns 0 if the enumeration is completed; 1
+ otherwise.]
+
+ SideEffects [The path is returned as a side effect. The
+ generator is modified.]
+
+ SeeAlso [Cudd_zddForeachPath Cudd_zddFirstPath Cudd_GenFree
+ Cudd_IsGenEmpty]
+
+******************************************************************************/
+int
+Cudd_zddNextPath(
+ DdGen * gen,
+ int ** path)
+{
+ DdNode *top, *next, *prev;
+ DdManager *zdd = gen->manager;
+
+ /* Backtrack from previously reached terminal node. */
+ while (1) {
+ if (gen->stack.sp == 1) {
+ /* The current node has no predecessor. */
+ gen->status = CUDD_GEN_EMPTY;
+ gen->stack.sp--;
+ goto done;
+ }
+ top = gen->stack.stack[gen->stack.sp-1];
+ prev = gen->stack.stack[gen->stack.sp-2];
+ next = cuddT(prev);
+ if (next != top) { /* follow the then branch next */
+ gen->gen.cubes.cube[prev->index] = 1;
+ gen->stack.stack[gen->stack.sp-1] = next;
+ break;
+ }
+ /* Pop the stack and try again. */
+ gen->gen.cubes.cube[prev->index] = 2;
+ gen->stack.sp--;
+ }
+
+ while (1) {
+ top = gen->stack.stack[gen->stack.sp-1];
+ if (!cuddIsConstant(top)) {
+ /* Take the else branch first. */
+ gen->gen.cubes.cube[top->index] = 0;
+ next = cuddE(top);
+ gen->stack.stack[gen->stack.sp] = next; gen->stack.sp++;
+ } else if (top == DD_ZERO(zdd)) {
+ /* Backtrack. */
+ while (1) {
+ if (gen->stack.sp == 1) {
+ /* The current node has no predecessor. */
+ gen->status = CUDD_GEN_EMPTY;
+ gen->stack.sp--;
+ goto done;
+ }
+ prev = gen->stack.stack[gen->stack.sp-2];
+ next = cuddT(prev);
+ if (next != top) { /* follow the then branch next */
+ gen->gen.cubes.cube[prev->index] = 1;
+ gen->stack.stack[gen->stack.sp-1] = next;
+ break;
+ }
+ /* Pop the stack and try again. */
+ gen->gen.cubes.cube[prev->index] = 2;
+ gen->stack.sp--;
+ top = gen->stack.stack[gen->stack.sp-1];
+ }
+ } else {
+ gen->status = CUDD_GEN_NONEMPTY;
+ gen->gen.cubes.value = cuddV(top);
+ goto done;
+ }
+ }
+
+done:
+ if (gen->status == CUDD_GEN_EMPTY) return(0);
+ *path = gen->gen.cubes.cube;
+ return(1);
+
+} /* end of Cudd_zddNextPath */
+
+
+/**Function********************************************************************
+
+ Synopsis [Converts a path of a ZDD representing a cover to a string.]
+
+ Description [Converts a path of a ZDD representing a cover to a
+ string. The string represents an implicant of the cover. The path
+ is typically produced by Cudd_zddForeachPath. Returns a pointer to
+ the string if successful; NULL otherwise. If the str input is NULL,
+ it allocates a new string. The string passed to this function must
+ have enough room for all variables and for the terminator.]
+
+ SideEffects [None]
+
+ SeeAlso [Cudd_zddForeachPath]
+
+******************************************************************************/
+char *
+Cudd_zddCoverPathToString(
+ DdManager *zdd /* DD manager */,
+ int *path /* path of ZDD representing a cover */,
+ char *str /* pointer to string to use if != NULL */
+ )
+{
+ int nvars = zdd->sizeZ;
+ int i;
+ char *res;
+
+ if (nvars & 1) return(NULL);
+ nvars >>= 1;
+ if (str == NULL) {
+ res = ALLOC(char, nvars+1);
+ if (res == NULL) return(NULL);
+ } else {
+ res = str;
+ }
+ for (i = 0; i < nvars; i++) {
+ int v = (path[2*i] << 2) | path[2*i+1];
+ switch (v) {
+ case 0:
+ case 2:
+ case 8:
+ case 10:
+ res[i] = '-';
+ break;
+ case 1:
+ case 9:
+ res[i] = '0';
+ break;
+ case 4:
+ case 6:
+ res[i] = '1';
+ break;
+ default:
+ res[i] = '?';
+ }
+ }
+ res[nvars] = 0;
+
+ return(res);
+
+} /* end of Cudd_zddCoverPathToString */
+
+
+/**Function********************************************************************
+
+ Synopsis [Writes a dot file representing the argument ZDDs.]
+
+ Description [Writes a file representing the argument ZDDs 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_zddDumpDot does not close the file: This is the caller
+ responsibility. Cudd_zddDumpDot 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_zddDumpDot uses the following convention to draw arcs:
+ <ul>
+ <li> solid line: THEN arcs;
+ <li> dashed line: ELSE arcs.
+ </ul>
+ The dot options are chosen so that the drawing fits on a letter-size
+ sheet.
+ ]
+
+ SideEffects [None]
+
+ SeeAlso [Cudd_DumpDot Cudd_zddPrintDebug]
+
+******************************************************************************/
+int
+Cudd_zddDumpDot(
+ 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->sizeZ;
+ st_table *visited = NULL;
+ st_generator *gen;
+ 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. */
+ for (i = 0; i < n; i++) {
+ support = Cudd_Support(dd,f[i]);
+ 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(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) 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;
+ }
+
+ /* Write the header and the global attributes. */
+ retval = fprintf(fp,"digraph \"ZDD\" {\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->invpermZ[i]]) {
+ if (inames == NULL) {
+ retval = fprintf(fp,"\" %d \" -> ", dd->invpermZ[i]);
+ } else {
+ retval = fprintf(fp,"\" %s \" -> ", inames[dd->invpermZ[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->invpermZ[i]]) {
+ retval = fprintf(fp,"{ rank = same; ");
+ if (retval == EOF) goto failure;
+ if (inames == NULL) {
+ retval = fprintf(fp,"\" %d \";\n", dd->invpermZ[i]);
+ } else {
+ retval = fprintf(fp,"\" %s \";\n", inames[dd->invpermZ[i]]);
+ }
+ if (retval == EOF) goto failure;
+ nodelist = dd->subtableZ[i].nodelist;
+ slots = dd->subtableZ[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;
+ 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->invpermZ[i]]) {
+ nodelist = dd->subtableZ[i].nodelist;
+ slots = dd->subtableZ[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;
+ 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_zddDumpBlif */
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of internal functions */
+/*---------------------------------------------------------------------------*/
+
+
+/**Function********************************************************************
+
+ Synopsis [Prints a ZDD to the standard output. One line per node is
+ printed.]
+
+ Description [Prints a ZDD to the standard output. One line per node is
+ printed. Returns 1 if successful; 0 otherwise.]
+
+ SideEffects [None]
+
+ SeeAlso [Cudd_zddPrintDebug]
+
+******************************************************************************/
+int
+cuddZddP(
+ DdManager * zdd,
+ DdNode * f)
+{
+ int retval;
+ st_table *table = st_init_table(st_ptrcmp, st_ptrhash);
+
+ if (table == NULL) return(0);
+
+ retval = zp2(zdd, f, table);
+ st_free_table(table);
+ (void) fputc('\n', zdd->out);
+ return(retval);
+
+} /* end of cuddZddP */
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of static functions */
+/*---------------------------------------------------------------------------*/
+
+
+/**Function********************************************************************
+
+ Synopsis [Performs the recursive step of cuddZddP.]
+
+ Description [Performs the recursive step of cuddZddP. Returns 1 in
+ case of success; 0 otherwise.]
+
+ SideEffects [None]
+
+ SeeAlso []
+
+******************************************************************************/
+static int
+zp2(
+ DdManager * zdd,
+ DdNode * f,
+ st_table * t)
+{
+ DdNode *n;
+ int T, E;
+ DdNode *base = DD_ONE(zdd);
+
+ if (f == NULL)
+ return(0);
+
+ if (Cudd_IsConstant(f)) {
+ (void)fprintf(zdd->out, "ID = %d\n", (f == base));
+ return(1);
+ }
+ if (st_is_member(t, (char *)f) == 1)
+ return(1);
+
+ if (st_insert(t, (char *) f, NULL) == ST_OUT_OF_MEM)
+ return(0);
+
+#if SIZEOF_VOID_P == 8
+ (void) fprintf(zdd->out, "ID = 0x%lx\tindex = %d\tr = %d\t",
+ (unsigned long)f / (unsigned long) sizeof(DdNode), f->index, f->ref);
+#else
+ (void) fprintf(zdd->out, "ID = 0x%x\tindex = %d\tr = %d\t",
+ (unsigned)f / (unsigned) sizeof(DdNode), f->index, f->ref);
+#endif
+
+ n = cuddT(f);
+ if (Cudd_IsConstant(n)) {
+ (void) fprintf(zdd->out, "T = %d\t\t", (n == base));
+ T = 1;
+ } else {
+#if SIZEOF_VOID_P == 8
+ (void) fprintf(zdd->out, "T = 0x%lx\t", (unsigned long) n /
+ (unsigned long) sizeof(DdNode));
+#else
+ (void) fprintf(zdd->out, "T = 0x%x\t", (unsigned) n / (unsigned) sizeof(DdNode));
+#endif
+ T = 0;
+ }
+
+ n = cuddE(f);
+ if (Cudd_IsConstant(n)) {
+ (void) fprintf(zdd->out, "E = %d\n", (n == base));
+ E = 1;
+ } else {
+#if SIZEOF_VOID_P == 8
+ (void) fprintf(zdd->out, "E = 0x%lx\n", (unsigned long) n /
+ (unsigned long) sizeof(DdNode));
+#else
+ (void) fprintf(zdd->out, "E = 0x%x\n", (unsigned) n / (unsigned) sizeof(DdNode));
+#endif
+ E = 0;
+ }
+
+ if (E == 0)
+ if (zp2(zdd, cuddE(f), t) == 0) return(0);
+ if (T == 0)
+ if (zp2(zdd, cuddT(f), t) == 0) return(0);
+ return(1);
+
+} /* end of zp2 */
+
+
+/**Function********************************************************************
+
+ Synopsis [Performs the recursive step of Cudd_zddPrintMinterm.]
+
+ Description []
+
+ SideEffects [None]
+
+ SeeAlso []
+
+******************************************************************************/
+static void
+zdd_print_minterm_aux(
+ DdManager * zdd /* manager */,
+ DdNode * node /* current node */,
+ int level /* depth in the recursion */,
+ int * list /* current recursion path */)
+{
+ DdNode *Nv, *Nnv;
+ int i, v;
+ DdNode *base = DD_ONE(zdd);
+
+ if (Cudd_IsConstant(node)) {
+ if (node == base) {
+ /* Check for missing variable. */
+ if (level != zdd->sizeZ) {
+ list[zdd->invpermZ[level]] = 0;
+ zdd_print_minterm_aux(zdd, node, level + 1, list);
+ return;
+ }
+ /* Terminal case: Print one cube based on the current recursion
+ ** path.
+ */
+ for (i = 0; i < zdd->sizeZ; i++) {
+ v = list[i];
+ if (v == 0)
+ (void) fprintf(zdd->out,"0");
+ else if (v == 1)
+ (void) fprintf(zdd->out,"1");
+ else if (v == 3)
+ (void) fprintf(zdd->out,"@"); /* should never happen */
+ else
+ (void) fprintf(zdd->out,"-");
+ }
+ (void) fprintf(zdd->out," 1\n");
+ }
+ } else {
+ /* Check for missing variable. */
+ if (level != cuddIZ(zdd,node->index)) {
+ list[zdd->invpermZ[level]] = 0;
+ zdd_print_minterm_aux(zdd, node, level + 1, list);
+ return;
+ }
+
+ Nnv = cuddE(node);
+ Nv = cuddT(node);
+ if (Nv == Nnv) {
+ list[node->index] = 2;
+ zdd_print_minterm_aux(zdd, Nnv, level + 1, list);
+ return;
+ }
+
+ list[node->index] = 1;
+ zdd_print_minterm_aux(zdd, Nv, level + 1, list);
+ list[node->index] = 0;
+ zdd_print_minterm_aux(zdd, Nnv, level + 1, list);
+ }
+ return;
+
+} /* end of zdd_print_minterm_aux */
+
+
+/**Function********************************************************************
+
+ Synopsis [Performs the recursive step of Cudd_zddPrintCover.]
+
+ Description []
+
+ SideEffects [None]
+
+ SeeAlso []
+
+******************************************************************************/
+static void
+zddPrintCoverAux(
+ DdManager * zdd /* manager */,
+ DdNode * node /* current node */,
+ int level /* depth in the recursion */,
+ int * list /* current recursion path */)
+{
+ DdNode *Nv, *Nnv;
+ int i, v;
+ DdNode *base = DD_ONE(zdd);
+
+ if (Cudd_IsConstant(node)) {
+ if (node == base) {
+ /* Check for missing variable. */
+ if (level != zdd->sizeZ) {
+ list[zdd->invpermZ[level]] = 0;
+ zddPrintCoverAux(zdd, node, level + 1, list);
+ return;
+ }
+ /* Terminal case: Print one cube based on the current recursion
+ ** path.
+ */
+ for (i = 0; i < zdd->sizeZ; i += 2) {
+ v = list[i] * 4 + list[i+1];
+ if (v == 0)
+ (void) putc('-',zdd->out);
+ else if (v == 4)
+ (void) putc('1',zdd->out);
+ else if (v == 1)
+ (void) putc('0',zdd->out);
+ else
+ (void) putc('@',zdd->out); /* should never happen */
+ }
+ (void) fprintf(zdd->out," 1\n");
+ }
+ } else {
+ /* Check for missing variable. */
+ if (level != cuddIZ(zdd,node->index)) {
+ list[zdd->invpermZ[level]] = 0;
+ zddPrintCoverAux(zdd, node, level + 1, list);
+ return;
+ }
+
+ Nnv = cuddE(node);
+ Nv = cuddT(node);
+ if (Nv == Nnv) {
+ list[node->index] = 2;
+ zddPrintCoverAux(zdd, Nnv, level + 1, list);
+ return;
+ }
+
+ list[node->index] = 1;
+ zddPrintCoverAux(zdd, Nv, level + 1, list);
+ list[node->index] = 0;
+ zddPrintCoverAux(zdd, Nnv, level + 1, list);
+ }
+ return;
+
+} /* end of zddPrintCoverAux */
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 12:52:18 +0000