From 19ff08d652de2890eee4674d2a6debe10e879f1f Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 4 Sep 2020 00:58:03 +0200 Subject: [PATCH] Added a new rule to simplify (bvugt (bvurem T x) x) (#4993) Motivated by #4936, this PR adds a new BV rewrite rule: (bvugt (bvurem T x) x) ==> (ite (= x 0) (bvugt T 0) false) Fixes #4936. --- src/theory/bv/theory_bv_rewrite_rules.h | 3 ++ .../theory_bv_rewrite_rules_simplification.h | 36 +++++++++++++++++++ src/theory/bv/theory_bv_rewriter.cpp | 6 ++-- test/regress/CMakeLists.txt | 2 ++ .../regress0/bv/pr4993-bvugt-bvurem-a.smt2 | 7 ++++ .../regress0/bv/pr4993-bvugt-bvurem-b.smt2 | 7 ++++ 6 files changed, 58 insertions(+), 3 deletions(-) create mode 100644 test/regress/regress0/bv/pr4993-bvugt-bvurem-a.smt2 create mode 100644 test/regress/regress0/bv/pr4993-bvugt-bvurem-b.smt2 diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index faebe9cfd..0dbb51753 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -156,6 +156,7 @@ enum RewriteRuleId UremOne, UremSelf, ShiftZero, + UgtUrem, UltOne, SltZero, @@ -324,6 +325,7 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case UremOne : out << "UremOne"; return out; case UremSelf : out << "UremSelf"; return out; case ShiftZero : out << "ShiftZero"; return out; + case UgtUrem: out << "UgtUrem"; return out; case SubEliminate : out << "SubEliminate"; return out; case CompEliminate : out << "CompEliminate"; return out; case XnorEliminate : out << "XnorEliminate"; return out; @@ -609,6 +611,7 @@ struct AllRewriteRules { RewriteRule rule143; RewriteRule rule144; RewriteRule rule145; + RewriteRule rule146; }; template<> inline diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index c35f33f53..a0a2c8c60 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -19,6 +19,7 @@ #pragma once +#include "options/bv_options.h" #include "theory/bv/theory_bv_rewrite_rules.h" #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" @@ -1557,6 +1558,41 @@ Node RewriteRule::apply(TNode node) { /* -------------------------------------------------------------------------- */ +/** + * UgtUrem + * + * (bvugt (bvurem T x) x) + * ==> (ite (= x 0_k) (bvugt T x) false) + * ==> (and (=> (= x 0_k) (bvugt T x)) (=> (not (= x 0_k)) false)) + * ==> (and (=> (= x 0_k) (bvugt T x)) (= x 0_k)) + * ==> (and (bvugt T x) (= x 0_k)) + * ==> (and (bvugt T 0_k) (= x 0_k)) + */ + +template <> +inline bool RewriteRule::applies(TNode node) +{ + return (options::bitvectorDivByZeroConst() + && node.getKind() == kind::BITVECTOR_UGT + && node[0].getKind() == kind::BITVECTOR_UREM_TOTAL + && node[0][1] == node[1]); +} + +template <> +inline Node RewriteRule::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule(" << node << ")" << std::endl; + const Node& T = node[0][0]; + const Node& x = node[1]; + Node zero = utils::mkConst(utils::getSize(x), 0); + NodeManager* nm = NodeManager::currentNM(); + return nm->mkNode(kind::AND, + nm->mkNode(kind::EQUAL, x, zero), + nm->mkNode(kind::BITVECTOR_UGT, T, zero)); +} + +/* -------------------------------------------------------------------------- */ + /** * BBPlusNeg * diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 0b1b58f9a..32df0c4e9 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -121,9 +121,9 @@ RewriteResponse TheoryBVRewriter::RewriteSle(TNode node, bool prerewrite){ } RewriteResponse TheoryBVRewriter::RewriteUgt(TNode node, bool prerewrite){ - Node resultNode = LinearRewriteStrategy - < RewriteRule - >::apply(node); + Node resultNode = + LinearRewriteStrategy, + RewriteRule>::apply(node); return RewriteResponse(REWRITE_AGAIN, resultNode); } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 1a33ee3a5..5c31c4fe1 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -366,6 +366,8 @@ set(regress_0_tests regress0/bv/mul-neg-unsat.smt2 regress0/bv/mul-negpow2.smt2 regress0/bv/mult-pow2-negative.smt2 + regress0/bv/pr4993-bvugt-bvurem-a.smt2 + regress0/bv/pr4993-bvugt-bvurem-b.smt2 regress0/bv/sizecheck.cvc regress0/bv/smtcompbug.smtv1.smt2 regress0/bv/test-bv_intro_pow2.smt2 diff --git a/test/regress/regress0/bv/pr4993-bvugt-bvurem-a.smt2 b/test/regress/regress0/bv/pr4993-bvugt-bvurem-a.smt2 new file mode 100644 index 000000000..c6748b19e --- /dev/null +++ b/test/regress/regress0/bv/pr4993-bvugt-bvurem-a.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --bv-div-zero-const --no-check-unsat-cores +(set-logic QF_BV) +(set-info :status unsat) +(declare-const x (_ BitVec 4)) +(declare-const y (_ BitVec 4)) +(assert (not (= (bvugt (bvurem y x) x) (ite (= x #x0) (bvugt y #x0) false)))) +(check-sat) diff --git a/test/regress/regress0/bv/pr4993-bvugt-bvurem-b.smt2 b/test/regress/regress0/bv/pr4993-bvugt-bvurem-b.smt2 new file mode 100644 index 000000000..7cc75ef62 --- /dev/null +++ b/test/regress/regress0/bv/pr4993-bvugt-bvurem-b.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --no-bv-div-zero-const --no-check-unsat-cores +(set-logic QF_BV) +(set-info :status sat) +(declare-const x (_ BitVec 4)) +(declare-const y (_ BitVec 4)) +(assert (not (= (bvugt (bvurem y x) x) (ite (= x #x0) (bvugt y #x0) false)))) +(check-sat) -- 2.30.2