From c693c990df9e2babb34b5e4b8e0e09b1513dd65d Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 25 Feb 2016 16:53:35 +0000 Subject: [PATCH] bv_bounds: speedup up to 10x in larger formulas introduce a may_simplify() function to short-circuit evaluation of expression trees that are guaranteed to not be simplifiable --- src/tactic/bv/bv_bounds_tactic.cpp | 88 +++++++++++++++++++++---- src/tactic/core/ctx_simplify_tactic.cpp | 8 +-- src/tactic/core/ctx_simplify_tactic.h | 1 + 3 files changed, 80 insertions(+), 17 deletions(-) diff --git a/src/tactic/bv/bv_bounds_tactic.cpp b/src/tactic/bv/bv_bounds_tactic.cpp index 587b9df9a..122096677 100644 --- a/src/tactic/bv/bv_bounds_tactic.cpp +++ b/src/tactic/bv/bv_bounds_tactic.cpp @@ -34,7 +34,7 @@ struct interval { unsigned sz; bool tight; - explicit interval() : l(0), h(0), sz(0), tight(false) {} + interval() {} interval(const rational& l, const rational& h, unsigned sz, bool tight = false) : l(l), h(h), sz(sz), tight(tight) { // canonicalize full set if (is_wrapped() && l == h + rational::one()) { @@ -51,10 +51,11 @@ struct interval { bool is_full() const { return l.is_zero() && h == uMaxInt(sz); } bool is_wrapped() const { return l > h; } + bool is_singleton() const { return l == h; } bool operator==(const interval& b) const { SASSERT(sz == b.sz); - return l == b.l && h == b.h; + return l == b.l && h == b.h && tight == b.tight; } bool operator!=(const interval& b) const { return !(*this == b); } @@ -79,7 +80,7 @@ struct interval { /// return false if intersection is unsat bool intersect(const interval& b, interval& result) const { - if (is_full() || (l == b.l && h == b.h)) { + if (is_full() || *this == b) { result = b; return true; } @@ -153,6 +154,8 @@ std::ostream& operator<<(std::ostream& o, const interval& I) { class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier { typedef obj_map map; + typedef obj_map expr_set; + typedef obj_map expr_list_map; ast_manager& m; params_ref m_params; @@ -160,11 +163,9 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier { bv_util m_bv; vector m_scopes; map *m_bound; + expr_list_map m_expr_vars; bool is_bound(expr *e, expr*& v, interval& b) { - if (!m.is_bool(e)) - return false; - rational n; expr *lhs, *rhs; unsigned sz; @@ -212,6 +213,45 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier { return false; } + expr_set* get_expr_vars(expr* t) { + expr_set*& entry = m_expr_vars.insert_if_not_there2(t, 0)->get_data().m_value; + if (entry) + return entry; + + expr_set* set = alloc(expr_set); + entry = set; + + if (!m_bv.is_numeral(t)) + set->insert(t, true); + + if (!is_app(t)) + return set; + + app* a = to_app(t); + for (unsigned i = 0; i < a->get_num_args(); ++i) { + expr_set* set_arg = get_expr_vars(a->get_arg(i)); + for (expr_set::iterator I = set_arg->begin(), E = set_arg->end(); I != E; ++I) { + set->insert(I->m_key, true); + } + } + return set; + } + + 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)); + + for (unsigned i = 0; i < a->get_num_args(); ++i) { + if (expr_has_bounds(a->get_arg(i))) + return true; + } + return false; + } + public: bv_bounds_simplifier(ast_manager& m, params_ref const& p) : m(m), m_params(p), m_bv(m) { @@ -229,7 +269,11 @@ public: r.insert("propagate-eq", CPK_BOOL, "(default: false) propagate equalities from inequalities"); } - virtual ~bv_bounds_simplifier() {} + 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); + } + } virtual bool assert_expr(expr * t, bool sign) { while (m.is_not(t, t)) { @@ -253,10 +297,17 @@ public: virtual bool simplify(expr* t, expr_ref& result) { expr* t1; - interval b, ctx, intr; - result = 0; - bool sign = false; + interval b; + if (m_bound->find(t, b) && b.is_singleton()) { + result = m_bv.mk_numeral(b.l, m_bv.get_bv_size(t)); + return true; + } + + if (!m.is_bool(t)) + return false; + + bool sign = false; while (m.is_not(t, t)) { sign = !sign; } @@ -272,12 +323,15 @@ public: } } + interval ctx, intr; + result = 0; + if (m_bound->find(t1, ctx)) { if (ctx.implies(b)) { result = m.mk_true(); } else if (!b.intersect(ctx, intr)) { result = m.mk_false(); - } else if (m_propagate_eq && intr.l == intr.h) { + } else if (m_propagate_eq && intr.is_singleton()) { result = m.mk_eq(t1, m_bv.mk_numeral(intr.l, m.get_sort(t1))); } } else if (b.is_full() && b.tight) { @@ -290,6 +344,18 @@ public: return result != 0; } + virtual bool may_simplify(expr* t) { + if (m_bv.is_numeral(t)) + return false; + + expr_set* used_exprs = get_expr_vars(t); + for (map::iterator I = m_bound->begin(), E = m_bound->end(); I != E; ++I) { + if (I->m_value.is_singleton() && used_exprs->contains(I->m_key)) + return true; + } + return expr_has_bounds(t); + } + virtual void push() { TRACE("bv", tout << "push\n";); unsigned sz = m_scopes.size(); diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp index e07f7417d..f127614aa 100644 --- a/src/tactic/core/ctx_simplify_tactic.cpp +++ b/src/tactic/core/ctx_simplify_tactic.cpp @@ -331,17 +331,13 @@ struct ctx_simplify_tactic::imp { void simplify(expr * t, expr_ref & r) { r = 0; - if (m_depth >= m_max_depth || m_num_steps >= m_max_steps || !is_app(t)) { + if (m_depth >= m_max_depth || m_num_steps >= m_max_steps || !is_app(t) || !m_simp->may_simplify(t)) { r = t; return; } checkpoint(); TRACE("ctx_simplify_tactic_detail", tout << "processing: " << mk_bounded_pp(t, m) << "\n";); - if (m_simp->simplify(t, r)) { - SASSERT(r.get() != 0); - return; - } - if (is_cached(t, r)) { + if (is_cached(t, r) || m_simp->simplify(t, r)) { SASSERT(r.get() != 0); return; } diff --git a/src/tactic/core/ctx_simplify_tactic.h b/src/tactic/core/ctx_simplify_tactic.h index 34258362b..7b1507f67 100644 --- a/src/tactic/core/ctx_simplify_tactic.h +++ b/src/tactic/core/ctx_simplify_tactic.h @@ -30,6 +30,7 @@ public: virtual ~simplifier() {} virtual bool assert_expr(expr * t, bool sign) = 0; virtual bool simplify(expr* t, expr_ref& result) = 0; + virtual bool may_simplify(expr* t) { return true; } virtual void push() = 0; virtual void pop(unsigned num_scopes) = 0; virtual simplifier * translate(ast_manager & m) = 0;