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