From 7cd8edce1fce4023fc6bcff54d6180987f5aa71e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 12 Apr 2023 21:01:05 -0700
Subject: [PATCH] perf and memory smash fixes to internal node count routine

---
 src/ast/for_each_expr.cpp          | 27 ++++++++-------------------
 src/ast/for_each_expr.h            |  5 +++--
 src/ast/rewriter/bool_rewriter.cpp | 17 +++++++++++++----
 src/ast/rewriter/bool_rewriter.h   |  2 ++
 4 files changed, 26 insertions(+), 25 deletions(-)

diff --git a/src/ast/for_each_expr.cpp b/src/ast/for_each_expr.cpp
index 374d7b496a8..832c1d0bcc0 100644
--- a/src/ast/for_each_expr.cpp
+++ b/src/ast/for_each_expr.cpp
@@ -45,7 +45,7 @@ unsigned get_num_exprs(expr * n) {
 }
 
 
-static void get_num_internal_exprs(unsigned_vector& counts, sbuffer<expr*>& todo, expr * n) {
+void get_num_internal_exprs(unsigned_vector& counts, ptr_vector<expr>& todo, expr * n) {
     counts.reserve(n->get_id() + 1);
     unsigned& rc = counts[n->get_id()];
     if (rc > 0) {
@@ -55,7 +55,6 @@ static void get_num_internal_exprs(unsigned_vector& counts, sbuffer<expr*>& todo
     rc = n->get_ref_count() - 1;
     unsigned i = todo.size();
     todo.push_back(n);
-    unsigned count = 0;
     for (; i < todo.size(); ++i) {
         n = todo[i];
         if (!is_app(n))
@@ -74,27 +73,17 @@ static void get_num_internal_exprs(unsigned_vector& counts, sbuffer<expr*>& todo
     }
 }
 
-unsigned get_num_internal_exprs(expr * n) {
-    unsigned_vector counts;
-    sbuffer<expr*> todo;
+unsigned count_internal_nodes(unsigned_vector& counts, ptr_vector<expr>& todo) {
     unsigned internal_nodes = 0;
-    get_num_internal_exprs(counts, todo, n);
-    for (expr* t : todo) 
-        if (counts[t->get_id()] == 0)
-            ++internal_nodes;
-    return internal_nodes;
-}
-
-unsigned get_num_internal_exprs(unsigned sz, expr * const * args) {
-    unsigned_vector counts;
-    sbuffer<expr*> todo;
-    unsigned internal_nodes = 0;
-    for (unsigned i = 0; i < sz; ++i)
-        get_num_internal_exprs(counts, todo, args[i]);
-    for (expr* t : todo) 
+    for (expr* t : todo) {
         if (counts[t->get_id()] == 0)
             ++internal_nodes;
+        else
+            counts[t->get_id()] = 0;
+    }
+    todo.reset();
     return internal_nodes;
+    
 }
 
 
diff --git a/src/ast/for_each_expr.h b/src/ast/for_each_expr.h
index c943489640d..0ba0dc9926d 100644
--- a/src/ast/for_each_expr.h
+++ b/src/ast/for_each_expr.h
@@ -163,12 +163,13 @@ struct for_each_expr_proc : public EscapeProc {
 unsigned get_num_exprs(expr * n);
 unsigned get_num_exprs(expr * n, expr_mark & visited);
 unsigned get_num_exprs(expr * n, expr_fast_mark1 & visited);
-unsigned get_num_internal_exprs(expr * n);
-unsigned get_num_internal_exprs(unsigned sz, expr * const * args);
+void get_num_internal_exprs(unsigned_vector& counts, ptr_vector<expr>& todo, expr * n);
+unsigned count_internal_nodes(unsigned_vector& counts, ptr_vector<expr>& todo);
 
 bool has_skolem_functions(expr * n);
 
 // pre-order traversal of subterms
+
 class subterms {
     bool            m_include_bound = false;
     expr_ref_vector m_es;
diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp
index 9ebdbe7fda7..95c0950d87e 100644
--- a/src/ast/rewriter/bool_rewriter.cpp
+++ b/src/ast/rewriter/bool_rewriter.cpp
@@ -269,19 +269,28 @@ br_status bool_rewriter::mk_nflat_or_core(unsigned num_args, expr * const * args
                 return BR_DONE;
         }
 
+#if 1
         br_status st;
-        st = m_hoist.mk_or(buffer.size(), buffer.data(), result);
+        expr_ref r(m());
+        st = m_hoist.mk_or(buffer.size(), buffer.data(), r);
         if (st != BR_FAILED) {
-            unsigned count1 = get_num_internal_exprs(result);
-            unsigned count2 = get_num_internal_exprs(buffer.size(), buffer.data());
+            m_counts1.reserve(m().get_num_asts() + 1);
+            m_counts2.reserve(m().get_num_asts() + 1);
+            get_num_internal_exprs(m_counts1, m_todo1, r);
+            for (unsigned i = 0; i < num_args; ++i)
+                get_num_internal_exprs(m_counts2, m_todo2, args[i]);
+            unsigned count1 = count_internal_nodes(m_counts1, m_todo1);
+            unsigned count2 = count_internal_nodes(m_counts2, m_todo2);
             if (count1 > count2)
                 st = BR_FAILED;
         }
+        if (st != BR_FAILED)
+            result = r;
         if (st == BR_DONE)
             return BR_REWRITE1;
         if (st != BR_FAILED)
             return st;
-
+#endif
         if (s) {
             ast_lt lt;
             std::sort(buffer.begin(), buffer.end(), lt);       
diff --git a/src/ast/rewriter/bool_rewriter.h b/src/ast/rewriter/bool_rewriter.h
index e02bf86d38f..0693e94ba85 100644
--- a/src/ast/rewriter/bool_rewriter.h
+++ b/src/ast/rewriter/bool_rewriter.h
@@ -62,6 +62,8 @@ class bool_rewriter {
     unsigned       m_local_ctx_limit;
     unsigned       m_local_ctx_cost;
     bool           m_elim_ite;
+    ptr_vector<expr> m_todo1, m_todo2;
+    unsigned_vector m_counts1, m_counts2;
 
     br_status mk_flat_and_core(unsigned num_args, expr * const * args, expr_ref & result);
     br_status mk_flat_or_core(unsigned num_args, expr * const * args, expr_ref & result);