mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

fix bit-vector rotation left bug

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-06-08 12:46:23 +01:00
parent 88bd01bc4f
commit 8ef4ec7009
3 changed files with 12 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
View file

@ -323,6 +323,9 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
result_pr = 0;
TRACE("bit_blaster", tout << f->get_name() << " ";
for (unsigned i = 0; i < num; ++i) tout << mk_pp(args[i], m()) << " ";
tout << "\n";);
if (num == 0 && f->get_family_id() == null_family_id && butil().is_bv_sort(f->get_range())) {
mk_const(f, result);
return BR_DONE;

10
src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
View file

@ -828,6 +828,12 @@ void bit_blaster_tpl<Cfg>::mk_eq(unsigned sz, expr * const * a_bits, expr * cons
template<typename Cfg>
void bit_blaster_tpl<Cfg>::mk_rotate_left(unsigned sz, expr * const * a_bits, unsigned n, expr_ref_vector & out_bits) {
TRACE("bit_blaster", tout << n << ": " << sz << " ";
for (unsigned i = 0; i < sz; ++i) {
tout << mk_pp(a_bits[i], m()) << " ";
}
tout << "\n";
);
n = n % sz;
for (unsigned i = sz - n; i < sz; i++)
out_bits.push_back(a_bits[i]);
@ -974,7 +980,7 @@ void bit_blaster_tpl<Cfg>::mk_ashr(unsigned sz, expr * const * a_bits, expr * co
mk_ite(eqs.get(i - j), a_bits[sz - j - 1], out, new_out);
out = new_out;
}
TRACE("bit_blaster_tpl<Cfg>", tout << (sz - i - 1) << " :\n" << mk_pp(out, m()) << "\n";);
TRACE("bit_blaster", tout << (sz - i - 1) << " :\n" << mk_pp(out, m()) << "\n";);
out_bits.set(sz - i - 1, out);
}
}
@ -1004,7 +1010,7 @@ void bit_blaster_tpl<Cfg>::mk_ext_rotate_left_right(unsigned sz, expr * const *
out = a_bits[i];
for (unsigned j = 1; j < sz; j++) {
expr_ref new_out(m());
unsigned src = (Left ? (i - j) : (i + j)) % sz;
unsigned src = (Left ? (sz + i - j) : (i + j)) % sz;
mk_ite(eqs.get(j), a_bits[src], out, new_out);
out = new_out;
}

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

@ -21,6 +21,7 @@ Notes:
#include"poly_rewriter_def.h"
#include"ast_smt2_pp.h"
mk_extract_proc::mk_extract_proc(bv_util & u):
m_util(u),
m_high(0),