mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

enable ranges for bit-vectors

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-08-13 10:53:37 -07:00
parent 72d140334f
commit c63ad2e834
7 changed files with 84 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/smt/smt_arith_value.cpp
View file

@ -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);

4
src/smt/smt_arith_value.h
View file

@ -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);

4
src/smt/smt_context.h
View file

@ -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.

45
src/smt/theory_bv.cpp
View file

@ -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);

3
src/smt/theory_bv.h
View file

@ -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;

8
src/smt/watch_list.h
View file

@ -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);

13
src/util/rational.h
View file

@ -173,6 +173,7 @@ public:
return *this;
}
rational & operator*=(rational const & r) {
m().mul(m_val, r.m_val, m_val);
return *this;
@ -188,6 +189,18 @@ public:
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);