adding bdd package

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

src/sat/sat_bdd.cpp

@@ -32,10 +32,16 @@ namespace sat {
             }
         }
         // add two dummy nodes for true_bdd and false_bdd
-        m_nodes.push_back(bdd_node(0,0,0));
+        for (unsigned i = 0; i <= bdd_no_op; ++i) {
-        m_nodes.push_back(bdd_node(0,0,0));
+            m_nodes.push_back(bdd_node(0,0,0));
-        m_nodes[0].m_refcount = max_rc;
+            m_nodes.back().m_refcount = max_rc;
-        m_nodes[1].m_refcount = max_rc;
+            m_nodes.back().m_index = m_nodes.size()-1;
+        }
+
+        m_spare_entry = nullptr;
+        m_max_num_bdd_nodes = 1 << 24; // up to 16M nodes
+        m_mark_level = 0;
+        alloc_free_nodes(1024);
         
         // add variables
         for (unsigned i = 0; i < num_vars; ++i) {
@@ -46,27 +52,43 @@ namespace sat {
             m_var2level.push_back(i);
             m_level2var.push_back(i);
         }            
-        
-        m_spare_entry = nullptr;
     }
 
-    bdd_manager::BDD bdd_manager::apply_const(BDD a, BDD b, bdd_op op) {
+    bdd_manager::~bdd_manager() {
-        switch (op) {
+        if (m_spare_entry) {
-        case bdd_and_op:
+            m_alloc.deallocate(sizeof(*m_spare_entry), m_spare_entry);
-            return (a == 1 && b == 1) ? 1 : 0;
+        }
-        case bdd_or_op:
+        for (auto* e : m_op_cache) {
-            return (a == 1 || b == 1) ? 1 : 0;
+            m_alloc.deallocate(sizeof(*e), e);
-        case bdd_iff_op:
-            return (a == b) ? 1 : 0;
-        default:
-            UNREACHABLE();
-            return 0;
         }
     }
     
+    bdd_manager::BDD bdd_manager::apply_const(BDD a, BDD b, bdd_op op) {
+        SASSERT(is_const(a) && is_const(b));
+        switch (op) {
+        case bdd_and_op:
+            return (a == true_bdd && b == true_bdd) ? true_bdd : false_bdd;
+        case bdd_or_op:
+            return (a == true_bdd || b == true_bdd) ? true_bdd : false_bdd;
+        case bdd_iff_op:
+            return (a == b) ? true_bdd : false_bdd;
+        default:
+            return false_bdd;
+        }
+    }
 
     bdd_manager::BDD bdd_manager::apply(BDD arg1, BDD arg2, bdd_op op) {
-        return apply_rec(arg1, arg2, op);
+        bool first = true;
+        while (true) {
+            try {
+                return apply_rec(arg1, arg2, op);
+            }
+            catch (bdd_exception) {
+                try_reorder();
+                if (!first) throw;
+                first = false;
+            }
+        }
     }
 
     bdd_manager::BDD bdd_manager::apply_rec(BDD a, BDD b, bdd_op op) {
@@ -95,11 +117,17 @@ namespace sat {
         if (is_const(a) && is_const(b)) {
             return m_apply_const[a + 2*b + 4*op];
         }
-        cache_entry * e1 = pop_entry(hash2(a, b, op));
+        op_entry * e1 = pop_entry(a, b, op);
-        cache_entry const* e2 = m_cache.insert_if_not_there(e1);
+        op_entry const* e2 = m_op_cache.insert_if_not_there(e1);
-        if (e2->m_op == op && e2->m_bdd1 == a && e2->m_bdd2 == b) {
+        if (e2 != e1) {
-            push_entry(e1);
+            if (e2->m_bdd1 == a && e2->m_bdd2 == b && e2->m_op == op) {
-            return e2->m_result;
+                push_entry(e1);
+                return e2->m_result;
+            }
+            e1 = const_cast<op_entry*>(e2);
+            e1->m_bdd1 = a;
+            e1->m_bdd2 = b;
+            e1->m_op = op;
         }
         BDD r;
         if (level(a) == level(b)) {
@@ -107,7 +135,7 @@ namespace sat {
             push(apply_rec(hi(a), hi(b), op));
             r = make_node(level(a), read(2), read(1));
         }
-        else if (level(a) < level(b)) {
+        else if (level(a) > level(b)) {
             push(apply_rec(lo(a), b, op));
             push(apply_rec(hi(a), b, op));
             r = make_node(level(a), read(2), read(1));
@@ -117,10 +145,8 @@ namespace sat {
             push(apply_rec(a, hi(b), op));
             r = make_node(level(b), read(2), read(1));
         }
+        pop(2);
         e1->m_result = r;
-        e1->m_bdd1 = a;
-        e1->m_bdd2 = b;
-        e1->m_op = op;
         return r;
     }
 
@@ -136,47 +162,64 @@ namespace sat {
         return m_bdd_stack[m_bdd_stack.size() - index];
     }
 
-
+    bdd_manager::op_entry* bdd_manager::pop_entry(BDD l, BDD r, BDD op) {
-    bdd_manager::cache_entry* bdd_manager::pop_entry(unsigned hash) {
+        op_entry* result = nullptr;
-        cache_entry* result = 0;
         if (m_spare_entry) {
             result = m_spare_entry;
-            m_spare_entry = 0;
+            m_spare_entry = nullptr;
-            result->m_hash = hash;
+            result->m_bdd1 = l;
+            result->m_bdd2 = r;
+            result->m_op = op;
         }
         else {
-            void * mem = m_alloc.allocate(sizeof(cache_entry));
+            void * mem = m_alloc.allocate(sizeof(op_entry));
-            result = new (mem) cache_entry(hash);
+            result = new (mem) op_entry(l, r, op);
         }
+        result->m_result = -1;
         return result;
     }
 
-    void bdd_manager::push_entry(cache_entry* e) {
+    void bdd_manager::push_entry(op_entry* e) {
         SASSERT(!m_spare_entry);
         m_spare_entry = e;
     }
 
-
     bdd_manager::BDD bdd_manager::make_node(unsigned level, BDD l, BDD r) {
         if (l == r) {
             return l;
         }
-#if 0
+
+        bdd_node n(level, l, r);
+        node_table::entry* e = m_node_table.insert_if_not_there2(n);
+        if (e->get_data().m_index != 0) {
+            return e->get_data().m_index;
+        }
+        e->get_data().m_refcount = 0;
+        if (m_free_nodes.empty()) {
+            gc();
+            e = m_node_table.insert_if_not_there2(n);
+            e->get_data().m_refcount = 0;
+        }
+        if (m_free_nodes.empty()) {
+            if (m_nodes.size() > m_max_num_bdd_nodes) {
+                throw bdd_exception();
+            }
+            e->get_data().m_index = m_nodes.size();
+            m_nodes.push_back(e->get_data());
+            alloc_free_nodes(m_nodes.size()/2);
+        }
+        else {
+            e->get_data().m_index = m_free_nodes.back();
+            m_nodes[e->get_data().m_index] = e->get_data();
+            m_free_nodes.pop_back();
+        }
+        return e->get_data().m_index;
+    }
+
+    void bdd_manager::try_reorder() {
         // TBD
-        unsigned hash = node_hash(level, l, r);
-        bdd result = m_
-#endif
-        int sz = m_nodes.size();
-        m_nodes.push_back(bdd_node(level, l, r));        
-        return sz;
     }
 
-#if 0
-    void bdd_manager::bdd_reorder(int) {
-        
-    }
-#endif
-
     bdd bdd_manager::mk_var(unsigned i) {
         return bdd(m_var2bdd[2*i+1], this);        
     }
@@ -185,76 +228,301 @@ namespace sat {
         return bdd(m_var2bdd[2*i+1], this);
     }
 
-    unsigned bdd_manager::hash2(BDD a, BDD b, bdd_op op) const {
-        return mk_mix(a, b, op);
-    }
-
     bdd bdd_manager::mk_not(bdd b) {
-        return bdd(mk_not_rec(b.root), this);
+        bool first = true;
+        while (true) {
+            try {
+                return bdd(mk_not_rec(b.root), this);
+            }
+            catch (bdd_exception) {
+                try_reorder();
+                if (!first) throw;
+                first = false;
+            }
+        }
     }
 
     bdd_manager::BDD bdd_manager::mk_not_rec(BDD b) {
         if (is_true(b)) return false_bdd;
         if (is_false(b)) return true_bdd;
-        cache_entry* e1 = pop_entry(hash1(b, bdd_not_op));
+        op_entry* e1 = pop_entry(b, b, bdd_not_op);
-        cache_entry const* e2 = m_cache.insert_if_not_there(e1);
+        op_entry const* e2 = m_op_cache.insert_if_not_there(e1);
-        if (e2->m_bdd1 == b && e2->m_op == bdd_not_op) {
+        if (e2 != e1) {
-            push_entry(e1);
+            if (e2->m_bdd1 == b && e2->m_bdd2 == b && e2->m_op == bdd_not_op) {
-            return e2->m_result;
+                push_entry(e1);
+                return e2->m_result;
+            }
+            e1 = const_cast<op_entry*>(e2);
+            e1->m_bdd1 = b;
+            e1->m_bdd2 = b;
+            e1->m_op = bdd_not_op;
         }
         push(mk_not_rec(lo(b)));
         push(mk_not_rec(hi(b)));
         BDD r = make_node(level(b), read(2), read(1));
         pop(2);
-        e1->m_bdd1 = b;
-        e1->m_bdd2 = b;
-        e1->m_op = bdd_not_op;
         e1->m_result = r;
         return r;
     }
 
-#if 0
+    bdd bdd_manager::mk_ite(bdd const& c, bdd const& t, bdd const& e) { 
-    bdd bdd_manager::mk_exists(bdd vars, bdd b) {
+        bool first = true;
+        while (true) {
+            try {
+                return bdd(mk_ite_rec(c.root, t.root, e.root), this); 
+            }
+            catch (bdd_exception) {
+                try_reorder();
+                if (!first) throw;
+                first = false;
+            }
+        }
+    }
+
+    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);
+        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);
+        if (e2 != e1) {
+            if (e2->m_bdd1 == a && e2->m_bdd2 == b && e2->m_op == c) {
+                push_entry(e1);
+                return e2->m_result;
+            }
+            e1 = const_cast<op_entry*>(e2);
+            e1->m_bdd1 = a;
+            e1->m_bdd2 = b;
+            e1->m_op = c;
+        }
+        unsigned la = level(a), lb = level(b), lc = level(c);
+        BDD r;
+        BDD a1, b1, c1, a2, b2, c2;
+        unsigned lvl = la;
+        if (la >= lb && la >= lc) {
+            a1 = lo(a), a2 = hi(a);
+            lvl = la;
+        }
+        else {
+            a1 = a, a2 = a;
+        }
+        if (lb >= la && lb >= lc) {
+            b1 = lo(b), b2 = hi(b);
+            lvl = lb;
+        }
+        else {
+            b1 = b, b2 = b;
+        }
+        if (lc >= la && lc >= lb) {
+            c1 = lo(c), c2 = hi(c);
+            lvl = lc;
+        }
+        else {
+            c1 = c, c2 = c;
+        }
+        push(mk_ite_rec(a1, b1, c1));
+        push(mk_ite_rec(a2, b2, c2));
+        r = make_node(lvl, read(2), read(1));
+        pop(2);                   
+        e1->m_result = r;
+        return r;
+    }
+
+    bdd bdd_manager::mk_exists(unsigned n, unsigned const* vars, bdd const& b) {
+        return bdd(mk_quant(n, vars, b.root, bdd_or_op), this);
+    }
+
+    bdd bdd_manager::mk_forall(unsigned n, unsigned const* vars, bdd const& b) {
+        return bdd(mk_quant(n, vars, b.root, bdd_and_op), this);
+    }
+
+    bdd_manager::BDD bdd_manager::mk_quant(unsigned n, unsigned const* vars, BDD b, bdd_op op) {
+        BDD result = b;
+        for (unsigned i = 0; i < n; ++i) {
+            result = mk_quant_rec(m_var2level[vars[i]], result, op);
+        }
+        return result;
+    }
+
+    bdd_manager::BDD bdd_manager::mk_quant_rec(unsigned l, BDD b, bdd_op op) {
+        unsigned lvl = level(b);
+        
+        if (lvl == l) {
+            return apply(lo(b), hi(b), op);
+        }
+        else if (lvl < l) {
+            return b;
+        }
+        else {
+            BDD a = level2bdd(l);
+            bdd_op q_op = op == bdd_and_op ? bdd_and_proj_op : bdd_or_proj_op;
+            op_entry * e1 = pop_entry(a, b, q_op);
+            op_entry const* e2 = m_op_cache.insert_if_not_there(e1);
+            if (e1 != e2) {
+                if (e2->m_bdd1 == a && e2->m_bdd2 == b && e2->m_op == q_op) {
+                    push_entry(e1);
+                    return e2->m_result;
+                }
+                e1 = const_cast<op_entry*>(e2);
+                e1->m_bdd1 = a;
+                e1->m_bdd2 = b;
+                e1->m_op = q_op;
+            }
+            push(mk_quant_rec(l, lo(b), op));
+            push(mk_quant_rec(l, hi(b), op));
+            BDD r = make_node(lvl, read(2), read(1));
+            pop(2);
+            e1->m_result = r;
+            return r;
+        }
+    }
+
+    double bdd_manager::path_count(bdd const& b) {
+        init_mark();
+        m_path_count.resize(m_nodes.size());
+        m_path_count[0] = 0;
+        m_path_count[1] = 1;
+        set_mark(0);
+        set_mark(1);
+        m_todo.push_back(b.root);
+        while (!m_todo.empty()) {
+            BDD r = m_todo.back();
+            if (is_marked(r)) {
+                m_todo.pop_back();
+            }
+            else if (!is_marked(lo(r))) {
+                m_todo.push_back(lo(r));
+            }
+            else if (!is_marked(hi(r))) {
+                m_todo.push_back(hi(r));
+            }
+            else {
+                m_path_count[r] = m_path_count[lo(r)] + m_path_count[hi(r)];
+                set_mark(r);
+                m_todo.pop_back();
+            }
+        }
+        return m_path_count[b.root];
 
     }
 
-    bdd bdd_manager::mk_forall(bdd vars, bdd b) {
+    void bdd_manager::alloc_free_nodes(unsigned n) {
-
+        for (unsigned i = 0; i < n; ++i) {
+            m_free_nodes.push_back(m_nodes.size());
+            m_nodes.push_back(bdd_node());
+            m_nodes.back().m_index = m_nodes.size() - 1;
+        }
+        m_free_nodes.reverse();
     }
 
-    bdd bdd_manager::mk_ite(bdd c, bdd t, bdd e) {
+    void bdd_manager::gc() {
-
+        IF_VERBOSE(1, verbose_stream() << "(bdd :gc " << m_nodes.size() << ")\n";);
+        SASSERT(m_free_nodes.empty());
+        svector<bool> reachable(m_nodes.size(), false);
+        for (unsigned i = m_bdd_stack.size(); i-- > 0; ) {
+            reachable[m_bdd_stack[i]] = true;
+            m_todo.push_back(m_bdd_stack[i]);
+        }
+        for (unsigned i = m_nodes.size(); i-- > 2; ) {
+            if (m_nodes[i].m_refcount > 0) {
+                reachable[i] = true;
+                m_todo.push_back(i);
+            }
+        }
+        while (!m_todo.empty()) {
+            BDD b = m_todo.back();
+            m_todo.pop_back();
+            SASSERT(reachable[b]);
+            if (is_const(b)) continue;
+            if (!reachable[lo(b)]) {
+                reachable[lo(b)] = true;
+                m_todo.push_back(lo(b));
+            }
+            if (!reachable[hi(b)]) {
+                reachable[hi(b)] = true;
+                m_todo.push_back(hi(b));
+            }
+        }
+        for (unsigned i = m_nodes.size(); i-- > 2; ) {
+            if (!reachable[i]) {
+                m_free_nodes.push_back(i);                
+            }
+        }
+        for (auto* e : m_op_cache) {
+            m_alloc.deallocate(sizeof(*e), e);
+        }
+        m_op_cache.reset();
+        m_node_table.reset();
+        // re-populate node cache
+        for (unsigned i = m_nodes.size(); i-- > 2; ) {
+            if (reachable[i]) {
+                SASSERT(m_nodes[i].m_index == i);
+                m_node_table.insert(m_nodes[i]);
+            }
+        }
     }
 
-    double bdd_manager::path_count(bdd b) {
+    void bdd_manager::init_mark() {
-
+        m_mark.resize(m_nodes.size());
+        ++m_mark_level;
+        if (m_mark_level == 0) {
+            m_mark.fill(0);
+        }
     }
 
-#endif
+    std::ostream& bdd_manager::display(std::ostream& out, bdd const& b) {
-
+        init_mark();
-    std::ostream& bdd_manager::display(std::ostream& out, bdd b) {
+        m_todo.push_back(b.root);
-    
+        while (!m_todo.empty()) {
+            BDD r = m_todo.back();
+            if (is_marked(r)) {
+                m_todo.pop_back();
+            }
+            else if (lo(r) == 0 && hi(r) == 0) {
+                set_mark(r);
+                m_todo.pop_back();
+            }
+            else if (!is_marked(lo(r))) {
+                m_todo.push_back(lo(r));
+            }
+            else if (!is_marked(hi(r))) {
+                m_todo.push_back(hi(r));
+            }
+            else {
+                out << r << " : " << var(r) << " " << lo(r) << " " << hi(r) << "\n";
+                set_mark(r);
+                m_todo.pop_back();
+            }
+        }
         return out;
     }
 
     std::ostream& bdd_manager::display(std::ostream& out) {
-
+        for (unsigned i = 0; i < m_nodes.size(); ++i) {
+            bdd_node const& n = m_nodes[i];
+            if (n.m_lo == 0 && n.m_hi == 0) continue;
+            out << i << " : " << m_level2var[n.m_level] << " " << n.m_lo << " " << n.m_hi << "\n";
+        }
         return out;
     }
 
-    bdd::bdd(int root, bdd_manager* m):
+    bdd::bdd(int root, bdd_manager* m): root(root), m(m) { m->inc_ref(root); }
-        root(root), m(m) { 
-        m->inc_ref(root); 
-    }
-
     bdd::bdd(bdd & other): root(other.root), m(other.m) { m->inc_ref(root); }
+    bdd::~bdd() { m->dec_ref(root); }
+    bdd bdd::operator!() { return m->mk_not(*this); }
+    bdd bdd::operator&&(bdd const& other) { return m->mk_and(*this, other); }
+    bdd bdd::operator||(bdd const& other) { return m->mk_or(*this, other); }
+    std::ostream& bdd::display(std::ostream& out) const {  return m->display(out, *this);  }
 
-
+    std::ostream& operator<<(std::ostream& out, bdd const& b) {
-    bdd::~bdd() {
+        return b.display(out);
-        m->dec_ref(root);
     }
 
-#if 0
+
-#endif
 
 }

src/sat/sat_bdd.h

@@ -42,20 +42,29 @@ namespace sat {
     public:
         bdd(bdd & other);
         ~bdd();        
-        // bdd operator!() { return m->mk_not(*this); }
+        bdd operator!();
+        bdd operator&&(bdd const& other);
+        bdd operator||(bdd const& other);
+        std::ostream& display(std::ostream& out) const;
+        bool operator==(bdd const& other) const { return root == other.root; }
+        bool operator!=(bdd const& other) const { return root != other.root; }
     };
 
+    std::ostream& operator<<(std::ostream& out, bdd const& b);
+
     class bdd_manager {
         friend bdd;
 
         typedef int BDD;
 
         enum bdd_op {
-            bdd_and_op = 0,
+            bdd_and_op = 2,
-            bdd_or_op,
+            bdd_or_op = 3,
-            bdd_iff_op,
+            bdd_iff_op = 4,
-            bdd_not_op,
+            bdd_not_op = 5,
-            bdd_no_op
+            bdd_and_proj_op = 6,
+            bdd_or_proj_op = 7,
+            bdd_no_op = 8,
         };
 
         struct bdd_node {
@@ -63,71 +72,99 @@ namespace sat {
                 m_refcount(0),
                 m_level(level),
                 m_lo(lo),
-                m_hi(hi)
+                m_hi(hi),
+                m_index(0)
             {}
+            bdd_node(): m_level(0), m_lo(0), m_hi(0), m_index(0) {}
             unsigned m_refcount : 10;
             unsigned m_level : 22;
             int      m_lo;
             int      m_hi;
-            //unsigned m_hash;
+            unsigned m_index;
-            //unsigned m_next;
+            unsigned hash() const { return mk_mix(m_level, m_lo, m_hi); }
         };
 
-        struct cache_entry {
+        struct hash_node {
-            cache_entry(unsigned hash):
+            unsigned operator()(bdd_node const& n) const { return n.hash(); }
-                m_bdd1(0),
+        };
-                m_bdd2(0),
+
-                m_op(bdd_no_op),
+        struct eq_node {
-                m_result(0),
+            bool operator()(bdd_node const& a, bdd_node const& b) const {
-                m_hash(hash)
+                return a.m_lo == b.m_lo && a.m_hi == b.m_hi && a.m_level == b.m_level;
+            }
+        };
+        
+        typedef hashtable<bdd_node, hash_node, eq_node> node_table;
+
+        struct op_entry {
+            op_entry(BDD l, BDD r, BDD op):
+                m_bdd1(l),
+                m_bdd2(r),
+                m_op(op),
+                m_result(0)
             {}
 
             BDD      m_bdd1;
             BDD      m_bdd2;
-            bdd_op   m_op;
+            BDD      m_op;
             BDD      m_result;
-            unsigned m_hash;
+            unsigned hash() const { return mk_mix(m_bdd1, m_bdd2, m_op); }
         };
 
         struct hash_entry {
-            unsigned operator()(cache_entry* e) const { return e->m_hash; }
+            unsigned operator()(op_entry* e) const { return e->hash(); }
         };
 
         struct eq_entry {
-            bool operator()(cache_entry * a, cache_entry * b) const { 
+            bool operator()(op_entry * a, op_entry * b) const { 
-                return a->m_hash == b->m_hash; 
+                return a->hash() == b->hash(); 
             }
         };
 
-        svector<bdd_node> m_nodes;
+        typedef ptr_hashtable<op_entry, hash_entry, eq_entry> op_table;
-        ptr_hashtable<cache_entry, hash_entry, eq_entry> m_cache;
+
+        svector<bdd_node>  m_nodes;
+        op_table           m_op_cache;
+        node_table         m_node_table;
         unsigned_vector    m_apply_const;
         svector<BDD>       m_bdd_stack;
-        cache_entry*       m_spare_entry;
+        op_entry*          m_spare_entry;
         svector<BDD>       m_var2bdd;
         unsigned_vector    m_var2level, m_level2var;
+        unsigned_vector    m_free_nodes;
         small_object_allocator m_alloc;
+        mutable svector<unsigned>  m_mark;
+        mutable unsigned           m_mark_level;
+        mutable svector<double>    m_path_count;
+        mutable svector<BDD>       m_todo;
+
+        unsigned           m_max_num_bdd_nodes;
 
         BDD make_node(unsigned level, BDD l, BDD r);
 
         BDD apply_const(BDD a, BDD b, bdd_op op);
         BDD apply(BDD arg1, BDD arg2, bdd_op op);
+        BDD mk_quant(unsigned n, unsigned const* vars, BDD b, bdd_op op);
+
         BDD apply_rec(BDD arg1, BDD arg2, bdd_op op);
+        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);
 
         void push(BDD b);
         void pop(unsigned num_scopes);
         BDD read(unsigned index);
 
-        cache_entry* pop_entry(unsigned hash);
+        op_entry* pop_entry(BDD l, BDD r, BDD op);
-        void push_entry(cache_entry* e);
+        void push_entry(op_entry* e);
         
-        // void bdd_reorder(int);
+        void gc();
+        void alloc_free_nodes(unsigned n);
+        void init_mark();
+        void set_mark(unsigned i) { m_mark[i] = m_mark_level; }
+        bool is_marked(unsigned i) { return m_mark[i] == m_mark_level; }
 
-        BDD mk_not_rec(BDD b);
+        void try_reorder();
-
-        unsigned hash1(BDD b, bdd_op op) const { return hash2(b, b, op); }
-        unsigned hash2(BDD a, BDD b, bdd_op op) const;
-        unsigned hash3(BDD a, BDD b, BDD c, bdd_op op) const;
 
         static const BDD false_bdd = 0;
         static const BDD true_bdd = 1;
@@ -136,33 +173,33 @@ namespace sat {
         inline bool is_true(BDD b) const { return b == true_bdd; }
         inline bool is_false(BDD b) const { return b == false_bdd; }
         inline bool is_const(BDD b) const { return 0 <= b && b <= 1; }
+        inline unsigned level(BDD b) const { return m_nodes[b].m_level; }
+        inline unsigned var(BDD b) const { return m_level2var[level(b)]; }
+        inline BDD lo(BDD b) const { return m_nodes[b].m_lo; }
+        inline BDD hi(BDD b) const { return m_nodes[b].m_hi; }
+        inline void inc_ref(BDD b) { if (m_nodes[b].m_refcount != max_rc) m_nodes[b].m_refcount++; }
+        inline void dec_ref(BDD b) { if (m_nodes[b].m_refcount != max_rc) m_nodes[b].m_refcount--; }
+        inline BDD level2bdd(unsigned l) const { return m_var2bdd[m_level2var[l]]; }
 
-        unsigned level(BDD b) const { return m_nodes[b].m_level; }
+        struct bdd_exception {};
-        BDD lo(BDD b) const { return m_nodes[b].m_lo; }
-        BDD hi(BDD b) const { return m_nodes[b].m_hi; }
-        void inc_ref(BDD b) { if (m_nodes[b].m_refcount != max_rc) m_nodes[b].m_refcount++; }
-        void dec_ref(BDD b) { if (m_nodes[b].m_refcount != max_rc && m_nodes[b].m_refcount > 0) m_nodes[b].m_refcount--; }
-
-        BDD mk_true() { return 1; }
-        BDD mk_false() { return 0; }
-
     public:
         bdd_manager(unsigned nodes, unsigned cache_size);
+        ~bdd_manager();
         
         bdd mk_var(unsigned i);
         bdd mk_nvar(unsigned i);
 
         bdd mk_not(bdd b);
-        bdd mk_exist(bdd vars, bdd b);
+        bdd mk_exists(unsigned n, unsigned const* vars, bdd const & b);
-        bdd mk_forall(bdd vars, bdd b);
+        bdd mk_forall(unsigned n, unsigned const* vars, bdd const & b);
-        bdd mk_and(bdd a, bdd b) { return bdd(apply(a.root, b.root, bdd_and_op), this); }
+        bdd mk_and(bdd const& a, bdd const& b) { return bdd(apply(a.root, b.root, bdd_and_op), this); }
-        bdd mk_or(bdd a, bdd b) { return bdd(apply(a.root, b.root, bdd_or_op), this); }
+        bdd mk_or(bdd const& a, bdd const& b) { return bdd(apply(a.root, b.root, bdd_or_op), this); }
-        bdd mk_iff(bdd a, bdd b) { return bdd(apply(a.root, b.root, bdd_iff_op), this); }
+        bdd mk_iff(bdd const& a, bdd const& b) { return bdd(apply(a.root, b.root, bdd_iff_op), this); }
-        bdd mk_ite(bdd c, bdd t, bdd e);
+        bdd mk_ite(bdd const& c, bdd const& t, bdd const& e);
 
-        double path_count(bdd b);
+        double path_count(bdd const& b);
 
-        std::ostream& display(std::ostream& out, bdd b);
+        std::ostream& display(std::ostream& out, bdd const& b);
         std::ostream& display(std::ostream& out);
     };
 }

src/test/CMakeLists.txt

@@ -16,6 +16,7 @@ add_executable(test-z3
   arith_rewriter.cpp
   arith_simplifier_plugin.cpp
   ast.cpp
+  bdd.cpp
   bit_blaster.cpp
   bits.cpp
   bit_vector.cpp

src/test/bdd.cpp

@@ -0,0 +1,40 @@
+#include "sat/sat_bdd.h"
+
+namespace sat {
+    static void test1() {
+        bdd_manager m(20, 1000);
+        bdd v0 = m.mk_var(0);
+        bdd v1 = m.mk_var(1);
+        bdd v2 = m.mk_var(2);
+        bdd c1 = v0 && v1 && v2;
+        bdd c2 = v2 && v0 && v1;
+        std::cout << c1 << "\n";
+        SASSERT(c1 == c2);
+
+        c1 = v0 || v1 || v2;
+        c2 = v2 || v1 || v0;
+        std::cout << c1 << "\n";
+        std::cout << c2 << "\n";
+        SASSERT(c1 == c2);
+    }
+
+    static void test2() {
+        bdd_manager m(20, 1000);
+        bdd v0 = m.mk_var(0);
+        bdd v1 = m.mk_var(1);
+        bdd v2 = m.mk_var(2);
+        SASSERT(m.mk_ite(v0,v0,v1) == (v0 || v1));
+        SASSERT(m.mk_ite(v0,v1,v1) == v1);
+        SASSERT(m.mk_ite(v1,v0,v1) == (v0 && v1));
+        SASSERT(m.mk_ite(v1,v0,v0) == v0);
+        SASSERT(m.mk_ite(v0,!v0,v1) == (!v0 && v1));
+        SASSERT(m.mk_ite(v0,v1,!v0) == (!v0 || v1));
+        SASSERT(!(v0 && v1) == (!v0 || !v1));
+        SASSERT(!(v0 || v1) == (!v0 && !v1));
+    }
+}
+
+void tst_bdd() {
+    sat::test1();
+    sat::test2();
+}

src/test/main.cpp

@@ -245,6 +245,7 @@ int main(int argc, char ** argv) {
     TST_ARGV(sat_lookahead);
     TST_ARGV(sat_local_search);
     TST_ARGV(cnf_backbones);
+    TST(bdd);
     //TST_ARGV(hs);
 }