From ac105b7d8c50c24d9cb27230591934212abd1064 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 19 Nov 2023 11:47:00 -0800 Subject: [PATCH] remove unused code Signed-off-by: Nikolaj Bjorner --- src/math/polynomial/polynomial.cpp | 169 ----------------------------- 1 file changed, 169 deletions(-) diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp index c303a154101..a352d1d37a0 100644 --- a/src/math/polynomial/polynomial.cpp +++ b/src/math/polynomial/polynomial.cpp @@ -5614,92 +5614,6 @@ namespace polynomial { } } - void psc_chain1(polynomial const * p, polynomial const * q, var x, polynomial_ref_vector & S) { - subresultant_chain(p, q, x, S); - unsigned sz = S.size(); - TRACE("psc", tout << "subresultant_chain\n"; - for (unsigned i = 0; i < sz; i++) { tout << "i: " << i << " "; S.get(i)->display(tout, m_manager); tout << "\n"; }); - for (unsigned i = 0; i < sz - 1; i++) { - S.set(i, coeff(S.get(i), x, i)); - } - S.set(sz-1, mk_one()); - } - - // Store in S a list of the non-zero principal subresultant coefficients of A and B - // If i < j then psc_{i}(A,B) precedes psc_{j}(A,B) in S. - // The leading coefficients of A and B are not included in S. - void psc_chain2(polynomial const * A, polynomial const * B, var x, polynomial_ref_vector & S) { - polynomial_ref G1(pm()); - polynomial_ref G2(pm()); - polynomial_ref G3(pm()); - polynomial_ref Gh3(pm()); - polynomial_ref g1(pm()), h0(pm()), hs0(pm()), h1(pm()), hs1(pm()); - unsigned n1 = degree(A, x); - unsigned n2 = degree(B, x); - if (n1 > n2) { - G1 = const_cast(A); - G2 = const_cast(B); - } - else { - G1 = const_cast(B); - G2 = const_cast(A); - std::swap(n1, n2); - } - unsigned d0 = 0; - unsigned d1 = n1 - n2; - unsigned i = 1; - unsigned n3 = 0; - S.reset(); - while (true) { - // Compute Gh_{i+2} - if (!is_zero(G2)) { - exact_pseudo_remainder(G1, G2, x, Gh3); - n3 = degree(Gh3, x); - if (!is_zero(Gh3) && d1%2 == 0) - Gh3 = neg(Gh3); - } - else - n3 = 0; - - // Compute hi - if (i > 1) { - g1 = lc(G1, x); - pw(g1, d0, h1); - if (i > 2) { - pw(h0, d0 - 1, hs0); - h1 = exact_div(h1, hs0); - S.push_back(h1); - if (is_zero(G2)) { - std::reverse(S.data(), S.data() + S.size()); - return; - } - } - } - - // Compute G_{i+2} - if (i == 1 || is_zero(Gh3)) { - G3 = Gh3; - } - else { - pw(h1, d1, hs1); - hs1 = mul(g1, hs1); - G3 = exact_div(Gh3, hs1); - hs1 = nullptr; - } - - // prepare for next iteration - n1 = n2; - n2 = n3; - d0 = d1; - d1 = n1 - n2; - G1 = G2; - G2 = G3; - if (i > 1) - h0 = h1; - i = i + 1; - } - } - // Optimized calculation of S_e using "Dichotomous Lazard" void Se_Lazard(unsigned d, polynomial const * lc_S_d, polynomial const * S_d_1, var x, polynomial_ref & S_e) { unsigned n = d - degree(S_d_1, x) - 1; @@ -5860,90 +5774,7 @@ namespace polynomial { std::reverse(S.data(), S.data() + S.size()); } - void psc_chain_classic_core(polynomial const * P, polynomial const * Q, var x, polynomial_ref_vector & S) { - TRACE("psc_chain_classic", tout << "P: "; P->display(tout, m_manager); tout << "\nQ: "; Q->display(tout, m_manager); tout << "\n";); - unsigned degP = degree(P, x); - unsigned degQ = degree(Q, x); - SASSERT(degP >= degQ); - polynomial_ref A(pm()), B(pm()), C(pm()), minus_Q(pm()), lc_Q(pm()), lc_B(pm()), lc_A(pm()); - polynomial_ref tmp1(pm()), tmp2(pm()), s_delta(pm()), minus_B(pm()), ps(pm()); - - lc_Q = lc(Q, x); - polynomial_ref s(pm()); - // s <- lc(Q)^(deg(P)-deg(Q)) - pw(lc_Q, degP - degQ, s); - minus_Q = neg(Q); - // A <- Q - A = const_cast(Q); - // B <- prem(P, -Q) - exact_pseudo_remainder(P, minus_Q, x, B); - while (true) { - unsigned d = degree(A, x); - unsigned e = degree(B, x); - if (is_zero(B)) - return; - TRACE("psc_chain_classic", tout << "A: " << A << "\nB: " << B << "\ns: " << s << "\nd: " << d << ", e: " << e << "\n";); - // B is S_{d-1} - ps = coeff(B, x, d-1); - if (!is_zero(ps)) - S.push_back(ps); - unsigned delta = d - e; - if (delta > 1) { - // C <- S_e - // Standard S_e calculation - // C <- (lc(B)^(delta-1) B) / s^(delta-1) - lc_B = lc(B, x); - pw(lc_B, delta-1, lc_B); - lc_B = mul(lc_B, B); - pw(s, delta - 1, s_delta); // s_delta <- s^(delta-1) - C = exact_div(lc_B, s_delta); - - // s_delta <- s^delta - s_delta = mul(s_delta, s); - // C is S_e - ps = coeff(C, x, e); - if (!is_zero(ps)) - S.push_back(ps); - - } - else { - SASSERT(delta == 0 || delta == 1); - C = B; - // s_delta <- s^delta - pw(s, delta, s_delta); - } - if (e == 0) - return; - // B <- prem(A, -B)/(s^delta * lc(A) - lc_A = lc(A, x); - minus_B = neg(B); - exact_pseudo_remainder(A, minus_B, x, tmp1); - tmp2 = mul(lc_A, s_delta); - B = exact_div(tmp1, tmp2); - // A <- C - A = C; - // s <- lc(A) - s = lc(A, x); - } - } - - void psc_chain_classic(polynomial const * P, polynomial const * Q, var x, polynomial_ref_vector & S) { - SASSERT(degree(P, x) > 0); - SASSERT(degree(Q, x) > 0); - S.reset(); - if (degree(P, x) >= degree(Q, x)) - psc_chain_classic_core(P, Q, x, S); - else - psc_chain_classic_core(Q, P, x, S); - if (S.empty()) - S.push_back(mk_zero()); - std::reverse(S.data(), S.data() + S.size()); - } - void psc_chain(polynomial const * A, polynomial const * B, var x, polynomial_ref_vector & S) { - // psc_chain1(A, B, x, S); - //psc_chain2(A, B, x, S); - //psc_chain_classic(A, B, x, S); psc_chain_optimized(A, B, x, S); }