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