mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-31 06:07:46 +00:00
Code Activity

simple choice of non-vanishing

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2026-01-11 20:35:25 -10:00
parent a35fe109ac
commit a46261efe5
1 changed files with 5 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

27
src/nlsat/levelwise.cpp
View file

@ -247,32 +247,15 @@ namespace nlsat {
return coeff; return coeff;
} }
// Second pass: pick the non-constant coefficient with minimal (total_degree, size, max_var). // Second pass : pick the first non-vanishing
polynomial_ref best(m_pm); for (unsigned j = deg + 1; j-- > 0; ) {
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); coeff = m_pm.coeff(p, x, j);
if (!coeff || is_zero(coeff)) if (!coeff || is_zero(coeff))
continue; continue;
if (m_am.eval_sign_at(coeff, sample()) == 0) if (m_am.eval_sign_at(coeff, sample()))
continue; return coeff; // prefer ldcf
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 best; return coeff; // still null
} }
void add_projections_for(todo_set& P, polynomial_ref const& p, unsigned x, polynomial_ref const& nonzero_coeff, bool add_leading_coeff) { void add_projections_for(todo_set& P, polynomial_ref const& p, unsigned x, polynomial_ref const& nonzero_coeff, bool add_leading_coeff) {