From 314ffe6c29bd20546af585f5632d3c3162143862 Mon Sep 17 00:00:00 2001
From: "github-actions[bot]"
 <41898282+github-actions[bot]@users.noreply.github.com>
Date: Tue, 28 Apr 2026 21:09:31 +0000
Subject: [PATCH] nla_grobner: remove dead code and fix indentation

- Remove two commented-out DEBUG_CODE/check_missing_propagation lines
- Remove commented-out IF_VERBOSE(0) and lemma.display debug calls
- Remove #if 0 dead code block in configure()
- Remove stale comment in diagnose_pdd_miss
- Fix 3-space indent to 4-space for --m_quota

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 src/math/lp/nla_grobner.cpp | 25 +------------------------
 1 file changed, 1 insertion(+), 24 deletions(-)

diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp
index 94c8c6990..61ab29def 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();
@@ -627,9 +607,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()) {