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.cpp125
1 files changed, 68 insertions, 57 deletions
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index 866883681..3380694e7 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -28,37 +28,34 @@ using namespace std;
namespace CVC4 {
namespace theory {
-unsigned long Rewriter::d_iterationCount = 0;
-
static TheoryId theoryOf(TNode node) {
return Theory::theoryOf(THEORY_OF_TYPE_BASED, node);
}
-#ifdef CVC4_ASSERTIONS
-static thread_local std::unique_ptr<std::unordered_set<Node, NodeHashFunction>>
- s_rewriteStack = nullptr;
-#endif /* CVC4_ASSERTIONS */
-
-class RewriterInitializer {
- static RewriterInitializer s_rewriterInitializer;
- RewriterInitializer() {
- Rewriter::init();
- }
- ~RewriterInitializer() { Rewriter::shutdown(); }
-};/* class RewriterInitializer */
-
-/**
- * This causes initialization of the rewriter before first use,
- * and tear-down at exit time.
- */
-RewriterInitializer RewriterInitializer::s_rewriterInitializer;
-
/**
* TheoryEngine::rewrite() keeps a stack of things that are being pre-
* and post-rewritten. Each element of the stack is a
* RewriteStackElement.
*/
struct RewriteStackElement {
+ /**
+ * Construct a fresh stack element.
+ */
+ RewriteStackElement(TNode node, TheoryId theoryId)
+ : node(node),
+ original(node),
+ theoryId(theoryId),
+ originalTheoryId(theoryId),
+ nextChild(0)
+ {
+ }
+
+ TheoryId getTheoryId() { return static_cast<TheoryId>(theoryId); }
+
+ TheoryId getOriginalTheoryId()
+ {
+ return static_cast<TheoryId>(originalTheoryId);
+ }
/** The node we're currently rewriting */
Node node;
@@ -72,21 +69,17 @@ struct RewriteStackElement {
unsigned nextChild : 32;
/** Builder for this node */
NodeBuilder<> builder;
-
- /**
- * Construct a fresh stack element.
- */
- RewriteStackElement(TNode node, TheoryId theoryId) :
- node(node),
- original(node),
- theoryId(theoryId),
- originalTheoryId(theoryId),
- nextChild(0) {
- }
};
Node Rewriter::rewrite(TNode node) {
- return rewriteTo(theoryOf(node), node);
+ Rewriter& rewriter = getInstance();
+ return rewriter.rewriteTo(theoryOf(node), node);
+}
+
+Rewriter& Rewriter::getInstance()
+{
+ thread_local static Rewriter rewriter;
+ return rewriter;
}
Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
@@ -94,9 +87,9 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
#ifdef CVC4_ASSERTIONS
bool isEquality = node.getKind() == kind::EQUAL && (!node[0].getType().isBoolean());
- if (s_rewriteStack == nullptr)
+ if (d_rewriteStack == nullptr)
{
- s_rewriteStack.reset(new std::unordered_set<Node, NodeHashFunction>());
+ d_rewriteStack.reset(new std::unordered_set<Node, NodeHashFunction>());
}
#endif
@@ -129,29 +122,38 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
// Get the top of the recursion stack
RewriteStackElement& rewriteStackTop = rewriteStack.back();
- Trace("rewriter") << "Rewriter::rewriting: " << (TheoryId) rewriteStackTop.theoryId << "," << rewriteStackTop.node << std::endl;
+ Trace("rewriter") << "Rewriter::rewriting: "
+ << rewriteStackTop.getTheoryId() << ","
+ << rewriteStackTop.node << std::endl;
// Before rewriting children we need to do a pre-rewrite of the node
if (rewriteStackTop.nextChild == 0) {
// Check if the pre-rewrite has already been done (it's in the cache)
- Node cached = Rewriter::getPreRewriteCache((TheoryId) rewriteStackTop.theoryId, rewriteStackTop.node);
+ Node cached = getPreRewriteCache(rewriteStackTop.getTheoryId(),
+ rewriteStackTop.node);
if (cached.isNull()) {
// Rewrite until fix-point is reached
for(;;) {
// Perform the pre-rewrite
- RewriteResponse response = Rewriter::callPreRewrite((TheoryId) rewriteStackTop.theoryId, rewriteStackTop.node);
+ RewriteResponse response =
+ d_theoryRewriters[rewriteStackTop.getTheoryId()]->preRewrite(
+ rewriteStackTop.node);
// Put the rewritten node to the top of the stack
rewriteStackTop.node = response.node;
TheoryId newTheory = theoryOf(rewriteStackTop.node);
// In the pre-rewrite, if changing theories, we just call the other theories pre-rewrite
- if (newTheory == (TheoryId) rewriteStackTop.theoryId && response.status == REWRITE_DONE) {
+ if (newTheory == rewriteStackTop.getTheoryId()
+ && response.status == REWRITE_DONE)
+ {
break;
}
rewriteStackTop.theoryId = newTheory;
}
// Cache the rewrite
- Rewriter::setPreRewriteCache((TheoryId) rewriteStackTop.originalTheoryId, rewriteStackTop.original, rewriteStackTop.node);
+ setPreRewriteCache(rewriteStackTop.getOriginalTheoryId(),
+ rewriteStackTop.original,
+ rewriteStackTop.node);
}
// Otherwise we're have already been pre-rewritten (in pre-rewrite cache)
else {
@@ -163,7 +165,8 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
rewriteStackTop.original =rewriteStackTop.node;
// Now it's time to rewrite the children, check if this has already been done
- Node cached = Rewriter::getPostRewriteCache((TheoryId) rewriteStackTop.theoryId, rewriteStackTop.node);
+ Node cached = getPostRewriteCache(rewriteStackTop.getTheoryId(),
+ rewriteStackTop.node);
// If not, go through the children
if(cached.isNull()) {
@@ -202,26 +205,33 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
// Done with all pre-rewriting, so let's do the post rewrite
for(;;) {
// Do the post-rewrite
- RewriteResponse response = Rewriter::callPostRewrite((TheoryId) rewriteStackTop.theoryId, rewriteStackTop.node);
+ RewriteResponse response =
+ d_theoryRewriters[rewriteStackTop.getTheoryId()]->postRewrite(
+ rewriteStackTop.node);
// We continue with the response we got
TheoryId newTheoryId = theoryOf(response.node);
- if (newTheoryId != (TheoryId) rewriteStackTop.theoryId || response.status == REWRITE_AGAIN_FULL) {
+ if (newTheoryId != rewriteStackTop.getTheoryId()
+ || response.status == REWRITE_AGAIN_FULL)
+ {
// In the post rewrite if we've changed theories, we must do a full rewrite
Assert(response.node != rewriteStackTop.node);
//TODO: this is not thread-safe - should make this assertion dependent on sequential build
#ifdef CVC4_ASSERTIONS
- Assert(s_rewriteStack->find(response.node) == s_rewriteStack->end());
- s_rewriteStack->insert(response.node);
+ Assert(d_rewriteStack->find(response.node) == d_rewriteStack->end());
+ d_rewriteStack->insert(response.node);
#endif
Node rewritten = rewriteTo(newTheoryId, response.node);
rewriteStackTop.node = rewritten;
#ifdef CVC4_ASSERTIONS
- s_rewriteStack->erase(response.node);
+ d_rewriteStack->erase(response.node);
#endif
break;
- } else if (response.status == REWRITE_DONE) {
+ }
+ else if (response.status == REWRITE_DONE)
+ {
#ifdef CVC4_ASSERTIONS
- RewriteResponse r2 = Rewriter::callPostRewrite(newTheoryId, response.node);
+ RewriteResponse r2 =
+ d_theoryRewriters[newTheoryId]->postRewrite(response.node);
Assert(r2.node == response.node);
#endif
rewriteStackTop.node = response.node;
@@ -229,15 +239,16 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
}
// Check for trivial rewrite loops of size 1 or 2
Assert(response.node != rewriteStackTop.node);
- Assert(Rewriter::callPostRewrite((TheoryId)rewriteStackTop.theoryId,
- response.node)
+ Assert(d_theoryRewriters[rewriteStackTop.getTheoryId()]
+ ->postRewrite(response.node)
.node
!= rewriteStackTop.node);
rewriteStackTop.node = response.node;
}
// We're done with the post rewrite, so we add to the cache
- Rewriter::setPostRewriteCache((TheoryId) rewriteStackTop.originalTheoryId, rewriteStackTop.original, rewriteStackTop.node);
-
+ setPostRewriteCache(rewriteStackTop.getOriginalTheoryId(),
+ rewriteStackTop.original,
+ rewriteStackTop.node);
} else {
// We were already in cache, so just remember it
rewriteStackTop.node = cached;
@@ -260,13 +271,13 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
}/* Rewriter::rewriteTo() */
void Rewriter::clearCaches() {
+ Rewriter& rewriter = getInstance();
+
#ifdef CVC4_ASSERTIONS
- if (s_rewriteStack != nullptr)
- {
- s_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