From 7f67de1dc1492f12e14d46316dcdd680d753b58c Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 1 Mar 2022 01:07:56 -0800 Subject: [PATCH] [BV] Fix rewriter policy for `bvneg` (#8196) Our rewriter was returning `REWRITE_DONE` prematurely for `bvneg`. This commit makes the status returned more conservative. --- src/theory/bv/theory_bv_rewriter.cpp | 6 +++++- test/regress/CMakeLists.txt | 1 + test/regress/regress0/bv/issue8159-1-rewrite-bvneg.smt2 | 6 ++++++ 3 files changed, 12 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress0/bv/issue8159-1-rewrite-bvneg.smt2 diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index c85e57b65..9b755a230 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -486,7 +486,11 @@ RewriteResponse TheoryBVRewriter::RewriteNeg(TNode node, bool prerewrite) { } } - return RewriteResponse(REWRITE_DONE, resultNode); + // There are cases where we need to rewrite the resulting term again. For + // example, if we rewrite (bvneg (bvneg (bvneg #b0))) to (bvneg #b0) then we + // have to rewrite again. + return RewriteResponse(resultNode != node ? REWRITE_AGAIN : REWRITE_DONE, + resultNode); } RewriteResponse TheoryBVRewriter::RewriteUdiv(TNode node, bool prerewrite){ diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 984e0e8a7..95fe01c0f 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -446,6 +446,7 @@ set(regress_0_tests regress0/bv/issue-4130.smt2 regress0/bv/issue3621.smt2 regress0/bv/issue5396.smt2 + regress0/bv/issue8159-1-rewrite-bvneg.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/issue8159-1-rewrite-bvneg.smt2 b/test/regress/regress0/bv/issue8159-1-rewrite-bvneg.smt2 new file mode 100644 index 000000000..1512eaedb --- /dev/null +++ b/test/regress/regress0/bv/issue8159-1-rewrite-bvneg.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --incremental +(set-logic QF_BV) +(assert (= (_ bv1 1) (bvsmod (_ bv0 1) (bvneg (bvneg (_ bv0 1)))))) +(push) +(set-info :status unsat) +(check-sat) -- 2.30.2