src/cuBdd/cuddBddCorr.c

Go to the documentation of this file.

#include "util.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.14 2004/08/13 18:04:46 fabio Exp $";
#endif

#ifdef CORREL_STATS
static  int     num_calls;
#endif

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

#ifdef __cplusplus
extern "C" {
#endif

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

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);

#ifdef __cplusplus
}
#endif


/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/


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 */


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                                            */
/*---------------------------------------------------------------------------*/


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, entry, &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 */


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, entry, &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 */


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 */


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 */


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 */

---