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

add contextual simplification to bv-bounds-tactic

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-01-24 17:49:48 -08:00
parent 6c9358ce41
commit f100d2f4de
2 changed files with 48 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/simplifiers/bound_simplifier.cpp
View file

@ -72,11 +72,13 @@ br_status bound_simplifier::reduce_app(func_decl* f, unsigned num_args, expr* co
return BR_FAILED; return BR_FAILED;
if (N > hi && lo >= 0) { if (N > hi && lo >= 0) {
result = x; result = x;
TRACE("propagate-ineqs", tout << expr_ref(m.mk_app(f, num_args, args), m) << " -> " << result << "\n");
return BR_DONE; return BR_DONE;
} }
if (2 * N > hi && lo >= N) { if (2 * N > hi && lo >= N) {
result = a.mk_sub(x, a.mk_int(N)); result = a.mk_sub(x, a.mk_int(N));
m_rewriter(result); m_rewriter(result);
TRACE("propagate-ineqs", tout << expr_ref(m.mk_app(f, num_args, args), m) << " -> " << result << "\n");
return BR_DONE; return BR_DONE;
} }
IF_VERBOSE(2, verbose_stream() << "potentially missed simplification: " << mk_pp(x, m) << " " << lo << " " << hi << " not reduced\n"); IF_VERBOSE(2, verbose_stream() << "potentially missed simplification: " << mk_pp(x, m) << " " << lo << " " << hi << " not reduced\n");

46
src/tactic/bv/bv_bounds_tactic.cpp
View file

@ -266,6 +266,7 @@ namespace {
svector<expr_cnt*> m_bound_exprs; svector<expr_cnt*> m_bound_exprs;
map m_bound; map m_bound;
bool m_propagate_eq = false; bool m_propagate_eq = false;
ptr_vector<expr> m_args;
bv_bounds_base(ast_manager& m):m(m), m_bv(m) {} bv_bounds_base(ast_manager& m):m(m), m_bv(m) {}
@ -390,6 +391,48 @@ namespace {
return expr_ref(m_bv.mk_ule(m_bv.mk_bv_add(t, m_bv.mk_numeral(-lo, s)), m_bv.mk_numeral(hi - lo, s)), m); return expr_ref(m_bv.mk_ule(m_bv.mk_bv_add(t, m_bv.mk_numeral(-lo, s)), m_bv.mk_numeral(hi - lo, s)), m);
} }
//
// use interval information to rewrite sub-terms x to (0 ++ x[hi:0])
// in other words, identify leading 0s.
//
bool zero_patch(expr* t, expr_ref& result) {
if (!is_app(t))
return false;
if (m_bv.is_extract(t))
return false;
m_args.reset();
bool simplified = false;
interval b;
for (expr* arg : *to_app(t)) {
if (!m_bv.is_bv(arg)) {
m_args.push_back(arg);
continue;
}
if (!m_bv.is_extract(arg) && m_bound.find(arg, b)) {
unsigned num_bits = b.hi().get_num_bits();
unsigned bv_size = m_bv.get_bv_size(arg);
if (0 < num_bits && num_bits < bv_size) {
m_args.push_back(m_bv.mk_concat(m_bv.mk_zero(bv_size - num_bits),
m_bv.mk_extract(num_bits - 1, 0, arg)));
simplified = true;
}
else
m_args.push_back(arg);
}
else
m_args.push_back(arg);
}
if (simplified) {
result = m.mk_app(to_app(t)->get_decl(), m_args);
return true;
}
return false;
}
bool simplify_core(expr* t, expr_ref& result) { bool simplify_core(expr* t, expr_ref& result) {
expr* t1; expr* t1;
interval b; interval b;
@ -399,6 +442,9 @@ namespace {
return true; return true;
} }
if (zero_patch(t, result))
return result;
if (!m.is_bool(t)) if (!m.is_bool(t))
return false; return false;