Support braced-init-lists with `mkNode()` (#6580)

This commit adds support for braced-init-lists in calls to `mkNode()`,
e.g., `mkNode(REGEXP_EMPTY, {})`. Previously, such a call would result
in a node of kind `REGEXP_EMPTY` with a single null node as a child
because the compiler chose the `mkNode(Kind kind, TNode child1)` variant
and converted `{}` to a node using the default constructor. This commit
adds an overload of `mkNode()` that takes an `initializer_list<TNode>`
to allow this use case. It also adds a `mkNode()` overload with zero children
for convenience and removes the 4- and 5-children variants because they
saw little use. Finally, it makes the default constructor of `NodeTemplate` 
explicit to avoid accidental conversions.

3 files changed, 51 insertions, 52 deletions

diff --git a/src/expr/node.h b/src/expr/node.h
index 9258a3264..fdcfcbe5f 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -261,8 +261,12 @@ public:
                  Iterator substitutionsEnd,
                  std::unordered_map<TNode, TNode>& cache) const;
 
- /** Default constructor, makes a null expression. */
- NodeTemplate() : d_nv(&expr::NodeValue::null()) {}
+ /** Default constructor, makes a null expression.
+  *
+  * This constructor is `explicit` to avoid accidentially creating a null node
+  * from an empty braced-init-list.
+  */
+ explicit NodeTemplate() : d_nv(&expr::NodeValue::null()) {}
 
  /**
   * Conversion between nodes that are reference-counted and those that are
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 5d37a6db4..c44720b67 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -1152,4 +1152,22 @@ Kind NodeManager::getKindForFunction(TNode fun)
   return kind::UNDEFINED_KIND;
 }
 
+Node NodeManager::mkNode(Kind kind, std::initializer_list<TNode> children)
+{
+  NodeBuilder nb(this, kind);
+  nb.append(children.begin(), children.end());
+  return nb.constructNode();
+}
+
+Node NodeManager::mkNode(TNode opNode, std::initializer_list<TNode> children)
+{
+  NodeBuilder nb(this, operatorToKind(opNode));
+  if (opNode.getKind() != kind::BUILTIN)
+  {
+    nb << opNode;
+  }
+  nb.append(children.begin(), children.end());
+  return nb.constructNode();
+}
+
 }  // namespace cvc5
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 64db01300..e99c70f7c 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -428,6 +428,9 @@ class NodeManager
   static Kind getKindForFunction(TNode fun);
 
   // general expression-builders
+  //
+  /** Create a node with no child. */
+  Node mkNode(Kind kind);
 
   /** Create a node with one child. */
   Node mkNode(Kind kind, TNode child1);
@@ -438,18 +441,21 @@ class NodeManager
   /** Create a node with three children. */
   Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3);
 
-  /** Create a node with four children. */
-  Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3,
-              TNode child4);
-
-  /** Create a node with five children. */
-  Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3,
-              TNode child4, TNode child5);
-
   /** Create a node with an arbitrary number of children. */
   template <bool ref_count>
   Node mkNode(Kind kind, const std::vector<NodeTemplate<ref_count> >& children);
 
+  /** Create a node using an initializer list.
+   *
+   * This function serves two purposes:
+   * - We can avoid creating a temporary vector in some cases, e.g., when we
+   *   want to create a node with a fixed, large number of children
+   * - It makes sure that calls to `mkNode` that braced-init-lists work as
+   *   expected, e.g., mkNode(REGEXP_EMPTY, {}) will call this overload instead
+   *   of creating a node with a null node as a child.
+   */
+  Node mkNode(Kind kind, std::initializer_list<TNode> children);
+
   /**
    * Create an AND node with arbitrary number of children. This returns the
    * true node if children is empty, or the single node in children if
@@ -484,18 +490,17 @@ class NodeManager
   /** Create a node with three children by operator. */
   Node mkNode(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);
-
-  /** Create a node with five children by operator. */
-  Node mkNode(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);
 
+  /**
+   * Create a node by applying an operator to an arbitrary number of children.
+   *
+   * Analoguous to `mkNode(Kind, std::initializer_list<TNode>)`.
+   */
+  Node mkNode(TNode opNode, std::initializer_list<TNode> children);
+
   Node mkBoundVar(const std::string& name, const TypeNode& type);
 
   Node mkBoundVar(const TypeNode& type);
@@ -1170,6 +1175,12 @@ inline Kind NodeManager::operatorToKind(TNode n) {
   return kind::operatorToKind(n.d_nv);
 }
 
+inline Node NodeManager::mkNode(Kind kind)
+{
+  NodeBuilder nb(this, kind);
+  return nb.constructNode();
+}
+
 inline Node NodeManager::mkNode(Kind kind, TNode child1) {
   NodeBuilder nb(this, kind);
   nb << child1;
@@ -1189,20 +1200,6 @@ inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
   return nb.constructNode();
 }
 
-inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
-                                TNode child3, TNode child4) {
-  NodeBuilder nb(this, kind);
-  nb << child1 << child2 << child3 << child4;
-  return nb.constructNode();
-}
-
-inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
-                                TNode child3, TNode child4, TNode child5) {
-  NodeBuilder nb(this, kind);
-  nb << child1 << child2 << child3 << child4 << child5;
-  return nb.constructNode();
-}
-
 // N-ary version
 template <bool ref_count>
 inline Node NodeManager::mkNode(Kind kind,
@@ -1278,26 +1275,6 @@ inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
   return nb.constructNode();
 }
 
-inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
-                                TNode child3, TNode child4) {
-  NodeBuilder nb(this, operatorToKind(opNode));
-  if(opNode.getKind() != kind::BUILTIN) {
-    nb << opNode;
-  }
-  nb << child1 << child2 << child3 << child4;
-  return nb.constructNode();
-}
-
-inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
-                                TNode child3, TNode child4, TNode child5) {
-  NodeBuilder nb(this, operatorToKind(opNode));
-  if(opNode.getKind() != kind::BUILTIN) {
-    nb << opNode;
-  }
-  nb << child1 << child2 << child3 << child4 << child5;
-  return nb.constructNode();
-}
-
 // N-ary version for operators
 template <bool ref_count>
 inline Node NodeManager::mkNode(TNode opNode,