From bb39d534c89dc2569aa048bb053196bfa5bbb3a1 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 21 May 2021 09:05:45 -0700 Subject: 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` 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. --- test/unit/node/node_manager_black.cpp | 24 ++++-------------------- 1 file changed, 4 insertions(+), 20 deletions(-) (limited to 'test/unit/node/node_manager_black.cpp') 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()); -- cgit v1.2.3