From c7a6721bf16fd66efc41cc89a117f6a1a1c1add4 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 9 Mar 2020 19:50:43 +0100
Subject: [PATCH] lessen depth expansin in nnf, add cancelation, add
 ast_marking to avoid repeated sub-expressions #3065

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/tactic/core/solve_eqs_tactic.cpp | 13 ++++++++-----
 1 file changed, 8 insertions(+), 5 deletions(-)

diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp
index 0eedb7769..6ee1f95aa 100644
--- a/src/tactic/core/solve_eqs_tactic.cpp
+++ b/src/tactic/core/solve_eqs_tactic.cpp
@@ -628,10 +628,12 @@ class solve_eqs_tactic : public tactic {
             return true;
         }
 
-        void hoist_nnf(goal const& g, expr* f, vector<nnf_context> & path, unsigned idx, unsigned depth) {
-            if (depth > 4) {
+        void hoist_nnf(goal const& g, expr* f, vector<nnf_context> & path, unsigned idx, unsigned depth, ast_mark& mark) {
+            if (depth > 3 || mark.is_marked(f)) {
                 return;
             }
+            mark.mark(f, true);
+            checkpoint();
             app_ref var(m());
             expr_ref def(m());
             proof_ref pr(m());
@@ -658,7 +660,7 @@ class solve_eqs_tactic : public tactic {
                     }
                     else {
                         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();
                     }                             
                 }
@@ -667,7 +669,7 @@ class solve_eqs_tactic : public tactic {
                 flatten_or(f, args);
                 for (unsigned i = 0; i < args.size(); ++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();
                 }
             }
@@ -675,10 +677,11 @@ class solve_eqs_tactic : public tactic {
 
         void collect_hoist(goal const& g) {
             unsigned size = g.size();
+            ast_mark mark;
             vector<nnf_context> path;
             for (unsigned idx = 0; idx < size; idx++) {
                 checkpoint();
-                hoist_nnf(g, g.form(idx), path, idx, 0);
+                hoist_nnf(g, g.form(idx), path, idx, 0, mark);
             }
         }