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

@@ -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 {

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<nex*>(p.first), p.second, sum, allocated_nexs);
+    for (auto& [nex_ptr, coeff] : map) {
+        process_map_pair(const_cast<nex*>(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";);    
 }
 

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

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) {

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

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

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

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;

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

src/smt/smt_internalizer.cpp

@@ -208,11 +208,10 @@ namespace smt {
 
         svector<expr_bool_pair> 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) {