Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Aina Niemetz, Andres Noetzli, Andrew Reynolds
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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::NodeBuilder.
14 : : */
15 : :
16 : : #include <limits.h>
17 : :
18 : : #include <sstream>
19 : : #include <vector>
20 : :
21 : : #include "base/check.h"
22 : : #include "expr/kind.h"
23 : : #include "expr/node.h"
24 : : #include "expr/node_builder.h"
25 : : #include "expr/node_manager.h"
26 : : #include "test_node.h"
27 : : #include "util/rational.h"
28 : :
29 : : #define K 30u
30 : : #define LARGE_K UINT_MAX / 40
31 : :
32 : : namespace cvc5::internal {
33 : :
34 : : namespace test {
35 : :
36 : : class TestNodeBlackNodeBuilder : public TestNode
37 : : {
38 : : protected:
39 : 10 : void push_back(NodeBuilder& nb, uint32_t n)
40 : : {
41 [ + + ]: 399 : for (uint32_t i = 0; i < n; ++i)
42 : : {
43 : 389 : nb << d_nodeManager->mkConst(true);
44 : : }
45 : 10 : }
46 : : Kind d_specKind = Kind::AND;
47 : : };
48 : :
49 : : /** Tests just constructors. No modification is done to the node. */
50 : 2 : TEST_F(TestNodeBlackNodeBuilder, ctors)
51 : : {
52 : : /* Default size tests. */
53 : 1 : NodeBuilder def;
54 [ - + ]: 1 : ASSERT_EQ(def.getKind(), Kind::UNDEFINED_KIND);
55 : : #ifdef CVC5_ASSERTIONS
56 : 1 : ASSERT_DEATH(def.getNumChildren(), "getKind\\(\\) != Kind::UNDEFINED_KIND");
57 : : #endif
58 : :
59 : 1 : NodeBuilder spec(d_specKind);
60 [ - + ]: 1 : ASSERT_EQ(spec.getKind(), d_specKind);
61 [ - + ]: 1 : ASSERT_EQ(spec.getNumChildren(), 0u);
62 : :
63 : 1 : NodeBuilder from_nm(d_nodeManager);
64 [ - + ]: 1 : ASSERT_EQ(from_nm.getKind(), Kind::UNDEFINED_KIND);
65 : : #ifdef CVC5_ASSERTIONS
66 : 1 : ASSERT_DEATH(from_nm.getNumChildren(),
67 : : "getKind\\(\\) != Kind::UNDEFINED_KIND");
68 : : #endif
69 : :
70 : 1 : NodeBuilder from_nm_kind(d_nodeManager, d_specKind);
71 [ - + ]: 1 : ASSERT_EQ(from_nm_kind.getKind(), d_specKind);
72 [ - + ]: 1 : ASSERT_EQ(from_nm_kind.getNumChildren(), 0u);
73 : :
74 : : /* Copy constructors */
75 : 1 : NodeBuilder copy(def);
76 [ - + ]: 1 : ASSERT_EQ(copy.getKind(), Kind::UNDEFINED_KIND);
77 : : #ifdef CVC5_ASSERTIONS
78 : 1 : ASSERT_DEATH(copy.getNumChildren(), "getKind\\(\\) != Kind::UNDEFINED_KIND");
79 : : #endif
80 : : }
81 : :
82 : 2 : TEST_F(TestNodeBlackNodeBuilder, dtor)
83 : : {
84 : 1 : std::unique_ptr<NodeBuilder> nb(new NodeBuilder());
85 : 1 : }
86 : :
87 : 2 : TEST_F(TestNodeBlackNodeBuilder, getKind)
88 : : {
89 : 1 : NodeBuilder noKind;
90 [ - + ]: 1 : ASSERT_EQ(noKind.getKind(), Kind::UNDEFINED_KIND);
91 : :
92 : 2 : Node x(d_skolemManager->mkDummySkolem("x", *d_intTypeNode));
93 : 1 : noKind << x << x;
94 [ - + ]: 1 : ASSERT_EQ(noKind.getKind(), Kind::UNDEFINED_KIND);
95 : :
96 : 1 : noKind << Kind::ADD;
97 [ - + ]: 1 : ASSERT_EQ(noKind.getKind(), Kind::ADD);
98 : :
99 : 1 : Node n = noKind;
100 : : #ifdef CVC5_ASSERTIONS
101 : 1 : ASSERT_DEATH(noKind.getKind(), "!isUsed\\(\\)");
102 : : #endif
103 : :
104 : 1 : NodeBuilder spec(Kind::ADD);
105 [ - + ]: 1 : ASSERT_EQ(spec.getKind(), Kind::ADD);
106 : 1 : spec << x << x;
107 [ - + ]: 1 : ASSERT_EQ(spec.getKind(), Kind::ADD);
108 : : }
109 : :
110 : 2 : TEST_F(TestNodeBlackNodeBuilder, getNumChildren)
111 : : {
112 : 2 : Node x(d_skolemManager->mkDummySkolem("x", *d_intTypeNode));
113 : :
114 : 1 : NodeBuilder nb;
115 : : #ifdef CVC5_ASSERTIONS
116 : 1 : ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != Kind::UNDEFINED_KIND");
117 : : #endif
118 : :
119 : 1 : nb << Kind::ADD << x << x;
120 [ - + ]: 1 : ASSERT_EQ(nb.getNumChildren(), 2u);
121 : :
122 : 1 : nb << x << x;
123 [ - + ]: 1 : ASSERT_EQ(nb.getNumChildren(), 4u);
124 : :
125 : 1 : nb.clear();
126 : : #ifdef CVC5_ASSERTIONS
127 : 1 : ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != Kind::UNDEFINED_KIND");
128 : : #endif
129 : :
130 : 1 : nb.clear(Kind::ADD);
131 [ - + ]: 1 : ASSERT_EQ(nb.getNumChildren(), 0u);
132 : :
133 : 1 : nb << x << x << x;
134 [ - + ]: 1 : ASSERT_EQ(nb.getNumChildren(), 3u);
135 : :
136 : 1 : nb << x << x << x;
137 [ - + ]: 1 : ASSERT_EQ(nb.getNumChildren(), 6u);
138 : :
139 : : #ifdef CVC5_ASSERTIONS
140 : 1 : ASSERT_DEATH(nb << Kind::ADD, "getKind\\(\\) == Kind::UNDEFINED_KIND");
141 : 1 : Node n = nb;
142 : 1 : ASSERT_DEATH(nb.getNumChildren(), "!isUsed\\(\\)");
143 : : #endif
144 : : }
145 : :
146 : 2 : TEST_F(TestNodeBlackNodeBuilder, operator_square)
147 : : {
148 : 1 : NodeBuilder arr(d_specKind);
149 : :
150 : 1 : Node i_0 = d_nodeManager->mkConst(false);
151 : 1 : Node i_2 = d_nodeManager->mkConst(true);
152 : 1 : Node i_K = d_nodeManager->mkNode(Kind::NOT, i_0);
153 : :
154 : : #ifdef CVC5_ASSERTIONS
155 : 1 : ASSERT_DEATH(arr[-1], "index out of range");
156 : 1 : ASSERT_DEATH(arr[0], "index out of range");
157 : : #endif
158 : :
159 : 1 : arr << i_0;
160 [ - + ]: 2 : ASSERT_EQ(arr[0], i_0);
161 : :
162 : 1 : push_back(arr, 1);
163 : 1 : arr << i_2;
164 [ - + ]: 2 : ASSERT_EQ(arr[0], i_0);
165 [ - + ]: 2 : ASSERT_EQ(arr[2], i_2);
166 : :
167 : 1 : push_back(arr, K - 3);
168 [ - + ]: 2 : ASSERT_EQ(arr[0], i_0);
169 [ - + ]: 2 : ASSERT_EQ(arr[2], i_2);
170 [ + + ]: 28 : for (unsigned i = 3; i < K; ++i)
171 : : {
172 [ - + ]: 54 : ASSERT_EQ(arr[i], d_nodeManager->mkConst(true));
173 : : }
174 : :
175 : 1 : arr << i_K;
176 [ - + ]: 2 : ASSERT_EQ(arr[0], i_0);
177 [ - + ]: 2 : ASSERT_EQ(arr[2], i_2);
178 [ + + ]: 28 : for (unsigned i = 3; i < K; ++i)
179 : : {
180 [ - + ]: 54 : ASSERT_EQ(arr[i], d_nodeManager->mkConst(true));
181 : : }
182 [ - + ]: 2 : ASSERT_EQ(arr[K], i_K);
183 : :
184 : : #ifdef CVC5_ASSERTIONS
185 : 1 : Node n = arr;
186 : 1 : ASSERT_DEATH(arr[0], "!isUsed\\(\\)");
187 : : #endif
188 : : }
189 : :
190 : 2 : TEST_F(TestNodeBlackNodeBuilder, clear)
191 : : {
192 : 1 : NodeBuilder nb;
193 [ - + ]: 1 : ASSERT_EQ(nb.getKind(), Kind::UNDEFINED_KIND);
194 : : #ifdef CVC5_ASSERTIONS
195 : 1 : ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != Kind::UNDEFINED_KIND");
196 : : #endif
197 : :
198 : 1 : nb << d_specKind;
199 : 1 : push_back(nb, K);
200 [ - + ]: 1 : ASSERT_EQ(nb.getKind(), d_specKind);
201 [ - + ]: 1 : ASSERT_EQ(nb.getNumChildren(), K);
202 : :
203 : 1 : nb.clear();
204 [ - + ]: 1 : ASSERT_EQ(nb.getKind(), Kind::UNDEFINED_KIND);
205 : : #ifdef CVC5_ASSERTIONS
206 : 1 : ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != Kind::UNDEFINED_KIND");
207 : : #endif
208 : :
209 : 1 : nb << d_specKind;
210 : 1 : push_back(nb, K);
211 [ - + ]: 1 : ASSERT_EQ(nb.getKind(), d_specKind);
212 [ - + ]: 1 : ASSERT_EQ(nb.getNumChildren(), K);
213 : :
214 : 1 : nb.clear(d_specKind);
215 [ - + ]: 1 : ASSERT_EQ(nb.getKind(), d_specKind);
216 [ - + ]: 1 : ASSERT_EQ(nb.getNumChildren(), 0u);
217 : :
218 : 1 : push_back(nb, K);
219 : 1 : nb.clear();
220 [ - + ]: 1 : ASSERT_EQ(nb.getKind(), Kind::UNDEFINED_KIND);
221 : : #ifdef CVC5_ASSERTIONS
222 : 1 : ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != Kind::UNDEFINED_KIND");
223 : : #endif
224 : : }
225 : :
226 : 2 : TEST_F(TestNodeBlackNodeBuilder, operator_stream_insertion_kind)
227 : : {
228 : : #ifdef CVC5_ASSERTIONS
229 : 1 : NodeBuilder spec(d_specKind);
230 : 1 : ASSERT_DEATH(spec << Kind::ADD, "can't redefine the Kind of a NodeBuilder");
231 : : #endif
232 : :
233 : 1 : NodeBuilder noSpec;
234 : 1 : noSpec << d_specKind;
235 [ - + ]: 1 : ASSERT_EQ(noSpec.getKind(), d_specKind);
236 : :
237 : 1 : NodeBuilder modified;
238 : 1 : push_back(modified, K);
239 : 1 : modified << d_specKind;
240 [ - + ]: 1 : ASSERT_EQ(modified.getKind(), d_specKind);
241 : :
242 : 1 : NodeBuilder nb(d_specKind);
243 : 1 : nb << d_nodeManager->mkConst(true) << d_nodeManager->mkConst(false);
244 : 1 : nb.clear(Kind::ADD);
245 : :
246 : : #ifdef CVC5_ASSERTIONS
247 : 1 : Node n;
248 : 1 : ASSERT_DEATH(n = nb, "Nodes with kind `\\+` must have at least 2 children");
249 : 1 : nb.clear(Kind::ADD);
250 : : #endif
251 : :
252 : : #ifdef CVC5_ASSERTIONS
253 : 1 : ASSERT_DEATH(nb << Kind::ADD, "can't redefine the Kind of a NodeBuilder");
254 : : #endif
255 : :
256 : 1 : NodeBuilder testRef;
257 [ - + ]: 1 : ASSERT_EQ((testRef << d_specKind).getKind(), d_specKind);
258 : :
259 : : #ifdef CVC5_ASSERTIONS
260 : 1 : NodeBuilder testTwo;
261 : 1 : ASSERT_DEATH(testTwo << d_specKind << Kind::ADD,
262 : : "can't redefine the Kind of a NodeBuilder");
263 : : #endif
264 : :
265 : 1 : NodeBuilder testMixOrder1;
266 [ - + ]: 1 : ASSERT_EQ(
267 : : (testMixOrder1 << d_specKind << d_nodeManager->mkConst(true)).getKind(),
268 : : d_specKind);
269 : 1 : NodeBuilder testMixOrder2;
270 [ - + ]: 1 : ASSERT_EQ(
271 : : (testMixOrder2 << d_nodeManager->mkConst(true) << d_specKind).getKind(),
272 : : d_specKind);
273 : : }
274 : :
275 : 2 : TEST_F(TestNodeBlackNodeBuilder, operator_stream_insertion_node)
276 : : {
277 : 1 : NodeBuilder nb(d_specKind);
278 [ - + ]: 1 : ASSERT_EQ(nb.getKind(), d_specKind);
279 [ - + ]: 1 : ASSERT_EQ(nb.getNumChildren(), 0u);
280 : 1 : push_back(nb, K);
281 [ - + ]: 1 : ASSERT_EQ(nb.getKind(), d_specKind);
282 [ - + ]: 1 : ASSERT_EQ(nb.getNumChildren(), K);
283 : :
284 : : #ifdef CVC5_ASSERTIONS
285 : 1 : Node n = nb;
286 : 1 : ASSERT_DEATH(nb << n, "!isUsed\\(\\)");
287 : : #endif
288 : :
289 : 1 : NodeBuilder overflow(d_specKind);
290 [ - + ]: 1 : ASSERT_EQ(overflow.getKind(), d_specKind);
291 [ - + ]: 1 : ASSERT_EQ(overflow.getNumChildren(), 0u);
292 : :
293 : 1 : push_back(overflow, 5 * K + 1);
294 [ - + ]: 1 : ASSERT_EQ(overflow.getKind(), d_specKind);
295 [ - + ]: 1 : ASSERT_EQ(overflow.getNumChildren(), 5 * K + 1);
296 : : }
297 : :
298 : 2 : TEST_F(TestNodeBlackNodeBuilder, append)
299 : : {
300 : 2 : Node x = d_skolemManager->mkDummySkolem("x", *d_boolTypeNode);
301 : 2 : Node y = d_skolemManager->mkDummySkolem("y", *d_boolTypeNode);
302 : 2 : Node z = d_skolemManager->mkDummySkolem("z", *d_boolTypeNode);
303 : 2 : Node m = d_nodeManager->mkNode(Kind::AND, y, z, x);
304 : 1 : Node n = d_nodeManager->mkNode(
305 : 2 : Kind::OR, d_nodeManager->mkNode(Kind::NOT, x), y, z);
306 : 2 : Node o = d_nodeManager->mkNode(Kind::XOR, y, x);
307 : :
308 : 2 : Node r = d_skolemManager->mkDummySkolem("r", *d_realTypeNode);
309 : 2 : Node s = d_skolemManager->mkDummySkolem("s", *d_realTypeNode);
310 : 2 : Node t = d_skolemManager->mkDummySkolem("t", *d_realTypeNode);
311 : :
312 : 1 : Node p = d_nodeManager->mkNode(
313 : : Kind::EQUAL,
314 : 2 : d_nodeManager->mkConst<Rational>(Kind::CONST_RATIONAL, 0),
315 : 3 : d_nodeManager->mkNode(
316 : 6 : Kind::ADD, r, d_nodeManager->mkNode(Kind::NEG, s), t));
317 : 1 : Node q = d_nodeManager->mkNode(
318 : 2 : Kind::AND, x, z, d_nodeManager->mkNode(Kind::NOT, y));
319 : :
320 : : #ifdef CVC5_ASSERTIONS
321 : 1 : ASSERT_DEATH(d_nodeManager->mkNode(Kind::XOR, y, x, x),
322 : : "Nodes with kind `xor` must have at most 2 children");
323 : : #endif
324 : :
325 : 1 : NodeBuilder b(d_specKind);
326 : :
327 : : /* test append(TNode) */
328 : 1 : b.append(n).append(o).append(q);
329 : :
330 [ - + ]: 1 : ASSERT_EQ(b.getNumChildren(), 3);
331 [ - + ]: 2 : ASSERT_EQ(b[0], n);
332 [ - + ]: 2 : ASSERT_EQ(b[1], o);
333 [ - + ]: 2 : ASSERT_EQ(b[2], q);
334 : :
335 : 1 : std::vector<Node> v;
336 : 1 : v.push_back(m);
337 : 1 : v.push_back(p);
338 : 1 : v.push_back(q);
339 : :
340 : : /* test append(vector<Node>) */
341 : 1 : b.append(v);
342 : :
343 [ - + ]: 1 : ASSERT_EQ(b.getNumChildren(), 6);
344 [ - + ]: 2 : ASSERT_EQ(b[0], n);
345 [ - + ]: 2 : ASSERT_EQ(b[1], o);
346 [ - + ]: 2 : ASSERT_EQ(b[2], q);
347 [ - + ]: 2 : ASSERT_EQ(b[3], m);
348 [ - + ]: 2 : ASSERT_EQ(b[4], p);
349 [ - + ]: 2 : ASSERT_EQ(b[5], q);
350 : :
351 : : /* test append(iterator, iterator) */
352 : 1 : b.append(v.rbegin(), v.rend());
353 : :
354 [ - + ]: 1 : ASSERT_EQ(b.getNumChildren(), 9);
355 [ - + ]: 2 : ASSERT_EQ(b[0], n);
356 [ - + ]: 2 : ASSERT_EQ(b[1], o);
357 [ - + ]: 2 : ASSERT_EQ(b[2], q);
358 [ - + ]: 2 : ASSERT_EQ(b[3], m);
359 [ - + ]: 2 : ASSERT_EQ(b[4], p);
360 [ - + ]: 2 : ASSERT_EQ(b[5], q);
361 [ - + ]: 2 : ASSERT_EQ(b[6], q);
362 [ - + ]: 2 : ASSERT_EQ(b[7], p);
363 [ - + ]: 2 : ASSERT_EQ(b[8], m);
364 : : }
365 : :
366 : 2 : TEST_F(TestNodeBlackNodeBuilder, operator_node_cast)
367 : : {
368 : 1 : NodeBuilder implicit(d_specKind);
369 : 1 : NodeBuilder explic(d_specKind);
370 : :
371 : 1 : push_back(implicit, K);
372 : 1 : push_back(explic, K);
373 : :
374 : 1 : Node nimpl = implicit;
375 : 1 : Node nexplicit = (Node)explic;
376 : :
377 [ - + ]: 1 : ASSERT_EQ(nimpl.getKind(), d_specKind);
378 [ - + ]: 1 : ASSERT_EQ(nimpl.getNumChildren(), K);
379 : :
380 [ - + ]: 1 : ASSERT_EQ(nexplicit.getKind(), d_specKind);
381 [ - + ]: 1 : ASSERT_EQ(nexplicit.getNumChildren(), K);
382 : :
383 : : #ifdef CVC5_ASSERTIONS
384 : 1 : ASSERT_DEATH(Node blah = implicit, "!isUsed\\(\\)");
385 : : #endif
386 : : }
387 : :
388 : 2 : TEST_F(TestNodeBlackNodeBuilder, leftist_building)
389 : : {
390 : 1 : NodeBuilder nb;
391 : :
392 : 2 : Node a = d_skolemManager->mkDummySkolem("a", *d_boolTypeNode);
393 : :
394 : 2 : Node b = d_skolemManager->mkDummySkolem("b", *d_boolTypeNode);
395 : 2 : Node c = d_skolemManager->mkDummySkolem("c", *d_boolTypeNode);
396 : :
397 : 2 : Node d = d_skolemManager->mkDummySkolem("d", *d_realTypeNode);
398 : 2 : Node e = d_skolemManager->mkDummySkolem("e", *d_realTypeNode);
399 : :
400 : 2 : nb << a << Kind::NOT << b << c << Kind::OR << c << a << Kind::AND << d << e
401 : 1 : << Kind::ITE;
402 : :
403 : 1 : Node n = nb;
404 [ - + ]: 1 : ASSERT_EQ(n.getNumChildren(), 3u);
405 [ - + ]: 2 : ASSERT_EQ(n.getType(), *d_realTypeNode);
406 [ - + ]: 2 : ASSERT_EQ(n[0].getType(), *d_boolTypeNode);
407 [ - + ]: 2 : ASSERT_EQ(n[1].getType(), *d_realTypeNode);
408 [ - + ]: 2 : ASSERT_EQ(n[2].getType(), *d_realTypeNode);
409 : :
410 : 1 : Node nota = d_nodeManager->mkNode(Kind::NOT, a);
411 : 2 : Node nota_or_b_or_c = d_nodeManager->mkNode(Kind::OR, nota, b, c);
412 : 2 : Node n0 = d_nodeManager->mkNode(Kind::AND, nota_or_b_or_c, c, a);
413 : 2 : Node nexpected = d_nodeManager->mkNode(Kind::ITE, n0, d, e);
414 : :
415 [ - + ]: 1 : ASSERT_EQ(nexpected, n);
416 : : }
417 : : } // namespace test
418 : : } // namespace cvc5::internal
|
