From c6aecebe573aeed87ef0661b38af7c3cbc7d641f Mon Sep 17 00:00:00 2001
From: Clark Barrett <barrett@cs.nyu.edu>
Date: Wed, 13 Jun 2012 13:54:14 +0000
Subject: [PATCH] Fixes more problems in bv rewrites

---
 .../theory_bv_rewrite_rules_normalization.h   | 28 +++++++++++++------
 src/theory/bv/theory_bv_rewriter.cpp          |  9 +++---
 2 files changed, 25 insertions(+), 12 deletions(-)

diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index f8399041d..896133e46 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -134,11 +134,20 @@ Node RewriteRule<ExtractArith2>::apply(TNode node) {
 
 template<> inline
 bool RewriteRule<FlattenAssocCommut>::applies(TNode node) {
-  return (node.getKind() == kind::BITVECTOR_PLUS ||
-          node.getKind() == kind::BITVECTOR_MULT ||
-          node.getKind() == kind::BITVECTOR_OR ||
-          node.getKind() == kind::BITVECTOR_XOR ||
-          node.getKind() == kind::BITVECTOR_AND);
+  Kind kind = node.getKind();
+  if (kind != kind::BITVECTOR_PLUS &&
+      kind != kind::BITVECTOR_MULT &&
+      kind != kind::BITVECTOR_OR &&
+      kind != kind::BITVECTOR_XOR &&
+      kind != kind::BITVECTOR_AND)
+    return false;
+  TNode::iterator child_it = node.begin();
+  for(; child_it != node.end(); ++child_it) {
+    if ((*child_it).getKind() == kind) {
+      return true;
+    }
+  }
+  return false;
 }
 
 
@@ -329,9 +338,12 @@ bool RewriteRule<MultSimplify>::applies(TNode node) {
       return true;
     }
   }
-  if ((*child_it).isConst() &&
-      (*child_it).getConst<BitVector>() == BitVector(utils::getSize(node), (unsigned) 0)) {
-    return true;
+  if ((*child_it).isConst()) {
+    BitVector bv = (*child_it).getConst<BitVector>();
+    if (bv == BitVector(utils::getSize(node), (unsigned) 0) ||
+        bv == BitVector(utils::getSize(node), (unsigned) 1)) {
+      return true;
+    }
   }
   return false;
 }
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index c2a5780a3..955acf707 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -319,13 +319,14 @@ RewriteResponse TheoryBVRewriter::RewriteMult(TNode node, bool preregister) {
 }
 
 RewriteResponse TheoryBVRewriter::RewritePlus(TNode node, bool preregister) {
-  Node resultNode = node;
-
-  resultNode = LinearRewriteStrategy
+  if (preregister) {
+    return RewriteResponse(REWRITE_DONE, node);
+  }
+  Node resultNode = LinearRewriteStrategy
     < RewriteRule<FlattenAssocCommut>, 
       RewriteRule<PlusCombineLikeTerms>
       // RewriteRule<PlusLiftConcat> 
-      >::apply(resultNode);
+      >::apply(node);
   if (resultNode == node) {
     return RewriteResponse(REWRITE_DONE, resultNode);
   } else {
-- 
2.30.2