Return `REWRITE_AGAIN` after rewriting bvcomp (#6624)

This commit fixes an assertion failure in the rewriter on some of the
SMT-LIB QF_ABVFP benchmarks (the regression in this commit is the
minified version of
`non_incremental/QF_ABVFP/20170428-Liew-KLEE/imperial_gsl_benchmarks_statistics_klee.x86_64/query.14.smt2`).
The problem was that after applying the `BvComp` rewrite, the bit-vector
rewriter was returning `REWRITE_DONE` instead of `REWRITE_AGAIN`. The
rewrite simplifies expressions of the form `bvcomp(t, c)` where `c` is a
constant of bit-width 1. If `c` is zero, then the rewrite returns
`bvnot(t)`. This node can potentially be rewritten further, e.g., if `t`
is `bvnot(x)`. This commit fixes the response and adds the corresponding
tests.

diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index d0579703db066e37b27a1f04197469e157a74cff..476803c59202298bb4feeb9b1c28f7f793f6c023 100644 (file)
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -375,9 +375,13 @@ RewriteResponse TheoryBVRewriter::RewriteNor(TNode node, bool prerewrite) {
 
 RewriteResponse TheoryBVRewriter::RewriteComp(TNode node, bool prerewrite)
 {
-  Node resultNode =
-      LinearRewriteStrategy<RewriteRule<EvalComp>, RewriteRule<BvComp> >::apply(
-          node);
+  Node resultNode = LinearRewriteStrategy<RewriteRule<EvalComp>>::apply(node);
+
+  if (node == resultNode && RewriteRule<BvComp>::applies(node))
+  {
+    resultNode = RewriteRule<BvComp>::run<false>(node);
+    return RewriteResponse(REWRITE_AGAIN, resultNode);
+  }
 
   return RewriteResponse(REWRITE_DONE, resultNode);
 }

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index a3244ff4a752e4f63d1d1be267afdc31edfd83d7..817ddc2ba6e9d855fa35cb0810b357456f41859e 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -582,6 +582,7 @@ set(regress_0_tests
   regress0/fmf/tail_rec.smt2
   regress0/fp/abs-unsound.smt2
   regress0/fp/abs-unsound2.smt2
+  regress0/fp/bvcomp-rewrite.smt2
   regress0/fp/down-cast-RNA.smt2
   regress0/fp/ext-rew-test.smt2
   regress0/fp/from_ubv.smt2

diff --git a/test/regress/regress0/fp/bvcomp-rewrite.smt2 b/test/regress/regress0/fp/bvcomp-rewrite.smt2
new file mode 100644 (file)
index 0000000..7c14ee5
--- /dev/null
+++ b/test/regress/regress0/fp/bvcomp-rewrite.smt2
@@ -0,0 +1,5 @@
+(set-logic QF_FP)
+(declare-const x Float64)
+(assert (fp.isNaN (fp.sub roundNearestTiesToEven (fp.mul roundNearestTiesToEven x (fp (_ bv0 1) (_ bv2047 11) (_ bv1 52))) (fp.mul roundNearestTiesToEven x x))))
+(set-info :status sat)
+(check-sat)

diff --git a/test/unit/theory/theory_bv_rewriter_white.cpp b/test/unit/theory/theory_bv_rewriter_white.cpp
index 5ea8fa4dd95ff8709f3f1168d0f9141928810ba3..31d9cfac9efbc5f40799056ed8cc26e7cba73c43 100644 (file)
--- a/test/unit/theory/theory_bv_rewriter_white.cpp
+++ b/test/unit/theory/theory_bv_rewriter_white.cpp
@@ -79,5 +79,19 @@ TEST_F(TestTheoryWhiteBvRewriter, rewrite_bv_ite)
   Node nr = Rewriter::rewrite(n);
   ASSERT_EQ(nr, Rewriter::rewrite(nr));
 }
+
+TEST_F(TestTheoryWhiteBvRewriter, rewrite_bv_comp)
+{
+  TypeNode bvType = d_nodeManager->mkBitVectorType(1);
+  Node zero = d_nodeManager->mkConst(BitVector(1, 0u));
+  Node x = d_nodeManager->mkVar("x", bvType);
+  Node lhs = d_nodeManager->mkNode(BITVECTOR_NOT, x);
+  Node rhs = d_nodeManager->mkNode(BITVECTOR_AND, zero, zero);
+  Node n = d_nodeManager->mkNode(BITVECTOR_COMP, lhs, rhs);
+  Node nr = Rewriter::rewrite(n);
+  // bvcomp(bvnot(x), bvand(0, 0)) ---> x
+  ASSERT_EQ(nr, x);
+}
+
 }  // namespace test
 }  // namespace cvc5