From c63ad2e834f3ca101d83556c03fe534c1888d3d9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 13 Aug 2020 10:53:37 -0700 Subject: [PATCH] enable ranges for bit-vectors Signed-off-by: Nikolaj Bjorner --- src/smt/smt_arith_value.cpp | 11 ++++++--- src/smt/smt_arith_value.h | 4 +++- src/smt/smt_context.h | 4 ++++ src/smt/theory_bv.cpp | 45 +++++++++++++++++++++++++++++++++++++ src/smt/theory_bv.h | 3 +++ src/smt/watch_list.h | 8 +++++++ src/util/rational.h | 13 +++++++++++ 7 files changed, 84 insertions(+), 4 deletions(-) diff --git a/src/smt/smt_arith_value.cpp b/src/smt/smt_arith_value.cpp index a5a59f60ff5..3f8e31f2979 100644 --- a/src/smt/smt_arith_value.cpp +++ b/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(th); m_thi = dynamic_cast(th); m_thr = dynamic_cast(th); + m_thb = dynamic_cast(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); diff --git a/src/smt/smt_arith_value.h b/src/smt/smt_arith_value.h index a204cad8c50..d802dcb18ab 100644 --- a/src/smt/smt_arith_value.h +++ b/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); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index cf06b485802..e4e46f77b64 100644 --- a/src/smt/smt_context.h +++ b/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. diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 3ff3c23f6cc..cfc75d0c6c1 100644 --- a/src/smt/theory_bv.cpp +++ b/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); diff --git a/src/smt/theory_bv.h b/src/smt/theory_bv.h index 8d01071ff73..1f309331d4e 100644 --- a/src/smt/theory_bv.h +++ b/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; diff --git a/src/smt/watch_list.h b/src/smt/watch_list.h index 0344ad74d99..e974ea51c35 100644 --- a/src/smt/watch_list.h +++ b/src/smt/watch_list.h @@ -144,6 +144,14 @@ namespace smt { literal const * end_literals() const { return reinterpret_cast(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); diff --git a/src/util/rational.h b/src/util/rational.h index d80db5f06c3..c4f96c3c55d 100644 --- a/src/util/rational.h +++ b/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);