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

disable caching of simplifier when applied to direct arguments of terms. Caching is only valid when applied to dominator children

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-10-07 00:20:58 +01:00
parent cabdc1f64c
commit 76c309a595
2 changed files with 17 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -101,7 +101,8 @@ bool expr_dominators::compute_dominators() {
expr * child = m_post2expr[i]; expr * child = m_post2expr[i];
ptr_vector<expr> const& p = m_parents[child]; ptr_vector<expr> const& p = m_parents[child];
expr * new_idom = 0, *idom2 = 0; expr * new_idom = 0, *idom2 = 0;
for (auto& pred : p) {
for (expr * pred : p) {
if (m_doms.contains(pred)) { if (m_doms.contains(pred)) {
new_idom = !new_idom ? pred : intersect(new_idom, pred); new_idom = !new_idom ? pred : intersect(new_idom, pred);
} }
@ -209,31 +210,31 @@ expr_ref dom_simplify_tactic::simplify_ite(app * ite) {
expr * c = 0, *t = 0, *e = 0; expr * c = 0, *t = 0, *e = 0;
VERIFY(m.is_ite(ite, c, t, e)); VERIFY(m.is_ite(ite, c, t, e));
unsigned old_lvl = scope_level(); unsigned old_lvl = scope_level();
expr_ref new_c = simplify(c); expr_ref new_c = simplify(c, false);
if (m.is_true(new_c)) { if (m.is_true(new_c)) {
r = simplify(t); r = simplify(t, false);
} }
else if (m.is_false(new_c) || !assert_expr(new_c, false)) { else if (m.is_false(new_c) || !assert_expr(new_c, false)) {
r = simplify(e); r = simplify(e, false);
} }
else { else {
for (expr * child : tree(ite)) { for (expr * child : tree(ite)) {
if (is_subexpr(child, t) && !is_subexpr(child, e)) { if (is_subexpr(child, t) && !is_subexpr(child, e)) {
simplify(child); simplify(child, true);
} }
} }
pop(scope_level() - old_lvl); pop(scope_level() - old_lvl);
expr_ref new_t = simplify(t); expr_ref new_t = simplify(t, false);
if (!assert_expr(new_c, true)) { if (!assert_expr(new_c, true)) {
return new_t; return new_t;
} }
for (expr * child : tree(ite)) { for (expr * child : tree(ite)) {
if (is_subexpr(child, e) && !is_subexpr(child, t)) { if (is_subexpr(child, e) && !is_subexpr(child, t)) {
simplify(child); simplify(child, true);
} }
} }
pop(scope_level() - old_lvl); pop(scope_level() - old_lvl);
expr_ref new_e = simplify(e); expr_ref new_e = simplify(e, false);
if (c == new_c && t == new_t && e == new_e) { if (c == new_c && t == new_t && e == new_e) {
r = ite; r = ite;
} }
@ -248,7 +249,7 @@ expr_ref dom_simplify_tactic::simplify_ite(app * ite) {
return r; return r;
} }
expr_ref dom_simplify_tactic::simplify(expr * e0) { expr_ref dom_simplify_tactic::simplify(expr * e0, bool cache_result) {
expr_ref r(m); expr_ref r(m);
expr* e = 0; expr* e = 0;
@ -272,7 +273,7 @@ expr_ref dom_simplify_tactic::simplify(expr * e0) {
} }
else { else {
for (expr * child : tree(e)) { for (expr * child : tree(e)) {
simplify(child); simplify(child, true);
} }
if (is_app(e)) { if (is_app(e)) {
m_args.reset(); m_args.reset();
@ -288,7 +289,7 @@ expr_ref dom_simplify_tactic::simplify(expr * e0) {
} }
} }
(*m_simplifier)(r); (*m_simplifier)(r);
cache(e0, r); if (cache_result) cache(e0, r);
TRACE("simplify", tout << "depth: " << m_depth << " " << mk_pp(e0, m) << " -> " << r << "\n";); TRACE("simplify", tout << "depth: " << m_depth << " " << mk_pp(e0, m) << " -> " << r << "\n";);
--m_depth; --m_depth;
m_subexpr_cache.reset(); m_subexpr_cache.reset();
@ -315,10 +316,10 @@ expr_ref dom_simplify_tactic::simplify_and_or(bool is_and, app * e) {
#define _SIMP_ARG(arg) \ #define _SIMP_ARG(arg) \
for (expr * child : tree(arg)) { \ for (expr * child : tree(arg)) { \
if (is_subexpr_arg(child, arg)) { \ if (is_subexpr_arg(child, arg)) { \
simplify(child); \ simplify(child, true); \
} \ } \
} \ } \
r = simplify(arg); \ r = simplify(arg, false); \
args.push_back(r); \ args.push_back(r); \
if (!assert_expr(r, !is_and)) { \ if (!assert_expr(r, !is_and)) { \
r = is_and ? m.mk_false() : m.mk_true(); \ r = is_and ? m.mk_false() : m.mk_true(); \
@ -364,7 +365,7 @@ void dom_simplify_tactic::simplify_goal(goal& g) {
if (!init(g)) return; if (!init(g)) return;
unsigned sz = g.size(); unsigned sz = g.size();
for (unsigned i = 0; !g.inconsistent() && i < sz; ++i) { for (unsigned i = 0; !g.inconsistent() && i < sz; ++i) {
expr_ref r = simplify(g.form(i)); expr_ref r = simplify(g.form(i), true);
if (i < sz - 1 && !m.is_true(r) && !m.is_false(r) && !g.dep(i) && !g.proofs_enabled() && !assert_expr(r, false)) { if (i < sz - 1 && !m.is_true(r) && !m.is_false(r) && !g.dep(i) && !g.proofs_enabled() && !assert_expr(r, false)) {
r = m.mk_false(); r = m.mk_false();
} }
@ -384,7 +385,7 @@ void dom_simplify_tactic::simplify_goal(goal& g) {
sz = g.size(); sz = g.size();
for (unsigned i = sz; !g.inconsistent() && i > 0; ) { for (unsigned i = sz; !g.inconsistent() && i > 0; ) {
--i; --i;
expr_ref r = simplify(g.form(i)); expr_ref r = simplify(g.form(i), true);
if (i > 0 && !m.is_true(r) && !m.is_false(r) && !g.dep(i) && !g.proofs_enabled() && !assert_expr(r, false)) { if (i > 0 && !m.is_true(r) && !m.is_false(r) && !g.dep(i) && !g.proofs_enabled() && !assert_expr(r, false)) {
r = m.mk_false(); r = m.mk_false();
} }

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

@ -99,7 +99,7 @@ class dom_simplify_tactic : public tactic {
obj_pair_map<expr, expr, bool> m_subexpr_cache; obj_pair_map<expr, expr, bool> m_subexpr_cache;
bool m_forward; bool m_forward;
expr_ref simplify(expr* t); expr_ref simplify(expr* t, bool cache);
expr_ref simplify_ite(app * ite); expr_ref simplify_ite(app * ite);
expr_ref simplify_and(app * ite) { return simplify_and_or(true, ite); } expr_ref simplify_and(app * ite) { return simplify_and_or(true, ite); }
expr_ref simplify_or(app * ite) { return simplify_and_or(false, ite); } expr_ref simplify_or(app * ite) { return simplify_and_or(false, ite); }