From 8811d784154b0eaf64aa72137d097d66123df4ff Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 17 Oct 2017 21:28:48 -0700 Subject: [PATCH 1/2] compress elimination stack representation Signed-off-by: Nikolaj Bjorner --- src/sat/sat_model_converter.cpp | 22 +++--- src/sat/sat_model_converter.h | 12 +-- src/sat/sat_simplifier.cpp | 128 ++++++++++++++++++++++---------- 3 files changed, 108 insertions(+), 54 deletions(-) diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp index c79cd2944..14443a2f7 100644 --- a/src/sat/sat_model_converter.cpp +++ b/src/sat/sat_model_converter.cpp @@ -38,16 +38,15 @@ namespace sat { return *this; } - void model_converter::process_stack(model & m, literal_vector const& stack) const { + void model_converter::process_stack(model & m, literal_vector const& c, elim_stackv const& stack) const { SASSERT(!stack.empty()); unsigned sz = stack.size(); - SASSERT(stack[sz - 1] == null_literal); - for (unsigned i = sz - 1; i-- > 0; ) { - literal lit = stack[i]; // this is the literal that is pivoted on. It is repeated + for (unsigned i = sz; i-- > 0; ) { + unsigned csz = stack[i].first; + literal lit = stack[i].second; bool sat = false; - for (; i > 0 && stack[--i] != null_literal;) { - if (sat) continue; - sat = value_at(stack[i], m) == l_true; + for (unsigned j = 0; !sat && j < csz; ++j) { + sat = value_at(c[j], m) == l_true; } if (!sat) { m[lit.var()] = lit.sign() ? l_false : l_true; @@ -66,6 +65,7 @@ namespace sat { bool sat = false; bool var_sign = false; unsigned index = 0; + literal_vector clause; for (literal l : it->m_clauses) { if (l == null_literal) { // end of clause @@ -74,13 +74,15 @@ namespace sat { } elim_stack* s = it->m_elim_stack[index]; if (s) { - process_stack(m, s->stack()); + process_stack(m, clause, s->stack()); } sat = false; ++index; + clause.reset(); continue; } + clause.push_back(l); if (sat) continue; bool sign = l.sign(); @@ -190,13 +192,13 @@ namespace sat { // TRACE("sat_mc_bug", tout << "adding (wrapper): "; for (literal l : c) tout << l << " "; tout << "\n";); } - void model_converter::insert(entry & e, literal_vector const& c, literal_vector const& elims) { + void model_converter::insert(entry & e, literal_vector const& c, elim_stackv const& elims) { SASSERT(c.contains(literal(e.var(), false)) || c.contains(literal(e.var(), true))); SASSERT(m_entries.begin() <= &e); SASSERT(&e < m_entries.end()); for (literal l : c) e.m_clauses.push_back(l); e.m_clauses.push_back(null_literal); - e.m_elim_stack.push_back(alloc(elim_stack, elims)); + e.m_elim_stack.push_back(elims.empty() ? nullptr : alloc(elim_stack, elims)); TRACE("sat_mc_bug", tout << "adding: " << c << "\n";); } diff --git a/src/sat/sat_model_converter.h b/src/sat/sat_model_converter.h index 00fd637b7..dcbe450a8 100644 --- a/src/sat/sat_model_converter.h +++ b/src/sat/sat_model_converter.h @@ -39,18 +39,20 @@ namespace sat { class model_converter { public: + typedef svector> elim_stackv; + class elim_stack { unsigned m_refcount; - literal_vector m_stack; + elim_stackv m_stack; public: - elim_stack(literal_vector const& stack): + elim_stack(elim_stackv const& stack): m_refcount(0), m_stack(stack) { } ~elim_stack() { } void inc_ref() { ++m_refcount; } void dec_ref() { if (0 == --m_refcount) dealloc(this); } - literal_vector const& stack() const { return m_stack; } + elim_stackv const& stack() const { return m_stack; } }; enum kind { ELIM_VAR = 0, BLOCK_LIT }; @@ -74,7 +76,7 @@ namespace sat { private: vector m_entries; - void process_stack(model & m, literal_vector const& stack) const; + void process_stack(model & m, literal_vector const& clause, elim_stackv const& stack) const; public: model_converter(); @@ -86,7 +88,7 @@ namespace sat { void insert(entry & e, clause const & c); void insert(entry & e, literal l1, literal l2); void insert(entry & e, clause_wrapper const & c); - void insert(entry & c, literal_vector const& covered_clause, literal_vector const& elim_stack); + void insert(entry & c, literal_vector const& covered_clause, elim_stackv const& elim_stack); bool empty() const { return m_entries.empty(); } diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index b09d180c0..b967ade06 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -965,6 +965,7 @@ namespace sat { literal l = m_queue.next(); process(l); } + cce(); } // @@ -1027,55 +1028,106 @@ namespace sat { literal_vector m_covered_clause; literal_vector m_intersection; - literal_vector m_elim_stack; + sat::model_converter::elim_stackv m_elim_stack; + unsigned m_ala_qhead; - bool cla(literal lit) { + /* + * C \/ l l \/ lit + * ------------------- + * C \/ l \/ ~lit + */ + void add_ala() { + for (; m_ala_qhead < m_covered_clause.size(); ++m_ala_qhead) { + literal l = m_covered_clause[m_ala_qhead]; + for (watched & w : s.get_wlist(~l)) { + if (w.is_binary_clause()) { + literal lit = w.get_literal(); + if (!s.is_marked(lit) && !s.is_marked(~lit)) { + //std::cout << "ALA " << ~lit << "\n"; + m_covered_clause.push_back(~lit); + s.mark_visited(~lit); + } + } + } + } + } + + bool add_cla(literal& blocked) { + for (unsigned i = 0; i < m_covered_clause.size(); ++i) { + m_intersection.reset(); + if (ri(m_covered_clause[i], m_intersection)) { + blocked = m_covered_clause[i]; + return true; + } + for (literal l : m_intersection) { + if (!s.is_marked(l)) { + s.mark_visited(l); + m_covered_clause.push_back(l); + } + } + if (!m_intersection.empty()) { + m_elim_stack.push_back(std::make_pair(m_covered_clause.size(), m_covered_clause[i])); + } + } + return false; + } + + bool cla(literal& blocked) { bool is_tautology = false; for (literal l : m_covered_clause) s.mark_visited(l); unsigned num_iterations = 0, sz; m_elim_stack.reset(); + m_ala_qhead = 0; do { - ++num_iterations; - sz = m_covered_clause.size(); - for (unsigned i = 0; i < m_covered_clause.size(); ++i) { - m_intersection.reset(); - if (ri(m_covered_clause[i], m_intersection) && m_covered_clause[i] == lit) { - is_tautology = true; - break; - } - for (literal l : m_intersection) { - if (!s.is_marked(l)) { - s.mark_visited(l); - m_covered_clause.push_back(l); - } - } - if (!m_intersection.empty()) { - m_elim_stack.append(m_covered_clause); // the current clause - m_elim_stack.push_back(m_covered_clause[i]); // the pivot literal - m_elim_stack.push_back(null_literal); // null demarcation - } + do { + ++num_iterations; + sz = m_covered_clause.size(); + is_tautology = add_cla(blocked); } + while (m_covered_clause.size() > sz && !is_tautology); + break; + //if (is_tautology) break; + //sz = m_covered_clause.size(); + // unsound? add_ala(); } - while (m_covered_clause.size() > sz && !is_tautology); + while (m_covered_clause.size() > sz); for (literal l : m_covered_clause) s.unmark_visited(l); - if (is_tautology) std::cout << "taut: " << num_iterations << "\n"; + // if (is_tautology) std::cout << "taut: " << num_iterations << " " << m_covered_clause.size() << " " << m_elim_stack.size() << "\n"; return is_tautology; } // perform covered clause elimination. // first extract the covered literal addition (CLA). // then check whether the CLA is blocked. - bool cce(clause& c, literal lit) { + bool cce(clause& c, literal& blocked) { m_covered_clause.reset(); for (literal l : c) m_covered_clause.push_back(l); - return cla(lit); + return cla(blocked); } - bool cce(literal lit, literal l2) { + bool cce(literal lit, literal l2, literal& blocked) { m_covered_clause.reset(); m_covered_clause.push_back(lit); m_covered_clause.push_back(l2); - return cla(lit); + return cla(blocked); + } + + void cce() { + m_to_remove.reset(); + literal blocked; + for (clause* cp : s.s.m_clauses) { + clause& c = *cp; + if (c.was_removed()) continue; + if (cce(c, blocked)) { + model_converter::entry * new_entry = 0; + block_covered_clause(c, blocked, new_entry); + s.m_num_covered_clauses++; + } + } + for (clause* c : m_to_remove) { + s.remove_clause(*c); + } + m_to_remove.reset(); } void process(literal l) { @@ -1085,6 +1137,7 @@ namespace sat { return; } + literal blocked = null_literal; m_to_remove.reset(); { clause_use_list & occs = s.m_use_list.get(l); @@ -1095,14 +1148,10 @@ namespace sat { SASSERT(c.contains(l)); s.mark_all_but(c, l); if (all_tautology(l)) { - s.unmark_all(c); block_clause(c, l, new_entry); s.m_num_blocked_clauses++; } - else if (cce(c, l)) { - block_covered_clause(c, l, new_entry); - s.m_num_covered_clauses++; - } + s.unmark_all(c); it.next(); } } @@ -1127,8 +1176,9 @@ namespace sat { block_binary(it, l, new_entry); s.m_num_blocked_clauses++; } - else if (cce(l, l2)) { - block_covered_binary(it, l, new_entry); + else if (cce(l, l2, blocked)) { + model_converter::entry * blocked_entry = 0; + block_covered_binary(it, l, blocked, blocked_entry); s.m_num_covered_clauses++; } else { @@ -1163,9 +1213,9 @@ namespace sat { mc.insert(*new_entry, m_covered_clause, m_elim_stack); } - void prepare_block_binary(watch_list::iterator it, literal l, model_converter::entry *& new_entry) { + void prepare_block_binary(watch_list::iterator it, literal l, literal blocked, model_converter::entry *& new_entry) { if (new_entry == 0) - new_entry = &(mc.mk(model_converter::BLOCK_LIT, l.var())); + new_entry = &(mc.mk(model_converter::BLOCK_LIT, blocked.var())); literal l2 = it->get_literal(); TRACE("blocked_clause", tout << "new blocked clause: " << l2 << " " << l << "\n";); s.remove_bin_clause_half(l2, l, it->is_learned()); @@ -1173,12 +1223,12 @@ namespace sat { } void block_binary(watch_list::iterator it, literal l, model_converter::entry *& new_entry) { - prepare_block_binary(it, l, new_entry); + prepare_block_binary(it, l, l, new_entry); mc.insert(*new_entry, l, it->get_literal()); } - void block_covered_binary(watch_list::iterator it, literal l, model_converter::entry *& new_entry) { - prepare_block_binary(it, l, new_entry); + void block_covered_binary(watch_list::iterator it, literal l, literal blocked, model_converter::entry *& new_entry) { + prepare_block_binary(it, l, blocked, new_entry); mc.insert(*new_entry, m_covered_clause, m_elim_stack); } From 80f24c29ab2831576b18d8bea4ac75f03b808ad9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 18 Oct 2017 08:52:03 -0700 Subject: [PATCH 2/2] debugging reordering Signed-off-by: Nikolaj Bjorner --- src/sat/sat_bdd.cpp | 145 ++++++++++++++++++++++++++++++-------------- src/sat/sat_bdd.h | 46 ++++++++------ src/test/bdd.cpp | 16 +++++ 3 files changed, 144 insertions(+), 63 deletions(-) diff --git a/src/sat/sat_bdd.cpp b/src/sat/sat_bdd.cpp index 1073f482e..3125b2a3a 100644 --- a/src/sat/sat_bdd.cpp +++ b/src/sat/sat_bdd.cpp @@ -18,6 +18,7 @@ Revision History: --*/ #include "sat/sat_bdd.h" +#include "util/trace.h" namespace sat { @@ -48,12 +49,7 @@ namespace sat { // add variables for (unsigned i = 0; i < num_vars; ++i) { - m_var2bdd.push_back(make_node(i, false_bdd, true_bdd)); - m_var2bdd.push_back(make_node(i, true_bdd, false_bdd)); - m_nodes[m_var2bdd[2*i]].m_refcount = max_rc; - m_nodes[m_var2bdd[2*i+1]].m_refcount = max_rc; - m_var2level.push_back(i); - m_level2var.push_back(i); + reserve_var(i); } } @@ -73,8 +69,8 @@ namespace sat { 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; + case bdd_xor_op: + return (a == b) ? false_bdd : true_bdd; default: return false_bdd; } @@ -99,7 +95,7 @@ namespace sat { bdd bdd_manager::mk_false() { return bdd(false_bdd, this); } bdd bdd_manager::mk_and(bdd const& a, bdd const& b) { return bdd(apply(a.root, b.root, bdd_and_op), this); } bdd bdd_manager::mk_or(bdd const& a, bdd const& b) { return bdd(apply(a.root, b.root, bdd_or_op), this); } - bdd bdd_manager::mk_iff(bdd const& a, bdd const& b) { return bdd(apply(a.root, b.root, bdd_iff_op), this); } + bdd bdd_manager::mk_xor(bdd const& a, bdd const& b) { return bdd(apply(a.root, b.root, bdd_xor_op), this); } bdd bdd_manager::mk_exists(unsigned v, bdd const& b) { return mk_exists(1, &v, b); } bdd bdd_manager::mk_forall(unsigned v, bdd const& b) { return mk_forall(1, &v, b); } @@ -132,10 +128,10 @@ namespace sat { if (is_false(b)) return a; if (is_true(a) || is_true(b)) return true_bdd; break; - case bdd_iff_op: - if (a == b) return true_bdd; - if (is_true(a)) return b; - if (is_true(b)) return a; + case bdd_xor_op: + if (a == b) return false_bdd; + if (is_false(a)) return b; + if (is_false(b)) return a; break; default: UNREACHABLE(); @@ -265,9 +261,9 @@ namespace sat { goto go_down; } go_up: + TRACE("bdd", tout << "sift up " << lvl << "\n";); while (lvl < max_lvl) { - sift_up(lvl); - ++lvl; + sift_up(lvl++); double cost = current_cost(); if (is_bad_cost(cost, best_cost)) break; best_cost = std::min(cost, best_cost); @@ -275,22 +271,20 @@ namespace sat { if (first) { first = false; while (lvl != start) { - sift_up(lvl-1); - --lvl; + sift_up(--lvl); } goto go_down; } else { while (current_cost() != best_cost) { - sift_up(lvl-1); - --lvl; + sift_up(--lvl); } return; } go_down: + TRACE("bdd", tout << "sift down " << lvl << "\n";); while (lvl > 0) { - sift_up(lvl-1); - --lvl; + sift_up(--lvl); double cost = current_cost(); if (is_bad_cost(cost, best_cost)) break; best_cost = std::min(cost, best_cost); @@ -298,15 +292,13 @@ namespace sat { if (first) { first = false; while (lvl != start) { - sift_up(lvl); - ++lvl; + sift_up(lvl++); } goto go_up; } else { while (current_cost() != best_cost) { - sift_up(lvl); - ++lvl; + sift_up(lvl++); } return; } @@ -330,30 +322,37 @@ namespace sat { else { m_T.push_back(n); } + TRACE("bdd", tout << "remove " << n << "\n";); m_node_table.remove(m_nodes[n]); } + m_level2nodes[lvl + 1].reset(); + m_level2nodes[lvl + 1].append(m_T); for (unsigned n : m_level2nodes[lvl]) { bdd_node& node = m_nodes[n]; m_node_table.remove(node); if (m_max_parent[n] == lvl + 1 && node.m_refcount == 0) { + TRACE("bdd", tout << "free " << n << "\n";); node.set_internal(); m_free_nodes.push_back(n); } else { + TRACE("bdd", tout << "set level " << n << " to " << lvl + 1 << "\n";); node.m_level = lvl + 1; m_node_table.insert(node); + m_level2nodes[lvl + 1].push_back(n); } } - + m_level2nodes[lvl].reset(); + m_level2nodes[lvl].append(m_S); + for (unsigned n : m_S) { m_nodes[n].m_level = lvl; m_node_table.insert(m_nodes[n]); } - std::swap(m_level2nodes[lvl], m_level2nodes[lvl + 1]); - for (unsigned n : m_T) { + TRACE("bdd", tout << "transform " << n << "\n";); BDD l = lo(n); BDD h = hi(n); if (l == 0 && h == 0) continue; @@ -392,6 +391,14 @@ namespace sat { std::swap(m_level2var[lvl], m_level2var[lvl+1]); std::swap(m_var2level[v], m_var2level[w]); m_disable_gc = false; + TRACE("bdd", tout << "sift " << lvl << "\n"; display(tout); ); + DEBUG_CODE( + for (unsigned i = 0; i < m_level2nodes.size(); ++i) { + for (unsigned n : m_level2nodes[i]) { + bdd_node const& node = m_nodes[n]; + SASSERT(node.m_level == i); + } + }); } void bdd_manager::init_reorder() { @@ -403,18 +410,41 @@ namespace sat { if (n.is_internal()) continue; unsigned lvl = n.m_level; SASSERT(i == m_nodes[i].m_index); - while (m_level2nodes.size() <= lvl) m_level2nodes.push_back(unsigned_vector()); + m_level2nodes.reserve(lvl + 1); m_level2nodes[lvl].push_back(i); m_max_parent[n.m_lo] = std::max(m_max_parent[n.m_lo], lvl); m_max_parent[n.m_hi] = std::max(m_max_parent[n.m_hi], lvl); } + TRACE("bdd", + display(tout); + for (unsigned i = 0; i < sz; ++i) { + bdd_node const& n = m_nodes[i]; + if (n.is_internal()) continue; + unsigned lvl = n.m_level; + tout << "lvl: " << lvl << " parent: " << m_max_parent[i] << " lo " << n.m_lo << " hi " << n.m_hi << "\n"; + } + ); + } + + void bdd_manager::reserve_var(unsigned i) { + while (m_var2level.size() <= i) { + unsigned v = m_var2level.size(); + m_var2bdd.push_back(make_node(v, false_bdd, true_bdd)); + m_var2bdd.push_back(make_node(v, true_bdd, false_bdd)); + m_nodes[m_var2bdd[2*v]].m_refcount = max_rc; + m_nodes[m_var2bdd[2*v+1]].m_refcount = max_rc; + m_var2level.push_back(v); + m_level2var.push_back(v); + } } bdd bdd_manager::mk_var(unsigned i) { + reserve_var(i); return bdd(m_var2bdd[2*i], this); } bdd bdd_manager::mk_nvar(unsigned i) { + reserve_var(i); return bdd(m_var2bdd[2*i+1], this); } @@ -581,6 +611,29 @@ namespace sat { return m_count[b.root]; } + unsigned bdd_manager::bdd_size(bdd const& b) { + init_mark(); + set_mark(0); + set_mark(1); + unsigned sz = 0; + m_todo.push_back(b.root); + while (!m_todo.empty()) { + BDD r = m_todo.back(); + m_todo.pop_back(); + if (!is_marked(r)) { + ++sz; + set_mark(r); + if (!is_marked(lo(r))) { + m_todo.push_back(lo(r)); + } + if (!is_marked(hi(r))) { + m_todo.push_back(hi(r)); + } + } + } + return sz; + } + void bdd_manager::alloc_free_nodes(unsigned n) { for (unsigned i = 0; i < n; ++i) { m_free_nodes.push_back(m_nodes.size()); @@ -678,31 +731,35 @@ namespace sat { return out; } + void bdd_manager::well_formed() { + for (unsigned n : m_free_nodes) { + VERIFY(lo(n) == 0 && hi(n) == 0 && m_nodes[n].m_refcount == 0); + } + for (bdd_node const& n : m_nodes) { + if (n.is_internal()) continue; + unsigned lvl = n.m_level; + BDD lo = n.m_lo; + BDD hi = n.m_hi; + VERIFY(is_const(lo) || level(lo) < lvl); + VERIFY(is_const(hi) || level(hi) < lvl); + } + } + 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.is_internal()) continue; out << i << " : " << m_level2var[n.m_level] << " " << n.m_lo << " " << n.m_hi << "\n"; } + for (unsigned i = 0; i < m_level2nodes.size(); ++i) { + out << i << " : "; + for (unsigned l : m_level2nodes[i]) out << l << " "; + out << "\n"; + } return out; } - bdd::bdd(unsigned 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(bdd && other): root(0), m(other.m) { std::swap(root, other.root); } - bdd::~bdd() { m->dec_ref(root); } - bdd bdd::lo() const { return bdd(m->lo(root), m); } - bdd bdd::hi() const { return bdd(m->hi(root), m); } - unsigned bdd::var() const { return m->var(root); } - bool bdd::is_true() const { return root == bdd_manager::true_bdd; } - bool bdd::is_false() const { return root == bdd_manager::false_bdd; } - 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); } bdd& bdd::operator=(bdd const& other) { unsigned r1 = root; root = other.root; m->inc_ref(root); m->dec_ref(r1); return *this; } - std::ostream& bdd::display(std::ostream& out) const { return m->display(out, *this); } std::ostream& operator<<(std::ostream& out, bdd const& b) { return b.display(out); } - double bdd::cnf_size() const { return m->cnf_size(*this); } - double bdd::dnf_size() const { return m->dnf_size(*this); } } diff --git a/src/sat/sat_bdd.h b/src/sat/sat_bdd.h index dbd19ec61..41e45c822 100644 --- a/src/sat/sat_bdd.h +++ b/src/sat/sat_bdd.h @@ -35,7 +35,7 @@ namespace sat { enum bdd_op { bdd_and_op = 2, bdd_or_op = 3, - bdd_iff_op = 4, + bdd_xor_op = 4, bdd_not_op = 5, bdd_and_proj_op = 6, bdd_or_proj_op = 7, @@ -149,7 +149,6 @@ namespace sat { void set_mark(unsigned i) { m_mark[i] = m_mark_level; } bool is_marked(unsigned i) { return m_mark[i] == m_mark_level; } - void try_reorder(); void init_reorder(); void sift_up(unsigned level); void sift_var(unsigned v); @@ -173,10 +172,15 @@ namespace sat { double dnf_size(bdd const& b) { return count(b, 0); } double cnf_size(bdd const& b) { return count(b, 1); } + unsigned bdd_size(bdd const& b); bdd mk_not(bdd b); 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); + + void reserve_var(unsigned v); + void well_formed(); public: struct mem_out {}; @@ -196,39 +200,43 @@ namespace sat { bdd mk_forall(unsigned n, unsigned const* vars, bdd const & b); bdd mk_exists(unsigned v, bdd const& b); bdd mk_forall(unsigned v, bdd const& b); - bdd mk_iff(bdd const& a, bdd const& b); bdd mk_ite(bdd const& c, bdd const& t, bdd const& e); std::ostream& display(std::ostream& out); std::ostream& display(std::ostream& out, bdd const& b); + + void try_reorder(); }; class bdd { friend class bdd_manager; unsigned root; bdd_manager* m; - bdd(unsigned root, bdd_manager* m); + bdd(unsigned root, bdd_manager* m): root(root), m(m) { m->inc_ref(root); } public: - bdd(bdd & other); - bdd(bdd && other); + bdd(bdd & other): root(other.root), m(other.m) { m->inc_ref(root); } + bdd(bdd && other): root(0), m(other.m) { std::swap(root, other.root); } bdd& operator=(bdd const& other); - ~bdd(); - bdd lo() const; - bdd hi() const; - unsigned var() const; - bool is_true() const; - bool is_false() const; - - bdd operator!(); - bdd operator&&(bdd const& other); - bdd operator||(bdd const& other); + ~bdd() { m->dec_ref(root); } + bdd lo() const { return bdd(m->lo(root), m); } + bdd hi() const { return bdd(m->hi(root), m); } + 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; } + + 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|=(bdd const& other) { return *this = *this || other; } bdd operator&=(bdd const& other) { return *this = *this && other; } - std::ostream& display(std::ostream& out) const; + 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; } - double cnf_size() const; - double dnf_size() const; + double cnf_size() const { return m->cnf_size(*this); } + double dnf_size() const { return m->dnf_size(*this); } + unsigned bdd_size() const { return m->bdd_size(*this); } }; std::ostream& operator<<(std::ostream& out, bdd const& b); diff --git a/src/test/bdd.cpp b/src/test/bdd.cpp index 6826df35e..b60522740 100644 --- a/src/test/bdd.cpp +++ b/src/test/bdd.cpp @@ -57,10 +57,26 @@ namespace sat { c2 = m.mk_exists(2, c1); SASSERT(c2 == ((v0 && v1) || v1 || !v0)); } + + void test4() { + bdd_manager m(3); + bdd v0 = m.mk_var(0); + bdd v1 = m.mk_var(1); + bdd v2 = m.mk_var(2); + bdd c1 = (v0 && v2) || v1; + std::cout << "before reorder:\n"; + std::cout << c1 << "\n"; + std::cout << c1.bdd_size() << "\n"; + m.try_reorder(); + std::cout << "after reorder:\n"; + std::cout << c1 << "\n"; + std::cout << c1.bdd_size() << "\n"; + } } void tst_bdd() { sat::test1(); sat::test2(); sat::test3(); + sat::test4(); }