From ff485eb545179ffb63d316a8ab2bc145203b582f Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Sat, 31 Jan 2026 17:13:07 -0800
Subject: [PATCH] Refactor sat_model_converter to use C++17 structured bindings
 (#8440)

* Initial plan

* Refactor sat_model_converter to use C++17 structured bindings

- Updated model_converter::process_stack() to use structured bindings
- Updated model_converter::display() to use structured bindings
- Updated model_converter::expand() to use structured bindings in range-based loop
- All changes compile successfully

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix build error in smt_justification.cpp structured binding

- Changed invalid syntax `enode_pair const & [n1, n2]` to `auto const& [n1, n2]`
- Wrapped for loop in extra parentheses to protect structured binding comma from macro expansion
- Build now completes successfully

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix DEBUG_CODE macro issue with structured bindings

- Reverted DEBUG_CODE block to use .first/.second instead of structured bindings
- Structured bindings with commas cause issues in macros (treated as argument separators)
- Build now works in both debug and release modes

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_model_converter.cpp | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp
index 2560e7e45..67136d79a 100644
--- a/src/sat/sat_model_converter.cpp
+++ b/src/sat/sat_model_converter.cpp
@@ -46,8 +46,7 @@ namespace sat {
         SASSERT(!stack.empty());
         unsigned sz = stack.size();
         for (unsigned i = sz; i-- > 0; ) {
-            unsigned csz = stack[i].first;
-            literal lit = stack[i].second;
+            auto [csz, lit] = stack[i];
             bool sat = false;
             for (unsigned j = 0; !sat && j < csz; ++j) {
                 sat = value_at(c[j], m) == l_true;
@@ -317,7 +316,8 @@ namespace sat {
                     elim_stackv const& stack = st->stack();
                     unsigned sz = stack.size();
                     for (unsigned i = sz; i-- > 0; ) {
-                        out << "\n   " << stack[i].first << " " << stack[i].second;
+                        auto [csz, lit] = stack[i];
+                        out << "\n   " << csz << " " << lit;
                     }
                 }
                 ++index;
@@ -385,9 +385,7 @@ namespace sat {
                     if (st) {
                         // clause sizes increase, so we can always swap
                         // the blocked literal to the front from the prefix.
-                        for (auto const& p : st->stack()) {
-                            unsigned csz = p.first;
-                            literal lit = p.second;
+                        for (auto const& [csz, lit] : st->stack()) {
                             swap(lit.var(), csz, clause);
                             update_stack.append(csz, clause.data());
                             update_stack.push_back(null_literal);