Modernize C++ patterns: range-based for loops and nullptr (#8167)

* Initial plan

* Replace NULL with nullptr in test files

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

* Convert iterator loops to range-based for loops (part 1)

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

* Convert iterator loops to range-based for loops (part 2)

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

* Fix compilation errors in iterator loop conversions

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/muz/base/bind_variables.cpp

@@ -41,8 +41,8 @@ expr_ref bind_variables::operator()(expr* fml, bool is_forall) {
     m_cache.reset();
     m_names.reset();
     m_bound.reset();
-    for (var2bound::iterator it = m_var2bound.begin(); it != m_var2bound.end(); ++it) {
+    for (auto& kv : m_var2bound) {
-        it->m_value = 0;
+        kv.m_value = 0;
     }
     return result;
 }

src/muz/ddnf/ddnf.cpp

@@ -367,9 +367,8 @@ namespace datalog {
         }
 
         void add_table(ddnf_nodes& dst, ddnf_nodes const& src) {
-            ddnf_nodes::iterator it = src.begin(), end = src.end();
+            for (ddnf_node* node : src) {
-            for (; it != end; ++it) {
+                dst.insert(node);
-                dst.insert(*it);
             }
         }        
     };
@@ -428,9 +427,8 @@ namespace datalog {
         u_map<ddnf_mgr*> m_mgrs;
     public:
         ~ddnfs() {
-            u_map<ddnf_mgr*>::iterator it = m_mgrs.begin(), end = m_mgrs.end();
+            for (auto const& kv : m_mgrs) {
-            for (; it != end; ++it) {
+                dealloc(kv.m_value);
-                dealloc(it->m_value);
             }
         }
         
@@ -838,11 +836,10 @@ namespace datalog {
             compile_var(v, w);
             unsigned num_bits = bv.get_bv_size(c);
             ddnf_nodes const& ns = m_ddnfs.lookup(num_bits, *t);
-            ddnf_nodes::iterator it = ns.begin(), end = ns.end();
             expr_ref_vector eqs(m);
             sort* s = w->get_sort();
-            for (; it != end; ++it) {
+            for (ddnf_node* node : ns) {
-                eqs.push_back(m.mk_eq(w, bv.mk_numeral(rational((*it)->get_id()), s)));
+                eqs.push_back(m.mk_eq(w, bv.mk_numeral(rational(node->get_id()), s)));
             }
             switch (eqs.size()) {
             case 0:

src/muz/rel/aig_exporter.cpp

@@ -189,9 +189,9 @@ namespace datalog {
             expr_ref_vector output(m);
             const func_decl_set& preds = m_rules.get_output_predicates();
 
-            for (func_decl_set::iterator I = preds.begin(), E = preds.end(); I != E; ++I) {
+            for (func_decl* pred : preds) {
                 exprs.reset();
-                assert_pred_id(*I, m_ruleid_var_set, exprs);
+                assert_pred_id(pred, m_ruleid_var_set, exprs);
                 output.push_back(m.mk_and(exprs.size(), exprs.data()));
             }
 

src/muz/rel/dl_bound_relation.cpp

@@ -392,14 +392,12 @@ namespace datalog {
         if (t.lt.empty() && t.le.empty()) {
             return;
         }
-        uint_set::iterator it = t.lt.begin(), end = t.lt.end();
         unsigned_vector ltv, lev;
-        for (; it != end; ++it) {
+        for (unsigned idx : t.lt) {
-            ltv.push_back(renaming[*it]);
+            ltv.push_back(renaming[idx]);
         }
-        it = t.le.begin(), end = t.le.end();
+        for (unsigned idx : t.le) {
-        for (; it != end; ++it) {
+            lev.push_back(renaming[idx]);
-            lev.push_back(renaming[*it]);
         }
         TRACE(dl, 
               tout << "project: ";
@@ -525,9 +523,8 @@ namespace datalog {
     }
 
     void bound_relation::normalize(uint_set const& src, uint_set& dst) const {
-        uint_set::iterator it = src.begin(), end = src.end();
+        for (unsigned idx : src) {
-        for (; it != end; ++it) {
+            dst.insert(find(idx));
-            dst.insert(find(*it));
         }
     }
     void bound_relation::normalize(uint_set2 const& src, uint_set2& dst) const {
@@ -551,13 +548,11 @@ namespace datalog {
                 continue;
             }
             uint_set2& src = (*m_elems)[j];
-            uint_set::iterator it = src.lt.begin(), end = src.lt.end();
+            for (unsigned idx : src.lt) {
-            for(; it != end; ++it) {
+                m_todo.push_back(std::make_pair(idx, true));
-                m_todo.push_back(std::make_pair(*it, true));
             }
-            it = src.le.begin(), end = src.le.end();
+            for (unsigned idx : src.le) {
-            for(; it != end; ++it) {
+                m_todo.push_back(std::make_pair(idx, strict));
-                m_todo.push_back(std::make_pair(*it, strict));
             }
             if (strict) {
                 dst.lt.insert(j);
@@ -628,18 +623,16 @@ namespace datalog {
                 s.le.reset();
                 continue;
             }
-            uint_set::iterator it = s.lt.begin(), end = s.lt.end();
+            for (unsigned idx : s.lt) {
-            for(; it != end; ++it) {
+                ext_numeral const& hi = src[idx].inf();
-                ext_numeral const& hi = src[*it].inf();
                 if (hi.is_infinite() || lo.to_rational() >= hi.to_rational()) {
-                    s.lt.remove(*it);
+                    s.lt.remove(idx);
                 }
             }            
-            it = s.le.begin(), end = s.le.end();
+            for (unsigned idx : s.le) {
-            for(; it != end; ++it) {
+                ext_numeral const& hi = src[idx].inf();
-                ext_numeral const& hi = src[*it].inf();
                 if (hi.is_infinite() || lo.to_rational() > hi.to_rational()) {
-                    s.le.remove(*it);
+                    s.le.remove(idx);
                 }
             }            
         }
@@ -662,13 +655,11 @@ namespace datalog {
                 continue;
             }
             uint_set2 const& upper = (*this)[i];
-            uint_set::iterator it = upper.lt.begin(), end = upper.lt.end();
+            for (unsigned idx : upper.lt) {
-            for (; it != end; ++it) {
+                conjs.push_back(arith.mk_lt(m.mk_var(i, sig[i]), m.mk_var(idx, sig[idx])));
-                conjs.push_back(arith.mk_lt(m.mk_var(i, sig[i]), m.mk_var(*it, sig[*it])));
             }
-            it = upper.le.begin(), end = upper.le.end();
+            for (unsigned idx : upper.le) {
-            for (; it != end; ++it) {
+                conjs.push_back(arith.mk_le(m.mk_var(i, sig[i]), m.mk_var(idx, sig[idx])));
-                conjs.push_back(arith.mk_le(m.mk_var(i, sig[i]), m.mk_var(*it, sig[*it])));
             }
         }
         bsimp.mk_and(conjs.size(), conjs.data(), fml);
@@ -676,19 +667,17 @@ namespace datalog {
 
 
     void bound_relation::display_index(unsigned i, uint_set2 const& src, std::ostream & out) const {
-        uint_set::iterator it = src.lt.begin(), end = src.lt.end();
         out << "#" << i;
         if (!src.lt.empty()) {
             out << " < ";
-            for(; it != end; ++it) {
+            for (unsigned idx : src.lt) {
-                out << *it << " ";
+                out << idx << " ";
             }
         }
         if (!src.le.empty()) {
-            it = src.le.begin(), end = src.le.end();
             out << " <= ";
-            for(; it != end; ++it) {
+            for (unsigned idx : src.le) {
-                out << *it << " ";
+                out << idx << " ";
             }
         }
         if (src.lt.empty() && src.le.empty()) {

src/muz/rel/dl_compiler.cpp

@@ -427,9 +427,8 @@ namespace datalog {
             counter_tail.count_vars(r->get_tail(i));
           }
 
-          rule_counter::iterator I = counter_tail.begin(), E = counter_tail.end();
+          for (auto const& kv : counter_tail) {
-          for (; I != E; ++I) {
+            int& n = counter.get(kv.m_key);
-            int& n = counter.get(I->m_key);
             if (n == 0)
               n = -1;
           }
@@ -577,11 +576,8 @@ namespace datalog {
         }
 
         //enforce equality of columns
-        int2ints::iterator vit=var_indexes.begin();
+        for (auto& kv : var_indexes) {
-        int2ints::iterator vend=var_indexes.end();
+            unsigned_vector & indexes = kv.m_value;
-        for(; vit!=vend; ++vit) {
-            int2ints::key_data & k = *vit;
-            unsigned_vector & indexes = k.m_value;
             if(indexes.size()==1) {
                 continue;
             }
@@ -688,13 +684,12 @@ namespace datalog {
             {
                 unsigned_vector var_idx_to_remove;
                 m_free_vars(r->get_head());
-                for (int2ints::iterator I = var_indexes.begin(), E = var_indexes.end();
+                for (auto const& kv : var_indexes) {
-                    I != E; ++I) {
+                    unsigned var_idx = kv.m_key;
-                    unsigned var_idx = I->m_key;
                     if (!m_free_vars.contains(var_idx)) {
-                        unsigned_vector & cols = I->m_value;
+                        unsigned_vector const& cols = kv.m_value;
-                        for (unsigned i = 0; i < cols.size(); ++i) {
+                        for (unsigned col : cols) {
-                            remove_columns.push_back(cols[i]);
+                            remove_columns.push_back(col);
                         }
                         var_idx_to_remove.push_back(var_idx);
                     }
@@ -715,9 +710,8 @@ namespace datalog {
                         }
                     }
 
-                    for (int2ints::iterator I = var_indexes.begin(), E = var_indexes.end();
+                    for (auto& kv : var_indexes) {
-                    I != E; ++I) {
+                        unsigned_vector & cols = kv.m_value;
-                        unsigned_vector & cols = I->m_value;
                         for (unsigned i = 0; i < cols.size(); ++i) {
                             cols[i] -= offsets[cols[i]];
                         }
@@ -895,10 +889,9 @@ namespace datalog {
             }
         }
         // add negative variables that are not in positive
-        u_map<expr*>::iterator it = neg_vars.begin(), end = neg_vars.end();
+        for (auto const& kv : neg_vars) {
-        for (; it != end; ++it) {
+            unsigned v = kv.m_key;
-            unsigned v = it->m_key;
+            expr* e = kv.m_value;
-            expr* e = it->m_value;
             if (!pos_vars.contains(v)) {
                 single_res_expr.push_back(e);
                 make_add_unbound_column(r, v, pred, single_res, e->get_sort(), single_res, dealloc, acc);

src/muz/rel/dl_product_relation.cpp

@@ -137,15 +137,11 @@ namespace datalog {
             std::sort(specs.back().begin(), specs.back().end());
         }
 
-        vector<rel_spec>::iterator sit = specs.begin(), send = specs.end();
-
         res.reset();
         for(;;) {
             family_id next = -1;
 
-            sit = specs.begin();
+            for (rel_spec& s : specs) {
-            for(; sit!=send; ++sit) {
-                rel_spec & s = *sit;
                 if(!s.empty() && s.back()>next) {
                     next = s.back();
                 }
@@ -155,9 +151,7 @@ namespace datalog {
                 break;
             }
             res.push_back(next);
-            sit = specs.begin();
+            for (rel_spec& s : specs) {
-            for(; sit!=send; ++sit) {
-                rel_spec & s = *sit;
                 while (!s.empty() && s.back()==next) {
                     s.pop_back();
                 }

src/muz/rel/dl_relation_manager.cpp

@@ -937,18 +937,11 @@ namespace datalog {
             unsigned t1first_func = t1.get_signature().first_functional();
             unsigned t2first_func = t2.get_signature().first_functional();
 
-            table_base::iterator els1it = t1.begin();
-            table_base::iterator els1end = t1.end();
-            table_base::iterator els2end = t2.end();
-
             table_fact acc;
 
-            for(; els1it!=els1end; ++els1it) {
+            for (const table_base::row_interface& row1 : t1) {
-                const table_base::row_interface & row1 = *els1it;
 
-                table_base::iterator els2it = t2.begin();
+                for (const table_base::row_interface& row2 : t2) {
-                for(; els2it!=els2end; ++els2it) {
-                    const table_base::row_interface & row2 = *els2it;
 
                     bool match=true;
                     for(unsigned i=0; i<m_col_cnt; i++) {
@@ -1491,10 +1484,7 @@ namespace datalog {
 
         bool should_remove(const table_fact & f) const override {
             if(!m_all_neg_bound || m_overlap) {
-                table_base::iterator nit = m_negated_table->begin();
+                for (const table_base::row_interface& nrow : *m_negated_table) {
-                table_base::iterator nend = m_negated_table->end();
-                for(; nit!=nend; ++nit) {
-                    const table_base::row_interface & nrow = *nit;
                     if(bindings_match(nrow, f)) {
                         return true;
                     }
@@ -1656,13 +1646,13 @@ namespace datalog {
             f.resize(m_result_col_cnt);
         }
 
-        void mk_project(table_base::iterator& it)  {
+        void mk_project(const table_base::row_interface& row)  {
             for (unsigned i = 0, j = 0, r_i = 0; i < m_inp_col_cnt; ++i) {
                 if (r_i < m_removed_col_cnt && m_removed_cols[r_i] == i) {
                     ++r_i;
                 }
                 else {
-                    m_row[j] = m_former_row[j] = (*it)[i];
+                    m_row[j] = m_former_row[j] = row[i];
                     ++j;
                 }
             }
@@ -1674,9 +1664,8 @@ namespace datalog {
             SASSERT(plugin.can_handle_signature(res_sign));
             table_base * res = plugin.mk_empty(res_sign);
 
-            table_base::iterator it = t.begin(), end = t.end();
+            for (const table_base::row_interface& row : t) {
-            for (; it != end; ++it) {
+                mk_project(row);
-                mk_project(it);
                 if (!res->suggest_fact(m_former_row)) {
                     (*m_reducer)(m_former_row.data()+m_res_first_functional, m_row.data()+m_res_first_functional);
                     res->ensure_fact(m_former_row);

src/muz/rel/rel_context.cpp

@@ -386,9 +386,7 @@ namespace datalog {
         rule_set::pred_set_vector const & pred_sets = all_rules.get_strats();
         bool non_empty = false;
         for (unsigned i = 1; i < pred_sets.size(); ++i) {
-            func_decl_set::iterator it = pred_sets[i]->begin(), end = pred_sets[i]->end();
+            for (func_decl* pred : *pred_sets[i]) {
-            for (; it != end; ++it) {
-                func_decl* pred = *it;
                 relation_base & rel = get_relation(pred);
                 if (!rel.fast_empty()) {
                     non_empty = true;
@@ -405,9 +403,7 @@ namespace datalog {
             bool change = true;
             while (change) {
                 change = false;
-                func_decl_set::iterator it = pred_sets[i]->begin(), end = pred_sets[i]->end();
+                for (func_decl* pred : *pred_sets[i]) {
-                for (; it != end; ++it) {
-                    func_decl* pred = *it;
                     if (depends_on_negation.contains(pred)) {
                         continue;
                     }
@@ -434,9 +430,7 @@ namespace datalog {
                 }
             }
         }        
-        func_decl_set::iterator it = depends_on_negation.begin(), end = depends_on_negation.end();
+        for (func_decl* pred : depends_on_negation) {
-        for (; it != end; ++it) {
-            func_decl* pred = *it;
             relation_base & rel = get_relation(pred);
             
             if (!rel.empty()) {

src/muz/rel/udoc_relation.cpp

@@ -194,9 +194,8 @@ namespace datalog {
         m_disable_fast_pass(false) {
     }
     udoc_plugin::~udoc_plugin() {
-        u_map<doc_manager*>::iterator it = m_dms.begin(), end = m_dms.end();
+        for (auto const& kv : m_dms) {
-        for (; it != end; ++it) {
+            dealloc(kv.m_value);
-            dealloc(it->m_value);
         }
     }
     udoc_relation& udoc_plugin::get(relation_base& r) {

src/muz/spacer/spacer_farkas_learner.cpp

@@ -177,9 +177,8 @@ void farkas_learner::get_lemmas(proof* root, expr_set const& bs, expr_ref_vector
     bool_rewriter brwr(m);
     func_decl_set Bsymbs;
     collect_pure_proc collect_proc(Bsymbs);
-    expr_set::iterator it = bs.begin(), end = bs.end();
+    for (expr* e : bs) {
-    for (; it != end; ++it) {
+        for_each_expr(collect_proc, e);
-        for_each_expr(collect_proc, *it);
     }
 
     proof_ref pr(root, m);

src/muz/tab/tab_context.cpp

@@ -756,9 +756,7 @@ namespace tb {
         void init(rules const& rs) {
             reset();
             double_vector& scores = m_scores;
-            rules::iterator it = rs.begin(), end = rs.end();
+            for (ref<clause> g : rs) {
-            for (; it != end; ++it) {
-                ref<clause> g = *it;
                 app* p = g->get_head();
                 scores.reset();
                 basic_score_predicate(p, scores);

src/muz/transforms/dl_mk_array_instantiation.cpp

@@ -94,10 +94,10 @@ namespace datalog {
             new_tail.append(instantiate_pred(to_app(preds[i].get())));
         }
         new_tail.append(phi);
-        for(obj_map<expr, var*>::iterator it = done_selects.begin(); it!=done_selects.end(); ++it)  {
+        for (auto const& kv : done_selects)  {
             expr_ref tmp(m);
-            tmp = &it->get_key();
+            tmp = kv.m_key;
-            new_tail.push_back(m.mk_eq(it->get_value(), tmp));
+            new_tail.push_back(m.mk_eq(kv.m_value, tmp));
         }
         proof_ref pr(m);
         src_manager->mk_rule(m.mk_implies(m.mk_and(new_tail.size(), new_tail.data()), new_head), pr, dest, r.name());

src/muz/transforms/dl_mk_karr_invariants.cpp

@@ -189,10 +189,8 @@ namespace datalog {
         if (!m_ctx.karr()) {
             return nullptr;
         }
-        rule_set::iterator it = source.begin(), end = source.end();
+        for (rule* r : source) {
-        for (; it != end; ++it) {
+            if (r->has_negation()) {
-            rule const& r = **it;
-            if (r.has_negation()) {
                 return nullptr;
             }
         }
@@ -225,8 +223,8 @@ namespace datalog {
         rel_context_base& rctx = *m_inner_ctx.get_rel_context();
         ptr_vector<func_decl> heads;
         func_decl_set const& predicates = m_ctx.get_predicates();
-        for (func_decl_set::iterator fit = predicates.begin(); fit != predicates.end(); ++fit) {
+        for (func_decl* pred : predicates) {
-            m_inner_ctx.register_predicate(*fit, false);
+            m_inner_ctx.register_predicate(pred, false);
         }
         m_inner_ctx.ensure_opened();
         m_inner_ctx.replace_rules(src);
@@ -256,9 +254,8 @@ namespace datalog {
 
     rule_set* mk_karr_invariants::update_rules(rule_set const& src) {
         scoped_ptr<rule_set> dst = alloc(rule_set, m_ctx);
-        rule_set::iterator it = src.begin(), end = src.end();
+        for (rule* r : src) {
-        for (; it != end; ++it) {
+            update_body(*dst, *r);
-            update_body(*dst, **it);
         }
         if (m_ctx.get_model_converter()) {
             add_invariant_model_converter* kmc = alloc(add_invariant_model_converter, m);

src/muz/transforms/dl_mk_slice.cpp

@@ -115,16 +115,14 @@ namespace datalog {
             if (!m_sliceform2rule.empty()) {
                 return;
             }
-            obj_map<rule, rule*>::iterator it  = m_rule2slice.begin();
-            obj_map<rule, rule*>::iterator end = m_rule2slice.end();
             expr_ref fml(m);
-            for (; it != end; ++it) {
+            for (auto const& kv : m_rule2slice) {
-                rm.to_formula(*it->m_value, fml);
+                rm.to_formula(*kv.m_value, fml);
                 m_pinned_exprs.push_back(fml);
                 TRACE(dl, 
                       tout << "orig: " << mk_pp(fml, m) << "\n";
-                      it->m_value->display(m_ctx, tout << "new:\n"););                
+                      kv.m_value->display(m_ctx, tout << "new:\n"););                
-                m_sliceform2rule.insert(fml, it->m_key);                
+                m_sliceform2rule.insert(fml, kv.m_key);                
             }
         }
 
@@ -714,14 +712,13 @@ namespace datalog {
     }
         
     void mk_slice::declare_predicates(rule_set const& src, rule_set& dst) {
-        obj_map<func_decl, bit_vector>::iterator it = m_sliceable.begin(), end = m_sliceable.end();
         ptr_vector<sort> domain;
         bool has_output = false;
         func_decl* f;
-        for (; it != end; ++it) {
+        for (auto const& kv : m_sliceable) {
             domain.reset();
-            func_decl* p = it->m_key;
+            func_decl* p = kv.m_key;
-            bit_vector const& bv = it->m_value;
+            bit_vector const& bv = kv.m_value;
             for (unsigned i = 0; i < bv.size(); ++i) {
                 if (!bv.get(i)) {
                     domain.push_back(p->get_domain(i));
@@ -848,9 +845,8 @@ namespace datalog {
         update_rules(src, *result);
         TRACE(dl, result->display(tout););
         if (m_mc) {
-            obj_map<func_decl, bit_vector>::iterator it = m_sliceable.begin(), end = m_sliceable.end();
+            for (auto const& kv : m_sliceable) {
-            for (; it != end; ++it) {
+                m_mc->add_sliceable(kv.m_key, kv.m_value);
-                m_mc->add_sliceable(it->m_key, it->m_value);
             }
         }
         m_ctx.add_proof_converter(spc.get());

src/test/no_overflow.cpp

@@ -23,7 +23,7 @@ Revision History:
 
 #define TEST(TEST_NAME, TEST_OUTCOME, NEG_TEST_OUTCOME) \
     do { \
-        if (TEST_NAME != NULL) \
+        if (TEST_NAME != nullptr) \
         { \
             Z3_solver_push(ctx, s);            \
             Z3_solver_assert(ctx, s, TEST_NAME);     \

src/test/sat_local_search.cpp

@@ -11,7 +11,6 @@ static bool build_instance(char const * filename, sat::solver& s, sat::local_sea
     // for temporary storage
 
     std::ifstream infile(filename);
-    //if (infile == NULL) //linux
     if (!infile) {
         std::cout << "File not found " << filename << "\n";
         return false;