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

add disabled pass to detect upper bound range constraints

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-07-05 16:51:05 -07:00
parent a374e2c575
commit f23dc894b4
2 changed files with 78 additions and 43 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -111,6 +111,18 @@ public:
numeral val; numeral val;
unsigned bv_sz; unsigned bv_sz;
expr * f, * lhs, * rhs; expr * f, * lhs, * rhs;
auto match_bitmask = [&](expr* lhs, expr* rhs) {
unsigned lo, hi;
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) ) {
val = rational::power_of_two(lo - 1) -1 ;
update_unsigned_upper(to_app(arg), val);
return true;
}
return false;
};
for (unsigned i = 0; i < sz; i++) { for (unsigned i = 0; i < sz; i++) {
bool negated = false; bool negated = false;
f = g.form(i); f = g.form(i);
@ -152,22 +164,31 @@ public:
else update_signed_lower(to_app(rhs), val); else update_signed_lower(to_app(rhs), val);
} }
} }
#if 0 #if 0
else if (m_util.is_bv_ule(f, lhs, rhs)) { else if (m_util.is_bv_ule(f, lhs, rhs)) {
if (is_uninterp_const(lhs) && m_util.is_numeral(rhs, val, bv_sz)) { if (is_uninterp_const(lhs) && m_util.is_numeral(rhs, val, bv_sz)) {
TRACE("bv_size_reduction", tout << (negated?"not ":"") << mk_ismt2_pp(f, m) << std::endl; ); TRACE("bv_size_reduction", tout << (negated?"not ":"") << mk_ismt2_pp(f, m) << std::endl; );
// v <= k // v <= k
if (negated) update_unsigned_lower(to_app(lhs), val+numeral(1)); if (negated)
else update_unsigned_upper(to_app(lhs), val); update_unsigned_lower(to_app(lhs), val+numeral(1));
else
update_unsigned_upper(to_app(lhs), val);
} }
else if (is_uninterp_const(rhs) && m_util.is_numeral(lhs, val, bv_sz)) { else if (is_uninterp_const(rhs) && m_util.is_numeral(lhs, val, bv_sz)) {
TRACE("bv_size_reduction", tout << (negated?"not ":"") << mk_ismt2_pp(f, m) << std::endl; ); TRACE("bv_size_reduction", tout << (negated?"not ":"") << mk_ismt2_pp(f, m) << std::endl; );
// k <= v // k <= v
if (negated) update_unsigned_upper(to_app(rhs), val-numeral(1)); if (negated)
else update_unsigned_lower(to_app(rhs), val); update_unsigned_upper(to_app(rhs), val-numeral(1));
else
update_unsigned_lower(to_app(rhs), val);
} }
} }
else if (m.is_eq(f, lhs, rhs)) {
if (match_bitmask(lhs, rhs))
continue;
if (match_bitmask(rhs, lhs))
continue;
}
#endif #endif
} }
} }
@ -185,6 +206,7 @@ public:
mc = nullptr; mc = nullptr;
m_mc = nullptr; m_mc = nullptr;
unsigned num_reduced = 0; unsigned num_reduced = 0;
{ {
tactic_report report("reduce-bv-size", g); tactic_report report("reduce-bv-size", g);
collect_bounds(g); collect_bounds(g);
@ -192,26 +214,40 @@ public:
// create substitution // create substitution
expr_substitution subst(m); expr_substitution subst(m);
auto insert_def = [&](app* k, expr* new_def, app* new_const) {
if (!new_def)
return;
subst.insert(k, new_def);
if (m_produce_models) {
if (!m_mc)
m_mc = alloc(bv_size_reduction_mc, m, "bv_size_reduction");
m_mc->add(k, new_def);
if (!m_fmc && new_const)
m_fmc = alloc(generic_model_converter, m, "bv_size_reduction");
if (new_const)
m_fmc->hide(new_const);
}
num_reduced++;
};
if (!(m_signed_lowers.empty() || m_signed_uppers.empty())) { if (!(m_signed_lowers.empty() || m_signed_uppers.empty())) {
TRACE("bv_size_reduction", TRACE("bv_size_reduction",
tout << "m_signed_lowers: " << std::endl; tout << "m_signed_lowers: " << std::endl;
for (obj_map<app, numeral>::iterator it = m_signed_lowers.begin(); it != m_signed_lowers.end(); it++) for (auto const& [k, v] : m_signed_lowers)
tout << mk_ismt2_pp(it->m_key, m) << " >= " << it->m_value.to_string() << std::endl; tout << mk_ismt2_pp(k, m) << " >= " << v.to_string() << std::endl;
tout << "m_signed_uppers: " << std::endl; tout << "m_signed_uppers: " << std::endl;
for (obj_map<app, numeral>::iterator it = m_signed_uppers.begin(); it != m_signed_uppers.end(); it++) for (auto const& [k, v] : m_signed_uppers)
tout << mk_ismt2_pp(it->m_key, m) << " <= " << it->m_value.to_string() << std::endl; tout << mk_ismt2_pp(k, m) << " <= " << v.to_string() << std::endl;
); );
obj_map<app, numeral>::iterator it = m_signed_lowers.begin(); for (auto& [k, val] : m_signed_lowers) {
obj_map<app, numeral>::iterator end = m_signed_lowers.end(); unsigned bv_sz = m_util.get_bv_size(k);
for (; it != end; ++it) { numeral l = m_util.norm(val, bv_sz, true);
app * v = it->m_key; obj_map<app, numeral>::obj_map_entry * entry = m_signed_uppers.find_core(k);
unsigned bv_sz = m_util.get_bv_size(v);
numeral l = m_util.norm(it->m_value, bv_sz, true);
obj_map<app, numeral>::obj_map_entry * entry = m_signed_uppers.find_core(v);
if (entry != nullptr) { if (entry != nullptr) {
numeral u = m_util.norm(entry->get_data().m_value, bv_sz, true); numeral u = m_util.norm(entry->get_data().m_value, bv_sz, true);
TRACE("bv_size_reduction", tout << l << " <= " << v->get_decl()->get_name() << " <= " << u << "\n";); TRACE("bv_size_reduction", tout << l << " <= " << k->get_decl()->get_name() << " <= " << u << "\n";);
expr * new_def = nullptr; expr * new_def = nullptr;
app * new_const = nullptr; app * new_const = nullptr;
if (l > u) { if (l > u) {
@ -219,19 +255,19 @@ public:
return; return;
} }
else if (l == u) { else if (l == u) {
new_def = m_util.mk_numeral(l, v->get_sort()); new_def = m_util.mk_numeral(l, k->get_sort());
} }
else { else {
// l < u // l < u
if (l.is_neg()) { if (l.is_neg()) {
unsigned l_nb = (-l).get_num_bits(); unsigned l_nb = (-l).get_num_bits();
unsigned v_nb = m_util.get_bv_size(v); unsigned v_nb = m_util.get_bv_size(k);
if (u.is_neg()) if (u.is_neg())
{ {
// l <= v <= u <= 0 // l <= v <= u <= 0
unsigned i_nb = l_nb; unsigned i_nb = l_nb;
TRACE("bv_size_reduction", tout << " l <= " << v->get_decl()->get_name() << " <= u <= 0 " << " --> " << i_nb << " bits\n";); TRACE("bv_size_reduction", tout << " l <= " << k->get_decl()->get_name() << " <= u <= 0 " << " --> " << i_nb << " bits\n";);
if (i_nb < v_nb) { if (i_nb < v_nb) {
new_const = m.mk_fresh_const(nullptr, m_util.mk_sort(i_nb)); new_const = m.mk_fresh_const(nullptr, m_util.mk_sort(i_nb));
new_def = m_util.mk_concat(m_util.mk_numeral(numeral(-1), v_nb - i_nb), new_const); new_def = m_util.mk_concat(m_util.mk_numeral(numeral(-1), v_nb - i_nb), new_const);
@ -241,7 +277,7 @@ public:
// l <= v <= 0 <= u // l <= v <= 0 <= u
unsigned u_nb = u.get_num_bits(); unsigned u_nb = u.get_num_bits();
unsigned i_nb = ((l_nb > u_nb) ? l_nb : u_nb) + 1; unsigned i_nb = ((l_nb > u_nb) ? l_nb : u_nb) + 1;
TRACE("bv_size_reduction", tout << " l <= " << v->get_decl()->get_name() << " <= 0 <= u " << " --> " << i_nb << " bits\n";); TRACE("bv_size_reduction", tout << " l <= " << k->get_decl()->get_name() << " <= 0 <= u " << " --> " << i_nb << " bits\n";);
if (i_nb < v_nb) { if (i_nb < v_nb) {
new_const = m.mk_fresh_const(nullptr, m_util.mk_sort(i_nb)); new_const = m.mk_fresh_const(nullptr, m_util.mk_sort(i_nb));
new_def = m_util.mk_sign_extend(v_nb - i_nb, new_const); new_def = m_util.mk_sign_extend(v_nb - i_nb, new_const);
@ -251,8 +287,8 @@ public:
else { else {
// 0 <= l <= v <= u // 0 <= l <= v <= u
unsigned u_nb = u.get_num_bits(); unsigned u_nb = u.get_num_bits();
unsigned v_nb = m_util.get_bv_size(v); unsigned v_nb = m_util.get_bv_size(k);
TRACE("bv_size_reduction", tout << l << " <= " << v->get_decl()->get_name() << " <= " << u << " --> " << u_nb << " bits\n";); TRACE("bv_size_reduction", tout << l << " <= " << k->get_decl()->get_name() << " <= " << u << " --> " << u_nb << " bits\n";);
if (u_nb < v_nb) { if (u_nb < v_nb) {
new_const = m.mk_fresh_const(nullptr, m_util.mk_sort(u_nb)); new_const = m.mk_fresh_const(nullptr, m_util.mk_sort(u_nb));
new_def = m_util.mk_concat(m_util.mk_numeral(numeral(0), v_nb - u_nb), new_const); new_def = m_util.mk_concat(m_util.mk_numeral(numeral(0), v_nb - u_nb), new_const);
@ -260,21 +296,20 @@ public:
} }
} }
if (new_def) { insert_def(k, new_def, new_const);
subst.insert(v, new_def);
if (m_produce_models) {
if (!m_mc)
m_mc = alloc(bv_size_reduction_mc, m, "bv_size_reduction");
m_mc->add(v, new_def);
if (!m_fmc && new_const)
m_fmc = alloc(generic_model_converter, m, "bv_size_reduction");
if (new_const)
m_fmc->hide(new_const);
}
num_reduced++;
} }
} }
} }
for (auto const& [k, v] : m_unsigned_uppers) {
unsigned shift;
unsigned bv_sz = m_util.get_bv_size(k);
numeral u = m_util.norm(v, bv_sz, true) + 1;
if (u.is_power_of_two(shift) && shift < bv_sz) {
app* new_const = m.mk_fresh_const(nullptr, m_util.mk_sort(shift));
expr* new_def = m_util.mk_concat(m_util.mk_numeral(numeral(0), bv_sz - shift), new_const);
insert_def(k, new_def, new_const);
}
} }
#if 0 #if 0

2
src/util/rational.h
View file

@ -343,7 +343,7 @@ public:
static rational power_of_two(unsigned k); static rational power_of_two(unsigned k);
bool is_power_of_two(unsigned & shift) { bool is_power_of_two(unsigned & shift) const {
return m().is_power_of_two(m_val, shift); return m().is_power_of_two(m_val, shift);
} }