From 4e55f0494212272be80a7242505b1821811b7b13 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 5 Oct 2014 10:41:37 -0700 Subject: [PATCH] use more efficient encoding of shift operations Signed-off-by: Nikolaj Bjorner --- .../bit_blaster/bit_blaster_tpl_def.h | 101 ++++++++++++------ 1 file changed, 71 insertions(+), 30 deletions(-) diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h index b41aa2238..b579d698e 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h +++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h @@ -911,18 +911,34 @@ void bit_blaster_tpl::mk_shl(unsigned sz, expr * const * a_bits, expr * con out_bits.push_back(a_bits[i]); } else { - expr_ref_vector eqs(m()); - mk_eqs(sz, b_bits, eqs); - for (unsigned i = 0; i < sz; i++) { + out_bits.append(sz, a_bits); + + unsigned i = 0; + expr_ref_vector new_out_bits(m()); + for (; i < sz; ++i) { checkpoint(); - expr_ref out(m()); - mk_ite(eqs.get(i), a_bits[0], m().mk_false(), out); - for (unsigned j = 1; j <= i; j++) { + unsigned shift_i = 1 << i; + if (shift_i >= sz) break; + for (unsigned j = 0; j < sz; ++j) { expr_ref new_out(m()); - mk_ite(eqs.get(i - j), a_bits[j], out, new_out); - out = new_out; + expr* a_j = m().mk_false(); + if (shift_i <= j) a_j = out_bits[j-shift_i].get(); + 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); + new_out_bits.reset(); + } + expr_ref is_large(m()); + is_large = m().mk_false(); + for (; i < sz; ++i) { + mk_or(is_large, b_bits[i], is_large); + } + for (unsigned j = 0; j < sz; ++j) { + expr_ref new_out(m()); + mk_ite(is_large, m().mk_false(), out_bits[j].get(), new_out); + out_bits[j] = new_out; } } } @@ -939,19 +955,32 @@ void bit_blaster_tpl::mk_lshr(unsigned sz, expr * const * a_bits, expr * co out_bits.push_back(m().mk_false()); } else { - expr_ref_vector eqs(m()); - mk_eqs(sz, b_bits, eqs); - out_bits.resize(sz); - for (unsigned i = 0; i < sz; i++) { + out_bits.append(sz, a_bits); + unsigned i = 0; + for (; i < sz; ++i) { checkpoint(); - expr_ref out(m()); - mk_ite(eqs.get(i), a_bits[sz-1], m().mk_false(), out); - for (unsigned j = 1; j <= i; j++) { + expr_ref_vector new_out_bits(m()); + unsigned shift_i = 1 << i; + if (shift_i >= sz) break; + for (unsigned j = 0; j < sz; ++j) { expr_ref new_out(m()); - mk_ite(eqs.get(i - j), a_bits[sz - j - 1], out, new_out); - out = new_out; + expr* a_j = m().mk_false(); + if (shift_i + j < sz) a_j = out_bits[j+shift_i].get(); + mk_ite(b_bits[i], a_j, out_bits[j].get(), new_out); + new_out_bits.push_back(new_out); } - out_bits.set(sz - i - 1, out); + out_bits.reset(); + out_bits.append(new_out_bits); + } + expr_ref is_large(m()); + is_large = m().mk_false(); + for (; i < sz; ++i) { + mk_or(is_large, b_bits[i], is_large); + } + for (unsigned j = 0; j < sz; ++j) { + expr_ref new_out(m()); + mk_ite(is_large, m().mk_false(), out_bits[j].get(), new_out); + out_bits[j] = new_out; } } } @@ -968,20 +997,32 @@ void bit_blaster_tpl::mk_ashr(unsigned sz, expr * const * a_bits, expr * co out_bits.push_back(a_bits[sz-1]); } else { - expr_ref_vector eqs(m()); - mk_eqs(sz, b_bits, eqs); - out_bits.resize(sz); - for (unsigned i = 0; i < sz; i++) { + out_bits.append(sz, a_bits); + unsigned i = 0; + for (; i < sz; ++i) { checkpoint(); - expr_ref out(m()); - out = a_bits[sz-1]; - for (unsigned j = 1; j <= i; j++) { + expr_ref_vector new_out_bits(m()); + unsigned shift_i = 1 << i; + if (shift_i >= sz) break; + for (unsigned j = 0; j < sz; ++j) { expr_ref new_out(m()); - mk_ite(eqs.get(i - j), a_bits[sz - j - 1], out, new_out); - out = new_out; + expr* a_j = a_bits[sz-1]; + if (shift_i + j < sz) a_j = out_bits[j+shift_i].get(); + mk_ite(b_bits[i], a_j, out_bits[j].get(), new_out); + new_out_bits.push_back(new_out); } - TRACE("bit_blaster", tout << (sz - i - 1) << " :\n" << mk_pp(out, m()) << "\n";); - out_bits.set(sz - i - 1, out); + out_bits.reset(); + out_bits.append(new_out_bits); + } + expr_ref is_large(m()); + is_large = m().mk_false(); + for (; i < sz; ++i) { + mk_or(is_large, b_bits[i], is_large); + } + for (unsigned j = 0; j < sz; ++j) { + expr_ref new_out(m()); + mk_ite(is_large, a_bits[sz-1], out_bits[j].get(), new_out); + out_bits[j] = new_out; } } }