From bb39d534c89dc2569aa048bb053196bfa5bbb3a1 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 21 May 2021 09:05:45 -0700 Subject: [PATCH] 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. --- src/expr/node.h | 8 +- src/expr/node_manager.cpp | 18 +++++ src/expr/node_manager.h | 77 +++++++------------ src/theory/arith/arith_utilities.h | 2 +- src/theory/arith/bound_inference.cpp | 2 +- src/theory/fp/theory_fp_rewriter.cpp | 3 +- src/theory/strings/kinds | 2 +- src/theory/strings/regexp_solver.cpp | 3 +- src/theory/strings/sequences_rewriter.cpp | 18 ++--- .../strings/theory_strings_preprocess.cpp | 4 +- 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 ++++--- .../util/boolean_simplification_black.cpp | 56 ++++++-------- 15 files changed, 119 insertions(+), 149 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& 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 children) +{ + NodeBuilder nb(this, kind); + nb.append(children.begin(), children.end()); + return nb.constructNode(); +} + +Node NodeManager::mkNode(TNode opNode, std::initializer_list 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 Node mkNode(Kind kind, const std::vector >& 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 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 Node mkNode(TNode opNode, const std::vector >& children); + /** + * Create a node by applying an operator to an arbitrary number of children. + * + * Analoguous to `mkNode(Kind, std::initializer_list)`. + */ + Node mkNode(TNode opNode, std::initializer_list 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 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 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() )" \ + "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 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 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 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 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 SequencesRewriter::firstMatch(Node n, Node r) Assert(r.getType().isRegExp()); NodeManager* nm = NodeManager::currentNM(); - std::vector 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(); 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; } 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)); -- 2.30.2