diff options
Diffstat (limited to 'src/bdd/cudd/cuddSign.c')
-rw-r--r-- | src/bdd/cudd/cuddSign.c | 292 |
1 files changed, 292 insertions, 0 deletions
diff --git a/src/bdd/cudd/cuddSign.c b/src/bdd/cudd/cuddSign.c new file mode 100644 index 00000000..fcaa65c4 --- /dev/null +++ b/src/bdd/cudd/cuddSign.c @@ -0,0 +1,292 @@ +/**CFile*********************************************************************** + + FileName [cuddSign.c] + + PackageName [cudd] + + Synopsis [Computation of signatures] + + Description [External procedures included in this module: + <ul> + <li> Cudd_CofMinterm(); + </ul> + Static procedures included in this module: + <ul> + <li> ddCofMintermAux() + </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_hack.h" +#include "cuddInt.h" + + +/*---------------------------------------------------------------------------*/ +/* Constant declarations */ +/*---------------------------------------------------------------------------*/ + + +/*---------------------------------------------------------------------------*/ +/* Stucture declarations */ +/*---------------------------------------------------------------------------*/ + + +/*---------------------------------------------------------------------------*/ +/* Type declarations */ +/*---------------------------------------------------------------------------*/ + + +/*---------------------------------------------------------------------------*/ +/* Variable declarations */ +/*---------------------------------------------------------------------------*/ + +#ifndef lint +static char rcsid[] DD_UNUSED = "$Id: cuddSign.c,v 1.1.1.1 2003/02/24 22:23:53 wjiang Exp $"; +#endif + +static int size; + +#ifdef DD_STATS +static int num_calls; /* should equal 2n-1 (n is the # of nodes) */ +static int table_mem; +#endif + + +/*---------------------------------------------------------------------------*/ +/* Macro declarations */ +/*---------------------------------------------------------------------------*/ + + +/**AutomaticStart*************************************************************/ + +/*---------------------------------------------------------------------------*/ +/* Static function prototypes */ +/*---------------------------------------------------------------------------*/ + +static double * ddCofMintermAux ARGS((DdManager *dd, DdNode *node, st_table *table)); + +/**AutomaticEnd***************************************************************/ + + +/*---------------------------------------------------------------------------*/ +/* Definition of exported functions */ +/*---------------------------------------------------------------------------*/ + +/**Function******************************************************************** + + Synopsis [Computes the fraction of minterms in the on-set of all the + positive cofactors of a BDD or ADD.] + + Description [Computes the fraction of minterms in the on-set of all + the positive cofactors of DD. Returns the pointer to an array of + doubles if successful; NULL otherwise. The array hs as many + positions as there are BDD variables in the manager plus one. The + last position of the array contains the fraction of the minterms in + the ON-set of the function represented by the BDD or ADD. The other + positions of the array hold the variable signatures.] + + SideEffects [None] + +******************************************************************************/ +double * +Cudd_CofMinterm( + DdManager * dd, + DdNode * node) +{ + st_table *table; + double *values; + double *result = NULL; + int i, firstLevel; + +#ifdef DD_STATS + long startTime; + startTime = util_cpu_time(); + num_calls = 0; + table_mem = sizeof(st_table); +#endif + + table = st_init_table(st_ptrcmp, st_ptrhash); + if (table == NULL) { + (void) fprintf(dd->err, + "out-of-memory, couldn't measure DD cofactors.\n"); + dd->errorCode = CUDD_MEMORY_OUT; + return(NULL); + } + size = dd->size; + values = ddCofMintermAux(dd, node, table); + if (values != NULL) { + result = ALLOC(double,size + 1); + if (result != NULL) { +#ifdef DD_STATS + table_mem += (size + 1) * sizeof(double); +#endif + if (Cudd_IsConstant(node)) + firstLevel = 1; + else + firstLevel = cuddI(dd,Cudd_Regular(node)->index); + for (i = 0; i < size; i++) { + if (i >= cuddI(dd,Cudd_Regular(node)->index)) { + result[dd->invperm[i]] = values[i - firstLevel]; + } else { + result[dd->invperm[i]] = values[size - firstLevel]; + } + } + result[size] = values[size - firstLevel]; + } else { + dd->errorCode = CUDD_MEMORY_OUT; + } + } + +#ifdef DD_STATS + table_mem += table->num_bins * sizeof(st_table_entry *); +#endif + if (Cudd_Regular(node)->ref == 1) FREE(values); + st_foreach(table, cuddStCountfree, NULL); + st_free_table(table); +#ifdef DD_STATS + (void) fprintf(dd->out,"Number of calls: %d\tTable memory: %d bytes\n", + num_calls, table_mem); + (void) fprintf(dd->out,"Time to compute measures: %s\n", + util_print_time(util_cpu_time() - startTime)); +#endif + if (result == NULL) { + (void) fprintf(dd->out, + "out-of-memory, couldn't measure DD cofactors.\n"); + dd->errorCode = CUDD_MEMORY_OUT; + } + return(result); + +} /* end of Cudd_CofMinterm */ + + +/*---------------------------------------------------------------------------*/ +/* Definition of internal functions */ +/*---------------------------------------------------------------------------*/ + + +/*---------------------------------------------------------------------------*/ +/* Definition of static functions */ +/*---------------------------------------------------------------------------*/ + + +/**Function******************************************************************** + + Synopsis [Recursive Step for Cudd_CofMinterm function.] + + Description [Traverses the DD node and computes the fraction of + minterms in the on-set of all positive cofactors simultaneously. + It allocates an array with two more entries than there are + variables below the one labeling the node. One extra entry (the + first in the array) is for the variable labeling the node. The other + entry (the last one in the array) holds the fraction of minterms of + the function rooted at node. Each other entry holds the value for + one cofactor. The array is put in a symbol table, to avoid repeated + computation, and its address is returned by the procedure, for use + by the caller. Returns a pointer to the array of cofactor measures.] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +static double * +ddCofMintermAux( + DdManager * dd, + DdNode * node, + st_table * table) +{ + DdNode *N; /* regular version of node */ + DdNode *Nv, *Nnv; + double *values; + double *valuesT, *valuesE; + int i; + int localSize, localSizeT, localSizeE; + double vT, vE; + + statLine(dd); +#ifdef DD_STATS + num_calls++; +#endif + + if (st_lookup(table, (char *) node, (char **) &values)) { + return(values); + } + + N = Cudd_Regular(node); + if (cuddIsConstant(N)) { + localSize = 1; + } else { + localSize = size - cuddI(dd,N->index) + 1; + } + values = ALLOC(double, localSize); + if (values == NULL) { + dd->errorCode = CUDD_MEMORY_OUT; + return(NULL); + } + + if (cuddIsConstant(N)) { + if (node == DD_ZERO(dd) || node == Cudd_Not(DD_ONE(dd))) { + values[0] = 0.0; + } else { + values[0] = 1.0; + } + } else { + Nv = Cudd_NotCond(cuddT(N),N!=node); + Nnv = Cudd_NotCond(cuddE(N),N!=node); + + valuesT = ddCofMintermAux(dd, Nv, table); + if (valuesT == NULL) return(NULL); + valuesE = ddCofMintermAux(dd, Nnv, table); + if (valuesE == NULL) return(NULL); + + if (Cudd_IsConstant(Nv)) { + localSizeT = 1; + } else { + localSizeT = size - cuddI(dd,Cudd_Regular(Nv)->index) + 1; + } + if (Cudd_IsConstant(Nnv)) { + localSizeE = 1; + } else { + localSizeE = size - cuddI(dd,Cudd_Regular(Nnv)->index) + 1; + } + values[0] = valuesT[localSizeT - 1]; + for (i = 1; i < localSize; i++) { + if (i >= cuddI(dd,Cudd_Regular(Nv)->index) - cuddI(dd,N->index)) { + vT = valuesT[i - cuddI(dd,Cudd_Regular(Nv)->index) + + cuddI(dd,N->index)]; + } else { + vT = valuesT[localSizeT - 1]; + } + if (i >= cuddI(dd,Cudd_Regular(Nnv)->index) - cuddI(dd,N->index)) { + vE = valuesE[i - cuddI(dd,Cudd_Regular(Nnv)->index) + + cuddI(dd,N->index)]; + } else { + vE = valuesE[localSizeE - 1]; + } + values[i] = (vT + vE) / 2.0; + } + if (Cudd_Regular(Nv)->ref == 1) FREE(valuesT); + if (Cudd_Regular(Nnv)->ref == 1) FREE(valuesE); + } + + if (N->ref > 1) { + if (st_add_direct(table, (char *) node, (char *) values) == ST_OUT_OF_MEM) { + FREE(values); + return(NULL); + } +#ifdef DD_STATS + table_mem += localSize * sizeof(double) + sizeof(st_table_entry); +#endif + } + return(values); + +} /* end of ddCofMintermAux */ + |