mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 21:53:23 +00:00
Code Activity

Fix bug

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-01-20 18:41:24 -08:00
parent 3344151aca
commit 5d938a5fe2
1 changed files with 38 additions and 30 deletions
Download patch file Download diff file Expand all files Collapse all files

68
src/math/realclosure/realclosure.cpp
View file

@ -4236,45 +4236,53 @@ namespace realclosure {
bool refine_algebraic_interval(algebraic * a, unsigned prec) { bool refine_algebraic_interval(algebraic * a, unsigned prec) {
save_interval_if_too_small(a, prec); save_interval_if_too_small(a, prec);
if (a->sdt() != 0) { 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; return false;
} }
else { else {
mpbqi & a_i = a->interval(); mpbqi & a_i = a->interval();
SASSERT(!a_i.lower_is_inf() && !a_i.upper_is_inf()); if (a_i.lower_is_inf() || a_i.upper_is_inf()) {
int lower_sign = INT_MIN; // we can't bisect the infinite intervals
while (!check_precision(a_i, prec)) { return false;
checkpoint(); }
SASSERT(!bqm().eq(a_i.lower(), a_i.upper())); else {
scoped_mpbq m(bqm()); mpbqi & a_i = a->interval();
bqm().add(a_i.lower(), a_i.upper(), m); SASSERT(!a_i.lower_is_inf() && !a_i.upper_is_inf());
bqm().div2(m); int lower_sign = INT_MIN;
int mid_sign = eval_sign_at(a->p().size(), a->p().c_ptr(), m); while (!check_precision(a_i, prec)) {
if (mid_sign == 0) { checkpoint();
// found the actual root SASSERT(!bqm().eq(a_i.lower(), a_i.upper()));
// set interval [m, m] scoped_mpbq m(bqm());
set_lower(a_i, m, false); bqm().add(a_i.lower(), a_i.upper(), m);
set_upper(a_i, m, false); bqm().div2(m);
return true; int mid_sign = eval_sign_at(a->p().size(), a->p().c_ptr(), m);
} if (mid_sign == 0) {
else { // found the actual root
SASSERT(mid_sign == 1 || mid_sign == -1); // set interval [m, m]
if (lower_sign == INT_MIN) { set_lower(a_i, m, false);
// initialize lower_sign set_upper(a_i, m, false);
lower_sign = eval_sign_at(a->p().size(), a->p().c_ptr(), a_i.lower()); return true;
}
SASSERT(lower_sign == 1 || lower_sign == -1);
if (mid_sign == lower_sign) {
// improved lower bound
set_lower(a_i, m);
} }
else { else {
// improved upper bound SASSERT(mid_sign == 1 || mid_sign == -1);
set_upper(a_i, m); 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;
} }
} }