mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-06 02:15:16 +00:00
Code Activity

NLA tracing: emit varmap and grobner-linear-eq for trace analysis (#9415)

Browse source 
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.
This commit is contained in:
Arie 2026-04-28 20:31:11 -04:00 • committed by GitHub
parent dbb91de64b
commit 6d38d5ed41
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 17 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/math/lp/nla_grobner.cpp
View file

@ -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;
}

8
src/smt/theory_lra.cpp
View file

@ -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);