diff --git a/buddy/ChangeLog b/buddy/ChangeLog index 87390ac00..8cca2b739 100644 --- a/buddy/ChangeLog +++ b/buddy/ChangeLog @@ -1,3 +1,7 @@ +2011-08-27 Alexandre Duret-Lutz + + * src/bddop.c (bdd_support): Speedup using a cache. + 2011-06-10 Alexandre Duret-Lutz * src/bddop.c (apply_rec, appquant_rec): Improve caching by diff --git a/buddy/src/bddop.c b/buddy/src/bddop.c index ee09f0ff2..395c568a2 100644 --- a/buddy/src/bddop.c +++ b/buddy/src/bddop.c @@ -50,6 +50,7 @@ #define CACHEID_SATCOULN 0x3 #define CACHEID_PATHCOU 0x4 #define CACHEID_SETXOR 0x5 +#define CACHEID_SUPPORT 0x6 /* Hash value modifiers for replace/compose */ #define CACHEID_REPLACE 0x0 @@ -166,6 +167,7 @@ static int varset2svartable(BDD); #define COMPOSEHASH(f,g) (PAIR(f,g)) #define SATCOUHASH(r) (r) #define PATHCOUHASH(r) (r) +#define SUPPORTHASH(r) (PAIR(r,CACHEID_SUPPORT)) #define APPEXHASH(l,r,op) (PAIR(l,r)) #ifndef M_LN2 @@ -2303,6 +2305,7 @@ RETURN {* A BDD variable set. *} */ BDD bdd_support(BDD r) { + BddCacheData *entry; static int supportSize = 0; int n; int res=1; @@ -2313,6 +2316,18 @@ BDD bdd_support(BDD r) if (r < 2) return bddtrue; + entry = BddCache_lookup(&misccache, SUPPORTHASH(r)); + if (entry->a == r && entry->c == CACHEID_SUPPORT) + { +#ifdef CACHESTATS + bddcachestats.opHit++; +#endif + return entry->r.res; + } +#ifdef CACHESTATS + bddcachestats.opMiss++; +#endif + /* On-demand allocation of support set */ if (__unlikely(supportSize < bddvarnum)) { @@ -2361,6 +2376,10 @@ BDD bdd_support(BDD r) bdd_enable_reorder(); + entry->a = r; + entry->c = CACHEID_SUPPORT; + entry->r.res = res; + return res; }