mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-20 09:13:20 +00:00
Code Activity

restore choose_non_zero_coeff

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2026-01-12 01:06:08 -10:00
parent c6125711b4
commit be3044c3f9
1 changed files with 22 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

27
src/nlsat/levelwise.cpp
View file

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