summaryrefslogtreecommitdiff
path: root/src/theory/rewriter.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/rewriter.cpp')
-rw-r--r--src/theory/rewriter.cpp18
1 files changed, 9 insertions, 9 deletions
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index 54b9f319d..ca552de66 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -18,6 +18,7 @@
#include "theory/rewriter.h"
#include "options/theory_options.h"
+#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
#include "smt/smt_statistics_registry.h"
#include "theory/rewriter_tables.h"
@@ -93,13 +94,13 @@ Node Rewriter::rewrite(TNode node) {
// eagerly for the sake of efficiency here.
return node;
}
- return getInstance().rewriteTo(theoryOf(node), node);
+ return getInstance()->rewriteTo(theoryOf(node), node);
}
void Rewriter::registerTheoryRewriter(theory::TheoryId tid,
- std::unique_ptr<TheoryRewriter> trew)
+ TheoryRewriter* trew)
{
- getInstance().d_theoryRewriters[tid] = std::move(trew);
+ getInstance()->d_theoryRewriters[tid] = trew;
}
void Rewriter::registerPreRewrite(
@@ -130,10 +131,9 @@ void Rewriter::registerPostRewriteEqual(
d_postRewritersEqual[tid] = fn;
}
-Rewriter& Rewriter::getInstance()
+Rewriter* Rewriter::getInstance()
{
- thread_local static Rewriter rewriter;
- return rewriter;
+ return smt::currentSmtEngine()->getRewriter();
}
Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
@@ -351,13 +351,13 @@ RewriteResponse Rewriter::postRewrite(theory::TheoryId theoryId, TNode n)
}
void Rewriter::clearCaches() {
- Rewriter& rewriter = getInstance();
+ Rewriter* rewriter = getInstance();
#ifdef CVC4_ASSERTIONS
- rewriter.d_rewriteStack.reset(nullptr);
+ rewriter->d_rewriteStack.reset(nullptr);
#endif
- rewriter.clearCachesInternal();
+ rewriter->clearCachesInternal();
}
}/* CVC4::theory namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback