From 896a1b204833395fbdca71f48ffd146ecf5bb19d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Apr 2020 15:04:05 -0700 Subject: [PATCH] fix #3679 Signed-off-by: Nikolaj Bjorner --- src/ackermannization/ackr_info.h | 2 +- src/ast/rewriter/arith_rewriter.cpp | 2 +- src/ast/rewriter/expr_replacer.cpp | 8 +-- src/ast/rewriter/expr_replacer.h | 2 +- src/ast/rewriter/rewriter_def.h | 70 +++++++++++----------- src/muz/fp/horn_tactic.cpp | 2 +- src/muz/spacer/spacer_context.cpp | 4 +- src/muz/spacer/spacer_qe_project.cpp | 2 +- src/qe/nlarith_util.cpp | 4 +- src/qe/qe.cpp | 6 +- src/smt/qi_queue.cpp | 1 + src/smt/theory_str_mc.cpp | 2 +- src/tactic/arith/nla2bv_tactic.cpp | 2 +- src/tactic/arith/purify_arith_tactic.cpp | 2 +- src/tactic/bv/bv_size_reduction_tactic.cpp | 2 +- src/tactic/core/solve_eqs_tactic.cpp | 2 +- src/tactic/core/symmetry_reduce_tactic.cpp | 2 +- 17 files changed, 59 insertions(+), 56 deletions(-) diff --git a/src/ackermannization/ackr_info.h b/src/ackermannization/ackr_info.h index 5180b68d9..500db7d78 100644 --- a/src/ackermannization/ackr_info.h +++ b/src/ackermannization/ackr_info.h @@ -36,7 +36,7 @@ class ackr_info { public: ackr_info(ast_manager& m) : m(m), - m_er(mk_default_expr_replacer(m)), + m_er(mk_default_expr_replacer(m, false)), m_subst(m), m_ref_count(0), m_sealed(false) diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index 0126c1e16..c6ec6e2bc 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -89,7 +89,7 @@ br_status arith_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c CTRACE("arith_rewriter", st != BR_FAILED, tout << st << ": " << mk_pp(f, m()); for (unsigned i = 0; i < num_args; ++i) tout << mk_pp(args[i], m()) << " "; tout << "\n==>\n" << mk_pp(result.get(), m()) << "\n"; - tout << "args: " << to_app(result)->get_num_args() << "\n"; + if (is_app(result)) tout << "args: " << to_app(result)->get_num_args() << "\n"; ); return st; } diff --git a/src/ast/rewriter/expr_replacer.cpp b/src/ast/rewriter/expr_replacer.cpp index d26a10b19..e822c1775 100644 --- a/src/ast/rewriter/expr_replacer.cpp +++ b/src/ast/rewriter/expr_replacer.cpp @@ -83,9 +83,9 @@ class default_expr_replacer : public expr_replacer { default_expr_replacer_cfg m_cfg; rewriter_tpl m_replacer; public: - default_expr_replacer(ast_manager & m): + default_expr_replacer(ast_manager & m, bool proofs_enabled): m_cfg(m), - m_replacer(m, m.proofs_enabled(), m_cfg) { + m_replacer(m, m.proofs_enabled() && proofs_enabled, m_cfg) { } ast_manager & m() const override { return m_replacer.m(); } @@ -115,8 +115,8 @@ public: } }; -expr_replacer * mk_default_expr_replacer(ast_manager & m) { - return alloc(default_expr_replacer, m); +expr_replacer * mk_default_expr_replacer(ast_manager & m, bool proofs_allowed) { + return alloc(default_expr_replacer, m, proofs_allowed); } /** diff --git a/src/ast/rewriter/expr_replacer.h b/src/ast/rewriter/expr_replacer.h index 811cd1f23..cc148fca0 100644 --- a/src/ast/rewriter/expr_replacer.h +++ b/src/ast/rewriter/expr_replacer.h @@ -49,7 +49,7 @@ public: /** \brief Create a vanilla replacer. It just applies the substitution. */ -expr_replacer * mk_default_expr_replacer(ast_manager & m); +expr_replacer * mk_default_expr_replacer(ast_manager & m, bool proofs_allowed); /** \brief Apply substitution and simplify. diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h index bb46e1d39..f32b07a9c 100644 --- a/src/ast/rewriter/rewriter_def.h +++ b/src/ast/rewriter/rewriter_def.h @@ -35,47 +35,49 @@ void rewriter_tpl::process_var(var * v) { m_r = nullptr; return; } - if (!ProofGen) { - // bindings are only used when Proof Generation is not enabled. - unsigned idx = v->get_idx(); + unsigned idx = v->get_idx(); + if (ProofGen) { + result_pr_stack().push_back(nullptr); // implicit reflexivity - if (idx < m_bindings.size()) { - unsigned index = m_bindings.size() - idx - 1; - expr * r = m_bindings[index]; - if (r != nullptr) { - CTRACE("rewriter", v->get_sort() != m().get_sort(r), - tout << expr_ref(v, m()) << ":" << sort_ref(v->get_sort(), m()) << " != " << expr_ref(r, m()) << ":" << sort_ref(m().get_sort(r), m()); - tout << "index " << index << " bindings " << m_bindings.size() << "\n"; - display_bindings(tout);); - SASSERT(v->get_sort() == m().get_sort(r)); - if (!is_ground(r) && m_shifts[index] != m_bindings.size()) { - - unsigned shift_amount = m_bindings.size() - m_shifts[index]; - expr* c = get_cached(r, shift_amount); - if (c) { - result_stack().push_back(c); - set_new_child_flag(v); - return; - } - expr_ref tmp(m()); - m_shifter(r, shift_amount, tmp); - result_stack().push_back(tmp); - TRACE("rewriter", tout << "shift: " << shift_amount << " idx: " << idx << " --> " << tmp << "\n"; - display_bindings(tout);); - cache_shifted_result(r, shift_amount, tmp); - } - else { - result_stack().push_back(r); - TRACE("rewriter", tout << idx << " " << mk_ismt2_pp(r, m()) << "\n";); - } + SASSERT( + true || // disabled for now + idx >= m_bindings.size() || + !m_bindings[m_bindings.size() - idx - 1] || + v == m_bindings[m_bindings.size() - idx - 1]); + } + unsigned index = 0; + expr * r; + if (!ProofGen && idx < m_bindings.size() && + (index = m_bindings.size() - idx - 1, r = m_bindings[index])) { + CTRACE("rewriter", v->get_sort() != m().get_sort(r), + tout << expr_ref(v, m()) << ":" << sort_ref(v->get_sort(), m()) << " != " << expr_ref(r, m()) << ":" << sort_ref(m().get_sort(r), m()); + tout << "index " << index << " bindings " << m_bindings.size() << "\n"; + display_bindings(tout);); + SASSERT(v->get_sort() == m().get_sort(r)); + if (!is_ground(r) && m_shifts[index] != m_bindings.size()) { + + unsigned shift_amount = m_bindings.size() - m_shifts[index]; + expr* c = get_cached(r, shift_amount); + if (c) { + result_stack().push_back(c); set_new_child_flag(v); return; } + expr_ref tmp(m()); + m_shifter(r, shift_amount, tmp); + result_stack().push_back(tmp); + TRACE("rewriter", tout << "shift: " << shift_amount << " idx: " << idx << " --> " << tmp << "\n"; + display_bindings(tout);); + cache_shifted_result(r, shift_amount, tmp); } + else { + result_stack().push_back(r); + TRACE("rewriter", tout << idx << " " << mk_ismt2_pp(r, m()) << "\n";); + } + set_new_child_flag(v); + return; } result_stack().push_back(v); - if (ProofGen) - result_pr_stack().push_back(nullptr); // implicit reflexivity } template diff --git a/src/muz/fp/horn_tactic.cpp b/src/muz/fp/horn_tactic.cpp index 8fee59990..7cc0fe58c 100644 --- a/src/muz/fp/horn_tactic.cpp +++ b/src/muz/fp/horn_tactic.cpp @@ -334,7 +334,7 @@ class horn_tactic : public tactic { expr_substitution sub(m); sub.insert(q, m.mk_false()); - scoped_ptr rep = mk_default_expr_replacer(m); + scoped_ptr rep = mk_default_expr_replacer(m, false); rep->set_substitution(&sub); g->inc_depth(); g->reset(); diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index b21379597..c77ae86f0 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -1124,7 +1124,7 @@ expr_ref pred_transformer::get_cover_delta(func_decl* p_orig, int level) v = m.mk_var(i, sig(i)->get_range()); sub.insert(c, v); } - scoped_ptr rep = mk_default_expr_replacer(m); + scoped_ptr rep = mk_default_expr_replacer(m, false); rep->set_substitution(&sub); (*rep)(result); @@ -1216,7 +1216,7 @@ void pred_transformer::add_cover(unsigned level, expr* property, bool bg) v = m.mk_var(i, sig(i)->get_range()); sub.insert(v, c, pr); } - scoped_ptr rep = mk_default_expr_replacer(m); + scoped_ptr rep = mk_default_expr_replacer(m, false); rep->set_substitution(&sub); (*rep)(result); TRACE("spacer", tout << "cover:\n" << mk_pp(result, m) << "\n";); diff --git a/src/muz/spacer/spacer_qe_project.cpp b/src/muz/spacer/spacer_qe_project.cpp index c4f7d2376..b6e0933aa 100644 --- a/src/muz/spacer/spacer_qe_project.cpp +++ b/src/muz/spacer/spacer_qe_project.cpp @@ -1163,7 +1163,7 @@ namespace spacer_qe { tout << "substituting " << mk_pp (m_var->x (), m) << " by " << mk_pp (x_term, m) << "\n"; ); } - scoped_ptr rep = mk_default_expr_replacer (m); + scoped_ptr rep = mk_default_expr_replacer (m, false); rep->set_substitution (&sub); (*rep)(fml); } diff --git a/src/qe/nlarith_util.cpp b/src/qe/nlarith_util.cpp index c2d95a1ee..4a04ec4bb 100644 --- a/src/qe/nlarith_util.cpp +++ b/src/qe/nlarith_util.cpp @@ -546,7 +546,7 @@ namespace nlarith { sqrt_form e0(*this, mk_uminus(c), 0, z(), b); // a_i = 0 /\ b_i != 0 /\ phi[e_i/x] TRACE("nlarith", display(tout << "a_i != 0 & b_i != 0 & hi[e_i / x]", p);tout<<"\n";); - scoped_ptr rp = mk_default_expr_replacer(m()); + scoped_ptr rp = mk_default_expr_replacer(m(), false); expr_substitution sub(m()); sub.insert(a, z()); rp->set_substitution(&sub); @@ -610,7 +610,7 @@ namespace nlarith { sqrt_form e0(*this, mk_uminus(c), 0, z(), b); es.reset(); subst.reset(); - scoped_ptr rp = mk_default_expr_replacer(m()); + scoped_ptr rp = mk_default_expr_replacer(m(), false); expr_substitution sub(m()); sub.insert(a, z()); rp->set_substitution(&sub); diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp index 320d1c474..8cee2919e 100644 --- a/src/qe/qe.cpp +++ b/src/qe/qe.cpp @@ -351,7 +351,7 @@ namespace qe { scoped_ptr m_replace; public: lift_ite(ast_manager& m, i_expr_pred& is_relevant) : - m(m), m_is_relevant(is_relevant), m_rewriter(m), m_replace(mk_default_expr_replacer(m)) {} + m(m), m_is_relevant(is_relevant), m_rewriter(m), m_replace(mk_default_expr_replacer(m, false)) {} bool operator()(expr* fml, expr_ref& result) { if (m.is_ite(fml)) { @@ -1465,7 +1465,7 @@ namespace qe { if (!is_sat) { fml = m.mk_false(); if (m_fml.get() != m_subfml.get()) { - scoped_ptr rp = mk_default_expr_replacer(m); + scoped_ptr rp = mk_default_expr_replacer(m, false); rp->apply_substitution(to_app(m_subfml.get()), fml, m_fml); fml = m_fml; } @@ -1497,7 +1497,7 @@ namespace qe { if (!m_free_vars.empty() || m_solver.inconsistent()) { if (m_fml.get() != m_subfml.get()) { - scoped_ptr rp = mk_default_expr_replacer(m); + scoped_ptr rp = mk_default_expr_replacer(m, false); rp->apply_substitution(to_app(m_subfml.get()), fml, m_fml); fml = m_fml; } diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp index d5807d4d1..9611d8485 100644 --- a/src/smt/qi_queue.cpp +++ b/src/smt/qi_queue.cpp @@ -226,6 +226,7 @@ namespace smt { return; } + TRACE("qi_queue", tout << "simplified instance:\n" << s_instance << "\n";); quantifier_stat * stat = m_qm.get_stat(q); stat->inc_num_instances(); if (stat->get_num_instances() % m_params.m_qi_profile_freq == 0) { diff --git a/src/smt/theory_str_mc.cpp b/src/smt/theory_str_mc.cpp index 9c19182c5..3a51a2061 100644 --- a/src/smt/theory_str_mc.cpp +++ b/src/smt/theory_str_mc.cpp @@ -1136,7 +1136,7 @@ namespace smt { } // TODO insert length values into substitution table as well? if (m_params.m_FixedLengthRefinement) { - scoped_ptr replacer = mk_default_expr_replacer(m); + scoped_ptr replacer = mk_default_expr_replacer(m, false); replacer->set_substitution(&subst); th_rewriter rw(m); if (!abstracted_boolean_formulas.empty()) { diff --git a/src/tactic/arith/nla2bv_tactic.cpp b/src/tactic/arith/nla2bv_tactic.cpp index 49bde4e57..43def0741 100644 --- a/src/tactic/arith/nla2bv_tactic.cpp +++ b/src/tactic/arith/nla2bv_tactic.cpp @@ -184,7 +184,7 @@ class nla2bv_tactic : public tactic { // substitute variables by bit-vectors void substitute_vars(goal & g) { - scoped_ptr er = mk_default_expr_replacer(m_manager); + scoped_ptr er = mk_default_expr_replacer(m_manager, false); er->set_substitution(&m_subst); expr_ref r(m_manager); for (unsigned i = 0; i < g.size(); ++i) { diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index 783202566..a4760c0ac 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -753,7 +753,7 @@ struct purify_arith_proc { unsigned idx = num_vars - i - 1; subst.insert(c, m().mk_var(idx, s)); } - scoped_ptr replacer = mk_default_expr_replacer(m()); + scoped_ptr replacer = mk_default_expr_replacer(m(), false); replacer->set_substitution(&subst); (*replacer)(new_body, new_body); new_body = m().mk_exists(num_vars, sorts.c_ptr(), names.c_ptr(), new_body, q->get_weight()); diff --git a/src/tactic/bv/bv_size_reduction_tactic.cpp b/src/tactic/bv/bv_size_reduction_tactic.cpp index 0aff332a7..52f9f450e 100644 --- a/src/tactic/bv/bv_size_reduction_tactic.cpp +++ b/src/tactic/bv/bv_size_reduction_tactic.cpp @@ -47,7 +47,7 @@ public: bv_size_reduction_tactic(ast_manager & m) : m(m), m_util(m), - m_replacer(mk_default_expr_replacer(m)) { + m_replacer(mk_default_expr_replacer(m, false)) { } tactic * translate(ast_manager & m) override { diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp index 74038951f..112fb97fb 100644 --- a/src/tactic/core/solve_eqs_tactic.cpp +++ b/src/tactic/core/solve_eqs_tactic.cpp @@ -67,7 +67,7 @@ class solve_eqs_tactic : public tactic { m_marked_candidates(m) { updt_params(p); if (m_r == nullptr) - m_r = mk_default_expr_replacer(m); + m_r = mk_default_expr_replacer(m, true); } ~imp() { diff --git a/src/tactic/core/symmetry_reduce_tactic.cpp b/src/tactic/core/symmetry_reduce_tactic.cpp index 33d6e976f..9e2a0224f 100644 --- a/src/tactic/core/symmetry_reduce_tactic.cpp +++ b/src/tactic/core/symmetry_reduce_tactic.cpp @@ -114,7 +114,7 @@ class symmetry_reduce_tactic::imp { ast_manager& m() const { return m_manager; } public: imp(ast_manager& m) : m_manager(m), m_rewriter(m) { - m_replace = mk_default_expr_replacer(m); + m_replace = mk_default_expr_replacer(m, false); } ~imp() {}