GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/api/sort_black.cpp Lines: 372 372 100.0 %
Date: 2021-03-23 Branches: 1176 3544 33.2 %

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