test sup

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/math/dd/dd_bdd.h

@@ -375,6 +375,8 @@ namespace dd {
     inline bddv operator*(rational const& r, bddv const& a) { return a * r; }
     inline bddv operator+(rational const& r, bddv const& a) { return a + r; }
     inline bddv operator-(rational const& r, bddv const& a) { return a.rev_sub(r); }
+    inline bdd operator<=(int i, bddv const& a) { return a >= rational(i); }
+    inline bdd operator<=(bddv const& a, int i) { return a <= rational(i); }
 
 
 }

src/math/dd/dd_fdd.cpp

@@ -121,7 +121,7 @@ namespace dd {
     }
 
   
-    bool fdd::sup(bdd const& x, bool_vector& lo) {
+    bool fdd::sup(bdd const& x, bool_vector& lo) const {
         SASSERT(lo.size() == num_bits());
 	//
 	// Assumption: common case is that high-order bits are before lower-order bits also
@@ -194,7 +194,7 @@ namespace dd {
         for (unsigned i = idx; i-- > 0; ) {
             SASSERT(!b.is_true());
             if (b.is_false()) {
-                for (unsigned j = 0; j < i; ++j)
+                for (unsigned j = 0; j <= i; ++j)
                     lo[j] = false;
                 break;
             }
@@ -206,20 +206,16 @@ namespace dd {
         }
 
         // subtract one from resulting vector:
-
-        for (unsigned i = 0; i < lo.size(); ++i) {
-            if (lo[i]) {
-                lo[i] = false;
+        for (auto& b : lo) {
+            b = !b;
+            if (!b)
                 break;
-            }
-            else 
-                lo[i] = true;                
         }
         
 	return true;
     }
     
-    bool fdd::inf(bdd const& b, bool_vector& hi) {
+    bool fdd::inf(bdd const& b, bool_vector& hi) const {
         SASSERT(hi.size() == num_bits());
 	return false;
     }

src/math/dd/dd_fdd.h

@@ -84,9 +84,9 @@ namespace dd {
 	 * \return false if b is false at lo/hi
 	 * \pre variables in b are a subset of variables from the fdd
 	 */ 
-	bool sup(bdd const& b, bool_vector& lo);
+	bool sup(bdd const& b, bool_vector& lo) const;
       
-	bool inf(bdd const& b, bool_vector& hi); 
+	bool inf(bdd const& b, bool_vector& hi) const; 
       
     };
 

src/test/bdd.cpp

@@ -438,6 +438,40 @@ public:
 	SASSERT(c1.cofactor(!v1) == m.mk_false());
     }
 
+    static void inc(bool_vector& x) {
+        for (auto& b : x) {
+            b = !b;
+            if (b)
+                break;
+        }
+    }
+
+    static unsigned value(bool_vector const& x) {
+        unsigned p = 1;
+        unsigned v = 0;
+        for (auto b : x) {
+            v += p*b;
+            p <<= 1;
+        }
+        return v;
+    }
+
+    static void test_sup() {
+	std::cout << "test_sup\n";
+	bdd_manager m(20);
+        fdd const x_dom(m, 10);
+        bddv const& x = x_dom.var();
+        bdd c = (1 <= x && x <= 5) || (11 <= x && x <= 13) || (29 <= x && x <= 33);
+        bool_vector lo(10, false);
+        for (unsigned i = 0; i < 30; ++i) {
+            bool found = x_dom.sup(c, lo);
+            std::cout << found << ": " << value(lo) << "\n";
+            if (found) 
+                std::cout << x_dom.sup(c, lo) << ": " << value(lo) << "\n";
+            inc(lo);
+        }        
+    }
+
 };
 
 }
@@ -460,4 +494,5 @@ void tst_bdd() {
     dd::test_bdd::test_fdd_twovars();
     dd::test_bdd::test_fdd_find_hint();
     dd::test_bdd::test_cofactor();
+    dd::test_bdd::test_sup();
 }