From c01f27fe132a762f4ef73ae83e5dbef1dcb88fab Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 6 Jan 2013 10:46:38 -0800 Subject: [PATCH] Add small interval caching infrastructure Signed-off-by: Leonardo de Moura --- src/math/realclosure/realclosure.cpp | 119 +++++++++++++++++++++++++-- src/math/realclosure/realclosure.h | 1 + 2 files changed, 112 insertions(+), 8 deletions(-) diff --git a/src/math/realclosure/realclosure.cpp b/src/math/realclosure/realclosure.cpp index ac0e0cfb0..11b05b6d3 100644 --- a/src/math/realclosure/realclosure.cpp +++ b/src/math/realclosure/realclosure.cpp @@ -149,10 +149,16 @@ namespace realclosure { // --------------------------------- struct value { - unsigned m_ref_count; //!< Reference counter - bool m_rational; //!< True if the value is represented as an abitrary precision rational value. - mpbqi m_interval; //!< approximation as an interval with binary rational end-points - value(bool rat):m_ref_count(0), m_rational(rat) {} + unsigned m_ref_count; //!< Reference counter + bool m_rational; //!< True if the value is represented as an abitrary precision rational value. + mpbqi m_interval; //!< approximation as an interval with binary rational end-points + // When performing an operation OP, we may have to make the width (upper - lower) of m_interval very small. + // The precision (i.e., a small interval) needed for executing OP is usually unnecessary for subsequent operations, + // This unnecessary precision will only slowdown the subsequent operations that do not need it. + // To cope with this issue, we cache the value m_interval in m_old_interval whenever the width of m_interval is below + // a give threshold. Then, after finishing OP, we restore the old_interval. + mpbqi * m_old_interval; + value(bool rat):m_ref_count(0), m_rational(rat), m_old_interval(0) {} bool is_rational() const { return m_rational; } mpbqi const & interval() const { return m_interval; } mpbqi & interval() { return m_interval; } @@ -304,7 +310,7 @@ namespace realclosure { typedef ref_buffer value_ref_buffer; typedef obj_ref value_ref; typedef _scoped_interval scoped_mpqi; - + small_object_allocator * m_allocator; bool m_own_allocator; unsynch_mpq_manager & m_qm; @@ -317,7 +323,12 @@ namespace realclosure { value * m_pi; mk_e_interval m_mk_e_interval; value * m_e; + ptr_vector m_to_restore; //!< Set of values v s.t. v->m_old_interval != 0 + + // Parameters unsigned m_ini_precision; //!< initial precision for transcendentals, infinitesimals, etc. + int m_min_magnitude; + volatile bool m_cancel; struct scoped_polynomial_seq { @@ -380,6 +391,7 @@ namespace realclosure { } ~imp() { + restore_saved_intervals(); // to free memory dec_ref(m_one); dec_ref(m_pi); dec_ref(m_e); @@ -404,6 +416,73 @@ namespace realclosure { return m_one; } + /** + \brief Return the magnitude of the given interval. + The magnitude is an approximation of the size of the interval. + */ + int magnitude(mpbq const & l, mpbq const & u) { + SASSERT(bqm().is_nonneg(l) || bqm().is_nonpos(u)); + int l_k = l.k(); + int u_k = u.k(); + if (l_k == u_k) + return bqm().magnitude_ub(l); + if (bqm().is_nonneg(l)) + return qm().log2(u.numerator()) - qm().log2(l.numerator()) - u_k + l_k - u_k; + else + return qm().mlog2(u.numerator()) - qm().mlog2(l.numerator()) - u_k + l_k - u_k; + } + + /** + \brief Return the magnitude of the given interval. + The magnitude is an approximation of the size of the interval. + */ + int magnitude(mpbqi const & i) { + return magnitude(i.lower(), i.upper()); + } + + /** + \brief Return true if the magnitude of the given interval is less than the parameter m_min_magnitude + */ + bool too_small(mpbqi const & i) { + return magnitude(i) < m_min_magnitude; + } + + /** + \brief Save the current interval (i.e., approximation) of the given value. + */ + void save_interval(value * v) { + if (v->m_old_interval != 0) + return; // interval was already saved. + m_to_restore.push_back(v); + inc_ref(v); + v->m_old_interval = new (allocator()) mpbqi(); + set_interval(*(v->m_old_interval), v->m_interval); + } + + /** + \brief Save the current interval (i.e., approximation) of the given value IF it is too small (i.e., too_small(v) == True). + */ + void save_interval_if_too_small(value * v) { + if (too_small(v->m_interval)) + save_interval(v); + } + + /** + \brief Restore the saved intervals (approximations) of RCF values. + */ + void restore_saved_intervals() { + unsigned sz = m_to_restore.size(); + for (unsigned i = 0; i < sz; i++) { + value * v = m_to_restore[i]; + set_interval(v->m_interval, *(v->m_old_interval)); + bqim().del(*(v->m_old_interval)); + allocator().deallocate(sizeof(mpbqi), v->m_old_interval); + v->m_old_interval = 0; + dec_ref(v); + } + m_to_restore.reset(); + } + void cleanup(extension::kind k) { ptr_vector & exts = m_extensions[k]; // keep removing unused slots @@ -427,7 +506,8 @@ namespace realclosure { } void updt_params(params_ref const & p) { - m_ini_precision = p.get_uint("initial_precision", 24); + m_ini_precision = p.get_uint("initial_precision", 24); + m_min_magnitude = -static_cast(p.get_uint("min_mag", 64)); // TODO } @@ -1526,7 +1606,7 @@ namespace realclosure { SASSERT(num_sz > 0 && den_sz > 0); if (num_sz == 1 && den_sz == 1) { // In this case, the normalization rules guarantee that den is one. - SASSERT(is_one(den[0])); + SASSERT(is_rational_one(den[0])); return num[0]; } rational_function_value * r = mk_rational_function_value_core(a->ext(), num_sz, num, den_sz, den); @@ -1704,7 +1784,7 @@ namespace realclosure { SASSERT(num_sz > 0 && den_sz > 0); if (num_sz == 1 && den_sz == 1) { // In this case, the normalization rules guarantee that den is one. - SASSERT(is_one(den[0])); + SASSERT(is_rational_one(den[0])); return num[0]; } rational_function_value * r = mk_rational_function_value_core(a->ext(), num_sz, num, den_sz, den); @@ -2142,6 +2222,14 @@ namespace realclosure { } }; + // Helper object for restoring the value intervals. + class save_interval_ctx { + manager::imp * m; + public: + save_interval_ctx(manager const * _this):m(_this->m_imp) { SASSERT (m); } + ~save_interval_ctx() { m->restore_saved_intervals(); } + }; + manager::manager(unsynch_mpq_manager & m, params_ref const & p, small_object_allocator * a) { m_imp = alloc(imp, m, p, a); } @@ -2195,6 +2283,7 @@ namespace realclosure { } void manager::isolate_roots(unsigned n, numeral const * as, numeral_vector & roots) { + save_interval_ctx ctx(this); m_imp->isolate_roots(n, as, roots); } @@ -2203,6 +2292,7 @@ namespace realclosure { } int manager::sign(numeral const & a) { + save_interval_ctx ctx(this); return m_imp->sign(a); } @@ -2247,14 +2337,17 @@ namespace realclosure { } void manager::root(numeral const & a, unsigned k, numeral & b) { + save_interval_ctx ctx(this); m_imp->root(a, k, b); } void manager::power(numeral const & a, unsigned k, numeral & b) { + save_interval_ctx ctx(this); m_imp->power(a, k, b); } void manager::add(numeral const & a, numeral const & b, numeral & c) { + save_interval_ctx ctx(this); m_imp->add(a, b, c); } @@ -2265,26 +2358,32 @@ namespace realclosure { } void manager::sub(numeral const & a, numeral const & b, numeral & c) { + save_interval_ctx ctx(this); m_imp->sub(a, b, c); } void manager::mul(numeral const & a, numeral const & b, numeral & c) { + save_interval_ctx ctx(this); m_imp->mul(a, b, c); } void manager::neg(numeral & a) { + save_interval_ctx ctx(this); m_imp->neg(a); } void manager::inv(numeral & a) { + save_interval_ctx ctx(this); m_imp->inv(a); } void manager::div(numeral const & a, numeral const & b, numeral & c) { + save_interval_ctx ctx(this); m_imp->div(a, b, c); } int manager::compare(numeral const & a, numeral const & b) { + save_interval_ctx ctx(this); return m_imp->compare(a, b); } @@ -2333,18 +2432,22 @@ namespace realclosure { } void manager::select(numeral const & prev, numeral const & next, numeral & result) { + save_interval_ctx ctx(this); m_imp->select(prev, next, result); } void manager::display(std::ostream & out, numeral const & a) const { + save_interval_ctx ctx(this); m_imp->display(out, a); } void manager::display_decimal(std::ostream & out, numeral const & a, unsigned precision) const { + save_interval_ctx ctx(this); m_imp->display_decimal(out, a, precision); } void manager::display_interval(std::ostream & out, numeral const & a) const { + save_interval_ctx ctx(this); m_imp->display_interval(out, a); } diff --git a/src/math/realclosure/realclosure.h b/src/math/realclosure/realclosure.h index 151323886..72e0da2aa 100644 --- a/src/math/realclosure/realclosure.h +++ b/src/math/realclosure/realclosure.h @@ -44,6 +44,7 @@ namespace realclosure { public: struct imp; private: + friend class save_interval_ctx; imp * m_imp; public: manager(unsynch_mpq_manager & m, params_ref const & p = params_ref(), small_object_allocator * a = 0);