From 1a7d39f9a0b6e6146128ddf349e394b250341a09 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 10 Jan 2013 12:09:07 -0800 Subject: [PATCH] Add refine_algebraic_interval Signed-off-by: Leonardo de Moura --- src/math/realclosure/realclosure.cpp | 62 +++++++++++++++++++++++++++- 1 file changed, 60 insertions(+), 2 deletions(-) diff --git a/src/math/realclosure/realclosure.cpp b/src/math/realclosure/realclosure.cpp index 1e9b1ee1a..5dd229fbf 100644 --- a/src/math/realclosure/realclosure.cpp +++ b/src/math/realclosure/realclosure.cpp @@ -3184,9 +3184,67 @@ namespace realclosure { } } + bool refine_algebraic_interval(algebraic * a, unsigned prec) { + if (a->sdt() != 0) { + // we can't bisect the interval, since it contains more than one root. + return false; + } + else { + mpbqi & a_i = a->interval(); + SASSERT(!a_i.lower_is_inf() && !a_i.upper_is_inf()); + int lower_sign = INT_MIN; + while (!check_precision(a_i, prec)) { + checkpoint(); + SASSERT(!bqm().eq(a_i.lower(), a_i.upper())); + scoped_mpbq m(bqm()); + bqm().add(a_i.lower(), a_i.upper(), m); + bqm().div2(m); + int mid_sign = eval_sign_at(a->p().size(), a->p().c_ptr(), m); + if (mid_sign == 0) { + // found the actual root + // set interval [m, m] + set_lower(a_i, m, false); + set_upper(a_i, m, false); + return true; + } + else { + SASSERT(mid_sign == 1 || mid_sign == -1); + if (lower_sign == INT_MIN) { + // initialize lower_sign + lower_sign = eval_sign_at(a->p().size(), a->p().c_ptr(), a_i.lower()); + } + SASSERT(lower_sign == 1 || lower_sign == -1); + if (mid_sign == lower_sign) { + // improved lower bound + set_lower(a_i, m); + } + else { + // improved upper bound + set_upper(a_i, m); + } + } + } + return true; + } + } + bool refine_algebraic_interval(rational_function_value * v, unsigned prec) { - // TODO - return false; + SASSERT(v->ext()->is_algebraic()); + polynomial const & n = v->num(); + polynomial const & d = v->den(); + unsigned _prec = prec; + while (true) { + if (!refine_coeffs_interval(n, _prec) || + !refine_coeffs_interval(d, _prec) || + !refine_algebraic_interval(to_algebraic(v->ext()), _prec)) + return false; + + update_rf_interval(v, prec); + TRACE("rcf_algebraic", tout << "after update_rf_interval: " << magnitude(v->interval()) << " "; bqim().display(tout, v->interval()); tout << std::endl;); + if (check_precision(v->interval(), prec)) + return true; + _prec++; + } } /**