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