fixed failed bv regressions by refactoring out some rewrite rules from smt_engine.cpp

2 files changed, 18 insertions, 2 deletions

diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 1335f8f4a..23018605f 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -594,6 +594,14 @@ void TheoryBVRewriter::initializeRewrites() {
   d_rewriteTable [ kind::BITVECTOR_ROTATE_LEFT ] = RewriteRotateLeft;
 }
 
+Node TheoryBVRewriter::eliminateBVSDiv(TNode node) {
+  Node result = bv::LinearRewriteStrategy <
+    bv::RewriteRule<bv::SremEliminate>,
+    bv::RewriteRule<bv::SdivEliminate>,
+    bv::RewriteRule<bv::SmodEliminate>
+    >::apply(node);
+  return result; 
+}
 
 
 
diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h
index 59a2f90f6..3e7fc272b 100644
--- a/src/theory/bv/theory_bv_rewriter.h
+++ b/src/theory/bv/theory_bv_rewriter.h
@@ -83,10 +83,18 @@ public:
   static RewriteResponse postRewrite(TNode node);
 
   static RewriteResponse preRewrite(TNode node);
-
+  
   static void init();
   static void shutdown();
-  
+  /** 
+   * Temporary hack for devision-by-zero until we refactor theory code from
+   * smt engine. 
+   * 
+   * @param node 
+   * 
+   * @return 
+   */
+  static Node eliminateBVSDiv(TNode node); 
 };/* class TheoryBVRewriter */
 
 }/* CVC4::theory::bv namespace */