1 files changed, 82 insertions, 2 deletions

diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp
index 433bca568..14ed9df07 100644
--- a/src/preprocessing/passes/ite_simp.cpp
+++ b/src/preprocessing/passes/ite_simp.cpp
@@ -22,7 +22,6 @@
 #include "preprocessing/assertion_pipeline.h"
 #include "preprocessing/preprocessing_pass_context.h"
 #include "smt/smt_statistics_registry.h"
-#include "smt_util/nary_builder.h"
 #include "theory/arith/arith_ite_utils.h"
 #include "theory/theory_engine.h"
 
@@ -34,6 +33,87 @@ namespace cvc5 {
 namespace preprocessing {
 namespace passes {
 
+Node mkAssocAnd(const std::vector<Node>& children)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  if (children.size() == 0)
+  {
+    return nm->mkConst(true);
+  }
+  else if (children.size() == 1)
+  {
+    return children[0];
+  }
+  else
+  {
+    const uint32_t max = kind::metakind::getMaxArityForKind(kind::AND);
+    const uint32_t min = kind::metakind::getMinArityForKind(kind::AND);
+
+    Assert(min <= children.size());
+
+    unsigned int numChildren = children.size();
+    if (numChildren <= max)
+    {
+      return nm->mkNode(kind::AND, children);
+    }
+
+    typedef std::vector<Node>::const_iterator const_iterator;
+    const_iterator it = children.begin();
+    const_iterator end = children.end();
+
+    /* The new top-level children and the children of each sub node */
+    std::vector<Node> newChildren;
+    std::vector<Node> subChildren;
+
+    while (it != end && numChildren > max)
+    {
+      /* Grab the next max children and make a node for them. */
+      for (const_iterator next = it + max; it != next; ++it, --numChildren)
+      {
+        subChildren.push_back(*it);
+      }
+      Node subNode = nm->mkNode(kind::AND, subChildren);
+      newChildren.push_back(subNode);
+      subChildren.clear();
+    }
+
+    /* If there's children left, "top off" the Expr. */
+    if (numChildren > 0)
+    {
+      /* If the leftovers are too few, just copy them into newChildren;
+       * otherwise make a new sub-node  */
+      if (numChildren < min)
+      {
+        for (; it != end; ++it)
+        {
+          newChildren.push_back(*it);
+        }
+      }
+      else
+      {
+        for (; it != end; ++it)
+        {
+          subChildren.push_back(*it);
+        }
+        Node subNode = nm->mkNode(kind::AND, subChildren);
+        newChildren.push_back(subNode);
+      }
+    }
+
+    /* It's inconceivable we could have enough children for this to fail
+     * (more than 2^32, in most cases?). */
+    AlwaysAssert(newChildren.size() <= max)
+        << "Too many new children in mkAssociative";
+
+    /* It would be really weird if this happened (it would require
+     * min > 2, for one thing), but let's make sure. */
+    AlwaysAssert(newChildren.size() >= min)
+        << "Too few new children in mkAssociative";
+
+    return nm->mkNode(kind::AND, newChildren);
+  }
+}
+
 /* -------------------------------------------------------------------------- */
 
 namespace {
@@ -71,7 +151,7 @@ void compressBeforeRealAssertions(AssertionPipeline* assertionsToPreprocess,
   assertionsToPreprocess->resize(before);
   size_t lastBeforeItes = assertionsToPreprocess->getRealAssertionsEnd() - 1;
   intoConjunction.push_back((*assertionsToPreprocess)[lastBeforeItes]);
-  Node newLast = cvc5::util::NaryBuilder::mkAssoc(kind::AND, intoConjunction);
+  Node newLast = mkAssocAnd(intoConjunction);
   assertionsToPreprocess->replace(lastBeforeItes, newLast);
   Assert(assertionsToPreprocess->size() == before);
 }