mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-18 20:03:38 +00:00
Code Activity

neatify

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-07-05 16:57:41 -07:00
parent f23dc894b4
commit 85c3d874dc
1 changed files with 15 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

21
src/tactic/bv/bv_size_reduction_tactic.cpp
View file

@ -115,12 +115,21 @@ public:
auto match_bitmask = [&](expr* lhs, expr* rhs) { auto match_bitmask = [&](expr* lhs, expr* rhs) {
unsigned lo, hi; unsigned lo, hi;
expr* arg; expr* arg;
if (m_util.is_numeral(rhs, val, bv_sz) && val.is_zero() && m_util.is_extract(lhs, lo, hi, arg) && lo > 0 && hi + 1 == m_util.get_bv_size(arg) && is_uninterp_const(arg) ) { if (!m_util.is_numeral(rhs, val, bv_sz))
val = rational::power_of_two(lo - 1) -1 ; return false;
update_unsigned_upper(to_app(arg), val); if (!val.is_zero())
return true; return false;
} if (!m_util.is_extract(lhs, lo, hi, arg))
return false; return false;
if (lo == 0)
return false;
if (hi + 1 != m_util.get_bv_size(arg))
return false;
if (!is_uninterp_const(arg))
return false;
val = rational::power_of_two(lo - 1) -1 ;
update_unsigned_upper(to_app(arg), val);
return true;
}; };
for (unsigned i = 0; i < sz; i++) { for (unsigned i = 0; i < sz; i++) {