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