1 files changed, 0 insertions, 58 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 69ff48721..c9e7c397e 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -19,7 +19,6 @@
 
 #include "theory/bv/theory_bv.h"
 #include "theory/bv/theory_bv_utils.h"
-#include "theory/bv/theory_bv_rewrite_rules.h"
 
 #include "theory/theory_engine.h"
 
@@ -41,63 +40,6 @@ void TheoryBV::preRegisterTerm(TNode node) {
   }
 }
 
-RewriteResponse TheoryBV::postRewrite(TNode node, bool topLevel) {
-
-  Debug("bitvector") << "TheoryBV::postRewrite(" << node << ", topLevel = " << (topLevel? "true" : "false") << ")" << std::endl;
-
-  Node result;
-
-  if (node.getKind() == kind::CONST_BITVECTOR /* || isLeaf(n)) */)
-    result = node;
-  else {
-    switch (node.getKind()) {
-    case kind::BITVECTOR_CONCAT:
-      result = LinearRewriteStrategy<
-                  // Flatten the top level concatenations
-                  CoreRewriteRules::ConcatFlatten,
-                  // Merge the adjacent extracts on non-constants
-                  CoreRewriteRules::ConcatExtractMerge,
-                  // Merge the adjacent extracts on constants
-                  CoreRewriteRules::ConcatConstantMerge,
-                  // At this point only Extract-Whole could apply, if the result is only one extract
-                  // or at some sub-expression if the result is a concatenation.
-                  ApplyRuleToChildren<kind::BITVECTOR_CONCAT, CoreRewriteRules::ExtractWhole>
-               >::apply(node);
-      break;
-    case kind::BITVECTOR_EXTRACT:
-      result = LinearRewriteStrategy<
-                  // Extract over a constant gives a constant
-                  CoreRewriteRules::ExtractConstant,
-                  // Extract over an extract is simplified to one extract
-                  CoreRewriteRules::ExtractExtract,
-                  // Extract over a concatenation is distributed to the appropriate concatenations
-                  CoreRewriteRules::ExtractConcat,
-                  // At this point only Extract-Whole could apply
-                  CoreRewriteRules::ExtractWhole
-                >::apply(node);
-      break;
-    case kind::EQUAL:
-      result = LinearRewriteStrategy<
-                  // Two distinct values rewrite to false
-                  CoreRewriteRules::FailEq,
-                  // If both sides are equal equality is true
-                  CoreRewriteRules::SimplifyEq
-                >::apply(node);
-      break;
-    default:
-      // TODO: figure out when this is an operator
-      result = node;
-      break;
-      // Unhandled();
-    }
-  }
-
-  Debug("bitvector") << "TheoryBV::postRewrite(" << node << ", topLevel = " << (topLevel? "true" : "false") << ") => " << result << std::endl;
-
-  return RewriteComplete(result);
-}
-
-
 void TheoryBV::check(Effort e) {
 
   Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;