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.

5 files changed, 53 insertions, 78 deletions

diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp
index 2309c0ac7..852f06dbc 100644
--- a/test/unit/node/node_black.cpp
+++ b/test/unit/node/node_black.cpp
@@ -620,7 +620,7 @@ TEST_F(TestNodeBlackNode, dagifier)
   Node fgx_eq_gy = d_nodeManager->mkNode(EQUAL, fgx, gy);
 
   Node n = d_nodeManager->mkNode(
-      OR, fffx_eq_x, fffx_eq_y, fx_eq_gx, x_eq_y, fgx_eq_gy);
+      OR, {fffx_eq_x, fffx_eq_y, fx_eq_gx, x_eq_y, fgx_eq_gy});
 
   std::stringstream sstr;
   sstr << Node::setdepth(-1) << Node::setlanguage(language::output::LANG_CVC);
diff --git a/test/unit/node/node_manager_black.cpp b/test/unit/node/node_manager_black.cpp
index 7d9d3b556..de0c76ce1 100644
--- a/test/unit/node/node_manager_black.cpp
+++ b/test/unit/node/node_manager_black.cpp
@@ -67,38 +67,22 @@ TEST_F(TestNodeBlackNodeManager, mkNode_three_children)
   ASSERT_EQ(n[2], z);
 }
 
-TEST_F(TestNodeBlackNodeManager, mkNode_four_children)
+TEST_F(TestNodeBlackNodeManager, mkNode_init_list)
 {
   Node x1 = d_skolemManager->mkDummySkolem("x1", d_nodeManager->booleanType());
   Node x2 = d_skolemManager->mkDummySkolem("x2", d_nodeManager->booleanType());
   Node x3 = d_skolemManager->mkDummySkolem("x3", d_nodeManager->booleanType());
   Node x4 = d_skolemManager->mkDummySkolem("x4", d_nodeManager->booleanType());
-  Node n = d_nodeManager->mkNode(AND, x1, x2, x3, x4);
+  // Negate second argument to test the use of temporary nodes
+  Node n = d_nodeManager->mkNode(AND, {x1, x2.negate(), x3, x4});
   ASSERT_EQ(n.getNumChildren(), 4u);
   ASSERT_EQ(n.getKind(), AND);
   ASSERT_EQ(n[0], x1);
-  ASSERT_EQ(n[1], x2);
+  ASSERT_EQ(n[1], x2.negate());
   ASSERT_EQ(n[2], x3);
   ASSERT_EQ(n[3], x4);
 }
 
-TEST_F(TestNodeBlackNodeManager, mkNode_five_children)
-{
-  Node x1 = d_skolemManager->mkDummySkolem("x1", d_nodeManager->booleanType());
-  Node x2 = d_skolemManager->mkDummySkolem("x2", d_nodeManager->booleanType());
-  Node x3 = d_skolemManager->mkDummySkolem("x3", d_nodeManager->booleanType());
-  Node x4 = d_skolemManager->mkDummySkolem("x4", d_nodeManager->booleanType());
-  Node x5 = d_skolemManager->mkDummySkolem("x5", d_nodeManager->booleanType());
-  Node n = d_nodeManager->mkNode(AND, x1, x2, x3, x4, x5);
-  ASSERT_EQ(n.getNumChildren(), 5u);
-  ASSERT_EQ(n.getKind(), AND);
-  ASSERT_EQ(n[0], x1);
-  ASSERT_EQ(n[1], x2);
-  ASSERT_EQ(n[2], x3);
-  ASSERT_EQ(n[3], x4);
-  ASSERT_EQ(n[4], x5);
-}
-
 TEST_F(TestNodeBlackNodeManager, mkNode_vector_of_node)
 {
   Node x1 = d_skolemManager->mkDummySkolem("x1", d_nodeManager->booleanType());
diff --git a/test/unit/theory/regexp_operation_black.cpp b/test/unit/theory/regexp_operation_black.cpp
index 6ba942b6b..23d2bfd22 100644
--- a/test/unit/theory/regexp_operation_black.cpp
+++ b/test/unit/theory/regexp_operation_black.cpp
@@ -66,7 +66,7 @@ class TestTheoryBlackRegexpOperation : public TestSmt
 
 TEST_F(TestTheoryBlackRegexpOperation, basic)
 {
-  Node sigma = d_nodeManager->mkNode(REGEXP_SIGMA, std::vector<Node>{});
+  Node sigma = d_nodeManager->mkNode(REGEXP_SIGMA);
   Node sigmaStar = d_nodeManager->mkNode(REGEXP_STAR, sigma);
   Node a = d_nodeManager->mkNode(STRING_TO_REGEXP,
                                  d_nodeManager->mkConst(String("a")));
@@ -93,7 +93,7 @@ TEST_F(TestTheoryBlackRegexpOperation, basic)
 
 TEST_F(TestTheoryBlackRegexpOperation, star_wildcards)
 {
-  Node sigma = d_nodeManager->mkNode(REGEXP_SIGMA, std::vector<Node>{});
+  Node sigma = d_nodeManager->mkNode(REGEXP_SIGMA);
   Node sigmaStar = d_nodeManager->mkNode(REGEXP_STAR, sigma);
   Node a = d_nodeManager->mkNode(STRING_TO_REGEXP,
                                  d_nodeManager->mkConst(String("a")));
@@ -104,22 +104,22 @@ TEST_F(TestTheoryBlackRegexpOperation, star_wildcards)
 
   Node _abc_ = d_nodeManager->mkNode(REGEXP_CONCAT, sigmaStar, abc, sigmaStar);
   Node _asc_ =
-      d_nodeManager->mkNode(REGEXP_CONCAT, sigmaStar, a, sigma, c, sigmaStar);
+      d_nodeManager->mkNode(REGEXP_CONCAT, {sigmaStar, a, sigma, c, sigmaStar});
   Node _sc_ = Rewriter::rewrite(
-      d_nodeManager->mkNode(REGEXP_CONCAT, sigmaStar, sigma, c, sigmaStar));
+      d_nodeManager->mkNode(REGEXP_CONCAT, {sigmaStar, sigma, c, sigmaStar}));
   Node _as_ = Rewriter::rewrite(
-      d_nodeManager->mkNode(REGEXP_CONCAT, sigmaStar, a, sigma, sigmaStar));
+      d_nodeManager->mkNode(REGEXP_CONCAT, {sigmaStar, a, sigma, sigmaStar}));
   Node _assc_ = d_nodeManager->mkNode(
       REGEXP_CONCAT,
       std::vector<Node>{sigmaStar, a, sigma, sigma, c, sigmaStar});
   Node _csa_ =
-      d_nodeManager->mkNode(REGEXP_CONCAT, sigmaStar, c, sigma, a, sigmaStar);
-  Node _c_a_ = d_nodeManager->mkNode(
-      REGEXP_CONCAT, sigmaStar, c, sigmaStar, a, sigmaStar);
+      d_nodeManager->mkNode(REGEXP_CONCAT, {sigmaStar, c, sigma, a, sigmaStar});
+  Node _c_a_ = d_nodeManager->mkNode(REGEXP_CONCAT,
+                                     {sigmaStar, c, sigmaStar, a, sigmaStar});
   Node _s_s_ = Rewriter::rewrite(d_nodeManager->mkNode(
-      REGEXP_CONCAT, sigmaStar, sigma, sigmaStar, sigma, sigmaStar));
+      REGEXP_CONCAT, {sigmaStar, sigma, sigmaStar, sigma, sigmaStar}));
   Node _a_abc_ = Rewriter::rewrite(d_nodeManager->mkNode(
-      REGEXP_CONCAT, sigmaStar, a, sigmaStar, abc, sigmaStar));
+      REGEXP_CONCAT, {sigmaStar, a, sigmaStar, abc, sigmaStar}));
 
   includes(_asc_, _abc_);
   doesNotInclude(_abc_, _asc_);
diff --git a/test/unit/theory/sequences_rewriter_white.cpp b/test/unit/theory/sequences_rewriter_white.cpp
index 02472e71e..bb7f900be 100644
--- a/test/unit/theory/sequences_rewriter_white.cpp
+++ b/test/unit/theory/sequences_rewriter_white.cpp
@@ -392,8 +392,8 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_concat)
   // (str.substr y 0 3))
   Node z = d_nodeManager->mkNode(kind::STRING_SUBSTR, y, zero, three);
   Node repl_e_x_z = d_nodeManager->mkNode(kind::STRING_STRREPL, empty, x, z);
-  repl_a = d_nodeManager->mkNode(kind::STRING_CONCAT, y, repl_e_x_z, z, a, z);
-  a_repl = d_nodeManager->mkNode(kind::STRING_CONCAT, y, z, repl_e_x_z, a, z);
+  repl_a = d_nodeManager->mkNode(kind::STRING_CONCAT, {y, repl_e_x_z, z, a, z});
+  a_repl = d_nodeManager->mkNode(kind::STRING_CONCAT, {y, z, repl_e_x_z, a, z});
   sameNormalForm(repl_a, a_repl);
 
   // Same normal form for:
@@ -452,10 +452,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, length_preserve_rewrite)
                             d_nodeManager->mkNode(kind::STRING_CONCAT, x, x));
   Node concat2 = d_nodeManager->mkNode(
       kind::STRING_CONCAT,
-      gh,
-      x,
-      d_nodeManager->mkNode(kind::STRING_STRREPL, x, gh, ij),
-      ij);
+      {gh, x, d_nodeManager->mkNode(kind::STRING_STRREPL, x, gh, ij), ij});
   Node res_concat1 = SequencesRewriter::lengthPreserveRewrite(concat1);
   Node res_concat2 = SequencesRewriter::lengthPreserveRewrite(concat2);
   ASSERT_EQ(res_concat1, res_concat2);
@@ -526,7 +523,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_indexOf)
     // (+ 2 (str.indexof (str.++ "A" x y) "A" 0))
     Node lhs = d_nodeManager->mkNode(
         kind::STRING_STRIDOF,
-        d_nodeManager->mkNode(kind::STRING_CONCAT, b, c, a, x, y),
+        d_nodeManager->mkNode(kind::STRING_CONCAT, {b, c, a, x, y}),
         a,
         zero);
     Node rhs = d_nodeManager->mkNode(
@@ -1296,10 +1293,10 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_contains)
     Node cat = d_nodeManager->mkNode(kind::STRING_CHARAT, x, n);
     lhs = d_nodeManager->mkNode(kind::STRING_STRCTN, abc, cat);
     rhs = d_nodeManager->mkNode(kind::OR,
-                                d_nodeManager->mkNode(kind::EQUAL, cat, empty),
-                                d_nodeManager->mkNode(kind::EQUAL, cat, a),
-                                d_nodeManager->mkNode(kind::EQUAL, cat, b),
-                                d_nodeManager->mkNode(kind::EQUAL, cat, c));
+                                {d_nodeManager->mkNode(kind::EQUAL, cat, empty),
+                                 d_nodeManager->mkNode(kind::EQUAL, cat, a),
+                                 d_nodeManager->mkNode(kind::EQUAL, cat, b),
+                                 d_nodeManager->mkNode(kind::EQUAL, cat, c)});
     sameNormalForm(lhs, rhs);
   }
 }
@@ -1325,7 +1322,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, infer_eqs_from_contains)
   sameNormalForm(StringsEntail::inferEqsFromContains(empty, xy), empty_x_y);
 
   // inferEqsFromContains(x, (str.++ x y)) returns false
-  Node bxya = d_nodeManager->mkNode(kind::STRING_CONCAT, b, y, x, a);
+  Node bxya = d_nodeManager->mkNode(kind::STRING_CONCAT, {b, y, x, a});
   sameNormalForm(StringsEntail::inferEqsFromContains(x, bxya), f);
 
   // inferEqsFromContains(x, y) returns null
@@ -1657,8 +1654,8 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_equality_ext)
     //      (= (str.++ y w) (str.++ "A" z)))
     Node lhs = d_nodeManager->mkNode(
         kind::EQUAL,
-        d_nodeManager->mkNode(kind::STRING_CONCAT, b, xrepl, z, y, w),
-        d_nodeManager->mkNode(kind::STRING_CONCAT, z, x, ba, z));
+        d_nodeManager->mkNode(kind::STRING_CONCAT, {b, xrepl, z, y, w}),
+        d_nodeManager->mkNode(kind::STRING_CONCAT, {z, x, ba, z}));
     Node rhs = d_nodeManager->mkNode(
         kind::AND,
         d_nodeManager->mkNode(
@@ -1804,8 +1801,8 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_membership)
     Node lhs = d_nodeManager->mkNode(
         kind::STRING_IN_REGEXP,
         x,
-        d_nodeManager->mkNode(
-            kind::REGEXP_CONCAT, sig_star, sig_star, re_abc, sig_star));
+        d_nodeManager->mkNode(kind::REGEXP_CONCAT,
+                              {sig_star, sig_star, re_abc, sig_star}));
     Node rhs = d_nodeManager->mkNode(kind::STRING_STRCTN, x, abc);
     sameNormalForm(lhs, rhs);
   }
diff --git a/test/unit/util/boolean_simplification_black.cpp b/test/unit/util/boolean_simplification_black.cpp
index 1078a0e4e..d7447f230 100644
--- a/test/unit/util/boolean_simplification_black.cpp
+++ b/test/unit/util/boolean_simplification_black.cpp
@@ -145,22 +145,16 @@ TEST_F(TestUtilBlackBooleanSimplification, simplifyClause)
   out = d_nodeManager->mkNode(kind::OR, d_a, d_d, d_b);
   test_nodes_equal(out, BooleanSimplification::simplifyClause(in));
 
-  in = d_nodeManager->mkNode(kind::OR,
-                             d_fa,
-                             d_ga.orNode(d_c).notNode(),
-                             d_hfc,
-                             d_ac,
-                             d_d.andNode(d_b));
+  in = d_nodeManager->mkNode(
+      kind::OR,
+      {d_fa, d_ga.orNode(d_c).notNode(), d_hfc, d_ac, d_d.andNode(d_b)});
   out = NodeBuilder(kind::OR) << d_fa << d_ga.orNode(d_c).notNode() << d_hfc
                               << d_ac << d_d.andNode(d_b);
   test_nodes_equal(out, BooleanSimplification::simplifyClause(in));
 
-  in = d_nodeManager->mkNode(kind::OR,
-                             d_fa,
-                             d_ga.andNode(d_c).notNode(),
-                             d_hfc,
-                             d_ac,
-                             d_d.andNode(d_b));
+  in = d_nodeManager->mkNode(
+      kind::OR,
+      {d_fa, d_ga.andNode(d_c).notNode(), d_hfc, d_ac, d_d.andNode(d_b)});
   out = NodeBuilder(kind::OR) << d_fa << d_ga.notNode() << d_c.notNode()
                               << d_hfc << d_ac << d_d.andNode(d_b);
   test_nodes_equal(out, BooleanSimplification::simplifyClause(in));
@@ -184,28 +178,28 @@ TEST_F(TestUtilBlackBooleanSimplification, simplifyHornClause)
   out = d_nodeManager->mkNode(kind::OR, d_a, d_ac.andNode(d_b));
   test_nodes_equal(out, BooleanSimplification::simplifyHornClause(in));
 
-  in =
-      d_a.andNode(d_b).impNode(d_nodeManager->mkNode(kind::AND,
-                                                     d_fa,
-                                                     d_ga.orNode(d_c).notNode(),
-                                                     d_hfc.orNode(d_ac),
-                                                     d_d.andNode(d_b)));
+  in = d_a.andNode(d_b).impNode(
+      d_nodeManager->mkNode(kind::AND,
+                            {d_fa,
+                             d_ga.orNode(d_c).notNode(),
+                             d_hfc.orNode(d_ac),
+                             d_d.andNode(d_b)}));
   out = d_nodeManager->mkNode(kind::OR,
                               d_a.notNode(),
                               d_b.notNode(),
                               d_nodeManager->mkNode(kind::AND,
-                                                    d_fa,
-                                                    d_ga.orNode(d_c).notNode(),
-                                                    d_hfc.orNode(d_ac),
-                                                    d_d.andNode(d_b)));
+                                                    {d_fa,
+                                                     d_ga.orNode(d_c).notNode(),
+                                                     d_hfc.orNode(d_ac),
+                                                     d_d.andNode(d_b)}));
   test_nodes_equal(out, BooleanSimplification::simplifyHornClause(in));
 
   in = d_a.andNode(d_b).impNode(
       d_nodeManager->mkNode(kind::OR,
-                            d_fa,
-                            d_ga.orNode(d_c).notNode(),
-                            d_hfc.orNode(d_ac),
-                            d_d.andNode(d_b).notNode()));
+                            {d_fa,
+                             d_ga.orNode(d_c).notNode(),
+                             d_hfc.orNode(d_ac),
+                             d_d.andNode(d_b).notNode()}));
   out = NodeBuilder(kind::OR)
         << d_a.notNode() << d_b.notNode() << d_fa << d_ga.orNode(d_c).notNode()
         << d_hfc << d_ac << d_d.notNode();
@@ -231,11 +225,11 @@ TEST_F(TestUtilBlackBooleanSimplification, simplifyConflict)
   test_nodes_equal(out, BooleanSimplification::simplifyConflict(in));
 
   in = d_nodeManager->mkNode(kind::AND,
-                             d_fa,
-                             d_ga.orNode(d_c).notNode(),
-                             d_fa,
-                             d_hfc.orNode(d_ac),
-                             d_d.andNode(d_b));
+                             {d_fa,
+                              d_ga.orNode(d_c).notNode(),
+                              d_fa,
+                              d_hfc.orNode(d_ac),
+                              d_d.andNode(d_b)});
   out = NodeBuilder(kind::AND) << d_fa << d_ga.notNode() << d_c.notNode()
                                << d_hfc.orNode(d_ac) << d_d << d_b;
   test_nodes_equal(out, BooleanSimplification::simplifyConflict(in));