From 6c64d271c8c9577cbf1b73850c28144364803376 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 12 Jan 2026 01:06:08 -1000 Subject: [PATCH] restore choose_non_zero_coeff Signed-off-by: Lev Nachmanson --- src/nlsat/levelwise.cpp | 27 ++++++++++++++++++++++----- 1 file changed, 22 insertions(+), 5 deletions(-) diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp index e77758921..49c365fcd 100644 --- a/src/nlsat/levelwise.cpp +++ b/src/nlsat/levelwise.cpp @@ -247,15 +247,32 @@ namespace nlsat { return coeff; } - // Second pass : pick the first non-vanishing - for (unsigned j = deg + 1; j-- > 0; ) { + // Second pass: pick the non-constant coefficient with minimal (total_degree, size, max_var). + polynomial_ref best(m_pm); + unsigned best_td = 0; + unsigned best_sz = 0; + var best_mv = null_var; + for (unsigned j = 0; j <= deg; ++j) { coeff = m_pm.coeff(p, x, j); if (!coeff || is_zero(coeff)) continue; - if (m_am.eval_sign_at(coeff, sample())) - return coeff; // prefer ldcf + if (m_am.eval_sign_at(coeff, sample()) == 0) + continue; + + unsigned td = total_degree(coeff); + unsigned sz = m_pm.size(coeff); + var mv = m_pm.max_var(coeff); + if (!best || + td < best_td || + (td == best_td && (sz < best_sz || + (sz == best_sz && (best_mv == null_var || mv < best_mv))))) { + best = coeff; + best_td = td; + best_sz = sz; + best_mv = mv; + } } - return coeff; // still null + return best; } void add_projections_for(todo_set& P, polynomial_ref const& p, unsigned x, polynomial_ref const& nonzero_coeff, bool add_leading_coeff) {