mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 01:24:08 +00:00
remove unused code
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
4350bd77ac
commit
ac105b7d8c
|
|
@ -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);
|
||||
}
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue