[Rewriter] Do not attempt to rewrite constants (#8061)

This commit changes our rewriter policy to not attempt to rewrite nodes
with no children.

diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index e1c49fc23457bbf353615dc5fd9cb23729a74843..0ed442252aa207157d264acb084ae9c26cd1d487 100644 (file)
--- 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