From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Wed, 17 Apr 2013 20:27:45 +0000 (-0400)
Subject: bool flatten: node num_children workaround
X-Git-Tag: cvc5-1.0.0~7318
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5721e631d63d5a9a5c8ce3a6c8ce1198a1ad4e50;p=cvc5.git

bool flatten: node num_children workaround
---

diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp
index e6b714749..9867ccd4e 100644
--- a/src/theory/booleans/theory_bool_rewriter.cpp
+++ b/src/theory/booleans/theory_bool_rewriter.cpp
@@ -46,7 +46,8 @@ RewriteResponse flattenNode(TNode n, TNode trivialNode, TNode skipNode)
   toProcess.push_back(n);
 
   Kind k = n.getKind();
-  NodeBuilder<> nb(k);
+  typedef std::vector<TNode> ChildList;
+  ChildList childList;   //TNode should be fine, since 'n' is still there
 
   for (unsigned i = 0; i < toProcess.size(); ++ i) {
     TNode current = toProcess[i];
@@ -61,13 +62,30 @@ RewriteResponse flattenNode(TNode n, TNode trivialNode, TNode skipNode)
         if(child.getKind() == k)
           toProcess.push_back(child);
         else
-          nb << child;
+          childList.push_back(child);
       }
     }
   }
-  if (nb.getNumChildren() == 0) return RewriteResponse(REWRITE_DONE, skipNode);
-  if (nb.getNumChildren() == 1) return RewriteResponse(REWRITE_AGAIN, nb.getChild(0));
-  return RewriteResponse(REWRITE_DONE, nb.constructNode());
+  if (childList.size() == 0) return RewriteResponse(REWRITE_DONE, skipNode);
+  if (childList.size() == 1) return RewriteResponse(REWRITE_AGAIN, childList[0]);
+
+  /* Trickery to stay under number of children possible in a node */
+  NodeManager* nodeManager = NodeManager::currentNM();
+  static const unsigned MAX_CHILDREN = (1u << __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN ) - 1;
+  if (childList.size() < MAX_CHILDREN) {
+    Node retNode = nodeManager->mkNode(k, childList);
+    return RewriteResponse(REWRITE_DONE, retNode);
+  } else {
+    Assert(childList.size() < size_t(MAX_CHILDREN) * size_t(MAX_CHILDREN) );
+    NodeBuilder<> nb(k);
+    ChildList::iterator cur = childList.begin(), next, en = childList.end();
+    while( cur != en ) {
+      next = min(cur + MAX_CHILDREN, en);
+      nb << (nodeManager->mkNode(k, ChildList(cur, next) ));
+      cur = next;
+    }
+    return RewriteResponse(REWRITE_DONE, nb.constructNode());
+  }
 }
 
 RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {