Fixes more problems in bv rewrites

diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index f8399041da15eac55c8dea3e78629ca8aec05ea8..896133e464d4e7f707601d910e146971cbdb01fc 100644 (file)
--- 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 c2a5780a3e687a6d401aee1a8ee7146654e9b227..955acf707c37dc39112ba17720339fb8ae16069d 100644 (file)
--- 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 {