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

draft rewrite

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-05-16 12:43:20 -07:00
parent 843b6cf149
commit 937afbf95b
1 changed files with 19 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1337,6 +1337,25 @@ br_status bv_rewriter::mk_bv_smod_core(expr * arg1, expr * arg2, bool hi_div0, e
return BR_REWRITE2;
}
#if 0
expr* a = nullptr, *b = nullptr;
if (r2.is_pos() &&
r2.get_num_bits() + 1 < bv_size &&
m_util.is_bv_mul(arg1, a, b) &&
!m_util.is_concat(a) &&
!m_util.is_concat(b)) {
unsigned nb = r2.get_num_bits();
expr_ref a1(m_util.mk_bv_smod(a, arg2), m());
expr_ref a2(m_util.mk_bv_smod(b, arg2), m());
a1 = m_util.mk_concat( mk_numeral(0, bv_size - nb), m_mk_extract(nb-1,0,a1));
a2 = m_util.mk_concat( mk_numeral(0, bv_size - nb), m_mk_extract(nb-1,0,a2));
result = m_util.mk_bv_mul(a1, a2);
std::cout << result << "\n";
result = m_util.mk_bv_smod(result, arg2);
return BR_REWRITE_FULL;
}
#endif
}
if (hi_div0) {