Commit for the theory engine and rewriter changes. Changes are substantial and not yet finalized but I need to put it in to work further with the theory writers. Please check the files that you 'own'. Any comments or discussion is welcome. Further details will be coming in a follow up email later.

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;