From cd774b6fdb04730244fbeeed3a9599f514099cc5 Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Tue, 27 Jan 2026 09:59:26 -0800
Subject: [PATCH] Refactor sat_anf_simplifier to use C++17 structured bindings
 (#8358)

* Initial plan

* Refactor sat_anf_simplifier.cpp to use C++17 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/sat/sat_anf_simplifier.cpp | 26 +++++++++++++++++---------
 1 file changed, 17 insertions(+), 9 deletions(-)

diff --git a/src/sat/sat_anf_simplifier.cpp b/src/sat/sat_anf_simplifier.cpp
index 20e605c9d..8f336dfcf 100644
--- a/src/sat/sat_anf_simplifier.cpp
+++ b/src/sat/sat_anf_simplifier.cpp
@@ -258,8 +258,9 @@ namespace sat {
     }
 
     void anf_simplifier::set_relevant(solver::bin_clause const& b) {
-        set_relevant(b.first); 
-        set_relevant(b.second);
+        auto [l1, l2] = b;
+        set_relevant(l1); 
+        set_relevant(l2);
     }
 
     void anf_simplifier::set_relevant(clause const& c) {
@@ -272,7 +273,8 @@ namespace sat {
     }
 
     bool anf_simplifier::is_pre_satisfied(solver::bin_clause const& b) {
-        return phase_is_true(b.first) || phase_is_true(b.second);
+        auto [l1, l2] = b;
+        return phase_is_true(l1) || phase_is_true(l2);
     }
     
     bool anf_simplifier::phase_is_true(literal l) {
@@ -286,7 +288,8 @@ namespace sat {
     }
 
     bool anf_simplifier::has_relevant_var(solver::bin_clause const& b) {
-        return is_relevant(b.first) || is_relevant(b.second);
+        auto [l1, l2] = b;
+        return is_relevant(l1) || is_relevant(l2);
     }
 
     /**
@@ -310,8 +313,9 @@ namespace sat {
     }
 
     static solver::bin_clause normalize(solver::bin_clause const& b) {
-        if (b.first.index() > b.second.index()) {
-            return solver::bin_clause(b.second, b.first);
+        auto [l1, l2] = b;
+        if (l1.index() > l2.index()) {
+            return solver::bin_clause(l2, l1);
         }
         else {
             return b;
@@ -368,7 +372,10 @@ namespace sat {
         for (unsigned i = 0; i < nv; ++i) id2var[var2id[i]] = i;
         for (unsigned i = 0; i < nv; ++i) vl[i] = std::make_pair(i, var2id[i]);
         std::sort(vl.begin(), vl.end());
-        for (unsigned i = 0; i < nv; ++i) l2v[i] = id2var[vl[i].second];
+        for (unsigned i = 0; i < nv; ++i) {
+            auto [level, varid] = vl[i];
+            l2v[i] = id2var[varid];
+        }
 
         ps.get_manager().reset(l2v);
 
@@ -387,10 +394,11 @@ namespace sat {
 #define lit2pdd(_l_) (_l_.sign() ? ~m.mk_var(_l_.var()) : m.mk_var(_l_.var()))
 
     void anf_simplifier::add_bin(solver::bin_clause const& b, pdd_solver& ps) {
+        auto [l1, l2] = b;
         auto& m = ps.get_manager();
-        dd::pdd p = (lit2pdd(b.first) | lit2pdd(b.second)) ^ true;
+        dd::pdd p = (lit2pdd(l1) | lit2pdd(l2)) ^ true;
         ps.add(p);
-        TRACE(anf_simplifier, tout << "bin: " << b.first << " " << b.second << " : " << p << "\n";);
+        TRACE(anf_simplifier, tout << "bin: " << l1 << " " << l2 << " : " << p << "\n";);
     }
 
     void anf_simplifier::add_clause(clause const& c, pdd_solver& ps) {