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

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 1fc32917e207bd0ebba70275feabc35c3fb3036d..32557e7c8d6c0433c27860bc9660473de4d2197c 100644 (file)
--- 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 1335f8f4a0f3fa6e674c42fd399c7a7bc57beb50..23018605fb0681775db664e4ceca47af747fad82 100644 (file)
--- 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 59a2f90f6716d056f162415cdd2678c6eecbfa91..3e7fc272b3ab9299aa6e357a72f2c5873a5fa1f7 100644 (file)
--- 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 */