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