mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-27 06:27:56 +00:00
Code Activity

fix #2965, fix #2968: bugs in domsimplify on cache usage and boolean trial propagation

Browse source
This commit is contained in:
Nuno Lopes 2020-02-10 10:56:36 +00:00
parent 524434cfbb
commit feba007696
2 changed files with 9 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/tactic/core/dom_simplify_tactic.cpp
View file

@ -238,6 +238,7 @@ expr_ref dom_simplify_tactic::simplify_ite(app * ite) {
r = m.mk_ite(new_c, new_t, new_e); r = m.mk_ite(new_c, new_t, new_e);
} }
} }
reset_cache();
return r; return r;
} }
@ -281,7 +282,12 @@ expr_ref dom_simplify_tactic::simplify_rec(expr * e0) {
if (is_app(e)) { if (is_app(e)) {
m_args.reset(); m_args.reset();
for (expr* arg : *to_app(e)) { for (expr* arg : *to_app(e)) {
m_args.push_back(simplify_arg(arg)); // we don't have a way to distinguish between e.g.
// ite(c, f(c), foo) (which should go to ite(c, f(true), foo))
// from and(or(x, y), f(x)), where we do a "trial" with x=false
// Trials are good for boolean formula simplification but not sound
// for fn applications.
m_args.push_back(m.is_bool(arg) ? arg : simplify_arg(arg));
} }
r = m.mk_app(to_app(e)->get_decl(), m_args.size(), m_args.c_ptr()); r = m.mk_app(to_app(e)->get_decl(), m_args.size(), m_args.c_ptr());
} }

1
src/tactic/core/dom_simplify_tactic.h
View file

@ -114,6 +114,7 @@ class dom_simplify_tactic : public tactic {
expr_ref get_cached(expr* t) { expr* r = nullptr; if (!m_result.find(t, r)) r = t; return expr_ref(r, m); } expr_ref get_cached(expr* t) { expr* r = nullptr; if (!m_result.find(t, r)) r = t; return expr_ref(r, m); }
void cache(expr *t, expr* r) { m_result.insert(t, r); m_trail.push_back(r); } void cache(expr *t, expr* r) { m_result.insert(t, r); m_trail.push_back(r); }
void reset_cache() { m_result.reset(); }
ptr_vector<expr> const & tree(expr * e); ptr_vector<expr> const & tree(expr * e);
expr* idom(expr *e) const { return m_dominators.idom(e); } expr* idom(expr *e) const { return m_dominators.idom(e); }