From 851b8ea31cb0bd955b1935e2087c988b534eecc8 Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Wed, 14 Jan 2026 19:52:01 -0800
Subject: [PATCH] Replace manual pair unpacking with structured bindings
 (#8197)

* Initial plan

* Apply structured bindings to enode_bool_pair usage

Replace manual unpacking of pairs with C++17 structured bindings in:
- src/ast/euf/euf_egraph.cpp
- src/smt/smt_internalizer.cpp
- src/smt/smt_context.cpp (2 locations)

This improves code readability and reduces boilerplate code.

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/ast/euf/euf_egraph.cpp   | 6 +++---
 src/smt/smt_context.cpp      | 8 +++-----
 src/smt/smt_internalizer.cpp | 4 +---
 3 files changed, 7 insertions(+), 11 deletions(-)

diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp
index 5ad79cd84..7240d60e8 100644
--- a/src/ast/euf/euf_egraph.cpp
+++ b/src/ast/euf/euf_egraph.cpp
@@ -71,9 +71,9 @@ namespace euf {
     enode_bool_pair egraph::insert_table(enode* p) {
         TRACE(euf_verbose, tout << "insert_table " << bpp(p) << "\n");
         //SASSERT(!m_table.contains_ptr(p));
-        auto rc = m_table.insert(p);
-        p->m_cg = rc.first;
-        return rc;
+        auto [cg, comm] = m_table.insert(p);
+        p->m_cg = cg;
+        return {cg, comm};
     }
 
     void egraph::erase_from_table(enode* p) {
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index fa56c83c9..c7555cf8d 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -656,8 +656,7 @@ namespace smt {
                 }
             }
             if (parent->is_cgc_enabled()) {
-                enode_bool_pair pair = m_cg_table.insert(parent);
-                enode * parent_prime = pair.first;
+                auto [parent_prime, used_commutativity] = m_cg_table.insert(parent);
                 if (parent_prime == parent) {
                     SASSERT(parent);
                     SASSERT(parent->is_cgr());
@@ -668,7 +667,6 @@ namespace smt {
                 parent->m_cg = parent_prime;
                 SASSERT(!m_cg_table.contains_ptr(parent));
                 if (parent_prime->m_root != parent->m_root) {
-                    bool used_commutativity = pair.second;
                     TRACE(cg, tout << "found new congruence: #" << parent->get_owner_id() << " = #" << parent_prime->get_owner_id()
                           << " used_commutativity: " << used_commutativity << "\n";);
                     push_new_congruence(parent, parent_prime, used_commutativity);
@@ -975,8 +973,8 @@ namespace smt {
                     (parent == cg ||           // parent was root of the congruence class before and after the merge
                      !congruent(parent, cg)    // parent was root of the congruence class before but not after the merge
                      )) {
-                    enode_bool_pair p = m_cg_table.insert(parent);
-                    parent->m_cg = p.first;
+                    auto [parent_cg, used_commutativity] = m_cg_table.insert(parent);
+                    parent->m_cg = parent_cg;
                 }
             }
         }
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index 36141636a..e27964bee 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -1029,11 +1029,9 @@ namespace smt {
             }
             else {
                 if (cgc_enabled) {
-                    enode_bool_pair pair = m_cg_table.insert(e);
-                    enode * e_prime      = pair.first;
+                    auto [e_prime, used_commutativity] = m_cg_table.insert(e);
                     if (e != e_prime) {
                         e->m_cg = e_prime;
-                        bool used_commutativity = pair.second;
                         push_new_congruence(e, e_prime, used_commutativity);
                     }
                     else {