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

Merge branch 'master' of https://github.com/Z3Prover/z3 into jan4

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-01-05 17:45:35 +00:00
parent d176c8714a ee157e47e4
commit 1610e4fbd0
2 changed files with 9 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -171,12 +171,14 @@ void bit_blaster_tpl<Cfg>::mk_multiplier(unsigned sz, expr * const * a_bits, exp
return;
}
#if 1
if (mk_const_multiplier(sz, a_bits, b_bits, out_bits)) {
return;
}
if (mk_const_multiplier(sz, b_bits, a_bits, out_bits)) {
return;
}
#endif
if (!m_use_wtm) {
#if 0
@ -1217,6 +1219,7 @@ void bit_blaster_tpl<Cfg>::mk_const_case_multiplier(bool is_a, unsigned i, unsig
n_a *= n_b;
num2bits(n_a, sz, out_bits);
}
SASSERT(out_bits.size() == sz);
}
template<typename Cfg>
@ -1227,7 +1230,8 @@ bool bit_blaster_tpl<Cfg>::mk_const_multiplier(unsigned sz, expr * const * a_bit
}
SASSERT(out_bits.empty());
if (mk_const_case_multiplier(sz, a_bits, b_bits, out_bits)) {
if (false && mk_const_case_multiplier(sz, a_bits, b_bits, out_bits)) {
SASSERT(sz == out_bits.size());
return true;
}
if (!m_use_bcm) {
@ -1239,7 +1243,7 @@ bool bit_blaster_tpl<Cfg>::mk_const_multiplier(unsigned sz, expr * const * a_bit
out_bits.resize(sz, m().mk_false());
#if 1
bool last=false, now;
bool last = false, now;
for (unsigned i = 0; i < sz; i++) {
now = m().is_true(a_bits[i]);
SASSERT(now || m().is_false(a_bits[i]));
@ -1311,5 +1315,6 @@ bool bit_blaster_tpl<Cfg>::mk_const_multiplier(unsigned sz, expr * const * a_bit
TRACE("bit_blaster_tpl_booth", for (unsigned i=0; i<out_bits.size(); i++)
tout << "Booth encoding: " << mk_pp(out_bits[i].get(), m()) << "\n"; );
SASSERT(out_bits.size() == sz);
return true;
}

4
src/ast/rewriter/bv_rewriter.cpp
View file

@ -2064,12 +2064,12 @@ br_status bv_rewriter::mk_mul_eq(expr * lhs, expr * rhs, expr_ref & result) {
}
}
if (m_util.is_numeral(lhs, c_val, sz) && is_add_mul_const(rhs)) {
unsigned sz = to_app(rhs)->get_num_args();
unsigned num_args = to_app(rhs)->get_num_args();
unsigned i = 0;
expr* c2, *x2;
numeral c2_val, c2_inv_val;
bool found = false;
for (; !found && i < sz; ++i) {
for (; !found && i < num_args; ++i) {
expr* arg = to_app(rhs)->get_arg(i);
if (m_util.is_bv_mul(arg, c2, x2) && m_util.is_numeral(c2, c2_val, sz) &&
m_util.mult_inverse(c2_val, sz, c2_inv_val)) {