diff --git a/src/main/java/com/github/javabdd/JFactory.java b/src/main/java/com/github/javabdd/JFactory.java index b843bdd..87604d9 100644 --- a/src/main/java/com/github/javabdd/JFactory.java +++ b/src/main/java/com/github/javabdd/JFactory.java @@ -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; @@ -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); @@ -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; } } }