From 3ebbb8472a4f57672528f69dc22850312dd9ba2d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 2 Dec 2022 07:54:14 -0800
Subject: [PATCH] fix perf bugs in new value propagation

---
 src/ast/simplifiers/propagate_values.cpp | 74 +++++++++++++-----------
 src/ast/simplifiers/propagate_values.h   |  6 ++
 2 files changed, 45 insertions(+), 35 deletions(-)

diff --git a/src/ast/simplifiers/propagate_values.cpp b/src/ast/simplifiers/propagate_values.cpp
index f0d85af7279..7d698faa310 100644
--- a/src/ast/simplifiers/propagate_values.cpp
+++ b/src/ast/simplifiers/propagate_values.cpp
@@ -22,44 +22,19 @@ Module Name:
 #include "params/tactic_params.hpp"
 #include "ast/ast_pp.h"
 #include "ast/ast_util.h"
-#include "ast/shared_occs.h"
 #include "ast/simplifiers/propagate_values.h"
 
 propagate_values::propagate_values(ast_manager& m, params_ref const& p, dependent_expr_state& fmls):
     dependent_expr_simplifier(m, fmls),
-    m_rewriter(m) {
-    m_rewriter.set_order_eq(true);
+    m_rewriter(m),
+    m_shared(m, true),
+    m_subst(m, true, false) {
     m_rewriter.set_flat_and_or(false);
     updt_params(p);
 }
 
-void propagate_values::reduce() {
-    shared_occs shared(m, true);
-    expr_substitution subst(m, true, false);
-    expr* x, * y;
-
-    auto add_shared = [&]() {
-        shared_occs_mark visited;
-        shared.reset();
-        for (unsigned i = 0; i < qtail(); ++i)
-            shared(m_fmls[i].fml(), visited);
-    };
-    
-    auto add_sub = [&](dependent_expr const& de) {
-        auto const& [f, dep] = de();
-        if (m.is_not(f, x) && shared.is_shared(x))
-            subst.insert(x, m.mk_false(), dep);
-        else if (shared.is_shared(f))
-            subst.insert(f, m.mk_true(), dep);
-        if (m.is_eq(f, x, y)) {
-            if (m.is_value(x) && shared.is_shared(y))
-                subst.insert(y, x, dep);
-            else if (m.is_value(y) && shared.is_shared(x))
-                subst.insert(x, y, dep);
-        }
-    };
-    
-    auto process_fml = [&](unsigned i) {
+void propagate_values::process_fml(unsigned i) {
+    if (!m_subst.empty()) {
         auto [f, dep] = m_fmls[i]();
         expr_ref fml(m);
         proof_ref pr(m);
@@ -70,14 +45,41 @@ void propagate_values::reduce() {
             ++m_stats.m_num_rewrites;
         }
         m_rewriter.reset_used_dependencies();
-        add_sub(m_fmls[i]);
-    };
+    }
+    add_sub(m_fmls[i]);
+}
+
+void propagate_values::add_sub(dependent_expr const& de) {
+    expr* x, * y;
+    auto const& [f, dep] = de();
+    if (m.is_not(f, x) && m_shared.is_shared(x))
+        m_subst.insert(x, m.mk_false(), dep);
+    if (m_shared.is_shared(f))
+        m_subst.insert(f, m.mk_true(), dep);
+    if (m.is_eq(f, x, y)) {
+        if (m.is_value(x) && m_shared.is_shared(y))
+            m_subst.insert(y, x, dep);
+        else if (m.is_value(y) && m_shared.is_shared(x))
+            m_subst.insert(x, y, dep);
+    }
+};
 
+void propagate_values::reduce() {
+    m_shared.reset();
+    m_subst.reset();
+
+    auto add_shared = [&]() {
+        shared_occs_mark visited;
+        m_shared.reset();
+        for (unsigned i = 0; i < qtail(); ++i)
+            m_shared(m_fmls[i].fml(), visited);
+    };   
+   
     auto init_sub = [&]() {
         add_shared();
-        subst.reset();
+        m_subst.reset();
         m_rewriter.reset();
-        m_rewriter.set_substitution(&subst);
+        m_rewriter.set_substitution(&m_subst);
         for (unsigned i = 0; i < qhead(); ++i)
             add_sub(m_fmls[i]);
     };
@@ -91,12 +93,14 @@ void propagate_values::reduce() {
         init_sub();
         for (unsigned i = qtail(); i-- > qhead() && m.inc() && !m_fmls.inconsistent();)
             process_fml(i);
-        if (subst.empty())
+        if (m_subst.empty())
             break;
     }
     
     m_rewriter.set_substitution(nullptr);        
     m_rewriter.reset();
+    m_subst.reset();
+    m_shared.reset();
 }
 
 void propagate_values::collect_statistics(statistics& st) const {
diff --git a/src/ast/simplifiers/propagate_values.h b/src/ast/simplifiers/propagate_values.h
index 9ad59d1b34d..8b4e9fdd09a 100644
--- a/src/ast/simplifiers/propagate_values.h
+++ b/src/ast/simplifiers/propagate_values.h
@@ -22,6 +22,7 @@ Module Name:
 
 #include "ast/simplifiers/dependent_expr_state.h"
 #include "ast/rewriter/th_rewriter.h"
+#include "ast/shared_occs.h"
 
 
 class propagate_values : public dependent_expr_simplifier {
@@ -34,6 +35,11 @@ class propagate_values : public dependent_expr_simplifier {
     th_rewriter            m_rewriter;
     stats                  m_stats;
     unsigned               m_max_rounds = 4;
+    shared_occs            m_shared;
+    expr_substitution      m_subst;
+
+    void process_fml(unsigned i);
+    void add_sub(dependent_expr const& de);
 
 public:
     propagate_values(ast_manager& m, params_ref const& p, dependent_expr_state& fmls);