diff options
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules.h | 3 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_simplification.h | 36 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewriter.cpp | 6 | ||||
-rw-r--r-- | test/regress/CMakeLists.txt | 2 | ||||
-rw-r--r-- | test/regress/regress0/bv/pr4993-bvugt-bvurem-a.smt2 | 7 | ||||
-rw-r--r-- | test/regress/regress0/bv/pr4993-bvugt-bvurem-b.smt2 | 7 |
6 files changed, 58 insertions, 3 deletions
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<SdivEliminate> rule143; RewriteRule<SremEliminate> rule144; RewriteRule<SmodEliminate> rule145; + RewriteRule<UgtUrem> 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" @@ -1558,6 +1559,41 @@ Node RewriteRule<ShiftZero>::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<UgtUrem>::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<UgtUrem>::apply(TNode node) +{ + Debug("bv-rewrite") << "RewriteRule<UgtUrem>(" << 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 * * -a1 - a2 - ... - an + ak + .. ==> - (a1 + a2 + ... + an) + ak 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<UgtEliminate> - >::apply(node); + Node resultNode = + LinearRewriteStrategy<RewriteRule<UgtUrem>, + RewriteRule<UgtEliminate>>::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) |