alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

[buddy] avoid cache errors in bdd_satcount() and friends

Browse source 
* src/bddop.c (bdd_satcount, bdd_satcountln): If the number of
declared variables changed since we last used it, reset misccache.
Otherwise, bdd_satcount() and friends might return incorrect results
after the number of variable is changed.  These is needed for the next
patch in Spot to pass all tests.
(misccache_varnum): New global variable to track that.
(bdd_satcountset): Make sure that bdd_satcountset(bddtrue, bddtrue)
return 1.0 and not 0.0.
This commit is contained in:
Alexandre Duret-Lutz 2020-05-18 19:25:14 +02:00
parent 66aa6d0883
commit da96a509e9
1 changed files with 24 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

27
buddy/src/bddop.c
View file

@ -125,6 +125,7 @@ static BddCache quantcache; /* Cache for exist/forall results */
static BddCache appexcache; /* Cache for appex/appall results */ static BddCache appexcache; /* Cache for appex/appall results */
static BddCache replacecache; /* Cache for replace results */ static BddCache replacecache; /* Cache for replace results */
static BddCache misccache; /* Cache for other results */ static BddCache misccache; /* Cache for other results */
static int misccache_varnum; /* if this changes, invalidate misccache */
static int cacheratio; static int cacheratio;
static BDD satPolarity; static BDD satPolarity;
static int firstReorder; /* Used instead of local variable in order static int firstReorder; /* Used instead of local variable in order
@ -214,6 +215,7 @@ int bdd_operator_init(int cachesize)
if (BddCache_init(&misccache,cachesize) < 0) if (BddCache_init(&misccache,cachesize) < 0)
return bdd_error(BDD_MEMORY); return bdd_error(BDD_MEMORY);
misccache_varnum = bddvarnum;
quantvarsetID = 0; quantvarsetID = 0;
quantvarset = NULL; quantvarset = NULL;
@ -249,6 +251,7 @@ void bdd_operator_reset(void)
BddCache_reset(&appexcache); BddCache_reset(&appexcache);
BddCache_reset(&replacecache); BddCache_reset(&replacecache);
BddCache_reset(&misccache); BddCache_reset(&misccache);
misccache_varnum = bddvarnum;
} }
@ -2805,6 +2808,14 @@ double bdd_satcount(BDD r)
CHECKa(r, 0.0); CHECKa(r, 0.0);
// Invalidate misccache if the number of variable changed since we
// last used it.
if (misccache_varnum != bddvarnum)
{
BddCache_reset(&misccache);
misccache_varnum = bddvarnum;
}
miscid = CACHEID_SATCOU; miscid = CACHEID_SATCOU;
size = pow(2.0, (double)LEVEL(r)); size = pow(2.0, (double)LEVEL(r));
@ -2817,8 +2828,10 @@ double bdd_satcountset(BDD r, BDD varset)
double unused = bddvarnum; double unused = bddvarnum;
BDD n; BDD n;
if (ISCONST(varset) || ISZERO(r)) /* empty set */ if (ISZERO(r))
return 0.0; return 0.0;
if (ISCONST(varset)) /* empty set */
return ISONE(r) ? 1.0 : 0.0;
for (n=varset ; !ISCONST(n) ; n=HIGH(n)) for (n=varset ; !ISCONST(n) ; n=HIGH(n))
unused--; unused--;
@ -2839,7 +2852,7 @@ static double satcount_rec(int root)
return root; return root;
entry = BddCache_lookup(&misccache, SATCOUHASH(root)); entry = BddCache_lookup(&misccache, SATCOUHASH(root));
if (entry->d.a == root && entry->d.c == miscid) if (entry->d.a == root && entry->d.c == miscid)
return entry->d.res; return entry->d.res;
node = &bddnodes[root]; node = &bddnodes[root];
@ -2886,6 +2899,14 @@ double bdd_satcountln(BDD r)
CHECKa(r, 0.0); CHECKa(r, 0.0);
// Invalidate misccache if the number of variable changed since we
// last used it.
if (misccache_varnum != bddvarnum)
{
BddCache_reset(&misccache);
misccache_varnum = bddvarnum;
}
miscid = CACHEID_SATCOULN; miscid = CACHEID_SATCOULN;
size = satcountln_rec(r); size = satcountln_rec(r);