merged master

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 4c31f3f4495d5b3433f8a5a17ec6367aecb98321..4803fd62e680955484f6feaeaba0c9995d287f66 100644 (file)
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -156,7 +156,6 @@ void TheoryBV::checkForLemma(TNode fact) {
 
 void TheoryBV::check(Effort e)
 {
-  Trace("bitvector") <<"TheoryBV::check (" << e << ")\n"; 
   Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;
   if (options::bitvectorEagerBitblast()) {
     return;
@@ -175,7 +174,7 @@ void TheoryBV::check(Effort e)
 
   while (!done()) {
     TNode fact = get().assertion;
-    // checkForLemma(fact); 
+       checkForLemma(fact); 
     for (unsigned i = 0; i < d_subtheories.size(); ++i) {
       d_subtheories[i]->assertFact(fact); 
     }
@@ -280,7 +279,7 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu
 Node TheoryBV::ppRewrite(TNode t)
 {
   if (RewriteRule<BitwiseEq>::applies(t)) {
-       Node result = RewriteRule<BitwiseEq>::run<false>(t);
+    Node result = RewriteRule<BitwiseEq>::run<false>(t);
     return Rewriter::rewrite(result);
   }
 

diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 22e3d0507deae7ab5aa245cd2bcd02dcd787be2d..708206d28119128bcb9af7231bcb4603fc485fda 100644 (file)
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -99,8 +99,6 @@ private:
   /** Index of the next literal to propagate */
   context::CDO<unsigned> d_literalsToPropagateIndex;
 
-
-  
   /**
    * Keeps a map from nodes to the subtheory that propagated it so that we can explain it
    * properly.

diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 5a43e2c5713dbff58184f27270e6b65e5199dd89..7844e5b923a8934c9027511940ad46fff1b9b187 100644 (file)
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -77,9 +77,7 @@ RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node, bool preregister) {
       // if both arguments are constants evaluates
       RewriteRule<UltZero>
       // a < 0 rewrites to false
-  //    RewriteRule<UltOne>,
-  //    RewriteRule<ZeroUlt>
-      >::apply(node);
+       >::apply(node);
   
   return RewriteResponse(REWRITE_DONE, resultNode); 
 }
@@ -87,8 +85,7 @@ RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node, bool preregister) {
 RewriteResponse TheoryBVRewriter::RewriteSlt(TNode node, bool preregister){
   Node resultNode = LinearRewriteStrategy
     < RewriteRule < EvalSlt >
-     // RewriteRule < SltZero >
-      >::apply(node);
+       >::apply(node);
 
   return RewriteResponse(REWRITE_DONE, resultNode); 
 
@@ -106,16 +103,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); 
 }