Merge pull request #68 from com-github-javabdd/67-bdd-satcount-may-produce-wrong-results

#67 BDD.pathCount/satCount return a BigInteger.

Author: dhendriks

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

@@ -14,6 +14,7 @@
 package com.github.javabdd;
 
 import java.io.PrintStream;
+import java.math.BigDecimal;
 import java.math.BigInteger;
 import java.util.Arrays;
 import java.util.HashMap;
@@ -1443,7 +1444,7 @@ protected int printdot_rec(PrintStream out, int current, boolean[] visited, Hash
      *
      * @return the number of paths leading to the true terminal
      */
-    public abstract double pathCount();
+    public abstract BigInteger pathCount();
 
     /**
      * Calculates the number of satisfying variable assignments.
@@ -1454,7 +1455,7 @@ protected int printdot_rec(PrintStream out, int current, boolean[] visited, Hash
      *
      * @return the number of satisfying variable assignments
      */
-    public abstract double satCount();
+    public abstract BigInteger satCount();
 
     /**
      * Calculates the number of satisfying variable assignments to the variables in the given varset. ASSUMES THAT THE
@@ -1468,18 +1469,19 @@ protected int printdot_rec(PrintStream out, int current, boolean[] visited, Hash
      * @param varset the given varset
      * @return the number of satisfying variable assignments
      */
-    public double satCount(BDDVarSet varset) {
+    public BigInteger satCount(BDDVarSet varset) {
         BDDFactory factory = getFactory();
 
         if (varset.isEmpty() || isZero()) { /* empty set */
-            return 0.;
+            return BigInteger.ZERO;
         }
 
-        double unused = factory.varNum();
+        int unused = factory.varNum();
         unused -= varset.size();
-        unused = satCount() / Math.pow(2.0, unused);
+        BigDecimal unused2 = new BigDecimal(satCount()).divide(new BigDecimal(BigInteger.TWO.pow(unused)));
 
-        return unused >= 1.0 ? unused : 1.0;
+        BigDecimal rslt = unused2.compareTo(BigDecimal.ONE) >= 0 ? unused2 : BigDecimal.ONE;
+        return rslt.toBigIntegerExact();
     }
 
     /**
@@ -1489,10 +1491,14 @@ public double satCount(BDDVarSet varset) {
      * Compare to bdd_satcount.
      * </p>
      *
+     * <p>
+     * Note that this returns a double, so it has more limited precision.
+     * </p>
+     *
      * @return the logarithm of the number of satisfying variable assignments
      */
     public double logSatCount() {
-        return Math.log(satCount());
+        return Math.log(satCount().doubleValue());
     }
 
     /**
@@ -1502,11 +1508,15 @@ public double logSatCount() {
      * Compare to bdd_satcountset.
      * </p>
      *
+     * <p>
+     * Note that this returns a double, so it has more limited precision.
+     * </p>
+     *
      * @param varset the given varset
      * @return the logarithm of the number of satisfying variable assignments
      */
     public double logSatCount(BDDVarSet varset) {
-        return Math.log(satCount(varset));
+        return Math.log(satCount(varset).doubleValue());
     }
 
     /**

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

@@ -405,7 +405,7 @@ public BigInteger[] getVarIndices(BDD that) {
      */
     public BigInteger[] getVarIndices(BDD that, int max) {
         BDDVarSet myvarset = set(); // can't use var here, must respect subclass a factory may provide
-        int n = (int)that.satCount(myvarset);
+        int n = that.satCount(myvarset).intValueExact();
         if (max != -1 && n > max) {
             n = max;
         }

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

@@ -13,6 +13,7 @@
 
 package com.github.javabdd;
 
+import java.math.BigInteger;
 import java.util.Collection;
 import java.util.Iterator;
 import java.util.List;
@@ -117,9 +118,9 @@ public abstract class BDDFactoryIntImpl extends BDDFactory {
 
     protected abstract int nodeCount_impl(/* bdd */int v);
 
-    protected abstract double pathCount_impl(/* bdd */int v);
+    protected abstract BigInteger pathCount_impl(/* bdd */int v);
 
-    protected abstract double satCount_impl(/* bdd */int v);
+    protected abstract BigInteger satCount_impl(/* bdd */int v);
 
     protected abstract /* bdd */int satOne_impl(/* bdd */int v);
 
@@ -269,7 +270,7 @@ public BDD not() {
         }
 
         @Override
-        public double pathCount() {
+        public BigInteger pathCount() {
             return pathCount_impl(v);
         }
 
@@ -306,7 +307,7 @@ public BDD restrictWith(BDD that) {
         }
 
         @Override
-        public double satCount() {
+        public BigInteger satCount() {
             return satCount_impl(v);
         }
 

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

@@ -17,6 +17,7 @@
 import java.io.BufferedWriter;
 import java.io.IOException;
 import java.io.PrintStream;
+import java.math.BigInteger;
 import java.util.Arrays;
 import java.util.Collection;
 import java.util.Collections;
@@ -297,12 +298,12 @@ protected int nodeCount_impl(int v) {
     }
 
     @Override
-    protected double pathCount_impl(int v) {
+    protected BigInteger pathCount_impl(int v) {
         return bdd_pathcount(v);
     }
 
     @Override
-    protected double satCount_impl(int v) {
+    protected BigInteger satCount_impl(int v) {
         return bdd_satcount(v);
     }
 
@@ -1062,16 +1063,16 @@ BddCacheData copy() {
         }
     }
 
-    private static class BddCacheDataD extends BddCacheData {
-        double dres;
+    private static class BddCacheDataBI extends BddCacheData {
+        BigInteger bires;
 
         @Override
         BddCacheData copy() {
-            BddCacheDataD that = new BddCacheDataD();
+            BddCacheDataBI that = new BddCacheDataBI();
             that.a = this.a;
             that.b = this.b;
             that.c = this.c;
-            that.dres = this.dres;
+            that.bires = this.bires;
             return that;
         }
     }
@@ -1083,9 +1084,9 @@ private static class BddCache {
 
         BddCache copy() {
             BddCache that = new BddCache();
-            boolean is_d = this.table instanceof BddCacheDataD[];
-            if (is_d) {
-                that.table = new BddCacheDataD[this.table.length];
+            boolean is_bi = this.table instanceof BddCacheDataBI[];
+            if (is_bi) {
+                that.table = new BddCacheDataBI[this.table.length];
             } else {
                 that.table = new BddCacheDataI[this.table.length];
             }
@@ -6277,110 +6278,92 @@ void varprofile_rec(int r, int[] varprofile) {
         varprofile_rec(HIGH(r), varprofile);
     }
 
-    double bdd_pathcount(int r) {
+    BigInteger bdd_pathcount(int r) {
         CHECK(r);
 
         miscid = CACHEID_PATHCOU;
 
         if (countcache == null) {
-            countcache = BddCacheD_init(cachesize);
+            countcache = BddCacheBI_init(cachesize);
         }
 
         return bdd_pathcount_rec(r);
     }
 
-    double bdd_pathcount_rec(int r) {
-        BddCacheDataD entry;
-        double size;
+    BigInteger bdd_pathcount_rec(int r) {
+        BddCacheDataBI entry;
 
         if (ISZERO(r)) {
-            return 0.0;
+            return BigInteger.ZERO;
         }
         if (ISONE(r)) {
-            return 1.0;
+            return BigInteger.ONE;
         }
 
-        entry = BddCache_lookupD(countcache, PATHCOUHASH(r));
+        entry = BddCache_lookupBI(countcache, PATHCOUHASH(r));
         if (entry.a == r && entry.c == miscid) {
-            return entry.dres;
+            return entry.bires;
         }
 
-        size = bdd_pathcount_rec(LOW(r)) + bdd_pathcount_rec(HIGH(r));
+        BigInteger size = bdd_pathcount_rec(LOW(r)).add(bdd_pathcount_rec(HIGH(r)));
 
         entry.a = r;
         entry.c = miscid;
-        entry.dres = size;
+        entry.bires = size;
 
         return size;
     }
 
-    double bdd_satcount(int r) {
+    BigInteger bdd_satcount(int r) {
         if (ZDD) {
             return bdd_pathcount(r);
         }
 
-        double size = 1;
-
         CHECK(r);
 
         if (countcache == null) {
-            countcache = BddCacheD_init(cachesize);
+            countcache = BddCacheBI_init(cachesize);
         }
 
         miscid = CACHEID_SATCOU;
-        if (!ZDD) {
-            size = Math.pow(2.0, LEVEL(r));
-        }
-
-        return size * satcount_rec(r);
-    }
-
-    double bdd_satcountset(int r, int varset) {
-        double unused = bddvarnum;
-        int n;
-
-        if (ISCONST(varset) || ISZERO(r)) { /* empty set */
-            return 0.0;
-        }
-
-        for (n = varset; !ISCONST(n); n = HIGH(n)) {
-            unused--;
+        BigInteger size;
+        if (ZDD) {
+            size = BigInteger.ONE;
+        } else {
+            size = BigInteger.TWO.pow(LEVEL(r));
         }
 
-        unused = bdd_satcount(r) / Math.pow(2.0, unused);
-
-        return unused >= 1.0 ? unused : 1.0;
+        return size.multiply(satcount_rec(r));
     }
 
-    double satcount_rec(int root) {
-        BddCacheDataD entry;
-        double size, s;
+    BigInteger satcount_rec(int root) {
+        BddCacheDataBI entry;
 
         if (root < 2) {
-            return root;
+            return BigInteger.valueOf(root);
         }
 
-        entry = BddCache_lookupD(countcache, SATCOUHASH(root));
+        entry = BddCache_lookupBI(countcache, SATCOUHASH(root));
         if (entry.a == root && entry.c == miscid) {
-            return entry.dres;
+            return entry.bires;
         }
 
-        size = 0;
-        s = 1;
+        BigInteger size = BigInteger.ZERO;
+        BigInteger s = BigInteger.ONE;
         if (!ZDD) {
-            s *= Math.pow(2.0, LEVEL(LOW(root)) - LEVEL(root) - 1);
+            s = s.multiply(BigInteger.TWO.pow(LEVEL(LOW(root)) - LEVEL(root) - 1));
         }
-        size += s * satcount_rec(LOW(root));
+        size = size.add(s.multiply(satcount_rec(LOW(root))));
 
-        s = 1;
+        s = BigInteger.ONE;
         if (!ZDD) {
-            s *= Math.pow(2.0, LEVEL(HIGH(root)) - LEVEL(root) - 1);
+            s = s.multiply(BigInteger.TWO.pow(LEVEL(HIGH(root)) - LEVEL(root) - 1));
         }
-        size += s * satcount_rec(HIGH(root));
+        size = size.add(s.multiply(satcount_rec(HIGH(root))));
 
         entry.a = root;
         entry.c = miscid;
-        entry.dres = size;
+        entry.bires = size;
 
         return size;
     }
@@ -6942,7 +6925,7 @@ void bdd_operator_init(int cachesize) {
             appexcache = BddCacheI_init(cachesize);
             replacecache = BddCacheI_init(cachesize);
             misccache = BddCacheI_init(cachesize);
-            countcache = BddCacheD_init(cachesize);
+            countcache = BddCacheBI_init(cachesize);
         }
 
         quantvarsetID = 0;
@@ -7050,16 +7033,16 @@ BddCache BddCacheI_init(int size) {
         return cache;
     }
 
-    BddCache BddCacheD_init(int size) {
+    BddCache BddCacheBI_init(int size) {
         int n;
 
         size = bdd_prime_gte(size);
 
         BddCache cache = new BddCache();
-        cache.table = new BddCacheDataD[size];
+        cache.table = new BddCacheDataBI[size];
 
         for (n = 0; n < size; n++) {
-            cache.table[n] = new BddCacheDataD();
+            cache.table[n] = new BddCacheDataBI();
             cache.table[n].a = -1;
         }
         cache.tablesize = size;
@@ -7082,21 +7065,21 @@ int BddCache_resize(BddCache cache, int newsize) {
         }
         int n;
 
-        boolean is_d = cache.table instanceof BddCacheDataD[];
+        boolean is_bi = cache.table instanceof BddCacheDataBI[];
 
         cache.table = null;
 
         newsize = bdd_prime_gte(newsize);
 
-        if (is_d) {
-            cache.table = new BddCacheDataD[newsize];
+        if (is_bi) {
+            cache.table = new BddCacheDataBI[newsize];
         } else {
             cache.table = new BddCacheDataI[newsize];
         }
 
         for (n = 0; n < newsize; n++) {
-            if (is_d) {
-                cache.table[n] = new BddCacheDataD();
+            if (is_bi) {
+                cache.table[n] = new BddCacheDataBI();
             } else {
                 cache.table[n] = new BddCacheDataI();
             }
@@ -7111,8 +7094,8 @@ BddCacheDataI BddCache_lookupI(BddCache cache, int hash) {
         return (BddCacheDataI)cache.table[Math.abs(hash % cache.tablesize)];
     }
 
-    BddCacheDataD BddCache_lookupD(BddCache cache, int hash) {
-        return (BddCacheDataD)cache.table[Math.abs(hash % cache.tablesize)];
+    BddCacheDataBI BddCache_lookupBI(BddCache cache, int hash) {
+        return (BddCacheDataBI)cache.table[Math.abs(hash % cache.tablesize)];
     }
 
     void BddCache_reset(BddCache cache) {