From: Andres Noetzli Date: Fri, 4 Feb 2022 19:04:07 +0000 (-0800) Subject: [Rewriter] Always rewrite again when kind changes (#8007) X-Git-Tag: cvc5-1.0.0~451 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f76b1dc5757518da2baa61c3924940cc776242ad;p=cvc5.git [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 c3d586244..e1c49fc23 100644 --- 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 d411dc73b..cc4eb67bc 100644 --- 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 fbe859eeb..e1efca4f5 100644 --- 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 index 000000000..5ee3c45c2 --- /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 index 000000000..62d769bc2 --- /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)