src/cuBdd/cuddBddCorr.c File Reference

#include "util.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 (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)
double Cudd_bddCorrelation (DdManager *manager, DdNode *f, DdNode *g)
double Cudd_bddCorrelationWeights (DdManager *manager, DdNode *f, DdNode *g, double *prob)

Variables

static char rcsid[] DD_UNUSED = "$Id: cuddBddCorr.c,v 1.14 2004/08/13 18:04:46 fabio 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 [Copyright (c) 1995-2004, Regents of the University of Colorado

All rights reserved.

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.

Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.

Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]

Function Documentation

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

AutomaticStart

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 233 of file cuddBddCorr.c.

00238 {
00239     DdNode      *Fv, *Fnv, *G, *Gv, *Gnv;
00240     double      min, *pmin, min1, min2, *dummy;
00241     HashEntry   *entry;
00242     unsigned int topF, topG;
00243 
00244     statLine(dd);
00245 #ifdef CORREL_STATS
00246     num_calls++;
00247 #endif
00248 
00249     /* Terminal cases: only work for BDDs. */
00250     if (f == g) return(1.0);
00251     if (f == Cudd_Not(g)) return(0.0);
00252 
00253     /* Standardize call using the following properties:
00254     **     (f EXNOR g)   = (g EXNOR f)
00255     **     (f' EXNOR g') = (f EXNOR g).
00256     */
00257     if (f > g) {
00258         DdNode *tmp = f;
00259         f = g; g = tmp;
00260     }
00261     if (Cudd_IsComplement(f)) {
00262         f = Cudd_Not(f);
00263         g = Cudd_Not(g);
00264     }
00265     /* From now on, f is regular. */
00266     
00267     entry = ALLOC(HashEntry,1);
00268     if (entry == NULL) {
00269         dd->errorCode = CUDD_MEMORY_OUT;
00270         return(CUDD_OUT_OF_MEM);
00271     }
00272     entry->f = f; entry->g = g;
00273 
00274     /* We do not use the fact that
00275     ** correlation(f,g') = 1 - correlation(f,g)
00276     ** to minimize the risk of cancellation.
00277     */
00278     if (st_lookup(table, entry, &dummy)) {
00279         min = *dummy;
00280         FREE(entry);
00281         return(min);
00282     }
00283 
00284     G = Cudd_Regular(g);
00285     topF = cuddI(dd,f->index); topG = cuddI(dd,G->index);
00286     if (topF <= topG) { Fv = cuddT(f); Fnv = cuddE(f); } else { Fv = Fnv = f; }
00287     if (topG <= topF) { Gv = cuddT(G); Gnv = cuddE(G); } else { Gv = Gnv = G; }
00288 
00289     if (g != G) {
00290         Gv = Cudd_Not(Gv);
00291         Gnv = Cudd_Not(Gnv);
00292     }
00293 
00294     min1 = bddCorrelationAux(dd, Fv, Gv, table) / 2.0;
00295     if (min1 == (double)CUDD_OUT_OF_MEM) {
00296         FREE(entry);
00297         return(CUDD_OUT_OF_MEM);
00298     }
00299     min2 = bddCorrelationAux(dd, Fnv, Gnv, table) / 2.0; 
00300     if (min2 == (double)CUDD_OUT_OF_MEM) {
00301         FREE(entry);
00302         return(CUDD_OUT_OF_MEM);
00303     }
00304     min = (min1+min2);
00305     
00306     pmin = ALLOC(double,1);
00307     if (pmin == NULL) {
00308         dd->errorCode = CUDD_MEMORY_OUT;
00309         return((double)CUDD_OUT_OF_MEM);
00310     }
00311     *pmin = min;
00312 
00313     if (st_insert(table,(char *)entry, (char *)pmin) == ST_OUT_OF_MEM) {
00314         FREE(entry);
00315         FREE(pmin);
00316         return((double)CUDD_OUT_OF_MEM);
00317     }
00318     return(min);
00319 
00320 } /* 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 335 of file cuddBddCorr.c.

00341 {
00342     DdNode      *Fv, *Fnv, *G, *Gv, *Gnv;
00343     double      min, *pmin, min1, min2, *dummy;
00344     HashEntry   *entry;
00345     int         topF, topG, index;
00346 
00347     statLine(dd);
00348 #ifdef CORREL_STATS
00349     num_calls++;
00350 #endif
00351 
00352     /* Terminal cases: only work for BDDs. */
00353     if (f == g) return(1.0);
00354     if (f == Cudd_Not(g)) return(0.0);
00355 
00356     /* Standardize call using the following properties:
00357     **     (f EXNOR g)   = (g EXNOR f)
00358     **     (f' EXNOR g') = (f EXNOR g).
00359     */
00360     if (f > g) {
00361         DdNode *tmp = f;
00362         f = g; g = tmp;
00363     }
00364     if (Cudd_IsComplement(f)) {
00365         f = Cudd_Not(f);
00366         g = Cudd_Not(g);
00367     }
00368     /* From now on, f is regular. */
00369     
00370     entry = ALLOC(HashEntry,1);
00371     if (entry == NULL) {
00372         dd->errorCode = CUDD_MEMORY_OUT;
00373         return((double)CUDD_OUT_OF_MEM);
00374     }
00375     entry->f = f; entry->g = g;
00376 
00377     /* We do not use the fact that
00378     ** correlation(f,g') = 1 - correlation(f,g)
00379     ** to minimize the risk of cancellation.
00380     */
00381     if (st_lookup(table, entry, &dummy)) {
00382         min = *dummy;
00383         FREE(entry);
00384         return(min);
00385     }
00386 
00387     G = Cudd_Regular(g);
00388     topF = cuddI(dd,f->index); topG = cuddI(dd,G->index);
00389     if (topF <= topG) {
00390         Fv = cuddT(f); Fnv = cuddE(f);
00391         index = f->index;
00392     } else {
00393         Fv = Fnv = f;
00394         index = G->index;
00395     }
00396     if (topG <= topF) { Gv = cuddT(G); Gnv = cuddE(G); } else { Gv = Gnv = G; }
00397 
00398     if (g != G) {
00399         Gv = Cudd_Not(Gv);
00400         Gnv = Cudd_Not(Gnv);
00401     }
00402 
00403     min1 = bddCorrelationWeightsAux(dd, Fv, Gv, prob, table) * prob[index];
00404     if (min1 == (double)CUDD_OUT_OF_MEM) {
00405         FREE(entry);
00406         return((double)CUDD_OUT_OF_MEM);
00407     }
00408     min2 = bddCorrelationWeightsAux(dd, Fnv, Gnv, prob, table) * (1.0 - prob[index]); 
00409     if (min2 == (double)CUDD_OUT_OF_MEM) {
00410         FREE(entry);
00411         return((double)CUDD_OUT_OF_MEM);
00412     }
00413     min = (min1+min2);
00414     
00415     pmin = ALLOC(double,1);
00416     if (pmin == NULL) {
00417         dd->errorCode = CUDD_MEMORY_OUT;
00418         return((double)CUDD_OUT_OF_MEM);
00419     }
00420     *pmin = min;
00421 
00422     if (st_insert(table,(char *)entry, (char *)pmin) == ST_OUT_OF_MEM) {
00423         FREE(entry);
00424         FREE(pmin);
00425         return((double)CUDD_OUT_OF_MEM);
00426     }
00427     return(min);
00428 
00429 } /* 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 500 of file cuddBddCorr.c.

00504 {
00505     double      *d;
00506     HashEntry *entry;
00507 
00508     entry = (HashEntry *) key;
00509     FREE(entry);
00510     d = (double *)value;
00511     FREE(d);
00512     return ST_CONTINUE;
00513 
00514 } /* 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 443 of file cuddBddCorr.c.

00446 {
00447     HashEntry *entry1;
00448     HashEntry *entry2;
00449 
00450     entry1 = (HashEntry *) key1;
00451     entry2 = (HashEntry *) key2;
00452     if (entry1->f != entry2->f || entry1->g != entry2->g) return(1);
00453 
00454     return(0);
00455 
00456 } /* 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 470 of file cuddBddCorr.c.

00473 {
00474     HashEntry *entry;
00475     int val = 0;
00476 
00477     entry = (HashEntry *) key;
00478 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
00479     val = ((int) ((long)entry->f))*997 + ((int) ((long)entry->g));
00480 #else
00481     val = ((int) entry->f)*997 + ((int) entry->g);
00482 #endif
00483 
00484     return ((val < 0) ? -val : val) % modulus;
00485 
00486 } /* 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 143 of file cuddBddCorr.c.

00147 {
00148 
00149     st_table    *table;
00150     double      correlation;
00151 
00152 #ifdef CORREL_STATS
00153     num_calls = 0;
00154 #endif
00155 
00156     table = st_init_table(CorrelCompare,CorrelHash);
00157     if (table == NULL) return((double)CUDD_OUT_OF_MEM);
00158     correlation = bddCorrelationAux(manager,f,g,table);
00159     st_foreach(table, CorrelCleanUp, NIL(char));
00160     st_free_table(table);
00161     return(correlation);
00162 
00163 } /* 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 185 of file cuddBddCorr.c.

00190 {
00191 
00192     st_table    *table;
00193     double      correlation;
00194 
00195 #ifdef CORREL_STATS
00196     num_calls = 0;
00197 #endif
00198 
00199     table = st_init_table(CorrelCompare,CorrelHash);
00200     if (table == NULL) return((double)CUDD_OUT_OF_MEM);
00201     correlation = bddCorrelationWeightsAux(manager,f,g,prob,table);
00202     st_foreach(table, CorrelCleanUp, NIL(char));
00203     st_free_table(table);
00204     return(correlation);
00205 
00206 } /* end of Cudd_bddCorrelationWeights */

Variable Documentation

char rcsid [] DD_UNUSED = "$Id: cuddBddCorr.c,v 1.14 2004/08/13 18:04:46 fabio Exp $" [static]

Definition at line 89 of file cuddBddCorr.c.

Generated on Tue Jan 12 13:57:18 2010 for glu-2.2 by  doxygen 1.6.1