source: vis_dev/glu-2.3/src/cuBdd/cuddBddCorr.c @ 21

Last change on this file since 21 was 13, checked in by cecile, 14 years ago

library glu 2.3
File size: 14.2 KB
Line 
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
78typedef struct hashEntry {
79    DdNode *f;
80    DdNode *g;
81} HashEntry;
82
83
84/*---------------------------------------------------------------------------*/
85/* Variable declarations                                                     */
86/*---------------------------------------------------------------------------*/
87
88#ifndef lint
89static 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
93static  int     num_calls;
94#endif
95
96/*---------------------------------------------------------------------------*/
97/* Macro declarations                                                        */
98/*---------------------------------------------------------------------------*/
99
100#ifdef __cplusplus
101extern "C" {
102#endif
103
104/**AutomaticStart*************************************************************/
105
106/*---------------------------------------------------------------------------*/
107/* Static function prototypes                                                */
108/*---------------------------------------------------------------------------*/
109
110static double bddCorrelationAux (DdManager *dd, DdNode *f, DdNode *g, st_table *table);
111static double bddCorrelationWeightsAux (DdManager *dd, DdNode *f, DdNode *g, double *prob, st_table *table);
112static int CorrelCompare (const char *key1, const char *key2);
113static int CorrelHash (char *key, int modulus);
114static 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******************************************************************************/
142double
143Cudd_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******************************************************************************/
184double
185Cudd_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******************************************************************************/
232static double
233bddCorrelationAux(
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******************************************************************************/
334static double
335bddCorrelationWeightsAux(
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******************************************************************************/
442static int
443CorrelCompare(
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******************************************************************************/
469static int
470CorrelHash(
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******************************************************************************/
499static enum st_retval
500CorrelCleanUp(
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
Note: See TracBrowser for help on using the repository browser.