mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-12 06:00:53 +00:00
Code Activity

remove unused square-free check

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-08-11 07:24:42 -07:00
parent b7d5add9c4
commit e33dc47d83
1 changed files with 0 additions and 28 deletions
Download patch file Download diff file Expand all files Collapse all files

28
src/nlsat/nlsat_explain.cpp
View file

@ -618,34 +618,6 @@ namespace nlsat {
} }
} }
// The monomials have to be square free according to
//"An improved projection operation for cylindrical algebraic decomposition of three-dimensional space", by McCallum, Scott
bool is_square_free_at_sample(polynomial_ref_vector &ps, var x) {
polynomial_ref p(m_pm);
polynomial_ref lc_poly(m_pm);
polynomial_ref disc_poly(m_pm);
for (unsigned i = 0; i < ps.size(); i++) {
p = ps.get(i);
unsigned k_deg = m_pm.degree(p, x);
if (k_deg == 0)
continue;
// p depends on x
disc_poly = discriminant(p, x); // Use global helper
if (sign(disc_poly) == 0) { // Discriminant is zero
TRACE(nlsat_explain, tout << "p is not square free:\n ";
display(tout, p); tout << "\ndiscriminant: "; display(tout, disc_poly) << "\n";
m_solver.display_assignment(tout) << '\n';
m_solver.display_var(tout << "x:", x) << '\n';
);
return false;
}
}
return true;
}
// For each p in ps add the leading coefficent to the projection, // For each p in ps add the leading coefficent to the projection,
void add_lc(polynomial_ref_vector &ps, var x) { void add_lc(polynomial_ref_vector &ps, var x) {
polynomial_ref p(m_pm); polynomial_ref p(m_pm);