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