mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-26 14:07:54 +00:00
Code Activity

#7673

Browse source 
perf fix
This commit is contained in:
Nikolaj Bjorner 2025-06-12 15:16:28 -07:00
parent e018b024c5
commit a15e4ad1e3
1 changed files with 17 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -993,16 +993,27 @@ void bit_blaster_tpl<Cfg>::mk_ext_rotate_left_right(unsigned sz, expr * const *
for (unsigned j = 0; j < sz; ++j) for (unsigned j = 0; j < sz; ++j)
out_bits.push_back(a_bits[j]); out_bits.push_back(a_bits[j]);
expr_ref_vector out(m()); 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));
};
for (unsigned i = 0, p = 1; i < sz; ++i) { for (unsigned i = 0, p = 1; i < sz; ++i) {
auto bit_i = b_bits[i]; auto bit_i = b_bits[i];
// rotate by p if bit_i is set. // rotate by p if bit_i is set.
out.reset();
for (unsigned j = 0; j < sz; ++j) { if (!m().is_false(bit_i)) {
unsigned src = (Left ? (sz + j - p) : (j + p)) % sz; out.reset();
out.push_back(m().mk_ite(bit_i, out_bits.get(src), out_bits.get(j))); 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)));
}
out_bits.reset();
out_bits.append(out);
} }
out_bits.reset();
out_bits.append(out);
p *= 2; p *= 2;
if (is_power_of_two(sz) && sz == p) if (is_power_of_two(sz) && sz == p)
break; break;