removed tracing code causing slowdown; cleaned up some code

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 6f450d08ec23dd095ff91ea6ea2cc61a3888d14f..4c31f3f4495d5b3433f8a5a17ec6367aecb98321 100644 (file)
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -173,14 +173,9 @@ void TheoryBV::check(Effort e)
     return;
   }
 
-  if (Theory::fullEffort(e)) {
-    Trace("bitvector-fulleffort") << "TheoryBV::fullEffort \n"; 
-    printFacts( Trace("bitvector-fulleffort") ); 
-  }
-  
   while (!done()) {
     TNode fact = get().assertion;
-    checkForLemma(fact); 
+    // checkForLemma(fact); 
     for (unsigned i = 0; i < d_subtheories.size(); ++i) {
       d_subtheories[i]->assertFact(fact); 
     }

diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
index 626116453c90b64e17433857564e6ee110535a61..cf36633fa30994836fd6b659f92912def826e503 100644 (file)
--- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
@@ -103,24 +103,6 @@ Node RewriteRule<SltEliminate>::apply(TNode node) {
   
 }
 
-// template <>
-// bool RewriteRule<SleEliminate>::applies(TNode node) {
-//   return (node.getKind() == kind::BITVECTOR_SLE); 
-// }
-
-// template <>
-// Node RewriteRule<SleEliminate>::apply(TNode node) {
-//   Debug("bv-rewrite") << "RewriteRule<SleEliminate>(" << node << ")" << std::endl;
-  
-//   unsigned size = utils::getSize(node[0]);
-//   Node pow_two = utils::mkConst(BitVector(size, Integer(1).multiplyByPow2(size - 1)));
-//   Node a = utils::mkNode(kind::BITVECTOR_PLUS, node[0], pow_two);
-//   Node b = utils::mkNode(kind::BITVECTOR_PLUS, node[1], pow_two);
-  
-//   return utils::mkNode(kind::BITVECTOR_ULE, a, b); 
-
-// }
-
 template <>
 bool RewriteRule<SleEliminate>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_SLE); 

diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 0775cb1f8292ef441621e327c905ae2a0cb1be6f..5a43e2c5713dbff58184f27270e6b65e5199dd89 100644 (file)
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -106,16 +106,16 @@ RewriteResponse TheoryBVRewriter::RewriteUle(TNode node, bool preregister){
       RewriteRule<UleMax>,
       RewriteRule<ZeroUle>,
       RewriteRule<UleZero>,
-      RewriteRule<UleSelf>,
-      RewriteRule<UleEliminate>
+      RewriteRule<UleSelf>//,
+      //      RewriteRule<UleEliminate>
       >::apply(node);
   return RewriteResponse(resultNode == node ? REWRITE_DONE : REWRITE_AGAIN, resultNode); 
 }
 
 RewriteResponse TheoryBVRewriter::RewriteSle(TNode node, bool preregister){
   Node resultNode = LinearRewriteStrategy
-    < RewriteRule <EvalSle>, 
-      RewriteRule <SleEliminate>
+    < RewriteRule <EvalSle>//, 
+      //      RewriteRule <SleEliminate>
       >::apply(node);
   return RewriteResponse(resultNode == node? REWRITE_DONE : REWRITE_AGAIN, resultNode); 
 }

diff --git a/src/theory/term_registration_visitor.h b/src/theory/term_registration_visitor.h
index d573213b7955b1fa3ef22f9a173755b182b02035..768508d2c31ef371cfd14e02750ca3ca81932fb1 100644 (file)
--- a/src/theory/term_registration_visitor.h
+++ b/src/theory/term_registration_visitor.h
@@ -95,6 +95,7 @@ public:
    * Notifies the engine of all the theories used.
    */
   bool done(TNode node);
+
 };