mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

bv_bounds: simplify negated expressions as well

Browse source
This commit is contained in:
Nuno Lopes 2016-02-17 19:14:02 +00:00
parent 16ced7cda5
commit 8718c1c99f
1 changed files with 5 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -49,6 +49,7 @@ struct interval {
SASSERT(sz == b.sz); SASSERT(sz == b.sz);
return l == b.l && h == b.h; return l == b.l && h == b.h;
} }
bool operator!=(const interval& b) const { return !(*this == b); }
bool implies(const interval& b) const { bool implies(const interval& b) const {
if (b.is_full()) if (b.is_full())
@ -182,6 +183,9 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier {
v = lhs; v = lhs;
return true; return true;
} }
} else if (m.is_not(e, lhs)) {
if (is_bound(lhs, v, b))
return b.negate(b);
} }
return false; return false;
} }
@ -223,9 +227,7 @@ 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) { } else if (intr.l == intr.h && intr != b) {
// no improvement in range; do nothing
} 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)) {
result = m.mk_true(); result = m.mk_true();