From c8908e81aab78ddc87d17282e647c9a2fc49fa47 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 2 Oct 2019 16:59:35 -0700 Subject: [PATCH] fix #2609 fix #2610 Signed-off-by: Nikolaj Bjorner --- src/math/polynomial/polynomial.cpp | 41 ++++++++++++++---------------- src/math/polynomial/polynomial.h | 2 +- 2 files changed, 20 insertions(+), 23 deletions(-) diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp index 17b688235..8d4755e82 100644 --- a/src/math/polynomial/polynomial.cpp +++ b/src/math/polynomial/polynomial.cpp @@ -374,10 +374,10 @@ namespace polynomial { 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) { out << "1"; - return; + return out; } for (unsigned i = 0; i < m_size; i++) { if (i > 0) { @@ -390,6 +390,7 @@ namespace polynomial { if (degree(i) > 1) out << "^" << degree(i); } + return out; } 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(), tout << "monomials leaked\n"; for (auto * m : m_monomials) { - m->display(tout); tout << "\n"; + m->display(tout << m->id() << " " << m->ref_count() << " ") << "\n"; }); SASSERT(m_monomials.empty()); if (m_own_allocator) @@ -1044,7 +1045,7 @@ namespace polynomial { return div_core(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()) return false; if (m1 == m2) { @@ -1513,10 +1514,10 @@ namespace polynomial { 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()) { out << "0"; - return; + return out; } for (unsigned i = 0; i < m_size; i++) { @@ -1552,6 +1553,7 @@ namespace polynomial { m(i)->display(out, proc, use_star); } } + return out; } 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_mgcd_iterpolators.flush(); m_mgcd_skeletons.reset(); - DEBUG_CODE({ - TRACE("polynomial", - tout << "leaked polynomials\n"; - for (unsigned i = 0; i < m_polynomials.size(); i++) { - if (m_polynomials[i] != nullptr) { - m_polynomials[i]->display(tout, m_manager); - tout << "\n"; - } - }); - m_polynomials.reset(); - }); + CTRACE("polynomial", !m_polynomials.empty(), + tout << "leaked polynomials\n"; + for (auto* p : m_polynomials) { + if (p) p->display(tout, m_manager) << "\n"; + }); + m_polynomials.reset(); SASSERT(m_polynomials.empty()); m_iccp_ZpX_buffers.clear(); m_monomial_manager->dec_ref(); @@ -2655,7 +2652,7 @@ namespace polynomial { 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); } @@ -5151,7 +5148,7 @@ namespace polynomial { } monomial const * m_r = R.m(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)); 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"; }); @@ -5188,7 +5185,7 @@ namespace polynomial { } monomial const * m_r = R.m(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); 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"; @@ -6048,7 +6045,7 @@ namespace polynomial { return true; } monomial * m = C.m(curr_max); - monomial * m_i; + monomial_ref m_i(pm()); if (!div(m, m1, m_i)) { // m1 does not divide maximal monomial of C. R.reset(); @@ -7088,7 +7085,7 @@ namespace polynomial { 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); } diff --git a/src/math/polynomial/polynomial.h b/src/math/polynomial/polynomial.h index 169ee8273..0aa3f5db5 100644 --- a/src/math/polynomial/polynomial.h +++ b/src/math/polynomial/polynomial.h @@ -644,7 +644,7 @@ namespace polynomial { /** \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.