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 |
|
* White box testing of cvc5::theory::TypeEnumerator. |
14 |
|
* |
15 |
|
* These tests depend on the ordering that the TypeEnumerators use, so it's a |
16 |
|
* white-box test. |
17 |
|
*/ |
18 |
|
|
19 |
|
#include <unordered_set> |
20 |
|
|
21 |
|
#include "expr/array_store_all.h" |
22 |
|
#include "expr/dtype.h" |
23 |
|
#include "expr/kind.h" |
24 |
|
#include "expr/type_node.h" |
25 |
|
#include "options/language.h" |
26 |
|
#include "test_smt.h" |
27 |
|
#include "theory/type_enumerator.h" |
28 |
|
|
29 |
|
namespace cvc5 { |
30 |
|
|
31 |
|
using namespace theory; |
32 |
|
using namespace kind; |
33 |
|
|
34 |
|
namespace test { |
35 |
|
|
36 |
28 |
class TestTheoryWhiteTypeEnumerator : public TestSmt |
37 |
|
{ |
38 |
|
}; |
39 |
|
|
40 |
16 |
TEST_F(TestTheoryWhiteTypeEnumerator, booleans) |
41 |
|
{ |
42 |
4 |
TypeEnumerator te(d_nodeManager->booleanType()); |
43 |
2 |
ASSERT_FALSE(te.isFinished()); |
44 |
2 |
ASSERT_EQ(*te, d_nodeManager->mkConst(false)); |
45 |
2 |
ASSERT_FALSE(te.isFinished()); |
46 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(true)); |
47 |
2 |
ASSERT_FALSE(te.isFinished()); |
48 |
4 |
ASSERT_THROW(*++te, NoMoreValuesException); |
49 |
2 |
ASSERT_TRUE(te.isFinished()); |
50 |
4 |
ASSERT_THROW(*++te, NoMoreValuesException); |
51 |
2 |
ASSERT_TRUE(te.isFinished()); |
52 |
4 |
ASSERT_THROW(*++te, NoMoreValuesException); |
53 |
2 |
ASSERT_TRUE(te.isFinished()); |
54 |
|
} |
55 |
|
|
56 |
16 |
TEST_F(TestTheoryWhiteTypeEnumerator, uf) |
57 |
|
{ |
58 |
4 |
TypeNode sort = d_nodeManager->mkSort("T"); |
59 |
4 |
TypeNode sort2 = d_nodeManager->mkSort("U"); |
60 |
4 |
TypeEnumerator te(sort); |
61 |
2 |
ASSERT_EQ(*te, d_nodeManager->mkConst(UninterpretedConstant(sort, 0))); |
62 |
200 |
for (size_t i = 1; i < 100; ++i) |
63 |
|
{ |
64 |
198 |
ASSERT_NE(*te, d_nodeManager->mkConst(UninterpretedConstant(sort, i))); |
65 |
198 |
ASSERT_NE(*te, d_nodeManager->mkConst(UninterpretedConstant(sort2, i))); |
66 |
198 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(UninterpretedConstant(sort, i))); |
67 |
198 |
ASSERT_NE(*te, d_nodeManager->mkConst(UninterpretedConstant(sort, i + 2))); |
68 |
|
} |
69 |
|
} |
70 |
|
|
71 |
16 |
TEST_F(TestTheoryWhiteTypeEnumerator, arith) |
72 |
|
{ |
73 |
4 |
TypeEnumerator te(d_nodeManager->integerType()); |
74 |
2 |
ASSERT_FALSE(te.isFinished()); |
75 |
2 |
ASSERT_EQ(*te, d_nodeManager->mkConst(Rational(0))); |
76 |
202 |
for (int i = 1; i <= 100; ++i) |
77 |
|
{ |
78 |
200 |
ASSERT_FALSE(te.isFinished()); |
79 |
200 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(i))); |
80 |
200 |
ASSERT_FALSE(te.isFinished()); |
81 |
200 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-i))); |
82 |
|
} |
83 |
2 |
ASSERT_FALSE(te.isFinished()); |
84 |
|
|
85 |
2 |
te = TypeEnumerator(d_nodeManager->realType()); |
86 |
2 |
ASSERT_FALSE(te.isFinished()); |
87 |
2 |
ASSERT_EQ(*te, d_nodeManager->mkConst(Rational(0, 1))); |
88 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(1, 1))); |
89 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-1, 1))); |
90 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(2, 1))); |
91 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-2, 1))); |
92 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(1, 2))); |
93 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-1, 2))); |
94 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(3, 1))); |
95 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-3, 1))); |
96 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(1, 3))); |
97 |
2 |
ASSERT_FALSE(te.isFinished()); |
98 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-1, 3))); |
99 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(4, 1))); |
100 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-4, 1))); |
101 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(3, 2))); |
102 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-3, 2))); |
103 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(2, 3))); |
104 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-2, 3))); |
105 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(1, 4))); |
106 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-1, 4))); |
107 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(5, 1))); |
108 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-5, 1))); |
109 |
2 |
ASSERT_FALSE(te.isFinished()); |
110 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(1, 5))); |
111 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-1, 5))); |
112 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(6, 1))); |
113 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-6, 1))); |
114 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(5, 2))); |
115 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-5, 2))); |
116 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(4, 3))); |
117 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-4, 3))); |
118 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(3, 4))); |
119 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-3, 4))); |
120 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(2, 5))); |
121 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-2, 5))); |
122 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(1, 6))); |
123 |
2 |
ASSERT_FALSE(te.isFinished()); |
124 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-1, 6))); |
125 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(7, 1))); |
126 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-7, 1))); |
127 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(5, 3))); |
128 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-5, 3))); |
129 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(3, 5))); |
130 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-3, 5))); |
131 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(1, 7))); |
132 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-1, 7))); |
133 |
2 |
ASSERT_FALSE(te.isFinished()); |
134 |
|
} |
135 |
|
|
136 |
16 |
TEST_F(TestTheoryWhiteTypeEnumerator, dtypes_finite) |
137 |
|
{ |
138 |
4 |
DType dt("Colors"); |
139 |
2 |
dt.addConstructor(std::make_shared<DTypeConstructor>("red")); |
140 |
2 |
dt.addConstructor(std::make_shared<DTypeConstructor>("orange")); |
141 |
2 |
dt.addConstructor(std::make_shared<DTypeConstructor>("yellow")); |
142 |
2 |
dt.addConstructor(std::make_shared<DTypeConstructor>("green")); |
143 |
2 |
dt.addConstructor(std::make_shared<DTypeConstructor>("blue")); |
144 |
2 |
dt.addConstructor(std::make_shared<DTypeConstructor>("violet")); |
145 |
4 |
TypeNode datatype = d_nodeManager->mkDatatypeType(dt); |
146 |
|
const std::vector<std::shared_ptr<DTypeConstructor> >& dtcons = |
147 |
2 |
datatype.getDType().getConstructors(); |
148 |
4 |
TypeEnumerator te(datatype); |
149 |
2 |
ASSERT_EQ( |
150 |
|
*te, |
151 |
2 |
d_nodeManager->mkNode(APPLY_CONSTRUCTOR, dtcons[0]->getConstructor())); |
152 |
2 |
ASSERT_EQ( |
153 |
|
*++te, |
154 |
2 |
d_nodeManager->mkNode(APPLY_CONSTRUCTOR, dtcons[1]->getConstructor())); |
155 |
2 |
ASSERT_EQ( |
156 |
|
*++te, |
157 |
2 |
d_nodeManager->mkNode(APPLY_CONSTRUCTOR, dtcons[2]->getConstructor())); |
158 |
2 |
ASSERT_EQ( |
159 |
|
*++te, |
160 |
2 |
d_nodeManager->mkNode(APPLY_CONSTRUCTOR, dtcons[3]->getConstructor())); |
161 |
2 |
ASSERT_EQ( |
162 |
|
*++te, |
163 |
2 |
d_nodeManager->mkNode(APPLY_CONSTRUCTOR, dtcons[4]->getConstructor())); |
164 |
2 |
ASSERT_EQ( |
165 |
|
*++te, |
166 |
2 |
d_nodeManager->mkNode(APPLY_CONSTRUCTOR, dtcons[5]->getConstructor())); |
167 |
4 |
ASSERT_THROW(*++te, NoMoreValuesException); |
168 |
4 |
ASSERT_THROW(*++te, NoMoreValuesException); |
169 |
4 |
ASSERT_THROW(*++te, NoMoreValuesException); |
170 |
|
} |
171 |
|
|
172 |
16 |
TEST_F(TestTheoryWhiteTypeEnumerator, dtypes_infinite) |
173 |
|
{ |
174 |
4 |
DType colors("Colors"); |
175 |
2 |
colors.addConstructor(std::make_shared<DTypeConstructor>("red")); |
176 |
2 |
colors.addConstructor(std::make_shared<DTypeConstructor>("orange")); |
177 |
2 |
colors.addConstructor(std::make_shared<DTypeConstructor>("yellow")); |
178 |
2 |
colors.addConstructor(std::make_shared<DTypeConstructor>("green")); |
179 |
2 |
colors.addConstructor(std::make_shared<DTypeConstructor>("blue")); |
180 |
2 |
colors.addConstructor(std::make_shared<DTypeConstructor>("violet")); |
181 |
4 |
TypeNode colorsType = d_nodeManager->mkDatatypeType(colors); |
182 |
|
const std::vector<std::shared_ptr<DTypeConstructor> >& ctCons = |
183 |
2 |
colorsType.getDType().getConstructors(); |
184 |
4 |
DType listColors("ListColors"); |
185 |
|
std::shared_ptr<DTypeConstructor> consC = |
186 |
4 |
std::make_shared<DTypeConstructor>("cons"); |
187 |
2 |
consC->addArg("car", colorsType); |
188 |
2 |
consC->addArgSelf("cdr"); |
189 |
2 |
listColors.addConstructor(consC); |
190 |
2 |
listColors.addConstructor(std::make_shared<DTypeConstructor>("nil")); |
191 |
4 |
TypeNode listColorsType = d_nodeManager->mkDatatypeType(listColors); |
192 |
|
const std::vector<std::shared_ptr<DTypeConstructor> >& lctCons = |
193 |
2 |
listColorsType.getDType().getConstructors(); |
194 |
|
|
195 |
4 |
TypeEnumerator te(listColorsType); |
196 |
2 |
ASSERT_FALSE(te.isFinished()); |
197 |
4 |
Node cons = lctCons[0]->getConstructor(); |
198 |
|
Node nil = |
199 |
4 |
d_nodeManager->mkNode(APPLY_CONSTRUCTOR, lctCons[1]->getConstructor()); |
200 |
|
Node red = |
201 |
4 |
d_nodeManager->mkNode(APPLY_CONSTRUCTOR, ctCons[0]->getConstructor()); |
202 |
|
Node orange = |
203 |
4 |
d_nodeManager->mkNode(APPLY_CONSTRUCTOR, ctCons[1]->getConstructor()); |
204 |
|
Node yellow = |
205 |
4 |
d_nodeManager->mkNode(APPLY_CONSTRUCTOR, ctCons[2]->getConstructor()); |
206 |
2 |
ASSERT_EQ(*te, nil); |
207 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkNode(APPLY_CONSTRUCTOR, cons, red, nil)); |
208 |
2 |
ASSERT_FALSE(te.isFinished()); |
209 |
2 |
ASSERT_EQ(*++te, |
210 |
|
d_nodeManager->mkNode( |
211 |
|
APPLY_CONSTRUCTOR, |
212 |
|
cons, |
213 |
|
red, |
214 |
2 |
d_nodeManager->mkNode(APPLY_CONSTRUCTOR, cons, red, nil))); |
215 |
2 |
ASSERT_FALSE(te.isFinished()); |
216 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkNode(APPLY_CONSTRUCTOR, cons, orange, nil)); |
217 |
2 |
ASSERT_FALSE(te.isFinished()); |
218 |
2 |
ASSERT_EQ(*++te, |
219 |
|
d_nodeManager->mkNode( |
220 |
|
APPLY_CONSTRUCTOR, |
221 |
|
cons, |
222 |
|
red, |
223 |
|
d_nodeManager->mkNode( |
224 |
|
APPLY_CONSTRUCTOR, |
225 |
|
cons, |
226 |
|
red, |
227 |
2 |
d_nodeManager->mkNode(APPLY_CONSTRUCTOR, cons, red, nil)))); |
228 |
2 |
ASSERT_FALSE(te.isFinished()); |
229 |
2 |
ASSERT_EQ(*++te, |
230 |
|
d_nodeManager->mkNode( |
231 |
|
APPLY_CONSTRUCTOR, |
232 |
|
cons, |
233 |
|
orange, |
234 |
2 |
d_nodeManager->mkNode(APPLY_CONSTRUCTOR, cons, red, nil))); |
235 |
2 |
ASSERT_FALSE(te.isFinished()); |
236 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkNode(APPLY_CONSTRUCTOR, cons, yellow, nil)); |
237 |
2 |
ASSERT_FALSE(te.isFinished()); |
238 |
2 |
ASSERT_EQ(*++te, |
239 |
|
d_nodeManager->mkNode( |
240 |
|
APPLY_CONSTRUCTOR, |
241 |
|
cons, |
242 |
|
red, |
243 |
2 |
d_nodeManager->mkNode(APPLY_CONSTRUCTOR, cons, orange, nil))); |
244 |
2 |
ASSERT_FALSE(te.isFinished()); |
245 |
|
} |
246 |
|
|
247 |
16 |
TEST_F(TestTheoryWhiteTypeEnumerator, arrays_infinite) |
248 |
|
{ |
249 |
6 |
TypeEnumerator te(d_nodeManager->mkArrayType(d_nodeManager->integerType(), |
250 |
8 |
d_nodeManager->integerType())); |
251 |
4 |
std::unordered_set<Node> elts; |
252 |
2002 |
for (uint32_t i = 0; i < 1000; ++i) |
253 |
|
{ |
254 |
2000 |
ASSERT_FALSE(te.isFinished()); |
255 |
4000 |
Node elt = *te++; |
256 |
|
// ensure no duplicates |
257 |
2000 |
ASSERT_TRUE(elts.find(elt) == elts.end()); |
258 |
2000 |
elts.insert(elt); |
259 |
|
} |
260 |
2 |
ASSERT_FALSE(te.isFinished()); |
261 |
|
|
262 |
|
// ensure that certain items were found |
263 |
4 |
TypeNode arrayType = d_nodeManager->mkArrayType(d_nodeManager->integerType(), |
264 |
8 |
d_nodeManager->integerType()); |
265 |
|
Node zeroes = d_nodeManager->mkConst( |
266 |
4 |
ArrayStoreAll(arrayType, d_nodeManager->mkConst(Rational(0)))); |
267 |
|
Node ones = d_nodeManager->mkConst( |
268 |
4 |
ArrayStoreAll(arrayType, d_nodeManager->mkConst(Rational(1)))); |
269 |
|
Node twos = d_nodeManager->mkConst( |
270 |
4 |
ArrayStoreAll(arrayType, d_nodeManager->mkConst(Rational(2)))); |
271 |
|
Node threes = d_nodeManager->mkConst( |
272 |
4 |
ArrayStoreAll(arrayType, d_nodeManager->mkConst(Rational(3)))); |
273 |
|
Node fours = d_nodeManager->mkConst( |
274 |
4 |
ArrayStoreAll(arrayType, d_nodeManager->mkConst(Rational(4)))); |
275 |
|
Node tens = d_nodeManager->mkConst( |
276 |
4 |
ArrayStoreAll(arrayType, d_nodeManager->mkConst(Rational(10)))); |
277 |
|
|
278 |
4 |
Node zero = d_nodeManager->mkConst(Rational(0)); |
279 |
4 |
Node one = d_nodeManager->mkConst(Rational(1)); |
280 |
4 |
Node two = d_nodeManager->mkConst(Rational(2)); |
281 |
4 |
Node three = d_nodeManager->mkConst(Rational(3)); |
282 |
4 |
Node four = d_nodeManager->mkConst(Rational(4)); |
283 |
4 |
Node five = d_nodeManager->mkConst(Rational(5)); |
284 |
4 |
Node eleven = d_nodeManager->mkConst(Rational(11)); |
285 |
|
|
286 |
2 |
ASSERT_EQ(elts.find(d_nodeManager->mkNode(STORE, ones, zero, zero)), |
287 |
2 |
elts.end()); |
288 |
|
|
289 |
|
// the arrays enumerator is currently not a fair enumerator -- when it is, |
290 |
|
// these should be flipped |
291 |
2 |
ASSERT_EQ(elts.find(d_nodeManager->mkNode(STORE, tens, four, five)), |
292 |
2 |
elts.end()); |
293 |
2 |
ASSERT_EQ(elts.find(d_nodeManager->mkNode( |
294 |
|
STORE, |
295 |
|
d_nodeManager->mkNode( |
296 |
|
STORE, |
297 |
|
d_nodeManager->mkNode(STORE, fours, eleven, two), |
298 |
|
two, |
299 |
|
one), |
300 |
|
zero, |
301 |
|
two)), |
302 |
2 |
elts.end()); |
303 |
2 |
ASSERT_EQ(elts.find(threes), elts.end()); |
304 |
2 |
ASSERT_EQ(elts.find(d_nodeManager->mkNode( |
305 |
|
STORE, |
306 |
|
d_nodeManager->mkNode( |
307 |
|
STORE, |
308 |
|
d_nodeManager->mkNode( |
309 |
|
STORE, |
310 |
|
d_nodeManager->mkNode(STORE, twos, three, zero), |
311 |
|
two, |
312 |
|
zero), |
313 |
|
one, |
314 |
|
zero), |
315 |
|
zero, |
316 |
|
zero)), |
317 |
2 |
elts.end()); |
318 |
|
} |
319 |
|
|
320 |
16 |
TEST_F(TestTheoryWhiteTypeEnumerator, bv) |
321 |
|
{ |
322 |
4 |
TypeEnumerator te(d_nodeManager->mkBitVectorType(3)); |
323 |
2 |
ASSERT_EQ(*te, d_nodeManager->mkConst(BitVector(3u, 0u))); |
324 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(BitVector(3u, 1u))); |
325 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(BitVector(3u, 2u))); |
326 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(BitVector(3u, 3u))); |
327 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(BitVector(3u, 4u))); |
328 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(BitVector(3u, 5u))); |
329 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(BitVector(3u, 6u))); |
330 |
2 |
ASSERT_EQ(*++te, d_nodeManager->mkConst(BitVector(3u, 7u))); |
331 |
4 |
ASSERT_THROW(*++te, NoMoreValuesException); |
332 |
4 |
ASSERT_THROW(*++te, NoMoreValuesException); |
333 |
4 |
ASSERT_THROW(*++te, NoMoreValuesException); |
334 |
|
} |
335 |
|
} // namespace test |
336 |
1494078 |
} // namespace cvc5 |