added some bv rewrite rules

6 files changed, 98 insertions, 18 deletions

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index c46af5196..326eab36a 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -254,7 +254,7 @@ Node TheoryBV::ppRewrite(TNode t)
   //   return Rewriter::rewrite(result);
   // }
 
-  if (options::bitvectorCoreSolver() && t.getKind() == kind::EQUAL) {
+  if (/*options::bitvectorCoreSolver() && */t.getKind() == kind::EQUAL) {
     std::vector<Node> equalities;
     Slicer::splitEqualities(t, equalities);
     return utils::mkAnd(equalities); 
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index e9a3494f0..cff85b92b 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -125,6 +125,10 @@ enum RewriteRuleId {
   UremOne,
   UremSelf,
   ShiftZero,
+
+  UltOne,
+  SltZero, 
+  ZeroUlt,
   
   /// normalization rules
   ExtractBitwise,
@@ -262,7 +266,10 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) {
   case OrSimplify : out << "OrSimplify"; return out;
   case XorSimplify : out << "XorSimplify"; return out;
   case NegPlus : out << "NegPlus"; return out;
-  case BBPlusNeg : out << "BBPlusNeg"; return out; 
+  case BBPlusNeg : out << "BBPlusNeg"; return out;
+  case UltOne : out << "UltOne"; return out;
+  case SltZero : out << "SltZero"; return out;
+  case ZeroUlt : out << "ZeroUlt"; return out; 
   default:
     Unreachable();
   }
@@ -477,6 +484,9 @@ struct AllRewriteRules {
   RewriteRule<BBPlusNeg> rule111;
   RewriteRule<SolveEq> rule112;
   RewriteRule<BitwiseEq> rule113;
+  RewriteRule<UltOne> rule114;
+  RewriteRule<SltZero> rule115;
+  
 };
 
 template<> inline
diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
index 06ddc215d..b466aceae 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
@@ -103,6 +103,24 @@ Node RewriteRule<SltEliminate>::apply(TNode node) {
   
 }
 
+// template <>
+// bool RewriteRule<SleEliminate>::applies(TNode node) {
+//   return (node.getKind() == kind::BITVECTOR_SLE); 
+// }
+
+// template <>
+// Node RewriteRule<SleEliminate>::apply(TNode node) {
+//   Debug("bv-rewrite") << "RewriteRule<SleEliminate>(" << node << ")" << std::endl;
+  
+//   unsigned size = utils::getSize(node[0]);
+//   Node pow_two = utils::mkConst(BitVector(size, Integer(1).multiplyByPow2(size - 1)));
+//   Node a = utils::mkNode(kind::BITVECTOR_PLUS, node[0], pow_two);
+//   Node b = utils::mkNode(kind::BITVECTOR_PLUS, node[1], pow_two);
+  
+//   return utils::mkNode(kind::BITVECTOR_ULE, a, b); 
+
+// }
+
 template <>
 bool RewriteRule<SleEliminate>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_SLE); 
@@ -111,16 +129,14 @@ bool RewriteRule<SleEliminate>::applies(TNode node) {
 template <>
 Node RewriteRule<SleEliminate>::apply(TNode node) {
   Debug("bv-rewrite") << "RewriteRule<SleEliminate>(" << node << ")" << std::endl;
-  
-  unsigned size = utils::getSize(node[0]);
-  Node pow_two = utils::mkConst(BitVector(size, Integer(1).multiplyByPow2(size - 1)));
-  Node a = utils::mkNode(kind::BITVECTOR_PLUS, node[0], pow_two);
-  Node b = utils::mkNode(kind::BITVECTOR_PLUS, node[1], pow_two);
-  
-  return utils::mkNode(kind::BITVECTOR_ULE, a, b); 
-  
+
+  TNode a = node[0];
+  TNode b = node[1];
+  Node b_slt_a = utils::mkNode(kind::BITVECTOR_SLT, b, a);
+  return utils::mkNode(kind::NOT, b_slt_a); 
 }
 
+
 template <>
 bool RewriteRule<CompEliminate>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_COMP); 
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index bcfb189af..d660dde29 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -524,6 +524,25 @@ Node RewriteRule<LteSelf>::apply(TNode node) {
 }
 
 /**
+ * ZeroUlt
+ *
+ * 0 < a ==> a != 0
+ */
+
+template<> inline
+bool RewriteRule<ZeroUlt>::applies(TNode node) {
+  return (node.getKind() == kind::BITVECTOR_ULT &&
+          node[0] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(0))));
+}
+
+template<> inline
+Node RewriteRule<ZeroUlt>::apply(TNode node) {
+  Debug("bv-rewrite") << "RewriteRule<ZeroUlt>(" << node << ")" << std::endl;
+  return utils::mkNode(kind::NOT, utils::mkNode(kind::EQUAL, node[0], node[1])); 
+}
+
+
+/**
  * UltZero
  *
  * a < 0 ==> false
@@ -541,6 +560,42 @@ Node RewriteRule<UltZero>::apply(TNode node) {
   return utils::mkFalse(); 
 }
 
+
+/**
+ * 
+ */
+template<> inline
+bool RewriteRule<UltOne>::applies(TNode node) {
+  return (node.getKind() == kind::BITVECTOR_ULT &&
+          node[1] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(1))));
+}
+
+template<> inline
+Node RewriteRule<UltOne>::apply(TNode node) {
+  Debug("bv-rewrite") << "RewriteRule<UltOne>(" << node << ")" << std::endl;
+  return utils::mkNode(kind::EQUAL, node[0], utils::mkConst(BitVector(utils::getSize(node[0]), 0u))); 
+}
+
+/**
+ * 
+ */
+template<> inline
+bool RewriteRule<SltZero>::applies(TNode node) {
+  return (node.getKind() == kind::BITVECTOR_SLT &&
+          node[1] == utils::mkConst(BitVector(utils::getSize(node[0]), Integer(0))));
+}
+
+template<> inline
+Node RewriteRule<SltZero>::apply(TNode node) {
+  Debug("bv-rewrite") << "RewriteRule<UltZero>(" << node << ")" << std::endl;
+  unsigned size = utils::getSize(node[0]); 
+  Node most_significant_bit = utils::mkExtract(node[0], size - 1, size - 1);
+  Node one = utils::mkConst(BitVector(1, 1u));
+  
+  return utils::mkNode(kind::EQUAL, most_significant_bit, one); 
+}
+
+
 /**
  * UltSelf
  *
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index a712a8391..07499d01a 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -75,8 +75,10 @@ RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node, bool preregister) {
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<EvalUlt>,
       // if both arguments are constants evaluates
-      RewriteRule<UltZero>
+      RewriteRule<UltZero>,
       // a < 0 rewrites to false
+      RewriteRule<UltOne>,
+      RewriteRule<ZeroUlt>
       >::apply(node);
   
   return RewriteResponse(REWRITE_DONE, resultNode); 
@@ -84,7 +86,8 @@ RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node, bool preregister) {
 
 RewriteResponse TheoryBVRewriter::RewriteSlt(TNode node, bool preregister){
   Node resultNode = LinearRewriteStrategy
-    < RewriteRule < EvalSlt >
+    < RewriteRule < EvalSlt >,
+      RewriteRule < SltZero >
       >::apply(node);
 
   return RewriteResponse(REWRITE_DONE, resultNode); 
@@ -110,7 +113,8 @@ RewriteResponse TheoryBVRewriter::RewriteUle(TNode node, bool preregister){
 
 RewriteResponse TheoryBVRewriter::RewriteSle(TNode node, bool preregister){
   Node resultNode = LinearRewriteStrategy
-    < RewriteRule < EvalSle >
+    < RewriteRule <EvalSle>,
+      RewriteRule <SleEliminate>
       >::apply(node);
 
   return RewriteResponse(REWRITE_DONE, resultNode); 
diff --git a/src/theory/term_registration_visitor.h b/src/theory/term_registration_visitor.h
index 5f89af9c6..d573213b7 100644
--- a/src/theory/term_registration_visitor.h
+++ b/src/theory/term_registration_visitor.h
@@ -95,11 +95,6 @@ public:
    * Notifies the engine of all the theories used.
    */
   bool done(TNode node);
-  ~PreRegisterVisitor() {
-    for (TNodeToTheorySetMap::const_iterator it = d_visited.begin(); it != d_visited.end(); ++it) {
-      std::cout << it->first <<"\n"; 
-    }
-  }
 };