Remove template argument from `NodeBuilder` (#6290)

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

Signed-off-by: Andres Noetzli noetzli@amazon.com

17 files changed, 93 insertions, 79 deletions

diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp
index 8e75f6850..caa052065 100644
--- a/src/theory/arith/approx_simplex.cpp
+++ b/src/theory/arith/approx_simplex.cpp
@@ -1785,7 +1785,7 @@ MipResult ApproxGLPK::solveMIP(bool activelyLog){
 
 // Node explainSet(const set<ConstraintP>& inp){
 //   Assert(!inp.empty());
-//   NodeBuilder<> nb(kind::AND);
+//   NodeBuilder nb(kind::AND);
 //   set<ConstraintP>::const_iterator iter, end;
 //   for(iter = inp.begin(), end = inp.end(); iter != end; ++iter){
 //     const ConstraintP c = *iter;
diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp
index 4c991dba3..218fdf179 100644
--- a/src/theory/arith/arith_ite_utils.cpp
+++ b/src/theory/arith/arith_ite_utils.cpp
@@ -35,7 +35,7 @@ namespace theory {
 namespace arith {
 
 Node ArithIteUtils::applyReduceVariablesInItes(Node n){
-  NodeBuilder<> nb(n.getKind());
+  NodeBuilder nb(n.getKind());
   if(n.getMetaKind() == kind::metakind::PARAMETERIZED) {
     nb << (n.getOperator());
   }
@@ -239,7 +239,7 @@ Node ArithIteUtils::reduceConstantIteByGCD(Node n){
   }
 
   if(n.getNumChildren() > 0){
-    NodeBuilder<> nb(n.getKind());
+    NodeBuilder nb(n.getKind());
     if(n.getMetaKind() == kind::metakind::PARAMETERIZED) {
       nb << (n.getOperator());
     }
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 87aba7b45..452200796 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -235,7 +235,7 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
               if( num==1 ){
                 return RewriteResponse(REWRITE_AGAIN, base);
               }else{
-                NodeBuilder<> nb(kind::MULT);
+                NodeBuilder nb(kind::MULT);
                 for(unsigned i=0; i < num; ++i){
                   nb << base;
                 }
diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp
index 9c764ac7a..ce54133c5 100644
--- a/src/theory/arith/arith_static_learner.cpp
+++ b/src/theory/arith/arith_static_learner.cpp
@@ -57,8 +57,8 @@ ArithStaticLearner::Statistics::~Statistics(){
   smtStatisticsRegistry()->unregisterStat(&d_iteConstantApplications);
 }
 
-void ArithStaticLearner::staticLearning(TNode n, NodeBuilder<>& learned){
-
+void ArithStaticLearner::staticLearning(TNode n, NodeBuilder& learned)
+{
   vector<TNode> workList;
   workList.push_back(n);
   TNodeSet processed;
@@ -101,8 +101,10 @@ void ArithStaticLearner::staticLearning(TNode n, NodeBuilder<>& learned){
   }
 }
 
-
-void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet& defTrue){
+void ArithStaticLearner::process(TNode n,
+                                 NodeBuilder& learned,
+                                 const TNodeSet& defTrue)
+{
   Debug("arith::static") << "===================== looking at " << n << endl;
 
   switch(n.getKind()){
@@ -136,7 +138,8 @@ void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet
   }
 }
 
-void ArithStaticLearner::iteMinMax(TNode n, NodeBuilder<>& learned){
+void ArithStaticLearner::iteMinMax(TNode n, NodeBuilder& learned)
+{
   Assert(n.getKind() == kind::ITE);
   Assert(n[0].getKind() != EQUAL);
   Assert(isRelationOperator(n[0].getKind()));
@@ -167,8 +170,8 @@ void ArithStaticLearner::iteMinMax(TNode n, NodeBuilder<>& learned){
     switch(k){
     case LT:   // (ite (< x y) x y)
     case LEQ: { // (ite (<= x y) x y)
-      Node nLeqX = NodeBuilder<2>(LEQ) << n << t;
-      Node nLeqY = NodeBuilder<2>(LEQ) << n << e;
+      Node nLeqX = NodeBuilder(LEQ) << n << t;
+      Node nLeqY = NodeBuilder(LEQ) << n << e;
       Debug("arith::static") << n << "is a min =>"  << nLeqX << nLeqY << endl;
       learned << nLeqX << nLeqY;
       ++(d_statistics.d_iteMinMaxApplications);
@@ -176,8 +179,8 @@ void ArithStaticLearner::iteMinMax(TNode n, NodeBuilder<>& learned){
     }
     case GT: // (ite (> x y) x y)
     case GEQ: { // (ite (>= x y) x y)
-      Node nGeqX = NodeBuilder<2>(GEQ) << n << t;
-      Node nGeqY = NodeBuilder<2>(GEQ) << n << e;
+      Node nGeqX = NodeBuilder(GEQ) << n << t;
+      Node nGeqY = NodeBuilder(GEQ) << n << e;
       Debug("arith::static") << n << "is a max =>"  << nGeqX << nGeqY << endl;
       learned << nGeqX << nGeqY;
       ++(d_statistics.d_iteMinMaxApplications);
@@ -188,7 +191,8 @@ void ArithStaticLearner::iteMinMax(TNode n, NodeBuilder<>& learned){
   }
 }
 
-void ArithStaticLearner::iteConstant(TNode n, NodeBuilder<>& learned){
+void ArithStaticLearner::iteConstant(TNode n, NodeBuilder& learned)
+{
   Assert(n.getKind() == ITE);
 
   Debug("arith::static") << "iteConstant(" << n << ")" << endl;
@@ -202,9 +206,11 @@ void ArithStaticLearner::iteConstant(TNode n, NodeBuilder<>& learned){
       d_minMap.insert(n, min);
       Node nGeqMin;
       if (min.getInfinitesimalPart() == 0) {
-        nGeqMin = NodeBuilder<2>(kind::GEQ) << n << mkRationalNode(min.getNoninfinitesimalPart());
+        nGeqMin = NodeBuilder(kind::GEQ)
+                  << n << mkRationalNode(min.getNoninfinitesimalPart());
       } else {
-        nGeqMin = NodeBuilder<2>(kind::GT) << n << mkRationalNode(min.getNoninfinitesimalPart());
+        nGeqMin = NodeBuilder(kind::GT)
+                  << n << mkRationalNode(min.getNoninfinitesimalPart());
       }
       learned << nGeqMin;
       Debug("arith::static") << n << " iteConstant"  << nGeqMin << endl;
@@ -221,9 +227,11 @@ void ArithStaticLearner::iteConstant(TNode n, NodeBuilder<>& learned){
       d_maxMap.insert(n, max);
       Node nLeqMax;
       if (max.getInfinitesimalPart() == 0) {
-        nLeqMax = NodeBuilder<2>(kind::LEQ) << n << mkRationalNode(max.getNoninfinitesimalPart());
+        nLeqMax = NodeBuilder(kind::LEQ)
+                  << n << mkRationalNode(max.getNoninfinitesimalPart());
       } else {
-        nLeqMax = NodeBuilder<2>(kind::LT) << n << mkRationalNode(max.getNoninfinitesimalPart());
+        nLeqMax = NodeBuilder(kind::LT)
+                  << n << mkRationalNode(max.getNoninfinitesimalPart());
       }
       learned << nLeqMax;
       Debug("arith::static") << n << " iteConstant"  << nLeqMax << endl;
diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h
index 73810dedd..b96d7a86a 100644
--- a/src/theory/arith/arith_static_learner.h
+++ b/src/theory/arith/arith_static_learner.h
@@ -45,19 +45,22 @@ private:
 public:
   ArithStaticLearner(context::Context* userContext);
   ~ArithStaticLearner();
-  void staticLearning(TNode n, NodeBuilder<>& learned);
+  void staticLearning(TNode n, NodeBuilder& learned);
 
   void addBound(TNode n);
 
-private:
-  void process(TNode n, NodeBuilder<>& learned, const TNodeSet& defTrue);
+ private:
+  void process(TNode n, NodeBuilder& learned, const TNodeSet& defTrue);
 
-  void iteMinMax(TNode n, NodeBuilder<>& learned);
-  void iteConstant(TNode n, NodeBuilder<>& learned);
+  void iteMinMax(TNode n, NodeBuilder& learned);
+  void iteConstant(TNode n, NodeBuilder& learned);
 
-  /** These fields are designed to be accessible to ArithStaticLearner methods. */
-  class Statistics {
-  public:
+  /**
+   * These fields are designed to be accessible to ArithStaticLearner methods.
+   */
+  class Statistics
+  {
+   public:
     IntStat d_iteMinMaxApplications;
     IntStat d_iteConstantApplications;
 
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index 852550917..bc35c6941 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -194,17 +194,18 @@ inline Kind negateKind(Kind k){
 
 inline Node negateConjunctionAsClause(TNode conjunction){
   Assert(conjunction.getKind() == kind::AND);
-  NodeBuilder<> orBuilder(kind::OR);
+  NodeBuilder orBuilder(kind::OR);
 
   for(TNode::iterator i = conjunction.begin(), end=conjunction.end(); i != end; ++i){
     TNode child = *i;
-    Node negatedChild = NodeBuilder<1>(kind::NOT)<<(child);
+    Node negatedChild = NodeBuilder(kind::NOT) << (child);
     orBuilder << negatedChild;
   }
   return orBuilder;
 }
 
-inline Node maybeUnaryConvert(NodeBuilder<>& builder){
+inline Node maybeUnaryConvert(NodeBuilder& builder)
+{
   Assert(builder.getKind() == kind::OR || builder.getKind() == kind::AND
          || builder.getKind() == kind::PLUS || builder.getKind() == kind::MULT);
   Assert(builder.getNumChildren() >= 1);
@@ -247,7 +248,8 @@ inline Node getIdentity(Kind k){
   }
 }
 
-inline Node safeConstructNary(NodeBuilder<>& nb) {
+inline Node safeConstructNary(NodeBuilder& nb)
+{
   switch (nb.getNumChildren()) {
     case 0:
       return getIdentity(nb.getKind());
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);
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index 055d5ddbb..325f7002b 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -212,7 +212,7 @@ private:
   void enableSharedTerms();
   void dequeueLiterals();
 
-  void enqueueIntoNB(const std::set<TNode> all, NodeBuilder<>& nb);
+  void enqueueIntoNB(const std::set<TNode> all, NodeBuilder& nb);
 
   /**
    * Determine an explaination for `internal`. That is a conjunction of theory
@@ -251,7 +251,7 @@ private:
    */
   TrustNode explain(TNode literal);
 
-  void explain(TNode lit, NodeBuilder<>& out);
+  void explain(TNode lit, NodeBuilder& out);
 
   void addWatchedPair(ArithVar s, TNode x, TNode y);
 
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index baa9b1ebb..14daca11b 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -481,7 +481,7 @@ bool Constraint::isInternalAssumption() const {
 
 TrustNode Constraint::externalExplainByAssertions() const
 {
-  NodeBuilder<> nb(kind::AND);
+  NodeBuilder nb(kind::AND);
   auto pfFromAssumptions = externalExplain(nb, AssertionOrderSentinel);
   Node exp = safeConstructNary(nb);
   if (d_database->isProofEnabled())
@@ -1078,12 +1078,12 @@ TrustNode Constraint::split()
   TNode lhs = eqNode[0];
   TNode rhs = eqNode[1];
 
-  Node leqNode = NodeBuilder<2>(kind::LEQ) << lhs << rhs;
-  Node ltNode = NodeBuilder<2>(kind::LT) << lhs << rhs;
-  Node gtNode = NodeBuilder<2>(kind::GT) << lhs << rhs;
-  Node geqNode = NodeBuilder<2>(kind::GEQ) << lhs << rhs;
+  Node leqNode = NodeBuilder(kind::LEQ) << lhs << rhs;
+  Node ltNode = NodeBuilder(kind::LT) << lhs << rhs;
+  Node gtNode = NodeBuilder(kind::GT) << lhs << rhs;
+  Node geqNode = NodeBuilder(kind::GEQ) << lhs << rhs;
 
-  Node lemma = NodeBuilder<3>(OR) << leqNode << geqNode;
+  Node lemma = NodeBuilder(OR) << leqNode << geqNode;
 
   TrustNode trustedLemma;
   if (d_database->isProofEnabled())
@@ -1517,7 +1517,7 @@ TrustNode Constraint::externalExplainForPropagation(TNode lit) const
   Assert(hasProof());
   Assert(!isAssumption());
   Assert(!isInternalAssumption());
-  NodeBuilder<> nb(Kind::AND);
+  NodeBuilder nb(Kind::AND);
   auto pfFromAssumptions = externalExplain(nb, d_assertionOrder);
   Node n = safeConstructNary(nb);
   if (d_database->isProofEnabled())
@@ -1553,7 +1553,7 @@ TrustNode Constraint::externalExplainConflict() const
 {
   Debug("pf::arith::explain") << this << std::endl;
   Assert(inConflict());
-  NodeBuilder<> nb(kind::AND);
+  NodeBuilder nb(kind::AND);
   auto pf1 = externalExplainByAssertions(nb);
   auto not2 = getNegation()->getProofLiteral().negate();
   auto pf2 = getNegation()->externalExplainByAssertions(nb);
@@ -1650,7 +1650,7 @@ void Constraint::assertionFringe(ConstraintCPVec& o, const ConstraintCPVec& i){
 }
 
 Node Constraint::externalExplain(const ConstraintCPVec& v, AssertionOrder order){
-  NodeBuilder<> nb(kind::AND);
+  NodeBuilder nb(kind::AND);
   ConstraintCPVec::const_iterator i, end;
   for(i = v.begin(), end = v.end(); i != end; ++i){
     ConstraintCP v_i = *i;
@@ -1660,7 +1660,7 @@ Node Constraint::externalExplain(const ConstraintCPVec& v, AssertionOrder order)
 }
 
 std::shared_ptr<ProofNode> Constraint::externalExplain(
-    NodeBuilder<>& nb, AssertionOrder order) const
+    NodeBuilder& nb, AssertionOrder order) const
 {
   if (Debug.isOn("pf::arith::explain"))
   {
@@ -1857,14 +1857,14 @@ std::shared_ptr<ProofNode> Constraint::externalExplain(
 }
 
 Node Constraint::externalExplainByAssertions(ConstraintCP a, ConstraintCP b){
-  NodeBuilder<> nb(kind::AND);
+  NodeBuilder nb(kind::AND);
   a->externalExplainByAssertions(nb);
   b->externalExplainByAssertions(nb);
   return nb;
 }
 
 Node Constraint::externalExplainByAssertions(ConstraintCP a, ConstraintCP b, ConstraintCP c){
-  NodeBuilder<> nb(kind::AND);
+  NodeBuilder nb(kind::AND);
   a->externalExplainByAssertions(nb);
   b->externalExplainByAssertions(nb);
   c->externalExplainByAssertions(nb);
@@ -1982,7 +1982,7 @@ TrustNode ConstraintDatabase::eeExplain(const Constraint* const c) const
   return d_congruenceManager.explain(c->getLiteral());
 }
 
-void ConstraintDatabase::eeExplain(ConstraintCP c, NodeBuilder<>& nb) const
+void ConstraintDatabase::eeExplain(ConstraintCP c, NodeBuilder& nb) const
 {
   Assert(c->hasLiteral());
   // NOTE: this is not a recommended method since it ignores proofs
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index d00f16c90..33e39a5f0 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -571,8 +571,7 @@ class Constraint {
    * This is not appropriate for propagation!
    * Use explainForPropagation() instead.
    */
-  std::shared_ptr<ProofNode> externalExplainByAssertions(
-      NodeBuilder<>& nb) const
+  std::shared_ptr<ProofNode> externalExplainByAssertions(NodeBuilder& nb) const
   {
     return externalExplain(nb, AssertionOrderSentinel);
   }
@@ -876,7 +875,7 @@ class Constraint {
    * This is the minimum fringe of the implication tree
    * s.t. every constraint is assertedBefore(order) or hasEqualityEngineProof().
    */
-  std::shared_ptr<ProofNode> externalExplain(NodeBuilder<>& nb,
+  std::shared_ptr<ProofNode> externalExplain(NodeBuilder& nb,
                                              AssertionOrder order) const;
 
   static Node externalExplain(const ConstraintCPVec& b, AssertionOrder order);
@@ -1168,7 +1167,7 @@ private:
    */
   TrustNode eeExplain(ConstraintCP c) const;
   /** Get an explanation for this constraint from the equality engine */
-  void eeExplain(ConstraintCP c, NodeBuilder<>& nb) const;
+  void eeExplain(ConstraintCP c, NodeBuilder& nb) const;
 
   /**
    * Returns a constraint with the variable v, the constraint type t, and a value
diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp
index 6e069cdf6..3825a3a42 100644
--- a/src/theory/arith/dio_solver.cpp
+++ b/src/theory/arith/dio_solver.cpp
@@ -198,7 +198,7 @@ Node DioSolver::proveIndex(TrailIndex i){
   const Polynomial& proof = d_trail[i].d_proof;
   Assert(!proof.isConstant());
 
-  NodeBuilder<> nb(kind::AND);
+  NodeBuilder nb(kind::AND);
   for(Polynomial::iterator iter = proof.begin(), end = proof.end(); iter!= end; ++iter){
     Monomial m = (*iter);
     Assert(!m.isConstant());
diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index 7b9002d82..940812604 100644
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -420,7 +420,7 @@ public:
 
 template <class GetNodeIterator>
 inline Node makeNode(Kind k, GetNodeIterator start, GetNodeIterator end) {
-  NodeBuilder<> nb(k);
+  NodeBuilder nb(k);
 
   while(start != end) {
     nb << (*start).getNode();
diff --git a/src/theory/arith/proof_checker.cpp b/src/theory/arith/proof_checker.cpp
index 23f141535..248897ced 100644
--- a/src/theory/arith/proof_checker.cpp
+++ b/src/theory/arith/proof_checker.cpp
@@ -108,8 +108,8 @@ Node ArithProofRuleChecker::checkInternal(PfRule id,
 
       // Whether a strict inequality is in the sum.
       bool strict = false;
-      NodeBuilder<> leftSum(Kind::PLUS);
-      NodeBuilder<> rightSum(Kind::PLUS);
+      NodeBuilder leftSum(Kind::PLUS);
+      NodeBuilder rightSum(Kind::PLUS);
       for (size_t i = 0; i < children.size(); ++i)
       {
         // Adjust strictness
@@ -163,8 +163,8 @@ Node ArithProofRuleChecker::checkInternal(PfRule id,
 
       // Whether a strict inequality is in the sum.
       bool strict = false;
-      NodeBuilder<> leftSum(Kind::PLUS);
-      NodeBuilder<> rightSum(Kind::PLUS);
+      NodeBuilder leftSum(Kind::PLUS);
+      NodeBuilder rightSum(Kind::PLUS);
       for (size_t i = 0; i < children.size(); ++i)
       {
         Rational scalar = args[i].getConst<Rational>();
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 834a3d52d..e68ff7d11 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -145,8 +145,8 @@ TrustNode TheoryArith::ppRewriteEq(TNode atom)
     return TrustNode::null();
   }
   Assert(atom[0].getType().isReal());
-  Node leq = NodeBuilder<2>(kind::LEQ) << atom[0] << atom[1];
-  Node geq = NodeBuilder<2>(kind::GEQ) << atom[0] << atom[1];
+  Node leq = NodeBuilder(kind::LEQ) << atom[0] << atom[1];
+  Node geq = NodeBuilder(kind::GEQ) << atom[0] << atom[1];
   Node rewritten = Rewriter::rewrite(leq.andNode(geq));
   Debug("arith::preprocess")
       << "arith::preprocess() : returning " << rewritten << endl;
@@ -167,7 +167,8 @@ Theory::PPAssertStatus TheoryArith::ppAssert(
   return d_internal->ppAssert(tin, outSubstitutions);
 }
 
-void TheoryArith::ppStaticLearn(TNode n, NodeBuilder<>& learned) {
+void TheoryArith::ppStaticLearn(TNode n, NodeBuilder& learned)
+{
   d_internal->ppStaticLearn(n, learned);
 }
 
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 0c1320b03..99fa9f379 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -122,7 +122,7 @@ class TheoryArith : public Theory {
    * symbols.
    */
   TrustNode ppRewrite(TNode atom, std::vector<SkolemLemma>& lems) override;
-  void ppStaticLearn(TNode in, NodeBuilder<>& learned) override;
+  void ppStaticLearn(TNode in, NodeBuilder& learned) override;
 
   std::string identify() const override { return std::string("TheoryArith"); }
 
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index d38dd881b..0a64a4e63 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -239,7 +239,7 @@ static void resolve(ConstraintCPVec& buf, ConstraintP c, const ConstraintCPVec&
   // Assert(uppos < upconf.getNumChildren());
   // Assert(equalUpToNegation(dnconf[dnpos], upconf[uppos]));
 
-  // NodeBuilder<> nb(kind::AND);
+  // NodeBuilder nb(kind::AND);
   // dropPosition(nb, dnconf, dnpos);
   // dropPosition(nb, upconf, uppos);
   // return safeConstructNary(nb);
@@ -1196,14 +1196,13 @@ Theory::PPAssertStatus TheoryArithPrivate::ppAssert(
   return Theory::PP_ASSERT_STATUS_UNSOLVED;
 }
 
-void TheoryArithPrivate::ppStaticLearn(TNode n, NodeBuilder<>& learned) {
+void TheoryArithPrivate::ppStaticLearn(TNode n, NodeBuilder& learned)
+{
   TimerStat::CodeTimer codeTimer(d_statistics.d_staticLearningTimer);
 
   d_learner.staticLearning(n, learned);
 }
 
-
-
 ArithVar TheoryArithPrivate::findShortestBasicRow(ArithVar variable){
   ArithVar bestBasic = ARITHVAR_SENTINEL;
   uint64_t bestRowLength = std::numeric_limits<uint64_t>::max();
@@ -2206,7 +2205,7 @@ std::pair<ConstraintP, ArithVar> TheoryArithPrivate::replayGetConstraint(const C
 
 Node toSumNode(const ArithVariables& vars, const DenseMap<Rational>& sum){
   Debug("arith::toSumNode") << "toSumNode() begin" << endl;
-  NodeBuilder<> nb(kind::PLUS);
+  NodeBuilder nb(kind::PLUS);
   NodeManager* nm = NodeManager::currentNM();
   DenseMap<Rational>::const_iterator iter, end;
   iter = sum.begin(), end = sum.end();
@@ -4677,7 +4676,7 @@ bool TheoryArithPrivate::tryToPropagate(RowIndex ridx, bool rowUp, ArithVar v, b
 }
 
 Node flattenImplication(Node imp){
-  NodeBuilder<> nb(kind::OR);
+  NodeBuilder nb(kind::OR);
   std::unordered_set<Node, NodeHashFunction> included;
   Node left = imp[0];
   Node right = imp[1];
@@ -4765,7 +4764,7 @@ bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, C
         // Add the explaination proofs.
         for (const auto constraint : explain)
         {
-          NodeBuilder<> nb;
+          NodeBuilder nb;
           conflictPfs.push_back(constraint->externalExplainByAssertions(nb));
         }
         // Collect the farkas coefficients, as nodes.
@@ -5270,7 +5269,7 @@ void TheoryArithPrivate::entailmentCheckRowSum(std::pair<Node, DeltaRational>& t
   Assert(Polynomial::isMember(tp));
 
   tmp.second = DeltaRational(0);
-  NodeBuilder<> nb(kind::AND);
+  NodeBuilder nb(kind::AND);
 
   Polynomial p = Polynomial::parsePolynomial(tp);
   for(Polynomial::iterator i = p.begin(), iend = p.end(); i != iend; ++i) {
@@ -5455,7 +5454,7 @@ std::pair<Node, DeltaRational> TheoryArithPrivate::entailmentCheckSimplex(int sg
   switch(finalState){
   case Inferred:
     {
-      NodeBuilder<> nb(kind::AND);
+      NodeBuilder nb(kind::AND);
       for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx); !ri.atEnd(); ++ri){
         const Tableau::Entry& e =*ri;
         ArithVar colVar = e.getColVar();
@@ -5668,7 +5667,7 @@ ArithProofRuleChecker* TheoryArithPrivate::getProofChecker()
 //   switch(finalState){
 //   case Inferred:
 //     {
-//       NodeBuilder<> nb(kind::AND);
+//       NodeBuilder nb(kind::AND);
 //       for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx);
 //       !ri.atEnd(); ++ri){
 //         const Tableau::Entry& e =*ri;
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index ca2df4bd8..ba3fdfaf5 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -474,7 +474,7 @@ private:
   void notifyRestart();
   Theory::PPAssertStatus ppAssert(TrustNode tin,
                                   TrustSubstitutionMap& outSubstitutions);
-  void ppStaticLearn(TNode in, NodeBuilder<>& learned);
+  void ppStaticLearn(TNode in, NodeBuilder& learned);
 
   std::string identify() const { return std::string("TheoryArith"); }
 
@@ -681,8 +681,7 @@ private:
   bool isImpliedUpperBound(ArithVar var, Node exp);
   bool isImpliedLowerBound(ArithVar var, Node exp);
 
-  void internalExplain(TNode n, NodeBuilder<>& explainBuilder);
-
+  void internalExplain(TNode n, NodeBuilder& explainBuilder);
 
   void asVectors(const Polynomial& p,
                  std::vector<Rational>& coeffs,