From 5fd3ef6580028fd4d17be1f97eab97a8b4568849 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 23 May 2021 16:50:47 -0700 Subject: [PATCH] na Signed-off-by: Nikolaj Bjorner --- src/math/polysat/fixplex.h | 1 + src/math/polysat/fixplex_def.h | 46 ++++++++++++++++++++++++++-------- 2 files changed, 37 insertions(+), 10 deletions(-) diff --git a/src/math/polysat/fixplex.h b/src/math/polysat/fixplex.h index 35f3ce890..8ca9a239b 100644 --- a/src/math/polysat/fixplex.h +++ b/src/math/polysat/fixplex.h @@ -224,6 +224,7 @@ namespace polysat { void propagate_bounds(ineq const& i); void new_bound(row const& r, var_t x, mod_interval const& range); void new_bound(ineq const& i, var_t x, numeral const& lo, numeral const& hi); + void conflict_bound(ineq const& i); void pivot(var_t x_i, var_t x_j, numeral const& b, numeral const& value); numeral value2delta(var_t v, numeral const& new_value) const; numeral value2error(var_t v, numeral const& new_value) const; diff --git a/src/math/polysat/fixplex_def.h b/src/math/polysat/fixplex_def.h index f64828ab1..aaec6f93a 100644 --- a/src/math/polysat/fixplex_def.h +++ b/src/math/polysat/fixplex_def.h @@ -1082,21 +1082,47 @@ namespace polysat { template void fixplex::propagate_bounds(ineq const& i) { - // v < w => hi(v) < hi(w) - // v < w => lo(v) < lo(w) - // v <= w => hi(v) <= hi(w) - // v <= w => lo(v) <= lo(w) - // TBD: detect conflicts, - // ensure overflow / underflow conditions + // v < w & lo(v) + 1 = 0 -> conflict + // v < w & hi(w) = 0 -> conflict + // v < w & lo(v) >= hi(w) -> conflict + // v <= w & lo(v) > hi(w) -> conflict + // v < w & hi(v) >= hi(w) -> hi(v) := hi(w) - 1 + // v < w & lo(v) >= lo(w) -> lo(w) := lo(v) + 1 + // v <= w & hi(v) > hi(w) -> hi(v) := hi(w) + // v <= w & lo(v) > lo(w) -> lo(w) := lo(w) var_t v = i.v, w = i.w; - if (i.strict && hi(v) >= hi(w)) + bool s = i.strict; + if (s && lo(v) + 1 == 0) + conflict_bound(i); + else if (s && hi(w) == 0) + conflict_bound(i); + else if (s && lo(v) >= hi(w)) + conflict_bound(i); + else if (!s && lo(v) > hi(w)) + conflict_bound(i); + else if (s && hi(v) >= hi(w)) { + SASSERT(lo(v) < hi(w)); + SASSERT(hi(w) != 0); new_bound(i, v, lo(v), hi(w) - 1); - if (i.strict && lo(v) >= lo(w)) + } + else if (s && lo(v) >= lo(w)) { + SASSERT(lo(v) + 1 != 0); + SASSERT(hi(w) > lo(v)); new_bound(i, w, lo(v) + 1, hi(w)); - if (!i.strict && hi(v) > hi(w)) + } + else if (!s && hi(v) > hi(w)) { + SASSERT(lo(v) <= hi(w)); new_bound(i, v, lo(v), hi(w)); - if (!i.strict && lo(v) > lo(w)) + } + else if (!s && lo(v) > lo(w)) { + SASSERT(lo(v) <= hi(w)); new_bound(i, w, lo(v), hi(w)); + } + } + + template + void fixplex::conflict_bound(ineq const& i) { + NOT_IMPLEMENTED_YET(); } template