mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

fix #3948 - cache has to be reset also when processing 'and' because it could be processed in an incompatible context by the caller

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-15 13:29:45 -07:00
parent 2e1e9c9082
commit 357ec2fd01
1 changed files with 30 additions and 25 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -20,6 +20,7 @@ Notes:
#include "ast/ast_util.h"
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
#include "tactic/core/dom_simplify_tactic.h"
/**
@ -92,7 +93,7 @@ bool expr_dominators::compute_dominators() {
change = false;
TRACE("simplify",
for (auto & kv : m_doms) {
tout << expr_ref(kv.m_key, m) << " |-> " << expr_ref(kv.m_value, m) << "\n";
tout << mk_bounded_pp(kv.m_key, m) << " |-> " << mk_bounded_pp(kv.m_value, m) << "\n";
});
SASSERT(m_post2expr.empty() || m_post2expr.back() == e);
@ -159,7 +160,7 @@ std::ostream& expr_dominators::display(std::ostream& out) {
std::ostream& expr_dominators::display(std::ostream& out, unsigned indent, expr* r) {
for (unsigned i = 0; i < indent; ++i) out << " ";
out << expr_ref(r, m) << "\n";
out << r->get_id() << ": " << mk_bounded_pp(r, m, 1) << "\n";
if (m_tree.contains(r)) {
for (expr* child : m_tree[r]) {
if (child != r)
@ -295,6 +296,7 @@ expr_ref dom_simplify_tactic::simplify_rec(expr * e0) {
r = e;
}
}
CTRACE("simplify", e0 != r, tout << "depth before: " << m_depth << " " << mk_pp(e0, m) << " -> " << r << "\n";);
(*m_simplifier)(r);
cache(e0, r);
CTRACE("simplify", e0 != r, tout << "depth: " << m_depth << " " << mk_pp(e0, m) << " -> " << r << "\n";);
@ -318,39 +320,40 @@ expr_ref dom_simplify_tactic::simplify_and_or(bool is_and, app * e) {
};
expr_ref_vector args(m);
auto simp_arg = [&](expr* arg) {
for (expr * child : tree(arg)) {
if (is_subexpr_arg(child, arg)) {
simplify_rec(child);
}
}
r = simplify_arg(arg);
args.push_back(r);
if (!assert_expr(r, !is_and)) {
pop(scope_level() - old_lvl);
r = is_and ? m.mk_false() : m.mk_true();
reset_cache();
return true;
}
return false;
};
if (m_forward) {
for (expr * arg : *e) {
#define _SIMP_ARG(arg) \
for (expr * child : tree(arg)) { \
if (is_subexpr_arg(child, arg)) { \
simplify_rec(child); \
} \
} \
r = simplify_arg(arg); \
args.push_back(r); \
if (!assert_expr(r, !is_and)) { \
pop(scope_level() - old_lvl); \
r = is_and ? m.mk_false() : m.mk_true(); \
if (!is_and) \
reset_cache(); \
return r; \
}
_SIMP_ARG(arg);
if (simp_arg(arg))
return r;
}
}
else {
for (unsigned i = e->get_num_args(); i > 0; ) {
--i;
expr* arg = e->get_arg(i);
_SIMP_ARG(arg);
for (unsigned i = e->get_num_args(); i-- > 0; ) {
if (simp_arg(e->get_arg(i)))
return r;
}
args.reverse();
}
pop(scope_level() - old_lvl);
// TODO: add stack for cache rather than destroy it completely everywhere
if (!is_and)
reset_cache();
reset_cache();
return { is_and ? mk_and(args) : mk_or(args), m };
}
@ -546,6 +549,8 @@ public:
if (m.is_true(t))
return !sign;
TRACE("simplify", tout << t->get_id() << ": " << mk_bounded_pp(t, m) << " " << (sign?" - neg":" - pos") << "\n";);
m_scoped_substitution.push();
if (!sign) {
update_substitution(t, nullptr);