mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-14 23:05:26 +00:00
Code Activity

get the finest factorizations before project

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-08-07 16:22:46 -07:00 • committed by Lev Nachmanson
parent efb0bda885
commit 88293bf45b
1 changed files with 17 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

34
src/nlsat/nlsat_explain.cpp
View file

@ -593,7 +593,7 @@ namespace nlsat {
/** /**
\brief Add factors of p to todo \brief Add factors of p to todo
*/ */
void add_factors(polynomial_ref & p) { void insert_fresh_factors_in_todo(polynomial_ref & p) {
if (is_const(p)) if (is_const(p))
return; return;
elim_vanishing(p); elim_vanishing(p);
@ -646,27 +646,21 @@ namespace nlsat {
return true; return true;
} }
// For each p in ps add the leading or all the coefficients of p to the projection, // For each p in ps add the leading or coefficent to the projection,
// depending on the well-orientedness of ps.
void add_lcs(polynomial_ref_vector &ps, var x) { void add_lcs(polynomial_ref_vector &ps, var x) {
polynomial_ref p(m_pm); polynomial_ref p(m_pm);
polynomial_ref coeff(m_pm); polynomial_ref coeff(m_pm);
bool sqf = is_square_free_at_sample(ps, x);
// Add coefficients based on well-orientedness // Add coefficients based on well-orientedness
for (unsigned i = 0; i < ps.size(); i++) { for (unsigned i = 0; i < ps.size(); i++) {
p = ps.get(i); p = ps.get(i);
unsigned k_deg = m_pm.degree(p, x); unsigned k_deg = m_pm.degree(p, x);
if (k_deg == 0) continue; if (k_deg == 0) continue;
// p depends on x // p depends on x
TRACE(nlsat_explain, tout << "processing poly of degree " << k_deg << " w.r.t x" << x << ": "; display(tout, p); tout << (sqf ? " (sqf)" : " (!sqf)") << "\n";); TRACE(nlsat_explain, tout << "processing poly of degree " << k_deg << " w.r.t x" << x << ": "; display(tout, p) << "\n";);
for (unsigned j_coeff_deg = k_deg; j_coeff_deg >= 1; j_coeff_deg--) { coeff = m_pm.coeff(p, x, k_deg);
coeff = m_pm.coeff(p, x, j_coeff_deg); TRACE(nlsat_explain, tout << " coeff deg " << k_deg << ": "; display(tout, coeff) << "\n";);
TRACE(nlsat_explain, tout << " coeff deg " << j_coeff_deg << ": "; display(tout, coeff) << "\n";); insert_fresh_factors_in_todo(coeff);
add_factors(coeff);
if (sqf)
break;
}
} }
} }
@ -772,7 +766,7 @@ namespace nlsat {
display(tout, s); display(tout, s);
tout << "\n";); tout << "\n";);
// s did not vanish completely, but its leading coefficient may have vanished // s did not vanish completely, but its leading coefficient may have vanished
add_factors(s); insert_fresh_factors_in_todo(s);
return; return;
} }
} }
@ -1231,18 +1225,24 @@ namespace nlsat {
return; return;
m_todo.reset(); m_todo.reset();
for (poly* p : ps) { for (unsigned i = 0; i < ps.size(); i++) {
m_todo.insert(p); polynomial_ref p(m_pm);
p = ps.get(i);
insert_fresh_factors_in_todo(p);
} }
// replace ps by the fresh factors
ps.reset();
for (auto p: m_todo.m_set)
ps.push_back(p);
var x = m_todo.extract_max_polys(ps); var x = m_todo.extract_max_polys(ps);
// Remark: after vanishing coefficients are eliminated, ps may not contain max_x anymore // Remark: after vanishing coefficients are eliminated, ps may not contain max_x anymore
polynomial_ref_vector samples(m_pm); polynomial_ref_vector samples(m_pm);
if (x < max_x){ if (x < max_x)
cac_add_cell_lits(ps, x, samples); cac_add_cell_lits(ps, x, samples);
}
while (true) { while (true) {
if (all_univ(ps, x) && m_todo.empty()) { if (all_univ(ps, x) && m_todo.empty()) {