From 159026b5e878a4ffee771725e0262754ace15c0d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 26 Aug 2022 10:44:33 -0700 Subject: [PATCH] regression fix to ackerman gc and memory smash, perf fix for handling bv2int axioms, perf fix for filtering ackerman this update addresses some perf regressions introduced when handling axioms for bv2int and a memory smash regression when decoupling bv-ackerman from in-processing. It adds a filter based on bv_eq_axioms for disabling ackerman reductions on disequalities. --- src/sat/smt/bv_ackerman.cpp | 9 ++++++--- src/sat/smt/bv_internalize.cpp | 2 ++ src/sat/smt/bv_solver.cpp | 20 +++++++++++++++++--- src/sat/smt/bv_solver.h | 5 +++-- src/sat/smt/euf_solver.cpp | 2 +- src/smt/theory_bv.cpp | 20 ++++++++++++++++---- src/smt/theory_bv.h | 1 + 7 files changed, 46 insertions(+), 13 deletions(-) diff --git a/src/sat/smt/bv_ackerman.cpp b/src/sat/smt/bv_ackerman.cpp index 88cca5257..940b1ebb0 100644 --- a/src/sat/smt/bv_ackerman.cpp +++ b/src/sat/smt/bv_ackerman.cpp @@ -49,16 +49,19 @@ namespace bv { update_glue(*other); vv::push_to_front(m_queue, other); - if (other == n) { + bool do_gc = other == n; + if (other == n) new_tmp(); - gc(); - } + if (other->m_glue == 0) { + do_gc = false; remove(other); add_cc(v1, v2); } else if (other->m_count > 2*m_propagate_high_watermark) propagate(); + if (do_gc) + gc(); } void ackerman::used_diseq_eh(euf::theory_var v1, euf::theory_var v2) { diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp index 9d4719544..04fde22f1 100644 --- a/src/sat/smt/bv_internalize.cpp +++ b/src/sat/smt/bv_internalize.cpp @@ -429,6 +429,8 @@ namespace bv { args.push_back(m.mk_ite(b, m_autil.mk_int(power2(i++)), zero)); expr_ref sum(m_autil.mk_add(sz, args.data()), m); sat::literal lit = eq_internalize(n, sum); + m_bv2ints.push_back(expr2enode(n)); + ctx.push(push_back_vector(m_bv2ints)); add_unit(lit); } diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp index 2a39fae6a..1e3cb0171 100644 --- a/src/sat/smt/bv_solver.cpp +++ b/src/sat/smt/bv_solver.cpp @@ -211,9 +211,8 @@ namespace bv { return; } euf::enode* n1 = var2enode(eq.v1()); - for (euf::enode* bv2int : euf::enode_class(n1)) { - if (!bv.is_bv2int(bv2int->get_expr())) - continue; + + auto propagate_bv2int = [&](euf::enode* bv2int) { euf::enode* bv2int_arg = bv2int->get_arg(0); for (euf::enode* p : euf::enode_parents(n1->get_root())) { if (bv.is_int2bv(p->get_expr()) && p->get_sort() == bv2int_arg->get_sort() && p->get_root() != bv2int_arg->get_root()) { @@ -224,6 +223,19 @@ namespace bv { break; } } + }; + + if (m_bv2ints.size() < n1->class_size()) { + for (auto* bv2int : m_bv2ints) { + if (bv2int->get_root() == n1->get_root()) + propagate_bv2int(bv2int); + } + } + else { + for (euf::enode* bv2int : euf::enode_class(n1)) { + if (bv.is_bv2int(bv2int->get_expr())) + propagate_bv2int(bv2int); + } } } @@ -279,6 +291,8 @@ namespace bv { ++m_stats.m_num_ne2bit; s().assign(consequent, mk_ne2bit_justification(undef_idx, v1, v2, consequent, antecedent)); } + else if (!get_config().m_bv_eq_axioms) + ; else if (s().at_search_lvl()) { force_push(); assert_ackerman(v1, v2); diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h index 5920f70f6..b77343e30 100644 --- a/src/sat/smt/bv_solver.h +++ b/src/sat/smt/bv_solver.h @@ -207,8 +207,9 @@ namespace bv { literal_vector m_tmp_literals; svector m_prop_queue; unsigned_vector m_prop_queue_lim; - unsigned m_prop_queue_head { 0 }; - sat::literal m_true { sat::null_literal }; + unsigned m_prop_queue_head = 0; + sat::literal m_true = sat::null_literal; + euf::enode_vector m_bv2ints; // internalize void insert_bv2a(bool_var bv, atom * a) { m_bool_var2atom.setx(bv, a, 0); } diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index 56480aa85..8a22ae68b 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -527,7 +527,7 @@ namespace euf { bool merged = false; for (unsigned i = m_egraph.nodes().size(); i-- > 0; ) { euf::enode* n = m_egraph.nodes()[i]; - if (!is_shared(n) || !m.is_bool(n->get_expr())) + if (!m.is_bool(n->get_expr()) || !is_shared(n)) continue; if (n->value() == l_true && !m.is_true(n->get_root()->get_expr())) { m_egraph.merge(n, mk_true(), to_ptr(sat::literal(n->bool_var()))); diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 6c4e1b3a7..b4290a198 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -599,6 +599,8 @@ namespace smt { TRACE("bv", tout << mk_bounded_pp(n, m) << "\n";); process_args(n); mk_enode(n); + m_bv2int.push_back(ctx.get_enode(n)); + ctx.push_trail(push_back_vector(m_bv2int)); if (!ctx.relevancy()) assert_bv2int_axiom(n); } @@ -1496,12 +1498,10 @@ namespace smt { unsigned sz = m_bits[v1].size(); bool changed = true; TRACE("bv", tout << "bits size: " << sz << "\n";); - if (sz == 0) { + if (sz == 0 && !m_bv2int.empty()) { // int2bv(bv2int(x)) = x when int2bv(bv2int(x)) has same sort as x enode* n1 = get_enode(r1); - for (enode* bv2int : *n1) { - if (!m_util.is_bv2int(bv2int->get_expr())) - continue; + auto propagate_bv2int = [&](enode* bv2int) { enode* bv2int_arg = bv2int->get_arg(0); for (enode* p : enode::parents(n1->get_root())) { if (m_util.is_int2bv(p->get_expr()) && p->get_root() != bv2int_arg->get_root() && p->get_sort() == bv2int_arg->get_sort()) { @@ -1514,6 +1514,18 @@ namespace smt { break; } } + }; + + if (m_bv2int.size() < n1->get_class_size()) { + for (enode* bv2int : m_bv2int) + if (bv2int->get_root() == n1->get_root()) + propagate_bv2int(bv2int); + } + else { + for (enode* bv2int : *n1) { + if (m_util.is_bv2int(bv2int->get_expr())) + propagate_bv2int(bv2int); + } } } do { diff --git a/src/smt/theory_bv.h b/src/smt/theory_bv.h index 5a5e1e6f2..a66aaab8a 100644 --- a/src/smt/theory_bv.h +++ b/src/smt/theory_bv.h @@ -112,6 +112,7 @@ namespace smt { svector m_wpos; // per var, watch position for fixed variable detection. vector m_zero_one_bits; // per var, see comment in the struct zero_one_bit bool_var2atom m_bool_var2atom; + enode_vector m_bv2int; typedef svector vars; typedef std::pair value_sort_pair;