rewriter: Make clearCaches non-static. (#7100)

This works towards getting rid of SmtEngine::currentSmtEngine and
closing #3468.

5 files changed, 17 insertions, 11 deletions

diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp
index d1dd389ae..5b13be619 100644
--- a/src/preprocessing/passes/ite_simp.cpp
+++ b/src/preprocessing/passes/ite_simp.cpp
@@ -136,7 +136,7 @@ bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess)
         Chat() << "....node manager contains " << nm->poolSize()
                << " nodes before cleanup" << endl;
         d_iteUtilities.clear();
-        Rewriter::clearCaches();
+        d_preprocContext->getRewriter()->clearCaches();
         nm->reclaimZombiesUntil(options::zombieHuntThreshold());
         Chat() << "....node manager contains " << nm->poolSize()
                << " nodes after cleanup" << endl;
diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp
index 7fefafce6..fe4c8784a 100644
--- a/src/preprocessing/preprocessing_pass_context.cpp
+++ b/src/preprocessing/preprocessing_pass_context.cpp
@@ -44,6 +44,12 @@ const LogicInfo& PreprocessingPassContext::getLogicInfo()
 {
   return d_env.getLogicInfo();
 }
+
+theory::Rewriter* PreprocessingPassContext::getRewriter()
+{
+  return d_env.getRewriter();
+}
+
 theory::TrustSubstitutionMap&
 PreprocessingPassContext::getTopLevelSubstitutions()
 {
diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
index aab1b453d..901322a10 100644
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -66,7 +66,10 @@ class PreprocessingPassContext
   /** Get the current logic info of the environment */
   const LogicInfo& getLogicInfo();
 
-  /** Gets a reference to the top-level substitution map */
+  /** Get a pointer to the Rewriter owned by the associated Env. */
+  theory::Rewriter* getRewriter();
+
+  /** Get a reference to the top-level substitution map */
   theory::TrustSubstitutionMap& getTopLevelSubstitutions();
 
   /** Record symbols in assertions
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index eeb2f166d..de8750d89 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -504,14 +504,13 @@ RewriteResponse Rewriter::processTrustRewriteResponse(
   return RewriteResponse(tresponse.d_status, trn.getNode());
 }
 
-void Rewriter::clearCaches() {
-  Rewriter* rewriter = getInstance();
-
+void Rewriter::clearCaches()
+{
 #ifdef CVC5_ASSERTIONS
-  rewriter->d_rewriteStack.reset(nullptr);
+  d_rewriteStack.reset(nullptr);
 #endif
 
-  rewriter->clearCachesInternal();
+  clearCachesInternal();
 }
 
 }  // namespace theory
diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h
index 3201bb2c8..09f0123bf 100644
--- a/src/theory/rewriter.h
+++ b/src/theory/rewriter.h
@@ -93,10 +93,8 @@ class Rewriter {
   /** Set proof node manager */
   void setProofNodeManager(ProofNodeManager* pnm);
 
-  /**
-   * Garbage collects the rewrite caches.
-   */
-  static void clearCaches();
+  /** Garbage collects the rewrite caches. */
+  void clearCaches();
 
   /**
    * Registers a theory rewriter with this rewriter. The rewriter does not own