From dc6ed64da1a534fae2cd83a96a63be9776a890f5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 18 Oct 2017 17:37:38 -0700 Subject: [PATCH] testing bdd for elim-vars Signed-off-by: Nikolaj Bjorner --- src/sat/sat_bdd.cpp | 248 +++++++++++++++++++++++++++++-------- src/sat/sat_bdd.h | 39 +++--- src/sat/sat_elim_vars.cpp | 9 +- src/sat/sat_elim_vars.h | 2 + src/sat/sat_lookahead.cpp | 76 ++---------- src/sat/sat_lookahead.h | 1 + src/sat/sat_simplifier.cpp | 6 +- src/test/bdd.cpp | 1 + src/util/vector.h | 5 + 9 files changed, 254 insertions(+), 133 deletions(-) diff --git a/src/sat/sat_bdd.cpp b/src/sat/sat_bdd.cpp index 3125b2a3a..e44bf7944 100644 --- a/src/sat/sat_bdd.cpp +++ b/src/sat/sat_bdd.cpp @@ -23,6 +23,8 @@ Revision History: namespace sat { bdd_manager::bdd_manager(unsigned num_vars) { + m_cost_metric = bdd_cost; + m_cost_bdd = 0; for (BDD a = 0; a < 2; ++a) { for (BDD b = 0; b < 2; ++b) { for (unsigned op = bdd_and_op; op < bdd_not_op; ++op) { @@ -58,6 +60,7 @@ namespace sat { m_alloc.deallocate(sizeof(*m_spare_entry), m_spare_entry); } for (auto* e : m_op_cache) { + VERIFY(e != m_spare_entry); m_alloc.deallocate(sizeof(*e), e); } } @@ -78,16 +81,21 @@ namespace sat { bdd_manager::BDD bdd_manager::apply(BDD arg1, BDD arg2, bdd_op op) { bool first = true; + SASSERT(well_formed()); while (true) { try { return apply_rec(arg1, arg2, op); } catch (mem_out) { + throw; +#if 0 try_reorder(); if (!first) throw; first = false; +#endif } } + SASSERT(well_formed()); } @@ -101,17 +109,20 @@ namespace sat { bool bdd_manager::check_result(op_entry*& e1, op_entry const* e2, BDD a, BDD b, BDD c) { + // std::cout << a << " " << b << " " << c << " " << e1 << " " << e2 << "\n"; if (e1 != e2) { + VERIFY(e2->m_result != -1); push_entry(e1); - if (e2->m_bdd1 == a && e2->m_bdd2 == b && e2->m_op == c) { - return true; - } - e1 = const_cast(e2); + e1 = nullptr; + return true; + } + else { + e1->m_bdd1 = a; + e1->m_bdd2 = b; + e1->m_op = c; + VERIFY(e1->m_result == -1); + return false; } - e1->m_bdd1 = a; - e1->m_bdd2 = b; - e1->m_op = c; - return false; } bdd_manager::BDD bdd_manager::apply_rec(BDD a, BDD b, bdd_op op) { @@ -143,8 +154,10 @@ namespace sat { op_entry * e1 = pop_entry(a, b, op); op_entry const* e2 = m_op_cache.insert_if_not_there(e1); if (check_result(e1, e2, a, b, op)) { + SASSERT(!m_free_nodes.contains(e2->m_result)); return e2->m_result; } + // VERIFY(well_formed()); BDD r; if (level(a) == level(b)) { push(apply_rec(lo(a), lo(b), op)); @@ -163,6 +176,8 @@ namespace sat { } pop(2); e1->m_result = r; + // VERIFY(well_formed()); + SASSERT(!m_free_nodes.contains(r)); return r; } @@ -190,6 +205,7 @@ namespace sat { else { void * mem = m_alloc.allocate(sizeof(op_entry)); result = new (mem) op_entry(l, r, op); + // std::cout << "alloc: " << result << "\n"; } result->m_result = -1; return result; @@ -200,16 +216,22 @@ namespace sat { m_spare_entry = e; } - bdd_manager::BDD bdd_manager::make_node(unsigned level, BDD l, BDD r) { + bdd_manager::BDD bdd_manager::make_node(unsigned lvl, BDD l, BDD h) { m_is_new_node = false; - if (l == r) { + if (l == h) { return l; } + if (!is_const(l) && level(l) >= lvl) { + display(std::cout << l << " level: " << level(l) << " lvl: " << lvl << "\n"); + } + VERIFY(is_const(l) || level(l) < lvl); + VERIFY(is_const(h) || level(h) < lvl); - bdd_node n(level, l, r); + bdd_node n(lvl, l, h); 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; + unsigned result = e->get_data().m_index; + return result; } e->get_data().m_refcount = 0; bool do_gc = m_free_nodes.empty(); @@ -226,25 +248,50 @@ namespace sat { } SASSERT(!m_free_nodes.empty()); - e->get_data().m_index = m_free_nodes.back(); - m_nodes[e->get_data().m_index] = e->get_data(); - m_free_nodes.pop_back(); - m_is_new_node = true; - return e->get_data().m_index; + unsigned result = m_free_nodes.back(); + m_free_nodes.pop_back(); + e->get_data().m_index = result; + m_nodes[result] = e->get_data(); + m_is_new_node = true; + SASSERT(!m_free_nodes.contains(result)); + SASSERT(m_nodes[result].m_index == result); + return result; } + void bdd_manager::try_cnf_reorder(bdd const& b) { + m_cost_bdd = b.root; + m_cost_metric = cnf_cost; + try_reorder(); + m_cost_metric = bdd_cost; + m_cost_bdd = 0; + } + void bdd_manager::try_reorder() { + gc(); + for (auto* e : m_op_cache) { + m_alloc.deallocate(sizeof(*e), e); + } + m_op_cache.reset(); init_reorder(); for (unsigned i = 0; i < m_var2level.size(); ++i) { sift_var(i); } + SASSERT(m_op_cache.empty()); + SASSERT(well_formed()); } double bdd_manager::current_cost() { -#if 0 - -#endif - return m_nodes.size() - m_free_nodes.size(); + switch (m_cost_metric) { + case bdd_cost: + return m_nodes.size() - m_free_nodes.size(); + case cnf_cost: + return cnf_size(m_cost_bdd); + case dnf_cost: + return dnf_size(m_cost_bdd); + default: + UNREACHABLE(); + return 0; + } } bool bdd_manager::is_bad_cost(double current_cost, double best_cost) const { @@ -306,9 +353,11 @@ namespace sat { void bdd_manager::sift_up(unsigned lvl) { if (m_level2nodes[lvl].empty()) return; + // VERIFY(well_formed()); // exchange level and level + 1. m_S.reset(); m_T.reset(); + m_to_free.reset(); m_disable_gc = true; for (unsigned n : m_level2nodes[lvl + 1]) { @@ -320,6 +369,8 @@ namespace sat { m_S.push_back(n); } else { + reorder_decref(l); + reorder_decref(h); m_T.push_back(n); } TRACE("bdd", tout << "remove " << n << "\n";); @@ -331,14 +382,12 @@ namespace sat { 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); + node.m_level = lvl + 1; + if (m_reorder_rc[n] == 0) { + m_to_free.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); } @@ -352,19 +401,18 @@ namespace sat { } 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; BDD a, b, c, d; - if (level(l) == lvl) { + if (level(l) == lvl + 1) { a = lo(l); b = hi(l); } else { a = b = l; } - if (level(h) == lvl) { + if (level(h) == lvl + 1) { c = lo(h); d = hi(h); } @@ -375,15 +423,22 @@ namespace sat { unsigned ac = make_node(lvl, a, c); if (is_new_node()) { m_level2nodes[lvl].push_back(ac); - m_max_parent.setx(ac, lvl + 1, 0); + m_reorder_rc.reserve(ac+1); + reorder_incref(a); + reorder_incref(c); } unsigned bd = make_node(lvl, b, d); if (is_new_node()) { m_level2nodes[lvl].push_back(bd); - m_max_parent.setx(bd, lvl + 1, 0); + m_reorder_rc.reserve(bd+1); + reorder_incref(b); + reorder_incref(d); } m_nodes[n].m_lo = ac; m_nodes[n].m_hi = bd; + reorder_incref(ac); + reorder_incref(bd); + TRACE("bdd", tout << "transform " << n << " " << " " << a << " " << b << " " << c << " " << d << " " << ac << " " << bd << "\n";); m_node_table.insert(m_nodes[n]); } unsigned v = m_level2var[lvl]; @@ -391,6 +446,30 @@ namespace sat { std::swap(m_level2var[lvl], m_level2var[lvl+1]); std::swap(m_var2level[v], m_var2level[w]); m_disable_gc = false; + + // add orphaned nodes to free-list + for (unsigned i = 0; i < m_to_free.size(); ++i) { + unsigned n = m_to_free[i]; + bdd_node& node = m_nodes[n]; + if (!node.is_internal()) { + VERIFY(!m_free_nodes.contains(n)); + VERIFY(node.m_refcount == 0); + m_free_nodes.push_back(n); + m_node_table.remove(node); + BDD l = lo(n); + BDD h = hi(n); + node.set_internal(); + + reorder_decref(l); + if (!m_nodes[l].is_internal() && m_reorder_rc[l] == 0) { + m_to_free.push_back(l); + } + reorder_decref(h); + if (!m_nodes[h].is_internal() && m_reorder_rc[h] == 0) { + m_to_free.push_back(h); + } + } + } TRACE("bdd", tout << "sift " << lvl << "\n"; display(tout); ); DEBUG_CODE( for (unsigned i = 0; i < m_level2nodes.size(); ++i) { @@ -399,12 +478,24 @@ namespace sat { SASSERT(node.m_level == i); } }); + + TRACE("bdd", + for (unsigned i = 0; i < m_nodes.size(); ++i) { + if (m_reorder_rc[i] != 0) { + tout << i << " " << m_reorder_rc[i] << "\n"; + }}); + + // VERIFY(well_formed()); } void bdd_manager::init_reorder() { m_level2nodes.reset(); unsigned sz = m_nodes.size(); - m_max_parent.fill(sz, 0); + m_reorder_rc.fill(sz, 0); + for (unsigned i = 0; i < sz; ++i) { + if (m_nodes[i].m_refcount > 0) + m_reorder_rc[i] = UINT_MAX; + } for (unsigned i = 0; i < sz; ++i) { bdd_node const& n = m_nodes[i]; if (n.is_internal()) continue; @@ -412,8 +503,8 @@ namespace sat { SASSERT(i == m_nodes[i].m_index); 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); + reorder_incref(n.m_lo); + reorder_incref(n.m_hi); } TRACE("bdd", display(tout); @@ -421,11 +512,19 @@ namespace sat { 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"; + tout << i << " lvl: " << lvl << " rc: " << m_reorder_rc[i] << " lo " << n.m_lo << " hi " << n.m_hi << "\n"; } ); } + void bdd_manager::reorder_incref(unsigned n) { + if (m_reorder_rc[n] != UINT_MAX) m_reorder_rc[n]++; + } + + void bdd_manager::reorder_decref(unsigned n) { + if (m_reorder_rc[n] != UINT_MAX) m_reorder_rc[n]--; + } + void bdd_manager::reserve_var(unsigned i) { while (m_var2level.size() <= i) { unsigned v = m_var2level.size(); @@ -455,9 +554,12 @@ namespace sat { return bdd(mk_not_rec(b.root), this); } catch (mem_out) { + throw; +#if 0 try_reorder(); if (!first) throw; first = false; +#endif } } } @@ -532,12 +634,13 @@ namespace sat { push(mk_ite_rec(a1, b1, c1)); push(mk_ite_rec(a2, b2, c2)); r = make_node(lvl, read(2), read(1)); - pop(2); + pop(2); e1->m_result = r; return r; } bdd bdd_manager::mk_exists(unsigned n, unsigned const* vars, bdd const& b) { + // VERIFY(well_formed()); return bdd(mk_quant(n, vars, b.root, bdd_or_op), this); } @@ -570,9 +673,11 @@ namespace sat { 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 (check_result(e1, e2, a, b, q_op)) + if (check_result(e1, e2, a, b, q_op)) { r = e2->m_result; + } else { + VERIFY(e1->m_result == -1); push(mk_quant_rec(l, lo(b), op)); push(mk_quant_rec(l, hi(b), op)); r = make_node(lvl, read(2), read(1)); @@ -580,26 +685,29 @@ namespace sat { e1->m_result = r; } } + VERIFY(r != UINT_MAX); return r; } - double bdd_manager::count(bdd const& b, unsigned z) { + double bdd_manager::count(BDD b, unsigned z) { init_mark(); m_count.resize(m_nodes.size()); m_count[0] = z; m_count[1] = 1-z; set_mark(0); set_mark(1); - m_todo.push_back(b.root); + m_todo.push_back(b); while (!m_todo.empty()) { BDD r = m_todo.back(); if (is_marked(r)) { m_todo.pop_back(); } else if (!is_marked(lo(r))) { + VERIFY (is_const(r) || r != lo(r)); m_todo.push_back(lo(r)); } else if (!is_marked(hi(r))) { + VERIFY (is_const(r) || r != hi(r)); m_todo.push_back(hi(r)); } else { @@ -608,7 +716,7 @@ namespace sat { m_todo.pop_back(); } } - return m_count[b.root]; + return m_count[b]; } unsigned bdd_manager::bdd_size(bdd const& b) { @@ -644,8 +752,8 @@ namespace sat { } void bdd_manager::gc() { + m_free_nodes.reset(); IF_VERBOSE(3, 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; @@ -674,6 +782,7 @@ namespace sat { for (unsigned i = m_nodes.size(); i-- > 2; ) { if (!reachable[i]) { m_nodes[i].set_internal(); + VERIFY(m_nodes[i].m_refcount == 0); m_free_nodes.push_back(i); } } @@ -681,10 +790,25 @@ namespace sat { std::sort(m_free_nodes.begin(), m_free_nodes.end()); m_free_nodes.reverse(); - for (auto* e : m_op_cache) { - m_alloc.deallocate(sizeof(*e), e); + ptr_vector to_delete, to_keep; + for (auto* e : m_op_cache) { + // std::cout << "check: " << e << "\n"; + if (!reachable[e->m_bdd1] || !reachable[e->m_bdd2] || !reachable[e->m_op] || (e->m_result != -1 && !reachable[e->m_result])) { + to_delete.push_back(e); + } + else { + to_keep.push_back(e); + } } m_op_cache.reset(); + for (op_entry* e : to_delete) { + // std::cout << "erase: " << e << "\n"; + m_alloc.deallocate(sizeof(*e), e); + } + for (op_entry* e : to_keep) { + m_op_cache.insert(e); + } + m_node_table.reset(); // re-populate node cache for (unsigned i = m_nodes.size(); i-- > 2; ) { @@ -693,6 +817,7 @@ namespace sat { m_node_table.insert(m_nodes[i]); } } + SASSERT(well_formed()); } void bdd_manager::init_mark() { @@ -707,6 +832,7 @@ namespace sat { std::ostream& bdd_manager::display(std::ostream& out, bdd const& b) { init_mark(); m_todo.push_back(b.root); + m_reorder_rc.reserve(m_nodes.size()); while (!m_todo.empty()) { BDD r = m_todo.back(); if (is_marked(r)) { @@ -723,7 +849,7 @@ namespace sat { m_todo.push_back(hi(r)); } else { - out << r << " : " << var(r) << " " << lo(r) << " " << hi(r) << "\n"; + out << r << " : " << var(r) << " @ " << level(r) << " " << lo(r) << " " << hi(r) << " " << m_reorder_rc[r] << "\n"; set_mark(r); m_todo.pop_back(); } @@ -731,30 +857,52 @@ namespace sat { return out; } - void bdd_manager::well_formed() { + bool bdd_manager::well_formed() { for (unsigned n : m_free_nodes) { - VERIFY(lo(n) == 0 && hi(n) == 0 && m_nodes[n].m_refcount == 0); + if (!(lo(n) == 0 && hi(n) == 0 && m_nodes[n].m_refcount == 0)) { + std::cout << "free node is not internal " << n << " " << lo(n) << " " << hi(n) << " " << m_nodes[n].m_refcount << "\n"; + display(std::cout); + UNREACHABLE(); + } } 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; + if (!is_const(lo) && level(lo) >= lvl) { + std::cout << n.m_index << " lo: " << lo << "\n"; + display(std::cout); + } VERIFY(is_const(lo) || level(lo) < lvl); + if (!is_const(hi) && level(hi) >= lvl) { + std::cout << n.m_index << " hi: " << hi << "\n"; + display(std::cout); + } VERIFY(is_const(hi) || level(hi) < lvl); + if (!is_const(lo) && m_nodes[lo].is_internal()) { + std::cout << n.m_index << " lo: " << lo << "\n"; + display(std::cout); + } + if (!is_const(hi) && m_nodes[hi].is_internal()) { + std::cout << n.m_index << " hi: " << hi << "\n"; + display(std::cout); + } + VERIFY(is_const(lo) || !m_nodes[lo].is_internal()); + VERIFY(is_const(hi) || !m_nodes[hi].is_internal()); } + return true; } std::ostream& bdd_manager::display(std::ostream& out) { + m_reorder_rc.reserve(m_nodes.size()); 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"; + out << i << " : v" << m_level2var[n.m_level] << " " << n.m_lo << " " << n.m_hi << " rc " << m_reorder_rc[i] << "\n"; } for (unsigned i = 0; i < m_level2nodes.size(); ++i) { - out << i << " : "; - for (unsigned l : m_level2nodes[i]) out << l << " "; - out << "\n"; + out << "level: " << i << " : " << m_level2nodes[i] << "\n"; } return out; } diff --git a/src/sat/sat_bdd.h b/src/sat/sat_bdd.h index 41e45c822..41d1115b9 100644 --- a/src/sat/sat_bdd.h +++ b/src/sat/sat_bdd.h @@ -50,7 +50,7 @@ namespace sat { m_hi(hi), m_index(0) {} - bdd_node(): m_level(0), m_lo(0), m_hi(0), m_index(0) {} + bdd_node(): m_refcount(0), m_level(0), m_lo(0), m_hi(0), m_index(0) {} unsigned m_refcount : 10; unsigned m_level : 22; BDD m_lo; @@ -58,7 +58,13 @@ namespace sat { unsigned m_index; unsigned hash() const { return mk_mix(m_level, m_lo, m_hi); } bool is_internal() const { return m_lo == 0 && m_hi == 0; } - void set_internal() { m_lo = m_hi = 0; } + void set_internal() { m_lo = 0; m_hi = 0; } + }; + + enum cost_metric { + cnf_cost, + dnf_cost, + bdd_cost }; struct hash_node { @@ -94,7 +100,7 @@ namespace sat { struct eq_entry { bool operator()(op_entry * a, op_entry * b) const { - return a->hash() == b->hash(); + return a->m_bdd1 == b->m_bdd2 && a->m_bdd2 == b->m_bdd2 && a->m_op == b->m_op; } }; @@ -117,9 +123,11 @@ namespace sat { bool m_disable_gc; bool m_is_new_node; unsigned m_max_num_bdd_nodes; - unsigned_vector m_S, m_T; // used for reordering + unsigned_vector m_S, m_T, m_to_free; // used for reordering vector m_level2nodes; - unsigned_vector m_max_parent; + unsigned_vector m_reorder_rc; + cost_metric m_cost_metric; + BDD m_cost_bdd; BDD make_node(unsigned level, BDD l, BDD r); bool is_new_node() const { return m_is_new_node; } @@ -141,15 +149,16 @@ namespace sat { void push_entry(op_entry* e); bool check_result(op_entry*& e1, op_entry const* e2, BDD a, BDD b, BDD c); - double count(bdd const& b, unsigned z); + double count(BDD b, unsigned z); - 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; } void init_reorder(); + void reorder_incref(unsigned n); + void reorder_decref(unsigned n); void sift_up(unsigned level); void sift_var(unsigned v); double current_cost(); @@ -166,12 +175,12 @@ namespace sat { 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 void inc_ref(BDD b) { if (m_nodes[b].m_refcount != max_rc) m_nodes[b].m_refcount++; VERIFY(!m_free_nodes.contains(b)); } + inline void dec_ref(BDD b) { if (m_nodes[b].m_refcount != max_rc) m_nodes[b].m_refcount--; VERIFY(!m_free_nodes.contains(b)); } inline BDD level2bdd(unsigned l) const { return m_var2bdd[m_level2var[l]]; } - double dnf_size(bdd const& b) { return count(b, 0); } - double cnf_size(bdd const& b) { return count(b, 1); } + double dnf_size(BDD b) { return count(b, 0); } + double cnf_size(BDD b) { return count(b, 1); } unsigned bdd_size(bdd const& b); bdd mk_not(bdd b); @@ -180,7 +189,7 @@ namespace sat { bdd mk_xor(bdd const& a, bdd const& b); void reserve_var(unsigned v); - void well_formed(); + bool well_formed(); public: struct mem_out {}; @@ -205,7 +214,9 @@ namespace sat { std::ostream& display(std::ostream& out); std::ostream& display(std::ostream& out, bdd const& b); + void gc(); void try_reorder(); + void try_cnf_reorder(bdd const& b); }; class bdd { @@ -234,8 +245,8 @@ namespace sat { 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 { return m->cnf_size(*this); } - double dnf_size() const { return m->dnf_size(*this); } + double cnf_size() const { return m->cnf_size(root); } + double dnf_size() const { return m->dnf_size(root); } unsigned bdd_size() const { return m->bdd_size(*this); } }; diff --git a/src/sat/sat_elim_vars.cpp b/src/sat/sat_elim_vars.cpp index 6edc125ea..99c15c247 100644 --- a/src/sat/sat_elim_vars.cpp +++ b/src/sat/sat_elim_vars.cpp @@ -26,6 +26,7 @@ namespace sat{ elim_vars::elim_vars(simplifier& s) : simp(s), s(s.s), m(20) { m_mark_lim = 0; m_max_literals = 11; + m_miss = 0; } bool elim_vars::operator()(bool_var v) { @@ -57,10 +58,11 @@ namespace sat{ double sz1 = b1.cnf_size(); if (sz1 > 2*clause_size) { return false; - } + } if (sz1 <= clause_size) { return elim_var(v, b1); } + m_vars.reverse(); bdd b2 = elim_var(v); double sz2 = b2.cnf_size(); @@ -73,6 +75,11 @@ namespace sat{ if (sz3 <= clause_size) { return elim_var(v, b3); } +#if 0 + m.try_cnf_reorder(b3); + sz3 = b3.cnf_size(); + if (sz3 <= clause_size) ++m_miss; +#endif return false; } diff --git a/src/sat/sat_elim_vars.h b/src/sat/sat_elim_vars.h index 8893bbc40..e4843c41c 100644 --- a/src/sat/sat_elim_vars.h +++ b/src/sat/sat_elim_vars.h @@ -40,6 +40,7 @@ namespace sat { unsigned m_mark_lim; unsigned_vector m_var2index; unsigned_vector m_occ; + unsigned m_miss; unsigned m_max_literals; @@ -61,6 +62,7 @@ namespace sat { public: elim_vars(simplifier& s); bool operator()(bool_var v); + unsigned miss() const { return m_miss; } }; }; diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index 5c039f664..be698fc46 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -412,11 +412,17 @@ namespace sat { for (literal l1 : m_trail) { SASSERT(is_true(l1)); for (literal l2 : m_binary[l1.index()]) { + VERIFY(is_true(l2)); if (is_undef(l2)) return true; } unsigned sz = m_ternary_count[(~l1).index()]; for (binary b : m_ternary[(~l1).index()]) { if (sz-- == 0) break; + if (!(is_true(b.m_u) || is_true(b.m_v) || (is_undef(b.m_v) && is_undef(b.m_u)))) { + std::cout << b.m_u << " " << b.m_v << "\n"; + std::cout << get_level(b.m_u) << " " << get_level(b.m_v) << " level: " << m_level << "\n"; + UNREACHABLE(); + } if ((is_false(b.m_u) && is_undef(b.m_v)) || (is_false(b.m_v) && is_undef(b.m_u))) return true; } @@ -424,6 +430,7 @@ namespace sat { for (nary * n : m_nary_clauses) { if (n->size() == 1 && !is_true(n->get_head())) { for (literal lit : *n) { + VERIFY(!is_undef(lit)); if (is_undef(lit)) return true; } } @@ -1743,74 +1750,10 @@ namespace sat { bool lookahead::check_autarky(literal l, unsigned level) { return false; -#if 0 - // no propagations are allowed to reduce clauses. - for (nary * cp : m_nary[(~l).index()]) { - clause& c = *cp; - unsigned sz = c.size(); - bool found = false; - for (unsigned i = 0; !found && i < sz; ++i) { - found = is_true(c[i]); - if (found) { - TRACE("sat", tout << c[i] << " is true in " << c << "\n";); - } - } - IF_VERBOSE(2, verbose_stream() << "skip autarky " << l << "\n";); - if (!found) return false; - } - // - // bail out if there is a pending binary propagation. - // In general, we would have to check, recursively that - // a binary propagation does not create reduced clauses. - // - literal_vector const& lits = m_binary[l.index()]; - TRACE("sat", tout << l << ": " << lits << "\n";); - for (unsigned i = 0; i < lits.size(); ++i) { - literal l2 = lits[i]; - if (is_true(l2)) continue; - SASSERT(!is_false(l2)); - return false; - } - - return true; -#endif } - - void lookahead::update_lookahead_reward(literal l, unsigned level) { - if (m_lookahead_reward == 0) { - if (!check_autarky(l, level)) { - // skip - } - else if (get_lookahead_reward(l) == 0) { - ++m_stats.m_autarky_propagations; - IF_VERBOSE(1, verbose_stream() << "(sat.lookahead autarky " << l << ")\n";); - - TRACE("sat", tout << "autarky: " << l << " @ " << m_stamp[l.var()] - << " " - << (!m_binary[l.index()].empty() || m_nary_count[l.index()] != 0) << "\n";); - lookahead_backtrack(); - assign(l); - propagate(); - } - else { - ++m_stats.m_autarky_equivalences; - // l => p is known, but p => l is possibly not. - // add p => l. - // justification: any consequence of l - // that is not a consequence of p does not - // reduce the clauses. - literal p = get_parent(l); - SASSERT(p != null_literal); - if (m_stamp[p.var()] > m_stamp[l.var()]) { - TRACE("sat", tout << "equivalence " << l << " == " << p << "\n"; display(tout);); - IF_VERBOSE(1, verbose_stream() << "(sat.lookahead equivalence " << l << " == " << p << ")\n";); - add_binary(~l, p); - set_level(l, p); - } - } - } - else { + void lookahead::update_lookahead_reward(literal l, unsigned level) { + if (m_lookahead_reward != 0) { inc_lookahead_reward(l, m_lookahead_reward); } } @@ -1852,7 +1795,6 @@ namespace sat { literal last_changed = null_literal; unsigned num_iterations = 0; while (change && num_iterations < m_config.m_dl_max_iterations && !inconsistent()) { - change = false; num_iterations++; for (unsigned i = 0; !inconsistent() && i < m_lookahead.size(); ++i) { literal lit = m_lookahead[i].m_lit; diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index d30485254..64a4ef63e 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -247,6 +247,7 @@ namespace sat { inline void set_true(literal l) { m_stamp[l.var()] = m_level + l.sign(); } inline void set_undef(literal l) { m_stamp[l.var()] = 0; } void set_level(literal d, literal s) { m_stamp[d.var()] = (m_stamp[s.var()] & ~0x1) + d.sign(); } + unsigned get_level(literal d) const { return m_stamp[d.var()]; } lbool value(literal l) const { return is_undef(l) ? l_undef : is_true(l) ? l_true : l_false; } // set the level within a scope of the search. diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index b967ade06..b1f0431cc 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -1657,6 +1657,7 @@ namespace sat { bool_var_vector vars; order_vars_for_elim(vars); sat::elim_vars elim_bdd(*this); + unsigned bdd_vars = 0; for (bool_var v : vars) { checkpoint(); @@ -1665,10 +1666,13 @@ namespace sat { if (try_eliminate(v)) { m_num_elim_vars++; } - else if (elim_bdd(v)) { + else if (false && elim_bdd(v)) { m_num_elim_vars++; + ++bdd_vars; } } + std::cout << "bdd elim: " << bdd_vars << "\n"; + std::cout << "bdd miss: " << elim_bdd.miss() << "\n"; m_pos_cls.finalize(); m_neg_cls.finalize(); diff --git a/src/test/bdd.cpp b/src/test/bdd.cpp index b60522740..ea5a0bc34 100644 --- a/src/test/bdd.cpp +++ b/src/test/bdd.cpp @@ -67,6 +67,7 @@ namespace sat { std::cout << "before reorder:\n"; std::cout << c1 << "\n"; std::cout << c1.bdd_size() << "\n"; + m.gc(); m.try_reorder(); std::cout << "after reorder:\n"; std::cout << c1 << "\n"; diff --git a/src/util/vector.h b/src/util/vector.h index c60585512..f068481db 100644 --- a/src/util/vector.h +++ b/src/util/vector.h @@ -472,6 +472,11 @@ typedef svector char_vector; typedef svector signed_char_vector; typedef svector double_vector; +inline std::ostream& operator<<(std::ostream& out, unsigned_vector const& v) { + for (unsigned u : v) out << u << " "; + return out; +} + template struct vector_hash_tpl { Hash m_hash;