src/bdd/cudd/cuddBddCorr.c File Reference

#include "util_hack.h"
#include "cuddInt.h"
Include dependency graph for cuddBddCorr.c:

Go to the source code of this file.

Data Structures

struct  hashEntry

Typedefs

typedef struct hashEntry HashEntry

Functions

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))
double Cudd_bddCorrelation (DdManager *manager, DdNode *f, DdNode *g)
double Cudd_bddCorrelationWeights (DdManager *manager, DdNode *f, DdNode *g, double *prob)
static double bddCorrelationAux (DdManager *dd, DdNode *f, DdNode *g, st_table *table)
static double bddCorrelationWeightsAux (DdManager *dd, DdNode *f, DdNode *g, double *prob, st_table *table)
static int CorrelCompare (const char *key1, const char *key2)
static int CorrelHash (char *key, int modulus)
static enum st_retval CorrelCleanUp (char *key, char *value, char *arg)

Variables

static char rcsid[] DD_UNUSED = "$Id: cuddBddCorr.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $"

Typedef Documentation

typedef struct hashEntry HashEntry

CFile***********************************************************************

FileName [cuddBddCorr.c]

PackageName [cudd]

Synopsis [Correlation between BDDs.]

Description [External procedures included in this module:

Static procedures included in this module:

]

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.]

Function Documentation

static enum st_retval CorrelCleanUp ARGS ( (char *key, char *value, char *arg)   )  [static]
static int CorrelHash ARGS ( (char *key, int modulus)   )  [static]
static int CorrelCompare ARGS ( (const char *key1, const char *key2)   )  [static]
static double bddCorrelationWeightsAux ARGS ( (DdManager *dd, DdNode *f, DdNode *g, double *prob, st_table *table)   )  [static]
static double bddCorrelationAux ARGS ( (DdManager *dd, DdNode *f, DdNode *g, st_table *table)   )  [static]

AutomaticStart

static double bddCorrelationAux ( DdManager *  dd,
DdNode *  f,
DdNode *  g,
st_table *  table 
) [static]

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]

Definition at line 199 of file cuddBddCorr.c.

00204 {
00205     DdNode      *Fv, *Fnv, *G, *Gv, *Gnv;
00206     double      min, *pmin, min1, min2, *dummy;
00207     HashEntry   *entry;
00208     unsigned int topF, topG;
00209 
00210     statLine(dd);
00211 #ifdef CORREL_STATS
00212     num_calls++;
00213 #endif
00214 
00215     /* Terminal cases: only work for BDDs. */
00216     if (f == g) return(1.0);
00217     if (f == Cudd_Not(g)) return(0.0);
00218 
00219     /* Standardize call using the following properties:
00220     **     (f EXNOR g)   = (g EXNOR f)
00221     **     (f' EXNOR g') = (f EXNOR g).
00222     */
00223     if (f > g) {
00224         DdNode *tmp = f;
00225         f = g; g = tmp;
00226     }
00227     if (Cudd_IsComplement(f)) {
00228         f = Cudd_Not(f);
00229         g = Cudd_Not(g);
00230     }
00231     /* From now on, f is regular. */
00232     
00233     entry = ALLOC(HashEntry,1);
00234     if (entry == NULL) {
00235         dd->errorCode = CUDD_MEMORY_OUT;
00236         return(CUDD_OUT_OF_MEM);
00237     }
00238     entry->f = f; entry->g = g;
00239 
00240     /* We do not use the fact that
00241     ** correlation(f,g') = 1 - correlation(f,g)
00242     ** to minimize the risk of cancellation.
00243     */
00244     if (st_lookup(table, (char *)entry, (char **)&dummy)) {
00245         min = *dummy;
00246         FREE(entry);
00247         return(min);
00248     }
00249 
00250     G = Cudd_Regular(g);
00251     topF = cuddI(dd,f->index); topG = cuddI(dd,G->index);
00252     if (topF <= topG) { Fv = cuddT(f); Fnv = cuddE(f); } else { Fv = Fnv = f; }
00253     if (topG <= topF) { Gv = cuddT(G); Gnv = cuddE(G); } else { Gv = Gnv = G; }
00254 
00255     if (g != G) {
00256         Gv = Cudd_Not(Gv);
00257         Gnv = Cudd_Not(Gnv);
00258     }
00259 
00260     min1 = bddCorrelationAux(dd, Fv, Gv, table) / 2.0;
00261     if (min1 == (double)CUDD_OUT_OF_MEM) {
00262         FREE(entry);
00263         return(CUDD_OUT_OF_MEM);
00264     }
00265     min2 = bddCorrelationAux(dd, Fnv, Gnv, table) / 2.0; 
00266     if (min2 == (double)CUDD_OUT_OF_MEM) {
00267         FREE(entry);
00268         return(CUDD_OUT_OF_MEM);
00269     }
00270     min = (min1+min2);
00271     
00272     pmin = ALLOC(double,1);
00273     if (pmin == NULL) {
00274         dd->errorCode = CUDD_MEMORY_OUT;
00275         return((double)CUDD_OUT_OF_MEM);
00276     }
00277     *pmin = min;
00278 
00279     if (st_insert(table,(char *)entry, (char *)pmin) == ST_OUT_OF_MEM) {
00280         FREE(entry);
00281         FREE(pmin);
00282         return((double)CUDD_OUT_OF_MEM);
00283     }
00284     return(min);
00285 
00286 } /* end of bddCorrelationAux */

static double bddCorrelationWeightsAux ( DdManager *  dd,
DdNode *  f,
DdNode *  g,
double *  prob,
st_table *  table 
) [static]

Function********************************************************************

Synopsis [Performs the recursive step of Cudd_bddCorrelationWeigths.]

Description []

SideEffects [None]

SeeAlso [bddCorrelationAux]

Definition at line 301 of file cuddBddCorr.c.

00307 {
00308     DdNode      *Fv, *Fnv, *G, *Gv, *Gnv;
00309     double      min, *pmin, min1, min2, *dummy;
00310     HashEntry   *entry;
00311     int         topF, topG, index;
00312 
00313     statLine(dd);
00314 #ifdef CORREL_STATS
00315     num_calls++;
00316 #endif
00317 
00318     /* Terminal cases: only work for BDDs. */
00319     if (f == g) return(1.0);
00320     if (f == Cudd_Not(g)) return(0.0);
00321 
00322     /* Standardize call using the following properties:
00323     **     (f EXNOR g)   = (g EXNOR f)
00324     **     (f' EXNOR g') = (f EXNOR g).
00325     */
00326     if (f > g) {
00327         DdNode *tmp = f;
00328         f = g; g = tmp;
00329     }
00330     if (Cudd_IsComplement(f)) {
00331         f = Cudd_Not(f);
00332         g = Cudd_Not(g);
00333     }
00334     /* From now on, f is regular. */
00335     
00336     entry = ALLOC(HashEntry,1);
00337     if (entry == NULL) {
00338         dd->errorCode = CUDD_MEMORY_OUT;
00339         return((double)CUDD_OUT_OF_MEM);
00340     }
00341     entry->f = f; entry->g = g;
00342 
00343     /* We do not use the fact that
00344     ** correlation(f,g') = 1 - correlation(f,g)
00345     ** to minimize the risk of cancellation.
00346     */
00347     if (st_lookup(table, (char *)entry, (char **)&dummy)) {
00348         min = *dummy;
00349         FREE(entry);
00350         return(min);
00351     }
00352 
00353     G = Cudd_Regular(g);
00354     topF = cuddI(dd,f->index); topG = cuddI(dd,G->index);
00355     if (topF <= topG) {
00356         Fv = cuddT(f); Fnv = cuddE(f);
00357         index = f->index;
00358     } else {
00359         Fv = Fnv = f;
00360         index = G->index;
00361     }
00362     if (topG <= topF) { Gv = cuddT(G); Gnv = cuddE(G); } else { Gv = Gnv = G; }
00363 
00364     if (g != G) {
00365         Gv = Cudd_Not(Gv);
00366         Gnv = Cudd_Not(Gnv);
00367     }
00368 
00369     min1 = bddCorrelationWeightsAux(dd, Fv, Gv, prob, table) * prob[index];
00370     if (min1 == (double)CUDD_OUT_OF_MEM) {
00371         FREE(entry);
00372         return((double)CUDD_OUT_OF_MEM);
00373     }
00374     min2 = bddCorrelationWeightsAux(dd, Fnv, Gnv, prob, table) * (1.0 - prob[index]); 
00375     if (min2 == (double)CUDD_OUT_OF_MEM) {
00376         FREE(entry);
00377         return((double)CUDD_OUT_OF_MEM);
00378     }
00379     min = (min1+min2);
00380     
00381     pmin = ALLOC(double,1);
00382     if (pmin == NULL) {
00383         dd->errorCode = CUDD_MEMORY_OUT;
00384         return((double)CUDD_OUT_OF_MEM);
00385     }
00386     *pmin = min;
00387 
00388     if (st_insert(table,(char *)entry, (char *)pmin) == ST_OUT_OF_MEM) {
00389         FREE(entry);
00390         FREE(pmin);
00391         return((double)CUDD_OUT_OF_MEM);
00392     }
00393     return(min);
00394 
00395 } /* end of bddCorrelationWeightsAux */

static enum st_retval CorrelCleanUp ( char *  key,
char *  value,
char *  arg 
) [static]

Function********************************************************************

Synopsis [Frees memory associated with hash table.]

Description [Frees memory associated with hash table. Returns ST_CONTINUE.]

SideEffects [None]

Definition at line 466 of file cuddBddCorr.c.

00470 {
00471     double      *d;
00472     HashEntry *entry;
00473 
00474     entry = (HashEntry *) key;
00475     FREE(entry);
00476     d = (double *)value;
00477     FREE(d);
00478     return ST_CONTINUE;
00479 
00480 } /* end of CorrelCleanUp */

static int CorrelCompare ( const char *  key1,
const char *  key2 
) [static]

Function********************************************************************

Synopsis [Compares two hash table entries.]

Description [Compares two hash table entries. Returns 0 if they are identical; 1 otherwise.]

SideEffects [None]

Definition at line 409 of file cuddBddCorr.c.

00412 {
00413     HashEntry *entry1;
00414     HashEntry *entry2;
00415 
00416     entry1 = (HashEntry *) key1;
00417     entry2 = (HashEntry *) key2;
00418     if (entry1->f != entry2->f || entry1->g != entry2->g) return(1);
00419 
00420     return(0);
00421 
00422 } /* end of CorrelCompare */

static int CorrelHash ( char *  key,
int  modulus 
) [static]

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]

Definition at line 436 of file cuddBddCorr.c.

00439 {
00440     HashEntry *entry;
00441     int val = 0;
00442 
00443     entry = (HashEntry *) key;
00444 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
00445     val = ((int) ((long)entry->f))*997 + ((int) ((long)entry->g));
00446 #else
00447     val = ((int) entry->f)*997 + ((int) entry->g);
00448 #endif
00449 
00450     return ((val < 0) ? -val : val) % modulus;
00451 
00452 } /* end of CorrelHash */

double Cudd_bddCorrelation ( DdManager *  manager,
DdNode *  f,
DdNode *  g 
)

AutomaticEnd 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]

Definition at line 109 of file cuddBddCorr.c.

00113 {
00114 
00115     st_table    *table;
00116     double      correlation;
00117 
00118 #ifdef CORREL_STATS
00119     num_calls = 0;
00120 #endif
00121 
00122     table = st_init_table(CorrelCompare,CorrelHash);
00123     if (table == NULL) return((double)CUDD_OUT_OF_MEM);
00124     correlation = bddCorrelationAux(manager,f,g,table);
00125     st_foreach(table, CorrelCleanUp, NIL(char));
00126     st_free_table(table);
00127     return(correlation);
00128 
00129 } /* end of Cudd_bddCorrelation */

double Cudd_bddCorrelationWeights ( DdManager *  manager,
DdNode *  f,
DdNode *  g,
double *  prob 
)

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]

Definition at line 151 of file cuddBddCorr.c.

00156 {
00157 
00158     st_table    *table;
00159     double      correlation;
00160 
00161 #ifdef CORREL_STATS
00162     num_calls = 0;
00163 #endif
00164 
00165     table = st_init_table(CorrelCompare,CorrelHash);
00166     if (table == NULL) return((double)CUDD_OUT_OF_MEM);
00167     correlation = bddCorrelationWeightsAux(manager,f,g,prob,table);
00168     st_foreach(table, CorrelCleanUp, NIL(char));
00169     st_free_table(table);
00170     return(correlation);
00171 
00172 } /* end of Cudd_bddCorrelationWeights */

Variable Documentation

char rcsid [] DD_UNUSED = "$Id: cuddBddCorr.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $" [static]

Definition at line 62 of file cuddBddCorr.c.

Generated on Tue Jan 5 12:18:53 2010 for abc70930 by  doxygen 1.6.1