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