mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-25 07:13:41 +00:00
Code Activity

Update bit_blaster_tpl_def.h

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-06-12 16:07:28 -07:00
parent a15e4ad1e3
commit a2ad90cba1
1 changed files with 3 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -993,13 +993,7 @@ void bit_blaster_tpl<Cfg>::mk_ext_rotate_left_right(unsigned sz, expr * const *
for (unsigned j = 0; j < sz; ++j)
out_bits.push_back(a_bits[j]);
expr_ref_vector out(m());
auto mk_ite = [&](expr* bit_i, expr* th, expr* el) {
if (m().is_false(bit_i))
return el;
if (m().is_true(bit_i))
return th;
return (expr*)(m().mk_ite(bit_i, th, el));
};
expr_ref tmp(m());
for (unsigned i = 0, p = 1; i < sz; ++i) {
auto bit_i = b_bits[i];
// rotate by p if bit_i is set.
@ -1008,7 +1002,8 @@ void bit_blaster_tpl<Cfg>::mk_ext_rotate_left_right(unsigned sz, expr * const *
out.reset();
for (unsigned j = 0; j < sz; ++j) {
unsigned src = (Left ? (sz + j - p) : (j + p)) % sz;
out.push_back(mk_ite(bit_i, out_bits.get(src), out_bits.get(j)));
mk_ite(bit_i, out_bits.get(src), out_bits.get(j), tmp));
out.push_back(tmp);
}
out_bits.reset();
out_bits.append(out);