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

Merge branch 'Z3Prover:master' into parallel-solving

Browse source
This commit is contained in:
Ilana Shapiro 2025-08-11 11:19:17 -07:00 • committed by GitHub
commit 53eb2cac31
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
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,
void add_lc(polynomial_ref_vector &ps, var x) {
polynomial_ref p(m_pm);