1 files changed, 73 insertions, 5 deletions
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 566bf3a68..2f3538837 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -21,17 +21,17 @@
 #include "theory/bv/theory_bv_rewriter.h"
 #include "theory/bv/theory_bv_rewrite_rules.h"
 #include "theory/bv/theory_bv_rewrite_rules_core.h"
+#include "theory/bv/theory_bv_rewrite_rules_arith.h"
 
 using namespace CVC4;
 using namespace CVC4::theory;
 using namespace CVC4::theory::bv;
 
 RewriteResponse TheoryBVRewriter::postRewrite(TNode node) {
-
+  
   BVDebug("bitvector") << "TheoryBV::postRewrite(" << node << ")" << std::endl;
-
-  Node result;
-
+    
+  Node result = node;
   if (node.getKind() == kind::CONST_BITVECTOR || (node.getKind() != kind::EQUAL && Theory::isLeafOf(node, THEORY_BV))) {
     result = node;
   } else {
@@ -67,10 +67,78 @@ RewriteResponse TheoryBVRewriter::postRewrite(TNode node) {
                   RewriteRule<FailEq>,
                   // If both sides are equal equality is true
                   RewriteRule<SimplifyEq>,
-                  // Normalize the equalities
+                  // Eliminate the equalities
                   RewriteRule<ReflexivityEq>
                 >::apply(node);
       break;
+    case kind::BITVECTOR_UGT:
+      result = LinearRewriteStrategy <
+                  RewriteRule<UgtToUlt>
+               >::apply(node);
+      break;
+
+    case kind::BITVECTOR_UGE:
+      result = LinearRewriteStrategy <
+                  RewriteRule<UgeToUle>
+               >::apply(node);
+      break;
+    case kind::BITVECTOR_SGT:
+      result = LinearRewriteStrategy <
+                  RewriteRule<SgtToSlt>
+               >::apply(node);
+      break;
+    case kind::BITVECTOR_SGE:
+      result = LinearRewriteStrategy <
+                  RewriteRule<SgeToSle>
+               >::apply(node);
+      break;
+    case kind::BITVECTOR_REPEAT:
+      result = LinearRewriteStrategy <
+                  RewriteRule<RepeatEliminate>
+               >::apply(node);
+      break;
+    case kind::BITVECTOR_ROTATE_RIGHT:
+      result = LinearRewriteStrategy <
+                  RewriteRule<RotateRightEliminate>
+               >::apply(node);
+      break;
+    case kind::BITVECTOR_ROTATE_LEFT:
+      result = LinearRewriteStrategy <
+                  RewriteRule<RotateLeftEliminate>
+               >::apply(node);
+      break;
+    case kind::BITVECTOR_NAND:
+      result = LinearRewriteStrategy <
+                  RewriteRule<NandEliminate>
+               >::apply(node);
+      break;
+    case kind::BITVECTOR_NOR:
+      result = LinearRewriteStrategy <
+                  RewriteRule<NorEliminate>
+               >::apply(node);
+      break;
+
+    case kind::BITVECTOR_SDIV:
+      result = LinearRewriteStrategy <
+                  RewriteRule<SdivEliminate>
+               >::apply(node);
+      break;
+  case kind::BITVECTOR_SREM:
+      result = LinearRewriteStrategy <
+                  RewriteRule<SremEliminate>
+               >::apply(node);
+     break;
+    case kind::BITVECTOR_SMOD:
+      result = LinearRewriteStrategy <
+                  RewriteRule<SmodEliminate>
+                >::apply(node);
+      break;
+    case kind::BITVECTOR_ZERO_EXTEND:
+      result = LinearRewriteStrategy <
+                  RewriteRule<ZeroExtendEliminate>
+                >::apply(node);
+      break;
+      
     default:
       // TODO: figure out when this is an operator
       result = node;