From 93cf989b780e51ec25ff8bdb8a6defbc0e08c2a2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 24 Mar 2025 12:35:46 -0700 Subject: [PATCH] household chores - move to iterators --- src/tactic/arith/degree_shift_tactic.cpp | 6 ++---- src/tactic/arith/fix_dl_var_tactic.cpp | 20 ++++++++------------ 2 files changed, 10 insertions(+), 16 deletions(-) diff --git a/src/tactic/arith/degree_shift_tactic.cpp b/src/tactic/arith/degree_shift_tactic.cpp index d9447d378..888503f6b 100644 --- a/src/tactic/arith/degree_shift_tactic.cpp +++ b/src/tactic/arith/degree_shift_tactic.cpp @@ -169,10 +169,8 @@ class degree_shift_tactic : public tactic { void collect(goal const & g) { m_var2degree.reset(); expr_fast_mark1 visited; - unsigned sz = g.size(); - for (unsigned i = 0; i < sz; i++) { - collect(g.form(i), visited); - } + for (auto [f, d, p] : g) + collect(f, visited); TRACE("degree_shift", display_candidates(tout);); } diff --git a/src/tactic/arith/fix_dl_var_tactic.cpp b/src/tactic/arith/fix_dl_var_tactic.cpp index 30e145ccb..7a51d01fe 100644 --- a/src/tactic/arith/fix_dl_var_tactic.cpp +++ b/src/tactic/arith/fix_dl_var_tactic.cpp @@ -216,10 +216,8 @@ class fix_dl_var_tactic : public tactic { try { expr_fast_mark1 visited; flet _visited(m_visited, &visited); - unsigned sz = g.size(); - for (unsigned i = 0; i < sz; i++) { - process(g.form(i)); - } + for (auto [f, d, p] : g) + process(f); return most_occs(); } catch (const failed &) { @@ -268,15 +266,13 @@ class fix_dl_var_tactic : public tactic { 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, d, p] : *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(p, new_pr); + g->update(idx++, new_curr, new_pr, d); } g->inc_depth(); }