[BV] Fix strategy for rewriting `bvnot` (#8297)

Fixes #8240. The currenty strategy was returning REWRITE_DONE
incorrectly, e.g., when we had a term like (bvnot (bvnot (bvnot #b0)))
because EvalNot was applied before NotIdemp, so we did not evaluate
the innermost bvnot after removing the double bvnot. The commit
fixes the strategy s.t. we are allowed to return REWRITE_DONE.

diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index 330bdc85bcd0305acf5385b540190e47a086909f..a43d42d952b34282e12cf08520cbfd4e8d68ac7a 100644 (file)
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -923,7 +923,13 @@ bool RewriteRule<NotIdemp>::applies(TNode node) {
 template<> inline
 Node RewriteRule<NotIdemp>::apply(TNode node) {
   Debug("bv-rewrite") << "RewriteRule<NotIdemp>(" << node << ")" << std::endl;
-  return node[0][0];
+  TNode ret = node[0][0];
+  while (ret.getKind() == kind::BITVECTOR_NOT
+         && ret[0].getKind() == kind::BITVECTOR_NOT)
+  {
+    ret = ret[0][0];
+  }
+  return ret;
 }
 
 /* -------------------------------------------------------------------------- */

diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 9b755a23054d8e0dcd381b1c42461b9b7ada9287..a968243c7d427f8da62cc421df8ac8333b1afc9e 100644 (file)
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -225,16 +225,14 @@ RewriteResponse TheoryBVRewriter::RewriteITEBv(TNode node, bool prerewrite)
 
 RewriteResponse TheoryBVRewriter::RewriteNot(TNode node, bool prerewrite){
   Node resultNode = node;
-  
-  // // if(RewriteRule<NotXor>::applies(node)) {
-  // //   resultNode = RewriteRule<NotXor>::run<false>(node);
-  // //   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
-  // // }
-  resultNode = LinearRewriteStrategy
-    < RewriteRule<EvalNot>,
-      RewriteRule<NotIdemp>
-    >::apply(node);
-  
+
+  resultNode =
+      LinearRewriteStrategy<RewriteRule<NotIdemp>, RewriteRule<EvalNot>>::apply(
+          node);
+
+  // It is is safe to return REWRITE_DONE here, because `NotIdemp` removes all
+  // pairs of `bvnot` and then `EvalNot` evaluates the remaining `bvnot` if
+  // applicable.
   return RewriteResponse(REWRITE_DONE, resultNode); 
 }
 

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 45d3701fc3ebcca9297411957f3470dd7c7da6a3..5a1d8f832588fae3c45b27460161a1a77fd27b1f 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -449,6 +449,7 @@ set(regress_0_tests
   regress0/bv/issue3621.smt2
   regress0/bv/issue5396.smt2
   regress0/bv/issue8159-1-rewrite-bvneg.smt2
+  regress0/bv/issue8240-rewrite-bvnot.smt2
   regress0/bv/mul-neg-unsat.smt2
   regress0/bv/mul-negpow2.smt2
   regress0/bv/mult-pow2-negative.smt2

diff --git a/test/regress/regress0/bv/issue8240-rewrite-bvnot.smt2 b/test/regress/regress0/bv/issue8240-rewrite-bvnot.smt2
new file mode 100644 (file)
index 0000000..8e0e97e
--- /dev/null
+++ b/test/regress/regress0/bv/issue8240-rewrite-bvnot.smt2
@@ -0,0 +1,4 @@
+(set-logic QF_BV)
+(assert (bvsle (concat (_ bv1 1) (_ bv0 1) ((_ zero_extend 1) (_ bv0 1))) (concat (_ bv1 1) ((_ zero_extend 1) (_ bv0 1)) (bvnot (bvnot (bvnot (_ bv0 1)))))))
+(set-info :status sat)
+(check-sat)