flatten or nodes

diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp
index d6aa51abaf681491f9285086a6d1d6945d54bddc..c9615d9cddf36cdd3db29ffe955cb0257979670c 100644 (file)
--- a/src/theory/booleans/theory_bool_rewriter.cpp
+++ b/src/theory/booleans/theory_bool_rewriter.cpp
@@ -22,6 +22,40 @@ namespace CVC4 {
 namespace theory {
 namespace booleans {
 
+RewriteResponse flattenOrNode(TNode n, TNode trueNode, TNode falseNode)
+{
+  typedef std::hash_set<TNode, TNodeHashFunction> node_set;
+
+  node_set visited;
+  visited.insert(falseNode);
+
+  std::vector<TNode> toProcess;
+  toProcess.push_back(n);
+
+  Kind k = n.getKind();
+  NodeBuilder<> nb(k);
+
+  for (unsigned i = 0; i < toProcess.size(); ++ i) {
+    TNode current = toProcess[i];
+    for(unsigned j = 0, j_end = current.getNumChildren(); j < j_end; ++ j) {
+      TNode child = current[j];
+      if(visited.find(child) != visited.end()) {
+        continue;
+      } else if(child == trueNode) {
+        return RewriteResponse(REWRITE_DONE, trueNode);
+      } else {
+        if(child.getKind() == k)
+          toProcess.push_back(child);
+        else
+          nb << child;
+      }
+    }
+  }
+  if (nb.getNumChildren() == 0) return RewriteResponse(REWRITE_DONE, falseNode);
+  if (nb.getNumChildren() == 1) return RewriteResponse(REWRITE_AGAIN, nb.getChild(0));
+  return RewriteResponse(REWRITE_AGAIN, nb.constructNode());
+}
+
 RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
   NodeManager* nodeManager = NodeManager::currentNM();
   Node tt = nodeManager->mkConst(true);
@@ -35,27 +69,15 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
     break;
   }
   case kind::OR: {
-    if (n.getNumChildren() == 2) {
-      if (n[0] == tt || n[1] == tt) return RewriteResponse(REWRITE_DONE, tt);
-      if (n[0] == ff) return RewriteResponse(REWRITE_AGAIN, n[1]);
-      if (n[1] == ff) return RewriteResponse(REWRITE_AGAIN, n[0]);
+    bool done = true;
+    TNode::iterator i = n.begin(), iend = n.end();
+    for(; i != iend; ++i) {
+      if (*i == tt) return RewriteResponse(REWRITE_DONE, tt);
+      if (*i == ff) done = false;
+      if ((*i).getKind() == kind::OR) done = false;
     }
-    else {
-      bool done = true;
-      TNode::iterator i = n.begin(), iend = n.end();
-      for(; i != iend; ++i) {
-        if (*i == tt) return RewriteResponse(REWRITE_DONE, tt);
-        if (*i == ff) done = false;
-      }
-      if (!done) {
-        NodeBuilder<> nb(kind::OR);
-        for(i = n.begin(); i != iend; ++i) {
-          if (*i != ff) nb << *i;
-        }
-        if (nb.getNumChildren() == 0) return RewriteResponse(REWRITE_DONE, ff);
-        if (nb.getNumChildren() == 1) return RewriteResponse(REWRITE_AGAIN, nb.getChild(0));
-        return RewriteResponse(REWRITE_AGAIN, nb.constructNode());
-      }
+    if (!done) {
+      return flattenOrNode(n, /*trueNode = */ tt, /* falseNode = */ ff);
     }
     break;
   }

diff --git a/test/regress/regress0/preprocess/Makefile.am b/test/regress/regress0/preprocess/Makefile.am
index 96b5d292874a58387d3f2817bf867843775a2aaf..42f763f079a088bc5e566b8076eba8f55ae4f114 100644 (file)
--- a/test/regress/regress0/preprocess/Makefile.am
+++ b/test/regress/regress0/preprocess/Makefile.am
@@ -37,7 +37,8 @@ CVC_TESTS = \
        preprocess_09.cvc \
        preprocess_10.cvc \
        preprocess_11.cvc \
-       preprocess_12.cvc
+       preprocess_12.cvc \
+       preprocess_13.cvc
 
 # Regression tests derived from bug reports
 BUG_TESTS = 

diff --git a/test/regress/regress0/preprocess/preprocess_13.cvc b/test/regress/regress0/preprocess/preprocess_13.cvc
new file mode 100644 (file)
index 0000000..7a2ed7d
--- /dev/null
+++ b/test/regress/regress0/preprocess/preprocess_13.cvc
@@ -0,0 +1,10 @@
+% EXPECT: valid
+
+a0, a1, a2, a3, a4, a5, a6, a7, a8, a9: BOOLEAN;
+
+ASSERT (a5);
+
+QUERY (a0 OR (a1 OR (a2 OR (a3 OR (a4 OR (a5 OR (FALSE OR (a6 OR (a7 OR (a8 OR a9))))))))));
+
+% EXIT: 20
+