some more copilot aided updated

Author: NikolajBjorner

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);
 }

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<app> 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);

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());

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());

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());