From: lianah <lianahady@gmail.com>
Date: Tue, 7 May 2013 20:32:07 +0000 (-0400)
Subject: one more fix for rewrites
X-Git-Tag: cvc5-1.0.0~7287^2~143
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=778004b0fe366f6ecfb53a594bd5be335a2dc4b7;p=cvc5.git

one more fix for rewrites
---

diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 621ae25c0..534347c4a 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -230,7 +230,7 @@ RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node, bool prerewrite) {
   if (!prerewrite) {
     resultNode = LinearRewriteStrategy
       < RewriteRule<BitwiseSlicing>
-        >::apply(node);
+        >::apply(resultNode);
   
     if (resultNode.getKind() != node.getKind()) {
       return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
@@ -250,7 +250,7 @@ RewriteResponse TheoryBVRewriter::RewriteOr(TNode node, bool prerewrite){
   if (!prerewrite) {
     resultNode = LinearRewriteStrategy
       < RewriteRule<BitwiseSlicing>
-        >::apply(node);
+        >::apply(resultNode);
     
     if (resultNode.getKind() != node.getKind()) {
       return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
@@ -273,7 +273,7 @@ RewriteResponse TheoryBVRewriter::RewriteXor(TNode node, bool prerewrite) {
     resultNode = LinearRewriteStrategy
       < RewriteRule<XorOne>, 
       RewriteRule <BitwiseSlicing>
-        >::apply(node);
+        >::apply(resultNode);
     
     if (resultNode.getKind() != node.getKind()) {
       return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
@@ -341,15 +341,24 @@ RewriteResponse TheoryBVRewriter::RewriteMult(TNode node, bool prerewrite) {
 }
 
 RewriteResponse TheoryBVRewriter::RewritePlus(TNode node, bool prerewrite) {
-  Node resultNode = LinearRewriteStrategy
-    < RewriteRule<FlattenAssocCommut>, 
+  Node resultNode = node;
+  if (prerewrite) {
+    resultNode = LinearRewriteStrategy
+      < RewriteRule<FlattenAssocCommut>
+        >::apply(node);
+    return RewriteResponse(REWRITE_DONE, resultNode);
+  }
+  
+  resultNode =  LinearRewriteStrategy
+    < RewriteRule<FlattenAssocCommut>,
       RewriteRule<PlusCombineLikeTerms>
       >::apply(node);
-  if (prerewrite || node == resultNode) {
-    return RewriteResponse(REWRITE_DONE, resultNode);
+
+  if (node != resultNode) {
+    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
   }
   
-  return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+  return RewriteResponse(REWRITE_DONE, resultNode); 
 }
 
 RewriteResponse TheoryBVRewriter::RewriteSub(TNode node, bool prerewrite){