summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/node.h8
-rw-r--r--src/expr/node_manager.cpp18
-rw-r--r--src/expr/node_manager.h77
-rw-r--r--src/theory/arith/arith_utilities.h2
-rw-r--r--src/theory/arith/bound_inference.cpp2
-rw-r--r--src/theory/fp/theory_fp_rewriter.cpp3
-rw-r--r--src/theory/strings/kinds2
-rw-r--r--src/theory/strings/regexp_solver.cpp3
-rw-r--r--src/theory/strings/sequences_rewriter.cpp18
-rw-r--r--src/theory/strings/theory_strings_preprocess.cpp4
-rw-r--r--test/unit/node/node_black.cpp2
-rw-r--r--test/unit/node/node_manager_black.cpp24
-rw-r--r--test/unit/theory/regexp_operation_black.cpp20
-rw-r--r--test/unit/theory/sequences_rewriter_white.cpp29
-rw-r--r--test/unit/util/boolean_simplification_black.cpp56
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<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 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<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 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 <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 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<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 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<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 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<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 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>{});
+ 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 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));
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback