From ac1b3fc6f2690101d706d39ea09529241c559a28 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 20 Nov 2020 11:12:45 -0800 Subject: [PATCH] fix delay blasting and relevancy --- src/sat/smt/bv_delay_internalize.cpp | 90 +++++----------------------- src/sat/smt/bv_solver.h | 3 +- src/sat/smt/euf_invariant.cpp | 5 +- src/sat/smt/euf_relevancy.cpp | 2 + 4 files changed, 21 insertions(+), 79 deletions(-) diff --git a/src/sat/smt/bv_delay_internalize.cpp b/src/sat/smt/bv_delay_internalize.cpp index 35b0e5b70..24d1b28b6 100644 --- a/src/sat/smt/bv_delay_internalize.cpp +++ b/src/sat/smt/bv_delay_internalize.cpp @@ -39,8 +39,18 @@ namespace bv { return true; } - bool solver::should_bit_blast(expr* e) { - return bv.get_bv_size(e) <= 12; + bool solver::should_bit_blast(app* e) { + if (bv.get_bv_size(e) <= 12) + return true; + unsigned num_vars = e->get_num_args(); + for (expr* arg : *e) + if (!m.is_value(arg)) + --num_vars; + if (num_vars <= 1) + return true; + if (bv.is_bv_add(e) && num_vars * bv.get_bv_size(e) <= 64) + return true; + return false; } expr_ref solver::eval_args(euf::enode* n, expr_ref_vector& args) { @@ -81,12 +91,6 @@ namespace bv { if (!check_mul_invertibility(e, args, r1)) return false; - // check discrepancies in low-order bits - // Add axioms for multiplication when fixing high-order bits - if (!check_mul_low_bits(e, args, r1, r2)) - return false; - - // Some other possible approaches: // algebraic rules: // x*(y+z), and there are nodes for x*y or x*z -> x*(y+z) = x*y + x*z @@ -230,73 +234,6 @@ namespace bv { return true; } - /** - * Check for discrepancies in low-order bits. - * Add bit-blasting axioms if there are discrepancies within low order bits. - */ - bool solver::check_mul_low_bits(app* n, expr_ref_vector const& arg_values, expr* value1, expr* value2) { - rational v0, v1, two(2); - unsigned sz; - VERIFY(bv.is_numeral(value1, v0, sz)); - VERIFY(bv.is_numeral(value2, v1)); - unsigned num_bits = 10; - if (sz <= num_bits) - return true; - bool diff = false; - for (unsigned i = 0; !diff && i < num_bits; ++i) { - rational b0 = mod(v0, two); - rational b1 = mod(v1, two); - diff = b0 != b1; - div(v0, two, v0); - div(v1, two, v1); - } - if (!diff) - return true; - - auto safe_for_fixing_bits = [&](expr* e) { - euf::enode* n = expr2enode(e); - theory_var v = n->get_th_var(get_id()); - for (unsigned i = num_bits; i < sz; ++i) { - sat::literal lit = m_bits[v][i]; - if (s().value(lit) == l_true && s().lvl(lit) > s().search_lvl()) - return false; - } - return true; - }; - for (expr* arg : *n) - if (!safe_for_fixing_bits(arg)) - return true; - if (!safe_for_fixing_bits(n)) - return true; - - auto value_for_bv = [&](expr* e) { - euf::enode* n = expr2enode(e); - theory_var v = n->get_th_var(get_id()); - rational val(0); - for (unsigned i = num_bits; i < sz; ++i) { - sat::literal lit = m_bits[v][i]; - if (s().value(lit) == l_true && s().lvl(lit) <= s().search_lvl()) - val += power2(i - num_bits); - } - return val; - }; - auto extract_low_bits = [&](expr* e) { - rational val = value_for_bv(e); - expr_ref lo(bv.mk_extract(num_bits - 1, 0, e), m); - expr_ref hi(bv.mk_numeral(val, sz - num_bits), m); - return expr_ref(bv.mk_concat(lo, hi), m); - }; - expr_ref_vector args(m); - for (expr* arg : *n) - args.push_back(extract_low_bits(arg)); - expr_ref lhs(extract_low_bits(n), m); - expr_ref rhs(m.mk_app(n->get_decl(), args), m); - set_delay_internalize(rhs, internalize_mode::no_delay_i); - add_unit(eq_internalize(lhs, rhs)); - TRACE("bv", tout << "low-bits: " << mk_pp(lhs,m) << " " << mk_pp(rhs, m) << "\n";); - std::cout << "low bits\n"; - return false; - } /** * The i'th bit in xs is 1 if the most significant bit of x is i or higher. @@ -430,7 +367,8 @@ namespace bv { case OP_BSREM_I: case OP_BUDIV_I: case OP_BSDIV_I: - if (should_bit_blast(e)) + case OP_BADD: + if (should_bit_blast(to_app(e))) return internalize_mode::no_delay_i; mode = internalize_mode::delay_i; if (!m_delay_internalize.find(e, mode)) diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h index 90f455d3e..b95cb5e73 100644 --- a/src/sat/smt/bv_solver.h +++ b/src/sat/smt/bv_solver.h @@ -265,13 +265,12 @@ namespace bv { obj_map m_delay_internalize; bool m_cheap_axioms{ true }; - bool should_bit_blast(expr * n); + bool should_bit_blast(app * n); bool check_delay_internalized(expr* e); bool check_mul(app* e); bool check_mul_invertibility(app* n, expr_ref_vector const& arg_values, expr* value); bool check_mul_zero(app* n, expr_ref_vector const& arg_values, expr* value1, expr* value2); bool check_mul_one(app* n, expr_ref_vector const& arg_values, expr* value1, expr* value2); - bool check_mul_low_bits(app* n, expr_ref_vector const& arg_values, expr* value1, expr* value2); bool check_umul_no_overflow(app* n, expr_ref_vector const& arg_values, expr* value); bool check_bv_eval(euf::enode* n); bool check_bool_eval(euf::enode* n); diff --git a/src/sat/smt/euf_invariant.cpp b/src/sat/smt/euf_invariant.cpp index 9b5103dfc..ded31db60 100644 --- a/src/sat/smt/euf_invariant.cpp +++ b/src/sat/smt/euf_invariant.cpp @@ -50,7 +50,10 @@ namespace euf { for (enode* n : m_egraph.nodes()) if (m.is_false(n->get_root()->get_expr()) && m.is_eq(n->get_expr()) && n->get_arg(0)->get_root() == n->get_arg(1)->get_root()) { - TRACE("euf", display(tout << n->get_expr_id() << ": " << mk_pp(n->get_expr(), m) << "\n");); + enable_trace("euf"); + TRACE("euf", display(tout << n->get_expr_id() << ": " << mk_pp(n->get_expr(), m) << "\n" + << "#" << n->get_arg(0)->get_expr_id() << " == #" << n->get_arg(1)->get_expr_id() << " r: " << n->get_arg(0)->get_root_id() << "\n"); + ); UNREACHABLE(); } } diff --git a/src/sat/smt/euf_relevancy.cpp b/src/sat/smt/euf_relevancy.cpp index 795c83108..4af05dc97 100644 --- a/src/sat/smt/euf_relevancy.cpp +++ b/src/sat/smt/euf_relevancy.cpp @@ -57,6 +57,8 @@ namespace euf { m_relevant_expr_ids.reset(); bool_vector visited; ptr_vector todo; + if (!relevancy_enabled()) + return true; if (!m_dual_solver) return true; if (!(*m_dual_solver)(s()))