mostly CVC presentation language parsing and printing

3 files changed, 343 insertions, 39 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 21fc0a4a1..870c77383 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -136,8 +136,8 @@ IntegerType ExprManager::integerType() const {
   return IntegerType(Type(d_nodeManager, new TypeNode(d_nodeManager->integerType())));
 }
 
-Expr ExprManager::mkExpr(Kind kind, const Expr& child1) {
-  const unsigned n = 1;
+Expr ExprManager::mkExpr(Kind kind, Expr child1) {
+  const unsigned n = 1 - (kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED ? 1 : 0);
   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
                 "Exprs with kind %s must have at least %u children and "
                 "at most %u children (the one under construction has %u)",
@@ -152,8 +152,8 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1) {
   }
 }
 
-Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) {
-  const unsigned n = 2;
+Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2) {
+  const unsigned n = 2 - (kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED ? 1 : 0);
   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
                 "Exprs with kind %s must have at least %u children and "
                 "at most %u children (the one under construction has %u)",
@@ -170,9 +170,9 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) {
   }
 }
 
-Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
-                         const Expr& child3) {
-  const unsigned n = 3;
+Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2,
+                         Expr child3) {
+  const unsigned n = 3 - (kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED ? 1 : 0);
   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
                 "Exprs with kind %s must have at least %u children and "
                 "at most %u children (the one under construction has %u)",
@@ -190,9 +190,9 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
   }
 }
 
-Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
-                         const Expr& child3, const Expr& child4) {
-  const unsigned n = 4;
+Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2,
+                         Expr child3, Expr child4) {
+  const unsigned n = 4 - (kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED ? 1 : 0);
   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
                 "Exprs with kind %s must have at least %u children and "
                 "at most %u children (the one under construction has %u)",
@@ -211,10 +211,10 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
   }
 }
 
-Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
-                         const Expr& child3, const Expr& child4,
-                         const Expr& child5) {
-  const unsigned n = 5;
+Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2,
+                         Expr child3, Expr child4,
+                         Expr child5) {
+  const unsigned n = 5 - (kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED ? 1 : 0);
   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
                 "Exprs with kind %s must have at least %u children and "
                 "at most %u children (the one under construction has %u)",
@@ -235,7 +235,7 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
 }
 
 Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) {
-  const unsigned n = children.size();
+  const unsigned n = children.size() - (kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED ? 1 : 0);
   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
                 "Exprs with kind %s must have at least %u children and "
                 "at most %u children (the one under construction has %u)",
@@ -259,9 +259,141 @@ Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& children) {
   }
 }
 
+Expr ExprManager::mkExpr(Expr opExpr) {
+  const unsigned n = 0;
+  Kind kind = kind::operatorKindToKind(opExpr.getKind());
+  CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+                "This Expr constructor is for parameterized kinds only");
+  CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
+                "Exprs with kind %s must have at least %u children and "
+                "at most %u children (the one under construction has %u)",
+                kind::kindToString(kind).c_str(),
+                minArity(kind), maxArity(kind), n);
+  NodeManagerScope nms(d_nodeManager);
+  try {
+    INC_STAT(kind);
+    return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode()));
+  } catch (const TypeCheckingExceptionPrivate& e) {
+    throw TypeCheckingException(this, &e);
+  }
+}
+
+Expr ExprManager::mkExpr(Expr opExpr, Expr child1) {
+  const unsigned n = 1;
+  Kind kind = kind::operatorKindToKind(opExpr.getKind());
+  CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+                "This Expr constructor is for parameterized kinds only");
+  CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
+                "Exprs with kind %s must have at least %u children and "
+                "at most %u children (the one under construction has %u)",
+                kind::kindToString(kind).c_str(),
+                minArity(kind), maxArity(kind), n);
+  NodeManagerScope nms(d_nodeManager);
+  try {
+    INC_STAT(kind);
+    return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(), child1.getNode()));
+  } catch (const TypeCheckingExceptionPrivate& e) {
+    throw TypeCheckingException(this, &e);
+  }
+}
+
+Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2) {
+  const unsigned n = 2;
+  Kind kind = kind::operatorKindToKind(opExpr.getKind());
+  CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+                "This Expr constructor is for parameterized kinds only");
+  CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
+                "Exprs with kind %s must have at least %u children and "
+                "at most %u children (the one under construction has %u)",
+                kind::kindToString(kind).c_str(),
+                minArity(kind), maxArity(kind), n);
+  NodeManagerScope nms(d_nodeManager);
+  try {
+    INC_STAT(kind);
+    return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(),
+                                               child1.getNode(),
+                                               child2.getNode()));
+  } catch (const TypeCheckingExceptionPrivate& e) {
+    throw TypeCheckingException(this, &e);
+  }
+}
+
+Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3) {
+  const unsigned n = 3;
+  Kind kind = kind::operatorKindToKind(opExpr.getKind());
+  CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+                "This Expr constructor is for parameterized kinds only");
+  CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
+                "Exprs with kind %s must have at least %u children and "
+                "at most %u children (the one under construction has %u)",
+                kind::kindToString(kind).c_str(),
+                minArity(kind), maxArity(kind), n);
+  NodeManagerScope nms(d_nodeManager);
+  try {
+    INC_STAT(kind);
+    return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(),
+                                               child1.getNode(),
+                                               child2.getNode(),
+                                               child3.getNode()));
+  } catch (const TypeCheckingExceptionPrivate& e) {
+    throw TypeCheckingException(this, &e);
+  }
+}
+
+Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3,
+                         Expr child4) {
+  const unsigned n = 4;
+  Kind kind = kind::operatorKindToKind(opExpr.getKind());
+  CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+                "This Expr constructor is for parameterized kinds only");
+  CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
+                "Exprs with kind %s must have at least %u children and "
+                "at most %u children (the one under construction has %u)",
+                kind::kindToString(kind).c_str(),
+                minArity(kind), maxArity(kind), n);
+  NodeManagerScope nms(d_nodeManager);
+  try {
+    INC_STAT(kind);
+    return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(),
+                                               child1.getNode(),
+                                               child2.getNode(),
+                                               child3.getNode(),
+                                               child4.getNode()));
+  } catch (const TypeCheckingExceptionPrivate& e) {
+    throw TypeCheckingException(this, &e);
+  }
+}
+
+Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3,
+                         Expr child4, Expr child5) {
+  const unsigned n = 5;
+  Kind kind = kind::operatorKindToKind(opExpr.getKind());
+  CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+                "This Expr constructor is for parameterized kinds only");
+  CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
+                "Exprs with kind %s must have at least %u children and "
+                "at most %u children (the one under construction has %u)",
+                kind::kindToString(kind).c_str(),
+                minArity(kind), maxArity(kind), n);
+  NodeManagerScope nms(d_nodeManager);
+  try {
+    INC_STAT(kind);
+    return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(),
+                                               child1.getNode(),
+                                               child2.getNode(),
+                                               child3.getNode(),
+                                               child4.getNode(),
+                                               child5.getNode()));
+  } catch (const TypeCheckingExceptionPrivate& e) {
+    throw TypeCheckingException(this, &e);
+  }
+}
+
 Expr ExprManager::mkExpr(Expr opExpr, const std::vector<Expr>& children) {
   const unsigned n = children.size();
   Kind kind = kind::operatorKindToKind(opExpr.getKind());
+  CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+                "This Expr constructor is for parameterized kinds only");
   CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
                 "Exprs with kind %s must have at least %u children and "
                 "at most %u children (the one under construction has %u)",
@@ -286,13 +418,13 @@ Expr ExprManager::mkExpr(Expr opExpr, const std::vector<Expr>& children) {
 }
 
 /** Make a function type from domain to range. */
-FunctionType ExprManager::mkFunctionType(const Type& domain, const Type& range) {
+FunctionType ExprManager::mkFunctionType(Type domain, Type range) {
   NodeManagerScope nms(d_nodeManager);
   return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(*domain.d_typeNode, *range.d_typeNode))));
 }
 
 /** Make a function type with input types from argTypes. */
-FunctionType ExprManager::mkFunctionType(const std::vector<Type>& argTypes, const Type& range) {
+FunctionType ExprManager::mkFunctionType(const std::vector<Type>& argTypes, Type range) {
   NodeManagerScope nms(d_nodeManager);
   Assert( argTypes.size() >= 1 );
   std::vector<TypeNode> argTypeNodes;
@@ -436,7 +568,7 @@ SortConstructorType ExprManager::mkSortConstructor(const std::string& name,
  * @param check whether we should check the type as we compute it
  * (default: false)
  */
-Type ExprManager::getType(const Expr& e, bool check) throw (TypeCheckingException) {
+Type ExprManager::getType(Expr e, bool check) throw (TypeCheckingException) {
   NodeManagerScope nms(d_nodeManager);
   Type t;
   try {
@@ -448,7 +580,7 @@ Type ExprManager::getType(const Expr& e, bool check) throw (TypeCheckingExceptio
   return t;
 }
 
-Expr ExprManager::mkVar(const std::string& name, const Type& type) {
+Expr ExprManager::mkVar(const std::string& name, Type type) {
   NodeManagerScope nms(d_nodeManager);
   Node* n = d_nodeManager->mkVarPtr(name, *type.d_typeNode);
   Debug("nm") << "set " << name << " on " << *n << std::endl;
@@ -456,7 +588,7 @@ Expr ExprManager::mkVar(const std::string& name, const Type& type) {
   return Expr(this, n);
 }
 
-Expr ExprManager::mkVar(const Type& type) {
+Expr ExprManager::mkVar(Type type) {
   NodeManagerScope nms(d_nodeManager);
   INC_STAT_VAR(type);
   return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode));
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 415d05878..31ce7855a 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -127,7 +127,7 @@ public:
    * @param child1 kind the kind of expression
    * @return the expression
    */
-  Expr mkExpr(Kind kind, const Expr& child1);
+  Expr mkExpr(Kind kind, Expr child1);
 
   /**
    * Make a binary expression of a given kind (AND, PLUS, ...).
@@ -136,7 +136,7 @@ public:
    * @param child2 the second child of the new expression
    * @return the expression
    */
-  Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2);
+  Expr mkExpr(Kind kind, Expr child1, Expr child2);
 
   /**
    * Make a 3-ary expression of a given kind (AND, PLUS, ...).
@@ -146,8 +146,7 @@ public:
    * @param child3 the third child of the new expression
    * @return the expression
    */
-  Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2,
-              const Expr& child3);
+  Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3);
 
   /**
    * Make a 4-ary expression of a given kind (AND, PLUS, ...).
@@ -158,8 +157,7 @@ public:
    * @param child4 the fourth child of the new expression
    * @return the expression
    */
-  Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2,
-              const Expr& child3, const Expr& child4);
+  Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4);
 
   /**
    * Make a 5-ary expression of a given kind (AND, PLUS, ...).
@@ -171,11 +169,13 @@ public:
    * @param child5 the fifth child of the new expression
    * @return the expression
    */
-  Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2,
-              const Expr& child3, const Expr& child4, const Expr& child5);
+  Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4,
+              Expr child5);
 
   /**
-   * Make an n-ary expression of given kind given a vector of it's children
+   * Make an n-ary expression of given kind given a vector of its
+   * children
+   *
    * @param kind the kind of expression to build
    * @param children the subexpressions
    * @return the n-ary expression
@@ -183,8 +183,73 @@ public:
   Expr mkExpr(Kind kind, const std::vector<Expr>& children);
 
   /**
-   * Make an n-ary expression of given tre operator to appply and a vector of
-   * it's children
+   * Make a nullary parameterized expression with the given operator.
+   *
+   * @param opExpr the operator expression
+   * @return the nullary expression
+   */
+  Expr mkExpr(Expr opExpr);
+
+  /**
+   * Make a unary parameterized expression with the given operator.
+   *
+   * @param opExpr the operator expression
+   * @param child1 the subexpression
+   * @return the unary expression
+   */
+  Expr mkExpr(Expr opExpr, Expr child1);
+
+  /**
+   * Make a binary parameterized expression with the given operator.
+   *
+   * @param opExpr the operator expression
+   * @param child1 the first subexpression
+   * @param child2 the second subexpression
+   * @return the binary expression
+   */
+  Expr mkExpr(Expr opExpr, Expr child1, Expr child2);
+
+  /**
+   * Make a ternary parameterized expression with the given operator.
+   *
+   * @param opExpr the operator expression
+   * @param child1 the first subexpression
+   * @param child2 the second subexpression
+   * @param child3 the third subexpression
+   * @return the ternary expression
+   */
+  Expr mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3);
+
+  /**
+   * Make a quaternary parameterized expression with the given operator.
+   *
+   * @param opExpr the operator expression
+   * @param child1 the first subexpression
+   * @param child2 the second subexpression
+   * @param child3 the third subexpression
+   * @param child4 the fourth subexpression
+   * @return the quaternary expression
+   */
+  Expr mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3, Expr child4);
+
+  /**
+   * Make a quinary parameterized expression with the given operator.
+   *
+   * @param opExpr the operator expression
+   * @param child1 the first subexpression
+   * @param child2 the second subexpression
+   * @param child3 the third subexpression
+   * @param child4 the fourth subexpression
+   * @param child5 the fifth subexpression
+   * @return the quinary expression
+   */
+  Expr mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3, Expr child4,
+              Expr child5);
+
+  /**
+   * Make an n-ary expression of given operator to apply and a vector
+   * of its children
+   *
    * @param opExpr the operator expression
    * @param children the subexpressions
    * @return the n-ary expression
@@ -210,13 +275,13 @@ public:
 
 
   /** Make a function type from domain to range. */
-  FunctionType mkFunctionType(const Type& domain, const Type& range);
+  FunctionType mkFunctionType(Type domain, Type range);
 
   /**
    * Make a function type with input types from argTypes.
    * <code>argTypes</code> must have at least one element.
    */
-  FunctionType mkFunctionType(const std::vector<Type>& argTypes, const Type& range);
+  FunctionType mkFunctionType(const std::vector<Type>& argTypes, Type range);
 
   /**
    * Make a function type with input types from
@@ -279,12 +344,12 @@ public:
                                         size_t arity) const;
 
   /** Get the type of an expression */
-  Type getType(const Expr& e, bool check = false)
+  Type getType(Expr e, bool check = false)
     throw (TypeCheckingException);
 
   // variables are special, because duplicates are permitted
-  Expr mkVar(const std::string& name, const Type& type);
-  Expr mkVar(const Type& type);
+  Expr mkVar(const std::string& name, Type type);
+  Expr mkVar(Type type);
 
   /** Returns the minimum arity of the given kind. */
   static unsigned minArity(Kind kind);
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 7f7d37a52..94b7e5c40 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -303,7 +303,35 @@ public:
   template <bool ref_count>
   Node* mkNodePtr(Kind kind, const std::vector<NodeTemplate<ref_count> >& children);
 
-  /** Create a node by applying an operator to the children */
+  /** Create a node (with no children) by operator. */
+  Node mkNode(TNode opNode);
+  Node* mkNodePtr(TNode opNode);
+
+  /** Create a node with one child by operator. */
+  Node mkNode(TNode opNode, TNode child1);
+  Node* mkNodePtr(TNode opNode, TNode child1);
+
+  /** Create a node with two children by operator. */
+  Node mkNode(TNode opNode, TNode child1, TNode child2);
+  Node* mkNodePtr(TNode opNode, TNode child1, TNode child2);
+
+  /** Create a node with three children by operator. */
+  Node mkNode(TNode opNode, TNode child1, TNode child2, TNode child3);
+  Node* mkNodePtr(TNode opNode, TNode child1, TNode child2, TNode child3);
+
+  /** Create a node with four children by operator. */
+  Node mkNode(TNode opNode, TNode child1, TNode child2, TNode child3,
+              TNode child4);
+  Node* mkNodePtr(TNode opNode, TNode child1, TNode child2, TNode child3,
+              TNode child4);
+
+  /** Create a node with five children by operator. */
+  Node mkNode(TNode opNode, TNode child1, TNode child2, TNode child3,
+              TNode child4, TNode child5);
+  Node* mkNodePtr(TNode opNode, TNode child1, TNode child2, TNode child3,
+              TNode child4, TNode child5);
+
+  /** Create a node by applying an operator to the children. */
   template <bool ref_count>
   Node mkNode(TNode opNode, const std::vector<NodeTemplate<ref_count> >& children);
   template <bool ref_count>
@@ -1021,6 +1049,85 @@ inline Node* NodeManager::mkNodePtr(Kind kind,
   return nb.constructNodePtr();
 }
 
+// for operators
+inline Node NodeManager::mkNode(TNode opNode) {
+  NodeBuilder<1> nb(this, kind::operatorKindToKind(opNode.getKind()));
+  nb << opNode;
+  return nb.constructNode();
+}
+
+inline Node* NodeManager::mkNodePtr(TNode opNode) {
+  NodeBuilder<1> nb(this, kind::operatorKindToKind(opNode.getKind()));
+  nb << opNode;
+  return nb.constructNodePtr();
+}
+
+inline Node NodeManager::mkNode(TNode opNode, TNode child1) {
+  NodeBuilder<2> nb(this, kind::operatorKindToKind(opNode.getKind()));
+  nb << opNode << child1;
+  return nb.constructNode();
+}
+
+inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1) {
+  NodeBuilder<2> nb(this, kind::operatorKindToKind(opNode.getKind()));
+  nb << opNode << child1;
+  return nb.constructNodePtr();
+}
+
+inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2) {
+  NodeBuilder<3> nb(this, kind::operatorKindToKind(opNode.getKind()));
+  nb << opNode << child1 << child2;
+  return nb.constructNode();
+}
+
+inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2) {
+  NodeBuilder<3> nb(this, kind::operatorKindToKind(opNode.getKind()));
+  nb << opNode << child1 << child2;
+  return nb.constructNodePtr();
+}
+
+inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
+                                TNode child3) {
+  NodeBuilder<4> nb(this, kind::operatorKindToKind(opNode.getKind()));
+  nb << opNode << child1 << child2 << child3;
+  return nb.constructNode();
+}
+
+inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
+                                TNode child3) {
+  NodeBuilder<4> nb(this, kind::operatorKindToKind(opNode.getKind()));
+  nb << opNode << child1 << child2 << child3;
+  return nb.constructNodePtr();
+}
+
+inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
+                                TNode child3, TNode child4) {
+  NodeBuilder<5> nb(this, kind::operatorKindToKind(opNode.getKind()));
+  nb << opNode << child1 << child2 << child3 << child4;
+  return nb.constructNode();
+}
+
+inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
+                                TNode child3, TNode child4) {
+  NodeBuilder<5> nb(this, kind::operatorKindToKind(opNode.getKind()));
+  nb << opNode << child1 << child2 << child3 << child4;
+  return nb.constructNodePtr();
+}
+
+inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
+                                TNode child3, TNode child4, TNode child5) {
+  NodeBuilder<6> nb(this, kind::operatorKindToKind(opNode.getKind()));
+  nb << opNode << child1 << child2 << child3 << child4 << child5;
+  return nb.constructNode();
+}
+
+inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
+                                    TNode child3, TNode child4, TNode child5) {
+  NodeBuilder<6> nb(this, kind::operatorKindToKind(opNode.getKind()));
+  nb << opNode << child1 << child2 << child3 << child4 << child5;
+  return nb.constructNodePtr();
+}
+
 // N-ary version for operators
 template <bool ref_count>
 inline Node NodeManager::mkNode(TNode opNode,
@@ -1034,8 +1141,8 @@ inline Node NodeManager::mkNode(TNode opNode,
 
 template <bool ref_count>
 inline Node* NodeManager::mkNodePtr(TNode opNode,
-                                const std::vector<NodeTemplate<ref_count> >&
-                                children) {
+                                    const std::vector<NodeTemplate<ref_count> >&
+                                    children) {
   NodeBuilder<> nb(this, kind::operatorKindToKind(opNode.getKind()));
   nb << opNode;
   nb.append(children);