mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

simplify based on comment from Jamie Sharp #5512

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-08-28 17:07:58 -07:00
parent e5a2f08cc9
commit 4f064ee5d6
1 changed files with 6 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -199,10 +199,6 @@ void bit_blaster_tpl<Cfg>::mk_multiplier(unsigned sz, expr * const * a_bits, exp
SASSERT(sz == out_bits.size()); SASSERT(sz == out_bits.size());
return; return;
} }
if (mk_const_case_multiplier(sz, b_bits, a_bits, out_bits)) {
SASSERT(sz == out_bits.size());
return;
}
out_bits.reset(); out_bits.reset();
#if 0 #if 0
static unsigned counter = 0; static unsigned counter = 0;
@ -1120,16 +1116,14 @@ bool bit_blaster_tpl<Cfg>::mk_const_case_multiplier(unsigned sz, expr * const *
unsigned case_size = 1; unsigned case_size = 1;
unsigned circuit_size = sz*sz*5; unsigned circuit_size = sz*sz*5;
for (unsigned i = 0; case_size < circuit_size && i < sz; ++i) { for (unsigned i = 0; case_size < circuit_size && i < sz; ++i) {
if (!is_bool_const(a_bits[i])) { if (!is_bool_const(a_bits[i]))
case_size *= 2; case_size *= 2;
} if (!is_bool_const(b_bits[i]))
if (!is_bool_const(b_bits[i])) {
case_size *= 2; case_size *= 2;
}
} }
if (case_size >= circuit_size) { if (case_size >= circuit_size)
return false; return false;
}
SASSERT(out_bits.empty()); SASSERT(out_bits.empty());
ptr_buffer<expr, 128> na_bits; ptr_buffer<expr, 128> na_bits;
na_bits.append(sz, a_bits); na_bits.append(sz, a_bits);