* src/bddop.c (bdd_support): Speedup using a cache.
This commit is contained in:
parent
d9fc75e94e
commit
24be6076f6
2 changed files with 23 additions and 0 deletions
|
|
@ -1,3 +1,7 @@
|
|||
2011-08-27 Alexandre Duret-Lutz <adl@lrde.epita.fr>
|
||||
|
||||
* src/bddop.c (bdd_support): Speedup using a cache.
|
||||
|
||||
2011-06-10 Alexandre Duret-Lutz <adl@lrde.epita.fr>
|
||||
|
||||
* src/bddop.c (apply_rec, appquant_rec): Improve caching by
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
}
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue