From: lianah <lianahady@gmail.com>
Date: Tue, 30 Apr 2013 19:52:40 +0000 (-0400)
Subject: updated the author name
X-Git-Tag: cvc5-1.0.0~7295
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a6cbb4dd9f8c8e5d53f0d4b77e177bfa4cc2fb92;p=cvc5.git

updated the author name
---

diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index 035bd4469..2da4dfa6a 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -1120,7 +1120,7 @@ template<> inline
 Node RewriteRule<BitwiseSlicing>::apply(TNode node) {
   Debug("bv-rewrite") << "RewriteRule<BitwiseSlicing>(" << node << ")" << std::endl;
   // get the constant
-  bool found_constant = false;
+  bool found_constant CVC4_UNUSED = false ;
   TNode constant;
   std::vector<Node> other_children; 
   for (unsigned i = 0; i < node.getNumChildren(); ++i) {
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 44c498947..0775cb1f8 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -177,10 +177,10 @@ RewriteResponse TheoryBVRewriter::RewriteExtract(TNode node, bool preregister) {
     return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
   }
 
-  // if (RewriteRule<ExtractSignExtend>::applies(node)) {
-  //   resultNode = RewriteRule<ExtractSignExtend>::run<false>(node);
-  //   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
-  // }
+  if (RewriteRule<ExtractSignExtend>::applies(node)) {
+    resultNode = RewriteRule<ExtractSignExtend>::run<false>(node);
+    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+  }
 
   if (RewriteRule<ExtractBitwise>::applies(node)) {
     resultNode = RewriteRule<ExtractBitwise>::run<false>(node);
@@ -228,8 +228,8 @@ RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node, bool preregister){
   
   resultNode = LinearRewriteStrategy
     < RewriteRule<FlattenAssocCommut>,
-      RewriteRule<AndSimplify>//,
-      //      RewriteRule<BitwiseSlicing>
+      RewriteRule<AndSimplify>,
+      RewriteRule<BitwiseSlicing>
       >::apply(node);
 
   if (resultNode.getKind() != node.getKind()) {
@@ -244,8 +244,8 @@ RewriteResponse TheoryBVRewriter::RewriteOr(TNode node, bool preregister){
 
   resultNode = LinearRewriteStrategy
     < RewriteRule<FlattenAssocCommut>,
-      RewriteRule<OrSimplify>//,
-      //      RewriteRule<BitwiseSlicing>
+      RewriteRule<OrSimplify>,
+      RewriteRule<BitwiseSlicing>
     >::apply(node);
 
   if (resultNode.getKind() != node.getKind()) {
@@ -261,8 +261,8 @@ RewriteResponse TheoryBVRewriter::RewriteXor(TNode node, bool preregister) {
   resultNode = LinearRewriteStrategy
     < RewriteRule<FlattenAssocCommut>, // flatten the expression 
       RewriteRule<XorSimplify>,        // simplify duplicates and constants
-      RewriteRule<XorZero>//,            // checks if the constant part is zero and eliminates it
-      //      RewriteRule<BitwiseSlicing>
+      RewriteRule<XorZero>,            // checks if the constant part is zero and eliminates it
+      RewriteRule<BitwiseSlicing>
     >::apply(node);
 
   // this simplification introduces new terms and might require further