mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2016-02-01 07:51:26 -08:00
parent 995a2e1a29 cc6769c866
commit fe6799699c
1 changed files with 8 additions and 1 deletions

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

@ -743,7 +743,14 @@ void bit_blaster_tpl<Cfg>::mk_srem(unsigned sz, expr * const * a_bits, expr * co
mk_abs(sz, a_bits, abs_a_bits);
mk_abs(sz, b_bits, abs_b_bits);
expr_ref_vector urem_bits(m());
mk_urem(sz, abs_a_bits.c_ptr(), abs_b_bits.c_ptr(), urem_bits);
numeral n_b;
unsigned shift;
// a urem 2^n -> a & ((2^n)-1)
if (is_numeral(sz, abs_b_bits.c_ptr(), n_b) && n_b.is_power_of_two(shift)) {
mk_zero_extend(shift, abs_a_bits.c_ptr(), sz - shift, urem_bits);
} else {
mk_urem(sz, abs_a_bits.c_ptr(), abs_b_bits.c_ptr(), urem_bits);
}
expr_ref_vector neg_urem_bits(m());
mk_neg(sz, urem_bits.c_ptr(), neg_urem_bits);
mk_multiplexer(a_msb, sz, neg_urem_bits.c_ptr(), urem_bits.c_ptr(), out_bits);