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.

1 files changed, 4 insertions, 20 deletions

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());