From ac105b7d8c50c24d9cb27230591934212abd1064 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 19 Nov 2023 11:47:00 -0800
Subject: [PATCH] remove unused code
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
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 c303a1541..a352d1d37 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<polynomial*>(A);
- G2 = const_cast<polynomial*>(B);
- }
- else {
- G1 = const_cast<polynomial*>(B);
- G2 = const_cast<polynomial*>(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<polynomial*>(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);
}