mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-07 19:51:22 +00:00
Code Activity

use more efficient encoding of shift operations

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-10-05 10:41:37 -07:00
parent 6a3f75822d
commit 4e55f04942
1 changed files with 71 additions and 30 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -911,18 +911,34 @@ 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);
for (unsigned i = 0; i < sz; i++) { unsigned i = 0;
expr_ref_vector new_out_bits(m());
for (; i < sz; ++i) {
checkpoint(); checkpoint();
expr_ref out(m()); unsigned shift_i = 1 << i;
mk_ite(eqs.get(i), a_bits[0], m().mk_false(), out); if (shift_i >= sz) break;
for (unsigned j = 1; j <= i; j++) { for (unsigned j = 0; j < sz; ++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 = 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<Cfg>::mk_lshr(unsigned sz, expr * const * a_bits, expr * co
out_bits.push_back(m().mk_false()); out_bits.push_back(m().mk_false());
} }
else { else {
expr_ref_vector eqs(m()); out_bits.append(sz, a_bits);
mk_eqs(sz, b_bits, eqs); unsigned i = 0;
out_bits.resize(sz); for (; i < sz; ++i) {
for (unsigned i = 0; i < sz; i++) {
checkpoint(); checkpoint();
expr_ref out(m()); expr_ref_vector new_out_bits(m());
mk_ite(eqs.get(i), a_bits[sz-1], m().mk_false(), out); unsigned shift_i = 1 << i;
for (unsigned j = 1; j <= i; j++) { if (shift_i >= sz) break;
for (unsigned j = 0; j < sz; ++j) {
expr_ref new_out(m()); expr_ref new_out(m());
mk_ite(eqs.get(i - j), a_bits[sz - j - 1], out, new_out); expr* a_j = m().mk_false();
out = new_out; 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<Cfg>::mk_ashr(unsigned sz, expr * const * a_bits, expr * co
out_bits.push_back(a_bits[sz-1]); out_bits.push_back(a_bits[sz-1]);
} }
else { else {
expr_ref_vector eqs(m()); out_bits.append(sz, a_bits);
mk_eqs(sz, b_bits, eqs); unsigned i = 0;
out_bits.resize(sz); for (; i < sz; ++i) {
for (unsigned i = 0; i < sz; i++) {
checkpoint(); checkpoint();
expr_ref out(m()); expr_ref_vector new_out_bits(m());
out = a_bits[sz-1]; unsigned shift_i = 1 << i;
for (unsigned j = 1; j <= i; j++) { if (shift_i >= sz) break;
for (unsigned j = 0; j < sz; ++j) {
expr_ref new_out(m()); expr_ref new_out(m());
mk_ite(eqs.get(i - j), a_bits[sz - j - 1], out, new_out); expr* a_j = a_bits[sz-1];
out = new_out; 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.reset();
out_bits.set(sz - i - 1, out); 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;
} }
} }
} }