Merge pull request #76 from wytseoortwijn/75-fix-cache-cleanup

#75 Fix cache cleanup + enable FLUSH_CACHE_ON_GC by default

Author: dhendriks

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;
             }
         }
     }