From d7b6373601c46ba3dc928c59280298b6e18be2e9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 14 Oct 2017 10:41:17 -0700 Subject: [PATCH] adding bdd package Signed-off-by: Nikolaj Bjorner --- src/sat/sat_bdd.cpp | 428 ++++++++++++++++++++++++++++++++-------- src/sat/sat_bdd.h | 135 ++++++++----- src/test/CMakeLists.txt | 1 + src/test/bdd.cpp | 40 ++++ src/test/main.cpp | 1 + 5 files changed, 476 insertions(+), 129 deletions(-) create mode 100644 src/test/bdd.cpp diff --git a/src/sat/sat_bdd.cpp b/src/sat/sat_bdd.cpp index fc3f94a25..50fc3f1d9 100644 --- a/src/sat/sat_bdd.cpp +++ b/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)); - m_nodes.push_back(bdd_node(0,0,0)); - m_nodes[0].m_refcount = max_rc; - m_nodes[1].m_refcount = max_rc; + for (unsigned i = 0; i <= bdd_no_op; ++i) { + m_nodes.push_back(bdd_node(0,0,0)); + m_nodes.back().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) { @@ -45,28 +51,44 @@ namespace sat { m_nodes[m_var2bdd[2*i+1]].m_refcount = max_rc; m_var2level.push_back(i); m_level2var.push_back(i); - } - - m_spare_entry = nullptr; + } + } + + bdd_manager::~bdd_manager() { + if (m_spare_entry) { + m_alloc.deallocate(sizeof(*m_spare_entry), m_spare_entry); + } + for (auto* e : m_op_cache) { + m_alloc.deallocate(sizeof(*e), e); + } } 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 == 1 && b == 1) ? 1 : 0; + return (a == true_bdd && b == true_bdd) ? true_bdd : false_bdd; case bdd_or_op: - return (a == 1 || b == 1) ? 1 : 0; + return (a == true_bdd || b == true_bdd) ? true_bdd : false_bdd; case bdd_iff_op: - return (a == b) ? 1 : 0; + return (a == b) ? true_bdd : false_bdd; default: - UNREACHABLE(); - return 0; + 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)); - cache_entry const* e2 = m_cache.insert_if_not_there(e1); - if (e2->m_op == op && e2->m_bdd1 == a && e2->m_bdd2 == b) { - push_entry(e1); - return e2->m_result; + op_entry * e1 = pop_entry(a, b, op); + 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 == op) { + push_entry(e1); + return e2->m_result; + } + e1 = const_cast(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,46 +162,63 @@ namespace sat { return m_bdd_stack[m_bdd_stack.size() - index]; } - - bdd_manager::cache_entry* bdd_manager::pop_entry(unsigned hash) { - cache_entry* result = 0; + bdd_manager::op_entry* bdd_manager::pop_entry(BDD l, BDD r, BDD op) { + op_entry* result = nullptr; if (m_spare_entry) { result = m_spare_entry; - m_spare_entry = 0; - result->m_hash = hash; + m_spare_entry = nullptr; + result->m_bdd1 = l; + result->m_bdd2 = r; + result->m_op = op; } else { - void * mem = m_alloc.allocate(sizeof(cache_entry)); - result = new (mem) cache_entry(hash); + void * mem = m_alloc.allocate(sizeof(op_entry)); + 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 - // 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; + + 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; } -#if 0 - void bdd_manager::bdd_reorder(int) { - + void bdd_manager::try_reorder() { + // TBD } -#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)); - cache_entry const* e2 = m_cache.insert_if_not_there(e1); - if (e2->m_bdd1 == b && e2->m_op == bdd_not_op) { - push_entry(e1); - return e2->m_result; + op_entry* e1 = pop_entry(b, b, bdd_not_op); + op_entry const* e2 = m_op_cache.insert_if_not_there(e1); + if (e2 != e1) { + if (e2->m_bdd1 == b && e2->m_bdd2 == b && e2->m_op == bdd_not_op) { + push_entry(e1); + return e2->m_result; + } + e1 = const_cast(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_exists(bdd vars, bdd b) { + bdd bdd_manager::mk_ite(bdd const& c, bdd const& t, bdd const& e) { + 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(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(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 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 b) { - + std::ostream& bdd_manager::display(std::ostream& out, bdd const& b) { + init_mark(); + 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): - root(root), m(m) { - m->inc_ref(root); - } - + bdd::bdd(int root, bdd_manager* m): 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); } - - bdd::~bdd() { - m->dec_ref(root); + std::ostream& operator<<(std::ostream& out, bdd const& b) { + return b.display(out); } -#if 0 -#endif + } diff --git a/src/sat/sat_bdd.h b/src/sat/sat_bdd.h index 4df0433fd..767fd5111 100644 --- a/src/sat/sat_bdd.h +++ b/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_or_op, - bdd_iff_op, - bdd_not_op, - bdd_no_op + bdd_and_op = 2, + bdd_or_op = 3, + bdd_iff_op = 4, + bdd_not_op = 5, + 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_next; + unsigned m_index; + unsigned hash() const { return mk_mix(m_level, m_lo, m_hi); } + }; + + struct hash_node { + unsigned operator()(bdd_node const& n) const { return n.hash(); } + }; + + struct eq_node { + bool operator()(bdd_node const& a, bdd_node const& b) const { + return a.m_lo == b.m_lo && a.m_hi == b.m_hi && a.m_level == b.m_level; + } }; - struct cache_entry { - cache_entry(unsigned hash): - m_bdd1(0), - m_bdd2(0), - m_op(bdd_no_op), - m_result(0), - m_hash(hash) + typedef hashtable 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 { - return a->m_hash == b->m_hash; + bool operator()(op_entry * a, op_entry * b) const { + return a->hash() == b->hash(); } }; - svector m_nodes; - ptr_hashtable m_cache; + typedef ptr_hashtable op_table; + + svector m_nodes; + op_table m_op_cache; + node_table m_node_table; unsigned_vector m_apply_const; svector m_bdd_stack; - cache_entry* m_spare_entry; + op_entry* m_spare_entry; svector m_var2bdd; unsigned_vector m_var2level, m_level2var; + unsigned_vector m_free_nodes; small_object_allocator m_alloc; + mutable svector m_mark; + mutable unsigned m_mark_level; + mutable svector m_path_count; + mutable svector 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); - void push_entry(cache_entry* e); + op_entry* pop_entry(BDD l, BDD r, BDD op); + 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); - - 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; + void try_reorder(); 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; } - 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; } - + struct bdd_exception {}; 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_forall(bdd vars, bdd b); - bdd mk_and(bdd a, bdd 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_iff(bdd a, bdd b) { return bdd(apply(a.root, b.root, bdd_iff_op), this); } - bdd mk_ite(bdd c, bdd t, bdd e); + bdd mk_exists(unsigned n, unsigned const* vars, bdd const & b); + bdd mk_forall(unsigned n, unsigned const* vars, bdd const & b); + bdd mk_and(bdd const& a, bdd const& b) { return bdd(apply(a.root, b.root, bdd_and_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 const& a, bdd const& b) { return bdd(apply(a.root, b.root, bdd_iff_op), this); } + 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); }; } diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index 1c1665363..b487fe9ba 100644 --- a/src/test/CMakeLists.txt +++ b/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 diff --git a/src/test/bdd.cpp b/src/test/bdd.cpp new file mode 100644 index 000000000..91d837f08 --- /dev/null +++ b/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(); +} diff --git a/src/test/main.cpp b/src/test/main.cpp index 4aeba26c5..33d0abae5 100644 --- a/src/test/main.cpp +++ b/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); }