From bef113254ca2a847d25012bd2f37161d58c75759 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sat, 17 Jan 2026 20:16:25 +0000 Subject: [PATCH] Migrate iterator-based for loops to range-based for loops in 11 files Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/api/c++/z3++.h | 4 ++-- src/ast/rewriter/bv_bounds.cpp | 18 ++++++------------ src/ast/sls/bvsls_opt_engine.h | 6 ++---- src/ast/sls/sls_bv_tracker.h | 9 ++++----- src/muz/rel/aig_exporter.cpp | 18 ++++++------------ src/muz/spacer/spacer_qe_project.cpp | 6 ++---- src/muz/transforms/dl_mk_rule_inliner.cpp | 13 ++++++------- .../transforms/dl_mk_subsumption_checker.cpp | 12 +++--------- src/tactic/bv/bv_size_reduction_tactic.cpp | 8 ++++---- 9 files changed, 35 insertions(+), 59 deletions(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index b4c8ddbf8..20ea4bda6 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -3431,7 +3431,7 @@ namespace z3 { Z3_optimize_inc_ref(c, m_opt); add(expr_vector(c, src.assertions())); expr_vector v(c, src.objectives()); - for (expr_vector::iterator it = v.begin(); it != v.end(); ++it) minimize(*it); + for (auto& e : v) minimize(e); } optimize& operator=(optimize const& o) { Z3_optimize_inc_ref(o.ctx(), o.m_opt); @@ -3447,7 +3447,7 @@ namespace z3 { Z3_optimize_assert(ctx(), m_opt, e); } void add(expr_vector const& es) { - for (expr_vector::iterator it = es.begin(); it != es.end(); ++it) add(*it); + for (auto& e : es) add(e); } void add(expr const& e, expr const& t) { assert(e.is_bool()); diff --git a/src/ast/rewriter/bv_bounds.cpp b/src/ast/rewriter/bv_bounds.cpp index 7123666e7..75b039063 100644 --- a/src/ast/rewriter/bv_bounds.cpp +++ b/src/ast/rewriter/bv_bounds.cpp @@ -238,9 +238,8 @@ bv_bounds::conv_res bv_bounds::convert(expr * e, vector& nis, bool ne } void bv_bounds::reset() { - intervals_map::iterator it = m_negative_intervals.begin(); - const intervals_map::iterator end = m_negative_intervals.end(); - for (; it != end; ++it) dealloc(it->m_value); + for (auto& [key, value] : m_negative_intervals) + dealloc(value); } br_status bv_bounds::rewrite(unsigned limit, func_decl * f, unsigned num, expr * const * args, expr_ref& result) { @@ -312,9 +311,7 @@ br_status bv_bounds::rewrite(unsigned limit, func_decl * f, unsigned num, expr * if (nargs.size() == num && !has_singls) return BR_FAILED; expr_ref eq(m_m); - for (bv_bounds::bound_map::iterator i = m_singletons.begin(); i != m_singletons.end(); ++i) { - app * const v = i->m_key; - const rational val = i->m_value; + for (auto& [v, val] : m_singletons) { eq = m_m.mk_eq(v, bvu().mk_numeral(val, v->get_decl()->get_range())); if (negated) eq = m_m.mk_not(eq); nargs.push_back(eq); @@ -568,20 +565,17 @@ bool bv_bounds::is_sat() { obj_hashtable seen; obj_hashtable::entry *dummy; - for (bound_map::iterator i = m_unsigned_lowers.begin(); i != m_unsigned_lowers.end(); ++i) { - app * const v = i->m_key; + for (auto& [v, _] : m_unsigned_lowers) { if (!seen.insert_if_not_there_core(v, dummy)) continue; if (!is_sat(v)) return false; } - for (bound_map::iterator i = m_unsigned_uppers.begin(); i != m_unsigned_uppers.end(); ++i) { - app * const v = i->m_key; + for (auto& [v, _] : m_unsigned_uppers) { if (!seen.insert_if_not_there_core(v, dummy)) continue; if (!is_sat(v)) return false; } - for (intervals_map::iterator i = m_negative_intervals.begin(); i != m_negative_intervals.end(); ++i) { - app * const v = i->m_key; + for (auto& [v, _] : m_negative_intervals) { if (!seen.insert_if_not_there_core(v, dummy)) continue; if (!is_sat(v)) return false; } diff --git a/src/ast/sls/bvsls_opt_engine.h b/src/ast/sls/bvsls_opt_engine.h index a55a33565..49a6487a2 100644 --- a/src/ast/sls/bvsls_opt_engine.h +++ b/src/ast/sls/bvsls_opt_engine.h @@ -57,10 +57,8 @@ protected: mpz top_score() { mpz res(0); obj_hashtable const & top_exprs = m_obj_tracker.get_top_exprs(); - for (obj_hashtable::iterator it = top_exprs.begin(); - it != top_exprs.end(); - ++it) - m_mpz_manager.add(res, m_obj_tracker.get_value(*it), res); + for (auto* e : top_exprs) + m_mpz_manager.add(res, m_obj_tracker.get_value(e), res); return res; } diff --git a/src/ast/sls/sls_bv_tracker.h b/src/ast/sls/sls_bv_tracker.h index aa0c7304c..cf76e4f9a 100644 --- a/src/ast/sls/sls_bv_tracker.h +++ b/src/ast/sls/sls_bv_tracker.h @@ -648,11 +648,10 @@ public: void randomize(ptr_vector const & as) { TRACE(sls_verbose, tout << "Abandoned model:" << std::endl; show_model(tout); ); - for (entry_point_type::iterator it = m_entry_points.begin(); it != m_entry_points.end(); ++it) { - func_decl * fd = it->m_key; + for (auto& [fd, ep] : m_entry_points) { sort * s = fd->get_range(); mpz temp = get_random(s); - set_value(it->m_value, temp); + set_value(ep, temp); m_mpz_manager.del(temp); } @@ -662,8 +661,8 @@ public: void reset(ptr_vector const & as) { TRACE(sls_verbose, tout << "Abandoned model:" << std::endl; show_model(tout); ); - for (entry_point_type::iterator it = m_entry_points.begin(); it != m_entry_points.end(); ++it) { - set_value(it->m_value, m_zero); + for (auto& [fd, ep] : m_entry_points) { + set_value(ep, m_zero); } } diff --git a/src/muz/rel/aig_exporter.cpp b/src/muz/rel/aig_exporter.cpp index e35e60569..9b9355cd5 100644 --- a/src/muz/rel/aig_exporter.cpp +++ b/src/muz/rel/aig_exporter.cpp @@ -23,14 +23,11 @@ namespace datalog { m_latch_vars(m), m_latch_varsp(m), m_ruleid_var_set(m), m_ruleid_varp_set(m) { std::set predicates; - for (rule_set::decl2rules::iterator I = m_rules.begin_grouped_rules(), - E = m_rules.end_grouped_rules(); I != E; ++I) { - predicates.insert(I->m_key); - } + for (auto& [pred, _] : m_rules.get_grouped_rules()) + predicates.insert(pred); - for (fact_vector::const_iterator I = facts->begin(), E = facts->end(); I != E; ++I) { - predicates.insert(I->first); - } + for (auto& [pred, _] : *facts) + predicates.insert(pred); // reserve pred id = 0 for initialization purposes unsigned num_preds = (unsigned)predicates.size() + 1; @@ -101,11 +98,8 @@ namespace datalog { expr_ref_vector exprs(m); substitution subst(m); - for (rule_set::decl2rules::iterator I = m_rules.begin_grouped_rules(), - E = m_rules.end_grouped_rules(); I != E; ++I) { - for (rule_vector::iterator II = I->get_value()->begin(), - EE = I->get_value()->end(); II != EE; ++II) { - rule *r = *II; + for (auto& [pred, rules] : m_rules.get_grouped_rules()) { + for (rule* r : *rules) { unsigned numqs = r->get_positive_tail_size(); if (numqs > 1) { throw default_exception("non-linear clauses not supported"); diff --git a/src/muz/spacer/spacer_qe_project.cpp b/src/muz/spacer/spacer_qe_project.cpp index cc04fefe5..f32018c01 100644 --- a/src/muz/spacer/spacer_qe_project.cpp +++ b/src/muz/spacer/spacer_qe_project.cpp @@ -2139,10 +2139,8 @@ class array_project_selects_util { } // dealloc - sel_map::iterator begin = m_sel_terms.begin(), end = m_sel_terms.end(); - for (sel_map::iterator it = begin; it != end; ++it) { - dealloc(it->m_value); - } + for (auto& [key, value] : m_sel_terms) + dealloc(value); m_sel_terms.reset(); } }; diff --git a/src/muz/transforms/dl_mk_rule_inliner.cpp b/src/muz/transforms/dl_mk_rule_inliner.cpp index c50e6f8d7..340b0ac56 100644 --- a/src/muz/transforms/dl_mk_rule_inliner.cpp +++ b/src/muz/transforms/dl_mk_rule_inliner.cpp @@ -580,20 +580,19 @@ namespace datalog { scoped_ptr res = alloc(rule_set, m_context); bool done_something = false; - rule_set::iterator rend = rules->end(); - for (rule_set::iterator rit = rules->begin(); rit!=rend; ++rit) { - rule_ref r(*rit, m_rm); + for (rule* r : *rules) { + rule_ref rl(r, m_rm); rule_ref replacement(m_rm); - while (r && do_eager_inlining(r, *rules, replacement)) { - r = replacement; + while (rl && do_eager_inlining(rl, *rules, replacement)) { + rl = replacement; done_something = true; } - if (!r) { + if (!rl) { continue; } - res->add_rule(r); + res->add_rule(rl); } if (done_something) { rules = res.detach(); diff --git a/src/muz/transforms/dl_mk_subsumption_checker.cpp b/src/muz/transforms/dl_mk_subsumption_checker.cpp index 135969426..c71fddf9e 100644 --- a/src/muz/transforms/dl_mk_subsumption_checker.cpp +++ b/src/muz/transforms/dl_mk_subsumption_checker.cpp @@ -100,9 +100,7 @@ namespace datalog { //(discovering a total relation might reveal other total relations) do { new_discovered = false; - rule_set::iterator rend = rules.end(); - for(rule_set::iterator rit = rules.begin(); rit!=rend; ++rit) { - rule * r = *rit; + for (rule* r : rules) { func_decl * head_pred = r->get_decl(); if(is_total_rule(r) && !m_total_relations.contains(head_pred)) { on_discovered_total_relation(head_pred, r); @@ -261,9 +259,7 @@ namespace datalog { func_decl_set const& candidate_preds = m_context.get_predicates(); - func_decl_set::iterator end = candidate_preds.end(); - for(func_decl_set::iterator it = candidate_preds.begin(); it!=end; ++it) { - func_decl * pred = *it; + for (func_decl* pred : candidate_preds) { unsigned rel_sz; if (m_total_relations.contains(pred)) { continue; } // already total @@ -306,9 +302,7 @@ namespace datalog { void mk_subsumption_checker::collect_ground_unconditional_rule_heads(const rule_set & rules) { - rule_set::iterator rend = rules.end(); - for(rule_set::iterator rit = rules.begin(); rit!=rend; ++rit) { - rule * r = *rit; + for (rule* r : rules) { func_decl * pred = r->get_decl(); if(r->get_tail_size()!=0) { continue; } diff --git a/src/tactic/bv/bv_size_reduction_tactic.cpp b/src/tactic/bv/bv_size_reduction_tactic.cpp index 850d1c8dd..64417f235 100644 --- a/src/tactic/bv/bv_size_reduction_tactic.cpp +++ b/src/tactic/bv/bv_size_reduction_tactic.cpp @@ -327,11 +327,11 @@ public: if (!(m_unsigned_lowers.empty() && m_unsigned_uppers.empty())) { TRACE(bv_size_reduction, tout << "m_unsigned_lowers: " << std::endl; - for (obj_map::iterator it = m_unsigned_lowers.begin(); it != m_unsigned_lowers.end(); ++it) - tout << mk_ismt2_pp(it->m_key, m) << " >= " << it->m_value.to_string() << std::endl; + for (auto& [key, value] : m_unsigned_lowers) + tout << mk_ismt2_pp(key, m) << " >= " << value.to_string() << std::endl; tout << "m_unsigned_uppers: " << std::endl; - for (obj_map::iterator it = m_unsigned_uppers.begin(); it != m_unsigned_uppers.end(); ++it) - tout << mk_ismt2_pp(it->m_key, m) << " <= " << it->m_value.to_string() << std::endl; + for (auto& [key, value] : m_unsigned_uppers) + tout << mk_ismt2_pp(key, m) << " <= " << value.to_string() << std::endl; ); obj_map::iterator it = m_unsigned_uppers.begin();