diff options
Diffstat (limited to 'src/theory/rewriter.cpp')
-rw-r--r-- | src/theory/rewriter.cpp | 59 |
1 files changed, 37 insertions, 22 deletions
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 0518c61a8..3380694e7 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -38,6 +38,24 @@ static TheoryId theoryOf(TNode node) { * 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; @@ -51,17 +69,6 @@ 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) { @@ -115,32 +122,36 @@ 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 = getPreRewriteCache((TheoryId)rewriteStackTop.theoryId, + Node cached = getPreRewriteCache(rewriteStackTop.getTheoryId(), rewriteStackTop.node); if (cached.isNull()) { // Rewrite until fix-point is reached for(;;) { // Perform the pre-rewrite RewriteResponse response = - d_theoryRewriters[(TheoryId)rewriteStackTop.theoryId]->preRewrite( + 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 - setPreRewriteCache((TheoryId)rewriteStackTop.originalTheoryId, + setPreRewriteCache(rewriteStackTop.getOriginalTheoryId(), rewriteStackTop.original, rewriteStackTop.node); } @@ -154,7 +165,7 @@ 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 = getPostRewriteCache((TheoryId)rewriteStackTop.theoryId, + Node cached = getPostRewriteCache(rewriteStackTop.getTheoryId(), rewriteStackTop.node); // If not, go through the children if(cached.isNull()) { @@ -195,11 +206,13 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { for(;;) { // Do the post-rewrite RewriteResponse response = - d_theoryRewriters[(TheoryId)rewriteStackTop.theoryId]->postRewrite( + 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 @@ -213,7 +226,9 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node 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 = d_theoryRewriters[newTheoryId]->postRewrite(response.node); @@ -224,14 +239,14 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { } // Check for trivial rewrite loops of size 1 or 2 Assert(response.node != rewriteStackTop.node); - Assert(d_theoryRewriters[(TheoryId)rewriteStackTop.theoryId] + 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 - setPostRewriteCache((TheoryId)rewriteStackTop.originalTheoryId, + setPostRewriteCache(rewriteStackTop.getOriginalTheoryId(), rewriteStackTop.original, rewriteStackTop.node); } else { |