mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity

bv_bounds: make may_simplify() more aggressive for the common case of a single comparison

Browse source 
fix expr_has_bounds to handle cases like (bvadd (ite c t e) ...)
This commit is contained in:
Nuno Lopes 2016-02-25 19:41:01 +00:00
parent 6563e458f0
commit 97d6098d00
1 changed files with 12 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -238,12 +238,10 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier {
}
bool expr_has_bounds(expr* t) {
if (!m.is_bool(t))
return false;
app* a = to_app(t);
if (m_bv.is_bv_ule(t) || m_bv.is_bv_sle(t) || m.is_eq(t))
return m_bv.is_numeral(a->get_arg(0)) ^ m_bv.is_numeral(a->get_arg(1));
if ((m_bv.is_bv_ule(t) || m_bv.is_bv_sle(t) || m.is_eq(t)) &&
(m_bv.is_numeral(a->get_arg(0)) || m_bv.is_numeral(a->get_arg(1))))
return true;
for (unsigned i = 0; i < a->get_num_args(); ++i) {
if (expr_has_bounds(a->get_arg(i)))
@ -353,6 +351,15 @@ public:
if (I->m_value.is_singleton() && used_exprs->contains(I->m_key))
return true;
}
while (m.is_not(t, t));
expr* t1;
interval b;
// skip common case: single bound constraint without any context for simplification
if (is_bound(t, t1, b)) {
return m_bound->contains(t1);
}
return expr_has_bounds(t);
}