From 740df5937639738a0238312dfb061643e62ba605 Mon Sep 17 00:00:00 2001
From: Liana Hadarean <lianahady@gmail.com>
Date: Tue, 13 Nov 2012 20:38:40 +0000
Subject: [PATCH] fixed failed bv regressions by refactoring out some rewrite
 rules from smt_engine.cpp

---
 src/smt/smt_engine.cpp               | 10 +++-------
 src/theory/bv/theory_bv_rewriter.cpp |  8 ++++++++
 src/theory/bv/theory_bv_rewriter.h   | 12 ++++++++++--
 3 files changed, 21 insertions(+), 9 deletions(-)

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 1fc32917e..32557e7c8 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -41,7 +41,7 @@
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "theory/theory_engine.h"
-#include "theory/bv/theory_bv_rewrite_rules.h"
+#include "theory/bv/theory_bv_rewriter.h"
 #include "proof/proof_manager.h"
 #include "util/proof.h"
 #include "util/boolean_simplification.h"
@@ -1195,16 +1195,12 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
 
   Node node = n;
   NodeManager* nm = d_smt.d_nodeManager;
-
+  // FIXME: this theory specific code should be factored out of the SmtEngine, somehow
   switch(k) {
   case kind::BITVECTOR_SDIV:
   case kind::BITVECTOR_SREM:
   case kind::BITVECTOR_SMOD: {
-    node = bv::LinearRewriteStrategy <
-      bv::RewriteRule<bv::SremEliminate>,
-      bv::RewriteRule<bv::SdivEliminate>,
-      bv::RewriteRule<bv::SmodEliminate>
-      >::apply(node);
+    node = bv::TheoryBVRewriter::eliminateBVSDiv(node);
     break;
   }
     
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 */
-- 
2.30.2