[Rewriter] Always rewrite again when kind changes (#8007)

Fixes cvc5/cvc5-projects#438. The rewriter
returned REWRITE_DONE prematurely when rewriting operators such as
bvand in certain cases. If only a single term was left after removing
duplicates from a bvand, the kind of the current node would change and
another pre-rewrite could apply, but the rewriter still returned
REWRITE_DONE. After adding an assertion in the rewriter that checks
that REWRITE_DONE implies that no other pre-rewrite applies, it was
discovered that not only the bit-vector rewriter has this issue, but
other rewriters, e.g., the Boolean rewriter, as well. This commit
changes our semantics for REWRITE_DONE to mean that no other rewrite
applies provided that the kind did not change. This makes it easier for
developers to decide when to return REWRITE_DONE, because it only
requires reasoning about rewrites that apply to a single kind.

diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index c3d58624499d925ab9a33cb6f7e1e1b1432f65c4..e1c49fc23457bbf353615dc5fd9cb23729a74843 100644 (file)
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -210,16 +210,30 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId,
         // Rewrite until fix-point is reached
         for(;;) {
           // Perform the pre-rewrite
+          Kind originalKind = rewriteStackTop.d_node.getKind();
           RewriteResponse response = preRewrite(
               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);
-          // In the pre-rewrite, if changing theories, we just call the other theories pre-rewrite
-          if (newTheory == rewriteStackTop.getTheoryId()
+          // 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 (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
+                  << " but it can be rewritten to " << rewrittenAgain;
+            }
             break;
           }
           rewriteStackTop.d_theoryId = newTheory;
@@ -284,6 +298,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId,
       // Done with all pre-rewriting, so let's do the post rewrite
       for(;;) {
         // Do the post-rewrite
+        Kind originalKind = rewriteStackTop.d_node.getKind();
         RewriteResponse response = postRewrite(
             rewriteStackTop.getTheoryId(), rewriteStackTop.d_node, tcpg);
 
@@ -307,7 +322,8 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId,
 #endif
           break;
         }
-        else if (response.d_status == REWRITE_DONE)
+        else if (response.d_status == REWRITE_DONE
+                 && originalKind == response.d_node.getKind())
         {
 #ifdef CVC5_ASSERTIONS
           RewriteResponse r2 =

diff --git a/src/theory/theory_rewriter.h b/src/theory/theory_rewriter.h
index d411dc73b416f60b15bcd5f479abd9ba352a585d..cc4eb67bc8e96202c39833e2fb94b41287f3fded 100644 (file)
--- a/src/theory/theory_rewriter.h
+++ b/src/theory/theory_rewriter.h
@@ -34,7 +34,11 @@ class Rewriter;
  */
 enum RewriteStatus
 {
-  /** The node is fully rewritten (no more rewrites apply) */
+  /**
+   * The node is fully rewritten (no more rewrites apply for the original
+   * kind). If the rewrite changes the kind, the rewriter will apply another
+   * round of rewrites.
+   */
   REWRITE_DONE,
   /** The node may be rewritten further */
   REWRITE_AGAIN,

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index fbe859eeb2c4e7e269c917309c3942f5d08ed1d5..e1efca4f50f3c1ea5a5787739e6b540e013701b6 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -437,6 +437,7 @@ set(regress_0_tests
   regress0/bv/pr4993-bvugt-bvurem-a.smt2
   regress0/bv/pr4993-bvugt-bvurem-b.smt2
   regress0/bv/proj-issue343.smt2
+  regress0/bv/proj-issue438-prerewrite-fixed-point.smt2
   regress0/bv/reset-assertions-assert-input.smt2
   regress0/bv/sizecheck.cvc.smt2
   regress0/bv/smtcompbug.smtv1.smt2
@@ -1712,6 +1713,7 @@ set(regress_1_tests
   regress1/bv/issue3776.smt2
   regress1/bv/issue3958.smt2
   regress1/bv/min-pp-rewrite-error.smt2
+  regress1/bv/proj-issue438-prerewrite-fixed-point-original.smt2
   regress1/bv/unsound1.smt2
   regress1/bvdiv2.smt2
   regress1/cee-bug0909-dd-scope.smt2

diff --git a/test/regress/regress0/bv/proj-issue438-prerewrite-fixed-point.smt2 b/test/regress/regress0/bv/proj-issue438-prerewrite-fixed-point.smt2
new file mode 100644 (file)
index 0000000..5ee3c45
--- /dev/null
+++ b/test/regress/regress0/bv/proj-issue438-prerewrite-fixed-point.smt2
@@ -0,0 +1,11 @@
+; Note: This benchmark triggers the same issue as
+; proj-issue438-prerewrite-fixed-point-original.smt2, but for a different node
+; kind.
+
+(set-logic QF_BV)
+(declare-const x (_ BitVec 3))
+(define-fun z () (_ BitVec 3) (bvadd x x))
+(define-fun s () (_ BitVec 3) (bvsub z z))
+(assert (bvule (bvnand s s) s))
+(set-info :status unsat)
+(check-sat)

diff --git a/test/regress/regress1/bv/proj-issue438-prerewrite-fixed-point-original.smt2 b/test/regress/regress1/bv/proj-issue438-prerewrite-fixed-point-original.smt2
new file mode 100644 (file)
index 0000000..62d769b
--- /dev/null
+++ b/test/regress/regress1/bv/proj-issue438-prerewrite-fixed-point-original.smt2
@@ -0,0 +1,5 @@
+(set-logic QF_BV)
+(declare-const T (_ BitVec 1))
+(assert (and (bvsle (_ bv0 32) (bvadd (bvadd (_ bv1 32) (_ bv0 32)) ((_ zero_extend 24) ((_ extract 15 8) (bvshl ((_ zero_extend 24) ((_ extract 15 8) (bvsub (bvxor ((_ zero_extend 24) ((_ extract 15 8) (bvsub ((_ zero_extend 24) ((_ extract 7 0) (bvxor (bvadd ((_ zero_extend 24) ((_ extract 7 0) ((_ extract 7 0) (bvsub (bvadd ((_ zero_extend 24) ((_ extract 7 0) (bvadd (_ bv0 32) ((_ zero_extend 24) ((_ extract 15 8) (bvsub (bvadd ((_ zero_extend 24) ((_ extract 7 0) (bvsub (bvxor (bvadd ((_ zero_extend 24) ((_ extract 7 0) (bvadd (_ bv0 32) ((_ zero_extend 24) (bvxor (bvxor (_ bv0 8) ((_ extract 7 0) ((_ extract 7 0) (bvxor (bvadd (_ bv0 32) ((_ zero_extend 24) ((_ extract 15 8) (bvsub ((_ zero_extend 24) ((_ extract 7 0) (bvsub (bvxor ((_ zero_extend 24) ((_ extract 7 0) (bvadd (_ bv0 32) (bvshl ((_ zero_extend 24) (bvxor (bvxor (_ bv0 8) ((_ extract 7 0) (bvadd (_ bv0 32) ((_ zero_extend 24) (bvxor (_ bv0 8) ((_ extract 7 0) (bvxor (bvadd (_ bv0 32) ((_ zero_extend 24) (bvxor (_ bv0 8) ((_ extract 7 0) (bvsub (_ bv0 32) ((_ zero_extend 24) ((_ zero_extend 7) T))))))) (_ bv0 32)))))))) (_ bv0 8))) (_ bv0 32))))) (_ bv0 32)) (_ bv1 32)))) (_ bv1 32))))) (_ bv0 32))))) (_ bv0 8)))))) (_ bv0 32)) (_ bv0 32)) (_ bv0 32)))) (_ bv0 32)) (_ bv1 32))))))) (_ bv0 32)) (_ bv0 32))))) (_ bv0 32)) (_ bv0 32)))) (_ bv1 32)))) (_ bv0 32)) (_ bv1 32)))) (_ bv1 32)))))) (= (_ bv0 32) (bvxor (_ bv0 32) (bvadd (bvadd (_ bv1 32) (_ bv0 32)) ((_ zero_extend 24) ((_ extract 15 8) (bvshl ((_ zero_extend 24) ((_ extract 15 8) (bvsub (bvxor ((_ zero_extend 24) ((_ extract 15 8) (bvsub ((_ zero_extend 24) ((_ extract 7 0) (bvxor (bvadd ((_ zero_extend 24) ((_ extract 7 0) ((_ extract 7 0) (bvsub (bvadd ((_ zero_extend 24) ((_ extract 7 0) (bvadd (_ bv0 32) ((_ zero_extend 24) ((_ extract 15 8) (bvsub (bvadd ((_ zero_extend 24) ((_ extract 7 0) (bvsub (bvxor (bvadd ((_ zero_extend 24) ((_ extract 7 0) (bvadd (_ bv0 32) ((_ zero_extend 24) (bvxor (bvxor (_ bv0 8) ((_ extract 7 0) ((_ extract 7 0) (bvxor (bvadd (_ bv0 32) ((_ zero_extend 24) ((_ extract 15 8) (bvsub ((_ zero_extend 24) ((_ extract 7 0) (bvsub (bvxor ((_ zero_extend 24) ((_ extract 7 0) (bvadd (_ bv0 32) (bvshl ((_ zero_extend 24) (bvxor (bvxor (_ bv0 8) ((_ extract 7 0) (bvadd (_ bv0 32) ((_ zero_extend 24) (bvxor (_ bv0 8) ((_ extract 7 0) (bvxor (bvadd (_ bv0 32) ((_ zero_extend 24) (bvxor (_ bv0 8) ((_ extract 7 0) (bvsub (_ bv0 32) ((_ zero_extend 24) ((_ zero_extend 7) T))))))) (_ bv0 32)))))))) (_ bv0 8))) (_ bv0 32))))) (_ bv0 32)) (_ bv1 32)))) (_ bv1 32))))) (_ bv0 32))))) (_ bv0 8)))))) (_ bv0 32)) (_ bv0 32)) (_ bv0 32)))) (_ bv0 32)) (_ bv1 32))))))) (_ bv0 32)) (_ bv0 32))))) (_ bv0 32)) (_ bv0 32)))) (_ bv1 32)))) (_ bv0 32)) (_ bv1 32)))) (_ bv1 32)))))))))
+(set-info :status unsat)
+(check-sat)