From 7869cdbbc88a70d7915f26c39259066985ea0d70 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 12 May 2021 10:43:16 -0700
Subject: [PATCH] #5259 - the Ranjit 2s shave

shave a couple of seconds from the Ranjit regression
---
 src/ast/normal_forms/nnf.cpp   | 11 ++++++-----
 src/ast/rewriter/var_subst.cpp |  4 +++-
 src/ast/used_vars.cpp          | 15 +++++++++++++--
 src/ast/used_vars.h            | 10 +++++++++-
 4 files changed, 31 insertions(+), 9 deletions(-)

diff --git a/src/ast/normal_forms/nnf.cpp b/src/ast/normal_forms/nnf.cpp
index 19b776aba..d0398543b 100644
--- a/src/ast/normal_forms/nnf.cpp
+++ b/src/ast/normal_forms/nnf.cpp
@@ -72,6 +72,7 @@ class skolemizer {
     cache         m_cache;
     cache         m_cache_pr;
     bool          m_proofs_enabled;
+    used_vars     m_uv;
 
 
     void process(quantifier * q, expr_ref & r, proof_ref & p) {
@@ -81,14 +82,14 @@ class skolemizer {
             p = nullptr;
             return;
         }
-        used_vars uv;
-        uv(q);
+        m_uv.reset();
+        m_uv(q);
         SASSERT(is_well_sorted(m, q));
-        unsigned sz = uv.get_max_found_var_idx_plus_1();
+        unsigned sz = m_uv.get_max_found_var_idx_plus_1();
         ptr_buffer<sort> sorts;
         expr_ref_vector args(m);
         for (unsigned i = 0; i < sz; i++) {
-            sort * s = uv.get(i);
+            sort * s = m_uv.get(i);
             if (s != nullptr) {
                 sorts.push_back(s);
                 args.push_back(m.mk_var(i, s));
@@ -111,7 +112,7 @@ class skolemizer {
         // (VAR num_decls-1) is in the last position.
         //
         for (unsigned i = 0; i < sz; i++) {
-            sort * s = uv.get(i);
+            sort * s = m_uv.get(i);
             if (s != nullptr)
                 substitution.push_back(m.mk_var(i, s));
             else
diff --git a/src/ast/rewriter/var_subst.cpp b/src/ast/rewriter/var_subst.cpp
index 13dd4f459..a61cfdc4e 100644
--- a/src/ast/rewriter/var_subst.cpp
+++ b/src/ast/rewriter/var_subst.cpp
@@ -79,7 +79,9 @@ expr_ref unused_vars_eliminator::operator()(quantifier* q) {
         result = q;
         return result;
     }
+    unsigned num_decls = q->get_num_decls();
     m_used.reset();
+    m_used.set_num_decls(num_decls);
     m_used.process(q->get_expr());
     unsigned num_patterns = q->get_num_patterns();
     for (unsigned i = 0; i < num_patterns; i++)
@@ -88,7 +90,7 @@ expr_ref unused_vars_eliminator::operator()(quantifier* q) {
     for (unsigned i = 0; i < num_no_patterns; i++)
         m_used.process(q->get_no_pattern(i));
 
-    unsigned num_decls = q->get_num_decls();
+    
     if (m_used.uses_all_vars(num_decls)) {
         q->set_no_unused_vars();
         result = q;
diff --git a/src/ast/used_vars.cpp b/src/ast/used_vars.cpp
index a3030f087..29321d98a 100644
--- a/src/ast/used_vars.cpp
+++ b/src/ast/used_vars.cpp
@@ -22,6 +22,9 @@ Revision History:
 void used_vars::process(expr * n, unsigned delta) {
     unsigned j, idx;
 
+    if (m_num_found_vars == m_num_decls)
+        return;
+
     m_cache.reset();
     m_todo.reset();
     m_todo.push_back(expr_delta_pair(n, delta));
@@ -58,8 +61,16 @@ void used_vars::process(expr * n, unsigned delta) {
             if (idx >= delta) {
                 idx = idx - delta;
                 if (idx >= m_found_vars.size())
-                    m_found_vars.resize(idx + 1);
-                m_found_vars[idx] = to_var(n)->get_sort();
+                    m_found_vars.resize(idx + 1, nullptr);
+                if (!m_found_vars[idx]) {
+                    m_found_vars[idx] = to_var(n)->get_sort();
+                    if (idx < m_num_decls)
+                        m_num_found_vars++;
+                    if (m_num_found_vars == m_num_decls) {
+                        m_todo.reset();
+                        return;
+                    }
+                }
             }
             break;
         case AST_QUANTIFIER:
diff --git a/src/ast/used_vars.h b/src/ast/used_vars.h
index dbd7ae854..c9ecdcfea 100644
--- a/src/ast/used_vars.h
+++ b/src/ast/used_vars.h
@@ -26,18 +26,26 @@ class used_vars {
     typedef hashtable<expr_delta_pair, obj_hash<expr_delta_pair>, default_eq<expr_delta_pair> > cache;
     cache                    m_cache;
     svector<expr_delta_pair> m_todo;
+    unsigned                 m_num_decls{ UINT_MAX };
+    unsigned                 m_num_found_vars{ 0 };
 
     void process(expr * n, unsigned delta);
 
 public:
     
     void operator()(expr * n) {
-        m_found_vars.reset();
+        reset();
         process(n, 0);
     }
 
     void reset() {
         m_found_vars.reset();
+        m_num_decls = UINT_MAX;
+        m_num_found_vars = 0;
+    }
+
+    void set_num_decls(unsigned n) {
+        m_num_decls = n;
     }
 
     void process(expr * n) {