From 55e02fa8ed99769cdc3546090f42daaeb326b639 Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Tue, 15 Mar 2022 15:20:09 -0700
Subject: [PATCH] [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.
---
 .../theory_bv_rewrite_rules_simplification.h   |  8 +++++++-
 src/theory/bv/theory_bv_rewriter.cpp           | 18 ++++++++----------
 test/regress/CMakeLists.txt                    |  1 +
 .../regress0/bv/issue8240-rewrite-bvnot.smt2   |  4 ++++
 4 files changed, 20 insertions(+), 11 deletions(-)
 create mode 100644 test/regress/regress0/bv/issue8240-rewrite-bvnot.smt2

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)
-- 
2.30.2