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