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

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

diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp
index d1dd389aed78c730d2bc41bae481f7ae631a00c2..5b13be619a20428c6bac2e1a0b27e65e892d245c 100644 (file)
--- 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 7fefafce68ae7d3a80f7ca639416904028f32176..fe4c8784a14a5e073db82a7735b7e7fb3147b8ae 100644 (file)
--- 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 aab1b453dbd1e9f37072b6b0b14d763c110ae413..901322a1024c634a457faf40bedc7abf274e788e 100644 (file)
--- 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 eeb2f166d5bf968e0d5c7f48d4a91f629d16e38b..de8750d89a2206a2c21097a57e7a090d36e23775 100644 (file)
--- 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 3201bb2c8ba90e2b45d78f29fa02839171642894..09f0123bfde1c3a00e900b567d990f26eb2d497e 100644 (file)
--- 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