From 6d38d5ed41dcb83c8473b5ecffeeee7959412bd9 Mon Sep 17 00:00:00 2001
From: Arie <123119895+1arie1@users.noreply.github.com>
Date: Tue, 28 Apr 2026 20:31:11 -0400
Subject: [PATCH] NLA tracing: emit varmap and grobner-linear-eq for trace
 analysis (#9415)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Two TRACE blocks under the existing nla_solver tag:

1. theory_lra::false_case_of_check_nla emits a "varmap:" line for each
   NLA lemma, listing j-var → SMT-name mappings for variables in the
   lemma's collect_vars set. Lets lemur nla resolve the LP-internal
   j-numbering back to the original SMT term names when displaying
   lemmas. Without this, lemma-level analysis has to either guess at
   variable identities (and j-numbers are reused across nlsat
   invocations under backtracking — see j-vars-unstable note) or use a
   different trace tag entirely (-tr:nra) for stable algebraic-number
   IDs.

2. nla_grobner emits a "grobner-linear-eq:" line at each call to
   add_term + update_column_type_and_bound that produces a Linear
   Propagation row from completion. Lets us count Gröbner's effective
   contribution to the LP tableau independently of the lemma stream.
   Useful when investigating Gröbner-deficit hypotheses in NLA cascade
   diagnosis.

Both are pure trace emission, behind TRACE(nla_solver, ...). Zero
runtime cost when tracing is off; no semantic change.
---
 src/math/lp/nla_grobner.cpp | 10 +++++++++-
 src/smt/theory_lra.cpp      |  8 ++++++++
 2 files changed, 17 insertions(+), 1 deletion(-)

diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp
index 94c8c6990..7339f5fe8 100644
--- a/src/math/lp/nla_grobner.cpp
+++ b/src/math/lp/nla_grobner.cpp
@@ -741,7 +741,15 @@ namespace nla {
 
         lp::lpvar j = c().lra.add_term(coeffs, UINT_MAX);
         c().lra.update_column_type_and_bound(j, lp::lconstraint_kind::EQ, offset, e.dep());
-        c().m_check_feasible = true; 
+        c().m_check_feasible = true;
+        TRACE(nla_solver,
+            // Print the term as installed (post subst_known_terms), not the
+            // pre-add_term coeffs vector. add_term normalizes/substitutes
+            // term-column references, so coeffs and the resulting row can
+            // diverge if any var is itself a term-column.
+            tout << "grobner-linear-eq: ";
+            c().lra.print_term(c().lra.get_term(j), tout);
+            tout << " = " << offset << "\n";);
         return true;
     }
 
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 23c102874..b4016dca8 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2126,6 +2126,14 @@ public:
         m_explanation = l.expl();
         literal_vector core;
         SASSERT(!m_lemma.is_empty());
+        TRACE(nla_solver,
+            tout << "varmap:";
+            for (lpvar j : m_nla->get_core().collect_vars(l)) {
+                auto ext = lp().local_to_external(j);
+                if (ext != lp::null_lpvar && static_cast<unsigned>(ext) < th.get_num_vars())
+                    tout << " " << lp().get_variable_name(j) << "=" << pp(ext);
+            }
+            tout << "\n";);
         for (auto const& ineq : m_lemma.ineqs()) {
             auto lit = mk_literal(ineq);
             core.push_back(~lit);