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_black.cpp | 2 +- test/unit/node/node_manager_black.cpp | 24 ++--------- test/unit/theory/regexp_operation_black.cpp | 20 ++++----- test/unit/theory/sequences_rewriter_white.cpp | 29 ++++++------- test/unit/util/boolean_simplification_black.cpp | 56 +++++++++++-------------- 5 files changed, 53 insertions(+), 78 deletions(-) (limited to 'test') 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 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 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{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)); -- cgit v1.2.3