From fb75dac63fa069b56390df615991dd7d595fc980 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 31 May 2021 12:01:23 -0700 Subject: [PATCH] #5223 --- src/ast/rewriter/bit_blaster/bit_blaster.h | 1 + src/sat/sat_solver.cpp | 2 +- src/sat/smt/array_axioms.cpp | 27 +++++++++++++++++----- src/sat/smt/bv_solver.cpp | 1 + src/sat/smt/euf_model.cpp | 15 ++++++------ 5 files changed, 32 insertions(+), 14 deletions(-) diff --git a/src/ast/rewriter/bit_blaster/bit_blaster.h b/src/ast/rewriter/bit_blaster/bit_blaster.h index 8f2e7e50fe6..ca034337f94 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster.h +++ b/src/ast/rewriter/bit_blaster/bit_blaster.h @@ -59,6 +59,7 @@ class bit_blaster : public bit_blaster_tpl { public: bit_blaster(ast_manager & m, bit_blaster_params const & params); bit_blaster_params const & get_params() const { return this->m_params; } + void set_flat(bool f) { m_rw.set_flat(f); } }; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index bbab830679e..9478c6ee9de 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1029,7 +1029,7 @@ namespace sat { return false; } while (m_qhead < m_trail.size()); - if (m_ext && !is_probing()) + if (m_ext && (!is_probing() || at_base_lvl())) m_ext->unit_propagate(); } if (m_inconsistent) diff --git a/src/sat/smt/array_axioms.cpp b/src/sat/smt/array_axioms.cpp index 1db56b3e18f..0954ef0968e 100644 --- a/src/sat/smt/array_axioms.cpp +++ b/src/sat/smt/array_axioms.cpp @@ -174,9 +174,13 @@ namespace array { SASSERT(store->get_num_args() == 1 + select->get_num_args()); ptr_buffer sel1_args, sel2_args; unsigned num_args = select->get_num_args(); + + if (expr2enode(select->get_arg(0))->get_root() == expr2enode(store)->get_root()) + return false; + sel1_args.push_back(store); sel2_args.push_back(store->get_arg(0)); - + bool has_diff = false; for (unsigned i = 1; i < num_args; i++) has_diff |= expr2enode(select->get_arg(i))->get_root() != expr2enode(store->get_arg(i))->get_root(); @@ -191,6 +195,7 @@ namespace array { expr_ref sel1(a.mk_select(sel1_args), m); expr_ref sel2(a.mk_select(sel2_args), m); expr_ref sel_eq_e(m.mk_eq(sel1, sel2), m); + euf::enode* s1 = e_internalize(sel1); euf::enode* s2 = e_internalize(sel2); TRACE("array", @@ -200,9 +205,13 @@ namespace array { if (s1->get_root() == s2->get_root()) return false; - sat::literal sel_eq = mk_literal(sel_eq_e); - if (s().value(sel_eq) == l_true) - return false; + sat::literal sel_eq = sat::null_literal; + auto init_sel_eq = [&]() { + if (sel_eq != sat::null_literal) + return true; + sel_eq = mk_literal(sel_eq_e); + return s().value(sel_eq) != l_true; + }; bool new_prop = false; for (unsigned i = 1; i < num_args; i++) { @@ -213,11 +222,17 @@ namespace array { if (r1 == r2) continue; if (m.are_distinct(r1->get_expr(), r2->get_expr())) { - new_prop = true; - add_clause(sel_eq); + if (init_sel_eq() && add_clause(sel_eq)) + new_prop = true; break; } sat::literal idx_eq = eq_internalize(idx1, idx2); + if (s().value(idx_eq) == l_true) + continue; + if (s().value(idx_eq) == l_undef) + new_prop = true; + if (!init_sel_eq()) + break; if (add_clause(idx_eq, sel_eq)) new_prop = true; } diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp index 2762a1244f5..4df92596efc 100644 --- a/src/sat/smt/bv_solver.cpp +++ b/src/sat/smt/bv_solver.cpp @@ -55,6 +55,7 @@ namespace bv { m_ackerman(*this), m_bb(m, get_config()), m_find(*this) { + m_bb.set_flat(false); } void solver::fixed_var_eh(theory_var v1) { diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp index 7020ed08cb2..3669fb52eed 100644 --- a/src/sat/smt/euf_model.cpp +++ b/src/sat/smt/euf_model.cpp @@ -253,13 +253,14 @@ namespace euf { if (!is_relevant(n)) continue; bool tt = l_true == s().value(n->bool_var()); - if (tt && mdl.is_false(e)) { - IF_VERBOSE(0, verbose_stream() << "Failed to validate " << bpp(n) << " " << mdl(e) << "\n"); - for (auto* arg : euf::enode_args(n)) - IF_VERBOSE(0, verbose_stream() << bpp(arg) << "\n" << mdl(arg->get_expr()) << "\n"); - } - if (!tt && mdl.is_true(e)) - IF_VERBOSE(0, verbose_stream() << "Failed to validate " << bpp(n) << " " << mdl(e) << "\n"); + if (tt && !mdl.is_false(e)) + continue; + if (!tt && !mdl.is_true(e)) + continue; + IF_VERBOSE(0, + verbose_stream() << "Failed to validate " << n->bool_var() << " " << bpp(n) << " " << mdl(e) << "\n"; + for (auto* arg : euf::enode_args(n)) + verbose_stream() << bpp(arg) << "\n" << mdl(arg->get_expr()) << "\n";); } }