From 09396b72ddd39fdc6753c358ec33d1db334e0b14 Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Wed, 29 Apr 2026 11:12:45 -0700
Subject: [PATCH] nla_grobner: remove dead code and fix indentation (#9423)

* Initial plan

* [code-simplifier] nla_grobner: remove dead code and fix indentation

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/1dc7dd96-d7d7-4fca-94b4-bde677fee842

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/math/lp/nla_grobner.cpp | 24 +-----------------------
 1 file changed, 1 insertion(+), 23 deletions(-)

diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp
index 7339f5fe8..19cb00c28 100644
--- a/src/math/lp/nla_grobner.cpp
+++ b/src/math/lp/nla_grobner.cpp
@@ -108,10 +108,6 @@ namespace nla {
             }
         }
 
-        // DEBUG_CODE(for (auto e : m_solver.equations()) check_missing_propagation(*e););
-
-        // for (auto e : m_solver.equations()) check_missing_propagation(*e);
-
         if (c().params().arith_nl_grobner_adaptive())
             update_growth_boost(productive);
 
@@ -120,7 +116,7 @@ namespace nla {
 
         ++m_delay_base;
         if (m_quota > 0)
-           --m_quota;
+            --m_quota;
 
         IF_VERBOSE(5, verbose_stream() << "grobner miss, quota " << m_quota << "\n");
         IF_VERBOSE(5, diagnose_pdd_miss(verbose_stream()));
@@ -235,8 +231,6 @@ namespace nla {
         if (vars.empty() || !q.is_linear())
             return false;
 
-        // IF_VERBOSE(0, verbose_stream() << "factored " << q << " : " << vars << "\n");
-
         auto [t, offset] = linear_to_term(q);
 
         vector<ineq> ineqs;
@@ -251,7 +245,6 @@ namespace nla {
         add_dependencies(lemma, eq);
         for (auto const& i : ineqs)
             lemma |= i;
-        //lemma.display(verbose_stream());
         return true;
     }
 
@@ -584,19 +577,6 @@ namespace nla {
         }
         TRACE(grobner, m_solver.display(tout));
 
-#if 0
-        IF_VERBOSE(2, m_pdd_grobner.display(verbose_stream()));
-        dd::pdd_eval eval(m_pdd_manager);
-        eval.var2val() = [&](unsigned j){ return val(j); };
-        for (auto* e : m_pdd_grobner.equations()) {
-            dd::pdd p = e->poly();
-            rational v = eval(p);
-            if (p.is_linear() && !eval(p).is_zero()) {
-                IF_VERBOSE(0, verbose_stream() << "violated linear constraint " << p << "\n");
-            }
-        }
-#endif
-   
         struct dd::solver::config cfg;
         cfg.m_max_steps = m_solver.equations().size();
         cfg.m_max_simplified = c().params().arith_nl_grobner_max_simplified();
@@ -628,8 +608,6 @@ namespace nla {
 
     std::ostream& grobner::diagnose_pdd_miss(std::ostream& out) {
 
-        // m_pdd_grobner.display(out);
-
         dd::pdd_eval eval;
         eval.var2val() = [&](unsigned j){ return val(j); };
         for (auto* e : m_solver.equations()) {