mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

fix #2609 fix #2610

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-10-02 16:59:35 -07:00
parent feff1f7f96
commit c8908e81aa
2 changed files with 20 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

41
src/math/polynomial/polynomial.cpp
View file

@ -374,10 +374,10 @@ namespace polynomial {
return y; return y;
} }
void display(std::ostream & out, display_var_proc const & proc = display_var_proc(), bool use_star = false) const { std::ostream& display(std::ostream & out, display_var_proc const & proc = display_var_proc(), bool use_star = false) const {
if (m_size == 0) { if (m_size == 0) {
out << "1"; out << "1";
return; return out;
} }
for (unsigned i = 0; i < m_size; i++) { for (unsigned i = 0; i < m_size; i++) {
if (i > 0) { if (i > 0) {
@ -390,6 +390,7 @@ namespace polynomial {
if (degree(i) > 1) if (degree(i) > 1)
out << "^" << degree(i); out << "^" << degree(i);
} }
return out;
} }
void display_smt2(std::ostream & out, display_var_proc const & proc = display_var_proc()) const { void display_smt2(std::ostream & out, display_var_proc const & proc = display_var_proc()) const {
@ -795,7 +796,7 @@ namespace polynomial {
CTRACE("polynomial", !m_monomials.empty(), CTRACE("polynomial", !m_monomials.empty(),
tout << "monomials leaked\n"; tout << "monomials leaked\n";
for (auto * m : m_monomials) { for (auto * m : m_monomials) {
m->display(tout); tout << "\n"; m->display(tout << m->id() << " " << m->ref_count() << " ") << "\n";
}); });
SASSERT(m_monomials.empty()); SASSERT(m_monomials.empty());
if (m_own_allocator) if (m_own_allocator)
@ -1044,7 +1045,7 @@ namespace polynomial {
return div_core<false>(m1->size(), m1->get_powers(), m2->size(), m2->get_powers(), m_tmp1); return div_core<false>(m1->size(), m1->get_powers(), m2->size(), m2->get_powers(), m_tmp1);
} }
bool div(monomial const * m1, monomial const * m2, monomial * & r) { bool div(monomial const * m1, monomial const * m2, monomial_ref & r) {
if (m1->total_degree() < m2->total_degree()) if (m1->total_degree() < m2->total_degree())
return false; return false;
if (m1 == m2) { if (m1 == m2) {
@ -1513,10 +1514,10 @@ namespace polynomial {
bool is_zero() const { return m_size == 0; } bool is_zero() const { return m_size == 0; }
void display(std::ostream & out, mpzzp_manager & nm, display_var_proc const & proc = display_var_proc(), bool use_star = false) const { std::ostream& display(std::ostream & out, mpzzp_manager & nm, display_var_proc const & proc = display_var_proc(), bool use_star = false) const {
if (is_zero()) { if (is_zero()) {
out << "0"; out << "0";
return; return out;
} }
for (unsigned i = 0; i < m_size; i++) { for (unsigned i = 0; i < m_size; i++) {
@ -1552,6 +1553,7 @@ namespace polynomial {
m(i)->display(out, proc, use_star); m(i)->display(out, proc, use_star);
} }
} }
return out;
} }
static void display_num_smt2(std::ostream & out, mpzzp_manager & nm, numeral const & a) { static void display_num_smt2(std::ostream & out, mpzzp_manager & nm, numeral const & a) {
@ -2366,17 +2368,12 @@ namespace polynomial {
m_manager.del(m_zero_numeral); m_manager.del(m_zero_numeral);
m_mgcd_iterpolators.flush(); m_mgcd_iterpolators.flush();
m_mgcd_skeletons.reset(); m_mgcd_skeletons.reset();
DEBUG_CODE({ CTRACE("polynomial", !m_polynomials.empty(),
TRACE("polynomial", tout << "leaked polynomials\n";
tout << "leaked polynomials\n"; for (auto* p : m_polynomials) {
for (unsigned i = 0; i < m_polynomials.size(); i++) { if (p) p->display(tout, m_manager) << "\n";
if (m_polynomials[i] != nullptr) { });
m_polynomials[i]->display(tout, m_manager); m_polynomials.reset();
tout << "\n";
}
});
m_polynomials.reset();
});
SASSERT(m_polynomials.empty()); SASSERT(m_polynomials.empty());
m_iccp_ZpX_buffers.clear(); m_iccp_ZpX_buffers.clear();
m_monomial_manager->dec_ref(); m_monomial_manager->dec_ref();
@ -2655,7 +2652,7 @@ namespace polynomial {
return mm().div(m1, m2); return mm().div(m1, m2);
} }
bool div(monomial const * m1, monomial const * m2, monomial * & r) { bool div(monomial const * m1, monomial const * m2, monomial_ref & r) {
return mm().div(m1, m2, r); return mm().div(m1, m2, r);
} }
@ -5151,7 +5148,7 @@ namespace polynomial {
} }
monomial const * m_r = R.m(max_R); monomial const * m_r = R.m(max_R);
numeral const & a_r = R.a(max_R); numeral const & a_r = R.a(max_R);
monomial * m_r_q = nullptr; monomial_ref m_r_q(pm());
VERIFY(div(m_r, m_q, m_r_q)); VERIFY(div(m_r, m_q, m_r_q));
TRACE("polynomial", tout << "m_r: "; m_r->display(tout); tout << "\nm_q: "; m_q->display(tout); tout << "\n"; TRACE("polynomial", tout << "m_r: "; m_r->display(tout); tout << "\nm_q: "; m_q->display(tout); tout << "\n";
if (m_r_q) { tout << "m_r_q: "; m_r_q->display(tout); tout << "\n"; }); if (m_r_q) { tout << "m_r_q: "; m_r_q->display(tout); tout << "\n"; });
@ -5188,7 +5185,7 @@ namespace polynomial {
} }
monomial const * m_r = R.m(max_R); monomial const * m_r = R.m(max_R);
numeral const & a_r = R.a(max_R); numeral const & a_r = R.a(max_R);
monomial * m_r_q = nullptr; monomial_ref m_r_q(pm());
bool q_div_r = div(m_r, m_q, m_r_q); bool q_div_r = div(m_r, m_q, m_r_q);
m_r_q_ref = m_r_q; m_r_q_ref = m_r_q;
TRACE("polynomial", tout << "m_r: "; m_r->display(tout); tout << "\nm_q: "; m_q->display(tout); tout << "\n"; TRACE("polynomial", tout << "m_r: "; m_r->display(tout); tout << "\nm_q: "; m_q->display(tout); tout << "\n";
@ -6048,7 +6045,7 @@ namespace polynomial {
return true; return true;
} }
monomial * m = C.m(curr_max); monomial * m = C.m(curr_max);
monomial * m_i; monomial_ref m_i(pm());
if (!div(m, m1, m_i)) { if (!div(m, m1, m_i)) {
// m1 does not divide maximal monomial of C. // m1 does not divide maximal monomial of C.
R.reset(); R.reset();
@ -7088,7 +7085,7 @@ namespace polynomial {
return m_imp->div(m1, m2); return m_imp->div(m1, m2);
} }
bool manager::div(monomial const * m1, monomial const * m2, monomial * & r) { bool manager::div(monomial const * m1, monomial const * m2, monomial_ref & r) {
return m_imp->div(m1, m2, r); return m_imp->div(m1, m2, r);
} }

2
src/math/polynomial/polynomial.h
View file

@ -644,7 +644,7 @@ namespace polynomial {
/** /**
\brief Return true if m2 divides m1, and store the result in r. \brief Return true if m2 divides m1, and store the result in r.
*/ */
bool div(monomial const * m1, monomial const * m2, monomial * & r); bool div(monomial const * m1, monomial const * m2, monomial_ref & r);
/** /**
\brief Newton interpolation algorithm for multivariate polynomials. \brief Newton interpolation algorithm for multivariate polynomials.