add outline of bv bounds tactic

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

scripts/mk_project.py

@@ -53,7 +53,7 @@ def init_project_def():
     add_lib('proto_model', ['model', 'simplifier', 'smt_params'], 'smt/proto_model')
     add_lib('smt', ['bit_blaster', 'macros', 'normal_forms', 'cmd_context', 'proto_model',
                     'substitution', 'grobner', 'euclid', 'simplex', 'proof_checker', 'pattern', 'parser_util', 'fpa'])
-    add_lib('bv_tactics', ['tactic', 'bit_blaster'], 'tactic/bv')
+    add_lib('bv_tactics', ['tactic', 'bit_blaster', 'core_tactics'], 'tactic/bv')
     add_lib('fuzzing', ['ast'], 'test/fuzzing')
     add_lib('smt_tactic', ['smt'], 'smt/tactic')
     add_lib('sls_tactic', ['tactic', 'normal_forms', 'core_tactics', 'bv_tactics'], 'tactic/sls')

src/tactic/bv/bv_bounds_tactic.cpp

@@ -0,0 +1,156 @@
+/*++
+Copyright (c) 2016 Microsoft Corporation
+
+Module Name:
+
+    bv_bounds_tactic.cpp
+
+Abstract:
+
+    Contextual bounds simplification tactic.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2016-2-12
+
+
+--*/
+
+#include "bv_bounds_tactic.h"
+#include "ctx_simplify_tactic.h"
+#include "bv_decl_plugin.h"
+
+class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier {
+    ast_manager&            m;
+    bv_util                 m_bv;
+    unsigned_vector         m_scopes;
+    expr_ref_vector         m_trail;
+    unsigned_vector         m_trail_kind;
+    obj_map<expr, rational> m_bound[4];
+
+    obj_map<expr, rational> & sle() { return m_bound[0]; }
+    obj_map<expr, rational> & ule() { return m_bound[1]; }
+    obj_map<expr, rational> & sge() { return m_bound[2]; }
+    obj_map<expr, rational> & uge() { return m_bound[3]; }
+
+    obj_map<expr, rational> & bound(bool lo, bool s) {
+        if (lo) {
+            if (s) return sle(); return ule();
+        }
+        else {
+            if (s) return sge(); return uge();
+        }
+    }
+
+    bool is_bound(expr* t, expr*& b, bool& lo, bool& sign, rational& n) {
+        expr* t1, *t2;
+        unsigned sz;
+        if (m_bv.is_bv_ule(t, t1, t2)) {
+            sign = false;
+            if (m_bv.is_numeral(t1, n, sz)) {
+                lo = false; 
+                b = t2;
+                return true;
+            }
+            else if (m_bv.is_numeral(t2, n, sz)) {
+                lo = true;
+                b = t1;
+                return true;
+            }
+        }
+        else if (m_bv.is_bv_sle(t, t1, t2)) {
+            sign = true;
+            if (m_bv.is_numeral(t2, n, sz)) {
+                lo = true;
+                b = t1;
+                return true;
+            }
+            else if (m_bv.is_numeral(t1, n, sz)) {
+                lo = false;
+                b = t2;
+                return true;
+            }
+        }
+        return false;
+    }
+    
+public:
+    bv_bounds_simplifier(ast_manager& m): m(m), m_bv(m), m_trail(m) {}
+
+    virtual ~bv_bounds_simplifier() {}
+
+    virtual void assert_expr(expr * t, bool sign) {
+        bool lo, s;
+        expr* t1;
+        rational n;
+        if (is_bound(t, t1, lo, s, n)) {
+            bound(lo, s).insert(t1, n);
+        }
+    }
+
+    virtual bool simplify(expr* t, expr_ref& result) {
+        bool lo, s;
+        expr* t1;
+        rational b1, b2;
+        if (is_bound(t, t1, lo, s, b1)) {
+            if (bound(!lo, s).find(t1, b2)) {
+                // t1 <= b1 < b2 <= t1
+                if (lo && b2 > b1) {
+                    result = m.mk_false();
+                    return true;
+                }
+                // t1 >= b1 > b2 >= t1
+                if (!lo && b2 < b1) {
+                    result = m.mk_false();
+                    return true;
+                }
+                if (b1 == b2) {
+                    result = m.mk_eq(t1, m_bv.mk_numeral(b1, m.get_sort(t1)));
+                    return true;
+                }
+            }
+            if (bound(lo, s).find(t1, b2)) {
+                // b1 <= b2 <= t1 
+                if (lo && b1 <= b2) {
+                    result = m.mk_true();
+                    return true;
+                }
+                // b1 >= b2 >= t1
+                if (!lo && b1 >= b2) {
+                    result = m.mk_true();
+                    return true;
+                }
+            }
+        }
+        return false;
+    }
+
+    virtual void push() {
+        m_scopes.push_back(m_trail.size());
+    }
+
+    virtual void pop(unsigned num_scopes) {
+        if (num_scopes == 0) return;
+        unsigned old_sz = m_scopes[m_scopes.size() - num_scopes];
+        for (unsigned i = old_sz; i < m_trail.size(); ++i) {
+            m_bound[m_trail_kind[i]].erase(m_trail[i].get());
+        }
+        m_trail_kind.resize(old_sz);
+        m_trail.resize(old_sz);
+        m_scopes.shrink(m_scopes.size() - num_scopes);
+    }
+
+    virtual simplifier * translate(ast_manager & m) {
+        return alloc(bv_bounds_simplifier, m);
+    }
+
+    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));
+}
+

src/tactic/bv/bv_bounds_tactic.h

@@ -0,0 +1,24 @@
+/*++
+Copyright (c) 2016 Microsoft Corporation
+
+Module Name:
+
+    bv_bounds_tactic.h
+
+Abstract:
+
+    Contextual bounds simplification tactic.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2016-2-12
+
+
+--*/
+#ifndef BV_BOUNDS_TACTIC_H_
+#define BV_BOUNDS_TACTIC_H_
+#include "tactic.h"
+
+tactic * mk_bv_bounds_tactic(ast_manager & m, params_ref const & p = params_ref());
+
+#endif