Fixed inefficiency in bit-vector rewrite rule.

diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index bc9095f03cda54cefb11226d163944a596e2149b..3cc1c323c27d2ad4c699204abb0f6cebb2ec3c7b 100644 (file)
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -152,6 +152,7 @@ enum RewriteRuleId {
   NotOr,  // not sure why this would help (not done)
   NotXor, // not sure why this would help (not done)
   FlattenAssocCommut,
+  FlattenAssocCommutNoDuplicates,
   PlusCombineLikeTerms,
   MultSimplify,
   MultDistribConst,
@@ -270,7 +271,8 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) {
   case SignExtendEliminate :            out << "SignExtendEliminate";             return out;
   case NotIdemp :                  out << "NotIdemp"; return out;
   case UleSelf:                    out << "UleSelf"; return out; 
-  case FlattenAssocCommut:     out << "FlattenAssocCommut"; return out; 
+  case FlattenAssocCommut:     out << "FlattenAssocCommut"; return out;
+  case FlattenAssocCommutNoDuplicates:     out << "FlattenAssocCommutNoDuplicates"; return out; 
   case PlusCombineLikeTerms: out << "PlusCombineLikeTerms"; return out;
   case MultSimplify: out << "MultSimplify"; return out;
   case MultDistribConst: out << "MultDistribConst"; return out;
@@ -485,8 +487,9 @@ struct AllRewriteRules {
   RewriteRule<SubEliminate> rule82; 
   RewriteRule<XorOne> rule83;
   RewriteRule<XorZero> rule84;
-  RewriteRule<MultPow2> rule87;
   RewriteRule<MultSlice> rule85;
+  RewriteRule<FlattenAssocCommutNoDuplicates> rule86;
+  RewriteRule<MultPow2> rule87;
   RewriteRule<ExtractMultLeadingBit> rule88;
   RewriteRule<NegIdemp> rule91;
   RewriteRule<UdivPow2> rule92;

diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index 21b59fa8ca8c3bd1a7cf86ebe6bd826c5564b8fb..bc1b92dce3f022202c9f050da6e35146d4aac7d4 100644 (file)
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -995,6 +995,51 @@ Node RewriteRule<AndSimplify>::apply(TNode node) {
   return utils::mkSortedNode(kind::BITVECTOR_AND, children); 
 }
 
+template<> inline
+bool RewriteRule<FlattenAssocCommutNoDuplicates>::applies(TNode node) {
+  Kind kind = node.getKind();
+  if (kind != kind::BITVECTOR_OR &&
+      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;
+}
+  
+template<> inline
+Node RewriteRule<FlattenAssocCommutNoDuplicates>::apply(TNode node) {
+  Debug("bv-rewrite") << "RewriteRule<FlattenAssocCommut>(" << node << ")" << std::endl;
+  std::vector<Node> processingStack;
+  processingStack.push_back(node);
+  __gnu_cxx::hash_set<TNode, TNodeHashFunction> processed;
+  std::vector<Node> children;
+  Kind kind = node.getKind(); 
+  
+  while (! processingStack.empty()) {
+    TNode current = processingStack.back();
+    processingStack.pop_back();
+    if (processed.count(current))
+      continue;
+
+    processed.insert(current);
+    
+    // flatten expression
+    if (current.getKind() == kind) {
+      for (unsigned i = 0; i < current.getNumChildren(); ++i) {
+        processingStack.push_back(current[i]);
+      }
+    } else {
+      children.push_back(current); 
+    }
+  }
+  return utils::mkSortedNode(kind, children);
+}
+  
+  
 template<> inline
 bool RewriteRule<OrSimplify>::applies(TNode node) {
   return (node.getKind() == kind::BITVECTOR_OR);

diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 306a3bd973aadd7189b087d006b88648aaebf058..dc91c338b23ca1db19f001a880e184e66681b885 100644 (file)
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -214,7 +214,7 @@ RewriteResponse TheoryBVRewriter::RewriteConcat(TNode node, bool prerewrite) {
 RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node, bool prerewrite) {
   Node resultNode = node;
   resultNode = LinearRewriteStrategy
-    < RewriteRule<FlattenAssocCommut>,
+    < RewriteRule<FlattenAssocCommutNoDuplicates>,
       RewriteRule<AndSimplify>
       >::apply(node);
 
@@ -234,7 +234,7 @@ RewriteResponse TheoryBVRewriter::RewriteAnd(TNode node, bool prerewrite) {
 RewriteResponse TheoryBVRewriter::RewriteOr(TNode node, bool prerewrite){
   Node resultNode = node;
   resultNode = LinearRewriteStrategy
-    < RewriteRule<FlattenAssocCommut>,
+    < RewriteRule<FlattenAssocCommutNoDuplicates>,
       RewriteRule<OrSimplify>
       >::apply(node);