From 3344151acaad1ab449e770d642829abd9ec69900 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 20 Jan 2013 18:21:09 -0800 Subject: [PATCH 1/2] Replace # with x in the definition of algebraic elements Signed-off-by: Leonardo de Moura --- src/math/realclosure/realclosure.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/math/realclosure/realclosure.cpp b/src/math/realclosure/realclosure.cpp index fc46c6d5c..a555486e0 100644 --- a/src/math/realclosure/realclosure.cpp +++ b/src/math/realclosure/realclosure.cpp @@ -5797,7 +5797,7 @@ namespace realclosure { struct display_free_var_proc { void operator()(std::ostream & out, bool compact) const { - out << "#"; + out << "x"; } }; From 5d938a5fe290a9f5643cf781a9fc6179d6e58fe9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 20 Jan 2013 18:41:24 -0800 Subject: [PATCH 2/2] Fix bug Signed-off-by: Leonardo de Moura --- src/math/realclosure/realclosure.cpp | 68 ++++++++++++++++------------ 1 file changed, 38 insertions(+), 30 deletions(-) diff --git a/src/math/realclosure/realclosure.cpp b/src/math/realclosure/realclosure.cpp index a555486e0..dac4c8e09 100644 --- a/src/math/realclosure/realclosure.cpp +++ b/src/math/realclosure/realclosure.cpp @@ -4236,45 +4236,53 @@ namespace realclosure { bool refine_algebraic_interval(algebraic * a, unsigned prec) { save_interval_if_too_small(a, prec); if (a->sdt() != 0) { - // we can't bisect the interval, since it contains more than one root. + // We don't bisect the interval, since it contains more than one root. + // To bisect this kind of interval we would have to use Tarski queries. 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); + if (a_i.lower_is_inf() || a_i.upper_is_inf()) { + // we can't bisect the infinite intervals + 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 { - // improved upper bound - set_upper(a_i, m); + 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; } - return true; } }