From f41e705bcc7313664dc49ee8c0640457077bdc02 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 23 Feb 2022 08:23:54 -0800 Subject: [PATCH] [Rewriter] Do not attempt to rewrite constants (#8061) This commit changes our rewriter policy to not attempt to rewrite nodes with no children. --- src/theory/rewriter.cpp | 34 ++++++++++++++++++---------------- 1 file changed, 18 insertions(+), 16 deletions(-) diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index e1c49fc23..0ed442252 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -215,28 +215,29 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, rewriteStackTop.getTheoryId(), rewriteStackTop.d_node, tcpg); // Put the rewritten node to the top of the stack - rewriteStackTop.d_node = response.d_node; - TheoryId newTheory = theoryOf(rewriteStackTop.d_node); + TNode newNode = response.d_node; + TheoryId newTheory = theoryOf(newNode); + rewriteStackTop.d_node = newNode; + rewriteStackTop.d_theoryId = newTheory; // In the pre-rewrite, if changing theories, we just call the other // theories pre-rewrite. If the kind of the node was changed, then we // pre-rewrite again. - if (originalKind == rewriteStackTop.d_node.getKind() - && response.d_status == REWRITE_DONE) + if ((originalKind == newNode.getKind() + && response.d_status == REWRITE_DONE) + || newNode.getNumChildren() == 0) { if (Configuration::isAssertionBuild()) { // REWRITE_DONE should imply that no other pre-rewriting can be // done. - Node rewritten = rewriteStackTop.d_node; Node rewrittenAgain = - preRewrite(newTheory, rewritten, nullptr).d_node; - Assert(rewritten == rewrittenAgain) - << "Rewriter returned REWRITE_DONE for " << rewritten + preRewrite(newTheory, newNode, nullptr).d_node; + Assert(newNode == rewrittenAgain) + << "Rewriter returned REWRITE_DONE for " << newNode << " but it can be rewritten to " << rewrittenAgain; } break; } - rewriteStackTop.d_theoryId = newTheory; } // Cache the rewrite @@ -303,7 +304,8 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, rewriteStackTop.getTheoryId(), rewriteStackTop.d_node, tcpg); // We continue with the response we got - TheoryId newTheoryId = theoryOf(response.d_node); + TNode newNode = response.d_node; + TheoryId newTheoryId = theoryOf(newNode); if (newTheoryId != rewriteStackTop.getTheoryId() || response.d_status == REWRITE_AGAIN_FULL) { @@ -322,16 +324,16 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, #endif break; } - else if (response.d_status == REWRITE_DONE - && originalKind == response.d_node.getKind()) + else if ((response.d_status == REWRITE_DONE + && originalKind == newNode.getKind()) + || newNode.getNumChildren() == 0) { #ifdef CVC5_ASSERTIONS RewriteResponse r2 = - d_theoryRewriters[newTheoryId]->postRewrite(response.d_node); - Assert(r2.d_node == response.d_node) - << r2.d_node << " != " << response.d_node; + d_theoryRewriters[newTheoryId]->postRewrite(newNode); + Assert(r2.d_node == newNode) << r2.d_node << " != " << newNode; #endif - rewriteStackTop.d_node = response.d_node; + rewriteStackTop.d_node = newNode; break; } // Check for trivial rewrite loops of size 1 or 2 -- 2.30.2