mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 09:34:08 +00:00
fix perf bug exposed by Shelly Grossman
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
3dcfbb8347
commit
18fe28c0f0
|
@ -43,6 +43,7 @@ public:
|
|||
bool unsat_core_enabled() const { return m_cores_enabled; }
|
||||
|
||||
bool empty() const { return m_subst.empty(); }
|
||||
unsigned size() const { return m_subst.size(); }
|
||||
void insert(expr * s, expr * def, proof * def_pr = nullptr, expr_dependency * def_dep = nullptr);
|
||||
void erase(expr * s);
|
||||
bool find(expr * s, expr * & def, proof * & def_pr);
|
||||
|
@ -82,6 +83,7 @@ public:
|
|||
}
|
||||
unsigned scope_level() const { return m_trail_lim.size(); }
|
||||
bool empty() const { return m_subst.empty(); }
|
||||
unsigned size() const { return m_subst.size(); }
|
||||
expr* find(expr * e) { proof* pr; expr* d = nullptr; if (find(e, d, pr)) return d; else return e; }
|
||||
bool find(expr * s, expr * & def, proof * & def_pr) { return m_subst.find(s, def, def_pr); }
|
||||
bool find(expr * s, expr * & def, proof * & def_pr, expr_dependency * & def_dep) { return m_subst.find(s, def, def_pr, def_dep); }
|
||||
|
|
|
@ -452,6 +452,7 @@ class solve_eqs_tactic : public tactic {
|
|||
{}
|
||||
};
|
||||
|
||||
ptr_vector<expr> m_todo;
|
||||
void mark_occurs(expr_mark& occ, goal const& g, expr* v) {
|
||||
expr_fast_mark2 visited;
|
||||
occ.mark(v, true);
|
||||
|
@ -500,14 +501,15 @@ class solve_eqs_tactic : public tactic {
|
|||
|
||||
bool is_compatible(goal const& g, unsigned idx, vector<nnf_context> const & path, expr* v, expr* eq) {
|
||||
expr_mark occ;
|
||||
svector<lbool> cache;
|
||||
mark_occurs(occ, g, v);
|
||||
return is_goal_compatible(g, occ, idx, v, eq) && is_path_compatible(occ, path, v, eq);
|
||||
return is_goal_compatible(g, occ, cache, idx, v, eq) && is_path_compatible(occ, cache, path, v, eq);
|
||||
}
|
||||
|
||||
bool is_goal_compatible(goal const& g, expr_mark& occ, unsigned idx, expr* v, expr* eq) {
|
||||
bool is_goal_compatible(goal const& g, expr_mark& occ, svector<lbool>& cache, unsigned idx, expr* v, expr* eq) {
|
||||
bool all_e = false;
|
||||
for (unsigned j = 0; j < g.size(); ++j) {
|
||||
if (j != idx && !check_eq_compat_rec(occ, g.form(j), v, eq, all_e)) {
|
||||
if (j != idx && !check_eq_compat_rec(occ, cache, g.form(j), v, eq, all_e)) {
|
||||
TRACE("solve_eqs", tout << "occurs goal " << mk_pp(eq, m()) << "\n";);
|
||||
return false;
|
||||
}
|
||||
|
@ -524,7 +526,7 @@ class solve_eqs_tactic : public tactic {
|
|||
// and, all_e -> all_e
|
||||
//
|
||||
|
||||
bool is_path_compatible(expr_mark& occ, vector<nnf_context> const & path, expr* v, expr* eq) {
|
||||
bool is_path_compatible(expr_mark& occ, svector<lbool>& cache, vector<nnf_context> const & path, expr* v, expr* eq) {
|
||||
bool all_e = true;
|
||||
for (unsigned i = path.size(); i-- > 0; ) {
|
||||
auto const& p = path[i];
|
||||
|
@ -541,7 +543,7 @@ class solve_eqs_tactic : public tactic {
|
|||
for (unsigned j = 0; j < args.size(); ++j) {
|
||||
if (j != p.m_index) {
|
||||
if (occurs(v, args[j])) {
|
||||
if (!check_eq_compat_rec(occ, args[j], v, eq, all_e)) {
|
||||
if (!check_eq_compat_rec(occ, cache, args[j], v, eq, all_e)) {
|
||||
TRACE("solve_eqs", tout << "occurs or " << mk_pp(eq, m()) << " " << mk_pp(args[j], m()) << "\n";);
|
||||
return false;
|
||||
}
|
||||
|
@ -556,18 +558,23 @@ class solve_eqs_tactic : public tactic {
|
|||
return true;
|
||||
}
|
||||
|
||||
ptr_vector<expr> m_todo;
|
||||
bool check_eq_compat_rec(expr_mark& occ, expr* f, expr* v, expr* eq, bool& all) {
|
||||
bool check_eq_compat_rec(expr_mark& occ, svector<lbool>& cache, expr* f, expr* v, expr* eq, bool& all) {
|
||||
expr_ref_vector args(m());
|
||||
expr* f1 = nullptr;
|
||||
if (!occ.is_marked(f)) {
|
||||
all = false;
|
||||
return true;
|
||||
}
|
||||
unsigned idx = f->get_id();
|
||||
if (cache.size() > idx && cache[idx] != l_undef) {
|
||||
return cache[idx] == l_true;
|
||||
}
|
||||
if (m().is_not(f, f1) && m().is_or(f1)) {
|
||||
flatten_and(f, args);
|
||||
for (expr* arg : args) {
|
||||
if (arg == eq) {
|
||||
cache.reserve(idx+1, l_undef);
|
||||
cache[idx] = l_true;
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
@ -580,10 +587,14 @@ class solve_eqs_tactic : public tactic {
|
|||
}
|
||||
|
||||
for (expr* arg : args) {
|
||||
if (!check_eq_compat_rec(occ, arg, v, eq, all)) {
|
||||
if (!check_eq_compat_rec(occ, cache, arg, v, eq, all)) {
|
||||
cache.reserve(idx+1, l_undef);
|
||||
cache[idx] = l_false;
|
||||
return false;
|
||||
}
|
||||
}
|
||||
cache.reserve(idx+1, l_undef);
|
||||
cache[idx] = l_true;
|
||||
return true;
|
||||
}
|
||||
|
||||
|
@ -889,9 +900,7 @@ class solve_eqs_tactic : public tactic {
|
|||
return;
|
||||
}
|
||||
g.elim_true();
|
||||
TRACE("solve_eqs",
|
||||
tout << "after applying substitution\n";
|
||||
g.display(tout););
|
||||
TRACE("solve_eqs", g.display(tout << "after applying substitution\n"););
|
||||
#if 0
|
||||
DEBUG_CODE({
|
||||
for (expr* v : m_ordered_vars) {
|
||||
|
@ -987,11 +996,13 @@ class solve_eqs_tactic : public tactic {
|
|||
if (m_context_solve) {
|
||||
collect_hoist(*g);
|
||||
}
|
||||
if (m_subst->empty())
|
||||
if (m_subst->empty()) {
|
||||
break;
|
||||
}
|
||||
sort_vars();
|
||||
if (m_ordered_vars.empty())
|
||||
if (m_ordered_vars.empty()) {
|
||||
break;
|
||||
}
|
||||
normalize();
|
||||
substitute(*(g.get()));
|
||||
if (g->inconsistent()) {
|
||||
|
|
Loading…
Reference in a new issue