fixed bv rewrite blow-up

diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 9c072444dfb589e84187e4d4895a14d2aa2a3433..621ae25c030dfa08568fc59dc1272084c723cc84 100644 (file)
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -70,7 +70,7 @@ RewriteResponse TheoryBVRewriter::postRewrite(TNode node) {
   return res; 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node, bool preregister) {
+RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node, bool prerewrite) {
   // reduce common subexpressions on both sides
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<EvalUlt>,
@@ -82,7 +82,7 @@ RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node, bool preregister) {
   return RewriteResponse(REWRITE_DONE, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteSlt(TNode node, bool preregister){
+RewriteResponse TheoryBVRewriter::RewriteSlt(TNode node, bool prerewrite){
   Node resultNode = LinearRewriteStrategy
     < RewriteRule < EvalSlt >
        >::apply(node);
@@ -97,7 +97,7 @@ RewriteResponse TheoryBVRewriter::RewriteSlt(TNode node, bool preregister){
   // return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteUle(TNode node, bool preregister){
+RewriteResponse TheoryBVRewriter::RewriteUle(TNode node, bool prerewrite){
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<EvalUle>,
       RewriteRule<UleMax>,
@@ -109,7 +109,7 @@ RewriteResponse TheoryBVRewriter::RewriteUle(TNode node, bool preregister){
   return RewriteResponse(resultNode == node ? REWRITE_DONE : REWRITE_AGAIN, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteSle(TNode node, bool preregister){
+RewriteResponse TheoryBVRewriter::RewriteSle(TNode node, bool prerewrite){
   Node resultNode = LinearRewriteStrategy
     < RewriteRule <EvalSle>, 
       RewriteRule <SleEliminate>
@@ -117,7 +117,7 @@ RewriteResponse TheoryBVRewriter::RewriteSle(TNode node, bool preregister){
   return RewriteResponse(resultNode == node? REWRITE_DONE : REWRITE_AGAIN, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteUgt(TNode node, bool preregister){
+RewriteResponse TheoryBVRewriter::RewriteUgt(TNode node, bool prerewrite){
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<UgtEliminate>
     >::apply(node);
@@ -125,7 +125,7 @@ RewriteResponse TheoryBVRewriter::RewriteUgt(TNode node, bool preregister){
   return RewriteResponse(REWRITE_AGAIN, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteSgt(TNode node, bool preregister){
+RewriteResponse TheoryBVRewriter::RewriteSgt(TNode node, bool prerewrite){
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<SgtEliminate>
       //RewriteRule<SltEliminate>
@@ -134,7 +134,7 @@ RewriteResponse TheoryBVRewriter::RewriteSgt(TNode node, bool preregister){
   return RewriteResponse(REWRITE_AGAIN, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteUge(TNode node, bool preregister){
+RewriteResponse TheoryBVRewriter::RewriteUge(TNode node, bool prerewrite){
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<UgeEliminate>
     >::apply(node);
@@ -142,7 +142,7 @@ RewriteResponse TheoryBVRewriter::RewriteUge(TNode node, bool preregister){
   return RewriteResponse(REWRITE_AGAIN, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteSge(TNode node, bool preregister){
+RewriteResponse TheoryBVRewriter::RewriteSge(TNode node, bool prerewrite){
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<SgeEliminate>
       //      RewriteRule<SleEliminate>
@@ -151,7 +151,7 @@ RewriteResponse TheoryBVRewriter::RewriteSge(TNode node, bool preregister){
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteNot(TNode node, bool preregister){
+RewriteResponse TheoryBVRewriter::RewriteNot(TNode node, bool prerewrite){
   Node resultNode = node;
   
   if(RewriteRule<NotXor>::applies(node)) {
@@ -166,7 +166,7 @@ RewriteResponse TheoryBVRewriter::RewriteNot(TNode node, bool preregister){
   return RewriteResponse(REWRITE_DONE, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteExtract(TNode node, bool preregister) {
+RewriteResponse TheoryBVRewriter::RewriteExtract(TNode node, bool prerewrite) {
   Node resultNode = node;
 
   if (RewriteRule<ExtractConcat>::applies(node)) {
@@ -206,7 +206,7 @@ RewriteResponse TheoryBVRewriter::RewriteExtract(TNode node, bool preregister) {
 }
 
 
-RewriteResponse TheoryBVRewriter::RewriteConcat(TNode node, bool preregister) {
+RewriteResponse TheoryBVRewriter::RewriteConcat(TNode node, bool prerewrite) {
   
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<ConcatFlatten>,
@@ -220,15 +220,18 @@ RewriteResponse TheoryBVRewriter::RewriteConcat(TNode node, bool preregister) {
    return RewriteResponse(REWRITE_DONE, resultNode);  
 }
 
-RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node, bool preregister){
+RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node, bool prerewrite) {
   Node resultNode = node;
-  if (!preregister) {
+  resultNode = LinearRewriteStrategy
+    < RewriteRule<FlattenAssocCommut>,
+      RewriteRule<AndSimplify>
+      >::apply(node);
+
+  if (!prerewrite) {
     resultNode = LinearRewriteStrategy
-      < RewriteRule<FlattenAssocCommut>,
-        RewriteRule<AndSimplify>,
-        RewriteRule<BitwiseSlicing>
+      < RewriteRule<BitwiseSlicing>
         >::apply(node);
-
+  
     if (resultNode.getKind() != node.getKind()) {
       return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
     }
@@ -237,39 +240,41 @@ RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node, bool preregister){
   return RewriteResponse(REWRITE_DONE, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteOr(TNode node, bool preregister){
+RewriteResponse TheoryBVRewriter::RewriteOr(TNode node, bool prerewrite){
   Node resultNode = node;
-  if (! preregister) {
+  resultNode = LinearRewriteStrategy
+    < RewriteRule<FlattenAssocCommut>,
+      RewriteRule<OrSimplify>
+      >::apply(node);
+
+  if (!prerewrite) {
     resultNode = LinearRewriteStrategy
-      < RewriteRule<FlattenAssocCommut>,
-        RewriteRule<OrSimplify>,
-        RewriteRule<BitwiseSlicing>
+      < RewriteRule<BitwiseSlicing>
         >::apply(node);
-
+    
     if (resultNode.getKind() != node.getKind()) {
       return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
     }
   }
+  
   return RewriteResponse(REWRITE_DONE, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteXor(TNode node, bool preregister) {
+RewriteResponse TheoryBVRewriter::RewriteXor(TNode node, bool prerewrite) {
   Node resultNode = node;
-  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);
+
+  if (!prerewrite) {
     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<XorOne>, 
+      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); 
     }
@@ -278,7 +283,7 @@ RewriteResponse TheoryBVRewriter::RewriteXor(TNode node, bool preregister) {
   return RewriteResponse(REWRITE_DONE, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteXnor(TNode node, bool preregister) {
+RewriteResponse TheoryBVRewriter::RewriteXnor(TNode node, bool prerewrite) {
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<XnorEliminate>
     >::apply(node);
@@ -286,7 +291,7 @@ RewriteResponse TheoryBVRewriter::RewriteXnor(TNode node, bool preregister) {
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteNand(TNode node, bool preregister) {
+RewriteResponse TheoryBVRewriter::RewriteNand(TNode node, bool prerewrite) {
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<NandEliminate>
       >::apply(node);
@@ -294,7 +299,7 @@ RewriteResponse TheoryBVRewriter::RewriteNand(TNode node, bool preregister) {
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteNor(TNode node, bool preregister) {
+RewriteResponse TheoryBVRewriter::RewriteNor(TNode node, bool prerewrite) {
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<NorEliminate>
     >::apply(node);
@@ -302,7 +307,7 @@ RewriteResponse TheoryBVRewriter::RewriteNor(TNode node, bool preregister) {
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteComp(TNode node, bool preregister) {
+RewriteResponse TheoryBVRewriter::RewriteComp(TNode node, bool prerewrite) {
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<CompEliminate>
       >::apply(node);
@@ -310,7 +315,7 @@ RewriteResponse TheoryBVRewriter::RewriteComp(TNode node, bool preregister) {
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteMult(TNode node, bool preregister) {
+RewriteResponse TheoryBVRewriter::RewriteMult(TNode node, bool prerewrite) {
   Node resultNode = node; 
 
   resultNode = LinearRewriteStrategy
@@ -320,7 +325,7 @@ RewriteResponse TheoryBVRewriter::RewriteMult(TNode node, bool preregister) {
     >::apply(node);
 
   // only apply if every subterm was already rewritten 
-  if (!preregister) {
+  if (!prerewrite) {
     // distributes multiplication by constant over +, - and unary -
     if(RewriteRule<MultDistribConst>::applies(resultNode)) {
       resultNode = RewriteRule<MultDistribConst>::run<false>(resultNode);
@@ -335,23 +340,19 @@ RewriteResponse TheoryBVRewriter::RewriteMult(TNode node, bool preregister) {
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewritePlus(TNode node, bool preregister) {
-  if (preregister) {
-    return RewriteResponse(REWRITE_DONE, node);
-  }
+RewriteResponse TheoryBVRewriter::RewritePlus(TNode node, bool prerewrite) {
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<FlattenAssocCommut>, 
       RewriteRule<PlusCombineLikeTerms>
-      // RewriteRule<PlusLiftConcat> 
       >::apply(node);
-  if (resultNode == node) {
+  if (prerewrite || node == resultNode) {
     return RewriteResponse(REWRITE_DONE, resultNode);
-  } else {
-    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
   }
+  
+  return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteSub(TNode node, bool preregister){
+RewriteResponse TheoryBVRewriter::RewriteSub(TNode node, bool prerewrite){
   // return RewriteResponse(REWRITE_DONE, node); 
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<SubEliminate>
@@ -360,7 +361,7 @@ RewriteResponse TheoryBVRewriter::RewriteSub(TNode node, bool preregister){
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteNeg(TNode node, bool preregister) {
+RewriteResponse TheoryBVRewriter::RewriteNeg(TNode node, bool prerewrite) {
   Node resultNode = node; 
   
   resultNode = LinearRewriteStrategy
@@ -374,7 +375,7 @@ RewriteResponse TheoryBVRewriter::RewriteNeg(TNode node, bool preregister) {
     return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
   }
   
-  if(!preregister) {
+  if(!prerewrite) {
     if (RewriteRule<NegMult>::applies(node)) {
       resultNode = RewriteRule<NegMult>::run<false>(node);
       return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
@@ -385,7 +386,7 @@ RewriteResponse TheoryBVRewriter::RewriteNeg(TNode node, bool preregister) {
 }
 
 
-RewriteResponse TheoryBVRewriter::RewriteUdivTotal(TNode node, bool preregister){
+RewriteResponse TheoryBVRewriter::RewriteUdivTotal(TNode node, bool prerewrite){
   Node resultNode = node;
 
   if(RewriteRule<UdivPow2>::applies(node)) {
@@ -402,7 +403,7 @@ RewriteResponse TheoryBVRewriter::RewriteUdivTotal(TNode node, bool preregister)
   return RewriteResponse(REWRITE_DONE, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteUremTotal(TNode node, bool preregister) {
+RewriteResponse TheoryBVRewriter::RewriteUremTotal(TNode node, bool prerewrite) {
   Node resultNode = node;
 
   if(RewriteRule<UremPow2>::applies(node)) {
@@ -418,7 +419,7 @@ RewriteResponse TheoryBVRewriter::RewriteUremTotal(TNode node, bool preregister)
   return RewriteResponse(REWRITE_DONE, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteSmod(TNode node, bool preregister) {
+RewriteResponse TheoryBVRewriter::RewriteSmod(TNode node, bool prerewrite) {
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<SmodEliminate>
       >::apply(node);
@@ -426,7 +427,7 @@ RewriteResponse TheoryBVRewriter::RewriteSmod(TNode node, bool preregister) {
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteSdiv(TNode node, bool preregister) {
+RewriteResponse TheoryBVRewriter::RewriteSdiv(TNode node, bool prerewrite) {
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<SdivEliminate>
       >::apply(node);
@@ -434,14 +435,14 @@ RewriteResponse TheoryBVRewriter::RewriteSdiv(TNode node, bool preregister) {
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteSrem(TNode node, bool preregister) {
+RewriteResponse TheoryBVRewriter::RewriteSrem(TNode node, bool prerewrite) {
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<SremEliminate>
        >::apply(node);
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteShl(TNode node, bool preregister) {
+RewriteResponse TheoryBVRewriter::RewriteShl(TNode node, bool prerewrite) {
   Node resultNode = node; 
   if(RewriteRule<ShlByConst>::applies(node)) {
     resultNode = RewriteRule<ShlByConst>::run <false> (node);
@@ -456,7 +457,7 @@ RewriteResponse TheoryBVRewriter::RewriteShl(TNode node, bool preregister) {
   return RewriteResponse(REWRITE_DONE, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteLshr(TNode node, bool preregister) {
+RewriteResponse TheoryBVRewriter::RewriteLshr(TNode node, bool prerewrite) {
   Node resultNode = node; 
   if(RewriteRule<LshrByConst>::applies(node)) {
     resultNode = RewriteRule<LshrByConst>::run <false> (node);
@@ -471,7 +472,7 @@ RewriteResponse TheoryBVRewriter::RewriteLshr(TNode node, bool preregister) {
   return RewriteResponse(REWRITE_DONE, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteAshr(TNode node, bool preregister) {
+RewriteResponse TheoryBVRewriter::RewriteAshr(TNode node, bool prerewrite) {
   Node resultNode = node; 
   if(RewriteRule<AshrByConst>::applies(node)) {
     resultNode = RewriteRule<AshrByConst>::run <false> (node);
@@ -487,7 +488,7 @@ RewriteResponse TheoryBVRewriter::RewriteAshr(TNode node, bool preregister) {
 }
 
 
-RewriteResponse TheoryBVRewriter::RewriteRepeat(TNode node, bool preregister) {
+RewriteResponse TheoryBVRewriter::RewriteRepeat(TNode node, bool prerewrite) {
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<RepeatEliminate >
     >::apply(node);
@@ -495,7 +496,7 @@ RewriteResponse TheoryBVRewriter::RewriteRepeat(TNode node, bool preregister) {
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteZeroExtend(TNode node, bool preregister){
+RewriteResponse TheoryBVRewriter::RewriteZeroExtend(TNode node, bool prerewrite){
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<ZeroExtendEliminate >
     >::apply(node);
@@ -503,7 +504,7 @@ RewriteResponse TheoryBVRewriter::RewriteZeroExtend(TNode node, bool preregister
   return RewriteResponse(REWRITE_AGAIN, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteSignExtend(TNode node, bool preregister) {
+RewriteResponse TheoryBVRewriter::RewriteSignExtend(TNode node, bool prerewrite) {
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<EvalSignExtend>
     >::apply(node);
@@ -513,7 +514,7 @@ RewriteResponse TheoryBVRewriter::RewriteSignExtend(TNode node, bool preregister
 }
 
 
-RewriteResponse TheoryBVRewriter::RewriteRotateRight(TNode node, bool preregister) {
+RewriteResponse TheoryBVRewriter::RewriteRotateRight(TNode node, bool prerewrite) {
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<RotateRightEliminate >
     >::apply(node);
@@ -521,7 +522,7 @@ RewriteResponse TheoryBVRewriter::RewriteRotateRight(TNode node, bool preregiste
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteRotateLeft(TNode node, bool preregister){
+RewriteResponse TheoryBVRewriter::RewriteRotateLeft(TNode node, bool prerewrite){
   Node resultNode = LinearRewriteStrategy
     < RewriteRule<RotateLeftEliminate >
       >::apply(node);
@@ -529,8 +530,8 @@ RewriteResponse TheoryBVRewriter::RewriteRotateLeft(TNode node, bool preregister
   return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteEqual(TNode node, bool preregister) {
-  if (preregister) {
+RewriteResponse TheoryBVRewriter::RewriteEqual(TNode node, bool prerewrite) {
+  if (prerewrite) {
     Node resultNode = LinearRewriteStrategy
       < RewriteRule<FailEq>,
         RewriteRule<SimplifyEq>,