1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Aina Niemetz, Andrew Reynolds, Mathias Preiner |
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 |
|
* Black box testing of the guards of the C++ API functions. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "test_api.h" |
17 |
|
|
18 |
|
namespace cvc5 { |
19 |
|
|
20 |
|
using namespace api; |
21 |
|
|
22 |
|
namespace test { |
23 |
|
|
24 |
224 |
class TestApiBlackSort : public TestApi |
25 |
|
{ |
26 |
|
protected: |
27 |
16 |
Sort create_datatype_sort() |
28 |
|
{ |
29 |
32 |
DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); |
30 |
32 |
DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); |
31 |
16 |
cons.addSelector("head", d_solver.getIntegerSort()); |
32 |
16 |
cons.addSelectorSelf("tail"); |
33 |
16 |
dtypeSpec.addConstructor(cons); |
34 |
32 |
DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); |
35 |
16 |
dtypeSpec.addConstructor(nil); |
36 |
32 |
return d_solver.mkDatatypeSort(dtypeSpec); |
37 |
|
} |
38 |
|
|
39 |
4 |
Sort create_param_datatype_sort() |
40 |
|
{ |
41 |
8 |
Sort sort = d_solver.mkParamSort("T"); |
42 |
8 |
DatatypeDecl paramDtypeSpec = d_solver.mkDatatypeDecl("paramlist", sort); |
43 |
|
DatatypeConstructorDecl paramCons = |
44 |
8 |
d_solver.mkDatatypeConstructorDecl("cons"); |
45 |
|
DatatypeConstructorDecl paramNil = |
46 |
8 |
d_solver.mkDatatypeConstructorDecl("nil"); |
47 |
4 |
paramCons.addSelector("head", sort); |
48 |
4 |
paramDtypeSpec.addConstructor(paramCons); |
49 |
4 |
paramDtypeSpec.addConstructor(paramNil); |
50 |
8 |
return d_solver.mkDatatypeSort(paramDtypeSpec); |
51 |
|
} |
52 |
|
}; |
53 |
|
|
54 |
65 |
TEST_F(TestApiBlackSort, operators_comparison) |
55 |
|
{ |
56 |
2 |
ASSERT_NO_THROW(d_solver.getIntegerSort() == Sort()); |
57 |
2 |
ASSERT_NO_THROW(d_solver.getIntegerSort() != Sort()); |
58 |
2 |
ASSERT_NO_THROW(d_solver.getIntegerSort() < Sort()); |
59 |
2 |
ASSERT_NO_THROW(d_solver.getIntegerSort() <= Sort()); |
60 |
2 |
ASSERT_NO_THROW(d_solver.getIntegerSort() > Sort()); |
61 |
2 |
ASSERT_NO_THROW(d_solver.getIntegerSort() >= Sort()); |
62 |
|
} |
63 |
|
|
64 |
65 |
TEST_F(TestApiBlackSort, isNull) |
65 |
|
{ |
66 |
4 |
Sort x; |
67 |
2 |
ASSERT_TRUE(x.isNull()); |
68 |
2 |
x = d_solver.getBooleanSort(); |
69 |
2 |
ASSERT_FALSE(x.isNull()); |
70 |
|
} |
71 |
|
|
72 |
65 |
TEST_F(TestApiBlackSort, isBoolean) |
73 |
|
{ |
74 |
2 |
ASSERT_TRUE(d_solver.getBooleanSort().isBoolean()); |
75 |
2 |
ASSERT_NO_THROW(Sort().isBoolean()); |
76 |
|
} |
77 |
|
|
78 |
65 |
TEST_F(TestApiBlackSort, isInteger) |
79 |
|
{ |
80 |
2 |
ASSERT_TRUE(d_solver.getIntegerSort().isInteger()); |
81 |
2 |
ASSERT_TRUE(!d_solver.getRealSort().isInteger()); |
82 |
2 |
ASSERT_NO_THROW(Sort().isInteger()); |
83 |
|
} |
84 |
|
|
85 |
65 |
TEST_F(TestApiBlackSort, isReal) |
86 |
|
{ |
87 |
2 |
ASSERT_TRUE(d_solver.getRealSort().isReal()); |
88 |
2 |
ASSERT_TRUE(!d_solver.getIntegerSort().isReal()); |
89 |
2 |
ASSERT_NO_THROW(Sort().isReal()); |
90 |
|
} |
91 |
|
|
92 |
65 |
TEST_F(TestApiBlackSort, isString) |
93 |
|
{ |
94 |
2 |
ASSERT_TRUE(d_solver.getStringSort().isString()); |
95 |
2 |
ASSERT_NO_THROW(Sort().isString()); |
96 |
|
} |
97 |
|
|
98 |
65 |
TEST_F(TestApiBlackSort, isRegExp) |
99 |
|
{ |
100 |
2 |
ASSERT_TRUE(d_solver.getRegExpSort().isRegExp()); |
101 |
2 |
ASSERT_NO_THROW(Sort().isRegExp()); |
102 |
|
} |
103 |
|
|
104 |
65 |
TEST_F(TestApiBlackSort, isRoundingMode) |
105 |
|
{ |
106 |
2 |
ASSERT_TRUE(d_solver.getRoundingModeSort().isRoundingMode()); |
107 |
2 |
ASSERT_NO_THROW(Sort().isRoundingMode()); |
108 |
|
} |
109 |
|
|
110 |
65 |
TEST_F(TestApiBlackSort, isBitVector) |
111 |
|
{ |
112 |
2 |
ASSERT_TRUE(d_solver.mkBitVectorSort(8).isBitVector()); |
113 |
2 |
ASSERT_NO_THROW(Sort().isBitVector()); |
114 |
|
} |
115 |
|
|
116 |
65 |
TEST_F(TestApiBlackSort, isFloatingPoint) |
117 |
|
{ |
118 |
2 |
ASSERT_TRUE(d_solver.mkFloatingPointSort(8, 24).isFloatingPoint()); |
119 |
2 |
ASSERT_NO_THROW(Sort().isFloatingPoint()); |
120 |
|
} |
121 |
|
|
122 |
65 |
TEST_F(TestApiBlackSort, isDatatype) |
123 |
|
{ |
124 |
4 |
Sort dt_sort = create_datatype_sort(); |
125 |
2 |
ASSERT_TRUE(dt_sort.isDatatype()); |
126 |
2 |
ASSERT_NO_THROW(Sort().isDatatype()); |
127 |
|
} |
128 |
|
|
129 |
65 |
TEST_F(TestApiBlackSort, isParametricDatatype) |
130 |
|
{ |
131 |
4 |
Sort param_dt_sort = create_param_datatype_sort(); |
132 |
2 |
ASSERT_TRUE(param_dt_sort.isParametricDatatype()); |
133 |
2 |
ASSERT_NO_THROW(Sort().isParametricDatatype()); |
134 |
|
} |
135 |
|
|
136 |
65 |
TEST_F(TestApiBlackSort, isConstructor) |
137 |
|
{ |
138 |
4 |
Sort dt_sort = create_datatype_sort(); |
139 |
4 |
Datatype dt = dt_sort.getDatatype(); |
140 |
4 |
Sort cons_sort = dt[0].getConstructorTerm().getSort(); |
141 |
2 |
ASSERT_TRUE(cons_sort.isConstructor()); |
142 |
2 |
ASSERT_NO_THROW(Sort().isConstructor()); |
143 |
|
} |
144 |
|
|
145 |
65 |
TEST_F(TestApiBlackSort, isSelector) |
146 |
|
{ |
147 |
4 |
Sort dt_sort = create_datatype_sort(); |
148 |
4 |
Datatype dt = dt_sort.getDatatype(); |
149 |
4 |
Sort cons_sort = dt[0][1].getSelectorTerm().getSort(); |
150 |
2 |
ASSERT_TRUE(cons_sort.isSelector()); |
151 |
2 |
ASSERT_NO_THROW(Sort().isSelector()); |
152 |
|
} |
153 |
|
|
154 |
65 |
TEST_F(TestApiBlackSort, isTester) |
155 |
|
{ |
156 |
4 |
Sort dt_sort = create_datatype_sort(); |
157 |
4 |
Datatype dt = dt_sort.getDatatype(); |
158 |
4 |
Sort testerSort = dt[0].getTesterTerm().getSort(); |
159 |
2 |
ASSERT_TRUE(testerSort.isTester()); |
160 |
2 |
ASSERT_NO_THROW(Sort().isTester()); |
161 |
|
} |
162 |
|
|
163 |
65 |
TEST_F(TestApiBlackSort, isUpdater) |
164 |
|
{ |
165 |
4 |
Sort dt_sort = create_datatype_sort(); |
166 |
4 |
Datatype dt = dt_sort.getDatatype(); |
167 |
4 |
Sort updaterSort = dt[0][0].getUpdaterTerm().getSort(); |
168 |
2 |
ASSERT_TRUE(updaterSort.isUpdater()); |
169 |
2 |
ASSERT_NO_THROW(Sort().isUpdater()); |
170 |
|
} |
171 |
|
|
172 |
65 |
TEST_F(TestApiBlackSort, isFunction) |
173 |
|
{ |
174 |
4 |
Sort fun_sort = d_solver.mkFunctionSort(d_solver.getRealSort(), |
175 |
8 |
d_solver.getIntegerSort()); |
176 |
2 |
ASSERT_TRUE(fun_sort.isFunction()); |
177 |
2 |
ASSERT_NO_THROW(Sort().isFunction()); |
178 |
|
} |
179 |
|
|
180 |
65 |
TEST_F(TestApiBlackSort, isPredicate) |
181 |
|
{ |
182 |
4 |
Sort pred_sort = d_solver.mkPredicateSort({d_solver.getRealSort()}); |
183 |
2 |
ASSERT_TRUE(pred_sort.isPredicate()); |
184 |
2 |
ASSERT_NO_THROW(Sort().isPredicate()); |
185 |
|
} |
186 |
|
|
187 |
65 |
TEST_F(TestApiBlackSort, isTuple) |
188 |
|
{ |
189 |
4 |
Sort tup_sort = d_solver.mkTupleSort({d_solver.getRealSort()}); |
190 |
2 |
ASSERT_TRUE(tup_sort.isTuple()); |
191 |
2 |
ASSERT_NO_THROW(Sort().isTuple()); |
192 |
|
} |
193 |
|
|
194 |
65 |
TEST_F(TestApiBlackSort, isRecord) |
195 |
|
{ |
196 |
|
Sort rec_sort = |
197 |
4 |
d_solver.mkRecordSort({std::make_pair("asdf", d_solver.getRealSort())}); |
198 |
2 |
ASSERT_TRUE(rec_sort.isRecord()); |
199 |
2 |
ASSERT_NO_THROW(Sort().isRecord()); |
200 |
|
} |
201 |
|
|
202 |
65 |
TEST_F(TestApiBlackSort, isArray) |
203 |
|
{ |
204 |
|
Sort arr_sort = |
205 |
4 |
d_solver.mkArraySort(d_solver.getRealSort(), d_solver.getIntegerSort()); |
206 |
2 |
ASSERT_TRUE(arr_sort.isArray()); |
207 |
2 |
ASSERT_NO_THROW(Sort().isArray()); |
208 |
|
} |
209 |
|
|
210 |
65 |
TEST_F(TestApiBlackSort, isSet) |
211 |
|
{ |
212 |
4 |
Sort set_sort = d_solver.mkSetSort(d_solver.getRealSort()); |
213 |
2 |
ASSERT_TRUE(set_sort.isSet()); |
214 |
2 |
ASSERT_NO_THROW(Sort().isSet()); |
215 |
|
} |
216 |
|
|
217 |
65 |
TEST_F(TestApiBlackSort, isBag) |
218 |
|
{ |
219 |
4 |
Sort bag_sort = d_solver.mkBagSort(d_solver.getRealSort()); |
220 |
2 |
ASSERT_TRUE(bag_sort.isBag()); |
221 |
2 |
ASSERT_NO_THROW(Sort().isBag()); |
222 |
|
} |
223 |
|
|
224 |
65 |
TEST_F(TestApiBlackSort, isSequence) |
225 |
|
{ |
226 |
4 |
Sort seq_sort = d_solver.mkSequenceSort(d_solver.getRealSort()); |
227 |
2 |
ASSERT_TRUE(seq_sort.isSequence()); |
228 |
2 |
ASSERT_NO_THROW(Sort().isSequence()); |
229 |
|
} |
230 |
|
|
231 |
65 |
TEST_F(TestApiBlackSort, isUninterpreted) |
232 |
|
{ |
233 |
4 |
Sort un_sort = d_solver.mkUninterpretedSort("asdf"); |
234 |
2 |
ASSERT_TRUE(un_sort.isUninterpretedSort()); |
235 |
2 |
ASSERT_NO_THROW(Sort().isUninterpretedSort()); |
236 |
|
} |
237 |
|
|
238 |
65 |
TEST_F(TestApiBlackSort, isSortConstructor) |
239 |
|
{ |
240 |
4 |
Sort sc_sort = d_solver.mkSortConstructorSort("asdf", 1); |
241 |
2 |
ASSERT_TRUE(sc_sort.isSortConstructor()); |
242 |
2 |
ASSERT_NO_THROW(Sort().isSortConstructor()); |
243 |
|
} |
244 |
|
|
245 |
65 |
TEST_F(TestApiBlackSort, isFirstClass) |
246 |
|
{ |
247 |
4 |
Sort fun_sort = d_solver.mkFunctionSort(d_solver.getRealSort(), |
248 |
8 |
d_solver.getIntegerSort()); |
249 |
2 |
ASSERT_TRUE(d_solver.getIntegerSort().isFirstClass()); |
250 |
2 |
ASSERT_TRUE(fun_sort.isFirstClass()); |
251 |
4 |
Sort reSort = d_solver.getRegExpSort(); |
252 |
2 |
ASSERT_FALSE(reSort.isFirstClass()); |
253 |
2 |
ASSERT_NO_THROW(Sort().isFirstClass()); |
254 |
|
} |
255 |
|
|
256 |
65 |
TEST_F(TestApiBlackSort, isFunctionLike) |
257 |
|
{ |
258 |
4 |
Sort fun_sort = d_solver.mkFunctionSort(d_solver.getRealSort(), |
259 |
8 |
d_solver.getIntegerSort()); |
260 |
2 |
ASSERT_FALSE(d_solver.getIntegerSort().isFunctionLike()); |
261 |
2 |
ASSERT_TRUE(fun_sort.isFunctionLike()); |
262 |
|
|
263 |
4 |
Sort dt_sort = create_datatype_sort(); |
264 |
4 |
Datatype dt = dt_sort.getDatatype(); |
265 |
4 |
Sort cons_sort = dt[0][1].getSelectorTerm().getSort(); |
266 |
2 |
ASSERT_TRUE(cons_sort.isFunctionLike()); |
267 |
|
|
268 |
2 |
ASSERT_NO_THROW(Sort().isFunctionLike()); |
269 |
|
} |
270 |
|
|
271 |
65 |
TEST_F(TestApiBlackSort, isSubsortOf) |
272 |
|
{ |
273 |
2 |
ASSERT_TRUE(d_solver.getIntegerSort().isSubsortOf(d_solver.getIntegerSort())); |
274 |
2 |
ASSERT_TRUE(d_solver.getIntegerSort().isSubsortOf(d_solver.getRealSort())); |
275 |
2 |
ASSERT_FALSE( |
276 |
2 |
d_solver.getIntegerSort().isSubsortOf(d_solver.getBooleanSort())); |
277 |
2 |
ASSERT_NO_THROW(Sort().isSubsortOf(Sort())); |
278 |
|
} |
279 |
|
|
280 |
65 |
TEST_F(TestApiBlackSort, isComparableTo) |
281 |
|
{ |
282 |
2 |
ASSERT_TRUE( |
283 |
2 |
d_solver.getIntegerSort().isComparableTo(d_solver.getIntegerSort())); |
284 |
2 |
ASSERT_TRUE(d_solver.getIntegerSort().isComparableTo(d_solver.getRealSort())); |
285 |
2 |
ASSERT_FALSE( |
286 |
2 |
d_solver.getIntegerSort().isComparableTo(d_solver.getBooleanSort())); |
287 |
2 |
ASSERT_NO_THROW(Sort().isComparableTo(Sort())); |
288 |
|
} |
289 |
|
|
290 |
65 |
TEST_F(TestApiBlackSort, getDatatype) |
291 |
|
{ |
292 |
4 |
Sort dtypeSort = create_datatype_sort(); |
293 |
2 |
ASSERT_NO_THROW(dtypeSort.getDatatype()); |
294 |
|
// create bv sort, check should fail |
295 |
4 |
Sort bvSort = d_solver.mkBitVectorSort(32); |
296 |
4 |
ASSERT_THROW(bvSort.getDatatype(), CVC5ApiException); |
297 |
|
} |
298 |
|
|
299 |
65 |
TEST_F(TestApiBlackSort, datatypeSorts) |
300 |
|
{ |
301 |
4 |
Sort intSort = d_solver.getIntegerSort(); |
302 |
4 |
Sort dtypeSort = create_datatype_sort(); |
303 |
4 |
Datatype dt = dtypeSort.getDatatype(); |
304 |
2 |
ASSERT_FALSE(dtypeSort.isConstructor()); |
305 |
4 |
ASSERT_THROW(dtypeSort.getConstructorCodomainSort(), CVC5ApiException); |
306 |
4 |
ASSERT_THROW(dtypeSort.getConstructorDomainSorts(), CVC5ApiException); |
307 |
4 |
ASSERT_THROW(dtypeSort.getConstructorArity(), CVC5ApiException); |
308 |
|
|
309 |
|
// get constructor |
310 |
4 |
DatatypeConstructor dcons = dt[0]; |
311 |
4 |
Term consTerm = dcons.getConstructorTerm(); |
312 |
4 |
Sort consSort = consTerm.getSort(); |
313 |
2 |
ASSERT_TRUE(consSort.isConstructor()); |
314 |
2 |
ASSERT_FALSE(consSort.isTester()); |
315 |
2 |
ASSERT_FALSE(consSort.isSelector()); |
316 |
2 |
ASSERT_EQ(consSort.getConstructorArity(), 2); |
317 |
4 |
std::vector<Sort> consDomSorts = consSort.getConstructorDomainSorts(); |
318 |
2 |
ASSERT_EQ(consDomSorts[0], intSort); |
319 |
2 |
ASSERT_EQ(consDomSorts[1], dtypeSort); |
320 |
2 |
ASSERT_EQ(consSort.getConstructorCodomainSort(), dtypeSort); |
321 |
|
|
322 |
|
// get tester |
323 |
4 |
Term isConsTerm = dcons.getTesterTerm(); |
324 |
2 |
ASSERT_TRUE(isConsTerm.getSort().isTester()); |
325 |
2 |
ASSERT_EQ(isConsTerm.getSort().getTesterDomainSort(), dtypeSort); |
326 |
4 |
Sort booleanSort = d_solver.getBooleanSort(); |
327 |
2 |
ASSERT_EQ(isConsTerm.getSort().getTesterCodomainSort(), booleanSort); |
328 |
4 |
ASSERT_THROW(booleanSort.getTesterDomainSort(), CVC5ApiException); |
329 |
4 |
ASSERT_THROW(booleanSort.getTesterCodomainSort(), CVC5ApiException); |
330 |
|
|
331 |
|
// get selector |
332 |
4 |
DatatypeSelector dselTail = dcons[1]; |
333 |
4 |
Term tailTerm = dselTail.getSelectorTerm(); |
334 |
2 |
ASSERT_TRUE(tailTerm.getSort().isSelector()); |
335 |
2 |
ASSERT_EQ(tailTerm.getSort().getSelectorDomainSort(), dtypeSort); |
336 |
2 |
ASSERT_EQ(tailTerm.getSort().getSelectorCodomainSort(), dtypeSort); |
337 |
4 |
ASSERT_THROW(booleanSort.getSelectorDomainSort(), CVC5ApiException); |
338 |
4 |
ASSERT_THROW(booleanSort.getSelectorCodomainSort(), CVC5ApiException); |
339 |
|
} |
340 |
|
|
341 |
65 |
TEST_F(TestApiBlackSort, instantiate) |
342 |
|
{ |
343 |
|
// instantiate parametric datatype, check should not fail |
344 |
4 |
Sort paramDtypeSort = create_param_datatype_sort(); |
345 |
2 |
ASSERT_NO_THROW( |
346 |
|
paramDtypeSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()})); |
347 |
|
// instantiate non-parametric datatype sort, check should fail |
348 |
4 |
DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); |
349 |
4 |
DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); |
350 |
2 |
cons.addSelector("head", d_solver.getIntegerSort()); |
351 |
2 |
dtypeSpec.addConstructor(cons); |
352 |
4 |
DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); |
353 |
2 |
dtypeSpec.addConstructor(nil); |
354 |
4 |
Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); |
355 |
4 |
ASSERT_THROW( |
356 |
|
dtypeSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()}), |
357 |
2 |
CVC5ApiException); |
358 |
|
} |
359 |
|
|
360 |
65 |
TEST_F(TestApiBlackSort, getFunctionArity) |
361 |
|
{ |
362 |
4 |
Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), |
363 |
8 |
d_solver.getIntegerSort()); |
364 |
2 |
ASSERT_NO_THROW(funSort.getFunctionArity()); |
365 |
4 |
Sort bvSort = d_solver.mkBitVectorSort(32); |
366 |
4 |
ASSERT_THROW(bvSort.getFunctionArity(), CVC5ApiException); |
367 |
|
} |
368 |
|
|
369 |
65 |
TEST_F(TestApiBlackSort, getFunctionDomainSorts) |
370 |
|
{ |
371 |
4 |
Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), |
372 |
8 |
d_solver.getIntegerSort()); |
373 |
2 |
ASSERT_NO_THROW(funSort.getFunctionDomainSorts()); |
374 |
4 |
Sort bvSort = d_solver.mkBitVectorSort(32); |
375 |
4 |
ASSERT_THROW(bvSort.getFunctionDomainSorts(), CVC5ApiException); |
376 |
|
} |
377 |
|
|
378 |
65 |
TEST_F(TestApiBlackSort, getFunctionCodomainSort) |
379 |
|
{ |
380 |
4 |
Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), |
381 |
8 |
d_solver.getIntegerSort()); |
382 |
2 |
ASSERT_NO_THROW(funSort.getFunctionCodomainSort()); |
383 |
4 |
Sort bvSort = d_solver.mkBitVectorSort(32); |
384 |
4 |
ASSERT_THROW(bvSort.getFunctionCodomainSort(), CVC5ApiException); |
385 |
|
} |
386 |
|
|
387 |
65 |
TEST_F(TestApiBlackSort, getArrayIndexSort) |
388 |
|
{ |
389 |
4 |
Sort elementSort = d_solver.mkBitVectorSort(32); |
390 |
4 |
Sort indexSort = d_solver.mkBitVectorSort(32); |
391 |
4 |
Sort arraySort = d_solver.mkArraySort(indexSort, elementSort); |
392 |
2 |
ASSERT_NO_THROW(arraySort.getArrayIndexSort()); |
393 |
4 |
ASSERT_THROW(indexSort.getArrayIndexSort(), CVC5ApiException); |
394 |
|
} |
395 |
|
|
396 |
65 |
TEST_F(TestApiBlackSort, getArrayElementSort) |
397 |
|
{ |
398 |
4 |
Sort elementSort = d_solver.mkBitVectorSort(32); |
399 |
4 |
Sort indexSort = d_solver.mkBitVectorSort(32); |
400 |
4 |
Sort arraySort = d_solver.mkArraySort(indexSort, elementSort); |
401 |
2 |
ASSERT_NO_THROW(arraySort.getArrayElementSort()); |
402 |
4 |
ASSERT_THROW(indexSort.getArrayElementSort(), CVC5ApiException); |
403 |
|
} |
404 |
|
|
405 |
65 |
TEST_F(TestApiBlackSort, getSetElementSort) |
406 |
|
{ |
407 |
4 |
Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); |
408 |
2 |
ASSERT_NO_THROW(setSort.getSetElementSort()); |
409 |
4 |
Sort elementSort = setSort.getSetElementSort(); |
410 |
2 |
ASSERT_EQ(elementSort, d_solver.getIntegerSort()); |
411 |
4 |
Sort bvSort = d_solver.mkBitVectorSort(32); |
412 |
4 |
ASSERT_THROW(bvSort.getSetElementSort(), CVC5ApiException); |
413 |
|
} |
414 |
|
|
415 |
65 |
TEST_F(TestApiBlackSort, getBagElementSort) |
416 |
|
{ |
417 |
4 |
Sort bagSort = d_solver.mkBagSort(d_solver.getIntegerSort()); |
418 |
2 |
ASSERT_NO_THROW(bagSort.getBagElementSort()); |
419 |
4 |
Sort elementSort = bagSort.getBagElementSort(); |
420 |
2 |
ASSERT_EQ(elementSort, d_solver.getIntegerSort()); |
421 |
4 |
Sort bvSort = d_solver.mkBitVectorSort(32); |
422 |
4 |
ASSERT_THROW(bvSort.getBagElementSort(), CVC5ApiException); |
423 |
|
} |
424 |
|
|
425 |
65 |
TEST_F(TestApiBlackSort, getSequenceElementSort) |
426 |
|
{ |
427 |
4 |
Sort seqSort = d_solver.mkSequenceSort(d_solver.getIntegerSort()); |
428 |
2 |
ASSERT_TRUE(seqSort.isSequence()); |
429 |
2 |
ASSERT_NO_THROW(seqSort.getSequenceElementSort()); |
430 |
4 |
Sort bvSort = d_solver.mkBitVectorSort(32); |
431 |
2 |
ASSERT_FALSE(bvSort.isSequence()); |
432 |
4 |
ASSERT_THROW(bvSort.getSequenceElementSort(), CVC5ApiException); |
433 |
|
} |
434 |
|
|
435 |
65 |
TEST_F(TestApiBlackSort, getUninterpretedSortName) |
436 |
|
{ |
437 |
4 |
Sort uSort = d_solver.mkUninterpretedSort("u"); |
438 |
2 |
ASSERT_NO_THROW(uSort.getUninterpretedSortName()); |
439 |
4 |
Sort bvSort = d_solver.mkBitVectorSort(32); |
440 |
4 |
ASSERT_THROW(bvSort.getUninterpretedSortName(), CVC5ApiException); |
441 |
|
} |
442 |
|
|
443 |
65 |
TEST_F(TestApiBlackSort, isUninterpretedSortParameterized) |
444 |
|
{ |
445 |
4 |
Sort uSort = d_solver.mkUninterpretedSort("u"); |
446 |
2 |
ASSERT_FALSE(uSort.isUninterpretedSortParameterized()); |
447 |
4 |
Sort sSort = d_solver.mkSortConstructorSort("s", 1); |
448 |
4 |
Sort siSort = sSort.instantiate({uSort}); |
449 |
2 |
ASSERT_TRUE(siSort.isUninterpretedSortParameterized()); |
450 |
4 |
Sort bvSort = d_solver.mkBitVectorSort(32); |
451 |
4 |
ASSERT_THROW(bvSort.isUninterpretedSortParameterized(), CVC5ApiException); |
452 |
|
} |
453 |
|
|
454 |
65 |
TEST_F(TestApiBlackSort, getUninterpretedSortParamSorts) |
455 |
|
{ |
456 |
4 |
Sort uSort = d_solver.mkUninterpretedSort("u"); |
457 |
2 |
ASSERT_NO_THROW(uSort.getUninterpretedSortParamSorts()); |
458 |
4 |
Sort sSort = d_solver.mkSortConstructorSort("s", 2); |
459 |
4 |
Sort siSort = sSort.instantiate({uSort, uSort}); |
460 |
2 |
ASSERT_EQ(siSort.getUninterpretedSortParamSorts().size(), 2); |
461 |
4 |
Sort bvSort = d_solver.mkBitVectorSort(32); |
462 |
4 |
ASSERT_THROW(bvSort.getUninterpretedSortParamSorts(), CVC5ApiException); |
463 |
|
} |
464 |
|
|
465 |
65 |
TEST_F(TestApiBlackSort, getUninterpretedSortConstructorName) |
466 |
|
{ |
467 |
4 |
Sort sSort = d_solver.mkSortConstructorSort("s", 2); |
468 |
2 |
ASSERT_NO_THROW(sSort.getSortConstructorName()); |
469 |
4 |
Sort bvSort = d_solver.mkBitVectorSort(32); |
470 |
4 |
ASSERT_THROW(bvSort.getSortConstructorName(), CVC5ApiException); |
471 |
|
} |
472 |
|
|
473 |
65 |
TEST_F(TestApiBlackSort, getUninterpretedSortConstructorArity) |
474 |
|
{ |
475 |
4 |
Sort sSort = d_solver.mkSortConstructorSort("s", 2); |
476 |
2 |
ASSERT_NO_THROW(sSort.getSortConstructorArity()); |
477 |
4 |
Sort bvSort = d_solver.mkBitVectorSort(32); |
478 |
4 |
ASSERT_THROW(bvSort.getSortConstructorArity(), CVC5ApiException); |
479 |
|
} |
480 |
|
|
481 |
65 |
TEST_F(TestApiBlackSort, getBitVectorSize) |
482 |
|
{ |
483 |
4 |
Sort bvSort = d_solver.mkBitVectorSort(32); |
484 |
2 |
ASSERT_NO_THROW(bvSort.getBitVectorSize()); |
485 |
4 |
Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); |
486 |
4 |
ASSERT_THROW(setSort.getBitVectorSize(), CVC5ApiException); |
487 |
|
} |
488 |
|
|
489 |
65 |
TEST_F(TestApiBlackSort, getFloatingPointExponentSize) |
490 |
|
{ |
491 |
4 |
Sort fpSort = d_solver.mkFloatingPointSort(4, 8); |
492 |
2 |
ASSERT_NO_THROW(fpSort.getFloatingPointExponentSize()); |
493 |
4 |
Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); |
494 |
4 |
ASSERT_THROW(setSort.getFloatingPointExponentSize(), CVC5ApiException); |
495 |
|
} |
496 |
|
|
497 |
65 |
TEST_F(TestApiBlackSort, getFloatingPointSignificandSize) |
498 |
|
{ |
499 |
4 |
Sort fpSort = d_solver.mkFloatingPointSort(4, 8); |
500 |
2 |
ASSERT_NO_THROW(fpSort.getFloatingPointSignificandSize()); |
501 |
4 |
Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); |
502 |
4 |
ASSERT_THROW(setSort.getFloatingPointSignificandSize(), CVC5ApiException); |
503 |
|
} |
504 |
|
|
505 |
65 |
TEST_F(TestApiBlackSort, getDatatypeParamSorts) |
506 |
|
{ |
507 |
|
// create parametric datatype, check should not fail |
508 |
4 |
Sort sort = d_solver.mkParamSort("T"); |
509 |
4 |
DatatypeDecl paramDtypeSpec = d_solver.mkDatatypeDecl("paramlist", sort); |
510 |
|
DatatypeConstructorDecl paramCons = |
511 |
4 |
d_solver.mkDatatypeConstructorDecl("cons"); |
512 |
4 |
DatatypeConstructorDecl paramNil = d_solver.mkDatatypeConstructorDecl("nil"); |
513 |
2 |
paramCons.addSelector("head", sort); |
514 |
2 |
paramDtypeSpec.addConstructor(paramCons); |
515 |
2 |
paramDtypeSpec.addConstructor(paramNil); |
516 |
4 |
Sort paramDtypeSort = d_solver.mkDatatypeSort(paramDtypeSpec); |
517 |
2 |
ASSERT_NO_THROW(paramDtypeSort.getDatatypeParamSorts()); |
518 |
|
// create non-parametric datatype sort, check should fail |
519 |
4 |
DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); |
520 |
4 |
DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); |
521 |
2 |
cons.addSelector("head", d_solver.getIntegerSort()); |
522 |
2 |
dtypeSpec.addConstructor(cons); |
523 |
4 |
DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); |
524 |
2 |
dtypeSpec.addConstructor(nil); |
525 |
4 |
Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); |
526 |
4 |
ASSERT_THROW(dtypeSort.getDatatypeParamSorts(), CVC5ApiException); |
527 |
|
} |
528 |
|
|
529 |
65 |
TEST_F(TestApiBlackSort, getDatatypeArity) |
530 |
|
{ |
531 |
|
// create datatype sort, check should not fail |
532 |
4 |
DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); |
533 |
4 |
DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); |
534 |
2 |
cons.addSelector("head", d_solver.getIntegerSort()); |
535 |
2 |
dtypeSpec.addConstructor(cons); |
536 |
4 |
DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); |
537 |
2 |
dtypeSpec.addConstructor(nil); |
538 |
4 |
Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); |
539 |
2 |
ASSERT_NO_THROW(dtypeSort.getDatatypeArity()); |
540 |
|
// create bv sort, check should fail |
541 |
4 |
Sort bvSort = d_solver.mkBitVectorSort(32); |
542 |
4 |
ASSERT_THROW(bvSort.getDatatypeArity(), CVC5ApiException); |
543 |
|
} |
544 |
|
|
545 |
65 |
TEST_F(TestApiBlackSort, getTupleLength) |
546 |
|
{ |
547 |
|
Sort tupleSort = d_solver.mkTupleSort( |
548 |
4 |
{d_solver.getIntegerSort(), d_solver.getIntegerSort()}); |
549 |
2 |
ASSERT_NO_THROW(tupleSort.getTupleLength()); |
550 |
4 |
Sort bvSort = d_solver.mkBitVectorSort(32); |
551 |
4 |
ASSERT_THROW(bvSort.getTupleLength(), CVC5ApiException); |
552 |
|
} |
553 |
|
|
554 |
65 |
TEST_F(TestApiBlackSort, getTupleSorts) |
555 |
|
{ |
556 |
|
Sort tupleSort = d_solver.mkTupleSort( |
557 |
4 |
{d_solver.getIntegerSort(), d_solver.getIntegerSort()}); |
558 |
2 |
ASSERT_NO_THROW(tupleSort.getTupleSorts()); |
559 |
4 |
Sort bvSort = d_solver.mkBitVectorSort(32); |
560 |
4 |
ASSERT_THROW(bvSort.getTupleSorts(), CVC5ApiException); |
561 |
|
} |
562 |
|
|
563 |
65 |
TEST_F(TestApiBlackSort, sortCompare) |
564 |
|
{ |
565 |
4 |
Sort boolSort = d_solver.getBooleanSort(); |
566 |
4 |
Sort intSort = d_solver.getIntegerSort(); |
567 |
4 |
Sort bvSort = d_solver.mkBitVectorSort(32); |
568 |
4 |
Sort bvSort2 = d_solver.mkBitVectorSort(32); |
569 |
2 |
ASSERT_TRUE(bvSort >= bvSort2); |
570 |
2 |
ASSERT_TRUE(bvSort <= bvSort2); |
571 |
2 |
ASSERT_TRUE((intSort > boolSort) != (intSort < boolSort)); |
572 |
2 |
ASSERT_TRUE((intSort > bvSort || intSort == bvSort) == (intSort >= bvSort)); |
573 |
|
} |
574 |
|
|
575 |
65 |
TEST_F(TestApiBlackSort, sortSubtyping) |
576 |
|
{ |
577 |
4 |
Sort intSort = d_solver.getIntegerSort(); |
578 |
4 |
Sort realSort = d_solver.getRealSort(); |
579 |
2 |
ASSERT_TRUE(intSort.isSubsortOf(realSort)); |
580 |
2 |
ASSERT_FALSE(realSort.isSubsortOf(intSort)); |
581 |
2 |
ASSERT_TRUE(intSort.isComparableTo(realSort)); |
582 |
2 |
ASSERT_TRUE(realSort.isComparableTo(intSort)); |
583 |
|
|
584 |
4 |
Sort arraySortII = d_solver.mkArraySort(intSort, intSort); |
585 |
4 |
Sort arraySortIR = d_solver.mkArraySort(intSort, realSort); |
586 |
2 |
ASSERT_FALSE(arraySortII.isComparableTo(intSort)); |
587 |
|
// we do not support subtyping for arrays |
588 |
2 |
ASSERT_FALSE(arraySortII.isComparableTo(arraySortIR)); |
589 |
|
|
590 |
4 |
Sort setSortI = d_solver.mkSetSort(intSort); |
591 |
4 |
Sort setSortR = d_solver.mkSetSort(realSort); |
592 |
|
// we don't support subtyping for sets |
593 |
2 |
ASSERT_FALSE(setSortI.isComparableTo(setSortR)); |
594 |
2 |
ASSERT_FALSE(setSortI.isSubsortOf(setSortR)); |
595 |
2 |
ASSERT_FALSE(setSortR.isComparableTo(setSortI)); |
596 |
2 |
ASSERT_FALSE(setSortR.isSubsortOf(setSortI)); |
597 |
|
} |
598 |
|
|
599 |
65 |
TEST_F(TestApiBlackSort, sortScopedToString) |
600 |
|
{ |
601 |
4 |
std::string name = "uninterp-sort"; |
602 |
4 |
Sort bvsort8 = d_solver.mkBitVectorSort(8); |
603 |
4 |
Sort uninterp_sort = d_solver.mkUninterpretedSort(name); |
604 |
2 |
ASSERT_EQ(bvsort8.toString(), "(_ BitVec 8)"); |
605 |
2 |
ASSERT_EQ(uninterp_sort.toString(), name); |
606 |
4 |
Solver solver2; |
607 |
2 |
ASSERT_EQ(bvsort8.toString(), "(_ BitVec 8)"); |
608 |
2 |
ASSERT_EQ(uninterp_sort.toString(), name); |
609 |
|
} |
610 |
|
|
611 |
|
} // namespace test |
612 |
171 |
} // namespace cvc5 |