diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-08-31 17:35:58 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-09-01 00:35:58 +0000 |
commit | 068a0aa316f3760b401d900d39101955ba66b6c2 (patch) | |
tree | 78f7da88e0040dade1da7033bb4d98f5bb8a23d3 /src | |
parent | 5e969241cd3bdec90138edb5d1c88d3e1797cb43 (diff) |
rewriter: Make clearCaches non-static. (#7100)
This works towards getting rid of SmtEngine::currentSmtEngine and
closing #3468.
Diffstat (limited to 'src')
-rw-r--r-- | src/preprocessing/passes/ite_simp.cpp | 2 | ||||
-rw-r--r-- | src/preprocessing/preprocessing_pass_context.cpp | 6 | ||||
-rw-r--r-- | src/preprocessing/preprocessing_pass_context.h | 5 | ||||
-rw-r--r-- | src/theory/rewriter.cpp | 9 | ||||
-rw-r--r-- | src/theory/rewriter.h | 6 |
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 |