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