From a78f8992258ec01a34ae186363d3f82c0c437d57 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 3 Nov 2019 10:28:58 +0100 Subject: [PATCH] expand deep stores by lambdas to avoid expanding select/store axioms Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/array_rewriter.cpp | 61 ++++++++++++++++ src/ast/rewriter/array_rewriter.h | 4 + src/ast/rewriter/array_rewriter_params.pyg | 1 + src/smt/asserted_formulas.cpp | 1 + src/tactic/fd_solver/smtfd_solver.cpp | 85 +++++++++++++--------- 5 files changed, 116 insertions(+), 36 deletions(-) diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp index 7e94acefa..0b101ef6d 100644 --- a/src/ast/rewriter/array_rewriter.cpp +++ b/src/ast/rewriter/array_rewriter.cpp @@ -28,6 +28,7 @@ void array_rewriter::updt_params(params_ref const & _p) { m_sort_store = p.sort_store(); m_expand_select_store = p.expand_select_store(); m_expand_store_eq = p.expand_store_eq(); + m_expand_nested_stores = p.expand_nested_stores(); m_expand_select_ite = false; } @@ -630,6 +631,49 @@ bool array_rewriter::add_store(expr_ref_vector& args, unsigned num_idxs, expr* e return true; } +bool array_rewriter::is_expandable_store(expr* s) { + unsigned count = s->get_ref_count(); + unsigned depth = 0; + while (m_util.is_store(s)) { + s = to_app(s)->get_arg(0); + count += s->get_ref_count(); + depth++; + } + return (depth >= 3 && count <= depth*2); +} + +expr_ref array_rewriter::expand_store(expr* s) { + ptr_vector stores; + expr_ref result(m()); + while (m_util.is_store(s)) { + stores.push_back(to_app(s)); + s = to_app(s)->get_arg(0); + } + stores.reverse(); + expr_ref_vector args(m()), eqs(m()); + ptr_vector sorts; + svector names; + sort* srt = m().get_sort(s); + args.push_back(s); + for (unsigned i = get_array_arity(srt); i-- > 0; ) { + args.push_back(m().mk_var(i, get_array_domain(srt, i))); + sorts.push_back(get_array_domain(srt, i)); + names.push_back(symbol(i)); + } + names.reverse(); + sorts.reverse(); + result = m_util.mk_select(args); + for (app* st : stores) { + eqs.reset(); + for (unsigned i = 1; i < args.size(); ++i) { + eqs.push_back(m().mk_eq(args.get(i), st->get_arg(i))); + } + result = m().mk_ite(mk_and(eqs), st->get_arg(args.size()), result); + } + result = m().mk_lambda(sorts.size(), sorts.c_ptr(), names.c_ptr(), result); + return result; +} + br_status array_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { TRACE("array_rewriter", tout << mk_pp(lhs, m()) << " " << mk_pp(rhs, m()) << "\n";); expr* v = nullptr; @@ -642,6 +686,22 @@ br_status array_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) result = m().update_quantifier(lam, quantifier_kind::forall_k, e); return BR_REWRITE2; } + expr_ref lh1(m()), rh1(m()); + if (m_expand_nested_stores) { + if (is_expandable_store(lhs)) { + lh1 = expand_store(lhs); + } + if (is_expandable_store(rhs)) { + rh1 = expand_store(rhs); + } + if (lh1 || rh1) { + if (!lh1) lh1 = lhs; + if (!rh1) rh1 = rhs; + result = m().mk_eq(lh1, rh1); + return BR_REWRITE_FULL; + } + } + if (!m_expand_store_eq) { return BR_FAILED; } @@ -666,6 +726,7 @@ br_status array_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) } } #endif + expr* lhs1 = lhs; while (m_util.is_store(lhs1)) { lhs1 = to_app(lhs1)->get_arg(0); diff --git a/src/ast/rewriter/array_rewriter.h b/src/ast/rewriter/array_rewriter.h index 23cbbacde..b15917d64 100644 --- a/src/ast/rewriter/array_rewriter.h +++ b/src/ast/rewriter/array_rewriter.h @@ -33,6 +33,7 @@ class array_rewriter { bool m_expand_select_store; bool m_expand_store_eq; bool m_expand_select_ite; + bool m_expand_nested_stores; template lbool compare_args(unsigned num_args, expr * const * args1, expr * const * args2); void mk_eq(expr* e, expr* lhs, expr* rhs, expr_ref_vector& fmls); @@ -41,6 +42,9 @@ class array_rewriter { bool add_store(expr_ref_vector& args, unsigned num_idxs, expr* e, expr* store_val, vector& stores); + bool is_expandable_store(expr* s); + expr_ref expand_store(expr* s); + public: array_rewriter(ast_manager & m, params_ref const & p = params_ref()): m_util(m) { diff --git a/src/ast/rewriter/array_rewriter_params.pyg b/src/ast/rewriter/array_rewriter_params.pyg index 3b4af7fb7..cb9120206 100644 --- a/src/ast/rewriter/array_rewriter_params.pyg +++ b/src/ast/rewriter/array_rewriter_params.pyg @@ -2,5 +2,6 @@ def_module_params(module_name='rewriter', class_name='array_rewriter_params', export=True, params=(("expand_select_store", BOOL, False, "replace a (select (store ...) ...) term by an if-then-else term"), + ("expand_nested_stores", BOOL, False, "replace nested stores by a lambda expression"), ("expand_store_eq", BOOL, False, "reduce (store ...) = (store ...) with a common base into selects"), ("sort_store", BOOL, False, "sort nested stores when the indices are known to be different"))) diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 73f7ffe72..61aa48d9c 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -133,6 +133,7 @@ void asserted_formulas::set_eliminate_and(bool flag) { m_params.set_bool("eq2ineq", m_smt_params.m_arith_eq2ineq); m_params.set_bool("gcd_rounding", true); m_params.set_bool("expand_select_store", true); + m_params.set_bool("expand_nested_stores", true); m_params.set_bool("bv_sort_ac", true); m_params.set_bool("som", true); m_rewriter.updt_params(m_params); diff --git a/src/tactic/fd_solver/smtfd_solver.cpp b/src/tactic/fd_solver/smtfd_solver.cpp index 0cb427485..ecd6aae44 100644 --- a/src/tactic/fd_solver/smtfd_solver.cpp +++ b/src/tactic/fd_solver/smtfd_solver.cpp @@ -163,7 +163,7 @@ namespace smtfd { expr* try_rep(expr* e) { return m_rep.get(e->get_id(), nullptr); } expr* fresh_var(expr* t) { - symbol name = is_app(t) ? to_app(t)->get_name() : symbol("X"); + symbol name = is_app(t) ? to_app(t)->get_name() : (is_quantifier(t) ? symbol("Q") : symbol("X")); if (m.is_bool(t)) { return m.mk_fresh_const(name, m.mk_bool_sort()); } @@ -1012,7 +1012,6 @@ namespace smtfd { continue; } if (!tT.find(fA, fT) || (value_of(fA) != value_of(fT) && !eq(m_vargs, fA))) { - TRACE("smtfd", tout << "found: " << tT.find(fA, fT) << "\n";); add_select_store_axiom(t, fA); ++r; } @@ -1229,6 +1228,7 @@ namespace smtfd { m_autil.is_select(t) || m_autil.is_map(t) || m_autil.is_ext(t) || + is_lambda(t) || m_autil.is_const(t); } @@ -1352,9 +1352,10 @@ namespace smtfd { if (!m_model->eval_expr(q->get_expr(), tmp, true)) { return l_undef; } - if (m.is_true(tmp)) { - return l_false; - } + TRACE("smtfd", + tout << mk_pp(q, m) << "\n"; + tout << "eval: " << tmp << "\n"; + tout << *m_model << "\n";); m_solver->push(); expr_ref_vector vars(m), vals(m); @@ -1369,6 +1370,7 @@ namespace smtfd { } var_subst subst(m); expr_ref body = subst(tmp, vars.size(), vars.c_ptr()); + if (is_forall(q)) { body = m.mk_not(body); } @@ -1376,6 +1378,7 @@ namespace smtfd { m_solver->assert_expr(body); lbool r = m_solver->check_sat(0, nullptr); model_ref mdl; + TRACE("smtfd", tout << "check: " << r << "\n";); if (r == l_true) { expr_ref qq(q->get_expr(), m); @@ -1406,6 +1409,7 @@ namespace smtfd { if (r == l_true) { body = subst(q->get_expr(), vals.size(), vals.c_ptr()); m_context.rewrite(body); + TRACE("smtfd", tout << vals << "\n" << body << "\n";); if (is_forall(q)) { body = m.mk_implies(q, body); } @@ -1520,8 +1524,7 @@ namespace smtfd { unsigned_vector m_assertions_lim; unsigned m_assertions_qhead; expr_ref_vector m_toggles; - expr_ref m_toggle; - expr_ref m_not_toggle; + unsigned_vector m_toggles_lim; model_ref m_model; std::string m_reason_unknown; unsigned m_max_lemmas; @@ -1536,20 +1539,30 @@ namespace smtfd { m_fd_core_solver->updt_params(p); } + expr* add_toggle(expr* toggle) { + m_toggles.push_back(abs(toggle)); + return toggle; + } + + bool is_toggle(expr* e) { + return m_toggles.contains(e); + } + void flush_assertions() { SASSERT(m_assertions_qhead <= m_assertions.size()); unsigned sz = m_assertions.size() - m_assertions_qhead; if (sz > 0) { - m_assertions.push_back(m_toggle); + m_assertions.push_back(m_toggles.back()); expr_ref fml(m.mk_and(sz + 1, m_assertions.c_ptr() + m_assertions_qhead), m); - m_assertions.pop_back(); - m_toggle = m.mk_fresh_const("toggle", m.mk_bool_sort()); - m_not_toggle = m.mk_not(m_toggle); - m_not_toggle = abs(m_not_toggle); + m_assertions.pop_back(); + expr* toggle = add_toggle(m.mk_fresh_const("toggle", m.mk_bool_sort())); m_assertions_qhead = m_assertions.size(); - fml = m.mk_iff(m_toggle, fml); - TRACE("smtfd_verbose", tout << fml << "\n";); - assert_fd(fml); + TRACE("smtfd", tout << "flush: " << m_assertions_qhead << " " << mk_bounded_pp(fml, m, 3) << "\n";); + fml = abs(fml); + m_fd_sat_solver->assert_expr(fml); + fml = m.mk_not(m.mk_and(toggle, fml)); + m_fd_core_solver->assert_expr(fml); + flush_atom_defs(); } } @@ -1563,8 +1576,6 @@ namespace smtfd { display(tout << asms << "\n");); TRACE("smtfd_verbose", m_fd_sat_solver->display(tout);); - SASSERT(asms.contains(m_toggle)); - m_fd_sat_solver->assert_expr(m_toggle); lbool r = m_fd_sat_solver->check_sat(asms); update_reason_unknown(r, m_fd_sat_solver); set_delay_simplify(); @@ -1578,15 +1589,14 @@ namespace smtfd { m_model->set_model_completion(true); init_model_assumptions(num_assumptions, assumptions, asms); TRACE("smtfd", display(tout << asms << "\n");); - SASSERT(asms.contains(m_not_toggle)); lbool r = m_fd_core_solver->check_sat(asms); update_reason_unknown(r, m_fd_core_solver); if (r == l_false) { m_fd_core_solver->get_unsat_core(core); TRACE("smtfd", display(tout << core << "\n");); - core.erase(m_not_toggle.get()); - SASSERT(asms.contains(m_not_toggle)); - SASSERT(!asms.contains(m_toggle)); + SASSERT(asms.contains(m_toggles.back())); + SASSERT(core.contains(m_toggles.back())); + core.erase(m_toggles.back()); rep(core); } return r; @@ -1643,7 +1653,6 @@ namespace smtfd { lbool is_decided_sat(expr_ref_vector const& core) { bool has_q = false; - bool has_non_covered = false; lbool is_decided = l_true; m_context.reset(m_model); for (expr* t : subterms(core)) { @@ -1656,7 +1665,7 @@ namespace smtfd { } m_context.populate_model(m_model, core); - TRACE("smtfd", tout << "has quantifier: " << has_q << " has non-converted: " << has_non_covered << "\n";); + TRACE("smtfd", tout << "has quantifier: " << has_q << "\n" << core << "\n";); if (!has_q) { return is_decided; } @@ -1679,7 +1688,6 @@ namespace smtfd { void init_assumptions(unsigned sz, expr* const* user_asms, expr_ref_vector& asms) { asms.reset(); - asms.push_back(m_toggle); for (unsigned i = 0; i < sz; ++i) { asms.push_back(abs_assumption(user_asms[i])); } @@ -1688,19 +1696,22 @@ namespace smtfd { void init_model_assumptions(unsigned sz, expr* const* user_asms, expr_ref_vector& asms) { asms.reset(); - asms.push_back(m_not_toggle); + asms.push_back(m_toggles.back()); for (unsigned i = 0; i < sz; ++i) { asms.push_back(abs(user_asms[i])); } for (expr* a : m_abs.atoms()) { - if (m_model->is_true(a)) { + if (is_toggle(a)) { + + } + else if (m_model->is_true(a)) { asms.push_back(a); } else { asms.push_back(m.mk_not(a)); } } - asms.erase(m_toggle.get()); + std::cout << "asms: " << asms << "\n"; } void checkpoint() { @@ -1749,12 +1760,11 @@ namespace smtfd { m_pb(m_context), m_assertions(m), m_assertions_qhead(0), - m_toggles(m), - m_toggle(m.mk_true(), m), - m_not_toggle(m.mk_false(), m), + m_toggles(m), m_max_conflicts(50) { updt_params(p); + add_toggle(m.mk_true()); } ~solver() override {} @@ -1774,12 +1784,12 @@ namespace smtfd { void push_core() override { init(); flush_assertions(); - m_toggles.push_back(m_toggle); m_abs.push(); m_fd_sat_solver->push(); m_fd_core_solver->push(); m_smt_solver->push(); m_assertions_lim.push_back(m_assertions.size()); + m_toggles_lim.push_back(m_toggles.size()); } void pop_core(unsigned n) override { @@ -1787,9 +1797,9 @@ namespace smtfd { m_fd_core_solver->pop(n); m_smt_solver->pop(n); m_abs.pop(n); - m_toggle = m_toggles.get(m_toggles.size() - n); - m_not_toggle = m.mk_not(m_toggle); - m_toggles.shrink(m_toggles.size() - n); + unsigned sz = m_toggles_lim[m_toggles_lim.size() - n]; + m_toggles.shrink(sz); + m_toggles_lim.shrink(m_toggles_lim.size() - n); m_assertions.shrink(m_assertions_lim[m_assertions_lim.size() - n]); m_assertions_lim.shrink(m_assertions_lim.size() - n); m_assertions_qhead = m_assertions.size(); @@ -1876,11 +1886,14 @@ namespace smtfd { flush_assertions(); lbool r = l_undef; expr_ref_vector core(m); + unsigned nt = m_toggles.size(); while (true) { IF_VERBOSE(1, verbose_stream() << "(smtfd-check-sat " << m_stats.m_num_rounds << " " << m_stats.m_num_lemmas << " " << m_stats.m_num_mbqi << ")\n"); m_stats.m_num_rounds++; checkpoint(); + m_toggles.shrink(nt); + std::cout << "toggles: " << m_toggles << "\n"; // phase 1: check sat of abs r = check_abs(num_assumptions, assumptions); @@ -1905,6 +1918,7 @@ namespace smtfd { break; case l_false: break; + // disable for now r = check_smt(core); switch (r) { case l_true: @@ -2002,8 +2016,7 @@ namespace smtfd { st.update("smtfd-num-mbqi", m_stats.m_num_mbqi); } void get_unsat_core(expr_ref_vector & r) override { - m_fd_sat_solver->get_unsat_core(r); - r.erase(m_toggle.get()); + m_fd_sat_solver->get_unsat_core(r); rep(r); } void get_model_core(model_ref & mdl) override {