Remove template argument from `NodeBuilder`an/refactor/NodeBuilder

Currently, `NodeBuilder` takes a single template argument: An integer
that determines the expected number of arguments. This argument is used
to determine the size of the `d_inlineNvChildSpace` array. This array is
used to construct nodes inline. The advantage of this is that we don't
have to allocate a `NodeValue` on the heap for the node under
construction until we are sure that the node is new. While templating
the array size may save some stack space (or avoid a heap allocation if
we statically know that we a fixed number of children and that number is
greater than 10), it complicates the code and leads to longer compile
times. Thus, this commit removes the template argument and moves some of
the `NodeBuilder` code to a source file for faster compilation.

CPU build time before change (debug build): 2429.68s
CPU build time after change (debug build): 2228.44s

1 files changed, 10 insertions, 7 deletions

diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index ea597468d..43589fdce 100644
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -223,7 +223,7 @@ void ArithCongruenceManager::watchedVariableIsZero(ConstraintCP lb, ConstraintCP
   TNode eq = d_watchedEqualities[s];
   ConstraintCP eqC = d_constraintDatabase.getConstraint(
       s, ConstraintType::Equality, lb->getValue());
-  NodeBuilder<> reasonBuilder(Kind::AND);
+  NodeBuilder reasonBuilder(Kind::AND);
   auto pfLb = lb->externalExplainByAssertions(reasonBuilder);
   auto pfUb = ub->externalExplainByAssertions(reasonBuilder);
   Node reason = safeConstructNary(reasonBuilder);
@@ -256,7 +256,7 @@ void ArithCongruenceManager::watchedVariableIsZero(ConstraintCP eq){
   //Explain for conflict is correct as these proofs are generated
   //and stored eagerly
   //These will be safe for propagation later as well
-  NodeBuilder<> nb(Kind::AND);
+  NodeBuilder nb(Kind::AND);
   // An open proof of eq from literals now in reason.
   if (Debug.isOn("arith::cong"))
   {
@@ -284,7 +284,7 @@ void ArithCongruenceManager::watchedVariableCannotBeZero(ConstraintCP c){
 
   //Explain for conflict is correct as these proofs are generated and stored eagerly
   //These will be safe for propagation later as well
-  NodeBuilder<> nb(Kind::AND);
+  NodeBuilder nb(Kind::AND);
   // An open proof of eq from literals now in reason.
   auto pf = c->externalExplainByAssertions(nb);
   if (Debug.isOn("arith::cong::notzero"))
@@ -456,7 +456,9 @@ void ArithCongruenceManager::explain(TNode literal, std::vector<TNode>& assumpti
   }
 }
 
-void ArithCongruenceManager::enqueueIntoNB(const std::set<TNode> s, NodeBuilder<>& nb){
+void ArithCongruenceManager::enqueueIntoNB(const std::set<TNode> s,
+                                           NodeBuilder& nb)
+{
   std::set<TNode>::const_iterator it = s.begin();
   std::set<TNode>::const_iterator it_end = s.end();
   for(; it != it_end; ++it) {
@@ -504,7 +506,8 @@ TrustNode ArithCongruenceManager::explain(TNode external)
   return trn;
 }
 
-void ArithCongruenceManager::explain(TNode external, NodeBuilder<>& out){
+void ArithCongruenceManager::explain(TNode external, NodeBuilder& out)
+{
   Node internal = externalToInternal(external);
 
   std::vector<TNode> assumptions;
@@ -627,7 +630,7 @@ void ArithCongruenceManager::equalsConstant(ConstraintCP c){
   Node eq = xAsNode.eqNode(asRational);
   d_keepAlive.push_back(eq);
 
-  NodeBuilder<> nb(Kind::AND);
+  NodeBuilder nb(Kind::AND);
   auto pf = c->externalExplainByAssertions(nb);
   Node reason = safeConstructNary(nb);
   d_keepAlive.push_back(reason);
@@ -646,7 +649,7 @@ void ArithCongruenceManager::equalsConstant(ConstraintCP lb, ConstraintCP ub){
                           << ub << std::endl;
 
   ArithVar x = lb->getVariable();
-  NodeBuilder<> nb(Kind::AND);
+  NodeBuilder nb(Kind::AND);
   auto pfLb = lb->externalExplainByAssertions(nb);
   auto pfUb = ub->externalExplainByAssertions(nb);
   Node reason = safeConstructNary(nb);