diff options
Diffstat (limited to 'src/bdd/cudd/cuddBddCorr.c')
-rw-r--r-- | src/bdd/cudd/cuddBddCorr.c | 481 |
1 files changed, 481 insertions, 0 deletions
diff --git a/src/bdd/cudd/cuddBddCorr.c b/src/bdd/cudd/cuddBddCorr.c new file mode 100644 index 00000000..c99324a8 --- /dev/null +++ b/src/bdd/cudd/cuddBddCorr.c @@ -0,0 +1,481 @@ +/**CFile*********************************************************************** + + FileName [cuddBddCorr.c] + + PackageName [cudd] + + Synopsis [Correlation between BDDs.] + + Description [External procedures included in this module: + <ul> + <li> Cudd_bddCorrelation() + <li> Cudd_bddCorrelationWeights() + </ul> + Static procedures included in this module: + <ul> + <li> bddCorrelationAux() + <li> bddCorrelationWeightsAux() + <li> CorrelCompare() + <li> CorrelHash() + <li> CorrelCleanUp() + </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 */ +/*---------------------------------------------------------------------------*/ + +typedef struct hashEntry { + DdNode *f; + DdNode *g; +} HashEntry; + + +/*---------------------------------------------------------------------------*/ +/* Variable declarations */ +/*---------------------------------------------------------------------------*/ + +#ifndef lint +static char rcsid[] DD_UNUSED = "$Id: cuddBddCorr.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $"; +#endif + +#ifdef CORREL_STATS +static int num_calls; +#endif + +/*---------------------------------------------------------------------------*/ +/* Macro declarations */ +/*---------------------------------------------------------------------------*/ + + +/**AutomaticStart*************************************************************/ + +/*---------------------------------------------------------------------------*/ +/* Static function prototypes */ +/*---------------------------------------------------------------------------*/ + +static double bddCorrelationAux ARGS((DdManager *dd, DdNode *f, DdNode *g, st_table *table)); +static double bddCorrelationWeightsAux ARGS((DdManager *dd, DdNode *f, DdNode *g, double *prob, st_table *table)); +static int CorrelCompare ARGS((const char *key1, const char *key2)); +static int CorrelHash ARGS((char *key, int modulus)); +static enum st_retval CorrelCleanUp ARGS((char *key, char *value, char *arg)); + +/**AutomaticEnd***************************************************************/ + + +/*---------------------------------------------------------------------------*/ +/* Definition of exported functions */ +/*---------------------------------------------------------------------------*/ + + +/**Function******************************************************************** + + Synopsis [Computes the correlation of f and g.] + + Description [Computes the correlation of f and g. If f == g, their + correlation is 1. If f == g', their correlation is 0. Returns the + fraction of minterms in the ON-set of the EXNOR of f and g. If it + runs out of memory, returns (double)CUDD_OUT_OF_MEM.] + + SideEffects [None] + + SeeAlso [Cudd_bddCorrelationWeights] + +******************************************************************************/ +double +Cudd_bddCorrelation( + DdManager * manager, + DdNode * f, + DdNode * g) +{ + + st_table *table; + double correlation; + +#ifdef CORREL_STATS + num_calls = 0; +#endif + + table = st_init_table(CorrelCompare,CorrelHash); + if (table == NULL) return((double)CUDD_OUT_OF_MEM); + correlation = bddCorrelationAux(manager,f,g,table); + st_foreach(table, CorrelCleanUp, NIL(char)); + st_free_table(table); + return(correlation); + +} /* end of Cudd_bddCorrelation */ + + +/**Function******************************************************************** + + Synopsis [Computes the correlation of f and g for given input + probabilities.] + + Description [Computes the correlation of f and g for given input + probabilities. On input, prob\[i\] is supposed to contain the + probability of the i-th input variable to be 1. + If f == g, their correlation is 1. If f == g', their + correlation is 0. Returns the probability that f and g have the same + value. If it runs out of memory, returns (double)CUDD_OUT_OF_MEM. The + correlation of f and the constant one gives the probability of f.] + + SideEffects [None] + + SeeAlso [Cudd_bddCorrelation] + +******************************************************************************/ +double +Cudd_bddCorrelationWeights( + DdManager * manager, + DdNode * f, + DdNode * g, + double * prob) +{ + + st_table *table; + double correlation; + +#ifdef CORREL_STATS + num_calls = 0; +#endif + + table = st_init_table(CorrelCompare,CorrelHash); + if (table == NULL) return((double)CUDD_OUT_OF_MEM); + correlation = bddCorrelationWeightsAux(manager,f,g,prob,table); + st_foreach(table, CorrelCleanUp, NIL(char)); + st_free_table(table); + return(correlation); + +} /* end of Cudd_bddCorrelationWeights */ + + +/*---------------------------------------------------------------------------*/ +/* Definition of internal functions */ +/*---------------------------------------------------------------------------*/ + + +/*---------------------------------------------------------------------------*/ +/* Definition of static functions */ +/*---------------------------------------------------------------------------*/ + + +/**Function******************************************************************** + + Synopsis [Performs the recursive step of Cudd_bddCorrelation.] + + Description [Performs the recursive step of Cudd_bddCorrelation. + Returns the fraction of minterms in the ON-set of the EXNOR of f and + g.] + + SideEffects [None] + + SeeAlso [bddCorrelationWeightsAux] + +******************************************************************************/ +static double +bddCorrelationAux( + DdManager * dd, + DdNode * f, + DdNode * g, + st_table * table) +{ + DdNode *Fv, *Fnv, *G, *Gv, *Gnv; + double min, *pmin, min1, min2, *dummy; + HashEntry *entry; + unsigned int topF, topG; + + statLine(dd); +#ifdef CORREL_STATS + num_calls++; +#endif + + /* Terminal cases: only work for BDDs. */ + if (f == g) return(1.0); + if (f == Cudd_Not(g)) return(0.0); + + /* Standardize call using the following properties: + ** (f EXNOR g) = (g EXNOR f) + ** (f' EXNOR g') = (f EXNOR g). + */ + if (f > g) { + DdNode *tmp = f; + f = g; g = tmp; + } + if (Cudd_IsComplement(f)) { + f = Cudd_Not(f); + g = Cudd_Not(g); + } + /* From now on, f is regular. */ + + entry = ALLOC(HashEntry,1); + if (entry == NULL) { + dd->errorCode = CUDD_MEMORY_OUT; + return(CUDD_OUT_OF_MEM); + } + entry->f = f; entry->g = g; + + /* We do not use the fact that + ** correlation(f,g') = 1 - correlation(f,g) + ** to minimize the risk of cancellation. + */ + if (st_lookup(table, (char *)entry, (char **)&dummy)) { + min = *dummy; + FREE(entry); + return(min); + } + + G = Cudd_Regular(g); + topF = cuddI(dd,f->index); topG = cuddI(dd,G->index); + if (topF <= topG) { Fv = cuddT(f); Fnv = cuddE(f); } else { Fv = Fnv = f; } + if (topG <= topF) { Gv = cuddT(G); Gnv = cuddE(G); } else { Gv = Gnv = G; } + + if (g != G) { + Gv = Cudd_Not(Gv); + Gnv = Cudd_Not(Gnv); + } + + min1 = bddCorrelationAux(dd, Fv, Gv, table) / 2.0; + if (min1 == (double)CUDD_OUT_OF_MEM) { + FREE(entry); + return(CUDD_OUT_OF_MEM); + } + min2 = bddCorrelationAux(dd, Fnv, Gnv, table) / 2.0; + if (min2 == (double)CUDD_OUT_OF_MEM) { + FREE(entry); + return(CUDD_OUT_OF_MEM); + } + min = (min1+min2); + + pmin = ALLOC(double,1); + if (pmin == NULL) { + dd->errorCode = CUDD_MEMORY_OUT; + return((double)CUDD_OUT_OF_MEM); + } + *pmin = min; + + if (st_insert(table,(char *)entry, (char *)pmin) == ST_OUT_OF_MEM) { + FREE(entry); + FREE(pmin); + return((double)CUDD_OUT_OF_MEM); + } + return(min); + +} /* end of bddCorrelationAux */ + + +/**Function******************************************************************** + + Synopsis [Performs the recursive step of Cudd_bddCorrelationWeigths.] + + Description [] + + SideEffects [None] + + SeeAlso [bddCorrelationAux] + +******************************************************************************/ +static double +bddCorrelationWeightsAux( + DdManager * dd, + DdNode * f, + DdNode * g, + double * prob, + st_table * table) +{ + DdNode *Fv, *Fnv, *G, *Gv, *Gnv; + double min, *pmin, min1, min2, *dummy; + HashEntry *entry; + int topF, topG, index; + + statLine(dd); +#ifdef CORREL_STATS + num_calls++; +#endif + + /* Terminal cases: only work for BDDs. */ + if (f == g) return(1.0); + if (f == Cudd_Not(g)) return(0.0); + + /* Standardize call using the following properties: + ** (f EXNOR g) = (g EXNOR f) + ** (f' EXNOR g') = (f EXNOR g). + */ + if (f > g) { + DdNode *tmp = f; + f = g; g = tmp; + } + if (Cudd_IsComplement(f)) { + f = Cudd_Not(f); + g = Cudd_Not(g); + } + /* From now on, f is regular. */ + + entry = ALLOC(HashEntry,1); + if (entry == NULL) { + dd->errorCode = CUDD_MEMORY_OUT; + return((double)CUDD_OUT_OF_MEM); + } + entry->f = f; entry->g = g; + + /* We do not use the fact that + ** correlation(f,g') = 1 - correlation(f,g) + ** to minimize the risk of cancellation. + */ + if (st_lookup(table, (char *)entry, (char **)&dummy)) { + min = *dummy; + FREE(entry); + return(min); + } + + G = Cudd_Regular(g); + topF = cuddI(dd,f->index); topG = cuddI(dd,G->index); + if (topF <= topG) { + Fv = cuddT(f); Fnv = cuddE(f); + index = f->index; + } else { + Fv = Fnv = f; + index = G->index; + } + if (topG <= topF) { Gv = cuddT(G); Gnv = cuddE(G); } else { Gv = Gnv = G; } + + if (g != G) { + Gv = Cudd_Not(Gv); + Gnv = Cudd_Not(Gnv); + } + + min1 = bddCorrelationWeightsAux(dd, Fv, Gv, prob, table) * prob[index]; + if (min1 == (double)CUDD_OUT_OF_MEM) { + FREE(entry); + return((double)CUDD_OUT_OF_MEM); + } + min2 = bddCorrelationWeightsAux(dd, Fnv, Gnv, prob, table) * (1.0 - prob[index]); + if (min2 == (double)CUDD_OUT_OF_MEM) { + FREE(entry); + return((double)CUDD_OUT_OF_MEM); + } + min = (min1+min2); + + pmin = ALLOC(double,1); + if (pmin == NULL) { + dd->errorCode = CUDD_MEMORY_OUT; + return((double)CUDD_OUT_OF_MEM); + } + *pmin = min; + + if (st_insert(table,(char *)entry, (char *)pmin) == ST_OUT_OF_MEM) { + FREE(entry); + FREE(pmin); + return((double)CUDD_OUT_OF_MEM); + } + return(min); + +} /* end of bddCorrelationWeightsAux */ + + +/**Function******************************************************************** + + Synopsis [Compares two hash table entries.] + + Description [Compares two hash table entries. Returns 0 if they are + identical; 1 otherwise.] + + SideEffects [None] + +******************************************************************************/ +static int +CorrelCompare( + const char * key1, + const char * key2) +{ + HashEntry *entry1; + HashEntry *entry2; + + entry1 = (HashEntry *) key1; + entry2 = (HashEntry *) key2; + if (entry1->f != entry2->f || entry1->g != entry2->g) return(1); + + return(0); + +} /* end of CorrelCompare */ + + +/**Function******************************************************************** + + Synopsis [Hashes a hash table entry.] + + Description [Hashes a hash table entry. It is patterned after + st_strhash. Returns a value between 0 and modulus.] + + SideEffects [None] + +******************************************************************************/ +static int +CorrelHash( + char * key, + int modulus) +{ + HashEntry *entry; + int val = 0; + + entry = (HashEntry *) key; +#if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4 + val = ((int) ((long)entry->f))*997 + ((int) ((long)entry->g)); +#else + val = ((int) entry->f)*997 + ((int) entry->g); +#endif + + return ((val < 0) ? -val : val) % modulus; + +} /* end of CorrelHash */ + + +/**Function******************************************************************** + + Synopsis [Frees memory associated with hash table.] + + Description [Frees memory associated with hash table. Returns + ST_CONTINUE.] + + SideEffects [None] + +******************************************************************************/ +static enum st_retval +CorrelCleanUp( + char * key, + char * value, + char * arg) +{ + double *d; + HashEntry *entry; + + entry = (HashEntry *) key; + FREE(entry); + d = (double *)value; + FREE(d); + return ST_CONTINUE; + +} /* end of CorrelCleanUp */ + |