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

lessen depth expansin in nnf, add cancelation, add ast_marking to avoid repeated sub-expressions #3065

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-09 19:50:43 +01:00
parent 8beb6618d3
commit c7a6721bf1
1 changed files with 8 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/tactic/core/solve_eqs_tactic.cpp
View file

@ -628,10 +628,12 @@ class solve_eqs_tactic : public tactic {
return true; return true;
} }
void hoist_nnf(goal const& g, expr* f, vector<nnf_context> & path, unsigned idx, unsigned depth) { void hoist_nnf(goal const& g, expr* f, vector<nnf_context> & path, unsigned idx, unsigned depth, ast_mark& mark) {
if (depth > 4) { if (depth > 3 || mark.is_marked(f)) {
return; return;
} }
mark.mark(f, true);
checkpoint();
app_ref var(m()); app_ref var(m());
expr_ref def(m()); expr_ref def(m());
proof_ref pr(m()); proof_ref pr(m());
@ -658,7 +660,7 @@ class solve_eqs_tactic : public tactic {
} }
else { else {
path.push_back(nnf_context(true, args, i)); path.push_back(nnf_context(true, args, i));
hoist_nnf(g, arg, path, idx, depth + 1); hoist_nnf(g, arg, path, idx, depth + 1, mark);
path.pop_back(); path.pop_back();
} }
} }
@ -667,7 +669,7 @@ class solve_eqs_tactic : public tactic {
flatten_or(f, args); flatten_or(f, args);
for (unsigned i = 0; i < args.size(); ++i) { for (unsigned i = 0; i < args.size(); ++i) {
path.push_back(nnf_context(false, args, i)); path.push_back(nnf_context(false, args, i));
hoist_nnf(g, args.get(i), path, idx, depth + 1); hoist_nnf(g, args.get(i), path, idx, depth + 1, mark);
path.pop_back(); path.pop_back();
} }
} }
@ -675,10 +677,11 @@ class solve_eqs_tactic : public tactic {
void collect_hoist(goal const& g) { void collect_hoist(goal const& g) {
unsigned size = g.size(); unsigned size = g.size();
ast_mark mark;
vector<nnf_context> path; vector<nnf_context> path;
for (unsigned idx = 0; idx < size; idx++) { for (unsigned idx = 0; idx < size; idx++) {
checkpoint(); checkpoint();
hoist_nnf(g, g.form(idx), path, idx, 0); hoist_nnf(g, g.form(idx), path, idx, 0, mark);
} }
} }