diff options
Diffstat (limited to 'src/theory/rewriter.cpp')
-rw-r--r-- | src/theory/rewriter.cpp | 125 |
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 */ |