Additional BDD operations; BDD vectors and finite domain abstraction

src/math/dd/CMakeLists.txt

@@ -1,6 +1,7 @@
 z3_add_component(dd
   SOURCES
     dd_bdd.cpp
+    dd_fdd.cpp
     dd_pdd.cpp
   COMPONENT_DEPENDENCIES
     util

src/math/dd/dd_bdd.cpp

@@ -142,6 +142,8 @@ namespace dd {
             if (a == b) return false_bdd;
             if (is_false(a)) return b;
             if (is_false(b)) return a;
+            if (is_true(a)) return mk_not_rec(b);
+            if (is_true(b)) return mk_not_rec(a);
             break;
         default:
             UNREACHABLE();
@@ -571,7 +573,63 @@ namespace dd {
         e1->m_result = r;
         return r;
     }
+
+    /**
+     * co-factor a using b. 
+     * b must be a variable bdd (it can be generalized to a cube)
+     */
+
+    bdd bdd_manager::mk_cofactor(bdd const& a, bdd const& b) {
+	bool first = true;
+        scoped_push _sp(*this);
+        SASSERT(!b.is_const() && b.lo().is_const() && b.hi().is_const());
+        while (true) {
+            try {
+                return bdd(mk_cofactor_rec(a.root, b.root), this); 
+            }
+            catch (const mem_out &) {
+                if (!first) throw;
+                try_reorder();
+                first = false;
+            }
+        }
+    }
+
+    bdd_manager::BDD bdd_manager::mk_cofactor_rec(BDD a, BDD b) {
+        if (is_const(a)) return a;
+        if (is_const(b)) return a;
+        unsigned la = level(a), lb = level(b);
+	// cases where b is a single literal
+	if (la == lb && is_const(lo(b)) && is_const(hi(b)))
+	    return is_true(hi(b)) ? hi(a) : lo(a);
+	if (la < lb && is_const(lo(b)) && is_const(hi(b)))
+	    return a;
+	// cases where b is a proper cube (with more than one literal
+	if (la == lb) {
+	    if (is_false(lo(b)))
+		a = hi(a), b = hi(b);
+	    else
+		a = lo(a), b = lo(b);
+	    return mk_cofactor_rec(a, b);
+	}
+	if (la < lb) 
+	    return mk_cofactor_rec(a, is_false(lo(b)) ? hi(b) : lo(b));
+
+        op_entry* e1 = pop_entry(a, b, bdd_cofactor_op);
+        op_entry const* e2 = m_op_cache.insert_if_not_there(e1);
+        if (check_result(e1, e2, a, b, bdd_cofactor_op))
+            return e2->m_result;
+
+        SASSERT(la > lb);
+        push(mk_cofactor_rec(lo(a), b));
+        push(mk_cofactor_rec(hi(a), b));
+        BDD r = make_node(la, read(2), read(1));
+        pop(2);
+        e1->m_result = r;
+        return r;
+    }
     
+
     bdd bdd_manager::mk_ite(bdd const& c, bdd const& t, bdd const& e) {         
         bool first = true;
         scoped_push _sp(*this);
@@ -587,14 +645,15 @@ namespace dd {
         }
     }
 
+
     bdd_manager::BDD bdd_manager::mk_ite_rec(BDD a, BDD b, BDD c) {
         if (is_true(a)) return b;
         if (is_false(a)) return c;
         if (b == c) return b;
-        if (is_true(b)) return apply(a, c, bdd_or_op);
-        if (is_false(c)) return apply(a, b, bdd_and_op);
-        if (is_false(b)) return apply(mk_not_rec(a), c, bdd_and_op);
-        if (is_true(c)) return apply(mk_not_rec(a), b, bdd_or_op);
+        if (is_true(b)) return apply_rec(a, c, bdd_or_op);
+        if (is_false(c)) return apply_rec(a, b, bdd_and_op);
+        if (is_false(b)) return apply_rec(mk_not_rec(a), c, bdd_and_op);
+        if (is_true(c)) return apply_rec(mk_not_rec(a), b, bdd_or_op);
         SASSERT(!is_const(a) && !is_const(b) && !is_const(c));
         op_entry * e1 = pop_entry(a, b, c);
         op_entry const* e2 = m_op_cache.insert_if_not_there(e1);
@@ -644,6 +703,7 @@ namespace dd {
 
     bdd_manager::BDD bdd_manager::mk_quant(unsigned n, unsigned const* vars, BDD b, bdd_op op) {
         BDD result = b;
+        // TODO: should this method catch mem_out like the other non-rec mk_ methods?
         for (unsigned i = 0; i < n; ++i) {
             result = mk_quant_rec(m_var2level[vars[i]], result, op);
         }
@@ -895,4 +955,299 @@ namespace dd {
     bdd& bdd::operator=(bdd const& other) { unsigned r1 = root; root = other.root; m->inc_ref(root); m->dec_ref(r1); return *this; }
     std::ostream& operator<<(std::ostream& out, bdd const& b) { return b.display(out); }
 
+
+    bdd bdd_manager::mk_eq(bddv const& a, bddv const& b) {
+        SASSERT(a.size() == b.size());
+        bdd eq = mk_true();
+        for (unsigned i = 0; i < a.size(); ++i)
+            eq &= !(a[i] ^ b[i]);
+        return eq;
+    }
+
+    bdd bdd_manager::mk_eq(bddv const& a, rational const& n) {
+        SASSERT(n.is_int() && n >= 0 && n < rational(2).expt(a.size()));
+        bdd b = mk_true();
+        for (unsigned i = 0; i < a.size(); ++i)
+            b &= n.get_bit(i) ? a[i] : !a[i];
+        return b;
+    }
+
+    bdd bdd_manager::mk_eq(unsigned_vector const& vars, rational const& n) {
+        SASSERT(n.is_int() && n >= 0 && n < rational(2).expt(vars.size()));
+        bdd b = mk_true();
+        for (unsigned i = 0; i < vars.size(); ++i)
+            b &= n.get_bit(i) ? mk_var(vars[i]) : mk_nvar(vars[i]);
+        return b;
+    }
+
+    bdd bdd_manager::mk_ule(bddv const& a, bddv const& b) {
+        SASSERT(a.size() == b.size());
+        bdd lt = mk_false();
+        bdd eq = mk_true();
+        for (unsigned i = a.size(); i-- > 0 && !eq.is_false(); ) {
+            lt |= eq && (!a[i] && b[i]);
+            eq &= !(a[i] ^ b[i]);
+        }
+        return lt || eq;
+    }
+    bdd bdd_manager::mk_uge(bddv const& a, bddv const& b) { return mk_ule(b, a); }
+    bdd bdd_manager::mk_ult(bddv const& a, bddv const& b) { return mk_ule(a, b) && !mk_eq(a, b); }
+    bdd bdd_manager::mk_ugt(bddv const& a, bddv const& b) { return mk_ult(b, a); }
+
+    bdd bdd_manager::mk_sle(bddv const& a, bddv const& b) {
+        SASSERT(a.size() == b.size());
+        // Note: sle can be reduced to ule by flipping the sign bits of both arguments
+        bdd lt = mk_false();
+        bdd eq = mk_true();
+        unsigned const sz = a.size();
+        if (sz > 0) {
+            lt = a[sz - 1] && !b[sz - 1];
+            eq = !(a[sz - 1] ^ b[sz - 1]);
+            for (unsigned i = sz - 1; i-- > 0; ) {
+                lt |= eq && (!a[i] && b[i]);
+                eq &= !(a[i] ^ b[i]);
+            }
+        }
+        return lt || eq;
+    }
+    bdd bdd_manager::mk_sge(bddv const& a, bddv const& b) { return mk_sle(b, a); }
+    bdd bdd_manager::mk_slt(bddv const& a, bddv const& b) { return mk_sle(a, b) && !mk_eq(a, b); }
+    bdd bdd_manager::mk_sgt(bddv const& a, bddv const& b) { return mk_slt(b, a); }
+
+    bddv bdd_manager::mk_add(bddv const& a, bddv const& b) {
+        SASSERT(a.size() == b.size());
+        bdd carry = mk_false();
+        bddv result(this);
+#if 0
+        for (unsigned i = 0; i < a.size(); ++i) {
+            result.push_back(carry ^ a[i] ^ b[i]);
+            carry = (carry && a[i]) || (carry && b[i]) || (a[i] && b[i]);
+        }
+#else
+        if (a.size() > 0)
+            result.push_back(a[0] ^ b[0]);
+        for (unsigned i = 1; i < a.size(); ++i) {
+            carry = (carry && a[i-1]) || (carry && b[i-1]) || (a[i-1] && b[i-1]);
+            result.push_back(carry ^ a[i] ^ b[i]);
+        }
+#endif
+        return result;
+    }
+
+    bddv bdd_manager::mk_add(bddv const& a, std::function<bdd(unsigned)>& b) {
+        bdd carry = mk_false();
+        bddv result(this);
+        if (a.size() > 0)
+            result.push_back(a[0] ^ b(0));
+        for (unsigned i = 1; i < a.size(); ++i) {
+            auto bi1 = b(i-1);
+            carry = (carry && a[i-1]) || (carry && bi1) || (a[i-1] && bi1);
+            result.push_back(carry ^ a[i] ^ b(i));
+        }
+        return result;
+    }
+
+
+    bddv bdd_manager::mk_sub(bddv const& a, bddv const& b) {
+        SASSERT(a.size() == b.size());
+        bdd carry = mk_false();
+        bddv result(this);
+        if (a.size() > 0)
+            result.push_back(a[0] ^ b[0]);
+        for (unsigned i = 1; i < a.size(); ++i) {
+            // carry = (a[i-1] && b[i-1] && carry) || (!a[i-1] && (b[i-1] || carry));
+            carry = mk_ite(a[i-1], b[i-1] && carry, b[i-1] || carry);
+            result.push_back(carry ^ a[i] ^ b[i]);
+        }
+        return result;
+    }
+
+    bddv bdd_manager::mk_usub(bddv const& a) {
+        bddv result(this);        
+        bdd carry = mk_false();
+        result.push_back(a[0]);
+        for (unsigned i = 1; i < a.size(); ++i) {
+            carry = a[i-1] || carry;
+            result.push_back(carry ^ a[i]);
+        }
+        return result;
+    }
+
+    bool_vector bdd_manager::mk_usub(bool_vector const& b) {
+        bool_vector result;
+        if (b.empty())
+            return result;
+        bool carry = false;
+        result.push_back(b[0]);
+        for (unsigned i = 1; i < b.size(); ++i) {
+            carry = carry || b[i-1];
+            result.push_back(carry ^ b[i]);
+        }
+        return result;
+    }
+
+
+    bddv bdd_manager::mk_mul(bddv const& a, bddv const& b) {
+        SASSERT(a.size() == b.size());
+        bddv result = mk_zero(a.size());
+        for (unsigned i = 0; i < b.size(); ++i) {
+            std::function<bdd(unsigned)> get_a = [&](unsigned k) {
+                if (k < i)
+                    return mk_false();
+                else
+                    return a[k - i] && b[i];
+            };
+            result = mk_add(result, get_a);
+        }
+        return result;
+    }
+
+    bddv bdd_manager::mk_mul(bddv const& a, rational const& val) {
+        SASSERT(val.is_int() && val >= 0 && val < rational::power_of_two(a.size()));
+        bool_vector b;
+        for (unsigned i = 0; i < a.size(); ++i) 
+            b.push_back(val.get_bit(i));
+        return mk_mul(a, b);
+    }
+
+    bddv bdd_manager::mk_mul(bddv const& a, bool_vector const& b) {
+        SASSERT(a.size() == b.size());
+        bddv result = mk_zero(a.size());
+
+        // use identity (bvmul a b) == (bvneg (bvmul (bvneg a) b))
+        unsigned cnt = 0;
+        for (auto v : b) if (v) cnt++; 
+        if (cnt*2 > b.size()+1)
+            return mk_usub(mk_mul(a, mk_usub(b)));
+
+        for (unsigned i = 0; i < a.size(); ++i) {
+            std::function<bdd(unsigned)> get_a = [&](unsigned k) {
+                if (k < i)
+                    return mk_false();
+                else
+                    return a[k - i];
+            };
+            if (b[i])
+                result = mk_add(result, get_a);
+        }
+        return result;
+    }
+
+    bddv bdd_manager::mk_concat(bddv const& a, bddv const& b) {
+        bddv result = a;
+        result.m_bits.append(b.m_bits);
+        return result;
+    }
+
+
+    /**
+     * Quotient remainder
+     * 
+     *  rem, div have size 2*|a| = worksize. 
+     * Initialization:
+     *  rem := a ++ false
+     *  div := false ++ b
+     */
+    void bdd_manager::mk_quot_rem(bddv const& a, bddv const& b, bddv& quot, bddv& rem) {
+        SASSERT(a.size() == b.size());
+        quot = mk_zero(a.size());
+        unsigned worksize = a.size() + b.size();
+        rem = a.append(mk_zero(b.size()));
+        bddv div = mk_zero(a.size()).append(b);
+        //
+        // Keep shifting divisor to the right and subtract whenever it is
+        // smaller than the remaining value
+        //
+        for (unsigned i = 0; i <= b.size(); ++i) {
+            bdd divLteRem = div <= rem;
+            bddv remSubDiv = rem - div;
+
+            for (unsigned j = 0; j < worksize; ++j)
+                rem[j] = mk_ite(divLteRem, remSubDiv[j], rem[j]);
+
+            if (i > 0)
+                quot[b.size() - i] = divLteRem;
+
+            div.shr();
+        }
+        rem.m_bits.shrink(b.size());
+    }
+
+    bddv bdd_manager::mk_num(rational const& n, unsigned num_bits) {
+        SASSERT(n.is_int() && n >= 0 && n < rational::power_of_two(num_bits));
+        bddv result(this);
+        for (unsigned i = 0; i < num_bits; ++i)
+            result.push_back(n.get_bit(i) ? mk_true() : mk_false());
+        return result;
+    }
+
+    bddv bdd_manager::mk_ones(unsigned num_bits) {
+        bddv result(this);
+        for (unsigned i = 0; i < num_bits; ++i)
+            result.push_back(mk_true());
+        return result;
+    }
+
+    bddv bdd_manager::mk_zero(unsigned num_bits) {
+        bddv result(this);
+        for (unsigned i = 0; i < num_bits; ++i)
+            result.push_back(mk_false());
+        return result;
+    }
+
+    bddv bdd_manager::mk_var(unsigned num_bits, unsigned const* vars) {
+        bddv result(this);
+        for (unsigned i = 0; i < num_bits; ++i)
+            result.push_back(mk_var(vars[i]));
+        return result;
+    }
+
+    bddv bdd_manager::mk_var(unsigned_vector const& vars) {
+        return mk_var(vars.size(), vars.data());
+    }
+
+    bool bdd_manager::is_constv(bddv const& a) {
+        for (bdd const& bit : a.bits())
+            if (!is_const(bit.root))
+                return false;
+        return true;
+    }
+
+    rational bdd_manager::to_val(bddv const& a) {
+        rational result = rational::zero();
+        for (unsigned i = 0; i < a.size(); ++i) {
+            bdd const &bit = a[i];
+            SASSERT(is_const(bit.root));
+            if (bit.is_true())
+                result += rational::power_of_two(i);
+        }
+        return result;
+    }
+
+    void bddv::shl() {
+        for (unsigned j = size(); j-- > 1;)
+            m_bits[j] = m_bits[j - 1];
+        m_bits[0] = m->mk_false();
+    }
+
+    void bddv::shr() {
+        for (unsigned j = 1; j < size(); ++j)
+            m_bits[j - 1] = m_bits[j];
+        m_bits[size() - 1] = m->mk_false();
+    }
+
+    bdd bddv::all0() const {
+        bdd r = m->mk_true();
+        for (unsigned i = 0; i < size() && !r.is_false(); ++i)
+            r &= !m_bits[i];
+        return r;
+    }
+
+    bdd bddv::all1() const {
+        bdd r = m->mk_true();
+        for (unsigned i = 0; i < size() && !r.is_false(); ++i) 
+            r &= m_bits[i];
+        return r;
+    }
+
 }

src/math/dd/dd_bdd.h

@@ -21,13 +21,18 @@ Revision History:
 #include "util/vector.h"
 #include "util/map.h"
 #include "util/small_object_allocator.h"
+#include "util/rational.h"
 
 namespace dd {
 
     class bdd;
+    class bddv;
+    class test_bdd;
 
     class bdd_manager {
         friend bdd;
+        friend bddv;
+        friend test_bdd;
 
         typedef unsigned BDD;
 
@@ -40,7 +45,8 @@ namespace dd {
             bdd_not_op = 5,
             bdd_and_proj_op = 6,
             bdd_or_proj_op = 7,
-            bdd_no_op = 8,
+	    bdd_cofactor_op = 8,
+            bdd_no_op = 9,
         };
 
         struct bdd_node {
@@ -141,6 +147,7 @@ namespace dd {
         BDD mk_not_rec(BDD b);
         BDD mk_ite_rec(BDD a, BDD b, BDD c);
         BDD mk_quant_rec(unsigned lvl, BDD b, bdd_op op);
+	BDD mk_cofactor_rec(BDD a, BDD b);
 
         void push(BDD b);
         void pop(unsigned num_scopes);
@@ -188,6 +195,7 @@ namespace dd {
         bdd mk_and(bdd const& a, bdd const& b);
         bdd mk_or(bdd const& a, bdd const& b);
         bdd mk_xor(bdd const& a, bdd const& b);
+	bdd mk_cofactor(bdd const& a, bdd const& b);
 
         void reserve_var(unsigned v);
         bool well_formed();
@@ -199,10 +207,13 @@ namespace dd {
             ~scoped_push() { m.m_bdd_stack.shrink(m_size); }
         };
 
+        bool_vector mk_usub(bool_vector const& b);
+
+
     public:
         struct mem_out {};
 
-        bdd_manager(unsigned nodes);
+        bdd_manager(unsigned num_vars);
         ~bdd_manager();
 
         void set_max_num_nodes(unsigned n) { m_max_num_bdd_nodes = n; }
@@ -219,6 +230,39 @@ namespace dd {
         bdd mk_forall(unsigned v, bdd const& b);
         bdd mk_ite(bdd const& c, bdd const& t, bdd const& e);
 
+        /* BDD vector operations
+         * - Fixed-width arithmetic, i.e., modulo 2^size
+         * - The lowest index is the LSB
+         */
+        bdd mk_ule(bddv const& a, bddv const& b);
+        bdd mk_uge(bddv const& a, bddv const& b); // { return mk_ule(b, a); }
+        bdd mk_ult(bddv const& a, bddv const& b); // { return mk_ule(a, b) && !mk_eq(a, b); }
+        bdd mk_ugt(bddv const& a, bddv const& b); // { return mk_ult(b, a); }
+        bdd mk_sle(bddv const& a, bddv const& b);
+        bdd mk_sge(bddv const& a, bddv const& b); // { return mk_sle(b, a); }
+        bdd mk_slt(bddv const& a, bddv const& b); // { return mk_sle(a, b) && !mk_eq(a, b); }
+        bdd mk_sgt(bddv const& a, bddv const& b); // { return mk_slt(b, a); }
+        bdd mk_eq(bddv const& a, bddv const& b);
+        bdd mk_eq(bddv const& a, rational const& v);
+        bdd mk_eq(unsigned_vector const& vars, rational const& v);
+        bddv mk_num(rational const& n, unsigned num_bits);
+        bddv mk_ones(unsigned num_bits);
+        bddv mk_zero(unsigned num_bits);
+        bddv mk_var(unsigned num_bits, unsigned const* vars);
+        bddv mk_var(unsigned_vector const& vars);
+        bddv mk_add(bddv const& a, bddv const& b);
+        bddv mk_add(bddv const& a, std::function<bdd(unsigned)>& get_bit);
+        bddv mk_sub(bddv const& a, bddv const& b);
+        bddv mk_usub(bddv const& a);
+        bddv mk_mul(bddv const& a, bddv const& b);
+        bddv mk_mul(bddv const& a, bool_vector const& b);
+        bddv mk_mul(bddv const& a, rational const& val);
+        bddv mk_concat(bddv const& a, bddv const& b);
+        void mk_quot_rem(bddv const& a, bddv const& b, bddv& quot, bddv& rem);
+        bool is_constv(bddv const& a);
+        rational to_val(bddv const& a);
+
+
         std::ostream& display(std::ostream& out);
         std::ostream& display(std::ostream& out, bdd const& b);
 
@@ -242,14 +286,16 @@ namespace dd {
         unsigned var() const { return m->var(root); }
 
         bool is_true() const { return root == bdd_manager::true_bdd; }
-        bool is_false() const { return root == bdd_manager::false_bdd; }        
+        bool is_false() const { return root == bdd_manager::false_bdd; }
+        bool is_const() const { return is_false() || is_true(); }
 
-        bdd operator!() { return m->mk_not(*this); }
-        bdd operator&&(bdd const& other) { return m->mk_and(*this, other); }
-        bdd operator||(bdd const& other) { return m->mk_or(*this, other); }
-        bdd operator^(bdd const& other) { return m->mk_xor(*this, other); }
+        bdd operator!() const { return m->mk_not(*this); }
+        bdd operator&&(bdd const& other) const { return m->mk_and(*this, other); }
+        bdd operator||(bdd const& other) const { return m->mk_or(*this, other); }
+        bdd operator^(bdd const& other) const { return m->mk_xor(*this, other); }
         bdd operator|=(bdd const& other) { return *this = *this || other; }
         bdd operator&=(bdd const& other) { return *this = *this && other; }
+	bdd cofactor(bdd const& cube) { return m->mk_cofactor(*this, cube); }
         std::ostream& display(std::ostream& out) const { return m->display(out, *this); }
         bool operator==(bdd const& other) const { return root == other.root; }
         bool operator!=(bdd const& other) const { return root != other.root; }
@@ -260,6 +306,79 @@ namespace dd {
 
     std::ostream& operator<<(std::ostream& out, bdd const& b);
 
+    class bddv {
+        friend bdd_manager;
+
+        vector<bdd>  m_bits;
+        bdd_manager* m;
+
+        bddv(vector<bdd> const& bits, bdd_manager* m): m_bits(bits), m(m) { SASSERT(m); }
+        bddv(vector<bdd>&& bits, bdd_manager* m): m_bits(std::move(bits)), m(m) { SASSERT(m); }
+
+        bddv(bdd_manager* m): m_bits(), m(m) { SASSERT(m); }
+        bdd const& operator[](unsigned i) const { return m_bits[i]; }
+        bdd& operator[](unsigned i) { return m_bits[i]; }
+        void push_back(bdd const& a) { m_bits.push_back(a); }
+        void push_back(bdd&& a) { m_bits.push_back(std::move(a)); }
+        void shl();
+        void shr();
+
+    public:
+        unsigned size() const { return m_bits.size(); }
+        vector<bdd> const& bits() const { return m_bits; }
+
+        /* unsigned comparison operators */
+        bdd operator<=(bddv const& other) const { return m->mk_ule(*this, other); }  ///< unsigned comparison
+        bdd operator>=(bddv const& other) const { return m->mk_uge(*this, other); }  ///< unsigned comparison
+        bdd operator< (bddv const& other) const { return m->mk_ult(*this, other); }  ///< unsigned comparison
+        bdd operator> (bddv const& other) const { return m->mk_ugt(*this, other); }  ///< unsigned comparison
+        bdd operator<=(rational const& other) const { return m->mk_ule(*this, m->mk_num(other, size())); }  ///< unsigned comparison
+        bdd operator>=(rational const& other) const { return m->mk_uge(*this, m->mk_num(other, size())); }  ///< unsigned comparison
+        bdd operator< (rational const& other) const { return m->mk_ult(*this, m->mk_num(other, size())); }  ///< unsigned comparison
+        bdd operator> (rational const& other) const { return m->mk_ugt(*this, m->mk_num(other, size())); }  ///< unsigned comparison
+
+        /* signed comparison operators */
+        bdd sle(bddv const& other) const { return m->mk_sle(*this, other); }
+        bdd sge(bddv const& other) const { return m->mk_sge(*this, other); }
+        bdd slt(bddv const& other) const { return m->mk_slt(*this, other); }
+        bdd sgt(bddv const& other) const { return m->mk_sgt(*this, other); }
+
+        bdd all0() const;        
+        bdd all1() const;
+
+        bdd operator==(bddv const& other) const { return m->mk_eq(*this, other); }
+        bdd operator==(rational const& other) const { return m->mk_eq(*this, other); }
+        bdd operator!=(bddv const& other) const { return !m->mk_eq(*this, other); }
+        bdd operator!=(rational const& other) const { return !m->mk_eq(*this, other); }
+
+        bddv operator+(bddv const& other) const { return m->mk_add(*this, other); }
+        bddv operator+(rational const& other) const { return m->mk_add(*this, m->mk_num(other, size())); }
+        bddv operator-(bddv const& other) const { return m->mk_sub(*this, other); }
+        bddv operator-(rational const& other) const { return m->mk_sub(*this, m->mk_num(other, size())); }
+        bddv rev_sub(rational const& other) const { return m->mk_sub(m->mk_num(other, size()), *this); }
+        bddv operator*(bddv const& other) const { return m->mk_mul(*this, other); }
+        bddv operator*(rational const& other) const { return m->mk_mul(*this, other); }
+        bddv operator*(bool_vector const& other) const { return m->mk_mul(*this, other); }
+        bddv append(bddv const& other) const { return m->mk_concat(*this, other); }
+        void quot_rem(bddv const& divisor, bddv& quot, bddv& rem) const { m->mk_quot_rem(*this, divisor, quot, rem); }
+
+        bool is_const() const { return m->is_constv(*this); }
+        rational to_val() const { return m->to_val(*this); }
+    };
+
+    inline bdd operator<=(rational const& r, bddv const& a) { return a >= r; }  ///< unsigned comparison
+    inline bdd operator>=(rational const& r, bddv const& a) { return a <= r; }  ///< unsigned comparison
+    inline bdd operator< (rational const& r, bddv const& a) { return a > r; }  ///< unsigned comparison
+    inline bdd operator> (rational const& r, bddv const& a) { return a < r; }  ///< unsigned comparison
+    inline bdd operator==(rational const& r, bddv const& a) { return a == r; }
+    inline bdd 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 + 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

@@ -0,0 +1,366 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    dd_fdd
+
+Abstract:
+
+    Finite domain abstraction for using BDDs as sets of integers, inspired by BuDDy's fdd module.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-04-20
+    Jakob Rath 2021-04-20
+
+--*/
+
+#include "math/dd/dd_fdd.h"
+
+namespace dd {
+
+    fdd::fdd(bdd_manager& manager, unsigned_vector&& vars)
+        : m_pos2var(std::move(vars))
+        , m_var2pos()
+        , m(&manager)
+        , m_var(manager.mk_var(m_pos2var))
+    {
+        for (unsigned pos = 0; pos < m_pos2var.size(); ++pos) {
+            unsigned const var = m_pos2var[pos];
+            while (var >= m_var2pos.size())
+                m_var2pos.push_back(UINT_MAX);
+            m_var2pos[var] = pos;
+        }
+    }
+
+    bdd fdd::non_zero() const {
+        bdd non_zero = m->mk_false();
+        for (unsigned var : m_pos2var) {
+            non_zero |= m->mk_var(var);
+        }
+        return non_zero;
+    }
+
+    unsigned fdd::var2pos(unsigned var) const {
+        return var < m_var2pos.size() ? m_var2pos[var] : UINT_MAX;
+    }
+
+    bool fdd::contains(bdd b, rational const& val) const {
+        while (!b.is_const()) {
+            unsigned const pos = var2pos(b.var());
+            SASSERT(pos != UINT_MAX && "Unexpected BDD variable");
+            b = val.get_bit(pos) ? b.hi() : b.lo();
+        }
+        return b.is_true();
+    }
+
+    find_t fdd::find(bdd b, rational& out_val) const {
+        return find_hint(b, rational::zero(), out_val);
+    }
+
+    find_t fdd::find_hint(bdd b, rational const& hint, rational& out_val) const {
+        out_val = 0;
+        if (b.is_false())
+            return find_t::empty;
+        bool is_unique = true;
+        bool hint_ok = !hint.is_zero();  // since we choose the 'lo' branch by default, we don't need to check the hint when it is 0.
+        unsigned num_vars = 0;
+        while (!b.is_true()) {
+            ++num_vars;
+            unsigned const pos = var2pos(b.var());
+            SASSERT(pos != UINT_MAX && "Unexpected BDD variable");
+
+            bool go_hi = false;
+            if (b.lo().is_false()) {
+                go_hi = true;
+                if (hint_ok && !hint.get_bit(pos))
+                    hint_ok = false;
+            }
+            else if (b.hi().is_false()) {
+                if (hint_ok && hint.get_bit(pos))
+                    hint_ok = false;
+            }
+            else {
+                // This is the only case where we have a choice
+                // => follow the hint
+                SASSERT(!b.lo().is_false() && !b.hi().is_false());
+                is_unique = false;
+                if (hint_ok && hint.get_bit(pos))
+                    go_hi = true;
+            }
+
+            if (go_hi) {
+                out_val += rational::power_of_two(pos);
+                b = b.hi();
+            }
+            else
+                b = b.lo();
+        }
+        if (num_vars != num_bits())
+            is_unique = false;
+        // If a variable corresponding to a 1-bit in hint does not appear in the BDD,
+        // out_val is wrong at this point, so we set it explicitly.
+        if (hint_ok)
+            out_val = hint;
+        // TODO: instead of computing out_val incrementally, we could mark the visited 'hi'-positions and only compute out_val from the marks when !hint_ok.
+        return is_unique ? find_t::singleton : find_t::multiple;
+    }
+
+    std::ostream& operator<<(std::ostream& out, find_t x) {
+        switch (x) {
+        case find_t::empty:
+            return out << "empty";
+        case find_t::singleton:
+            return out << "singleton";
+        case find_t::multiple:
+            return out << "multiple";
+        }
+        UNREACHABLE();
+        return out;
+    }
+
+    bool fdd::contains(bdd const& x, bool_vector const& value) const {
+	bdd b = x;
+	while (!b.is_true()) {
+	    unsigned const pos = var2pos(b.var());
+            SASSERT(pos != UINT_MAX && "Unexpected BDD variable");
+	    if (value[pos] && b.hi().is_false())
+		return false;
+	    if (!value[pos] && b.lo().is_false())
+		return false;	    
+	    if (value[pos])
+		b = b.hi();
+	    else
+		b = b.lo();
+	}
+        return true;
+    }
+
+
+    // subtract one from x
+    static void dec(bool_vector& x) {
+        for (auto& b : x) {
+            b = !b;
+            if (!b)
+                break;
+        }
+    }
+
+    // add one to x
+    static void inc(bool_vector& x) {
+        for (auto& b : x) {
+            b = !b;
+            if (b)
+                break;
+        }
+    }
+
+    static void reset(bool_vector& x, bool value) {
+        for (auto& b : x)
+            b = value;
+    }
+
+  
+    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
+	// after re-ordering. Then co-factoring is relatively cheap.
+	//
+
+        if (!contains(x, lo))
+            return false;
+
+        //
+        // find minimal index where b is false for some 
+        // value larger than lo.
+        //
+        // Let ua(x lo) be shorthand for "unbounded-above" of variable
+        // x with bit-string lo.
+        // 
+        // we have the following identities:
+        // ua(_ []) = true
+        // ua(x 1 ++ lo) = hi(x) = T or ua(hi(x), lo)
+        // ua(x 0 ++ lo) = hi(x) = T and ua(lo(x), lo)
+        // 
+        // the least significant bit where ua is false
+        // represents the position where the smallest number above
+        // lo resides that violates x.
+
+        unsigned idx = UINT_MAX;
+        vector<bdd> trail;
+        bdd b = x;
+        for (unsigned i = lo.size(); i-- > 0; ) {
+            trail.push_back(b);
+            unsigned v = m_pos2var[i];
+            bdd w = m->mk_var(v);
+            bdd hi = b.cofactor(w);
+            if (lo[i]) {
+                if (hi.is_true())
+                    break;
+                SASSERT(!hi.is_false());
+                b = hi;
+            }
+            else {
+                if (!hi.is_true())
+                    idx = i;
+                b = b.cofactor(m->mk_nvar(v));
+            }
+        }
+        if (idx == UINT_MAX) {
+            // all values above lo satisfy x
+            reset(lo, true);
+            return true;
+        }
+
+        SASSERT(!lo[idx]);
+        lo[idx] = true;
+        unsigned v = m_pos2var[idx];
+        b = trail[lo.size() - idx - 1].cofactor(m->mk_var(v));
+        for (unsigned i = idx; i-- > 0; ) {
+            SASSERT(!b.is_true());
+            if (b.is_false()) {
+                for (unsigned j = 0; j <= i; ++j)
+                    lo[j] = false;
+                break;
+            }
+            lo[i] = b.lo().is_true();
+            if (lo[i]) 
+                b = b.hi();
+            else 
+                b = b.lo();
+        }
+
+        dec(lo);
+        
+	    return true;
+    }
+    
+    bool fdd::inf(bdd const& x, bool_vector& hi) const {
+        SASSERT(hi.size() == num_bits());
+        if (!contains(x, hi))
+            return false;
+
+        // Let ub(x hi) be shorthand for "unbounded-below" of variable
+        // x with bit-string hi.
+        // 
+        // we have the following identities:
+        // ub(_ []) = true
+        // ub(x 0 ++ hi) = lo(x) = T or ub(lo(x), hi)
+        // ub(x 1 ++ hi) = lo(x) = T and ub(hi(x), hi)
+        // 
+
+        unsigned idx = UINT_MAX;
+        vector<bdd> trail;
+        bdd b = x;
+        for (unsigned i = hi.size(); i-- > 0; ) {
+            trail.push_back(b);
+            unsigned v = m_pos2var[i];
+            bdd nw = m->mk_nvar(v);
+            bdd lo = b.cofactor(nw);
+            if (!hi[i]) {
+                if (lo.is_true())
+                    break;
+                SASSERT(!lo.is_false());
+                b = lo;
+            }
+            else {
+                if (!lo.is_true())
+                    idx = i;
+                b = b.cofactor(m->mk_var(v));
+            }
+        }
+        if (idx == UINT_MAX) {
+            // all values below hi satisfy x
+            reset(hi, false);
+            return true;
+        }
+
+        SASSERT(hi[idx]);
+        hi[idx] = false;
+        unsigned v = m_pos2var[idx];
+        b = trail[hi.size() - idx - 1].cofactor(m->mk_nvar(v));
+
+        for (unsigned i = idx; i-- > 0; ) {
+            SASSERT(!b.is_true());
+            if (b.is_false()) {
+                for (unsigned j = 0; j <= i; ++j)
+                    hi[j] = true;
+                break;
+            }
+            hi[i] = !b.hi().is_true();
+            if (!hi[i]) 
+                b = b.lo();
+            else 
+                b = b.hi();
+        }
+
+        inc(hi);
+
+        return true;
+    }
+
+    bool_vector fdd::rational2bits(rational const& r) const {
+        bool_vector result;
+        for (unsigned i = 0; i < num_bits(); ++i)
+            result.push_back(r.get_bit(i));
+        return result;
+    }
+
+    rational fdd::bits2rational(bool_vector const& v) const {
+        rational result(0);
+        for (unsigned i = 0; i < num_bits(); ++i)
+            if (v[i])
+                result += rational::power_of_two(i);
+        return result;
+    }
+
+    bool fdd::sup(bdd const& b, rational& _lo) const {
+        bool_vector lo = rational2bits(_lo);
+        if (!sup(b, lo))
+            return false;
+        _lo = bits2rational(lo);
+        return true;
+    }
+    
+    bool fdd::inf(bdd const& b, rational& _hi) const {
+        bool_vector hi = rational2bits(_hi);
+        if (!inf(b, hi))
+            return false;
+        _hi = bits2rational(hi);
+        return true;
+    }
+
+    rational fdd::max(bdd b) const {
+        SASSERT(!b.is_false());
+        rational result(0);
+        for (unsigned i = num_bits(); i-- > 0; ) {
+            unsigned v = m_pos2var[i];
+            bdd w = m->mk_var(v);
+            bdd hi = b.cofactor(w);
+            if (!hi.is_false()) {
+                b = hi;
+                result += rational::power_of_two(i);
+            }
+        }
+        return result;
+    }
+
+    rational fdd::min(bdd b) const {
+        SASSERT(!b.is_false());
+        rational result(0);
+        for (unsigned i = num_bits(); i-- > 0; ) {
+            unsigned v = m_pos2var[i];
+            bdd nw = m->mk_nvar(v);
+            bdd lo = b.cofactor(nw);
+            if (lo.is_false())
+                result += rational::power_of_two(i);
+            else
+                b = lo;
+        }
+        return result;
+    }
+
+
+}

src/math/dd/dd_fdd.h

@@ -0,0 +1,108 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    dd_fdd
+
+Abstract:
+
+    Finite domain abstraction for using BDDs as sets of integers, inspired by BuDDy's fdd module.
+
+Author:
+
+    Jakob Rath 2021-04-20
+    Nikolaj Bjorner (nbjorner) 2021-04-20
+
+--*/
+#pragma once
+
+#include "math/dd/dd_bdd.h"
+#include "util/vector.h"
+#include "util/rational.h"
+
+namespace dd {
+
+    enum class find_t { empty, singleton, multiple };
+    std::ostream& operator<<(std::ostream& out, find_t x);
+
+    /**
+     * Finite domain abstraction over BDDs.
+     */
+    class fdd {
+        unsigned_vector m_pos2var;  // pos -> BDD var
+        unsigned_vector m_var2pos;  // var -> pos (pos = place number in the bit representation, 0 is LSB's place)
+        bdd_manager*    m;
+        bddv            m_var;
+
+        static unsigned_vector seq(unsigned count, unsigned start = 0, unsigned step = 1) {
+            unsigned_vector result;
+            unsigned k = start;
+            for (unsigned i = 0; i < count; ++i, k += step)
+                result.push_back(k);
+            return result;
+        }
+
+        unsigned var2pos(unsigned var) const;
+
+        bool contains(bdd const& b, bool_vector const& value) const;
+
+        rational bits2rational(bool_vector const& v) const;
+
+        bool_vector rational2bits(rational const& r) const;
+
+    public:
+        /** Initialize FDD using BDD variables from 0 to num_bits-1. */
+        fdd(bdd_manager& manager, unsigned num_bits, unsigned start = 0, unsigned step = 1) : fdd(manager, seq(num_bits, start, step)) { }
+        fdd(bdd_manager& manager, unsigned_vector const& vars) : fdd(manager, unsigned_vector(vars)) { }
+        fdd(bdd_manager& manager, unsigned_vector&& vars);
+
+        unsigned num_bits() const { return m_pos2var.size(); }
+        unsigned_vector const& bdd_vars() const { return m_pos2var; }
+
+        bddv const& var() const { return m_var; }
+
+        /** Equivalent to var() != 0 */
+        bdd non_zero() const;
+
+        /** Checks whether the integer val is contained in the BDD when viewed as set of integers.
+         * Precondition: the bdd only contains variables managed by this fdd.
+         */
+        bool contains(bdd b, rational const& val) const;
+
+        /** Returns an integer contained in the BDD, if any, and whether the BDD is a singleton.
+         * Precondition: the bdd only contains variables managed by this fdd.
+         */
+        find_t find(bdd b, rational& out_val) const;
+
+        /** Like find, but returns hint if it is contained in the BDD. */
+        find_t find_hint(bdd b, rational const& hint, rational& out_val) const;
+
+        /*
+         * find largest value at lo or above such that bdd b evaluates to true
+         * at lo and all values between.
+         * dually, find smallest value below hi that evaluates b to true
+         * and all values between the value and hi also evaluate b to true.
+         * \param b - a bdd using variables from this
+         * \param lo/hi - bound to be traversed.
+         * \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) const;
+
+        bool inf(bdd const& b, bool_vector& hi) const;
+
+        bool sup(bdd const& b, rational& lo) const;
+
+        bool inf(bdd const& b, rational& hi) const;
+
+        /*
+        * Find the min-max satisfying assignment.
+        * \pre b is not false.
+        */
+        rational max(bdd b) const;
+
+        rational min(bdd b) const;
+    };
+
+}