From 2e2a2e28df7cc6c1d2dc9401e3ebf873fb3148f5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 16 Mar 2025 20:04:04 -0700 Subject: [PATCH] use iterators on goal and other refactoring --- src/tactic/bv/elim_small_bv_tactic.cpp | 15 ++++----- src/tactic/core/cofactor_term_ite_tactic.cpp | 7 ++-- src/tactic/core/ctx_simplify_tactic.cpp | 9 +++-- src/tactic/core/der_tactic.cpp | 13 +++----- src/tactic/goal.cpp | 29 ++++++++-------- src/tactic/goal.h | 35 ++++++++++++++++++++ src/test/algebraic.cpp | 12 +++---- src/test/lp/gomory_test.h | 10 +++--- 8 files changed, 77 insertions(+), 53 deletions(-) diff --git a/src/tactic/bv/elim_small_bv_tactic.cpp b/src/tactic/bv/elim_small_bv_tactic.cpp index 54f4dc915..43ff9090d 100644 --- a/src/tactic/bv/elim_small_bv_tactic.cpp +++ b/src/tactic/bv/elim_small_bv_tactic.cpp @@ -256,22 +256,19 @@ public: 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()); diff --git a/src/tactic/core/cofactor_term_ite_tactic.cpp b/src/tactic/core/cofactor_term_ite_tactic.cpp index b65fd8353..1bd4cf11a 100644 --- a/src/tactic/core/cofactor_term_ite_tactic.cpp +++ b/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); } } diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp index e3cd7893a..ed9b277a8 100644 --- a/src/tactic/core/ctx_simplify_tactic.cpp +++ b/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 { diff --git a/src/tactic/core/der_tactic.cpp b/src/tactic/core/der_tactic.cpp index 011804803..4df46e19e 100644 --- a/src/tactic/core/der_tactic.cpp +++ b/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(); } diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp index 43cecf92d..96cf4e888 100644 --- a/src/tactic/goal.cpp +++ b/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)) diff --git a/src/tactic/goal.h b/src/tactic/goal.h index b0b8d95f1..b93d655c0 100644 --- a/src/tactic/goal.h +++ b/src/tactic/goal.h @@ -165,6 +165,41 @@ public: bool is_cnf() const; goal * translate(ast_translation & translator) const; + + class iterator { + public: + using value_type = std::tuple; + 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); diff --git a/src/test/algebraic.cpp b/src/test/algebraic.cpp index 8d1b60777..371997c02 100644 --- a/src/test/algebraic.cpp +++ b/src/test/algebraic.cpp @@ -25,18 +25,18 @@ Notes: 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"; } } diff --git a/src/test/lp/gomory_test.h b/src/test/lp/gomory_test.h index f7f822566..9ac675d1a 100644 --- a/src/test/lp/gomory_test.h +++ b/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)