From 31122b0c105730e1cabcfb1547df97760041fc68 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Sun, 11 Jan 2026 17:44:12 -0800 Subject: [PATCH] Adopt C++17 structured bindings for map/pair iteration (#8159) * Initial plan * Adopt structured bindings for map iteration Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Fix DEBUG_CODE macro issue with structured bindings 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/math/lp/lar_solver.cpp | 2 +- src/math/lp/nex_creator.cpp | 8 ++++---- src/opt/maxsmt.h | 2 +- src/sat/sat_anf_simplifier.cpp | 4 ++-- src/sat/sat_simplifier.cpp | 6 +++--- src/sat/smt/arith_solver.cpp | 4 ++-- src/sat/smt/pb_pb.h | 2 +- src/sat/smt/pb_solver.h | 2 +- src/smt/seq_ne_solver.cpp | 6 ++---- src/smt/smt_internalizer.cpp | 7 +++---- 10 files changed, 20 insertions(+), 23 deletions(-) diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index e65e0a80a..b31014d6b 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -1504,7 +1504,7 @@ namespace lp { variable_values[j] = get_value(j); TRACE(lar_solver_model, tout << "delta = " << m_imp->m_delta << "\nmodel:\n"; - for (auto p : variable_values) tout << this->get_variable_name(p.first) << " = " << p.second << "\n";); + for (auto [var_idx, val] : variable_values) tout << this->get_variable_name(var_idx) << " = " << val << "\n";); } bool lar_solver::init_model() const { diff --git a/src/math/lp/nex_creator.cpp b/src/math/lp/nex_creator.cpp index 763251a9e..30a8b2477 100644 --- a/src/math/lp/nex_creator.cpp +++ b/src/math/lp/nex_creator.cpp @@ -425,17 +425,17 @@ void nex_creator::sort_join_sum(nex_sum& sum) { rational common_scalar(0); fill_join_map_for_sum(sum, map, allocated_nexs, common_scalar); - TRACE(grobner_d, for (auto & p : map ) { tout << "(" << *p.first << ", " << p.second << ") ";}); + TRACE(grobner_d, for (auto & [nex_ptr, coeff] : map ) { tout << "(" << *nex_ptr << ", " << coeff << ") ";}); sum.m_children.reset(); - for (auto& p : map) { - process_map_pair(const_cast(p.first), p.second, sum, allocated_nexs); + for (auto& [nex_ptr, coeff] : map) { + process_map_pair(const_cast(nex_ptr), coeff, sum, allocated_nexs); } if (!common_scalar.is_zero()) { sum.m_children.push_back(mk_scalar(common_scalar)); } TRACE(grobner_d, tout << "map="; - for (auto & p : map ) tout << "(" << *p.first << ", " << p.second << ") "; + for (auto & [nex_ptr, coeff] : map ) tout << "(" << *nex_ptr << ", " << coeff << ") "; tout << "\nchildren=" << sum << "\n";); } diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h index 938f6b870..edf24d9bb 100644 --- a/src/opt/maxsmt.h +++ b/src/opt/maxsmt.h @@ -197,7 +197,7 @@ namespace opt { for (expr* e : soft) _soft.push_back(std::make_pair(e, rational::one())); lbool r = (*this)(_soft); soft.reset(); - for (auto const& p : _soft) soft.push_back(p.first); + for (auto const& [e, w] : _soft) soft.push_back(e); return r; } diff --git a/src/sat/sat_anf_simplifier.cpp b/src/sat/sat_anf_simplifier.cpp index 81d3bb2dd..20e605c9d 100644 --- a/src/sat/sat_anf_simplifier.cpp +++ b/src/sat/sat_anf_simplifier.cpp @@ -251,10 +251,10 @@ namespace sat { TRACE(anf_simplifier, tout << "kept:\n"; for (clause* cp : clauses) tout << *cp << "\n"; - for (auto b : bins) tout << b.first << " " << b.second << "\n"; + for (auto [l1, l2] : bins) tout << l1 << " " << l2 << "\n"; tout << "removed:\n"; for (clause* cp : oclauses) tout << *cp << "\n"; - for (auto b : obins) tout << b.first << " " << b.second << "\n";); + for (auto [l1, l2] : obins) tout << l1 << " " << l2 << "\n";); } void anf_simplifier::set_relevant(solver::bin_clause const& b) { diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 39d01981b..e4a797d0f 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -1766,10 +1766,10 @@ namespace sat { m_elim_todo.reset(); std::stable_sort(tmp.begin(), tmp.end(), bool_var_and_cost_lt()); TRACE(sat_simplifier, - for (auto& p : tmp) tout << "(" << p.first << ", " << p.second << ") "; + for (auto& [v, c] : tmp) tout << "(" << v << ", " << c << ") "; tout << "\n";); - for (auto& p : tmp) - r.push_back(p.first); + for (auto& [v, c] : tmp) + r.push_back(v); } /** diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index 0fab5105c..8228c7118 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -1260,7 +1260,7 @@ namespace arith { TRACE(arith_conflict, tout << "Lemma - " << (is_conflict ? "conflict" : "propagation") << "\n"; for (literal c : m_core) tout << c << ": " << literal2expr(c) << " := " << s().value(c) << "\n"; - for (auto p : m_eqs) tout << ctx.bpp(p.first) << " == " << ctx.bpp(p.second) << "\n";); + for (auto [n1, n2] : m_eqs) tout << ctx.bpp(n1) << " == " << ctx.bpp(n2) << "\n";); if (ctx.get_config().m_arith_validate) VERIFY(validate_conflict()); @@ -1268,7 +1268,7 @@ namespace arith { if (is_conflict) { DEBUG_CODE( for (literal c : m_core) VERIFY(s().value(c) == l_true); - for (auto p : m_eqs) VERIFY(p.first->get_root() == p.second->get_root())); + for (auto [n1, n2] : m_eqs) VERIFY(n1->get_root() == n2->get_root())); ++m_num_conflicts; ++m_stats.m_conflicts; auto* hint = explain_conflict(ty, m_core, m_eqs); diff --git a/src/sat/smt/pb_pb.h b/src/sat/smt/pb_pb.h index 169fe2479..30d1f0c1c 100644 --- a/src/sat/smt/pb_pb.h +++ b/src/sat/smt/pb_pb.h @@ -47,7 +47,7 @@ namespace pb { void negate() override; void set_k(unsigned k) override { m_k = k; VERIFY(k < 4000000000); update_max_sum(); } void swap(unsigned i, unsigned j) noexcept override { std::swap(m_wlits[i], m_wlits[j]); } - literal_vector literals() const override { literal_vector lits; for (auto wl : *this) lits.push_back(wl.second); return lits; } + literal_vector literals() const override { literal_vector lits; for (auto [w, l] : *this) lits.push_back(l); return lits; } bool is_watching(literal l) const override; literal get_lit(unsigned i) const override { return m_wlits[i].second; } void set_lit(unsigned i, literal l) override { m_wlits[i].second = l; } diff --git a/src/sat/smt/pb_solver.h b/src/sat/smt/pb_solver.h index 8ef463dc3..5a09742da 100644 --- a/src/sat/smt/pb_solver.h +++ b/src/sat/smt/pb_solver.h @@ -74,7 +74,7 @@ namespace pb { unsigned bv_coeff(bool_var v) const; void divide(unsigned c); void weaken(unsigned i); - bool contains(literal l) const { for (auto wl : m_wlits) if (wl.second == l) return true; return false; } + bool contains(literal l) const { for (auto [w, lit] : m_wlits) if (lit == l) return true; return false; } }; sat::sat_internalizer& si; diff --git a/src/smt/seq_ne_solver.cpp b/src/smt/seq_ne_solver.cpp index 4afabb896..5abed268c 100644 --- a/src/smt/seq_ne_solver.cpp +++ b/src/smt/seq_ne_solver.cpp @@ -198,12 +198,10 @@ bool theory_seq::reduce_ne(unsigned idx) { tout << "num eqs: " << eqs.size() << "\n"; tout << "num new eqs: " << new_eqs.size() << "\n"; tout << eqs << "\n"; - for (auto const& p : new_eqs) tout << p.first << " != " << p.second << "\n"; + for (auto const& [fst, snd] : new_eqs) tout << fst << " != " << snd << "\n"; tout << p.first << " != " << p.second << "\n";); - for (auto const& p : eqs) { - expr* nl = p.first; - expr* nr = p.second; + for (auto const& [nl, nr] : eqs) { if (m_util.is_seq(nl) || m_util.is_re(nl)) { ls.reset(); rs.reset(); diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 7f0fe1e9e..578a1956e 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -208,11 +208,10 @@ namespace smt { svector sorted_exprs; top_sort_expr(exprs, num_exprs, sorted_exprs); - TRACE(deep_internalize, for (auto & kv : sorted_exprs) tout << "#" << kv.first->get_id() << " " << kv.second << "\n"; ); - for (auto & kv : sorted_exprs) { - expr* e = kv.first; + TRACE(deep_internalize, for (auto & [e, b] : sorted_exprs) tout << "#" << e->get_id() << " " << b << "\n"; ); + for (auto & [e, b] : sorted_exprs) { SASSERT(should_internalize_rec(e)); - internalize_rec(e, kv.second); + internalize_rec(e, b); } } void context::internalize_deep(expr* n) {