From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Tue, 15 Mar 2022 22:20:09 +0000 (-0700)
Subject: [BV] Fix strategy for rewriting `bvnot` (#8297)
X-Git-Tag: cvc5-1.0.0~250
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=55e02fa8ed99769cdc3546090f42daaeb326b639;p=cvc5.git

[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 330bdc85b..a43d42d95 100644
--- 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 9b755a230..a968243c7 100644
--- 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 45d3701fc..5a1d8f832 100644
--- 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
index 000000000..8e0e97eb2
--- /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)