From: lianah <lianahady@gmail.com>
Date: Thu, 2 May 2013 18:38:46 +0000 (-0400)
Subject: merged master
X-Git-Tag: cvc5-1.0.0~7289
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a5d1513db484457ac64a96711088aca1460af62e;p=cvc5.git

merged master
---

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 4c31f3f44..4803fd62e 100644
--- 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 22e3d0507..708206d28 100644
--- 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 5a43e2c57..7844e5b92 100644
--- 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); 
 }