From d036ca9091767e31b41fc76afabd0cc6c451f153 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 4 Feb 2022 18:15:22 -0600 Subject: [PATCH] Fix another rewrite involving iand (#8054) Fixes #8052. --- src/theory/arith/arith_rewriter.cpp | 6 ++++-- test/regress/CMakeLists.txt | 1 + test/regress/regress1/nl/issue8052-iand-rewrite.smt2 | 5 +++++ 3 files changed, 10 insertions(+), 2 deletions(-) create mode 100644 test/regress/regress1/nl/issue8052-iand-rewrite.smt2 diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 7d4bd4b83..abef4eec3 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -732,8 +732,10 @@ RewriteResponse ArithRewriter::postRewriteIAnd(TNode t) } else if (t[0] == t[1]) { - // ((_ iand k) x x) ---> x - return RewriteResponse(REWRITE_DONE, t[0]); + // ((_ iand k) x x) ---> (mod x 2^k) + Node twok = nm->mkConstInt(Rational(Integer(2).pow(bsize))); + Node ret = nm->mkNode(kind::INTS_MODULUS, t[0], twok); + return RewriteResponse(REWRITE_AGAIN, ret); } // simplifications involving constants for (unsigned i = 0; i < 2; i++) diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index e1efca4f5..13c5e3094 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1880,6 +1880,7 @@ set(regress_1_tests regress1/nl/issue5662-nl-tc-min.smt2 regress1/nl/issue7924-sqrt-partial.smt2 regress1/nl/issue8016-iand-rewrite.smt2 + regress1/nl/issue8052-iand-rewrite.smt2 regress1/nl/metitarski-1025.smt2 regress1/nl/metitarski-3-4.smt2 regress1/nl/metitarski_3_4_2e.smt2 diff --git a/test/regress/regress1/nl/issue8052-iand-rewrite.smt2 b/test/regress/regress1/nl/issue8052-iand-rewrite.smt2 new file mode 100644 index 000000000..c4d715090 --- /dev/null +++ b/test/regress/regress1/nl/issue8052-iand-rewrite.smt2 @@ -0,0 +1,5 @@ +(set-logic ALL) +(set-info :status unsat) +(declare-fun v () Int) +(assert (exists ((V Int)) (and (= 2 v) (= v ((_ iand 1) v v))))) +(check-sat) -- 2.30.2