Skip to content

Commit

Permalink
remove unused code
Browse files Browse the repository at this point in the history 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
  • Loading branch information
@NikolajBjorner
NikolajBjorner committed Nov 19, 2023
1 parent 4350bd7 commit ac105b7
Showing 1 changed file with 0 additions and 169 deletions.
169 changes: 0 additions & 169 deletions src/math/polynomial/polynomial.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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);
}

Expand Down

0 comments on commit ac105b7

Please sign in to comment.