mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Code Activity

bv_bounds: make may_simplify more precise to skip exprs with just 1 bound expr

Browse source 
speedups up to 3x in selected benchmarks
This commit is contained in:
Nuno Lopes 2016-03-01 11:31:08 +00:00
parent 33431ef922
commit 62e46aacd9
1 changed files with 42 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -164,7 +164,7 @@ struct undo_bound {
class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier {
typedef obj_map<expr, interval> map;
typedef obj_map<expr, bool> expr_set;
typedef obj_map<expr, expr_set*> expr_list_map;
typedef obj_map<expr, unsigned> expr_cnt;
ast_manager& m;
params_ref m_params;
@ -172,8 +172,8 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier {
bv_util m_bv;
vector<undo_bound> m_scopes;
map m_bound;
expr_list_map m_expr_vars;
expr_set m_bound_exprs;
svector<expr_set*> m_expr_vars;
svector<expr_cnt*> m_bound_exprs;
bool is_number(expr *e, uint64& n, unsigned& sz) const {
rational r;
@ -233,7 +233,9 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier {
}
expr_set* get_expr_vars(expr* t) {
expr_set*& entry = m_expr_vars.insert_if_not_there2(t, 0)->get_data().m_value;
unsigned id = t->get_id();
m_expr_vars.reserve(id + 1);
expr_set*& entry = m_expr_vars[id];
if (entry)
return entry;
@ -256,23 +258,33 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier {
return set;
}
bool expr_has_bounds(expr* t) {
bool has_bounds = false;
if (m_bound_exprs.find(t, has_bounds))
return has_bounds;
expr_cnt* get_expr_bounds(expr* t) {
unsigned id = t->get_id();
m_bound_exprs.reserve(id + 1);
expr_cnt*& entry = m_bound_exprs[id];
if (entry)
return entry;
expr_cnt* set = alloc(expr_cnt);
entry = set;
if (!is_app(t))
return set;
interval b;
expr* e;
if (is_bound(t, e, b)) {
set->insert_if_not_there2(e, 0)->get_data().m_value++;
}
app* a = to_app(t);
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)))) {
has_bounds = true;
for (unsigned i = 0; i < a->get_num_args(); ++i) {
expr_cnt* set_arg = get_expr_bounds(a->get_arg(i));
for (expr_cnt::iterator I = set_arg->begin(), E = set_arg->end(); I != E; ++I) {
set->insert_if_not_there2(I->m_key, 0)->get_data().m_value += I->m_value;
}
}
for (unsigned i = 0; !has_bounds && i < a->get_num_args(); ++i) {
has_bounds = expr_has_bounds(a->get_arg(i));
}
m_bound_exprs.insert(t, has_bounds);
return has_bounds;
return set;
}
public:
@ -289,8 +301,11 @@ public:
}
virtual ~bv_bounds_simplifier() {
for (expr_list_map::iterator I = m_expr_vars.begin(), E = m_expr_vars.end(); I != E; ++I) {
dealloc(I->m_value);
for (unsigned i = 0, e = m_expr_vars.size(); i < e; ++i) {
dealloc(m_expr_vars[i]);
}
for (unsigned i = 0, e = m_bound_exprs.size(); i < e; ++i) {
dealloc(m_bound_exprs[i]);
}
}
@ -393,7 +408,13 @@ public:
if (is_bound(t, t1, b)) {
return b.is_full() || m_bound.contains(t1);
}
return expr_has_bounds(t);
expr_cnt* bounds = get_expr_bounds(t);
for (expr_cnt::iterator I = bounds->begin(), E = bounds->end(); I != E; ++I) {
if (I->m_value > 1 || m_bound.contains(I->m_key))
return true;
}
return false;
}
virtual void pop(unsigned num_scopes) {