diff options
Diffstat (limited to 'src/bdd/cudd/cuddZddMisc.c')
-rw-r--r-- | src/bdd/cudd/cuddZddMisc.c | 252 |
1 files changed, 0 insertions, 252 deletions
diff --git a/src/bdd/cudd/cuddZddMisc.c b/src/bdd/cudd/cuddZddMisc.c deleted file mode 100644 index 6a4ddd09..00000000 --- a/src/bdd/cudd/cuddZddMisc.c +++ /dev/null @@ -1,252 +0,0 @@ -/**CFile*********************************************************************** - - FileName [cuddZddMisc.c] - - PackageName [cudd] - - Synopsis [.] - - Description [External procedures included in this module: - <ul> - <li> Cudd_zddDagSize() - <li> Cudd_zddCountMinterm() - <li> Cudd_zddPrintSubtable() - </ul> - Internal procedures included in this module: - <ul> - </ul> - Static procedures included in this module: - <ul> - <li> cuddZddDagInt() - </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 <math.h> -#include "util_hack.h" -#include "cuddInt.h" - -/*---------------------------------------------------------------------------*/ -/* Constant declarations */ -/*---------------------------------------------------------------------------*/ - - -/*---------------------------------------------------------------------------*/ -/* Stucture declarations */ -/*---------------------------------------------------------------------------*/ - - -/*---------------------------------------------------------------------------*/ -/* Type declarations */ -/*---------------------------------------------------------------------------*/ - - -/*---------------------------------------------------------------------------*/ -/* Variable declarations */ -/*---------------------------------------------------------------------------*/ - -#ifndef lint -static char rcsid[] DD_UNUSED = "$Id: cuddZddMisc.c,v 1.1.1.1 2003/02/24 22:23:54 wjiang Exp $"; -#endif - -/*---------------------------------------------------------------------------*/ -/* Macro declarations */ -/*---------------------------------------------------------------------------*/ - - -/**AutomaticStart*************************************************************/ - -/*---------------------------------------------------------------------------*/ -/* Static function prototypes */ -/*---------------------------------------------------------------------------*/ - -static int cuddZddDagInt ARGS((DdNode *n, st_table *tab)); - -/**AutomaticEnd***************************************************************/ - - -/*---------------------------------------------------------------------------*/ -/* Definition of exported functions */ -/*---------------------------------------------------------------------------*/ - - -/**Function******************************************************************** - - Synopsis [Counts the number of nodes in a ZDD.] - - Description [Counts the number of nodes in a ZDD. This function - duplicates Cudd_DagSize and is only retained for compatibility.] - - SideEffects [None] - - SeeAlso [Cudd_DagSize] - -******************************************************************************/ -int -Cudd_zddDagSize( - DdNode * p_node) -{ - - int i; - st_table *table; - - table = st_init_table(st_ptrcmp, st_ptrhash); - i = cuddZddDagInt(p_node, table); - st_free_table(table); - return(i); - -} /* end of Cudd_zddDagSize */ - - -/**Function******************************************************************** - - Synopsis [Counts the number of minterms of a ZDD.] - - Description [Counts the number of minterms of the ZDD rooted at - <code>node</code>. This procedure takes a parameter - <code>path</code> that specifies how many variables are in the - support of the function. If the procedure runs out of memory, it - returns (double) CUDD_OUT_OF_MEM.] - - SideEffects [None] - - SeeAlso [Cudd_zddCountDouble] - -******************************************************************************/ -double -Cudd_zddCountMinterm( - DdManager * zdd, - DdNode * node, - int path) -{ - double dc_var, minterms; - - dc_var = (double)((double)(zdd->sizeZ) - (double)path); - minterms = Cudd_zddCountDouble(zdd, node) / pow(2.0, dc_var); - return(minterms); - -} /* end of Cudd_zddCountMinterm */ - - -/**Function******************************************************************** - - Synopsis [Prints the ZDD table.] - - Description [Prints the ZDD table for debugging purposes.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -void -Cudd_zddPrintSubtable( - DdManager * table) -{ - int i, j; - DdNode *z1, *z1_next, *base; - DdSubtable *ZSubTable; - - base = table->one; - for (i = table->sizeZ - 1; i >= 0; i--) { - ZSubTable = &(table->subtableZ[i]); - printf("subtable[%d]:\n", i); - for (j = ZSubTable->slots - 1; j >= 0; j--) { - z1 = ZSubTable->nodelist[j]; - while (z1 != NIL(DdNode)) { - (void) fprintf(table->out, -#if SIZEOF_VOID_P == 8 - "ID = 0x%lx\tindex = %d\tr = %d\t", - (unsigned long) z1 / (unsigned long) sizeof(DdNode), - z1->index, z1->ref); -#else - "ID = 0x%x\tindex = %d\tr = %d\t", - (unsigned) z1 / (unsigned) sizeof(DdNode), - z1->index, z1->ref); -#endif - z1_next = cuddT(z1); - if (Cudd_IsConstant(z1_next)) { - (void) fprintf(table->out, "T = %d\t\t", - (z1_next == base)); - } - else { -#if SIZEOF_VOID_P == 8 - (void) fprintf(table->out, "T = 0x%lx\t", - (unsigned long) z1_next / (unsigned long) sizeof(DdNode)); -#else - (void) fprintf(table->out, "T = 0x%x\t", - (unsigned) z1_next / (unsigned) sizeof(DdNode)); -#endif - } - z1_next = cuddE(z1); - if (Cudd_IsConstant(z1_next)) { - (void) fprintf(table->out, "E = %d\n", - (z1_next == base)); - } - else { -#if SIZEOF_VOID_P == 8 - (void) fprintf(table->out, "E = 0x%lx\n", - (unsigned long) z1_next / (unsigned long) sizeof(DdNode)); -#else - (void) fprintf(table->out, "E = 0x%x\n", - (unsigned) z1_next / (unsigned) sizeof(DdNode)); -#endif - } - - z1_next = z1->next; - z1 = z1_next; - } - } - } - putchar('\n'); - -} /* Cudd_zddPrintSubtable */ - - -/*---------------------------------------------------------------------------*/ -/* Definition of static functions */ -/*---------------------------------------------------------------------------*/ - - -/**Function******************************************************************** - - Synopsis [Performs the recursive step of Cudd_zddDagSize.] - - Description [Performs the recursive step of Cudd_zddDagSize. Does - not check for out-of-memory conditions.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -static int -cuddZddDagInt( - DdNode * n, - st_table * tab) -{ - if (n == NIL(DdNode)) - return(0); - - if (st_is_member(tab, (char *)n) == 1) - return(0); - - if (Cudd_IsConstant(n)) - return(0); - - (void)st_insert(tab, (char *)n, NIL(char)); - return(1 + cuddZddDagInt(cuddT(n), tab) + - cuddZddDagInt(cuddE(n), tab)); - -} /* cuddZddDagInt */ - |