From e33dc47d837857bd5dae342f1b98fab2efaab4bd Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 11 Aug 2025 07:24:42 -0700 Subject: [PATCH] remove unused square-free check Signed-off-by: Lev Nachmanson --- src/nlsat/nlsat_explain.cpp | 28 ---------------------------- 1 file changed, 28 deletions(-) diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index f2fa7e623..eaa087999 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -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);