distr/cudd/cuddBddCorr.c

   1 /**CFile***********************************************************************
   2
   3   FileName    [cuddBddCorr.c]
   4
   5   PackageName [cudd]
   6
   7   Synopsis    [Correlation between BDDs.]
   8
   9   Description [External procedures included in this module:
  10                 <ul>
  11                 <li> Cudd_bddCorrelation()
  12                 <li> Cudd_bddCorrelationWeights()
  13                 </ul>
  14             Static procedures included in this module:
  15                 <ul>
  16                 <li> bddCorrelationAux()
  17                 <li> bddCorrelationWeightsAux()
  18                 <li> CorrelCompare()
  19                 <li> CorrelHash()
  20                 <li> CorrelCleanUp()
  21                 </ul>
  22                 ]
  23
  24   Author      [Fabio Somenzi]
  25
  26   Copyright   [Copyright (c) 1995-2004, Regents of the University of Colorado
  27
  28   All rights reserved.
  29
  30   Redistribution and use in source and binary forms, with or without
  31   modification, are permitted provided that the following conditions
  32   are met:
  33
  34   Redistributions of source code must retain the above copyright
  35   notice, this list of conditions and the following disclaimer.
  36
  37   Redistributions in binary form must reproduce the above copyright
  38   notice, this list of conditions and the following disclaimer in the
  39   documentation and/or other materials provided with the distribution.
  40
  41   Neither the name of the University of Colorado nor the names of its
  42   contributors may be used to endorse or promote products derived from
  43   this software without specific prior written permission.
  44
  45   THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  46   "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  47   LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  48   FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  49   COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  50   INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  51   BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  52   LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  53   CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  54   LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  55   ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  56   POSSIBILITY OF SUCH DAMAGE.]
  57
  58 ******************************************************************************/
  59
  60 #include "util.h"
  61 #include "cuddInt.h"
  62
  63
  64 /*---------------------------------------------------------------------------*/
  65 /* Constant declarations                                                     */
  66 /*---------------------------------------------------------------------------*/
  67
  68
  69 /*---------------------------------------------------------------------------*/
  70 /* Stucture declarations                                                     */
  71 /*---------------------------------------------------------------------------*/
  72
  73
  74 /*---------------------------------------------------------------------------*/
  75 /* Type declarations                                                         */
  76 /*---------------------------------------------------------------------------*/
  77
  78 typedef struct hashEntry {
  79     DdNode *f;
  80     DdNode *g;
  81 } HashEntry;
  82
  83
  84 /*---------------------------------------------------------------------------*/
  85 /* Variable declarations                                                     */
  86 /*---------------------------------------------------------------------------*/
  87
  88 #ifndef lint
  89 static char rcsid[] DD_UNUSED = "$Id: cuddBddCorr.c,v 1.14 2004/08/13 18:04:46 fabio Exp $";
  90 #endif
  91
  92 #ifdef CORREL_STATS
  93 static  int     num_calls;
  94 #endif
  95
  96 /*---------------------------------------------------------------------------*/
  97 /* Macro declarations                                                        */
  98 /*---------------------------------------------------------------------------*/
  99
 100 #ifdef __cplusplus
 101 extern "C" {
 102 #endif
 103
 104 /**AutomaticStart*************************************************************/
 105
 106 /*---------------------------------------------------------------------------*/
 107 /* Static function prototypes                                                */
 108 /*---------------------------------------------------------------------------*/
 109
 110 static double bddCorrelationAux (DdManager *dd, DdNode *f, DdNode *g, st_table *table);
 111 static double bddCorrelationWeightsAux (DdManager *dd, DdNode *f, DdNode *g, double *prob, st_table *table);
 112 static int CorrelCompare (const char *key1, const char *key2);
 113 static int CorrelHash (char *key, int modulus);
 114 static enum st_retval CorrelCleanUp (char *key, char *value, char *arg);
 115
 116 /**AutomaticEnd***************************************************************/
 117
 118 #ifdef __cplusplus
 119 }
 120 #endif
 121
 122
 123 /*---------------------------------------------------------------------------*/
 124 /* Definition of exported functions                                          */
 125 /*---------------------------------------------------------------------------*/
 126
 127
 128 /**Function********************************************************************
 129
 130   Synopsis    [Computes the correlation of f and g.]
 131
 132   Description [Computes the correlation of f and g. If f == g, their
 133   correlation is 1. If f == g', their correlation is 0.  Returns the
 134   fraction of minterms in the ON-set of the EXNOR of f and g.  If it
 135   runs out of memory, returns (double)CUDD_OUT_OF_MEM.]
 136
 137   SideEffects [None]
 138
 139   SeeAlso     [Cudd_bddCorrelationWeights]
 140
 141 ******************************************************************************/
 142 double
 143 Cudd_bddCorrelation(
 144   DdManager * manager,
 145   DdNode * f,
 146   DdNode * g)
 147 {
 148
 149     st_table    *table;
 150     double      correlation;
 151
 152 #ifdef CORREL_STATS
 153     num_calls = 0;
 154 #endif
 155
 156     table = st_init_table(CorrelCompare,CorrelHash);
 157     if (table == NULL) return((double)CUDD_OUT_OF_MEM);
 158     correlation = bddCorrelationAux(manager,f,g,table);
 159     st_foreach(table, CorrelCleanUp, NIL(char));
 160     st_free_table(table);
 161     return(correlation);
 162
 163 } /* end of Cudd_bddCorrelation */
 164
 165
 166 /**Function********************************************************************
 167
 168   Synopsis    [Computes the correlation of f and g for given input
 169   probabilities.]
 170
 171   Description [Computes the correlation of f and g for given input
 172   probabilities. On input, prob\[i\] is supposed to contain the
 173   probability of the i-th input variable to be 1.
 174   If f == g, their correlation is 1. If f == g', their
 175   correlation is 0.  Returns the probability that f and g have the same
 176   value. If it runs out of memory, returns (double)CUDD_OUT_OF_MEM. The
 177   correlation of f and the constant one gives the probability of f.]
 178
 179   SideEffects [None]
 180
 181   SeeAlso     [Cudd_bddCorrelation]
 182
 183 ******************************************************************************/
 184 double
 185 Cudd_bddCorrelationWeights(
 186   DdManager * manager,
 187   DdNode * f,
 188   DdNode * g,
 189   double * prob)
 190 {
 191
 192     st_table    *table;
 193     double      correlation;
 194
 195 #ifdef CORREL_STATS
 196     num_calls = 0;
 197 #endif
 198
 199     table = st_init_table(CorrelCompare,CorrelHash);
 200     if (table == NULL) return((double)CUDD_OUT_OF_MEM);
 201     correlation = bddCorrelationWeightsAux(manager,f,g,prob,table);
 202     st_foreach(table, CorrelCleanUp, NIL(char));
 203     st_free_table(table);
 204     return(correlation);
 205
 206 } /* end of Cudd_bddCorrelationWeights */
 207
 208
 209 /*---------------------------------------------------------------------------*/
 210 /* Definition of internal functions                                          */
 211 /*---------------------------------------------------------------------------*/
 212
 213
 214 /*---------------------------------------------------------------------------*/
 215 /* Definition of static functions                                            */
 216 /*---------------------------------------------------------------------------*/
 217
 218
 219 /**Function********************************************************************
 220
 221   Synopsis    [Performs the recursive step of Cudd_bddCorrelation.]
 222
 223   Description [Performs the recursive step of Cudd_bddCorrelation.
 224   Returns the fraction of minterms in the ON-set of the EXNOR of f and
 225   g.]
 226
 227   SideEffects [None]
 228
 229   SeeAlso     [bddCorrelationWeightsAux]
 230
 231 ******************************************************************************/
 232 static double
 233 bddCorrelationAux(
 234   DdManager * dd,
 235   DdNode * f,
 236   DdNode * g,
 237   st_table * table)
 238 {
 239     DdNode      *Fv, *Fnv, *G, *Gv, *Gnv;
 240     double      min, *pmin, min1, min2, *dummy;
 241     HashEntry   *entry;
 242     unsigned int topF, topG;
 243
 244     statLine(dd);
 245 #ifdef CORREL_STATS
 246     num_calls++;
 247 #endif
 248
 249     /* Terminal cases: only work for BDDs. */
 250     if (f == g) return(1.0);
 251     if (f == Cudd_Not(g)) return(0.0);
 252
 253     /* Standardize call using the following properties:
 254     **     (f EXNOR g)   = (g EXNOR f)
 255     **     (f' EXNOR g') = (f EXNOR g).
 256     */
 257     if (f > g) {
 258         DdNode *tmp = f;
 259         f = g; g = tmp;
 260     }
 261     if (Cudd_IsComplement(f)) {
 262         f = Cudd_Not(f);
 263         g = Cudd_Not(g);
 264     }
 265     /* From now on, f is regular. */
 266
 267     entry = ALLOC(HashEntry,1);
 268     if (entry == NULL) {
 269         dd->errorCode = CUDD_MEMORY_OUT;
 270         return(CUDD_OUT_OF_MEM);
 271     }
 272     entry->f = f; entry->g = g;
 273
 274     /* We do not use the fact that
 275     ** correlation(f,g') = 1 - correlation(f,g)
 276     ** to minimize the risk of cancellation.
 277     */
 278     if (st_lookup(table, entry, &dummy)) {
 279         min = *dummy;
 280         FREE(entry);
 281         return(min);
 282     }
 283
 284     G = Cudd_Regular(g);
 285     topF = cuddI(dd,f->index); topG = cuddI(dd,G->index);
 286     if (topF <= topG) { Fv = cuddT(f); Fnv = cuddE(f); } else { Fv = Fnv = f; }
 287     if (topG <= topF) { Gv = cuddT(G); Gnv = cuddE(G); } else { Gv = Gnv = G; }
 288
 289     if (g != G) {
 290         Gv = Cudd_Not(Gv);
 291         Gnv = Cudd_Not(Gnv);
 292     }
 293
 294     min1 = bddCorrelationAux(dd, Fv, Gv, table) / 2.0;
 295     if (min1 == (double)CUDD_OUT_OF_MEM) {
 296         FREE(entry);
 297         return(CUDD_OUT_OF_MEM);
 298     }
 299     min2 = bddCorrelationAux(dd, Fnv, Gnv, table) / 2.0;
 300     if (min2 == (double)CUDD_OUT_OF_MEM) {
 301         FREE(entry);
 302         return(CUDD_OUT_OF_MEM);
 303     }
 304     min = (min1+min2);
 305
 306     pmin = ALLOC(double,1);
 307     if (pmin == NULL) {
 308         dd->errorCode = CUDD_MEMORY_OUT;
 309         return((double)CUDD_OUT_OF_MEM);
 310     }
 311     *pmin = min;
 312
 313     if (st_insert(table,(char *)entry, (char *)pmin) == ST_OUT_OF_MEM) {
 314         FREE(entry);
 315         FREE(pmin);
 316         return((double)CUDD_OUT_OF_MEM);
 317     }
 318     return(min);
 319
 320 } /* end of bddCorrelationAux */
 321
 322
 323 /**Function********************************************************************
 324
 325   Synopsis    [Performs the recursive step of Cudd_bddCorrelationWeigths.]
 326
 327   Description []
 328
 329   SideEffects [None]
 330
 331   SeeAlso     [bddCorrelationAux]
 332
 333 ******************************************************************************/
 334 static double
 335 bddCorrelationWeightsAux(
 336   DdManager * dd,
 337   DdNode * f,
 338   DdNode * g,
 339   double * prob,
 340   st_table * table)
 341 {
 342     DdNode      *Fv, *Fnv, *G, *Gv, *Gnv;
 343     double      min, *pmin, min1, min2, *dummy;
 344     HashEntry   *entry;
 345     int         topF, topG, index;
 346
 347     statLine(dd);
 348 #ifdef CORREL_STATS
 349     num_calls++;
 350 #endif
 351
 352     /* Terminal cases: only work for BDDs. */
 353     if (f == g) return(1.0);
 354     if (f == Cudd_Not(g)) return(0.0);
 355
 356     /* Standardize call using the following properties:
 357     **     (f EXNOR g)   = (g EXNOR f)
 358     **     (f' EXNOR g') = (f EXNOR g).
 359     */
 360     if (f > g) {
 361         DdNode *tmp = f;
 362         f = g; g = tmp;
 363     }
 364     if (Cudd_IsComplement(f)) {
 365         f = Cudd_Not(f);
 366         g = Cudd_Not(g);
 367     }
 368     /* From now on, f is regular. */
 369
 370     entry = ALLOC(HashEntry,1);
 371     if (entry == NULL) {
 372         dd->errorCode = CUDD_MEMORY_OUT;
 373         return((double)CUDD_OUT_OF_MEM);
 374     }
 375     entry->f = f; entry->g = g;
 376
 377     /* We do not use the fact that
 378     ** correlation(f,g') = 1 - correlation(f,g)
 379     ** to minimize the risk of cancellation.
 380     */
 381     if (st_lookup(table, entry, &dummy)) {
 382         min = *dummy;
 383         FREE(entry);
 384         return(min);
 385     }
 386
 387     G = Cudd_Regular(g);
 388     topF = cuddI(dd,f->index); topG = cuddI(dd,G->index);
 389     if (topF <= topG) {
 390         Fv = cuddT(f); Fnv = cuddE(f);
 391         index = f->index;
 392     } else {
 393         Fv = Fnv = f;
 394         index = G->index;
 395     }
 396     if (topG <= topF) { Gv = cuddT(G); Gnv = cuddE(G); } else { Gv = Gnv = G; }
 397
 398     if (g != G) {
 399         Gv = Cudd_Not(Gv);
 400         Gnv = Cudd_Not(Gnv);
 401     }
 402
 403     min1 = bddCorrelationWeightsAux(dd, Fv, Gv, prob, table) * prob[index];
 404     if (min1 == (double)CUDD_OUT_OF_MEM) {
 405         FREE(entry);
 406         return((double)CUDD_OUT_OF_MEM);
 407     }
 408     min2 = bddCorrelationWeightsAux(dd, Fnv, Gnv, prob, table) * (1.0 - prob[index]);
 409     if (min2 == (double)CUDD_OUT_OF_MEM) {
 410         FREE(entry);
 411         return((double)CUDD_OUT_OF_MEM);
 412     }
 413     min = (min1+min2);
 414
 415     pmin = ALLOC(double,1);
 416     if (pmin == NULL) {
 417         dd->errorCode = CUDD_MEMORY_OUT;
 418         return((double)CUDD_OUT_OF_MEM);
 419     }
 420     *pmin = min;
 421
 422     if (st_insert(table,(char *)entry, (char *)pmin) == ST_OUT_OF_MEM) {
 423         FREE(entry);
 424         FREE(pmin);
 425         return((double)CUDD_OUT_OF_MEM);
 426     }
 427     return(min);
 428
 429 } /* end of bddCorrelationWeightsAux */
 430
 431
 432 /**Function********************************************************************
 433
 434   Synopsis    [Compares two hash table entries.]
 435
 436   Description [Compares two hash table entries. Returns 0 if they are
 437   identical; 1 otherwise.]
 438
 439   SideEffects [None]
 440
 441 ******************************************************************************/
 442 static int
 443 CorrelCompare(
 444   const char * key1,
 445   const char * key2)
 446 {
 447     HashEntry *entry1;
 448     HashEntry *entry2;
 449
 450     entry1 = (HashEntry *) key1;
 451     entry2 = (HashEntry *) key2;
 452     if (entry1->f != entry2->f || entry1->g != entry2->g) return(1);
 453
 454     return(0);
 455
 456 } /* end of CorrelCompare */
 457
 458
 459 /**Function********************************************************************
 460
 461   Synopsis    [Hashes a hash table entry.]
 462
 463   Description [Hashes a hash table entry. It is patterned after
 464   st_strhash. Returns a value between 0 and modulus.]
 465
 466   SideEffects [None]
 467
 468 ******************************************************************************/
 469 static int
 470 CorrelHash(
 471   char * key,
 472   int  modulus)
 473 {
 474     HashEntry *entry;
 475     int val = 0;
 476
 477     entry = (HashEntry *) key;
 478 #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4
 479     val = ((int) ((long)entry->f))*997 + ((int) ((long)entry->g));
 480 #else
 481     val = ((int) entry->f)*997 + ((int) entry->g);
 482 #endif
 483
 484     return ((val < 0) ? -val : val) % modulus;
 485
 486 } /* end of CorrelHash */
 487
 488
 489 /**Function********************************************************************
 490
 491   Synopsis    [Frees memory associated with hash table.]
 492
 493   Description [Frees memory associated with hash table. Returns
 494   ST_CONTINUE.]
 495
 496   SideEffects [None]
 497
 498 ******************************************************************************/
 499 static enum st_retval
 500 CorrelCleanUp(
 501   char * key,
 502   char * value,
 503   char * arg)
 504 {
 505     double      *d;
 506     HashEntry *entry;
 507
 508     entry = (HashEntry *) key;
 509     FREE(entry);
 510     d = (double *)value;
 511     FREE(d);
 512     return ST_CONTINUE;
 513
 514 } /* end of CorrelCleanUp */
 515