mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

port simplifications on bv2int

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-08-28 02:55:50 -07:00
parent 03f263b974
commit 9e4b2a6795
2 changed files with 82 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

79
src/ast/rewriter/bv_rewriter.cpp
View file

@ -1365,13 +1365,88 @@ br_status bv_rewriter::mk_bv2int(expr * arg, expr_ref & result) {
result = m_autil.mk_numeral(v, true);
return BR_DONE;
}
// TODO: add other simplifications
if (m_util.is_concat(arg)) {
if (to_app(arg)->get_num_args() == 0) {
result = m_autil.mk_int(0);
return BR_DONE;
}
expr_ref_vector args(m());
unsigned num_args = to_app(arg)->get_num_args();
for (expr* x : *to_app(arg)) {
args.push_back(m_util.mk_bv2int(x));
}
unsigned sz = get_bv_size(to_app(arg)->get_arg(num_args-1));
for (unsigned i = num_args - 1; i > 0; ) {
expr_ref tmp(m());
--i;
tmp = args[i].get();
tmp = m_autil.mk_mul(m_autil.mk_numeral(power(numeral(2), sz), true), tmp);
args[i] = tmp;
sz += get_bv_size(to_app(arg)->get_arg(i));
}
result = m_autil.mk_add(args.size(), args.c_ptr());
return BR_REWRITE2;
}
if (is_mul_no_overflow(arg)) {
expr_ref_vector args(m());
for (expr* x : *to_app(arg)) args.push_back(m_util.mk_bv2int(x));
result = m_autil.mk_mul(args.size(), args.c_ptr());
return BR_REWRITE2;
}
if (is_add_no_overflow(arg)) {
expr_ref_vector args(m());
for (expr* x : *to_app(arg)) args.push_back(m_util.mk_bv2int(x));
result = m_autil.mk_add(args.size(), args.c_ptr());
return BR_REWRITE2;
}
return BR_FAILED;
}
bool bv_rewriter::is_mul_no_overflow(expr* e) {
if (!m_util.is_bv_mul(e)) return false;
unsigned sz = get_bv_size(e);
unsigned sum = 0;
for (expr* x : *to_app(e)) sum += sz-num_leading_zero_bits(x);
return sum < sz;
}
bool bv_rewriter::is_add_no_overflow(expr* e) {
if (!is_add(e)) return false;
for (expr* x : *to_app(e)) {
if (0 == num_leading_zero_bits(x)) return false;
}
return true;
}
unsigned bv_rewriter::num_leading_zero_bits(expr* e) {
numeral v;
unsigned sz = get_bv_size(e);
if (m_util.is_numeral(e, v)) {
while (v.is_pos()) {
SASSERT(sz > 0);
--sz;
v = div(v, numeral(2));
}
return sz;
}
else if (m_util.is_concat(e)) {
app* a = to_app(e);
unsigned sz1 = get_bv_size(a->get_arg(0));
unsigned nb1 = num_leading_zero_bits(a->get_arg(0));
if (sz1 == nb1) {
nb1 += num_leading_zero_bits(a->get_arg(1));
}
return nb1;
}
return 0;
}
br_status bv_rewriter::mk_concat(unsigned num_args, expr * const * args, expr_ref & result) {
expr_ref_buffer new_args(m());
numeral v1;

5
src/ast/rewriter/bv_rewriter.h
View file

@ -42,6 +42,7 @@ protected:
decl_kind mul_decl_kind() const { return OP_BMUL; }
bool use_power() const { return false; }
decl_kind power_decl_kind() const { UNREACHABLE(); return static_cast<decl_kind>(UINT_MAX); }
public:
bv_rewriter_core(ast_manager & m):m_util(m) {}
};
@ -108,6 +109,10 @@ class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
br_status mk_bv_ashr(expr * arg1, expr * arg2, expr_ref & result);
bool is_minus_one_core(expr * arg) const;
bool is_x_minus_one(expr * arg, expr * & x);
bool is_add_no_overflow(expr* e);
bool is_mul_no_overflow(expr* e);
unsigned num_leading_zero_bits(expr* e);
br_status mk_bv_sdiv_core(expr * arg1, expr * arg2, bool hi_div0, expr_ref & result);
br_status mk_bv_udiv_core(expr * arg1, expr * arg2, bool hi_div0, expr_ref & result);
br_status mk_bv_srem_core(expr * arg1, expr * arg2, bool hi_div0, expr_ref & result);