Migrate iterator-based for loops to range-based for loops (#8231)

* Initial plan

* Migrate iterator-based for loops to range-based for loops in 11 files

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix compilation error in aig_exporter.cpp - use correct iterator API

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Revert changes to z3++.h as requested

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

src/ast/rewriter/bv_bounds.cpp

@@ -238,9 +238,8 @@ bv_bounds::conv_res bv_bounds::convert(expr * e, vector<ninterval>& nis, bool ne
 }
 
 void bv_bounds::reset() {
-    intervals_map::iterator it = m_negative_intervals.begin();
+    for (auto& [key, value] : m_negative_intervals)
-    const intervals_map::iterator end = m_negative_intervals.end();
+        dealloc(value);
-    for (; it != end; ++it) dealloc(it->m_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) {
+    for (auto& [v, val] : m_singletons) {
-        app * const v = i->m_key;
-        const rational val = i->m_value;
         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<app>   seen;
     obj_hashtable<app>::entry *dummy;
 
-    for (bound_map::iterator i = m_unsigned_lowers.begin(); i != m_unsigned_lowers.end(); ++i) {
+    for (auto& [v, _] : m_unsigned_lowers) {
-        app * const v = i->m_key;
         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) {
+    for (auto& [v, _] : m_unsigned_uppers) {
-        app * const v = i->m_key;
         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) {
+    for (auto& [v, _] : m_negative_intervals) {
-        app * const v = i->m_key;
         if (!seen.insert_if_not_there_core(v, dummy)) continue;
         if (!is_sat(v)) return false;
     }

src/ast/sls/bvsls_opt_engine.h

@@ -57,10 +57,8 @@ protected:
     mpz top_score() {
         mpz res(0);
         obj_hashtable<expr> const & top_exprs = m_obj_tracker.get_top_exprs();
-        for (obj_hashtable<expr>::iterator it = top_exprs.begin();
+        for (auto* e : top_exprs)
-             it != top_exprs.end();
+            m_mpz_manager.add(res, m_obj_tracker.get_value(e), res);
-             ++it)
-             m_mpz_manager.add(res, m_obj_tracker.get_value(*it), res);
         return res;
     }
 

src/ast/sls/sls_bv_tracker.h

@@ -648,11 +648,10 @@ public:
     void randomize(ptr_vector<expr> 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) {
+        for (auto& [fd, ep] : m_entry_points) {
-            func_decl * fd = it->m_key;
             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<expr> 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) {
+        for (auto& [fd, ep] : m_entry_points) {
-            set_value(it->m_value, m_zero);
+            set_value(ep, m_zero);
         }
     }              
 

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<func_decl*> predicates;
-        for (rule_set::decl2rules::iterator I = m_rules.begin_grouped_rules(),
+        for (auto it = m_rules.begin_grouped_rules(), end = m_rules.end_grouped_rules(); it != end; ++it)
-            E = m_rules.end_grouped_rules(); I != E; ++I) {
+            predicates.insert(it->m_key);
-            predicates.insert(I->m_key);
-        }
 
-        for (fact_vector::const_iterator I = facts->begin(), E = facts->end(); I != E; ++I) {
+        for (auto& [pred, _] : *facts)
-            predicates.insert(I->first);
+            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(),
+        for (auto it = m_rules.begin_grouped_rules(), end = m_rules.end_grouped_rules(); it != end; ++it) {
-            E = m_rules.end_grouped_rules(); I != E; ++I) {
+            for (rule* r : *it->get_value()) {
-            for (rule_vector::iterator II = I->get_value()->begin(),
-                EE = I->get_value()->end(); II != EE; ++II) {
-                rule *r = *II;
                 unsigned numqs = r->get_positive_tail_size();
                 if (numqs > 1) {
                     throw default_exception("non-linear clauses not supported");

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 (auto& [key, value] : m_sel_terms)
-        for (sel_map::iterator it = begin; it != end; ++it) {
+            dealloc(value);
-            dealloc(it->m_value);
-        }
         m_sel_terms.reset();
     }
 };

src/muz/transforms/dl_mk_rule_inliner.cpp

@@ -580,20 +580,19 @@ namespace datalog {
         scoped_ptr<rule_set> res = alloc(rule_set, m_context);
         bool done_something = false;
 
-        rule_set::iterator rend = rules->end();
+        for (rule* r : *rules) {
-        for (rule_set::iterator rit = rules->begin(); rit!=rend; ++rit) {
+            rule_ref rl(r, m_rm);
-            rule_ref r(*rit, m_rm);
 
             rule_ref replacement(m_rm);
-            while (r && do_eager_inlining(r, *rules, replacement)) {
+            while (rl && do_eager_inlining(rl, *rules, replacement)) {
-                r = 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();

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* r : rules) {
-            for(rule_set::iterator rit = rules.begin(); rit!=rend; ++rit) {
-                rule * r = *rit;
                 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* pred : candidate_preds) {
-        for(func_decl_set::iterator it = candidate_preds.begin(); it!=end; ++it) {
-            func_decl * pred = *it;
             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* r : rules) {
-        for(rule_set::iterator rit = rules.begin(); rit!=rend; ++rit) {
-            rule * r = *rit;
             func_decl * pred = r->get_decl();
 
             if(r->get_tail_size()!=0) { continue; }

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<app, numeral>::iterator it = m_unsigned_lowers.begin(); it != m_unsigned_lowers.end(); ++it)
+                    for (auto& [key, value] : m_unsigned_lowers)
-                        tout << mk_ismt2_pp(it->m_key, m) << " >= " << it->m_value.to_string() << std::endl;
+                        tout << mk_ismt2_pp(key, m) << " >= " << value.to_string() << std::endl;
                     tout << "m_unsigned_uppers: " << std::endl;
-                    for (obj_map<app, numeral>::iterator it = m_unsigned_uppers.begin(); it != m_unsigned_uppers.end(); ++it)
+                    for (auto& [key, value] : m_unsigned_uppers)
-                        tout << mk_ismt2_pp(it->m_key, m) << " <= " << it->m_value.to_string() << std::endl;
+                        tout << mk_ismt2_pp(key, m) << " <= " << value.to_string() << std::endl;
                     );
 
                 obj_map<app, numeral>::iterator it  = m_unsigned_uppers.begin();