From eea33841068d71e45d79e93e32aeb7d3eb8dde12 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 15 Jan 2013 16:35:36 -0800 Subject: [PATCH] Add lazy normalization for algebraic extension values. Increase default max_precision to 128. Signed-off-by: Leonardo de Moura --- src/math/realclosure/rcf.pyg | 4 +++- src/math/realclosure/realclosure.cpp | 35 +++++++++++++++++++++++++--- 2 files changed, 35 insertions(+), 4 deletions(-) diff --git a/src/math/realclosure/rcf.pyg b/src/math/realclosure/rcf.pyg index a394ae32a..36c13035b 100644 --- a/src/math/realclosure/rcf.pyg +++ b/src/math/realclosure/rcf.pyg @@ -5,4 +5,6 @@ def_module_params('rcf', ('clean_denominators', BOOL, True, "clean denominators before root isolation"), ('initial_precision', UINT, 24, "a value k that is the initial interval size (as 1/2^k) when creating transcendentals and approximated division"), ('inf_precision', UINT, 24, "a value k that is the initial interval size (i.e., (0, 1/2^l)) used as an approximation for infinitesimal values"), - ('max_precision', UINT, 64, "during sign determination we switch from interval arithmetic to complete methods when the interval size is less than 1/2^k, where k is the max_precision"))) + ('max_precision', UINT, 128, "during sign determination we switch from interval arithmetic to complete methods when the interval size is less than 1/2^k, where k is the max_precision"), + ('lazy_algebraic_normalization', BOOL, True, "during sturm-seq and square-free polynomial computations, only normalize algebraic polynomial expressions when the definining polynomial is monic") + )) diff --git a/src/math/realclosure/realclosure.cpp b/src/math/realclosure/realclosure.cpp index 8f9697d98..50737a97b 100644 --- a/src/math/realclosure/realclosure.cpp +++ b/src/math/realclosure/realclosure.cpp @@ -378,11 +378,13 @@ namespace realclosure { unsigned m_inf_precision; //!< 2^m_inf_precision is used as the lower bound of oo and -2^m_inf_precision is used as the upper_bound of -oo scoped_mpbq m_plus_inf_approx; // lower bound for binary rational intervals used to approximate an infinite positive value scoped_mpbq m_minus_inf_approx; // upper bound for binary rational intervals used to approximate an infinite negative value - + bool m_lazy_algebraic_normalization; // Tracing unsigned m_exec_depth; + bool m_in_aux_values; // True if we are computing SquareFree polynomials or Sturm sequences. That is, the values being computed will be discarded. + volatile bool m_cancel; struct scoped_polynomial_seq { @@ -495,6 +497,8 @@ namespace realclosure { m_exec_depth = 0; + m_in_aux_values = false; + m_cancel = false; updt_params(p); @@ -723,6 +727,7 @@ namespace realclosure { m_ini_precision = p.initial_precision(); m_inf_precision = p.inf_precision(); m_max_precision = p.max_precision(); + m_lazy_algebraic_normalization = p.lazy_algebraic_normalization(); bqm().power(mpbq(2), m_inf_precision, m_plus_inf_approx); bqm().set(m_minus_inf_approx, m_plus_inf_approx); bqm().neg(m_minus_inf_approx); @@ -3454,6 +3459,10 @@ namespace realclosure { return p.size() > 0 && is_rational_one(p[p.size() - 1]); } + bool is_monic(polynomial const & p) { + return p.size() > 0 && is_rational_one(p[p.size() - 1]); + } + /** \brief Force the leading coefficient of p to be 1. */ @@ -3589,6 +3598,7 @@ namespace realclosure { Store in r the square free factors of p. */ void square_free(unsigned sz, value * const * p, value_ref_buffer & r) { + flet set(m_in_aux_values, true); if (sz <= 1) { r.append(sz, p); } @@ -3616,6 +3626,8 @@ namespace realclosure { */ void sturm_seq_core(scoped_polynomial_seq & seq) { INC_DEPTH(); + flet set(m_in_aux_values, true); + SASSERT(seq.size() >= 2); TRACE("rcf_sturm_seq", unsigned sz = seq.size(); @@ -3788,6 +3800,8 @@ namespace realclosure { \brief Evaluate the sign of p(b) by computing a value object. */ int expensive_eval_sign_at(unsigned n, value * const * p, mpbq const & b) { + flet set(m_in_aux_values, true); + SASSERT(n > 1); SASSERT(p[n - 1] != 0); // Actually, given b = c/2^k, we compute the sign of (2^k)^n*p(c) @@ -4877,7 +4891,13 @@ namespace realclosure { */ void normalize_algebraic(algebraic * x, unsigned sz1, value * const * p1, value_ref_buffer & new_p1) { polynomial const & p = x->p(); - rem(sz1, p1, p.size(), p.c_ptr(), new_p1); + if (!m_lazy_algebraic_normalization || !m_in_aux_values || is_monic(p)) { + rem(sz1, p1, p.size(), p.c_ptr(), new_p1); + } + else { + new_p1.reset(); + new_p1.append(sz1, p1); + } } /** @@ -5693,7 +5713,16 @@ namespace realclosure { } void display_poly(std::ostream & out, unsigned n, value * const * p) const { - display_polynomial(out, n, p, display_free_var_proc(), false); + collect_algebraic_refs c; + for (unsigned i = 0; i < n; i++) + c.mark(p[i]); + display_polynomial(out, n, p, display_free_var_proc(), true); + std::sort(c.m_found.begin(), c.m_found.end(), rank_lt_proc()); + for (unsigned i = 0; i < c.m_found.size(); i++) { + algebraic * ext = c.m_found[i]; + out << "\n r!" << ext->idx() << " := "; + display_algebraic_def(out, ext, true); + } } void display_ext(std::ostream & out, extension * r, bool compact) const {