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::NodeManager.
11 : : */
12 : :
13 : : #include <string>
14 : : #include <vector>
15 : :
16 : : #include "base/output.h"
17 : : #include "expr/node_manager.h"
18 : : #include "expr/node_manager_attributes.h"
19 : : #include "test_node.h"
20 : : #include "util/integer.h"
21 : : #include "util/rational.h"
22 : :
23 : : namespace cvc5::internal {
24 : :
25 : : using namespace expr;
26 : :
27 : : namespace test {
28 : :
29 : : class TestNodeBlackNodeManager : public TestNode
30 : : {
31 : : };
32 : :
33 : 4 : TEST_F(TestNodeBlackNodeManager, mkNode_not)
34 : : {
35 : 2 : Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType());
36 : 1 : Node n = d_nodeManager->mkNode(Kind::NOT, x);
37 [ - + ][ + - ]: 1 : ASSERT_EQ(n.getNumChildren(), 1u);
38 [ - + ][ + - ]: 1 : ASSERT_EQ(n.getKind(), Kind::NOT);
39 [ - + ][ + - ]: 2 : ASSERT_EQ(n[0], x);
40 [ + - ][ + - ]: 1 : }
41 : :
42 : 4 : TEST_F(TestNodeBlackNodeManager, mkNode_binary)
43 : : {
44 : 2 : Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType());
45 : 2 : Node y = d_skolemManager->mkDummySkolem("y", d_nodeManager->booleanType());
46 : 2 : Node n = d_nodeManager->mkNode(Kind::IMPLIES, x, y);
47 [ - + ][ + - ]: 1 : ASSERT_EQ(n.getNumChildren(), 2u);
48 [ - + ][ + - ]: 1 : ASSERT_EQ(n.getKind(), Kind::IMPLIES);
49 [ - + ][ + - ]: 2 : ASSERT_EQ(n[0], x);
50 [ - + ][ + - ]: 2 : ASSERT_EQ(n[1], y);
51 [ + - ][ + - ]: 1 : }
[ + - ]
52 : :
53 : 4 : TEST_F(TestNodeBlackNodeManager, mkNode_three_children)
54 : : {
55 : 2 : Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType());
56 : 2 : Node y = d_skolemManager->mkDummySkolem("y", d_nodeManager->booleanType());
57 : 2 : Node z = d_skolemManager->mkDummySkolem("z", d_nodeManager->booleanType());
58 : 2 : Node n = d_nodeManager->mkNode(Kind::AND, x, y, z);
59 [ - + ][ + - ]: 1 : ASSERT_EQ(n.getNumChildren(), 3u);
60 [ - + ][ + - ]: 1 : ASSERT_EQ(n.getKind(), Kind::AND);
61 [ - + ][ + - ]: 2 : ASSERT_EQ(n[0], x);
62 [ - + ][ + - ]: 2 : ASSERT_EQ(n[1], y);
63 [ - + ][ + - ]: 2 : ASSERT_EQ(n[2], z);
64 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
65 : :
66 : 4 : TEST_F(TestNodeBlackNodeManager, mkNode_init_list)
67 : : {
68 : 2 : Node x1 = d_skolemManager->mkDummySkolem("x1", d_nodeManager->booleanType());
69 : 2 : Node x2 = d_skolemManager->mkDummySkolem("x2", d_nodeManager->booleanType());
70 : 2 : Node x3 = d_skolemManager->mkDummySkolem("x3", d_nodeManager->booleanType());
71 : 2 : Node x4 = d_skolemManager->mkDummySkolem("x4", d_nodeManager->booleanType());
72 : : // Negate second argument to test the use of temporary nodes
73 : 6 : Node n = d_nodeManager->mkNode(Kind::AND, {x1, x2.negate(), x3, x4});
74 [ - + ][ + - ]: 1 : ASSERT_EQ(n.getNumChildren(), 4u);
75 [ - + ][ + - ]: 1 : ASSERT_EQ(n.getKind(), Kind::AND);
76 [ - + ][ + - ]: 2 : ASSERT_EQ(n[0], x1);
77 [ - + ][ + - ]: 2 : ASSERT_EQ(n[1], x2.negate());
78 [ - + ][ + - ]: 2 : ASSERT_EQ(n[2], x3);
79 [ - + ][ + - ]: 2 : ASSERT_EQ(n[3], x4);
80 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ]
81 : :
82 : 4 : TEST_F(TestNodeBlackNodeManager, mkNode_vector_of_node)
83 : : {
84 : 2 : Node x1 = d_skolemManager->mkDummySkolem("x1", d_nodeManager->booleanType());
85 : 2 : Node x2 = d_skolemManager->mkDummySkolem("x2", d_nodeManager->booleanType());
86 : 2 : Node x3 = d_skolemManager->mkDummySkolem("x3", d_nodeManager->booleanType());
87 : 1 : std::vector<Node> args;
88 : 1 : args.push_back(x1);
89 : 1 : args.push_back(x2);
90 : 1 : args.push_back(x3);
91 : 1 : Node n = d_nodeManager->mkNode(Kind::AND, args);
92 [ - + ][ + - ]: 1 : ASSERT_EQ(n.getNumChildren(), args.size());
93 [ - + ][ + - ]: 1 : ASSERT_EQ(n.getKind(), Kind::AND);
94 [ + + ]: 4 : for (unsigned i = 0; i < args.size(); ++i)
95 : : {
96 [ - + ][ + - ]: 6 : ASSERT_EQ(n[i], args[i]);
97 : : }
98 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ]
99 : :
100 : 4 : TEST_F(TestNodeBlackNodeManager, mkNode_vector_of_tnode)
101 : : {
102 : 2 : Node x1 = d_skolemManager->mkDummySkolem("x1", d_nodeManager->booleanType());
103 : 2 : Node x2 = d_skolemManager->mkDummySkolem("x2", d_nodeManager->booleanType());
104 : 2 : Node x3 = d_skolemManager->mkDummySkolem("x3", d_nodeManager->booleanType());
105 : 1 : std::vector<TNode> args;
106 : 1 : args.push_back(x1);
107 : 1 : args.push_back(x2);
108 : 1 : args.push_back(x3);
109 : 1 : Node n = d_nodeManager->mkNode(Kind::AND, args);
110 [ - + ][ + - ]: 1 : ASSERT_EQ(n.getNumChildren(), args.size());
111 [ - + ][ + - ]: 1 : ASSERT_EQ(n.getKind(), Kind::AND);
112 [ + + ]: 4 : for (unsigned i = 0; i < args.size(); ++i)
113 : : {
114 [ - + ][ + - ]: 6 : ASSERT_EQ(n[i], args[i]);
115 : : }
116 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ]
117 : :
118 : 4 : TEST_F(TestNodeBlackNodeManager, mkSkolem_with_name)
119 : : {
120 : 1 : Node x = d_skolemManager->mkDummySkolem(
121 : 2 : "x", *d_boolTypeNode, SkolemFlags::SKOLEM_EXACT_NAME);
122 [ - + ][ + - ]: 1 : ASSERT_EQ(x.getKind(), Kind::DUMMY_SKOLEM);
123 [ - + ][ + - ]: 1 : ASSERT_EQ(x.getNumChildren(), 0u);
124 [ - + ][ + - ]: 2 : ASSERT_EQ(x.getAttribute(VarNameAttr()), "x");
125 [ - + ][ + - ]: 2 : ASSERT_EQ(x.getType(), *d_boolTypeNode);
126 [ + - ]: 1 : }
127 : :
128 : 4 : TEST_F(TestNodeBlackNodeManager, mkConst_bool)
129 : : {
130 : 1 : Node tt = d_nodeManager->mkConst(true);
131 [ - + ][ + - ]: 1 : ASSERT_EQ(tt.getConst<bool>(), true);
132 : 1 : Node ff = d_nodeManager->mkConst(false);
133 [ - + ][ + - ]: 1 : ASSERT_EQ(ff.getConst<bool>(), false);
134 [ + - ]: 1 : }
135 : :
136 : 4 : TEST_F(TestNodeBlackNodeManager, mkConst_rational)
137 : : {
138 : 1 : Rational r("3/2");
139 : 1 : Node n = d_nodeManager->mkConstReal(r);
140 [ - + ][ + - ]: 1 : ASSERT_EQ(n.getConst<Rational>(), r);
141 [ + - ][ + - ]: 1 : }
142 : :
143 : 4 : TEST_F(TestNodeBlackNodeManager, hasOperator)
144 : : {
145 [ - + ][ + - ]: 1 : ASSERT_TRUE(NodeManager::hasOperator(Kind::AND));
146 [ - + ][ + - ]: 1 : ASSERT_TRUE(NodeManager::hasOperator(Kind::OR));
147 [ - + ][ + - ]: 1 : ASSERT_TRUE(NodeManager::hasOperator(Kind::NOT));
148 [ - + ][ + - ]: 1 : ASSERT_TRUE(NodeManager::hasOperator(Kind::APPLY_UF));
149 [ - + ][ + - ]: 1 : ASSERT_TRUE(!NodeManager::hasOperator(Kind::VARIABLE));
150 : : }
151 : :
152 : 4 : TEST_F(TestNodeBlackNodeManager, booleanType)
153 : : {
154 : 1 : TypeNode t = d_nodeManager->booleanType();
155 : 1 : TypeNode t2 = d_nodeManager->booleanType();
156 : 2 : TypeNode t3 = d_nodeManager->mkSort("T");
157 [ - + ][ + - ]: 1 : ASSERT_TRUE(t.isBoolean());
158 [ - + ][ + - ]: 1 : ASSERT_FALSE(t.isFunction());
159 [ - + ][ + - ]: 1 : ASSERT_FALSE(t.isNull());
160 [ - + ][ + - ]: 1 : ASSERT_FALSE(t.isPredicate());
161 [ - + ][ + - ]: 1 : ASSERT_FALSE(t.isUninterpretedSort());
162 [ - + ][ + - ]: 1 : ASSERT_EQ(t, t2);
163 [ - + ][ + - ]: 1 : ASSERT_NE(t, t3);
164 : :
165 : 1 : TypeNode bt = t;
166 [ - + ][ + - ]: 1 : ASSERT_EQ(bt, t);
167 [ + - ][ + - ]: 1 : }
[ + - ]
168 : :
169 : 4 : TEST_F(TestNodeBlackNodeManager, mkFunctionType_bool_to_bool)
170 : : {
171 : 1 : TypeNode booleanType = d_nodeManager->booleanType();
172 : 1 : TypeNode t = d_nodeManager->mkFunctionType(booleanType, booleanType);
173 : 1 : TypeNode t2 = d_nodeManager->mkFunctionType(booleanType, booleanType);
174 : :
175 [ - + ][ + - ]: 1 : ASSERT_FALSE(t.isBoolean());
176 [ - + ][ + - ]: 1 : ASSERT_TRUE(t.isFunction());
177 [ - + ][ + - ]: 1 : ASSERT_FALSE(t.isNull());
178 [ - + ][ + - ]: 1 : ASSERT_TRUE(t.isPredicate());
179 [ - + ][ + - ]: 1 : ASSERT_FALSE(t.isUninterpretedSort());
180 : :
181 [ - + ][ + - ]: 1 : ASSERT_EQ(t, t2);
182 : :
183 : 1 : TypeNode ft = t;
184 [ - + ][ + - ]: 1 : ASSERT_EQ(ft, t);
185 [ - + ][ + - ]: 1 : ASSERT_EQ(ft.getArgTypes().size(), 1u);
186 [ - + ][ + - ]: 2 : ASSERT_EQ(ft.getArgTypes()[0], booleanType);
187 [ - + ][ + - ]: 2 : ASSERT_EQ(ft.getRangeType(), booleanType);
188 [ + - ][ + - ]: 1 : }
[ + - ]
189 : :
190 : 4 : TEST_F(TestNodeBlackNodeManager, mkFunctionType_vector_args_with_return_type)
191 : : {
192 : 1 : TypeNode a = d_nodeManager->mkSort();
193 : 1 : TypeNode b = d_nodeManager->mkSort();
194 : 1 : TypeNode c = d_nodeManager->mkSort();
195 : :
196 : 1 : std::vector<TypeNode> argTypes;
197 : 1 : argTypes.push_back(a);
198 : 1 : argTypes.push_back(b);
199 : :
200 : 1 : TypeNode t = d_nodeManager->mkFunctionType(argTypes, c);
201 : 1 : TypeNode t2 = d_nodeManager->mkFunctionType(argTypes, c);
202 : :
203 [ - + ][ + - ]: 1 : ASSERT_FALSE(t.isBoolean());
204 [ - + ][ + - ]: 1 : ASSERT_TRUE(t.isFunction());
205 [ - + ][ + - ]: 1 : ASSERT_FALSE(t.isNull());
206 [ - + ][ + - ]: 1 : ASSERT_FALSE(t.isPredicate());
207 [ - + ][ + - ]: 1 : ASSERT_FALSE(t.isUninterpretedSort());
208 : :
209 [ - + ][ + - ]: 1 : ASSERT_EQ(t, t2);
210 : :
211 : 1 : TypeNode ft = t;
212 [ - + ][ + - ]: 1 : ASSERT_EQ(ft, t);
213 [ - + ][ + - ]: 1 : ASSERT_EQ(ft.getArgTypes().size(), argTypes.size());
214 [ - + ][ + - ]: 2 : ASSERT_EQ(ft.getArgTypes()[0], a);
215 [ - + ][ + - ]: 2 : ASSERT_EQ(ft.getArgTypes()[1], b);
216 [ - + ][ + - ]: 2 : ASSERT_EQ(ft.getRangeType(), c);
217 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
218 : :
219 : 4 : TEST_F(TestNodeBlackNodeManager, mkFunctionType_vector_of_arguments)
220 : : {
221 : 1 : TypeNode a = d_nodeManager->mkSort();
222 : 1 : TypeNode b = d_nodeManager->mkSort();
223 : 1 : TypeNode c = d_nodeManager->mkSort();
224 : :
225 : 1 : std::vector<TypeNode> types;
226 : 1 : types.push_back(a);
227 : 1 : types.push_back(b);
228 : 1 : types.push_back(c);
229 : :
230 : 1 : TypeNode t = d_nodeManager->mkFunctionType(types);
231 : 1 : TypeNode t2 = d_nodeManager->mkFunctionType(types);
232 : :
233 [ - + ][ + - ]: 1 : ASSERT_FALSE(t.isBoolean());
234 [ - + ][ + - ]: 1 : ASSERT_TRUE(t.isFunction());
235 [ - + ][ + - ]: 1 : ASSERT_FALSE(t.isNull());
236 [ - + ][ + - ]: 1 : ASSERT_FALSE(t.isPredicate());
237 [ - + ][ + - ]: 1 : ASSERT_FALSE(t.isUninterpretedSort());
238 : :
239 [ - + ][ + - ]: 1 : ASSERT_EQ(t, t2);
240 : :
241 : 1 : TypeNode ft = t;
242 [ - + ][ + - ]: 1 : ASSERT_EQ(ft, t);
243 [ - + ][ + - ]: 1 : ASSERT_EQ(ft.getArgTypes().size(), types.size() - 1);
244 [ - + ][ + - ]: 2 : ASSERT_EQ(ft.getArgTypes()[0], a);
245 [ - + ][ + - ]: 2 : ASSERT_EQ(ft.getArgTypes()[1], b);
246 [ - + ][ + - ]: 2 : ASSERT_EQ(ft.getRangeType(), c);
247 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
248 : :
249 : 4 : TEST_F(TestNodeBlackNodeManager, mkPredicateType)
250 : : {
251 : 2 : TypeNode a = d_nodeManager->mkSort("a");
252 : 2 : TypeNode b = d_nodeManager->mkSort("b");
253 : 2 : TypeNode c = d_nodeManager->mkSort("c");
254 : 1 : TypeNode booleanType = d_nodeManager->booleanType();
255 : :
256 : 1 : std::vector<TypeNode> argTypes;
257 : 1 : argTypes.push_back(a);
258 : 1 : argTypes.push_back(b);
259 : 1 : argTypes.push_back(c);
260 : :
261 : 1 : TypeNode t = d_nodeManager->mkPredicateType(argTypes);
262 : 1 : TypeNode t2 = d_nodeManager->mkPredicateType(argTypes);
263 : :
264 [ - + ][ + - ]: 1 : ASSERT_FALSE(t.isBoolean());
265 [ - + ][ + - ]: 1 : ASSERT_TRUE(t.isFunction());
266 [ - + ][ + - ]: 1 : ASSERT_FALSE(t.isNull());
267 [ - + ][ + - ]: 1 : ASSERT_TRUE(t.isPredicate());
268 [ - + ][ + - ]: 1 : ASSERT_FALSE(t.isUninterpretedSort());
269 : :
270 [ - + ][ + - ]: 1 : ASSERT_EQ(t, t2);
271 : :
272 : 1 : TypeNode ft = t;
273 [ - + ][ + - ]: 1 : ASSERT_EQ(ft, t);
274 [ - + ][ + - ]: 1 : ASSERT_EQ(ft.getArgTypes().size(), argTypes.size());
275 [ - + ][ + - ]: 2 : ASSERT_EQ(ft.getArgTypes()[0], a);
276 [ - + ][ + - ]: 2 : ASSERT_EQ(ft.getArgTypes()[1], b);
277 [ - + ][ + - ]: 2 : ASSERT_EQ(ft.getArgTypes()[2], c);
278 [ - + ][ + - ]: 2 : ASSERT_EQ(ft.getRangeType(), booleanType);
279 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ]
280 : :
281 : : /* This test is only valid if assertions are enabled. */
282 : 4 : TEST_F(TestNodeBlackNodeManager, mkNode_too_few_children)
283 : : {
284 : : #ifdef CVC5_ASSERTIONS
285 : 2 : Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType());
286 : 1 : ASSERT_DEATH(d_nodeManager->mkNode(Kind::AND, x),
287 : : "Nodes with kind `and` must have at least 2 children");
288 : : #endif
289 [ + - ]: 1 : }
290 : :
291 : : /* This test is only valid if assertions are enabled. */
292 : 4 : TEST_F(TestNodeBlackNodeManager, mkNode_too_many_children)
293 : : {
294 : : #ifdef CVC5_ASSERTIONS
295 : 1 : std::vector<Node> vars;
296 : 1 : const uint32_t max = kind::metakind::getMaxArityForKind(Kind::AND);
297 : 1 : TypeNode boolType = d_nodeManager->booleanType();
298 : 2 : Node skolem_i = d_skolemManager->mkDummySkolem("i", boolType);
299 : 2 : Node skolem_j = d_skolemManager->mkDummySkolem("j", boolType);
300 : 1 : Node andNode = skolem_i.andNode(skolem_j);
301 : 1 : Node orNode = skolem_i.orNode(skolem_j);
302 [ + + ]: 22369623 : while (vars.size() <= max)
303 : : {
304 : 22369622 : vars.push_back(andNode);
305 : 22369622 : vars.push_back(skolem_j);
306 : 22369622 : vars.push_back(orNode);
307 : : }
308 : 1 : ASSERT_DEATH(d_nodeManager->mkNode(Kind::AND, vars),
309 : : "toSize > d_nvMaxChildren");
310 : : #endif
311 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ][ + - ]
312 : : } // namespace test
313 : : } // namespace cvc5::internal
|
