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

@@ -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<expr, interval> map;
+    typedef obj_map<expr, bool> expr_set;
+    typedef obj_map<expr, expr_set*> 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<map>  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;
+        interval b;
-        result = 0;
-        bool sign = false;
 
+        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();

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)) {
+        if (is_cached(t, r) || m_simp->simplify(t, r)) {
-            SASSERT(r.get() != 0);
-            return;
-        }
-        if (is_cached(t, r)) {
             SASSERT(r.get() != 0);
             return;
         }

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;