Merge pull request #41 from com-github-javabdd/40-rethink-the-cache-ratio-option

#40 Redesign the operator cache ratio.

Author: dhendriks

src/main/java/com/github/javabdd/BDDFactory.java

@@ -417,7 +417,8 @@ public void reset() {
 
     /**
      * Sets the cache ratio for the operator caches. When the node table grows, operator caches will also grow to
-     * maintain the ratio.
+     * maintain the ratio. A ratio of {@code 0.5} leads to caches that are half the node table size, while a ratio
+     * of {@code 2.0} leads to caches that are twice the node table size.
      *
      * <p>
      * Compare to bdd_setcacheratio.

src/main/java/com/github/javabdd/JFactory.java

@@ -434,7 +434,7 @@ public void printStat() {
 
     @Override
     public double setCacheRatio(double x) {
-        return bdd_setcacheratio((int)x);
+        return bdd_setcacheratio(x);
     }
 
     @Override
@@ -4726,7 +4726,7 @@ void bdd_init(int initnodesize, int cs) {
 
     BddCache countcache; /* Cache for count results */
 
-    int cacheratio;
+    double cacheratio;
 
     boolean satPolarity;
 
@@ -4817,7 +4817,7 @@ int bdd_setcachesize(int newcachesize) {
 
     void bdd_operator_noderesize() {
         if (cacheratio > 0) {
-            int newcachesize = bddnodesize / cacheratio;
+            int newcachesize = (int)(bddnodesize * cacheratio);
 
             BddCache_resize(applycache, newcachesize);
             BddCache_resize(itecache, newcachesize);
@@ -6088,8 +6088,8 @@ int bdd_setmaxincrease(int size) {
         return old;
     }
 
-    int bdd_setcacheratio(int r) {
-        int old = cacheratio;
+    double bdd_setcacheratio(double r) {
+        double old = cacheratio;
 
         if (r <= 0) {
             return bdd_error(BDD_RANGE);