From: Liana Hadarean <lianahady@gmail.com>
Date: Tue, 7 May 2013 01:46:30 +0000 (-0400)
Subject: fixed bv rewrite rule bug
X-Git-Tag: cvc5-1.0.0~7287^2~150
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9b035b4aedd977213a5f5acb6e8cb01bf160c415;p=cvc5.git

fixed bv rewrite rule bug
---

diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 7844e5b92..9c072444d 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -222,15 +222,16 @@ RewriteResponse TheoryBVRewriter::RewriteConcat(TNode node, bool preregister) {
 
 RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node, bool preregister){
   Node resultNode = node;
-  
-  resultNode = LinearRewriteStrategy
-    < RewriteRule<FlattenAssocCommut>,
-      RewriteRule<AndSimplify>,
-      RewriteRule<BitwiseSlicing>
-      >::apply(node);
+  if (!preregister) {
+    resultNode = LinearRewriteStrategy
+      < RewriteRule<FlattenAssocCommut>,
+        RewriteRule<AndSimplify>,
+        RewriteRule<BitwiseSlicing>
+        >::apply(node);
 
-  if (resultNode.getKind() != node.getKind()) {
-    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+    if (resultNode.getKind() != node.getKind()) {
+      return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+    }
   }
   
   return RewriteResponse(REWRITE_DONE, resultNode); 
@@ -238,39 +239,40 @@ RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node, bool preregister){
 
 RewriteResponse TheoryBVRewriter::RewriteOr(TNode node, bool preregister){
   Node resultNode = node;
+  if (! preregister) {
+    resultNode = LinearRewriteStrategy
+      < RewriteRule<FlattenAssocCommut>,
+        RewriteRule<OrSimplify>,
+        RewriteRule<BitwiseSlicing>
+        >::apply(node);
 
-  resultNode = LinearRewriteStrategy
-    < RewriteRule<FlattenAssocCommut>,
-      RewriteRule<OrSimplify>,
-      RewriteRule<BitwiseSlicing>
-    >::apply(node);
-
-  if (resultNode.getKind() != node.getKind()) {
-    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+    if (resultNode.getKind() != node.getKind()) {
+      return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+    }
   }
-  
   return RewriteResponse(REWRITE_DONE, resultNode); 
 }
 
 RewriteResponse TheoryBVRewriter::RewriteXor(TNode node, bool preregister) {
   Node resultNode = node;
-
-  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>
-    >::apply(node);
-
-  // this simplification introduces new terms and might require further
-  // rewriting
-  if (RewriteRule<XorOne>::applies(resultNode)) {
-    resultNode = RewriteRule<XorOne>::run<false> (resultNode);
-    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
-  }
-
-  if (resultNode.getKind() != node.getKind()) {
-    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+  if (! 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>
+        >::apply(node);
+    
+    // this simplification introduces new terms and might require further
+    // rewriting
+    if (RewriteRule<XorOne>::applies(resultNode)) {
+      resultNode = RewriteRule<XorOne>::run<false> (resultNode);
+      return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+    }
+    
+    if (resultNode.getKind() != node.getKind()) {
+      return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
+    }
   }
 
   return RewriteResponse(REWRITE_DONE, resultNode);