From 0b1d30e86f01dbea778a98ef29cfb719d38be6ad Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Wed, 28 Jan 2026 19:42:40 -0800 Subject: [PATCH] [WIP] Refactor NLSAT solver to use structured bindings for variable bounds (#8425) * Initial plan * Refactor NLSAT solver to use structured bindings for variable bounds 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/nlsat/nlsat_solver.cpp | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index ebb7c9fe7..a8497aae5 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -1979,9 +1979,7 @@ namespace nlsat { << " :propagations " << m_stats.m_propagations << " :clauses " << m_clauses.size() << " :learned " << m_learned.size() << ")\n"); - for (auto const& b : bounds) { - var x = b.first; - rational lo = b.second; + for (auto const& [x, lo] : bounds) { rational hi = lo + 1; // rational::one(); bool is_even = false; polynomial_ref p(m_pm);