From 735888145e6c350cf9a089e7d0cdd924671a7853 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 26 Apr 2020 20:10:58 -0700 Subject: [PATCH] fix #4112 Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 1 + src/ast/rewriter/rewriter_def.h | 1 - src/ast/shared_occs.cpp | 2 ++ src/tactic/core/symmetry_reduce_tactic.cpp | 1 - src/tactic/ufbv/ufbv_rewriter.cpp | 34 ++++++++++++---------- src/tactic/ufbv/ufbv_rewriter.h | 4 +-- 6 files changed, 23 insertions(+), 20 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 56b5d76a8..48d922f29 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1986,6 +1986,7 @@ void ast_manager::delete_node(ast * n) { } } + sort * ast_manager::mk_sort(family_id fid, decl_kind k, unsigned num_parameters, parameter const * parameters) { decl_plugin * p = get_plugin(fid); if (p) diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h index 6e5d73b58..fea4aa0d1 100644 --- a/src/ast/rewriter/rewriter_def.h +++ b/src/ast/rewriter/rewriter_def.h @@ -134,7 +134,6 @@ bool rewriter_tpl::process_const(app * t0) { template template bool rewriter_tpl::visit(expr * t, unsigned max_depth) { - // retry: TRACE("rewriter_visit", tout << "visiting\n" << mk_ismt2_pp(t, m()) << "\n";); expr * new_t = nullptr; proof * new_t_pr = nullptr; diff --git a/src/ast/shared_occs.cpp b/src/ast/shared_occs.cpp index 9528892e7..249459a95 100644 --- a/src/ast/shared_occs.cpp +++ b/src/ast/shared_occs.cpp @@ -93,7 +93,9 @@ void shared_occs::operator()(expr * t, shared_occs_mark & visited) { expr * curr = fr.first; switch (curr->get_kind()) { case AST_APP: { + unsigned num_args = to_app(curr)->get_num_args(); + while (fr.second < num_args) { expr * arg = to_app(curr)->get_arg(fr.second); fr.second++; diff --git a/src/tactic/core/symmetry_reduce_tactic.cpp b/src/tactic/core/symmetry_reduce_tactic.cpp index adb669a75..3dbdfde91 100644 --- a/src/tactic/core/symmetry_reduce_tactic.cpp +++ b/src/tactic/core/symmetry_reduce_tactic.cpp @@ -515,7 +515,6 @@ private: public: num_occurrences(app_map& occs): m_occs(occs) {} void operator()(app* n) { - app_map::obj_map_entry* e; m_occs.insert_if_not_there(n, 0); unsigned sz = n->get_num_args(); for (unsigned i = 0; i < sz; ++i) { diff --git a/src/tactic/ufbv/ufbv_rewriter.cpp b/src/tactic/ufbv/ufbv_rewriter.cpp index 1db0881f4..47a530bd8 100644 --- a/src/tactic/ufbv/ufbv_rewriter.cpp +++ b/src/tactic/ufbv/ufbv_rewriter.cpp @@ -31,6 +31,7 @@ ufbv_rewriter::ufbv_rewriter(ast_manager & m): m_match_subst(m), m_bsimp(m), m_todo(m), + m_new_args(m), m_rewrite_todo(m), m_rewrite_cache(m), m_new_exprs(m) { @@ -221,11 +222,12 @@ void ufbv_rewriter::remove_fwd_idx(func_decl * f, quantifier * demodulator) { fwd_idx_map::iterator it = m_fwd_idx.find_iterator(f); if (it != m_fwd_idx.end()) { demodulator2lhs_rhs::iterator fit = m_demodulator2lhs_rhs.find_iterator(demodulator); - m.dec_ref(fit->m_value.first); - m.dec_ref(fit->m_value.second); - m.dec_ref(demodulator); + expr_pair p = fit->m_value; m_demodulator2lhs_rhs.erase(demodulator); it->m_value->erase(demodulator); + m.dec_ref(p.first); + m.dec_ref(p.second); + m.dec_ref(demodulator); } else { SASSERT(m_demodulator2lhs_rhs.contains(demodulator)); } @@ -262,11 +264,11 @@ void ufbv_rewriter::show_fwd_idx(std::ostream & out) { } } -bool ufbv_rewriter::rewrite1(func_decl * f, ptr_vector & m_new_args, expr_ref & np) { +bool ufbv_rewriter::rewrite1(func_decl * f, expr_ref_vector & m_new_args, expr_ref & np) { fwd_idx_map::iterator it = m_fwd_idx.find_iterator(f); if (it != m_fwd_idx.end()) { TRACE("demodulator_bug", tout << "trying to rewrite: " << f->get_name() << " args:\n"; - for (unsigned i = 0; i < m_new_args.size(); i++) { tout << mk_pp(m_new_args[i], m) << "\n"; }); + tout << m_new_args << "\n";); for (quantifier* d : *it->m_value) { SASSERT(m_demodulator2lhs_rhs.contains(d)); @@ -305,12 +307,12 @@ bool ufbv_rewriter::rewrite_visit_children(app * a) { if (ebp.second) v = ebp.first; } - for (unsigned i = sz; i > 0; i--) { - if (m_rewrite_todo[i - 1] == v) { + for (unsigned i = sz; i-- > 0;) { + if (m_rewrite_todo[i] == v) { recursive = true; TRACE("demodulator", tout << "Detected demodulator cycle: " << mk_pp(a, m) << " --> " << mk_pp(v, m) << std::endl;); - m_rewrite_cache.insert(e, expr_bool_pair(v, true)); + rewrite_cache(e, v, true); break; } } @@ -346,7 +348,7 @@ expr * ufbv_rewriter::rewrite(expr * n) { ); expr * e = m_rewrite_todo.back(); - expr * actual = e; + expr_ref actual(e, m); if (m_rewrite_cache.contains(e)) { const expr_bool_pair &ebp = m_rewrite_cache.get(e); @@ -370,9 +372,8 @@ expr * ufbv_rewriter::rewrite(expr * n) { func_decl * f = a->get_decl(); m_new_args.reset(); unsigned num_args = a->get_num_args(); - bool all_untouched=true; - for (unsigned i = 0 ; i < num_args ; i++ ) { - expr * o_child = a->get_arg(i); + bool all_untouched = true; + for (expr* o_child : *a) { expr * n_child; SASSERT(m_rewrite_cache.contains(o_child) && m_rewrite_cache.get(o_child).second); expr_bool_pair const & ebp = m_rewrite_cache.get(o_child); @@ -386,17 +387,17 @@ expr * ufbv_rewriter::rewrite(expr * n) { rewrite_cache(e, np, false); // No pop. } else { - if(all_untouched) { + if (all_untouched) { rewrite_cache(e, actual, true); } else { expr_ref na(m); if (f->get_family_id() != m.get_basic_family_id()) - na = m.mk_app(f, m_new_args.size(), m_new_args.c_ptr()); + na = m.mk_app(f, m_new_args); else m_bsimp.mk_app(f, m_new_args.size(), m_new_args.c_ptr(), na); TRACE("demodulator_bug", tout << "e:\n" << mk_pp(e, m) << "\nnew_args: \n"; - for (unsigned i = 0; i < m_new_args.size(); i++) { tout << mk_pp(m_new_args[i], m) << "\n"; } + tout << m_new_args << "\n"; tout << "=====>\n"; tout << "na:\n " << mk_pp(na, m) << "\n";); rewrite_cache(e, na, true); @@ -577,7 +578,7 @@ void ufbv_rewriter::reschedule_demodulators(func_decl * f, expr * lhs) { expr_ref l(m); for (auto s : *it->m_value) - all_occurrences.insert(s); + all_occurrences.insert(s); // Run over all f-demodulators for (expr* occ : all_occurrences) { @@ -853,6 +854,7 @@ bool ufbv_rewriter::match_subst::match_args(app * lhs, expr * const * args) { bool ufbv_rewriter::match_subst::operator()(app * lhs, expr * rhs, expr * const * args, expr_ref & new_rhs) { + if (match_args(lhs, args)) { if (m_all_args_eq) { // quick success... diff --git a/src/tactic/ufbv/ufbv_rewriter.h b/src/tactic/ufbv/ufbv_rewriter.h index 4cf3439c6..cbc903b80 100644 --- a/src/tactic/ufbv/ufbv_rewriter.h +++ b/src/tactic/ufbv/ufbv_rewriter.h @@ -165,7 +165,7 @@ class ufbv_rewriter { demodulator2lhs_rhs m_demodulator2lhs_rhs; expr_ref_buffer m_todo; obj_hashtable m_processed; - ptr_vector m_new_args; + expr_ref_vector m_new_args; expr_ref_buffer m_rewrite_todo; rewrite_cache_map m_rewrite_cache; @@ -179,7 +179,7 @@ class ufbv_rewriter { bool can_rewrite(expr * n, expr * lhs); expr * rewrite(expr * n); - bool rewrite1(func_decl * f, ptr_vector & m_new_args, expr_ref & np); + bool rewrite1(func_decl * f, expr_ref_vector & m_new_args, expr_ref & np); bool rewrite_visit_children(app * a); void rewrite_cache(expr * e, expr * new_e, bool done); void reschedule_processed(func_decl * f);