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.

diff --git a/src/expr/node.h b/src/expr/node.h
index 9258a32649681ecf7f2678afcd29f5f790a2057e..fdcfcbe5f28c08ee4f3f0aafd60546c59e24918e 100644 (file)
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -261,8 +261,12 @@ public:
                  Iterator substitutionsEnd,
                  std::unordered_map<TNode, TNode>& 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 5d37a6db4520bb02b2f447daec97408142c9e9b5..c44720b67da3c8668b0135e3353a7ee70921d844 100644 (file)
--- 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<TNode> children)
+{
+  NodeBuilder nb(this, kind);
+  nb.append(children.begin(), children.end());
+  return nb.constructNode();
+}
+
+Node NodeManager::mkNode(TNode opNode, std::initializer_list<TNode> 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 64db0130093833115156a2501cbeddf56b75b79f..e99c70f7ce9e95d3fccbf50f50dec5f5ea75897c 100644 (file)
--- 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 <bool ref_count>
   Node mkNode(Kind kind, const std::vector<NodeTemplate<ref_count> >& 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<TNode> 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 <bool ref_count>
   Node mkNode(TNode opNode, const std::vector<NodeTemplate<ref_count> >& children);
 
+  /**
+   * Create a node by applying an operator to an arbitrary number of children.
+   *
+   * Analoguous to `mkNode(Kind, std::initializer_list<TNode>)`.
+   */
+  Node mkNode(TNode opNode, std::initializer_list<TNode> 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 <bool ref_count>
 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 <bool ref_count>
 inline Node NodeManager::mkNode(TNode opNode,

diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index 6617fccb07aa0ef7ad9f10c75fa7073171360636..b842ae58e2b29b6a156fc072278ab64023c45003 100644 (file)
--- 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 3b40f925e359a95e5a84fa8b04cb3c967e977098..5824d8239137f3b89c63259c57c63840222f6d35 100644 (file)
--- 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 628c00c300756a28f0c32eea48ca78a91b8e4aab..4f340e774d7fd7896dc7251374ea18d2bef615c2 100644 (file)
--- 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 33e94d3e63c724b14be4c1eb76ecced7ba463b13..b9847e22abddc0dc52b1a4b92c14236ea74889f7 100644 (file)
--- 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<Node>() )" \
+    "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 167ce9570765f1e19f4a005c524890b0503e1dc7..164e4e1c056959eaa96bd3bd294a3fddbc579ed5 100644 (file)
--- 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<Node> 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 bc77a9bc52b9728fa87422136254f6002963eb77..5b046fbc59f125f19fa5bc24f63a07df9eec617b 100644 (file)
--- 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<Node> 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<Node> 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<Node> 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<size_t, size_t> SequencesRewriter::firstMatch(Node n, Node r)
   Assert(r.getType().isRegExp());
   NodeManager* nm = NodeManager::currentNM();
 
-  std::vector<Node> 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<String>();
 

diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index c0f1805ffd23a1a30a8be8a0b64842d47ab9b1bf..f1b591e43288863e145badd50eeb162cad5f5359 100644 (file)
--- 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 2309c0ac76c78f3dda099cc6e47ef0f873d7b016..852f06dbcf0be9923f7f0628862b326736179795 100644 (file)
--- 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 7d9d3b556bf8684f8f023cbce557bf7879f75c9c..de0c76ce1aa89fe9e82921b0f7ee23a375d82b37 100644 (file)
--- 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 6ba942b6b0d1d865f1e202b3094d4c03a6141e63..23d2bfd22f8a54c713e5c675c30e9c1e07bdcc83 100644 (file)
--- 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 02472e71ebf21bc8d9fd2fb21ebea3340e214ffd..bb7f900be5e85c762bf16a7fc4ec18fd09969486 100644 (file)
--- 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 1078a0e4e459aeb42052c2a9e9b81c569b0b183e..d7447f230bea93243edbb91a5cea087b9233229b 100644 (file)
--- 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));