mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fixup bdd reordering, assertions and perf

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-10-18 19:32:49 -07:00
parent 553bf74f47
commit 636f740b1a
4 changed files with 52 additions and 79 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

89
src/sat/sat_bdd.cpp
View file

@ -19,6 +19,7 @@ Revision History:
#include "sat/sat_bdd.h" #include "sat/sat_bdd.h"
#include "util/trace.h" #include "util/trace.h"
#include "util/stopwatch.h"
namespace sat { namespace sat {
@ -60,7 +61,7 @@ namespace sat {
m_alloc.deallocate(sizeof(*m_spare_entry), m_spare_entry); m_alloc.deallocate(sizeof(*m_spare_entry), m_spare_entry);
} }
for (auto* e : m_op_cache) { for (auto* e : m_op_cache) {
VERIFY(e != m_spare_entry); SASSERT(e != m_spare_entry);
m_alloc.deallocate(sizeof(*e), e); m_alloc.deallocate(sizeof(*e), e);
} }
} }
@ -87,12 +88,9 @@ namespace sat {
return apply_rec(arg1, arg2, op); return apply_rec(arg1, arg2, op);
} }
catch (mem_out) { catch (mem_out) {
throw;
#if 0
try_reorder(); try_reorder();
if (!first) throw; if (!first) throw;
first = false; first = false;
#endif
} }
} }
SASSERT(well_formed()); SASSERT(well_formed());
@ -109,9 +107,8 @@ namespace sat {
bool bdd_manager::check_result(op_entry*& e1, op_entry const* e2, BDD a, BDD b, BDD c) { 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) { if (e1 != e2) {
VERIFY(e2->m_result != -1); SASSERT(e2->m_result != -1);
push_entry(e1); push_entry(e1);
e1 = nullptr; e1 = nullptr;
return true; return true;
@ -120,7 +117,7 @@ namespace sat {
e1->m_bdd1 = a; e1->m_bdd1 = a;
e1->m_bdd2 = b; e1->m_bdd2 = b;
e1->m_op = c; e1->m_op = c;
VERIFY(e1->m_result == -1); SASSERT(e1->m_result == -1);
return false; return false;
} }
} }
@ -157,7 +154,7 @@ namespace sat {
SASSERT(!m_free_nodes.contains(e2->m_result)); SASSERT(!m_free_nodes.contains(e2->m_result));
return e2->m_result; return e2->m_result;
} }
// VERIFY(well_formed()); // SASSERT(well_formed());
BDD r; BDD r;
if (level(a) == level(b)) { if (level(a) == level(b)) {
push(apply_rec(lo(a), lo(b), op)); push(apply_rec(lo(a), lo(b), op));
@ -176,7 +173,7 @@ namespace sat {
} }
pop(2); pop(2);
e1->m_result = r; e1->m_result = r;
// VERIFY(well_formed()); // SASSERT(well_formed());
SASSERT(!m_free_nodes.contains(r)); SASSERT(!m_free_nodes.contains(r));
return r; return r;
} }
@ -205,7 +202,6 @@ namespace sat {
else { else {
void * mem = m_alloc.allocate(sizeof(op_entry)); void * mem = m_alloc.allocate(sizeof(op_entry));
result = new (mem) op_entry(l, r, op); result = new (mem) op_entry(l, r, op);
// std::cout << "alloc: " << result << "\n";
} }
result->m_result = -1; result->m_result = -1;
return result; return result;
@ -221,11 +217,8 @@ namespace sat {
if (l == h) { if (l == h) {
return l; return l;
} }
if (!is_const(l) && level(l) >= lvl) { SASSERT(is_const(l) || level(l) < lvl);
display(std::cout << l << " level: " << level(l) << " lvl: " << lvl << "\n"); SASSERT(is_const(h) || level(h) < lvl);
}
VERIFY(is_const(l) || level(l) < lvl);
VERIFY(is_const(h) || level(h) < lvl);
bdd_node n(lvl, l, h); bdd_node n(lvl, l, h);
node_table::entry* e = m_node_table.insert_if_not_there2(n); node_table::entry* e = m_node_table.insert_if_not_there2(n);
@ -353,7 +346,7 @@ namespace sat {
void bdd_manager::sift_up(unsigned lvl) { void bdd_manager::sift_up(unsigned lvl) {
if (m_level2nodes[lvl].empty()) return; if (m_level2nodes[lvl].empty()) return;
// VERIFY(well_formed()); // SASSERT(well_formed());
// exchange level and level + 1. // exchange level and level + 1.
m_S.reset(); m_S.reset();
m_T.reset(); m_T.reset();
@ -452,8 +445,8 @@ namespace sat {
unsigned n = m_to_free[i]; unsigned n = m_to_free[i];
bdd_node& node = m_nodes[n]; bdd_node& node = m_nodes[n];
if (!node.is_internal()) { if (!node.is_internal()) {
VERIFY(!m_free_nodes.contains(n)); SASSERT(!m_free_nodes.contains(n));
VERIFY(node.m_refcount == 0); SASSERT(node.m_refcount == 0);
m_free_nodes.push_back(n); m_free_nodes.push_back(n);
m_node_table.remove(node); m_node_table.remove(node);
BDD l = lo(n); BDD l = lo(n);
@ -485,7 +478,7 @@ namespace sat {
tout << i << " " << m_reorder_rc[i] << "\n"; tout << i << " " << m_reorder_rc[i] << "\n";
}}); }});
// VERIFY(well_formed()); // SASSERT(well_formed());
} }
void bdd_manager::init_reorder() { void bdd_manager::init_reorder() {
@ -554,12 +547,9 @@ namespace sat {
return bdd(mk_not_rec(b.root), this); return bdd(mk_not_rec(b.root), this);
} }
catch (mem_out) { catch (mem_out) {
throw;
#if 0
try_reorder(); try_reorder();
if (!first) throw; if (!first) throw;
first = false; first = false;
#endif
} }
} }
} }
@ -640,7 +630,7 @@ namespace sat {
} }
bdd bdd_manager::mk_exists(unsigned n, unsigned const* vars, bdd const& b) { bdd bdd_manager::mk_exists(unsigned n, unsigned const* vars, bdd const& b) {
// VERIFY(well_formed()); // SASSERT(well_formed());
return bdd(mk_quant(n, vars, b.root, bdd_or_op), this); return bdd(mk_quant(n, vars, b.root, bdd_or_op), this);
} }
@ -677,7 +667,7 @@ namespace sat {
r = e2->m_result; r = e2->m_result;
} }
else { else {
VERIFY(e1->m_result == -1); SASSERT(e1->m_result == -1);
push(mk_quant_rec(l, lo(b), op)); push(mk_quant_rec(l, lo(b), op));
push(mk_quant_rec(l, hi(b), op)); push(mk_quant_rec(l, hi(b), op));
r = make_node(lvl, read(2), read(1)); r = make_node(lvl, read(2), read(1));
@ -685,7 +675,7 @@ namespace sat {
e1->m_result = r; e1->m_result = r;
} }
} }
VERIFY(r != UINT_MAX); SASSERT(r != UINT_MAX);
return r; return r;
} }
@ -703,11 +693,11 @@ namespace sat {
m_todo.pop_back(); m_todo.pop_back();
} }
else if (!is_marked(lo(r))) { else if (!is_marked(lo(r))) {
VERIFY (is_const(r) || r != lo(r)); SASSERT (is_const(r) || r != lo(r));
m_todo.push_back(lo(r)); m_todo.push_back(lo(r));
} }
else if (!is_marked(hi(r))) { else if (!is_marked(hi(r))) {
VERIFY (is_const(r) || r != hi(r)); SASSERT (is_const(r) || r != hi(r));
m_todo.push_back(hi(r)); m_todo.push_back(hi(r));
} }
else { else {
@ -782,7 +772,7 @@ namespace sat {
for (unsigned i = m_nodes.size(); i-- > 2; ) { for (unsigned i = m_nodes.size(); i-- > 2; ) {
if (!reachable[i]) { if (!reachable[i]) {
m_nodes[i].set_internal(); m_nodes[i].set_internal();
VERIFY(m_nodes[i].m_refcount == 0); SASSERT(m_nodes[i].m_refcount == 0);
m_free_nodes.push_back(i); m_free_nodes.push_back(i);
} }
} }
@ -792,8 +782,7 @@ namespace sat {
ptr_vector<op_entry> to_delete, to_keep; ptr_vector<op_entry> to_delete, to_keep;
for (auto* e : m_op_cache) { for (auto* e : m_op_cache) {
// std::cout << "check: " << e << "\n"; if (e->m_result != -1) {
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); to_delete.push_back(e);
} }
else { else {
@ -802,7 +791,6 @@ namespace sat {
} }
m_op_cache.reset(); m_op_cache.reset();
for (op_entry* e : to_delete) { for (op_entry* e : to_delete) {
// std::cout << "erase: " << e << "\n";
m_alloc.deallocate(sizeof(*e), e); m_alloc.deallocate(sizeof(*e), e);
} }
for (op_entry* e : to_keep) { for (op_entry* e : to_keep) {
@ -858,11 +846,15 @@ namespace sat {
} }
bool bdd_manager::well_formed() { bool bdd_manager::well_formed() {
bool ok = true;
for (unsigned n : m_free_nodes) { for (unsigned n : m_free_nodes) {
if (!(lo(n) == 0 && hi(n) == 0 && m_nodes[n].m_refcount == 0)) { ok &= (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"; if (!ok) {
display(std::cout); IF_VERBOSE(0,
verbose_stream() << "free node is not internal " << n << " " << lo(n) << " " << hi(n) << " " << m_nodes[n].m_refcount << "\n";
display(verbose_stream()););
UNREACHABLE(); UNREACHABLE();
return false;
} }
} }
for (bdd_node const& n : m_nodes) { for (bdd_node const& n : m_nodes) {
@ -870,28 +862,17 @@ namespace sat {
unsigned lvl = n.m_level; unsigned lvl = n.m_level;
BDD lo = n.m_lo; BDD lo = n.m_lo;
BDD hi = n.m_hi; BDD hi = n.m_hi;
if (!is_const(lo) && level(lo) >= lvl) { ok &= is_const(lo) || level(lo) < lvl;
std::cout << n.m_index << " lo: " << lo << "\n"; ok &= is_const(hi) || level(hi) < lvl;
display(std::cout); ok &= is_const(lo) || !m_nodes[lo].is_internal();
ok &= is_const(hi) || !m_nodes[hi].is_internal();
if (!ok) {
IF_VERBOSE(0, display(verbose_stream() << n.m_index << " lo " << lo << " hi " << hi << "\n"););
UNREACHABLE();
return false;
} }
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; return ok;
} }
std::ostream& bdd_manager::display(std::ostream& out) { std::ostream& bdd_manager::display(std::ostream& out) {

29
src/sat/sat_elim_vars.cpp
View file

@ -27,6 +27,8 @@ namespace sat{
m_mark_lim = 0; m_mark_lim = 0;
m_max_literals = 11; m_max_literals = 11;
m_miss = 0; m_miss = 0;
m_hit1 = 0;
m_hit2 = 0;
} }
bool elim_vars::operator()(bool_var v) { bool elim_vars::operator()(bool_var v) {
@ -57,29 +59,20 @@ namespace sat{
bdd b1 = elim_var(v); bdd b1 = elim_var(v);
double sz1 = b1.cnf_size(); double sz1 = b1.cnf_size();
if (sz1 > 2*clause_size) { if (sz1 > 2*clause_size) {
++m_miss;
return false; return false;
} }
if (sz1 <= clause_size) { if (sz1 <= clause_size) {
++m_hit1;
return elim_var(v, b1); return elim_var(v, b1);
} }
m.try_cnf_reorder(b1);
m_vars.reverse(); sz1 = b1.cnf_size();
bdd b2 = elim_var(v); if (sz1 <= clause_size) {
double sz2 = b2.cnf_size(); ++m_hit2;
if (sz2 <= clause_size) { return elim_var(v, b1);
return elim_var(v, b2); }
} ++m_miss;
shuffle_vars();
bdd b3 = elim_var(v);
double sz3 = b3.cnf_size();
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; return false;
} }

6
src/sat/sat_elim_vars.h
View file

@ -41,6 +41,8 @@ namespace sat {
unsigned_vector m_var2index; unsigned_vector m_var2index;
unsigned_vector m_occ; unsigned_vector m_occ;
unsigned m_miss; unsigned m_miss;
unsigned m_hit1;
unsigned m_hit2;
unsigned m_max_literals; unsigned m_max_literals;
@ -62,7 +64,9 @@ namespace sat {
public: public:
elim_vars(simplifier& s); elim_vars(simplifier& s);
bool operator()(bool_var v); bool operator()(bool_var v);
unsigned miss() const { return m_miss; } unsigned hit2() const { return m_hit1; } // first round bdd construction is minimal
unsigned hit1() const { return m_hit2; } // minimal after reshufling
unsigned miss() const { return m_miss; } // not-minimal
}; };
}; };

7
src/sat/sat_simplifier.cpp
View file

@ -1657,8 +1657,6 @@ namespace sat {
bool_var_vector vars; bool_var_vector vars;
order_vars_for_elim(vars); order_vars_for_elim(vars);
sat::elim_vars elim_bdd(*this); sat::elim_vars elim_bdd(*this);
unsigned bdd_vars = 0;
for (bool_var v : vars) { for (bool_var v : vars) {
checkpoint(); checkpoint();
if (m_elim_counter < 0) if (m_elim_counter < 0)
@ -1666,13 +1664,10 @@ namespace sat {
if (try_eliminate(v)) { if (try_eliminate(v)) {
m_num_elim_vars++; m_num_elim_vars++;
} }
else if (false && elim_bdd(v)) { else if (elim_bdd(v)) {
m_num_elim_vars++; 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_pos_cls.finalize();
m_neg_cls.finalize(); m_neg_cls.finalize();