Skip to content

#75 Fix cache cleanup + enable FLUSH_CACHE_ON_GC by default #76

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 3 commits into from
Aug 7, 2025
Merged

#75 Fix cache cleanup + enable FLUSH_CACHE_ON_GC by default #76

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
0983498
com-github-javabdd#75 Rewrote itecache table cleanup
wytseoortwijn Aug 6, 2025
a98a38a
com-github-javabdd#75 Removed old cleanup method
wytseoortwijn Aug 6, 2025
c6d5031
com-github-javabdd#75 Disabling cache flushing by default
wytseoortwijn Aug 6, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
60 changes: 49 additions & 11 deletions src/main/java/com/github/javabdd/JFactory.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ public class JFactory extends BDDFactoryIntImpl {
* Flush the operation cache on every garbage collection. If this is false, we only clean the collected entries on
* every GC, rather than emptying the whole cache. For most problems, you should keep this set to true.
*/
public static boolean FLUSH_CACHE_ON_GC = true;
public static boolean FLUSH_CACHE_ON_GC = false;

static final boolean VERIFY_ASSERTIONS = false;

Expand Down Expand Up @@ -6995,7 +6995,7 @@ void bdd_operator_reset() {

void bdd_operator_clean() {
BddCache_clean_ab(applycache);
BddCache_clean_abc(itecache);
BddCache_clean_itecache(itecache);
BddCache_clean_a(quantcache);
BddCache_clean_ab(appexcache);
BddCache_clean_ab(replacecache);
Expand Down Expand Up @@ -7177,20 +7177,58 @@ void BddCache_clean_ab(BddCache cache) {
}
}

void BddCache_clean_abc(BddCache cache) {
void BddCache_clean_itecache(BddCache cache) {
if (cache == null) {
return;
}
int n;
for (n = 0; n < cache.tablesize; n++) {
int a = cache.table[n].a;
if (a < 0) {

for (int i = 0; i < cache.tablesize; i++) {
BddCacheDataI entry = (BddCacheDataI)cache.table[i];

if (entry == null) {
throw new RuntimeException("Expected a non-null cache entry.");
}

if (entry.a < 0) {
continue;
}
if (LOW(a) == -1 || LOW(cache.table[n].b) == INVALID_BDD || LOW(cache.table[n].c) == INVALID_BDD
|| LOW(((BddCacheDataI)cache.table[n]).res) == INVALID_BDD)
{
cache.table[n].a = -1;

boolean isInvalid = false;

switch (entry.e) {
case bddop_ite:
case bddop_relnext:
case bddop_relprev:
isInvalid = LOW(entry.a) == INVALID_BDD || LOW(entry.b) == INVALID_BDD
|| LOW(entry.c) == INVALID_BDD || LOW(entry.res) == INVALID_BDD;
break;

case bddop_relnextUnion:
case bddop_relnextIntersection:
case bddop_relprevUnion:
case bddop_relprevIntersection:
isInvalid = LOW(entry.a) == INVALID_BDD || LOW(entry.b) == INVALID_BDD
|| LOW(entry.c) == INVALID_BDD || LOW(entry.d) == INVALID_BDD
|| LOW(entry.res) == INVALID_BDD;
break;

case bddop_saturationForward:
case bddop_saturationBackward:
isInvalid = LOW(entry.a) == INVALID_BDD || LOW(entry.res) == INVALID_BDD;
break;

case bddop_boundedSaturationForward:
case bddop_boundedSaturationBackward:
isInvalid = LOW(entry.a) == INVALID_BDD || LOW(entry.b) == INVALID_BDD
|| LOW(entry.res) == INVALID_BDD;
break;

default:
throw new RuntimeException("Unknown cache entry.");
}

if (isInvalid) {
entry.a = -1;
}
}
}
Expand Down