mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-08 18:10:57 +00:00
Code Activity

add all coeffs ot a nullified polynomial to the projection

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2026-02-17 14:20:58 -10:00
parent a781f9c0a0
commit 269dba0525
1 changed files with 11 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/nlsat/levelwise.cpp
View file

@ -267,6 +267,17 @@ namespace nlsat {
// request_factorized each of them and continue to the next level. // request_factorized each of them and continue to the next level.
// When a non-vanishing derivative is found, request_factorized it and stop. // When a non-vanishing derivative is found, request_factorized it and stop.
void handle_nullified_poly(polynomial_ref const& p) { void handle_nullified_poly(polynomial_ref const& p) {
// Add all coefficients of p (w.r.t. m_level) to m_todo.
unsigned deg = m_pm.degree(p, m_level);
for (unsigned j = 0; j <= deg; ++j) {
polynomial_ref coeff(m_pm.coeff(p, m_level, j), m_pm);
if (!coeff || is_zero(coeff) || is_const(coeff))
continue;
request_factorized(coeff);
}
// Compute partial derivatives level by level. If all derivatives at a level vanish,
// request_factorized each of them and continue to the next level.
// When a non-vanishing derivative is found, request_factorized it and stop.
polynomial_ref_vector current(m_pm); polynomial_ref_vector current(m_pm);
current.push_back(p); current.push_back(p);
while (!current.empty()) { while (!current.empty()) {