use iterators on goal and other refactoring

Author: NikolajBjorner

src/tactic/bv/elim_small_bv_tactic.cpp

@@ -256,22 +256,19 @@ class elim_small_bv_tactic : public tactic {
     void operator()(goal_ref const & g,
                     goal_ref_buffer & result) override {
         tactic_report report("elim-small-bv", *g);
-        bool produce_proofs = g->proofs_enabled();
         fail_if_proof_generation("elim-small-bv", g);
         fail_if_unsat_core_generation("elim-small-bv", g);
         m_rw.cfg().m_produce_models = g->models_enabled();
 
         expr_ref   new_curr(m);
         proof_ref  new_pr(m);
-        unsigned   size = g->size();
-        for (unsigned idx = 0; !g->inconsistent() && idx < size; idx++) {
-            expr * curr = g->form(idx);
+        unsigned idx = 0;
+        for (auto [curr, dep, pr] : *g) {
+            if (g->inconsistent())
+                break;
             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);
         }
         g->add(m_rw.m_cfg.m_mc.get());
 

src/tactic/core/cofactor_term_ite_tactic.cpp

@@ -29,14 +29,13 @@ class cofactor_term_ite_tactic : public tactic {
 
     void process(goal & g) {
         ast_manager & m = g.m();
-        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);
             m_elim_ite(f, new_f);
-            g.update(i, new_f, nullptr, g.dep(i));
+            g.update(idx++, new_f, nullptr, dep);            
         }
     }
 

src/tactic/core/ctx_simplify_tactic.cpp

@@ -569,16 +569,15 @@ struct ctx_simplify_tactic::imp {
         m_occs.reset();
         m_occs(g);
         m_num_steps = 0;
-        unsigned sz = g.size();
         tactic_report report("ctx-simplify", g);
         if (g.proofs_enabled()) {
             expr_ref r(m);
-            for (unsigned i = 0; !g.inconsistent() && i < sz; ++i) {
-                expr * t = g.form(i);
+            unsigned idx = 0;
+            for (auto [t, dep, pr] : g) {
                 process(t, r);
                 proof_ref new_pr(m.mk_rewrite(t, r), m);
-                new_pr = m.mk_modus_ponens(g.pr(i), new_pr);
-                g.update(i, r, new_pr, g.dep(i));
+                new_pr = m.mk_modus_ponens(pr, new_pr);
+                g.update(idx++, r, new_pr, dep);
             }
         }
         else {

src/tactic/core/der_tactic.cpp

@@ -34,21 +34,16 @@ class der_tactic : public tactic {
         }
 
         void operator()(goal & g) {
-            bool proofs_enabled = g.proofs_enabled();
             tactic_report report("der", g);
             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) {
                 if (g.inconsistent())
                     break;
-                expr * curr = g.form(idx);
                 m_r(curr, new_curr, new_pr);
-                if (proofs_enabled) {
-                    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);
             }
             g.elim_redundancies();
         }

src/tactic/goal.cpp

@@ -486,22 +486,21 @@ void goal::shrink(unsigned j) {
 /**
    \brief Eliminate true formulas.
 */
-void goal::elim_true() {
-    unsigned sz = size();
-    unsigned j = 0;
-    for (unsigned i = 0; i < sz; i++) {
-        expr * f = form(i);
-        if (m().is_true(f))
-            continue;
-        if (i == j) {
-            j++;
+void goal::elim_true() {    
+    unsigned i = 0, j = 0;
+    for (auto [f, dep, pr] : *this) {
+        if (m().is_true(f)) {
+            ++i;
             continue;
         }
-        m().set(m_forms, j, f);
-        m().set(m_proofs, j, m().get(m_proofs, i));
-        if (unsat_core_enabled())
-            m().set(m_dependencies, j, m().get(m_dependencies, i));
-        j++;
+        if (i != j) {
+            m().set(m_forms, j, f);
+            m().set(m_proofs, j, pr);
+            if (unsat_core_enabled())
+                m().set(m_dependencies, j, dep);
+        }
+        ++i;
+        ++j;
     }
     shrink(j);
 }
@@ -539,7 +538,7 @@ void goal::elim_redundancies() {
     expr_ref_fast_mark1 neg_lits(m());
     expr_ref_fast_mark2 pos_lits(m());
     unsigned sz = size();
-    unsigned j  = 0;
+    unsigned j = 0;
     for (unsigned i = 0; i < sz; i++) {
         expr * f = form(i);
         if (m().is_true(f))

src/tactic/goal.h

@@ -165,6 +165,41 @@ class goal {
     bool is_cnf() const;
 
     goal * translate(ast_translation & translator) const;
+
+    class iterator {
+    public:
+        using value_type = std::tuple<expr*, expr_dependency*, proof*>;
+        using reference = value_type&;
+        using pointer = value_type*;
+        using difference_type = std::ptrdiff_t;
+        using iterator_category = std::forward_iterator_tag;
+
+        iterator(goal const* g, unsigned idx) : m_goal(g), m_idx(idx) {}
+
+        value_type operator*() const {
+            return std::make_tuple(m_goal->form(m_idx), m_goal->dep(m_idx), m_goal->pr(m_idx));
+        }
+
+        iterator& operator++() {
+            ++m_idx;
+            return *this;
+        }
+
+        bool operator==(const iterator& other) const {
+            return m_goal == other.m_goal && m_idx == other.m_idx;
+        }
+
+        bool operator!=(const iterator& other) const {
+            return !(*this == other);
+        }
+
+    private:
+        goal const* m_goal;
+        unsigned m_idx;
+    };
+
+    iterator begin() const { return iterator(this, 0); }
+    iterator end() const { return iterator(this, size()); }
 };
 
 std::ostream & operator<<(std::ostream & out, goal::precision p);

src/test/algebraic.cpp

@@ -25,18 +25,18 @@ Module Name:
 static void display_anums(std::ostream & out, scoped_anum_vector const & rs) {
     out << "numbers in decimal:\n";
     algebraic_numbers::manager & m = rs.m();
-    for (const auto& r : rs) {
-        m.display_decimal(out, r, 10);
+    for (unsigned i = 0; i < rs.size(); i++) {
+        m.display_decimal(out, rs[i], 10);
         out << "\n";
     }
     out << "numbers as root objects\n";
-    for (const auto& r : rs) {
-        m.display_root(out, r);
+    for (unsigned i = 0; i < rs.size(); i++) {
+        m.display_root(out, rs[i]);
         out << "\n";
     }
     out << "numbers as intervals\n";
-    for (const auto& r : rs) {
-        m.display_interval(out, r);
+    for (unsigned i = 0; i < rs.size(); i++) {
+        m.display_interval(out, rs[i]);
         out << "\n";
     }
 }

src/test/lp/gomory_test.h

@@ -158,8 +158,8 @@ struct gomory_test {
             TRACE("gomory_cut_detail", tout << "pol.size() > 1" << std::endl;);
             lcm_den = lcm(lcm_den, denominator(k));
             TRACE("gomory_cut_detail", tout << "k: " << k << " lcm_den: " << lcm_den << "\n";
-                  for (const auto& p : pol) {
-                      tout << p.first << " " << p.second << "\n";
+                  for (unsigned i = 0; i < pol.size(); i++) {
+                      tout << pol[i].first << " " << pol[i].second << "\n";
                   }
                   tout << "k: " << k << "\n";);
             lp_assert(lcm_den.is_pos());
@@ -172,8 +172,8 @@ struct gomory_test {
                 k *= lcm_den;
             }
             TRACE("gomory_cut_detail", tout << "after *lcm\n";
-                  for (const auto& p : pol) {
-                      tout << p.first << " * v" << p.second << "\n";
+                  for (unsigned i = 0; i < pol.size(); i++) {
+                      tout << pol[i].first << " * v" << pol[i].second << "\n";
                   }
                   tout << "k: " << k << "\n";);
 
@@ -210,7 +210,7 @@ struct gomory_test {
         bool some_int_columns = false;
         mpq f_0  = fractional_part(get_value(inf_col));
         mpq one_min_f_0 = 1 - f_0;
-        for (const auto& pp : row) {
+        for ( auto pp : row) {
             a = pp.first;
             x_j = pp.second;
             if (x_j == inf_col)