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.

diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index faebe9cfda261b16ecea5c1a4e4e1cf98e7e3b83..0dbb51753258b71b9581d21d09529518a459ec39 100644 (file)
--- 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 c35f33f5347ee5d2faa263ec2696057d5976b784..a0a2c8c60cfcc331359ed3bfeaf3e3546052b2e1 100644 (file)
--- 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<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
  * 

diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 0b1b58f9aef538a5b6074b3b3e5c8710b6aab206..32df0c4e9654abc710868487c32ec24cccd2f0c9 100644 (file)
--- 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 1a33ee3a5a4b7ce2c4e4fa34379cb13f12e4782d..5c31c4fe12e6b33d24762d45d54484b6ecc6faa7 100644 (file)
--- 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 (file)
index 0000000..c6748b1
--- /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 (file)
index 0000000..7cc75ef
--- /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)