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

use is_square_free_at_sample instead of is_well_oriented

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-06-17 07:20:05 -07:00
parent 411fef05d4
commit d4d98a76b8
1 changed files with 13 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

21
src/nlsat/nlsat_explain.cpp
View file

@ -617,11 +617,11 @@ namespace nlsat {
m_todo.insert(p); m_todo.insert(p);
} }
} }
// It is the only check I found to test for well-orientedness, that first appears in
// "An improved projection operation for cylindrical algebraic decomposition of three-dimensional space",
// by McCallum, Scott
bool is_well_oriented(polynomial_ref_vector &ps, var x) { // 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 p(m_pm);
polynomial_ref lc_poly(m_pm); polynomial_ref lc_poly(m_pm);
polynomial_ref disc_poly(m_pm); polynomial_ref disc_poly(m_pm);
@ -634,7 +634,12 @@ namespace nlsat {
// p depends on x // p depends on x
disc_poly = discriminant(p, x); // Use global helper disc_poly = discriminant(p, x); // Use global helper
if (sign(disc_poly) == 0) { // Discriminant is zero if (sign(disc_poly) == 0) { // Discriminant is zero
TRACE(nlsat_explain, tout << "Global !WO: Discriminant of poly is zero. Poly: "; display(tout, p); tout << " Disc: "; display(tout, disc_poly) << "\\n";); 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 false;
} }
} }
@ -647,19 +652,19 @@ namespace nlsat {
polynomial_ref p(m_pm); polynomial_ref p(m_pm);
polynomial_ref coeff(m_pm); polynomial_ref coeff(m_pm);
bool wo = is_well_oriented(ps, x); 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 << (wo ? " (wo)" : " (!wo)") << "\n";); TRACE(nlsat_explain, tout << "processing poly of degree " << k_deg << " w.r.t x" << x << ": "; display(tout, p); tout << (sqf ? " (sqf)" : " (!sqf)") << "\n";);
for (unsigned j_coeff_deg = k_deg; j_coeff_deg >= 1; j_coeff_deg--) { for (unsigned j_coeff_deg = k_deg; j_coeff_deg >= 1; j_coeff_deg--) {
coeff = m_pm.coeff(p, x, j_coeff_deg); coeff = m_pm.coeff(p, x, j_coeff_deg);
TRACE(nlsat_explain, tout << " coeff deg " << j_coeff_deg << ": "; display(tout, coeff) << "\n";); TRACE(nlsat_explain, tout << " coeff deg " << j_coeff_deg << ": "; display(tout, coeff) << "\n";);
add_factors(coeff); add_factors(coeff);
if (wo) if (sqf)
break; break;
} }