diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-02-13 13:42:25 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-02-13 13:42:25 -0800 |
commit | e7b544f11151f09a4a3fbe39b4a176795a82f677 (patch) | |
tree | a6cbbeb138c9bfe5b2554a5838124ffc3a6c0a5b /src/bdd/cudd/cuddBddCorr.c | |
parent | d99de60e6c88e5f6157b1d5c9b25cfd5d08a1c9a (diff) | |
download | abc-e7b544f11151f09a4a3fbe39b4a176795a82f677.tar.gz abc-e7b544f11151f09a4a3fbe39b4a176795a82f677.tar.bz2 abc-e7b544f11151f09a4a3fbe39b4a176795a82f677.zip |
Upgrade to the latest CUDD 2.4.2.
Diffstat (limited to 'src/bdd/cudd/cuddBddCorr.c')
-rw-r--r-- | src/bdd/cudd/cuddBddCorr.c | 205 |
1 files changed, 121 insertions, 84 deletions
diff --git a/src/bdd/cudd/cuddBddCorr.c b/src/bdd/cudd/cuddBddCorr.c index f3f017b0..32d5d97c 100644 --- a/src/bdd/cudd/cuddBddCorr.c +++ b/src/bdd/cudd/cuddBddCorr.c @@ -7,26 +7,53 @@ Synopsis [Correlation between BDDs.] Description [External procedures included in this module: - <ul> - <li> Cudd_bddCorrelation() - <li> Cudd_bddCorrelationWeights() - </ul> - Static procedures included in this module: - <ul> - <li> bddCorrelationAux() - <li> bddCorrelationWeightsAux() - <li> CorrelCompare() - <li> CorrelHash() - <li> CorrelCleanUp() - </ul> - ] + <ul> + <li> Cudd_bddCorrelation() + <li> Cudd_bddCorrelationWeights() + </ul> + Static procedures included in this module: + <ul> + <li> bddCorrelationAux() + <li> bddCorrelationWeightsAux() + <li> CorrelCompare() + <li> CorrelHash() + <li> CorrelCleanUp() + </ul> + ] Author [Fabio Somenzi] - Copyright [This file was created at the University of Colorado at - Boulder. The University of Colorado at Boulder makes no warranty - about the suitability of this software for any purpose. It is - presented on an AS IS basis.] + 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.] ******************************************************************************/ @@ -37,6 +64,7 @@ ABC_NAMESPACE_IMPL_START + /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ @@ -62,17 +90,20 @@ typedef struct hashEntry { /*---------------------------------------------------------------------------*/ #ifndef lint -static char rcsid[] DD_UNUSED = "$Id: cuddBddCorr.c,v 1.1.1.1 2003/02/24 22:23:51 wjiang Exp $"; +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; +static int num_calls; #endif /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ +#ifdef __cplusplus +extern "C" { +#endif /**AutomaticStart*************************************************************/ @@ -80,14 +111,18 @@ static int num_calls; /* Static function prototypes */ /*---------------------------------------------------------------------------*/ -static double bddCorrelationAux ARGS((DdManager *dd, DdNode *f, DdNode *g, st_table *table)); -static double bddCorrelationWeightsAux ARGS((DdManager *dd, DdNode *f, DdNode *g, double *prob, st_table *table)); -static int CorrelCompare ARGS((const char *key1, const char *key2)); -static int CorrelHash ARGS((const char *key, int modulus)); -static enum st_retval CorrelCleanUp ARGS((char *key, char *value, char *arg)); +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 (const char *key, int modulus); +static enum st_retval CorrelCleanUp (char *key, char *value, char *arg); /**AutomaticEnd***************************************************************/ +#ifdef __cplusplus +} +#endif + /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ @@ -116,7 +151,7 @@ Cudd_bddCorrelation( { st_table *table; - double correlation; + double correlation; #ifdef CORREL_STATS num_calls = 0; @@ -125,7 +160,7 @@ Cudd_bddCorrelation( table = st_init_table(CorrelCompare,CorrelHash); if (table == NULL) return((double)CUDD_OUT_OF_MEM); correlation = bddCorrelationAux(manager,f,g,table); - st_foreach(table, (ST_PFSR)CorrelCleanUp, NIL(char)); + st_foreach(table, CorrelCleanUp, NIL(char)); st_free_table(table); return(correlation); @@ -159,7 +194,7 @@ Cudd_bddCorrelationWeights( { st_table *table; - double correlation; + double correlation; #ifdef CORREL_STATS num_calls = 0; @@ -168,7 +203,7 @@ Cudd_bddCorrelationWeights( 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, (ST_PFSR)CorrelCleanUp, NIL(char)); + st_foreach(table, CorrelCleanUp, NIL(char)); st_free_table(table); return(correlation); @@ -205,9 +240,9 @@ bddCorrelationAux( DdNode * g, st_table * table) { - DdNode *Fv, *Fnv, *G, *Gv, *Gnv; - double min, *pmin, min1, min2, *dummy; - HashEntry *entry; + DdNode *Fv, *Fnv, *G, *Gv, *Gnv; + double min, *pmin, min1, min2, *dummy; + HashEntry *entry; unsigned int topF, topG; statLine(dd); @@ -224,19 +259,19 @@ bddCorrelationAux( ** (f' EXNOR g') = (f EXNOR g). */ if (f > g) { - DdNode *tmp = f; - f = g; g = tmp; + DdNode *tmp = f; + f = g; g = tmp; } if (Cudd_IsComplement(f)) { - f = Cudd_Not(f); - g = Cudd_Not(g); + f = Cudd_Not(f); + g = Cudd_Not(g); } /* From now on, f is regular. */ entry = ABC_ALLOC(HashEntry,1); if (entry == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - return(CUDD_OUT_OF_MEM); + dd->errorCode = CUDD_MEMORY_OUT; + return(CUDD_OUT_OF_MEM); } entry->f = f; entry->g = g; @@ -244,10 +279,10 @@ bddCorrelationAux( ** correlation(f,g') = 1 - correlation(f,g) ** to minimize the risk of cancellation. */ - if (st_lookup(table, (char *)entry, (char **)&dummy)) { - min = *dummy; - ABC_FREE(entry); - return(min); + if (st_lookup(table, (const char *)entry, (char **)&dummy)) { + min = *dummy; + ABC_FREE(entry); + return(min); } G = Cudd_Regular(g); @@ -256,33 +291,33 @@ bddCorrelationAux( if (topG <= topF) { Gv = cuddT(G); Gnv = cuddE(G); } else { Gv = Gnv = G; } if (g != G) { - Gv = Cudd_Not(Gv); - Gnv = Cudd_Not(Gnv); + Gv = Cudd_Not(Gv); + Gnv = Cudd_Not(Gnv); } min1 = bddCorrelationAux(dd, Fv, Gv, table) / 2.0; if (min1 == (double)CUDD_OUT_OF_MEM) { - ABC_FREE(entry); - return(CUDD_OUT_OF_MEM); + ABC_FREE(entry); + return(CUDD_OUT_OF_MEM); } min2 = bddCorrelationAux(dd, Fnv, Gnv, table) / 2.0; if (min2 == (double)CUDD_OUT_OF_MEM) { - ABC_FREE(entry); - return(CUDD_OUT_OF_MEM); + ABC_FREE(entry); + return(CUDD_OUT_OF_MEM); } min = (min1+min2); pmin = ABC_ALLOC(double,1); if (pmin == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - return((double)CUDD_OUT_OF_MEM); + 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) { - ABC_FREE(entry); - ABC_FREE(pmin); - return((double)CUDD_OUT_OF_MEM); + ABC_FREE(entry); + ABC_FREE(pmin); + return((double)CUDD_OUT_OF_MEM); } return(min); @@ -308,10 +343,10 @@ bddCorrelationWeightsAux( double * prob, st_table * table) { - DdNode *Fv, *Fnv, *G, *Gv, *Gnv; - double min, *pmin, min1, min2, *dummy; - HashEntry *entry; - int topF, topG, index; + DdNode *Fv, *Fnv, *G, *Gv, *Gnv; + double min, *pmin, min1, min2, *dummy; + HashEntry *entry; + int topF, topG, index; statLine(dd); #ifdef CORREL_STATS @@ -327,19 +362,19 @@ bddCorrelationWeightsAux( ** (f' EXNOR g') = (f EXNOR g). */ if (f > g) { - DdNode *tmp = f; - f = g; g = tmp; + DdNode *tmp = f; + f = g; g = tmp; } if (Cudd_IsComplement(f)) { - f = Cudd_Not(f); - g = Cudd_Not(g); + f = Cudd_Not(f); + g = Cudd_Not(g); } /* From now on, f is regular. */ entry = ABC_ALLOC(HashEntry,1); if (entry == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - return((double)CUDD_OUT_OF_MEM); + dd->errorCode = CUDD_MEMORY_OUT; + return((double)CUDD_OUT_OF_MEM); } entry->f = f; entry->g = g; @@ -347,51 +382,51 @@ bddCorrelationWeightsAux( ** correlation(f,g') = 1 - correlation(f,g) ** to minimize the risk of cancellation. */ - if (st_lookup(table, (char *)entry, (char **)&dummy)) { - min = *dummy; - ABC_FREE(entry); - return(min); + if (st_lookup(table, (const char *)entry, (char **)&dummy)) { + min = *dummy; + ABC_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; + Fv = cuddT(f); Fnv = cuddE(f); + index = f->index; } else { - Fv = Fnv = f; - index = G->index; + 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); + Gv = Cudd_Not(Gv); + Gnv = Cudd_Not(Gnv); } min1 = bddCorrelationWeightsAux(dd, Fv, Gv, prob, table) * prob[index]; if (min1 == (double)CUDD_OUT_OF_MEM) { - ABC_FREE(entry); - return((double)CUDD_OUT_OF_MEM); + ABC_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) { - ABC_FREE(entry); - return((double)CUDD_OUT_OF_MEM); + ABC_FREE(entry); + return((double)CUDD_OUT_OF_MEM); } min = (min1+min2); pmin = ABC_ALLOC(double,1); if (pmin == NULL) { - dd->errorCode = CUDD_MEMORY_OUT; - return((double)CUDD_OUT_OF_MEM); + 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) { - ABC_FREE(entry); - ABC_FREE(pmin); - return((double)CUDD_OUT_OF_MEM); + ABC_FREE(entry); + ABC_FREE(pmin); + return((double)CUDD_OUT_OF_MEM); } return(min); @@ -440,10 +475,10 @@ CorrelHash( const char * key, int modulus) { - const HashEntry *entry; + HashEntry *entry; int val = 0; - entry = (const HashEntry *) key; + entry = (HashEntry *) key; #if SIZEOF_VOID_P == 8 && SIZEOF_INT == 4 val = ((int) ((long)entry->f))*997 + ((int) ((long)entry->g)); #else @@ -471,7 +506,7 @@ CorrelCleanUp( char * value, char * arg) { - double *d; + double *d; HashEntry *entry; entry = (HashEntry *) key; @@ -482,5 +517,7 @@ CorrelCleanUp( } /* end of CorrelCleanUp */ + ABC_NAMESPACE_IMPL_END + |