bail out dominators after log number of steps

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/tactic/bv/bv_bounds_tactic.cpp

@@ -18,6 +18,7 @@ Author:
 
 #include "tactic/bv/bv_bounds_tactic.h"
 #include "tactic/core/ctx_simplify_tactic.h"
+#include "tactic/core/dom_simplify_tactic.h"
 #include "ast/bv_decl_plugin.h"
 #include "ast/ast_pp.h"
 #include <climits>
@@ -105,7 +106,8 @@ struct interval {
                 } else {
                     return b.intersect(*this, result);
                 }
-        } else if (b.is_wrapped()) {
+            } 
+            else if (b.is_wrapped()) {
                 // ... b.h ... l ... h ... b.l ..
                 if (h < b.l && l > b.h) {
                     return false;
@@ -190,7 +192,7 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier {
 
         bool is_bound(expr *e, expr*& v, interval& b) const {
             uint64 n;
-        expr *lhs, *rhs;
+            expr *lhs = 0, *rhs = 0;
             unsigned sz;
 
             if (m_bv.is_bv_ule(e, lhs, rhs)) {
@@ -206,7 +208,8 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier {
                     v = lhs;
                     return true;
                 }
-        } else if (m_bv.is_bv_sle(e, lhs, rhs)) {
+            } 
+            else if (m_bv.is_bv_sle(e, lhs, rhs)) {
                 if (is_number(lhs, n, sz)) { // C sle x <=> x sge C
                     if (m_bv.is_numeral(rhs))
                         return false;
@@ -530,8 +533,322 @@ public:
         }
     };
 
+
+    class dom_bv_bounds_simplifier : public dom_simplifier {
+        typedef obj_map<expr, interval> map;
+        typedef obj_map<expr, bool> expr_set;
+        typedef obj_map<expr, unsigned> expr_cnt;
+
+        ast_manager&       m;
+        params_ref         m_params;
+        bool               m_propagate_eq;
+        bv_util            m_bv;
+        vector<undo_bound> m_scopes;
+        map                m_bound;
+        svector<expr_set*> m_expr_vars;
+        svector<expr_cnt*> m_bound_exprs;
+
+        bool is_number(expr *e, uint64& n, unsigned& sz) const {
+            rational r;
+            if (m_bv.is_numeral(e, r, sz) && sz <= 64) {
+                n = r.get_uint64();
+                return true;
+            }
+            return false;
+        }
+
+        bool is_bound(expr *e, expr*& v, interval& b) const {
+            uint64 n;
+            expr *lhs = 0, *rhs = 0;
+            unsigned sz;
+
+            if (m_bv.is_bv_ule(e, lhs, rhs)) {
+                if (is_number(lhs, n, sz)) { // C ule x <=> x uge C
+                    if (m_bv.is_numeral(rhs))
+                        return false;
+                    b = interval(n, uMaxInt(sz), sz, true);
+                    v = rhs;
+                    return true;
+                }
+                if (is_number(rhs, n, sz)) { // x ule C
+                    b = interval(0, n, sz, true);
+                    v = lhs;
+                    return true;
+                }
+            } 
+            else if (m_bv.is_bv_sle(e, lhs, rhs)) {
+                if (is_number(lhs, n, sz)) { // C sle x <=> x sge C
+                    if (m_bv.is_numeral(rhs))
+                        return false;
+                    b = interval(n, (1ull << (sz-1)) - 1, sz, true);
+                    v = rhs;
+                    return true;
+                }
+                if (is_number(rhs, n, sz)) { // x sle C
+                    b = interval(1ull << (sz-1), n, sz, true);
+                    v = lhs;
+                    return true;
+                }
+            } else if (m.is_eq(e, lhs, rhs)) {
+                if (is_number(lhs, n, sz)) {
+                    if (m_bv.is_numeral(rhs))
+                        return false;
+                    b = interval(n, n, sz, true);
+                    v = rhs;
+                    return true;
+                }
+                if (is_number(rhs, n, sz)) {
+                    b = interval(n, n, sz, true);
+                    v = lhs;
+                    return true;
+                }
+            }
+            return false;
+        }
+
+
+    public:
+        dom_bv_bounds_simplifier(ast_manager& m, params_ref const& p) : m(m), m_params(p), m_bv(m) {
+            updt_params(p);
+        }
+
+        virtual void updt_params(params_ref const & p) {
+            m_propagate_eq = p.get_bool("propagate_eq", false);
+        }
+
+        static void get_param_descrs(param_descrs& r) {
+            r.insert("propagate-eq", CPK_BOOL, "(default: false) propagate equalities from inequalities");
+        }
+
+        virtual ~dom_bv_bounds_simplifier() {
+            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]);
+            }
+        }
+
+        virtual bool assert_expr(expr * t, bool sign) {
+            while (m.is_not(t, t)) {
+                sign = !sign;
+            }
+
+            interval b;
+            expr* t1;
+            if (is_bound(t, t1, b)) {
+                SASSERT(!m_bv.is_numeral(t1));
+                if (sign)
+                    VERIFY(b.negate(b));
+
+                TRACE("bv", tout << (sign?"(not ":"") << mk_pp(t, m) << (sign ? ")" : "") << ": " << mk_pp(t1, m) << " in " << b << "\n";);
+                map::obj_map_entry* e = m_bound.find_core(t1);
+                if (e) {
+                    interval& old = e->get_data().m_value;
+                    interval intr;
+                    if (!old.intersect(b, intr))
+                        return false;
+                    if (old == intr)
+                        return true;
+                    m_scopes.insert(undo_bound(t1, old, false));
+                    old = intr;
+                } else {
+                    m_bound.insert(t1, b);
+                    m_scopes.insert(undo_bound(t1, interval(), true));
+                }
+            }
+            return true;
+        }
+
+        virtual void operator()(expr_ref& r) {
+            expr* t1, * t = r;
+            interval b;
+
+            if (m_bound.find(t, b) && b.is_singleton()) {
+                r = m_bv.mk_numeral(b.l, m_bv.get_bv_size(t));
+                return;
+            }
+
+            if (!m.is_bool(t))
+                return;
+
+            bool sign = false;
+            while (m.is_not(t, t)) {
+                sign = !sign;
+            }
+
+            if (!is_bound(t, t1, b))
+                return;
+
+            if (sign && b.tight) {
+                sign = false;
+                if (!b.negate(b)) {
+                    r = m.mk_false();
+                    return;
+                }
+            }
+
+            interval ctx, intr;
+            bool unchanged = false;
+            if (b.is_full() && b.tight) {
+                r = m.mk_true();
+            } else if (m_bound.find(t1, ctx)) {
+                if (ctx.implies(b)) {
+                    r = m.mk_true();
+                } else if (!b.intersect(ctx, intr)) {
+                    r = m.mk_false();
+                } else if (m_propagate_eq && intr.is_singleton()) {
+                    r = m.mk_eq(t1, m_bv.mk_numeral(rational(intr.l, rational::ui64()),
+                                                    m.get_sort(t1)));
+                }
+            }
+            else {
+                unchanged = true;
+            }
+
+            CTRACE("bv", !unchanged, tout << mk_pp(t, m) << " " << b << " (ctx: " << ctx << ") (intr: " << intr << "): " << r << "\n";);
+            if (sign && unchanged)
+                r = m.mk_not(r);
+        }
+
+        // check if t contains v
+        ptr_vector<expr> todo;
+        bool contains(expr* t, expr* v) {
+            ast_fast_mark1 mark;
+            todo.push_back(t);
+            while (!todo.empty()) {
+                t = todo.back();
+                todo.pop_back();
+                if (mark.is_marked(t)) {
+                    continue;
+                }
+                if (t == v) {
+                    todo.reset();
+                    return true;
+                }
+                mark.mark(t);
+            
+                if (!is_app(t)) {
+                    continue;
+                }
+                app* a = to_app(t);
+                todo.append(a->get_num_args(), a->get_args());
+            }
+            return false;
+        }
+
+        bool contains_bound(expr* t) {
+            ast_fast_mark1 mark1;
+            ast_fast_mark2 mark2;
+
+            todo.push_back(t);
+            while (!todo.empty()) {
+                t = todo.back();
+                todo.pop_back();
+                if (mark1.is_marked(t)) {
+                    continue;
+                }
+                mark1.mark(t);
+            
+                if (!is_app(t)) {
+                    continue;
+                }
+                interval b;
+                expr* e;
+                if (is_bound(t, e, b)) {
+                    if (mark2.is_marked(e)) {
+                        todo.reset();
+                        return true;
+                    }
+                    mark2.mark(e);
+                    if (m_bound.contains(e)) {
+                        todo.reset();
+                        return true;
+                    }
+                }
+
+                app* a = to_app(t);
+                todo.append(a->get_num_args(), a->get_args());
+            }
+            return false;
+        }
+
+        virtual bool may_simplify(expr* t) {
+            if (m_bv.is_numeral(t))
+                return false;
+
+            while (m.is_not(t, t));
+
+            for (auto & v : m_bound) {
+                if (contains(t, v.m_key)) return true;
+            }
+
+#if 0
+            expr_set* used_exprs = get_expr_vars(t);
+            for (map::iterator I = m_bound.begin(), E = m_bound.end(); I != E; ++I) {
+                if (contains(t, I->m_key)) return true;
+                if (I->m_value.is_singleton() && used_exprs->contains(I->m_key))
+                    return true;
+            }
+#endif
+
+            expr* t1;
+            interval b;
+            // skip common case: single bound constraint without any context for simplification
+            if (is_bound(t, t1, b)) {
+                return b.is_full() || m_bound.contains(t1);
+            }
+
+            if (contains_bound(t)) {
+                return true;
+            }
+#if 0
+            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;
+            }
+#endif
+            return false;
+        }
+
+        virtual void pop(unsigned num_scopes) {
+            TRACE("bv", tout << "pop: " << num_scopes << "\n";);
+            if (m_scopes.empty())
+                return;
+            unsigned target = m_scopes.size() - num_scopes;
+            if (target == 0) {
+                m_bound.reset();
+                m_scopes.reset();
+                return;
+            }
+            for (unsigned i = m_scopes.size()-1; i >= target; --i) {
+                undo_bound& undo = m_scopes[i];
+                SASSERT(m_bound.contains(undo.e));
+                if (undo.fresh) {
+                    m_bound.erase(undo.e);
+                } else {
+                    m_bound.insert(undo.e, undo.b);
+                }
+            }
+            m_scopes.shrink(target);
+        }
+
+        virtual dom_simplifier * translate(ast_manager & m) {
+            return alloc(dom_bv_bounds_simplifier, m, m_params);
+        }
+
+        virtual unsigned scope_level() const {
+            return m_scopes.size();
+        }
+    };
+
 }
 
 tactic * mk_bv_bounds_tactic(ast_manager & m, params_ref const & p) {
     return clean(alloc(ctx_simplify_tactic, m, alloc(bv_bounds_simplifier, m, p), p));
 }
+
+tactic * mk_dom_bv_bounds_tactic(ast_manager & m, params_ref const & p) {
+    return clean(alloc(dom_simplify_tactic, m, alloc(dom_bv_bounds_simplifier, m, p), p));
+}

src/tactic/core/dom_simplify_tactic.cpp

@@ -83,11 +83,12 @@ expr* expr_dominators::intersect(expr* x, expr * y) {
     return x;
 }
 
-void expr_dominators::compute_dominators() {
+bool expr_dominators::compute_dominators() {
     expr * e = m_root;
     SASSERT(m_doms.empty());
     m_doms.insert(e, e);
     bool change = true;
+    unsigned iterations = 1;
     while (change) {
         change = false;
         SASSERT(m_post2expr.empty() || m_post2expr.back() == e);
@@ -109,8 +110,13 @@ void expr_dominators::compute_dominators() {
                 change = true;
             }
         }
+        iterations *= 2;        
+        if (change && iterations > m_post2expr.size()) {
+            return false;
         }
     }
+    return true;
+}
 
 void expr_dominators::extract_tree() {
     for (auto const& kv : m_doms) {
@@ -118,17 +124,18 @@ void expr_dominators::extract_tree() {
     }
 }
 
-void expr_dominators::compile(expr * e) {
+bool expr_dominators::compile(expr * e) {
     reset();
     m_root = e;
     compute_post_order();
-    compute_dominators();
+    if (!compute_dominators()) return false;
     extract_tree();
+    return true;
 }
 
-void expr_dominators::compile(unsigned sz, expr * const* es) {
+bool expr_dominators::compile(unsigned sz, expr * const* es) {
     expr_ref e(m.mk_and(sz, es), m);
-    compile(e);
+    return compile(e);
 }
 
 void expr_dominators::reset() {
@@ -293,14 +300,14 @@ expr_ref dom_simplify_tactic::simplify_and_or(bool is_and, app * e) {
 }
 
 
-void dom_simplify_tactic::init(goal& g) {
+bool dom_simplify_tactic::init(goal& g) {
     expr_ref_vector args(m);
     unsigned sz = g.size();
     for (unsigned i = 0; i < sz; ++i) args.push_back(g.form(i));
     expr_ref fml = mk_and(args);
     m_result.reset();
     m_trail.reset();
-    m_dominators.compile(fml);
+    return m_dominators.compile(fml);
 }
 
 void dom_simplify_tactic::simplify_goal(goal& g) {
@@ -312,7 +319,7 @@ void dom_simplify_tactic::simplify_goal(goal& g) {
         change = false;
 
         // go forwards
-        init(g);
+        if (!init(g)) return;
         unsigned sz = g.size();
         for (unsigned i = 0; !g.inconsistent() && i < sz; ++i) {
             expr_ref r = simplify(g.form(i));
@@ -329,7 +336,7 @@ void dom_simplify_tactic::simplify_goal(goal& g) {
         pop(scope_level());
         
         // go backwards
-        init(g);
+        if (!init(g)) return;
         sz = g.size();
         for (unsigned i = sz; !g.inconsistent() && i > 0; ) {
             --i;

src/tactic/core/dom_simplify_tactic.h

@@ -45,14 +45,14 @@ private:
 
     void compute_post_order();
     expr* intersect(expr* x, expr * y);
-    void compute_dominators();
+    bool compute_dominators();
     void extract_tree();
 
 public:
     expr_dominators(ast_manager& m): m(m), m_root(m) {}
 
-    void compile(expr * e);
-    void compile(unsigned sz, expr * const* es);
+    bool compile(expr * e);
+    bool compile(unsigned sz, expr * const* es);
     tree_t const& get_tree() { return m_tree; }
     void reset();
     
@@ -115,7 +115,7 @@ private:
     void pop(unsigned n) { SASSERT(n <= m_scope_level); m_scope_level -= n; m_simplifier->pop(n); }
     bool assert_expr(expr* f, bool sign) { m_scope_level++; return m_simplifier->assert_expr(f, sign); }
 
-    void init(goal& g);
+    bool init(goal& g);
 
 public:
     dom_simplify_tactic(ast_manager & m, dom_simplifier* s, params_ref const & p = params_ref()):