mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-06 11:20:26 +00:00
Code Activity

bv_bounds: fix intersection of wrapped intervals

Browse source 
e.g., [117, 115] /\ [115, 113] -> [115, 113]
This commit is contained in:
Nuno Lopes 2016-02-17 15:41:12 +00:00
parent 98a92b9255
commit ac20d8bc11
1 changed files with 13 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/tactic/bv/bv_bounds_tactic.cpp
View file

@ -45,6 +45,11 @@ struct interval {
bool is_full() const { return l.is_zero() && h == uMaxInt(sz); } bool is_full() const { return l.is_zero() && h == uMaxInt(sz); }
bool is_wrapped() const { return l > h; } bool is_wrapped() const { return l > h; }
bool operator==(const interval& b) const {
SASSERT(sz == b.sz);
return l == b.l && h == b.h;
}
bool implies(const interval& b) const { bool implies(const interval& b) const {
if (b.is_full()) if (b.is_full())
return true; return true;
@ -77,9 +82,9 @@ struct interval {
if (is_wrapped()) { if (is_wrapped()) {
if (b.is_wrapped()) { if (b.is_wrapped()) {
if (h > b.l) { if (h >= b.l) {
result = b; result = b;
} else if (b.h > l) { } else if (b.h >= l) {
result = *this; result = *this;
} else { } else {
result = interval(std::max(l, b.l), std::min(h, b.h), sz); result = interval(std::max(l, b.l), std::min(h, b.h), sz);
@ -194,6 +199,10 @@ public:
virtual ~bv_bounds_simplifier() {} virtual ~bv_bounds_simplifier() {}
virtual void assert_expr(expr * t, bool sign) { virtual void assert_expr(expr * t, bool sign) {
while (m.is_not(t, t)) {
sign = !sign;
}
interval b; interval b;
expr* t1; expr* t1;
if (is_bound(t, t1, b)) { if (is_bound(t, t1, b)) {
@ -215,6 +224,8 @@ public:
if (m_bound->find(t1, ctx)) { if (m_bound->find(t1, ctx)) {
if (!b.intersect(ctx, intr)) { if (!b.intersect(ctx, intr)) {
result = m.mk_false(); result = m.mk_false();
} else if (intr == b) {
// no improvement in range; do nothing
} else if (intr.l == intr.h) { } else if (intr.l == intr.h) {
result = m.mk_eq(t1, m_bv.mk_numeral(intr.l, m.get_sort(t1))); result = m.mk_eq(t1, m_bv.mk_numeral(intr.l, m.get_sort(t1)));
} else if (ctx.implies(b)) { } else if (ctx.implies(b)) {