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