mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

change implementation of shl to use log(n)*n intermediary bits instead of n^2/2

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-10-02 09:07:39 -07:00
parent bb15ddbf15
commit 504709f0a1
1 changed files with 13 additions and 10 deletions
Show stats 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

@ -911,18 +911,21 @@ void bit_blaster_tpl<Cfg>::mk_shl(unsigned sz, expr * const * a_bits, expr * con
out_bits.push_back(a_bits[i]); out_bits.push_back(a_bits[i]);
} }
else { else {
expr_ref_vector eqs(m()); out_bits.append(sz, a_bits);
mk_eqs(sz, b_bits, eqs); expr_ref_vector new_out_bits(m());
for (unsigned i = 0; i < sz; i++) {
checkpoint(); for (unsigned i = 0; i < sz; ++i) {
expr_ref out(m()); unsigned shift_i = 1 << i;
mk_ite(eqs.get(i), a_bits[0], m().mk_false(), out); for (unsigned j = 0; j < sz; ++j) {
for (unsigned j = 1; j <= i; j++) {
expr_ref new_out(m()); expr_ref new_out(m());
mk_ite(eqs.get(i - j), a_bits[j], out, new_out); expr* a_j = m().mk_false();
out = new_out; if (shift_i <= j) a_j = a_bits[j-shift_i];
mk_ite(b_bits[i], a_j, out_bits[j].get(), new_out);
new_out_bits.push_back(new_out);
} }
out_bits.push_back(out); out_bits.reset();
out_bits.append(new_out_bits);
if (shift_i > sz) break;
} }
} }
} }