diff options
Diffstat (limited to 'src/bdd/cudd/cuddZddUtil.c')
| -rw-r--r-- | src/bdd/cudd/cuddZddUtil.c | 1021 |
1 files changed, 0 insertions, 1021 deletions
diff --git a/src/bdd/cudd/cuddZddUtil.c b/src/bdd/cudd/cuddZddUtil.c deleted file mode 100644 index 616d16d4..00000000 --- a/src/bdd/cudd/cuddZddUtil.c +++ /dev/null @@ -1,1021 +0,0 @@ -/**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 > 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 > 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 */ |