Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Black box testing of cvc5::Node.
11 : : */
12 : :
13 : : #include <cvc5/cvc5.h>
14 : :
15 : : #include <algorithm>
16 : : #include <sstream>
17 : : #include <string>
18 : : #include <vector>
19 : :
20 : : #include "expr/array_store_all.h"
21 : : #include "expr/dtype.h"
22 : : #include "expr/dtype_cons.h"
23 : : #include "expr/node.h"
24 : : #include "expr/node_builder.h"
25 : : #include "expr/node_manager.h"
26 : : #include "expr/node_value.h"
27 : : #include "expr/skolem_manager.h"
28 : : #include "options/base_options.h"
29 : : #include "options/io_utils.h"
30 : : #include "options/language.h"
31 : : #include "options/options_public.h"
32 : : #include "smt/solver_engine.h"
33 : : #include "test_node.h"
34 : : #include "theory/rewriter.h"
35 : : #include "util/bitvector.h"
36 : : #include "util/rational.h"
37 : :
38 : : namespace cvc5::internal {
39 : :
40 : : namespace test {
41 : :
42 : : namespace {
43 : : /** Returns N skolem nodes from 'nodeManager' with the same `type`. */
44 : 4 : std::vector<Node> makeNSkolemNodes(NodeManager* nodeManager,
45 : : uint32_t n,
46 : : TypeNode type)
47 : : {
48 : 4 : std::vector<Node> skolems;
49 : 4 : SkolemManager* sm = nodeManager->getSkolemManager();
50 [ + + ]: 16 : for (uint32_t i = 0; i < n; i++)
51 : : {
52 : 12 : skolems.push_back(sm->mkDummySkolem("skolem_", type));
53 : : }
54 : 4 : return skolems;
55 : 0 : }
56 : : } // namespace
57 : :
58 : : class TestNodeBlackNode : public TestNode
59 : : {
60 : : protected:
61 : 32 : void SetUp() override
62 : : {
63 : 32 : TestNode::SetUp();
64 : : // setup an SMT engine so that options are in scope
65 : 32 : Options opts;
66 : 32 : d_slvEngine.reset(new SolverEngine(d_nodeManager.get(), &opts));
67 : 32 : d_slvEngine->setOption("output-language", "ast");
68 : 32 : }
69 : :
70 : : std::unique_ptr<SolverEngine> d_slvEngine;
71 : :
72 : : bool imp(bool a, bool b) const { return (!a) || (b); }
73 [ - + ][ - - ]: 9 : bool iff(bool a, bool b) const { return (a && b) || ((!a) && (!b)); }
[ + - ][ + - ]
74 : :
75 : 500 : void testNaryExpForSize(Kind k, uint32_t n)
76 : : {
77 : 500 : NodeBuilder nbz(d_nodeManager.get(), k);
78 : 500 : Node trueNode = d_nodeManager->mkConst(true);
79 [ + + ]: 257226 : for (uint32_t i = 0; i < n; ++i)
80 : : {
81 : 256726 : nbz << trueNode;
82 : : }
83 : 500 : Node result = nbz;
84 [ - + ][ + - ]: 500 : ASSERT_EQ(n, result.getNumChildren());
85 [ + - ][ + - ]: 500 : }
[ + - ]
86 : : };
87 : :
88 : 4 : TEST_F(TestNodeBlackNode, null) { Node::null(); }
89 : :
90 : 4 : TEST_F(TestNodeBlackNode, is_null)
91 : : {
92 : 1 : Node a = Node::null();
93 [ - + ][ + - ]: 1 : ASSERT_TRUE(a.isNull());
94 : :
95 : 1 : Node b = Node();
96 [ - + ][ + - ]: 1 : ASSERT_TRUE(b.isNull());
97 : :
98 : 1 : Node c = b;
99 [ - + ][ + - ]: 1 : ASSERT_TRUE(c.isNull());
100 [ + - ]: 1 : }
101 : :
102 : 4 : TEST_F(TestNodeBlackNode, copy_ctor) { Node e(Node::null()); }
103 : :
104 : 4 : TEST_F(TestNodeBlackNode, dtor)
105 : : {
106 : : /* No access to internals? Only test that this is crash free. */
107 : 1 : Node* n = nullptr;
108 [ + - ][ + - ]: 1 : ASSERT_NO_FATAL_FAILURE(n = new Node());
[ - + ][ + - ]
109 [ + - ]: 1 : if (n)
110 : : {
111 [ + - ]: 1 : delete n;
112 : : }
113 : : }
114 : :
115 : : /* operator== */
116 : 4 : TEST_F(TestNodeBlackNode, operator_equals)
117 : : {
118 : 1 : Node a, b, c;
119 : :
120 : 1 : b = d_skolemManager->mkDummySkolem("b", d_nodeManager->booleanType());
121 : :
122 : 1 : a = b;
123 : 1 : c = a;
124 : :
125 : 2 : Node d = d_skolemManager->mkDummySkolem("d", d_nodeManager->booleanType());
126 : :
127 [ - + ][ + - ]: 1 : ASSERT_TRUE(a == a);
128 [ - + ][ + - ]: 1 : ASSERT_TRUE(a == b);
129 [ - + ][ + - ]: 1 : ASSERT_TRUE(a == c);
130 : :
131 [ - + ][ + - ]: 1 : ASSERT_TRUE(b == a);
132 [ - + ][ + - ]: 1 : ASSERT_TRUE(b == b);
133 [ - + ][ + - ]: 1 : ASSERT_TRUE(b == c);
134 : :
135 [ - + ][ + - ]: 1 : ASSERT_TRUE(c == a);
136 [ - + ][ + - ]: 1 : ASSERT_TRUE(c == b);
137 [ - + ][ + - ]: 1 : ASSERT_TRUE(c == c);
138 : :
139 [ - + ][ + - ]: 1 : ASSERT_TRUE(d == d);
140 : :
141 [ - + ][ + - ]: 1 : ASSERT_FALSE(d == a);
142 [ - + ][ + - ]: 1 : ASSERT_FALSE(d == b);
143 [ - + ][ + - ]: 1 : ASSERT_FALSE(d == c);
144 : :
145 [ - + ][ + - ]: 1 : ASSERT_FALSE(a == d);
146 [ - + ][ + - ]: 1 : ASSERT_FALSE(b == d);
147 [ - + ][ + - ]: 1 : ASSERT_FALSE(c == d);
148 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
149 : :
150 : : /* operator!= */
151 : 4 : TEST_F(TestNodeBlackNode, operator_not_equals)
152 : : {
153 : 1 : Node a, b, c;
154 : :
155 : 1 : b = d_skolemManager->mkDummySkolem("b", d_nodeManager->booleanType());
156 : :
157 : 1 : a = b;
158 : 1 : c = a;
159 : :
160 : 2 : Node d = d_skolemManager->mkDummySkolem("d", d_nodeManager->booleanType());
161 : :
162 : : /*structed assuming operator == works */
163 [ - + ][ + - ]: 1 : ASSERT_TRUE(iff(a != a, !(a == a)));
164 [ - + ][ + - ]: 1 : ASSERT_TRUE(iff(a != b, !(a == b)));
165 [ - + ][ + - ]: 1 : ASSERT_TRUE(iff(a != c, !(a == c)));
166 : :
167 [ - + ][ + - ]: 1 : ASSERT_TRUE(iff(b != a, !(b == a)));
168 [ - + ][ + - ]: 1 : ASSERT_TRUE(iff(b != b, !(b == b)));
169 [ - + ][ + - ]: 1 : ASSERT_TRUE(iff(b != c, !(b == c)));
170 : :
171 [ - + ][ + - ]: 1 : ASSERT_TRUE(iff(c != a, !(c == a)));
172 [ - + ][ + - ]: 1 : ASSERT_TRUE(iff(c != b, !(c == b)));
173 [ - + ][ + - ]: 1 : ASSERT_TRUE(iff(c != c, !(c == c)));
174 : :
175 [ - + ][ + - ]: 1 : ASSERT_TRUE(!(d != d));
176 : :
177 [ - + ][ + - ]: 1 : ASSERT_TRUE(d != a);
178 [ - + ][ + - ]: 1 : ASSERT_TRUE(d != b);
179 [ - + ][ + - ]: 1 : ASSERT_TRUE(d != c);
180 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
181 : :
182 : : /* operator[] */
183 : 4 : TEST_F(TestNodeBlackNode, operator_square)
184 : : {
185 : : #ifdef CVC5_ASSERTIONS
186 : : // Basic bounds check on a node w/out children
187 : 1 : ASSERT_DEATH(Node::null()[-1], "i >= 0 && unsigned\\(i\\) < d_nchildren");
188 : 1 : ASSERT_DEATH(Node::null()[0], "i >= 0 && unsigned\\(i\\) < d_nchildren");
189 : : #endif
190 : :
191 : : // Basic access check
192 : 1 : Node tb = d_nodeManager->mkConst(true);
193 : 1 : Node eb = d_nodeManager->mkConst(false);
194 : 2 : Node cnd = d_nodeManager->mkNode(Kind::XOR, tb, eb);
195 : 1 : Node ite = cnd.iteNode(tb, eb);
196 : :
197 [ - + ][ + - ]: 2 : ASSERT_EQ(tb, cnd[0]);
198 [ - + ][ + - ]: 2 : ASSERT_EQ(eb, cnd[1]);
199 : :
200 [ - + ][ + - ]: 2 : ASSERT_EQ(cnd, ite[0]);
201 [ - + ][ + - ]: 2 : ASSERT_EQ(tb, ite[1]);
202 [ - + ][ + - ]: 2 : ASSERT_EQ(eb, ite[2]);
203 : :
204 : : #ifdef CVC5_ASSERTIONS
205 : : // Bounds check on a node with children
206 : 1 : ASSERT_DEATH(ite == ite[-1], "i >= 0 && unsigned\\(i\\) < d_nchildren");
207 : 1 : ASSERT_DEATH(ite == ite[4], "i >= 0 && unsigned\\(i\\) < d_nchildren");
208 : : #endif
209 : : }
210 : :
211 : : /* operator= */
212 : 4 : TEST_F(TestNodeBlackNode, operator_assign)
213 : : {
214 : 1 : Node a, b;
215 : 1 : Node c = d_nodeManager->mkNode(
216 : : Kind::NOT,
217 : 2 : d_skolemManager->mkDummySkolem("c", d_nodeManager->booleanType()));
218 : :
219 : 1 : b = c;
220 [ - + ][ + - ]: 1 : ASSERT_EQ(b, c);
221 : :
222 : 1 : a = b = c;
223 : :
224 [ - + ][ + - ]: 1 : ASSERT_EQ(a, b);
225 [ - + ][ + - ]: 1 : ASSERT_EQ(a, c);
226 [ + - ][ + - ]: 1 : }
[ + - ]
227 : :
228 : : /* operator< */
229 : 4 : TEST_F(TestNodeBlackNode, operator_less_than)
230 : : {
231 : : // We don't have access to the ids so we can't test the implementation
232 : : // in the black box tests.
233 : :
234 : 2 : Node a = d_skolemManager->mkDummySkolem("a", d_nodeManager->booleanType());
235 : 2 : Node b = d_skolemManager->mkDummySkolem("b", d_nodeManager->booleanType());
236 : :
237 [ - + ][ - - ]: 1 : ASSERT_TRUE(a < b || b < a);
[ - + ][ + - ]
238 [ + - ][ + - ]: 1 : ASSERT_TRUE(!(a < b && b < a));
[ - + ][ + - ]
239 : :
240 : 2 : Node c = d_nodeManager->mkNode(Kind::AND, a, b);
241 : 2 : Node d = d_nodeManager->mkNode(Kind::AND, a, b);
242 : :
243 [ - + ][ + - ]: 1 : ASSERT_FALSE(c < d);
244 [ - + ][ + - ]: 1 : ASSERT_FALSE(d < c);
245 : :
246 : : // simple test of descending descendant property
247 : 1 : Node child = d_nodeManager->mkConst(true);
248 : 1 : Node parent = d_nodeManager->mkNode(Kind::NOT, child);
249 : :
250 [ - + ][ + - ]: 1 : ASSERT_TRUE(child < parent);
251 : :
252 : : // slightly less simple test of DD property
253 : 1 : std::vector<Node> chain;
254 : 1 : const int N = 500;
255 : 2 : Node curr = d_nodeManager->mkNode(Kind::OR, a, b);
256 : 1 : chain.push_back(curr);
257 [ + + ]: 501 : for (int i = 0; i < N; ++i)
258 : : {
259 : 500 : curr = d_nodeManager->mkNode(Kind::AND, curr, curr);
260 : 500 : chain.push_back(curr);
261 : : }
262 : :
263 [ + + ]: 501 : for (int i = 0; i < N; ++i)
264 : : {
265 [ + + ]: 125250 : for (int j = i + 1; j < N; ++j)
266 : : {
267 : 124750 : Node chain_i = chain[i];
268 : 124750 : Node chain_j = chain[j];
269 [ - + ][ + - ]: 124750 : ASSERT_TRUE(chain_i < chain_j);
270 [ + - ][ + - ]: 124750 : }
271 : : }
272 [ + - ][ + - ]: 1 : }
273 : :
274 : 4 : TEST_F(TestNodeBlackNode, eqNode)
275 : : {
276 : 1 : TypeNode t = d_nodeManager->mkSort();
277 : 2 : Node left = d_skolemManager->mkDummySkolem("left", t);
278 : 2 : Node right = d_skolemManager->mkDummySkolem("right", t);
279 : 1 : Node eq = left.eqNode(right);
280 : :
281 [ - + ][ + - ]: 1 : ASSERT_EQ(Kind::EQUAL, eq.getKind());
282 [ - + ][ + - ]: 1 : ASSERT_EQ(2, eq.getNumChildren());
283 : :
284 [ - + ][ + - ]: 2 : ASSERT_EQ(eq[0], left);
285 [ - + ][ + - ]: 2 : ASSERT_EQ(eq[1], right);
286 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
287 : :
288 : 4 : TEST_F(TestNodeBlackNode, notNode)
289 : : {
290 : 1 : Node child = d_nodeManager->mkConst(true);
291 : 1 : Node parent = child.notNode();
292 : :
293 [ - + ][ + - ]: 1 : ASSERT_EQ(Kind::NOT, parent.getKind());
294 [ - + ][ + - ]: 1 : ASSERT_EQ(1, parent.getNumChildren());
295 : :
296 [ - + ][ + - ]: 2 : ASSERT_EQ(parent[0], child);
297 [ + - ][ + - ]: 1 : }
298 : :
299 : 4 : TEST_F(TestNodeBlackNode, andNode)
300 : : {
301 : 1 : Node left = d_nodeManager->mkConst(true);
302 : : Node right =
303 : 2 : d_nodeManager->mkNode(Kind::NOT, (d_nodeManager->mkConst(false)));
304 : 1 : Node eq = left.andNode(right);
305 : :
306 [ - + ][ + - ]: 1 : ASSERT_EQ(Kind::AND, eq.getKind());
307 [ - + ][ + - ]: 1 : ASSERT_EQ(2, eq.getNumChildren());
308 : :
309 [ - + ][ + - ]: 2 : ASSERT_EQ(*(eq.begin()), left);
310 [ - + ][ + - ]: 2 : ASSERT_EQ(*(++eq.begin()), right);
311 [ + - ][ + - ]: 1 : }
[ + - ]
312 : :
313 : 4 : TEST_F(TestNodeBlackNode, orNode)
314 : : {
315 : 1 : Node left = d_nodeManager->mkConst(true);
316 : : Node right =
317 : 2 : d_nodeManager->mkNode(Kind::NOT, (d_nodeManager->mkConst(false)));
318 : 1 : Node eq = left.orNode(right);
319 : :
320 [ - + ][ + - ]: 1 : ASSERT_EQ(Kind::OR, eq.getKind());
321 [ - + ][ + - ]: 1 : ASSERT_EQ(2, eq.getNumChildren());
322 : :
323 [ - + ][ + - ]: 2 : ASSERT_EQ(*(eq.begin()), left);
324 [ - + ][ + - ]: 2 : ASSERT_EQ(*(++eq.begin()), right);
325 [ + - ][ + - ]: 1 : }
[ + - ]
326 : :
327 : 4 : TEST_F(TestNodeBlackNode, iteNode)
328 : : {
329 : 2 : Node a = d_skolemManager->mkDummySkolem("a", d_nodeManager->booleanType());
330 : 2 : Node b = d_skolemManager->mkDummySkolem("b", d_nodeManager->booleanType());
331 : :
332 : 2 : Node cnd = d_nodeManager->mkNode(Kind::OR, a, b);
333 : 1 : Node thenBranch = d_nodeManager->mkConst(true);
334 : : Node elseBranch =
335 : 2 : d_nodeManager->mkNode(Kind::NOT, d_nodeManager->mkConst(false));
336 : 1 : Node ite = cnd.iteNode(thenBranch, elseBranch);
337 : :
338 [ - + ][ + - ]: 1 : ASSERT_EQ(Kind::ITE, ite.getKind());
339 [ - + ][ + - ]: 1 : ASSERT_EQ(3, ite.getNumChildren());
340 : :
341 [ - + ][ + - ]: 2 : ASSERT_EQ(*(ite.begin()), cnd);
342 [ - + ][ + - ]: 2 : ASSERT_EQ(*(++ite.begin()), thenBranch);
343 [ - + ][ + - ]: 2 : ASSERT_EQ(*(++(++ite.begin())), elseBranch);
344 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
345 : :
346 : 4 : TEST_F(TestNodeBlackNode, iffNode)
347 : : {
348 : 1 : Node left = d_nodeManager->mkConst(true);
349 : : Node right =
350 : 2 : d_nodeManager->mkNode(Kind::NOT, (d_nodeManager->mkConst(false)));
351 : 1 : Node eq = left.eqNode(right);
352 : :
353 [ - + ][ + - ]: 1 : ASSERT_EQ(Kind::EQUAL, eq.getKind());
354 [ - + ][ + - ]: 1 : ASSERT_EQ(2, eq.getNumChildren());
355 : :
356 [ - + ][ + - ]: 2 : ASSERT_EQ(*(eq.begin()), left);
357 [ - + ][ + - ]: 2 : ASSERT_EQ(*(++eq.begin()), right);
358 [ + - ][ + - ]: 1 : }
[ + - ]
359 : :
360 : 4 : TEST_F(TestNodeBlackNode, impNode)
361 : : {
362 : 1 : Node left = d_nodeManager->mkConst(true);
363 : : Node right =
364 : 2 : d_nodeManager->mkNode(Kind::NOT, (d_nodeManager->mkConst(false)));
365 : 1 : Node eq = left.impNode(right);
366 : :
367 [ - + ][ + - ]: 1 : ASSERT_EQ(Kind::IMPLIES, eq.getKind());
368 [ - + ][ + - ]: 1 : ASSERT_EQ(2, eq.getNumChildren());
369 : :
370 [ - + ][ + - ]: 2 : ASSERT_EQ(*(eq.begin()), left);
371 [ - + ][ + - ]: 2 : ASSERT_EQ(*(++eq.begin()), right);
372 [ + - ][ + - ]: 1 : }
[ + - ]
373 : :
374 : 4 : TEST_F(TestNodeBlackNode, xorNode)
375 : : {
376 : 1 : Node left = d_nodeManager->mkConst(true);
377 : : Node right =
378 : 2 : d_nodeManager->mkNode(Kind::NOT, (d_nodeManager->mkConst(false)));
379 : 1 : Node eq = left.xorNode(right);
380 : :
381 [ - + ][ + - ]: 1 : ASSERT_EQ(Kind::XOR, eq.getKind());
382 [ - + ][ + - ]: 1 : ASSERT_EQ(2, eq.getNumChildren());
383 : :
384 [ - + ][ + - ]: 2 : ASSERT_EQ(*(eq.begin()), left);
385 [ - + ][ + - ]: 2 : ASSERT_EQ(*(++eq.begin()), right);
386 [ + - ][ + - ]: 1 : }
[ + - ]
387 : :
388 : 4 : TEST_F(TestNodeBlackNode, getKind)
389 : : {
390 : 2 : Node a = d_skolemManager->mkDummySkolem("a", d_nodeManager->booleanType());
391 : 2 : Node b = d_skolemManager->mkDummySkolem("b", d_nodeManager->booleanType());
392 : :
393 : 1 : Node n = d_nodeManager->mkNode(Kind::NOT, a);
394 [ - + ][ + - ]: 1 : ASSERT_EQ(Kind::NOT, n.getKind());
395 : :
396 : 1 : n = d_nodeManager->mkNode(Kind::EQUAL, a, b);
397 [ - + ][ + - ]: 1 : ASSERT_EQ(Kind::EQUAL, n.getKind());
398 : :
399 : 2 : Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->realType());
400 : 2 : Node y = d_skolemManager->mkDummySkolem("y", d_nodeManager->realType());
401 : :
402 : 1 : n = d_nodeManager->mkNode(Kind::ADD, x, y);
403 [ - + ][ + - ]: 1 : ASSERT_EQ(Kind::ADD, n.getKind());
404 : :
405 : 1 : n = d_nodeManager->mkNode(Kind::NEG, x);
406 [ - + ][ + - ]: 1 : ASSERT_EQ(Kind::NEG, n.getKind());
407 [ + - ][ + - ]: 1 : }
[ + - ]
408 : :
409 : 4 : TEST_F(TestNodeBlackNode, getOperator)
410 : : {
411 : 2 : TypeNode sort = d_nodeManager->mkSort("T");
412 : 1 : TypeNode booleanType = d_nodeManager->booleanType();
413 : 1 : TypeNode predType = d_nodeManager->mkFunctionType(sort, booleanType);
414 : :
415 : 2 : Node f = d_skolemManager->mkDummySkolem("f", predType);
416 : 2 : Node a = d_skolemManager->mkDummySkolem("a", sort);
417 : 2 : Node fa = d_nodeManager->mkNode(Kind::APPLY_UF, f, a);
418 : :
419 [ - + ][ + - ]: 1 : ASSERT_TRUE(fa.hasOperator());
420 [ - + ][ + - ]: 1 : ASSERT_FALSE(f.hasOperator());
421 [ - + ][ + - ]: 1 : ASSERT_FALSE(a.hasOperator());
422 : :
423 [ - + ][ + - ]: 1 : ASSERT_EQ(fa.getNumChildren(), 1);
424 [ - + ][ + - ]: 1 : ASSERT_EQ(f.getNumChildren(), 0);
425 [ - + ][ + - ]: 1 : ASSERT_EQ(a.getNumChildren(), 0);
426 : :
427 [ - + ][ + - ]: 2 : ASSERT_EQ(f, fa.getOperator());
428 : : #ifdef CVC5_ASSERTIONS
429 : 1 : ASSERT_DEATH(f.getOperator(), "mk == kind::metakind::PARAMETERIZED");
430 : 1 : ASSERT_DEATH(a.getOperator(), "mk == kind::metakind::PARAMETERIZED");
431 : : #endif
432 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
433 : :
434 : 4 : TEST_F(TestNodeBlackNode, getNumChildren)
435 : : {
436 : 1 : Node trueNode = d_nodeManager->mkConst(true);
437 : :
438 [ - + ][ + - ]: 1 : ASSERT_EQ(0, (Node::null()).getNumChildren());
439 [ - + ][ + - ]: 1 : ASSERT_EQ(1, trueNode.notNode().getNumChildren());
440 [ - + ][ + - ]: 1 : ASSERT_EQ(2, trueNode.andNode(trueNode).getNumChildren());
441 : :
442 : 1 : srand(0);
443 [ + + ]: 501 : for (uint32_t i = 0; i < 500; ++i)
444 : : {
445 : 500 : uint32_t n = rand() % 1000 + 2;
446 : 500 : testNaryExpForSize(Kind::AND, n);
447 : : }
448 : :
449 : : #ifdef CVC5_ASSERTIONS
450 : 1 : ASSERT_DEATH(testNaryExpForSize(Kind::AND, 0),
451 : : "getNumChildren\\(\\) >= "
452 : : "kind::metakind::getMinArityForKind\\(getKind\\(\\)\\)");
453 : 1 : ASSERT_DEATH(testNaryExpForSize(Kind::AND, 1),
454 : : "getNumChildren\\(\\) >= "
455 : : "kind::metakind::getMinArityForKind\\(getKind\\(\\)\\)");
456 : 1 : ASSERT_DEATH(testNaryExpForSize(Kind::NOT, 0),
457 : : "getNumChildren\\(\\) >= "
458 : : "kind::metakind::getMinArityForKind\\(getKind\\(\\)\\)");
459 : 1 : ASSERT_DEATH(testNaryExpForSize(Kind::NOT, 2),
460 : : "getNumChildren\\(\\) <= "
461 : : "kind::metakind::getMaxArityForKind\\(getKind\\(\\)\\)");
462 : : #endif /* CVC5_ASSERTIONS */
463 [ + - ]: 1 : }
464 : :
465 : 4 : TEST_F(TestNodeBlackNode, iterator)
466 : : {
467 : 1 : NodeBuilder b(d_nodeManager.get());
468 : 2 : Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType());
469 : 2 : Node y = d_skolemManager->mkDummySkolem("y", d_nodeManager->booleanType());
470 : 2 : Node z = d_skolemManager->mkDummySkolem("z", d_nodeManager->booleanType());
471 : 1 : Node n = b << x << y << z << Kind::AND;
472 : :
473 : : { // iterator
474 : 1 : Node::iterator i = n.begin();
475 [ - + ][ + - ]: 2 : ASSERT_EQ(*i++, x);
476 [ - + ][ + - ]: 2 : ASSERT_EQ(*i++, y);
477 [ - + ][ + - ]: 2 : ASSERT_EQ(*i++, z);
478 [ - + ][ + - ]: 1 : ASSERT_EQ(i, n.end());
479 : : }
480 : :
481 : : { // same for const iterator
482 : 1 : const Node& c = n;
483 : 1 : Node::const_iterator i = c.begin();
484 [ - + ][ + - ]: 2 : ASSERT_EQ(*i++, x);
485 [ - + ][ + - ]: 2 : ASSERT_EQ(*i++, y);
486 [ - + ][ + - ]: 2 : ASSERT_EQ(*i++, z);
487 [ - + ][ + - ]: 1 : ASSERT_EQ(i, n.end());
488 : : }
489 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ]
490 : :
491 : 4 : TEST_F(TestNodeBlackNode, const_reverse_iterator)
492 : : {
493 : 1 : NodeBuilder b(d_nodeManager.get());
494 : 2 : Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType());
495 : 2 : Node y = d_skolemManager->mkDummySkolem("y", d_nodeManager->booleanType());
496 : 2 : Node z = d_skolemManager->mkDummySkolem("z", d_nodeManager->booleanType());
497 : 1 : Node n = b << x << y << z << Kind::AND;
498 : :
499 : : { // same for const iterator
500 : 1 : const Node& c = n;
501 : 1 : Node::const_reverse_iterator i = c.rbegin();
502 [ - + ][ + - ]: 2 : ASSERT_EQ(*i++, z);
503 [ - + ][ + - ]: 2 : ASSERT_EQ(*i++, y);
504 [ - + ][ + - ]: 2 : ASSERT_EQ(*i++, x);
505 [ - + ][ + - ]: 1 : ASSERT_EQ(i, n.rend());
506 : : }
507 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ]
508 : :
509 : 4 : TEST_F(TestNodeBlackNode, kinded_iterator)
510 : : {
511 : 1 : TypeNode integerType = d_nodeManager->integerType();
512 : :
513 : 2 : Node x = d_skolemManager->mkDummySkolem("x", integerType);
514 : 2 : Node y = d_skolemManager->mkDummySkolem("y", integerType);
515 : 2 : Node z = d_skolemManager->mkDummySkolem("z", integerType);
516 : 2 : Node plus_x_y_z = d_nodeManager->mkNode(Kind::ADD, x, y, z);
517 : 2 : Node x_minus_y = d_nodeManager->mkNode(Kind::SUB, x, y);
518 : :
519 : : { // iterator
520 : 1 : Node::kinded_iterator i = plus_x_y_z.begin(Kind::ADD);
521 [ - + ][ + - ]: 2 : ASSERT_EQ(*i++, x);
522 [ - + ][ + - ]: 2 : ASSERT_EQ(*i++, y);
523 [ - + ][ + - ]: 2 : ASSERT_EQ(*i++, z);
524 [ - + ][ + - ]: 1 : ASSERT_TRUE(i == plus_x_y_z.end(Kind::ADD));
525 : :
526 : 1 : i = x.begin(Kind::ADD);
527 [ - + ][ + - ]: 2 : ASSERT_EQ(*i++, x);
528 [ - + ][ + - ]: 1 : ASSERT_TRUE(i == x.end(Kind::ADD));
529 [ + - ]: 1 : }
530 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
531 : :
532 : 4 : TEST_F(TestNodeBlackNode, toString)
533 : : {
534 : 1 : TypeNode booleanType = d_nodeManager->booleanType();
535 : :
536 : 1 : Node w = d_skolemManager->mkDummySkolem(
537 : 2 : "w", booleanType, SkolemFlags::SKOLEM_EXACT_NAME);
538 : 1 : Node x = d_skolemManager->mkDummySkolem(
539 : 2 : "x", booleanType, SkolemFlags::SKOLEM_EXACT_NAME);
540 : 1 : Node y = d_skolemManager->mkDummySkolem(
541 : 2 : "y", booleanType, SkolemFlags::SKOLEM_EXACT_NAME);
542 : 1 : Node z = d_skolemManager->mkDummySkolem(
543 : 2 : "z", booleanType, SkolemFlags::SKOLEM_EXACT_NAME);
544 : 1 : Node m = NodeBuilder(d_nodeManager.get()) << w << x << Kind::OR;
545 : 1 : Node n = NodeBuilder(d_nodeManager.get()) << m << y << z << Kind::AND;
546 : :
547 [ - + ][ + - ]: 2 : ASSERT_EQ(n.toString(), "(AND (OR w x) y z)");
548 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ]
549 : :
550 : 4 : TEST_F(TestNodeBlackNode, toStream)
551 : : {
552 : 1 : TypeNode booleanType = d_nodeManager->booleanType();
553 : :
554 : 1 : Node w = d_skolemManager->mkDummySkolem(
555 : 2 : "w", booleanType, SkolemFlags::SKOLEM_EXACT_NAME);
556 : 1 : Node x = d_skolemManager->mkDummySkolem(
557 : 2 : "x", booleanType, SkolemFlags::SKOLEM_EXACT_NAME);
558 : 1 : Node y = d_skolemManager->mkDummySkolem(
559 : 2 : "y", booleanType, SkolemFlags::SKOLEM_EXACT_NAME);
560 : 1 : Node z = d_skolemManager->mkDummySkolem(
561 : 2 : "z", booleanType, SkolemFlags::SKOLEM_EXACT_NAME);
562 : 1 : Node m = NodeBuilder(d_nodeManager.get()) << x << y << Kind::OR;
563 : 1 : Node n = NodeBuilder(d_nodeManager.get()) << w << m << z << Kind::AND;
564 : 1 : Node o = NodeBuilder(d_nodeManager.get()) << n << n << Kind::XOR;
565 : :
566 : 1 : std::stringstream sstr;
567 : 1 : options::ioutils::applyDagThresh(sstr, 0);
568 : 1 : n.toStream(sstr);
569 [ - + ][ + - ]: 2 : ASSERT_EQ(sstr.str(), "(AND w (OR x y) z)");
570 : :
571 : 1 : sstr.str(std::string());
572 : 1 : o.toStream(sstr);
573 [ - + ][ + - ]: 2 : ASSERT_EQ(sstr.str(), "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
574 : :
575 : 1 : sstr.str(std::string());
576 : 1 : sstr << n;
577 [ - + ][ + - ]: 2 : ASSERT_EQ(sstr.str(), "(AND w (OR x y) z)");
578 : :
579 : 1 : sstr.str(std::string());
580 : 1 : sstr << o;
581 [ - + ][ + - ]: 2 : ASSERT_EQ(sstr.str(), "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
582 : :
583 : 1 : sstr.str(std::string());
584 : 1 : options::ioutils::applyNodeDepth(sstr, -1);
585 : 1 : sstr << n;
586 [ - + ][ + - ]: 2 : ASSERT_EQ(sstr.str(), "(AND w (OR x y) z)");
587 : :
588 : 1 : sstr.str(std::string());
589 : 1 : sstr << o;
590 [ - + ][ + - ]: 2 : ASSERT_EQ(sstr.str(), "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
591 : :
592 : 1 : sstr.str(std::string());
593 : 1 : options::ioutils::applyNodeDepth(sstr, 1);
594 : 1 : sstr << n;
595 [ - + ][ + - ]: 2 : ASSERT_EQ(sstr.str(), "(AND w (OR (...) (...)) z)");
596 : :
597 : 1 : sstr.str(std::string());
598 : 1 : sstr << o;
599 [ - + ]: 2 : ASSERT_EQ(sstr.str(),
600 [ + - ]: 1 : "(XOR (AND (...) (...) (...)) (AND (...) (...) (...)))");
601 : :
602 : 1 : sstr.str(std::string());
603 : 1 : options::ioutils::applyNodeDepth(sstr, 2);
604 : 1 : sstr << n;
605 [ - + ][ + - ]: 2 : ASSERT_EQ(sstr.str(), "(AND w (OR x y) z)");
606 : :
607 : 1 : sstr.str(std::string());
608 : 1 : sstr << o;
609 [ - + ]: 2 : ASSERT_EQ(sstr.str(),
610 [ + - ]: 1 : "(XOR (AND w (OR (...) (...)) z) (AND w (OR (...) (...)) z))");
611 : :
612 : 1 : sstr.str(std::string());
613 : 1 : options::ioutils::applyNodeDepth(sstr, 3);
614 : 1 : sstr << n;
615 [ - + ][ + - ]: 2 : ASSERT_EQ(sstr.str(), "(AND w (OR x y) z)");
616 : :
617 : 1 : sstr.str(std::string());
618 : 1 : sstr << o;
619 [ - + ][ + - ]: 2 : ASSERT_EQ(sstr.str(), "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
620 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ]
621 : :
622 : 4 : TEST_F(TestNodeBlackNode, dagifier)
623 : : {
624 : 1 : TypeNode intType = d_nodeManager->integerType();
625 : 1 : TypeNode fnType = d_nodeManager->mkFunctionType(intType, intType);
626 : :
627 : 1 : Node x = d_skolemManager->mkDummySkolem(
628 : 2 : "x", intType, SkolemFlags::SKOLEM_EXACT_NAME);
629 : 1 : Node y = d_skolemManager->mkDummySkolem(
630 : 2 : "y", intType, SkolemFlags::SKOLEM_EXACT_NAME);
631 : 1 : Node f = d_skolemManager->mkDummySkolem(
632 : 2 : "f", fnType, SkolemFlags::SKOLEM_EXACT_NAME);
633 : 1 : Node g = d_skolemManager->mkDummySkolem(
634 : 2 : "g", fnType, SkolemFlags::SKOLEM_EXACT_NAME);
635 : 2 : Node fx = d_nodeManager->mkNode(Kind::APPLY_UF, f, x);
636 : 2 : Node fy = d_nodeManager->mkNode(Kind::APPLY_UF, f, y);
637 : 2 : Node gx = d_nodeManager->mkNode(Kind::APPLY_UF, g, x);
638 : 2 : Node gy = d_nodeManager->mkNode(Kind::APPLY_UF, g, y);
639 : 2 : Node fgx = d_nodeManager->mkNode(Kind::APPLY_UF, f, gx);
640 : 2 : Node ffx = d_nodeManager->mkNode(Kind::APPLY_UF, f, fx);
641 : 2 : Node fffx = d_nodeManager->mkNode(Kind::APPLY_UF, f, ffx);
642 : 2 : Node fffx_eq_x = d_nodeManager->mkNode(Kind::EQUAL, fffx, x);
643 : 2 : Node fffx_eq_y = d_nodeManager->mkNode(Kind::EQUAL, fffx, y);
644 : 2 : Node fx_eq_gx = d_nodeManager->mkNode(Kind::EQUAL, fx, gx);
645 : 2 : Node x_eq_y = d_nodeManager->mkNode(Kind::EQUAL, x, y);
646 : 2 : Node fgx_eq_gy = d_nodeManager->mkNode(Kind::EQUAL, fgx, gy);
647 : :
648 : 6 : Node n = d_nodeManager->mkNode(
649 : 1 : Kind::OR, {fffx_eq_x, fffx_eq_y, fx_eq_gx, x_eq_y, fgx_eq_gy});
650 : :
651 : 1 : std::stringstream sstr;
652 : 1 : options::ioutils::applyDagThresh(sstr, 0);
653 : 1 : options::ioutils::applyOutputLanguage(sstr, Language::LANG_SMTLIB_V2_6);
654 : 1 : sstr << n; // never dagify
655 [ - + ]: 2 : ASSERT_EQ(sstr.str(),
656 : : "(or (= (f (f (f x))) x) (= (f (f (f x))) y) (= (f x) (g x)) (= x "
657 [ + - ]: 1 : "y) (= (f (g x)) (g y)))");
658 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
659 : :
660 : 4 : TEST_F(TestNodeBlackNode, for_each_over_nodes_as_node)
661 : : {
662 : : const std::vector<Node> skolems =
663 : 1 : makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType());
664 : 1 : Node add = d_nodeManager->mkNode(Kind::ADD, skolems);
665 : 1 : std::vector<Node> children;
666 [ + + ]: 4 : for (Node child : add)
667 : : {
668 : 3 : children.push_back(child);
669 : 3 : }
670 [ + - ][ + - ]: 1 : ASSERT_TRUE(children.size() == skolems.size()
[ - + ]
671 [ + - ]: 1 : && std::equal(children.begin(), children.end(), skolems.begin()));
672 [ + - ][ + - ]: 1 : }
[ + - ]
673 : :
674 : 4 : TEST_F(TestNodeBlackNode, for_each_over_nodes_as_tnode)
675 : : {
676 : : const std::vector<Node> skolems =
677 : 1 : makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType());
678 : 1 : Node add = d_nodeManager->mkNode(Kind::ADD, skolems);
679 : 1 : std::vector<TNode> children;
680 [ + + ]: 4 : for (TNode child : add)
681 : : {
682 : 3 : children.push_back(child);
683 : 3 : }
684 [ + - ][ + - ]: 1 : ASSERT_TRUE(children.size() == skolems.size()
[ - + ]
685 [ + - ]: 1 : && std::equal(children.begin(), children.end(), skolems.begin()));
686 [ + - ][ + - ]: 1 : }
[ + - ]
687 : :
688 : 4 : TEST_F(TestNodeBlackNode, for_each_over_tnodes_as_node)
689 : : {
690 : : const std::vector<Node> skolems =
691 : 1 : makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType());
692 : 1 : Node add_node = d_nodeManager->mkNode(Kind::ADD, skolems);
693 : 1 : TNode add_tnode = add_node;
694 : 1 : std::vector<Node> children;
695 [ + + ]: 4 : for (Node child : add_tnode)
696 : : {
697 : 3 : children.push_back(child);
698 : 3 : }
699 [ + - ][ + - ]: 1 : ASSERT_TRUE(children.size() == skolems.size()
[ - + ]
700 [ + - ]: 1 : && std::equal(children.begin(), children.end(), skolems.begin()));
701 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
702 : :
703 : 4 : TEST_F(TestNodeBlackNode, for_each_over_tnodes_as_tnode)
704 : : {
705 : : const std::vector<Node> skolems =
706 : 1 : makeNSkolemNodes(d_nodeManager.get(), 3, d_nodeManager->integerType());
707 : 1 : Node add_node = d_nodeManager->mkNode(Kind::ADD, skolems);
708 : 1 : TNode add_tnode = add_node;
709 : 1 : std::vector<TNode> children;
710 [ + + ]: 4 : for (TNode child : add_tnode)
711 : : {
712 : 3 : children.push_back(child);
713 : 3 : }
714 [ + - ][ + - ]: 1 : ASSERT_TRUE(children.size() == skolems.size()
[ - + ]
715 [ + - ]: 1 : && std::equal(children.begin(), children.end(), skolems.begin()));
716 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
717 : :
718 : 4 : TEST_F(TestNodeBlackNode, isConst)
719 : : {
720 : : // more complicated "constants" exist in datatypes and arrays theories
721 : 2 : DType list("list");
722 : : std::shared_ptr<DTypeConstructor> consC =
723 : 1 : std::make_shared<DTypeConstructor>("cons");
724 : 1 : consC->addArg("car", d_nodeManager->integerType());
725 : 1 : consC->addArgSelf("cdr");
726 : 1 : list.addConstructor(consC);
727 : 1 : list.addConstructor(std::make_shared<DTypeConstructor>("nil"));
728 : 1 : TypeNode listType = d_nodeManager->mkDatatypeType(list);
729 : : const std::vector<std::shared_ptr<DTypeConstructor> >& lcons =
730 : 1 : listType.getDType().getConstructors();
731 : 1 : Node cons = lcons[0]->getConstructor();
732 : 1 : Node nil = lcons[1]->getConstructor();
733 : 2 : Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->integerType());
734 : 1 : Node cons_x_nil = d_nodeManager->mkNode(
735 : : Kind::APPLY_CONSTRUCTOR,
736 : : cons,
737 : : x,
738 : 2 : d_nodeManager->mkNode(Kind::APPLY_CONSTRUCTOR, nil));
739 : 1 : Node cons_1_nil = d_nodeManager->mkNode(
740 : : Kind::APPLY_CONSTRUCTOR,
741 : : cons,
742 : 2 : d_nodeManager->mkConstInt(Rational(1)),
743 : 4 : d_nodeManager->mkNode(Kind::APPLY_CONSTRUCTOR, nil));
744 : 1 : Node cons_1_cons_2_nil = d_nodeManager->mkNode(
745 : : Kind::APPLY_CONSTRUCTOR,
746 : : cons,
747 : 2 : d_nodeManager->mkConstInt(Rational(1)),
748 : 1 : d_nodeManager->mkNode(
749 : : Kind::APPLY_CONSTRUCTOR,
750 : : cons,
751 : 2 : d_nodeManager->mkConstInt(Rational(2)),
752 : 6 : d_nodeManager->mkNode(Kind::APPLY_CONSTRUCTOR, nil)));
753 [ - + ][ + - ]: 1 : ASSERT_TRUE(d_nodeManager->mkNode(Kind::APPLY_CONSTRUCTOR, nil).isConst());
754 [ - + ][ + - ]: 1 : ASSERT_FALSE(cons_x_nil.isConst());
755 [ - + ][ + - ]: 1 : ASSERT_TRUE(cons_1_nil.isConst());
756 [ - + ][ + - ]: 1 : ASSERT_TRUE(cons_1_cons_2_nil.isConst());
757 : :
758 : 3 : TypeNode arrType = d_nodeManager->mkArrayType(d_nodeManager->integerType(),
759 : 2 : d_nodeManager->integerType());
760 : 1 : Node zero = d_nodeManager->mkConstInt(Rational(0));
761 : 1 : Node one = d_nodeManager->mkConstInt(Rational(1));
762 : 1 : Node storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero));
763 [ - + ][ + - ]: 1 : ASSERT_TRUE(storeAll.isConst());
764 : :
765 : 2 : Node arr = d_nodeManager->mkNode(Kind::STORE, storeAll, zero, zero);
766 [ - + ][ + - ]: 1 : ASSERT_FALSE(arr.isConst());
767 : 1 : arr = d_nodeManager->mkNode(Kind::STORE, storeAll, zero, one);
768 [ - + ][ + - ]: 1 : ASSERT_TRUE(arr.isConst());
769 : 2 : Node arr2 = d_nodeManager->mkNode(Kind::STORE, arr, one, zero);
770 [ - + ][ + - ]: 1 : ASSERT_FALSE(arr2.isConst());
771 : 1 : arr2 = d_nodeManager->mkNode(Kind::STORE, arr, zero, one);
772 [ - + ][ + - ]: 1 : ASSERT_FALSE(arr2.isConst());
773 : :
774 : 2 : arrType = d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(1),
775 : 2 : d_nodeManager->mkBitVectorType(1));
776 : 1 : zero = d_nodeManager->mkConst(BitVector(1, unsigned(0)));
777 : 1 : one = d_nodeManager->mkConst(BitVector(1, unsigned(1)));
778 : 1 : storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero));
779 [ - + ][ + - ]: 1 : ASSERT_TRUE(storeAll.isConst());
780 : :
781 : 1 : arr = d_nodeManager->mkNode(Kind::STORE, storeAll, zero, zero);
782 [ - + ][ + - ]: 1 : ASSERT_FALSE(arr.isConst());
783 : 1 : arr = d_nodeManager->mkNode(Kind::STORE, storeAll, zero, one);
784 [ - + ][ + - ]: 1 : ASSERT_TRUE(arr.isConst());
785 : 1 : arr2 = d_nodeManager->mkNode(Kind::STORE, arr, one, zero);
786 [ - + ][ + - ]: 1 : ASSERT_FALSE(arr2.isConst());
787 : 1 : arr2 = d_nodeManager->mkNode(Kind::STORE, arr, one, one);
788 [ - + ][ + - ]: 1 : ASSERT_FALSE(arr2.isConst());
789 : 1 : arr2 = d_nodeManager->mkNode(Kind::STORE, arr, zero, one);
790 [ - + ][ + - ]: 1 : ASSERT_FALSE(arr2.isConst());
791 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ]
792 : :
793 : : namespace {
794 : 1 : Node level0(NodeManager* nm)
795 : : {
796 : 1 : SkolemManager* sm = nm->getSkolemManager();
797 : 1 : NodeBuilder nb(nm, Kind::AND);
798 : 2 : Node x = sm->mkDummySkolem("x", nm->booleanType());
799 : 1 : nb << x;
800 : 1 : nb << x;
801 : 2 : return Node(nb.constructNode());
802 : 1 : }
803 : 0 : TNode level1(NodeManager* nm) { return level0(nm); }
804 : : } // namespace
805 : :
806 : : /**
807 : : * This is for demonstrating what a certain type of user error looks like.
808 : : */
809 : 4 : TEST_F(TestNodeBlackNode, node_tnode_usage)
810 : : {
811 : 1 : Node n;
812 [ + - ][ + - ]: 1 : ASSERT_NO_FATAL_FAILURE(n = level0(d_nodeManager.get()));
[ - + ][ + - ]
813 : 1 : ASSERT_DEATH(n = level1(d_nodeManager.get()), "d_nv->d_rc > 0");
814 [ + - ]: 1 : }
815 : :
816 : : } // namespace test
817 : : } // namespace cvc5::internal
|
