enable ranges for bit-vectors

Signed-off-by: Nikolaj Bjorner <[email protected]>

src/smt/smt_arith_value.cpp

@@ -23,15 +23,17 @@ Revision History:
 namespace smt {
 
     arith_value::arith_value(ast_manager& m): 
-        m_ctx(nullptr), m(m), a(m) {}
+        m_ctx(nullptr), m(m), a(m), b(m) {}
 
     void arith_value::init(context* ctx) {
         m_ctx = ctx;
         family_id afid = a.get_family_id();
+        family_id bfid = b.get_family_id();
         theory* th = m_ctx->get_theory(afid);
         m_tha = dynamic_cast<theory_mi_arith*>(th);
         m_thi = dynamic_cast<theory_i_arith*>(th);
         m_thr = dynamic_cast<theory_lra*>(th);
+        m_thb = dynamic_cast<theory_bv*>(m_ctx->get_theory(bfid));
     }
 
     bool arith_value::get_lo_equiv(expr* e, rational& lo, bool& is_strict) {
@@ -79,6 +81,7 @@ namespace smt {
         if (!m_ctx->e_internalized(e)) return false;
         is_strict = false;
         enode* n = m_ctx->get_enode(e);
+        if (b.is_bv(e) && m_thb) return m_thb->get_upper(n, up);
         if (m_tha) return m_tha->get_upper(n, up, is_strict);
         if (m_thi) return m_thi->get_upper(n, up, is_strict);
         if (m_thr) return m_thr->get_upper(n, up, is_strict);
@@ -90,6 +93,7 @@ namespace smt {
         if (!m_ctx->e_internalized(e)) return false;
         is_strict = false;
         enode* n = m_ctx->get_enode(e);
+        if (b.is_bv(e) && m_thb) return m_thb->get_lower(n, up);
         if (m_tha) return m_tha->get_lower(n, up, is_strict);
         if (m_thi) return m_thi->get_lower(n, up, is_strict);
         if (m_thr) return m_thr->get_lower(n, up, is_strict);
@@ -101,6 +105,7 @@ namespace smt {
         if (!m_ctx->e_internalized(e)) return false;
         expr_ref _val(m);
         enode* n = m_ctx->get_enode(e);
+        if (m_thb && b.is_bv(e)) return m_thb->get_value(n, _val);
         if (m_tha && m_tha->get_value(n, _val) && a.is_numeral(_val, val)) return true;
         if (m_thi && m_thi->get_value(n, _val) && a.is_numeral(_val, val)) return true;
         if (m_thr && m_thr->get_value(n, val)) return true;
@@ -128,7 +133,7 @@ namespace smt {
     expr_ref arith_value::get_lo(expr* e) const {
         rational lo;
         bool s = false;
-        if (a.is_int_real(e) && get_lo(e, lo, s) && !s) {
+        if ((a.is_int_real(e) || b.is_bv(e)) && get_lo(e, lo, s) && !s) {
             return expr_ref(a.mk_numeral(lo, m.get_sort(e)), m);
         }
         return expr_ref(e, m);
@@ -137,7 +142,7 @@ namespace smt {
     expr_ref arith_value::get_up(expr* e) const {
         rational up;
         bool s = false;
-        if (a.is_int_real(e) && get_up(e, up, s) && !s) {
+        if ((a.is_int_real(e) || b.is_bv(e)) && get_up(e, up, s) && !s) {
             return expr_ref(a.mk_numeral(up, m.get_sort(e)), m);
         }
         return expr_ref(e, m);

src/smt/smt_arith_value.h

@@ -23,16 +23,18 @@ Revision History:
 #include "smt/smt_context.h"
 #include "smt/theory_lra.h"
 #include "smt/theory_arith.h"
-
+#include "smt/theory_bv.h"
 
 namespace smt {
     class arith_value {
         context* m_ctx;        
         ast_manager& m;
         arith_util a;
+        bv_util    b;
         theory_mi_arith* m_tha;
         theory_i_arith*  m_thi;
         theory_lra*      m_thr;
+        theory_bv*       m_thb;
     public:
         arith_value(ast_manager& m);
         void init(context* ctx);

src/smt/smt_context.h

@@ -376,6 +376,10 @@ namespace smt {
             return m_assigned_literals;
         }
 
+        watch_list const& get_watch(literal l) const {
+            return m_watches[l.index()];
+        }
+
         lbool get_assignment(expr * n) const;
 
         // Similar to get_assignment, but returns l_undef if n is not internalized.

src/smt/theory_bv.cpp

@@ -1641,6 +1641,51 @@ namespace smt {
         // SASSERT(check_zero_one_bits(v2));
     }
 
+    bool theory_bv::get_lower(enode* n, rational& value) {
+        theory_var v = n->get_th_var(get_id());
+        if (v != null_theory_var && is_bv(v)) {
+            value = 0;
+            rational p(1);
+            for (literal bit : m_bits[v]) {
+                switch (ctx.get_assignment(bit)) {
+                case l_true:
+                    value += p;
+                    break;
+                default:
+                    break;
+                }
+                p *= 2;
+            }
+            return true;
+        }
+        return false;
+    }
+
+    bool theory_bv::get_upper(enode* n, rational& value) {
+        theory_var v = n->get_th_var(get_id());
+        if (v != null_theory_var && is_bv(v)) {
+            literal_vector const & bits = m_bits[v];
+            rational p = rational::power_of_two(bits.size());
+            value = p - 1;
+            p /= 2;
+            for (unsigned i = bits.size(); i-- > 0; ) {
+                switch (ctx.get_assignment(bits[i])) {
+                case l_false:
+                    value -= p;
+                    break;
+                case l_true:
+                    break;
+                default: {                 
+                    break;
+                }
+                }
+                p /= 2;
+            }
+            return true;
+        }
+        return false;
+    }
+
     void theory_bv::init_model(model_generator & mg) {
         m_factory = alloc(bv_factory, m);
         mg.register_factory(m_factory);

src/smt/theory_bv.h

@@ -265,6 +265,9 @@ namespace smt {
         void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) { SASSERT(check_zero_one_bits(r1)); }
         void unmerge_eh(theory_var v1, theory_var v2);
 
+        bool get_lower(enode* n, rational& v);
+        bool get_upper(enode* n, rational& v);
+
         void display_var(std::ostream & out, theory_var v) const;
         void display_bit_atom(std::ostream & out, bool_var v, bit_atom const * a) const;
         void display_atoms(std::ostream & out) const;

src/smt/watch_list.h

@@ -144,6 +144,14 @@ namespace smt {
         literal const * end_literals() const {
             return reinterpret_cast<literal const *>(m_data + end_lits());
         }
+
+        class literal_iterator { 
+            watch_list const& w;
+        public:
+            literal_iterator(watch_list const& w): w(w) {}
+            literal const* begin() const { return w.begin_literals(); }
+            literal const* end() const { return w.end_literals(); }
+        };
 
         literal * find_literal(literal const & l) {
             return std::find(begin_literals(), end_literals(), l);

src/util/rational.h

@@ -173,6 +173,7 @@ class rational {
         return *this; 
     }
 
+
     rational & operator*=(rational const & r) {
         m().mul(m_val, r.m_val, m_val);
         return *this; 
@@ -188,6 +189,18 @@ class rational {
         return *this; 
     }    
 
+    rational & operator%=(int v) {
+        return *this %= rational(v);
+    }    
+
+    rational & operator/=(int v) {
+        return *this /= rational(v);
+    }    
+
+    rational & operator*=(int v) {
+        return *this *= rational(v);
+    }    
+
     friend inline rational div(rational const & r1, rational const & r2) {
         rational r;
         rational::m().idiv(r1.m_val, r2.m_val, r.m_val);