added bv inequality rewrite

3 files changed, 42 insertions, 2 deletions

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index f6092031c..441577c9e 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -548,6 +548,7 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu
 
 Node TheoryBV::ppRewrite(TNode t)
 {
+  Debug("bv-pp-rewrite") << "TheoryBV::ppRewrite " << t << "\n"; 
   Node res = t;
   if (RewriteRule<BitwiseEq>::applies(t)) {
     Node result = RewriteRule<BitwiseEq>::run<false>(t);
@@ -556,6 +557,9 @@ Node TheoryBV::ppRewrite(TNode t)
     std::vector<Node> equalities;
     Slicer::splitEqualities(t, equalities);
     res = utils::mkAnd(equalities);
+  } else if (RewriteRule<UltPlusOne>::applies(t)) {
+    Node result = RewriteRule<UltPlusOne>::run<false>(t);
+    res = Rewriter::rewrite(result);
   }
 
   // if(t.getKind() == kind::EQUAL &&
@@ -593,6 +597,7 @@ Node TheoryBV::ppRewrite(TNode t)
   if (options::bvAbstraction() && t.getType().isBoolean()) {
     d_abstractionModule->addInputAtom(res); 
   }
+  Debug("bv-pp-rewrite") << "to   " << res << "\n"; 
   return res;
 }
 
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index 9f01e46da..496e05c86 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -163,8 +163,9 @@ enum RewriteRuleId {
   XorSimplify,
   BitwiseSlicing,
   // rules to simplify bitblasting
-  BBPlusNeg
- };
+  BBPlusNeg,
+  UltPlusOne
+};
 
 
 inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) {
@@ -289,6 +290,7 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) {
   case BitwiseSlicing : out << "BitwiseSlicing"; return out;
   case ExtractSignExtend : out << "ExtractSignExtend"; return out;
   case MultDistrib: out << "MultDistrib"; return out;
+  case UltPlusOne: out << "UltPlusOne"; return out;
   default:
     Unreachable();
   }
@@ -510,6 +512,7 @@ struct AllRewriteRules {
   RewriteRule<BVToNatEliminate>  rule116;
   RewriteRule<IntToBVEliminate>  rule117;
   RewriteRule<MultDistrib> rule118;
+  RewriteRule<UltPlusOne> rule119;
 };
 
 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 db0d8bac8..1569fb008 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -1152,6 +1152,38 @@ Node RewriteRule<MultSlice>::apply(TNode node) {
   return utils::mkNode(kind::BITVECTOR_PLUS, term1, term2, term3); 
 }
 
+/** 
+ * x < y + 1 <=> (not y < x) and y != 1...1
+ * 
+ * @param node 
+ * 
+ * @return 
+ */
+template<> inline
+bool RewriteRule<UltPlusOne>::applies(TNode node) {
+  if (node.getKind() != kind::BITVECTOR_ULT) return false;
+  TNode x = node[0];
+  TNode y1 = node[1];
+  if (y1.getKind() != kind::BITVECTOR_PLUS) return false;
+  if (y1[0].getKind() != kind::CONST_BITVECTOR &&
+      y1[1].getKind() != kind::CONST_BITVECTOR)
+    return false;
+  TNode one = y1[0].getKind() == kind::CONST_BITVECTOR ? y1[0] : y1[1];
+  if (one != utils::mkConst(utils::getSize(one), 1)) return false;
+  return true; 
+}
+
+template<> inline
+Node RewriteRule<UltPlusOne>::apply(TNode node) {
+  Debug("bv-rewrite") << "RewriteRule<UltPlusOne>(" << node << ")" << std::endl;
+  TNode x = node[0];
+  TNode y1 = node[1];
+  TNode y = y1[0].getKind() != kind::CONST_BITVECTOR ? y1[0] : y1[1];
+  unsigned size = utils::getSize(x); 
+  Node not_y_eq_1 = utils::mkNode(kind::NOT, utils::mkNode(kind::EQUAL, y, utils::mkOnes(size)));
+  Node not_y_lt_x = utils::mkNode(kind::NOT, utils::mkNode(kind::BITVECTOR_ULT, y, x));
+  return utils::mkNode(kind::AND, not_y_eq_1, not_y_lt_x);
+}
 
 
 // /**