From 1d49af5ee6ffee72fd27676dadbff665cfe69496 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Tue, 27 Jan 2026 20:06:07 -0800 Subject: [PATCH] Refactor sat_solver to use C++17 structured bindings for pair destructuring (#8403) * Initial plan * Refactor sat_solver.cpp to use structured bindings for pairs - Line 1398: Changed priorities[i].second to use [priority, var] - Lines 2154-2156: Changed p.first/p.second to use [l1, l2] for binary clauses - Lines 4182-4184: Eliminated intermediate l1, l2 variables using [l1, l2] binding This modernizes the code to use C++17 structured bindings instead of .first/.second member accesses. 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/sat/sat_solver.cpp | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index ad2bae1a5..c5744e2b4 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1394,8 +1394,10 @@ namespace sat { for (unsigned i = 0; i < mdl.size(); ++i) priorities[i] = { m_local_search->get_priority(i), i }; std::sort(priorities.begin(), priorities.end(), [](auto& x, auto& y) { return x.first > y.first; }); - for (unsigned i = priorities.size() / 10; i-- > 0; ) - move_to_front(priorities[i].second); + for (unsigned i = priorities.size() / 10; i-- > 0; ) { + auto [priority, var] = priorities[i]; + move_to_front(var); + } #endif @@ -2151,9 +2153,9 @@ namespace sat { #if 0 IF_VERBOSE(2, for (bool_var v = 0; v < num; ++v) verbose_stream() << v << ": " << m_model[v] << "\n";); - for (auto p : big::s_del_bin) { - if (value(p.first) != l_true && value(p.second) != l_true) { - IF_VERBOSE(2, verbose_stream() << "binary violation: " << p.first << " " << p.second << "\n"); + for (auto [l1, l2] : big::s_del_bin) { + if (value(l1) != l_true && value(l2) != l_true) { + IF_VERBOSE(2, verbose_stream() << "binary violation: " << l1 << " " << l2 << "\n"); } } #endif @@ -4179,9 +4181,7 @@ namespace sat { // m_binary_clause_graph.reset(); collect_bin_clauses(m_user_bin_clauses, true, false); hashtable, default_eq > seen_bc; - for (auto const& b : m_user_bin_clauses) { - literal l1 = b.first; - literal l2 = b.second; + for (auto const& [l1, l2] : m_user_bin_clauses) { literal_pair p(l1, l2); if (!seen_bc.contains(p)) { seen_bc.insert(p);