Version 0.5.1

CHANGELOG.md

@@ -2,6 +2,10 @@
 
 ## 0.5
 
+### 0.5.1 (2019-08-19)
+
+* Small fixes and improvements
+
 ### 0.5.0 (2019-08-06)
 
 * Added an (mostly) iterative implementation of bdds to alleviate stack overflow problems for deep structures

build.gradle

@@ -1,5 +1,5 @@
 group 'de.tum.in'
-version '0.5.0'
+version '0.5.1'
 
 apply plugin: 'java'
 
@@ -34,7 +34,7 @@ dependencies {
 
 apply from: 'gradle/analysis.gradle'
 
-// Deployment - run with -Prelease clean uploadArchives closeAndReleaseRepository
+// Deployment - run with -Prelease clean publish
 if (project.hasProperty('release')) {
     apply plugin: 'maven-publish'
     apply plugin: 'signing'

src/main/java/de/tum/in/jbdd/BddCache.java

@@ -224,7 +224,7 @@ void clearVolatileCache() {
   }
 
 
-  String getStatistics() {
+  public String getStatistics() {
     @SuppressWarnings("MagicNumber")
     StringBuilder builder = new StringBuilder(512);
     builder.append("Negation: size: ").append(getNegationCacheKeyCount()) //
@@ -304,14 +304,6 @@ private float computeVolatileLoadFactor() {
   }
 
 
-  private int ensureMinimumCacheKeyCount(int cacheSize) {
-    if (cacheSize < associatedBdd.getConfiguration().minimumNodeTableSize()) {
-      return MathUtil.nextPrime(associatedBdd.getConfiguration().minimumNodeTableSize());
-    }
-    return MathUtil.nextPrime(cacheSize);
-  }
-
-
   private int getBinaryCachePosition(int hash) {
     return mod(hash, getBinaryCacheKeyCount()) * binaryBinsPerHash;
   }
@@ -618,7 +610,7 @@ void putXor(int hash, int inputNode1, int inputNode2, int resultNode) {
   private void reallocateBinary() {
     int keyCount = associatedBdd.getTableSize()
       / associatedBdd.getConfiguration().cacheBinaryDivider();
-    int actualSize = ensureMinimumCacheKeyCount(keyCount) * binaryBinsPerHash;
+    int actualSize = MathUtil.nextPrime(keyCount) * binaryBinsPerHash;
     binaryKeyStorage = new long[actualSize];
     binaryResultStorage = new int[actualSize];
   }
@@ -630,30 +622,30 @@ private void reallocateCompose() {
     }
     int keyCount = associatedBdd.getTableSize()
       / associatedBdd.getConfiguration().cacheComposeDivider();
-    int actualSize = ensureMinimumCacheKeyCount(keyCount)
+    int actualSize = MathUtil.nextPrime(keyCount)
       * (2 + associatedBdd.numberOfVariables());
     composeStorage = new int[actualSize];
   }
 
   private void reallocateSatisfaction() {
     int keyCount = associatedBdd.getTableSize()
       / associatedBdd.getConfiguration().cacheSatisfactionDivider();
-    int actualSize = ensureMinimumCacheKeyCount(keyCount) * satisfactionBinsPerHash;
+    int actualSize = MathUtil.nextPrime(keyCount) * satisfactionBinsPerHash;
     satisfactionKeyStorage = new int[actualSize];
     satisfactionResultStorage = new BigInteger[actualSize];
   }
 
   private void reallocateTernary() {
     int keyCount = associatedBdd.getTableSize()
       / associatedBdd.getConfiguration().cacheTernaryDivider();
-    int actualSize = ensureMinimumCacheKeyCount(keyCount) * ternaryBinsPerHash * 2;
+    int actualSize = MathUtil.nextPrime(keyCount) * ternaryBinsPerHash * 2;
     ternaryStorage = new long[actualSize];
   }
 
   private void reallocateNegation() {
     int keyCount = associatedBdd.getTableSize()
       / associatedBdd.getConfiguration().cacheNegationDivider();
-    int actualSize = ensureMinimumCacheKeyCount(keyCount) * negationBinsPerHash;
+    int actualSize = MathUtil.nextPrime(keyCount) * negationBinsPerHash;
     negationStorage = new long[actualSize];
   }
 
@@ -906,7 +898,7 @@ private static final class ShutdownHookPrinter implements Runnable {
     public void run() {
       if (!logger.isLoggable(Level.FINER)) {
         if (!cacheShutdownHook.isEmpty()) {
-          System.err.println("Not printing statistics since FINER level disabled");
+          logger.log(Level.INFO, "Not printing statistics since FINER level disabled");
         }
         return;
       }

src/main/java/de/tum/in/jbdd/BddConfiguration.java

@@ -38,13 +38,8 @@ public class BddConfiguration {
   public static final int DEFAULT_INITIAL_VARIABLE_NODES = 32;
   public static final int DEFAULT_MINIMUM_CACHE_SIZE = 32;
   public static final int DEFAULT_MINIMUM_NODE_TABLE_SIZE = 100;
-  public static final float DEFAULT_NODE_TABLE_FREE_NODE_PERCENTAGE = 0.05f;
-  public static final int DEFAULT_NODE_TABLE_GC_DEAD_NODE_COUNT = 2_000;
-  public static final int DEFAULT_NODE_TABLE_IS_BIG_THRESHOLD = 40_000;
-  public static final int DEFAULT_NODE_TABLE_IS_SMALL_THRESHOLD = 2_000;
-  public static final int DEFAULT_NODE_TABLE_MAXIMUM_GROWTH = 50_000;
-  public static final int DEFAULT_NODE_TABLE_MINIMUM_FREE_NODE_COUNT = 1_000;
-  public static final int DEFAULT_NODE_TABLE_MINIMUM_GROWTH = 5_000;
+  public static final double DEFAULT_NODE_TABLE_FREE_NODE_PERCENTAGE = 0.05d;
+  public static final double DEFAULT_NODE_TABLE_GROWTH_FACTOR = 1.5d;
 
   @Value.Default
   public int cacheBinaryBinsPerHash() {
@@ -116,49 +111,19 @@ public boolean logStatisticsOnShutdown() {
     return true;
   }
 
-  @Value.Default
-  public int maximumNodeTableGrowth() {
-    return DEFAULT_NODE_TABLE_MAXIMUM_GROWTH;
-  }
-
   @Value.Default
   public int minimumCacheSize() {
     return DEFAULT_MINIMUM_CACHE_SIZE;
   }
 
   @Value.Default
-  public int minimumDeadNodesCountForGcInGrow() {
-    return DEFAULT_NODE_TABLE_GC_DEAD_NODE_COUNT;
-  }
-
-  @Value.Default
-  public int minimumFreeNodeCountAfterGc() {
-    return DEFAULT_NODE_TABLE_MINIMUM_FREE_NODE_COUNT;
-  }
-
-  @Value.Default
-  public float minimumFreeNodePercentageAfterGc() {
+  public double minimumFreeNodePercentageAfterGc() {
     return DEFAULT_NODE_TABLE_FREE_NODE_PERCENTAGE;
   }
 
   @Value.Default
-  public int minimumNodeTableGrowth() {
-    return DEFAULT_NODE_TABLE_MINIMUM_GROWTH;
-  }
-
-  @Value.Default
-  public int minimumNodeTableSize() {
-    return DEFAULT_MINIMUM_NODE_TABLE_SIZE;
-  }
-
-  @Value.Default
-  public int nodeTableBigThreshold() {
-    return DEFAULT_NODE_TABLE_IS_BIG_THRESHOLD;
-  }
-
-  @Value.Default
-  public int nodeTableSmallThreshold() {
-    return DEFAULT_NODE_TABLE_IS_SMALL_THRESHOLD;
+  public double growthFactor() {
+    return DEFAULT_NODE_TABLE_GROWTH_FACTOR;
   }
 
   @Value.Default

src/main/java/de/tum/in/jbdd/BddIterative.java

@@ -914,12 +914,16 @@ private int ifThenElseIterative(int ifNode, int thenNode, int elseNode, int base
             result = andIterative(pushToWorkStack(not), currentElse, stackIndex);
             popWorkStack();
           }
-        } else if (currentElse == FALSE_NODE) {
-          result = andIterative(currentIf, currentThen, stackIndex);
         } else if (currentElse == TRUE_NODE) {
           int not = notIterative(currentThen, stackIndex);
           result = notAndIterative(currentIf, pushToWorkStack(not), stackIndex);
           popWorkStack();
+        } else if (currentElse == FALSE_NODE) {
+          result = andIterative(currentIf, currentThen, stackIndex);
+        } else if (currentIf == currentThen) {
+          result = orIterative(currentIf, currentElse, stackIndex);
+        } else if (currentIf == currentElse) {
+          result = andIterative(currentIf, currentThen, stackIndex);
         } else if (cache.lookupIfThenElse(currentIf, currentThen, currentElse)) {
           result = cache.getLookupResult();
         } else {

src/main/java/de/tum/in/jbdd/BddRecursive.java

@@ -636,14 +636,20 @@ private int ifThenElseRecursive(int ifNode, int thenNode, int elseNode) {
       return result;
     }
 
-    if (elseNode == FALSE_NODE) {
-      return andRecursive(ifNode, thenNode);
-    }
     if (elseNode == TRUE_NODE) {
       int result = notAndRecursive(ifNode, pushToWorkStack(notRecursive(thenNode)));
       popWorkStack();
       return result;
     }
+    if (elseNode == FALSE_NODE) {
+      return andRecursive(ifNode, thenNode);
+    }
+    if (ifNode == thenNode) {
+      return orRecursive(ifNode, elseNode);
+    }
+    if (ifNode == elseNode) {
+      return andRecursive(ifNode, thenNode);
+    }
 
     if (cache.lookupIfThenElse(ifNode, thenNode, elseNode)) {
       return cache.getLookupResult();

src/main/java/de/tum/in/jbdd/CanonicalGcManager.java

@@ -99,7 +99,7 @@ private void processReferenceQueue(int protectedNode) {
   }
 
   @SuppressWarnings("InterfaceMayBeAnnotatedFunctional")
-  interface BddWrapper {
+  public interface BddWrapper {
     int node();
   }