From 03f18c148e2b5d62ed486d5c3efd607a57eeeeed Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 16 Mar 2025 21:14:29 -0700 Subject: [PATCH] some more copilot aided updated --- src/tactic/arith/add_bounds_tactic.cpp | 4 +- src/tactic/arith/degree_shift_tactic.cpp | 57 ++++++++++------------- src/tactic/core/blast_term_ite_tactic.cpp | 15 ++---- src/tactic/core/reduce_args_tactic.cpp | 7 ++- src/tactic/core/tseitin_cnf_tactic.cpp | 8 ++-- 5 files changed, 39 insertions(+), 52 deletions(-) diff --git a/src/tactic/arith/add_bounds_tactic.cpp b/src/tactic/arith/add_bounds_tactic.cpp index 75db906a1..78235d647 100644 --- a/src/tactic/arith/add_bounds_tactic.cpp +++ b/src/tactic/arith/add_bounds_tactic.cpp @@ -41,8 +41,8 @@ struct is_unbounded_proc { bool is_unbounded(goal const & g) { ast_manager & m = g.m(); bound_manager bm(m); - for (unsigned i = 0; i < g.size(); ++i) - bm(g.form(i), g.dep(i), g.pr(i)); + for (auto [f, d, p] : g) + bm(f, d, p); is_unbounded_proc proc(bm); return test(g, proc); } diff --git a/src/tactic/arith/degree_shift_tactic.cpp b/src/tactic/arith/degree_shift_tactic.cpp index 26c3f9ef5..d9447d378 100644 --- a/src/tactic/arith/degree_shift_tactic.cpp +++ b/src/tactic/arith/degree_shift_tactic.cpp @@ -161,11 +161,9 @@ class degree_shift_tactic : public tactic { void display_candidates(std::ostream & out) { out << "candidates:\n"; - for (auto const& kv : m_var2degree) { - if (!kv.m_value.is_one()) { - out << "POWER: " << kv.m_value << "\n" << mk_ismt2_pp(kv.m_key, m) << "\n"; - } - } + for (auto const& [k, v] : m_var2degree) + if (!v.is_one()) + out << "POWER: " << v << "\n" << mk_ismt2_pp(k, m) << "\n"; } void collect(goal const & g) { @@ -182,12 +180,11 @@ class degree_shift_tactic : public tactic { void discard_non_candidates() { m_pinned.reset(); ptr_vector to_delete; - for (auto const& kv : m_var2degree) { - if (kv.m_value.is_one()) - to_delete.push_back(kv.m_key); + for (auto const& [k, v] : m_var2degree) + if (v.is_one()) + to_delete.push_back(k); else - m_pinned.push_back(kv.m_key); // make sure it is not deleted during simplifications - } + m_pinned.push_back(k); // make sure it is not deleted during simplifications for (app* a : to_delete) m_var2degree.erase(a); } @@ -199,23 +196,23 @@ class degree_shift_tactic : public tactic { xmc = alloc(generic_model_converter, m, "degree_shift"); mc = xmc; } - for (auto const& kv : m_var2degree) { - SASSERT(kv.m_value.is_int()); - SASSERT(kv.m_value >= rational(2)); - app * fresh = m.mk_fresh_const(nullptr, kv.m_key->get_decl()->get_range()); + for (auto const& [k, v] : m_var2degree) { + SASSERT(v.is_int()); + SASSERT(v >= rational(2)); + app * fresh = m.mk_fresh_const(nullptr, k->get_decl()->get_range()); m_pinned.push_back(fresh); - m_var2var.insert(kv.m_key, fresh); + m_var2var.insert(k, fresh); if (m_produce_models) { xmc->hide(fresh->get_decl()); - xmc->add(kv.m_key->get_decl(), mk_power(fresh, rational(1)/kv.m_value)); + xmc->add(k->get_decl(), mk_power(fresh, rational(1)/v)); } if (m_produce_proofs) { - expr * s = mk_power(kv.m_key, kv.m_value); + expr * s = mk_power(k, v); expr * eq = m.mk_eq(fresh, s); proof * pr1 = m.mk_def_intro(eq); proof * result_pr = m.mk_apply_def(fresh, s, pr1); m_pinned.push_back(result_pr); - m_var2pr.insert(kv.m_key, result_pr); + m_var2pr.insert(k, result_pr); } } } @@ -235,28 +232,24 @@ class degree_shift_tactic : public tactic { // substitute expr_ref new_curr(m); proof_ref new_pr(m); - unsigned size = g->size(); - for (unsigned idx = 0; idx < size; idx++) { + unsigned idx = 0; + for (auto [curr, dep, pr] : *g) { checkpoint(); - expr * curr = g->form(idx); (*m_rw)(curr, new_curr, new_pr); - if (m_produce_proofs) { - proof * pr = g->pr(idx); - new_pr = m.mk_modus_ponens(pr, new_pr); - } - g->update(idx, new_curr, new_pr, g->dep(idx)); + new_pr = m.mk_modus_ponens(pr, new_pr); + g->update(idx++, new_curr, new_pr, dep); } // add >= 0 constraints for variables with even degree - for (auto const& kv : m_var2degree) { - SASSERT(kv.m_value.is_int()); - SASSERT(kv.m_value >= rational(2)); - if (kv.m_value.is_even()) { - app * new_var = m_var2var.find(kv.m_key); + for (auto const& [k,v] : m_var2degree) { + SASSERT(v.is_int()); + SASSERT(v >= rational(2)); + if (v.is_even()) { + app * new_var = m_var2var.find(k); app * new_c = m_autil.mk_ge(new_var, m_autil.mk_numeral(rational(0), false)); proof * new_pr = nullptr; if (m_produce_proofs) { - proof * pr = m_var2pr.find(kv.m_key); + proof * pr = m_var2pr.find(k); new_pr = m.mk_th_lemma(m_autil.get_family_id(), new_c, 1, &pr); } g->assert_expr(new_c, new_pr, nullptr); diff --git a/src/tactic/core/blast_term_ite_tactic.cpp b/src/tactic/core/blast_term_ite_tactic.cpp index b38f08e54..93c69af4a 100644 --- a/src/tactic/core/blast_term_ite_tactic.cpp +++ b/src/tactic/core/blast_term_ite_tactic.cpp @@ -127,26 +127,21 @@ class blast_term_ite_tactic : public tactic { void operator()(goal_ref const & g, goal_ref_buffer & result) { tactic_report report("blast-term-ite", *g); - bool produce_proofs = g->proofs_enabled(); - expr_ref new_curr(m); proof_ref new_pr(m); - unsigned size = g->size(); unsigned num_fresh = 0; - for (unsigned idx = 0; idx < size; idx++) { - expr * curr = g->form(idx); + unsigned idx = 0; + for (auto [curr, dep, pr] : *g) { if (m_rw.m_cfg.m_max_inflation < UINT_MAX) { m_rw.m_cfg.m_init_term_size = get_num_exprs(curr); num_fresh += m_rw.m_cfg.m_num_fresh; m_rw.m_cfg.m_num_fresh = 0; } m_rw(curr, new_curr, new_pr); - if (produce_proofs) { - proof * pr = g->pr(idx); - new_pr = m.mk_modus_ponens(pr, new_pr); - } - g->update(idx, new_curr, new_pr, g->dep(idx)); + new_pr = m.mk_modus_ponens(pr, new_pr); + g->update(idx++, new_curr, new_pr, dep); } + report_tactic_progress(":blast-term-ite-consts", m_rw.m_cfg.m_num_fresh + num_fresh); g->inc_depth(); result.push_back(g.get()); diff --git a/src/tactic/core/reduce_args_tactic.cpp b/src/tactic/core/reduce_args_tactic.cpp index e46c5cb9b..dc3fe1acb 100644 --- a/src/tactic/core/reduce_args_tactic.cpp +++ b/src/tactic/core/reduce_args_tactic.cpp @@ -425,14 +425,13 @@ class reduce_args_tactic : public tactic { reduce_args_ctx ctx(m); reduce_args_rw rw(*this, decl2args, ctx.m_decl2arg2funcs); - unsigned sz = g.size(); - for (unsigned i = 0; i < sz; i++) { + unsigned idx = 0; + for (auto [f, dep, pr] : g) { if (g.inconsistent()) break; - expr * f = g.form(i); expr_ref new_f(m); rw(f, new_f); - g.update(i, new_f); + g.update(idx++, new_f); } report_tactic_progress(":reduced-funcs", decl2args.size()); diff --git a/src/tactic/core/tseitin_cnf_tactic.cpp b/src/tactic/core/tseitin_cnf_tactic.cpp index dce1fe459..e2260dc3c 100644 --- a/src/tactic/core/tseitin_cnf_tactic.cpp +++ b/src/tactic/core/tseitin_cnf_tactic.cpp @@ -852,10 +852,10 @@ class tseitin_cnf_tactic : public tactic { else m_mc = nullptr; - unsigned size = g->size(); - for (unsigned idx = 0; idx < size; idx++) { - process(g->form(idx), g->dep(idx)); - g->update(idx, m.mk_true(), nullptr, nullptr); // to save memory + unsigned idx = 0; + for (auto [f, dep, pr] : *g) { + process(f, dep); + g->update(idx++, m.mk_true(), nullptr, nullptr); } SASSERT(!m_produce_unsat_cores || m_clauses.size() == m_deps.size());