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.

10 files changed, 66 insertions, 71 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,
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index 6617fccb0..b842ae58e 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -231,7 +231,7 @@ inline Node getIdentity(Kind k){
   case kind::MULT:
   case kind::NONLINEAR_MULT:
     return mkRationalNode(1);
-  default: Unreachable(); return {};  // silence warning
+  default: Unreachable(); return Node::null();  // silence warning
   }
 }
 
diff --git a/src/theory/arith/bound_inference.cpp b/src/theory/arith/bound_inference.cpp
index 3b40f925e..5824d8239 100644
--- a/src/theory/arith/bound_inference.cpp
+++ b/src/theory/arith/bound_inference.cpp
@@ -43,7 +43,7 @@ Bounds BoundInference::get(const Node& lhs) const
   auto it = d_bounds.find(lhs);
   if (it == d_bounds.end())
   {
-    return Bounds{};
+    return Bounds();
   }
   return it->second;
 }
diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp
index 628c00c30..4f340e774 100644
--- a/src/theory/fp/theory_fp_rewriter.cpp
+++ b/src/theory/fp/theory_fp_rewriter.cpp
@@ -290,7 +290,8 @@ namespace rewrite {
     Assert(!isPreRewrite);  // Likely redundant in pre-rewrite
 
     if (node[1] > node[2]) {
-      Node normal = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_FMA,node[0],node[2],node[1],node[3]);
+      Node normal = NodeManager::currentNM()->mkNode(
+          kind::FLOATINGPOINT_FMA, {node[0], node[2], node[1], node[3]});
       return RewriteResponse(REWRITE_DONE, normal);
     } else {
       return RewriteResponse(REWRITE_DONE, node);
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index 33e94d3e6..b9847e22a 100644
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -49,7 +49,7 @@ sort STRING_TYPE \
 sort REGEXP_TYPE \
     Cardinality::INTEGERS \
     well-founded \
-    "NodeManager::currentNM()->mkNode(REGEXP_EMPTY, std::vector<Node>() )" \
+    "NodeManager::currentNM()->mkNode(REGEXP_EMPTY)" \
     "util/string.h" \
     "RegExp type"
 
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index 167ce9570..164e4e1c0 100644
--- a/src/theory/strings/regexp_solver.cpp
+++ b/src/theory/strings/regexp_solver.cpp
@@ -49,8 +49,7 @@ RegExpSolver::RegExpSolver(SolverState& s,
       d_regexp_opr(skc)
 {
   d_emptyString = NodeManager::currentNM()->mkConst(::cvc5::String(""));
-  std::vector<Node> nvec;
-  d_emptyRegexp = NodeManager::currentNM()->mkNode(REGEXP_EMPTY, nvec);
+  d_emptyRegexp = NodeManager::currentNM()->mkNode(REGEXP_EMPTY);
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);
 }
diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index bc77a9bc5..5b046fbc5 100644
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -757,8 +757,7 @@ Node SequencesRewriter::rewriteConcatRegExp(TNode node)
     else if (c.getKind() == REGEXP_EMPTY)
     {
       // re.++( ..., empty, ... ) ---> empty
-      std::vector<Node> nvec;
-      Node ret = nm->mkNode(REGEXP_EMPTY, nvec);
+      Node ret = nm->mkNode(REGEXP_EMPTY);
       return returnRewrite(node, ret, Rewrite::RE_CONCAT_EMPTY);
     }
     else
@@ -983,7 +982,6 @@ Node SequencesRewriter::rewriteAndOrRegExp(TNode node)
     }
   }
   NodeManager* nm = NodeManager::currentNM();
-  std::vector<Node> emptyVec;
   // use inclusion tests
   for (const Node& negMem : polRegExp[1])
   {
@@ -999,11 +997,11 @@ Node SequencesRewriter::rewriteAndOrRegExp(TNode node)
         Node retNode;
         if (nk == REGEXP_INTER)
         {
-          retNode = nm->mkNode(kind::REGEXP_EMPTY, emptyVec);
+          retNode = nm->mkNode(kind::REGEXP_EMPTY);
         }
         else
         {
-          retNode = nm->mkNode(REGEXP_STAR, nm->mkNode(REGEXP_SIGMA, emptyVec));
+          retNode = nm->mkNode(REGEXP_STAR, nm->mkNode(REGEXP_SIGMA));
         }
         return returnRewrite(node, retNode, Rewrite::RE_ANDOR_INC_CONFLICT);
       }
@@ -1014,11 +1012,11 @@ Node SequencesRewriter::rewriteAndOrRegExp(TNode node)
   {
     if (nk == REGEXP_INTER)
     {
-      retNode = nm->mkNode(REGEXP_STAR, nm->mkNode(REGEXP_SIGMA, emptyVec));
+      retNode = nm->mkNode(REGEXP_STAR, nm->mkNode(REGEXP_SIGMA));
     }
     else
     {
-      retNode = nm->mkNode(kind::REGEXP_EMPTY, emptyVec);
+      retNode = nm->mkNode(kind::REGEXP_EMPTY);
     }
   }
   else
@@ -1151,8 +1149,7 @@ Node SequencesRewriter::rewriteRangeRegExp(TNode node)
   if (ch[0] > ch[1])
   {
     // re.range( "B", "A" ) ---> re.none
-    std::vector<Node> emptyVec;
-    Node retNode = nm->mkNode(REGEXP_EMPTY, emptyVec);
+    Node retNode = nm->mkNode(REGEXP_EMPTY);
     return returnRewrite(node, retNode, Rewrite::RE_RANGE_EMPTY);
   }
   return node;
@@ -3176,8 +3173,7 @@ std::pair<size_t, size_t> SequencesRewriter::firstMatch(Node n, Node r)
   Assert(r.getType().isRegExp());
   NodeManager* nm = NodeManager::currentNM();
 
-  std::vector<Node> emptyVec;
-  Node sigmaStar = nm->mkNode(REGEXP_STAR, nm->mkNode(REGEXP_SIGMA, emptyVec));
+  Node sigmaStar = nm->mkNode(REGEXP_STAR, nm->mkNode(REGEXP_SIGMA));
   Node re = nm->mkNode(REGEXP_CONCAT, r, sigmaStar);
   String s = n.getConst<String>();
 
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index c0f1805ff..f1b591e43 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -96,7 +96,7 @@ Node StringsPreprocess::reduce(Node t,
     // Length of the result is at most m
     Node b14 = nm->mkNode(LEQ, nm->mkNode(STRING_LENGTH, skt), m);
 
-    Node b1 = nm->mkNode(AND, b11, b12, b13, b14);
+    Node b1 = nm->mkNode(AND, {b11, b12, b13, b14});
     Node b2 = skt.eqNode(emp);
     Node lemma = nm->mkNode(ITE, cond, b1, b2);
 
@@ -652,7 +652,7 @@ Node StringsPreprocess::reduce(Node t,
         nm->mkNode(ITE,
                    matchesEmpty,
                    res1,
-                   nm->mkNode(AND, splitX, firstMatch, k2Match, res2)),
+                   nm->mkNode(AND, {splitX, firstMatch, k2Match, res2})),
         k.eqNode(x)));
     retNode = k;
   }