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

make the new multivariate factorization more resilient

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2026-03-22 15:40:19 -10:00 • committed by Lev Nachmanson
parent 09339c82ab
commit 31c6c3ee79
1 changed files with 27 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

37
src/math/polynomial/polynomial.cpp
View file

@ -470,8 +470,8 @@ namespace polynomial {
void reset(monomial const * m) { void reset(monomial const * m) {
unsigned id = m->id(); unsigned id = m->id();
SASSERT(id < m_m2pos.size()); if (id < m_m2pos.size())
m_m2pos[id] = UINT_MAX; m_m2pos[id] = UINT_MAX;
} }
void set(monomial const * m, unsigned pos) { void set(monomial const * m, unsigned pos) {
@ -7200,10 +7200,28 @@ namespace polynomial {
return; return;
} }
// Multivariate factorization via evaluation + bivariate Hensel lifting. // Try multivariate factorization. If checkpoint() throws during the
// Strategy: try (main_var, lift_var, eval_point) configurations. // attempt, the shared som_buffer/m_m2pos may be left dirty. Catch the
// For each, reduce to bivariate, factor via Hensel lifting, then check if // exception, reset the buffers, return unfactored, then rethrow so
// the bivariate factors divide the original polynomial. // cancellation propagates normally.
try {
if (try_multivar_factor(p, r, x, k))
return;
}
catch (...) {
m_som_buffer.reset();
m_som_buffer2.reset();
m_cheap_som_buffer.reset();
m_cheap_som_buffer2.reset();
throw;
}
// Could not factor, return p as-is
r.push_back(const_cast<polynomial*>(p), k);
}
// Returns true if factorization succeeded and factors were added to r.
bool try_multivar_factor(polynomial const * p, factors & r, var x, unsigned k) {
var_vector all_vars; var_vector all_vars;
m_wrapper.vars(p, all_vars); m_wrapper.vars(p, all_vars);
@ -7374,7 +7392,7 @@ namespace polynomial {
else else
r.push_back(bf, k); r.push_back(bf, k);
} }
return; return true;
} }
// Multivariate: check if bivariate factors divide original p. // Multivariate: check if bivariate factors divide original p.
@ -7410,7 +7428,7 @@ namespace polynomial {
else else
r.push_back(part, k); r.push_back(part, k);
} }
return; return true;
} }
} }
} }
@ -7420,8 +7438,7 @@ namespace polynomial {
} }
} }
// Could not factor, return p as-is return false;
r.push_back(const_cast<polynomial*>(p), k);
} }
void factor_sqf_pp(polynomial const * p, factors & r, var x, unsigned k, factor_params const & params) { void factor_sqf_pp(polynomial const * p, factors & r, var x, unsigned k, factor_params const & params) {