From ea1ebdeae07197daea859d76c49a5d0af8cc45e1 Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Tue, 27 Jan 2026 11:47:31 -0800
Subject: [PATCH] Refactor smt_context to use structured bindings for pair
 decomposition (#8385)

* Initial plan

* Refactor smt_context.cpp to use C++17 structured bindings for pair patterns

- Replace .first/.second access with structured bindings in reset_tmp_clauses()
- Replace .first/.second access with structured bindings in decide_clause()
- Replace .first/.second access with structured bindings in init_assumptions()
- Eliminate 3 intermediate variable assignments
- 4 refactoring sites across 3 functions
- Verified successful compilation and all tests pass

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/smt/smt_context.cpp | 13 +++++--------
 1 file changed, 5 insertions(+), 8 deletions(-)

diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 8556a1607..185a830d8 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3336,16 +3336,15 @@ namespace smt {
     }
 
     void context::reset_tmp_clauses() {
-        for (auto& p : m_tmp_clauses) {
-            if (p.first) del_clause(false, p.first);
+        for (auto& [clausep, lits] : m_tmp_clauses) {
+            if (clausep) del_clause(false, clausep);
         }
         m_tmp_clauses.reset();
     }
 
     lbool context::decide_clause() {
         if (m_tmp_clauses.empty()) return l_true;
-        for (auto & tmp_clause : m_tmp_clauses) {
-            literal_vector& lits = tmp_clause.second;
+        for (auto & [clausep, lits] : m_tmp_clauses) {
             literal unassigned = null_literal;
             for (literal l : lits) {
                 switch (get_assignment(l)) {
@@ -3369,7 +3368,7 @@ namespace smt {
                 set_conflict(b_justification(), ~lits[0]);
             }
             else {
-                set_conflict(b_justification(tmp_clause.first), null_literal);
+                set_conflict(b_justification(clausep), null_literal);
             }
             VERIFY(!resolve_conflict());
             return l_false;
@@ -3397,11 +3396,9 @@ namespace smt {
             push_scope();
             vector<std::pair<expr*,expr_ref>> asm2proxy;
             internalize_proxies(asms, asm2proxy);
-            for (auto const& p: asm2proxy) {
+            for (auto const& [orig_assumption, curr_assumption] : asm2proxy) {
                 if (inconsistent())
                     break;
-                expr_ref curr_assumption = p.second;
-                expr* orig_assumption = p.first;
                 if (m.is_true(curr_assumption)) continue;
                 SASSERT(is_valid_assumption(m, curr_assumption));
                 proof * pr = m.mk_asserted(curr_assumption);