GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/api/sort_black.cpp Lines: 370 370 100.0 %
Date: 2021-03-22 Branches: 1170 3524 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_FALSE(fun_sort.isFirstClass());
234
2
  ASSERT_NO_THROW(Sort().isFirstClass());
235
}
236
237
63
TEST_F(TestApiBlackSort, isFunctionLike)
238
{
239
4
  Sort fun_sort = d_solver.mkFunctionSort(d_solver.getRealSort(),
240
8
                                          d_solver.getIntegerSort());
241
2
  ASSERT_FALSE(d_solver.getIntegerSort().isFunctionLike());
242
2
  ASSERT_TRUE(fun_sort.isFunctionLike());
243
244
4
  Sort dt_sort = create_datatype_sort();
245
4
  Datatype dt = dt_sort.getDatatype();
246
4
  Sort cons_sort = dt[0][1].getSelectorTerm().getSort();
247
2
  ASSERT_TRUE(cons_sort.isFunctionLike());
248
249
2
  ASSERT_NO_THROW(Sort().isFunctionLike());
250
}
251
252
63
TEST_F(TestApiBlackSort, isSubsortOf)
253
{
254
2
  ASSERT_TRUE(d_solver.getIntegerSort().isSubsortOf(d_solver.getIntegerSort()));
255
2
  ASSERT_TRUE(d_solver.getIntegerSort().isSubsortOf(d_solver.getRealSort()));
256
2
  ASSERT_FALSE(
257
2
      d_solver.getIntegerSort().isSubsortOf(d_solver.getBooleanSort()));
258
2
  ASSERT_NO_THROW(Sort().isSubsortOf(Sort()));
259
}
260
261
63
TEST_F(TestApiBlackSort, isComparableTo)
262
{
263
2
  ASSERT_TRUE(
264
2
      d_solver.getIntegerSort().isComparableTo(d_solver.getIntegerSort()));
265
2
  ASSERT_TRUE(d_solver.getIntegerSort().isComparableTo(d_solver.getRealSort()));
266
2
  ASSERT_FALSE(
267
2
      d_solver.getIntegerSort().isComparableTo(d_solver.getBooleanSort()));
268
2
  ASSERT_NO_THROW(Sort().isComparableTo(Sort()));
269
}
270
271
63
TEST_F(TestApiBlackSort, getDatatype)
272
{
273
4
  Sort dtypeSort = create_datatype_sort();
274
2
  ASSERT_NO_THROW(dtypeSort.getDatatype());
275
  // create bv sort, check should fail
276
4
  Sort bvSort = d_solver.mkBitVectorSort(32);
277
4
  ASSERT_THROW(bvSort.getDatatype(), CVC4ApiException);
278
}
279
280
63
TEST_F(TestApiBlackSort, datatypeSorts)
281
{
282
4
  Sort intSort = d_solver.getIntegerSort();
283
4
  Sort dtypeSort = create_datatype_sort();
284
4
  Datatype dt = dtypeSort.getDatatype();
285
2
  ASSERT_FALSE(dtypeSort.isConstructor());
286
4
  ASSERT_THROW(dtypeSort.getConstructorCodomainSort(), CVC4ApiException);
287
4
  ASSERT_THROW(dtypeSort.getConstructorDomainSorts(), CVC4ApiException);
288
4
  ASSERT_THROW(dtypeSort.getConstructorArity(), CVC4ApiException);
289
290
  // get constructor
291
4
  DatatypeConstructor dcons = dt[0];
292
4
  Term consTerm = dcons.getConstructorTerm();
293
4
  Sort consSort = consTerm.getSort();
294
2
  ASSERT_TRUE(consSort.isConstructor());
295
2
  ASSERT_FALSE(consSort.isTester());
296
2
  ASSERT_FALSE(consSort.isSelector());
297
2
  ASSERT_EQ(consSort.getConstructorArity(), 2);
298
4
  std::vector<Sort> consDomSorts = consSort.getConstructorDomainSorts();
299
2
  ASSERT_EQ(consDomSorts[0], intSort);
300
2
  ASSERT_EQ(consDomSorts[1], dtypeSort);
301
2
  ASSERT_EQ(consSort.getConstructorCodomainSort(), dtypeSort);
302
303
  // get tester
304
4
  Term isConsTerm = dcons.getTesterTerm();
305
2
  ASSERT_TRUE(isConsTerm.getSort().isTester());
306
2
  ASSERT_EQ(isConsTerm.getSort().getTesterDomainSort(), dtypeSort);
307
4
  Sort booleanSort = d_solver.getBooleanSort();
308
2
  ASSERT_EQ(isConsTerm.getSort().getTesterCodomainSort(), booleanSort);
309
4
  ASSERT_THROW(booleanSort.getTesterDomainSort(), CVC4ApiException);
310
4
  ASSERT_THROW(booleanSort.getTesterCodomainSort(), CVC4ApiException);
311
312
  // get selector
313
4
  DatatypeSelector dselTail = dcons[1];
314
4
  Term tailTerm = dselTail.getSelectorTerm();
315
2
  ASSERT_TRUE(tailTerm.getSort().isSelector());
316
2
  ASSERT_EQ(tailTerm.getSort().getSelectorDomainSort(), dtypeSort);
317
2
  ASSERT_EQ(tailTerm.getSort().getSelectorCodomainSort(), dtypeSort);
318
4
  ASSERT_THROW(booleanSort.getSelectorDomainSort(), CVC4ApiException);
319
4
  ASSERT_THROW(booleanSort.getSelectorCodomainSort(), CVC4ApiException);
320
}
321
322
63
TEST_F(TestApiBlackSort, instantiate)
323
{
324
  // instantiate parametric datatype, check should not fail
325
4
  Sort paramDtypeSort = create_param_datatype_sort();
326
2
  ASSERT_NO_THROW(
327
      paramDtypeSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()}));
328
  // instantiate non-parametric datatype sort, check should fail
329
4
  DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
330
4
  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
331
2
  cons.addSelector("head", d_solver.getIntegerSort());
332
2
  dtypeSpec.addConstructor(cons);
333
4
  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
334
2
  dtypeSpec.addConstructor(nil);
335
4
  Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
336
4
  ASSERT_THROW(
337
      dtypeSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()}),
338
2
      CVC4ApiException);
339
}
340
341
63
TEST_F(TestApiBlackSort, getFunctionArity)
342
{
343
4
  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
344
8
                                         d_solver.getIntegerSort());
345
2
  ASSERT_NO_THROW(funSort.getFunctionArity());
346
4
  Sort bvSort = d_solver.mkBitVectorSort(32);
347
4
  ASSERT_THROW(bvSort.getFunctionArity(), CVC4ApiException);
348
}
349
350
63
TEST_F(TestApiBlackSort, getFunctionDomainSorts)
351
{
352
4
  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
353
8
                                         d_solver.getIntegerSort());
354
2
  ASSERT_NO_THROW(funSort.getFunctionDomainSorts());
355
4
  Sort bvSort = d_solver.mkBitVectorSort(32);
356
4
  ASSERT_THROW(bvSort.getFunctionDomainSorts(), CVC4ApiException);
357
}
358
359
63
TEST_F(TestApiBlackSort, getFunctionCodomainSort)
360
{
361
4
  Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
362
8
                                         d_solver.getIntegerSort());
363
2
  ASSERT_NO_THROW(funSort.getFunctionCodomainSort());
364
4
  Sort bvSort = d_solver.mkBitVectorSort(32);
365
4
  ASSERT_THROW(bvSort.getFunctionCodomainSort(), CVC4ApiException);
366
}
367
368
63
TEST_F(TestApiBlackSort, getArrayIndexSort)
369
{
370
4
  Sort elementSort = d_solver.mkBitVectorSort(32);
371
4
  Sort indexSort = d_solver.mkBitVectorSort(32);
372
4
  Sort arraySort = d_solver.mkArraySort(indexSort, elementSort);
373
2
  ASSERT_NO_THROW(arraySort.getArrayIndexSort());
374
4
  ASSERT_THROW(indexSort.getArrayIndexSort(), CVC4ApiException);
375
}
376
377
63
TEST_F(TestApiBlackSort, getArrayElementSort)
378
{
379
4
  Sort elementSort = d_solver.mkBitVectorSort(32);
380
4
  Sort indexSort = d_solver.mkBitVectorSort(32);
381
4
  Sort arraySort = d_solver.mkArraySort(indexSort, elementSort);
382
2
  ASSERT_NO_THROW(arraySort.getArrayElementSort());
383
4
  ASSERT_THROW(indexSort.getArrayElementSort(), CVC4ApiException);
384
}
385
386
63
TEST_F(TestApiBlackSort, getSetElementSort)
387
{
388
4
  Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
389
2
  ASSERT_NO_THROW(setSort.getSetElementSort());
390
4
  Sort elementSort = setSort.getSetElementSort();
391
2
  ASSERT_EQ(elementSort, d_solver.getIntegerSort());
392
4
  Sort bvSort = d_solver.mkBitVectorSort(32);
393
4
  ASSERT_THROW(bvSort.getSetElementSort(), CVC4ApiException);
394
}
395
396
63
TEST_F(TestApiBlackSort, getBagElementSort)
397
{
398
4
  Sort bagSort = d_solver.mkBagSort(d_solver.getIntegerSort());
399
2
  ASSERT_NO_THROW(bagSort.getBagElementSort());
400
4
  Sort elementSort = bagSort.getBagElementSort();
401
2
  ASSERT_EQ(elementSort, d_solver.getIntegerSort());
402
4
  Sort bvSort = d_solver.mkBitVectorSort(32);
403
4
  ASSERT_THROW(bvSort.getBagElementSort(), CVC4ApiException);
404
}
405
406
63
TEST_F(TestApiBlackSort, getSequenceElementSort)
407
{
408
4
  Sort seqSort = d_solver.mkSequenceSort(d_solver.getIntegerSort());
409
2
  ASSERT_TRUE(seqSort.isSequence());
410
2
  ASSERT_NO_THROW(seqSort.getSequenceElementSort());
411
4
  Sort bvSort = d_solver.mkBitVectorSort(32);
412
2
  ASSERT_FALSE(bvSort.isSequence());
413
4
  ASSERT_THROW(bvSort.getSequenceElementSort(), CVC4ApiException);
414
}
415
416
63
TEST_F(TestApiBlackSort, getUninterpretedSortName)
417
{
418
4
  Sort uSort = d_solver.mkUninterpretedSort("u");
419
2
  ASSERT_NO_THROW(uSort.getUninterpretedSortName());
420
4
  Sort bvSort = d_solver.mkBitVectorSort(32);
421
4
  ASSERT_THROW(bvSort.getUninterpretedSortName(), CVC4ApiException);
422
}
423
424
63
TEST_F(TestApiBlackSort, isUninterpretedSortParameterized)
425
{
426
4
  Sort uSort = d_solver.mkUninterpretedSort("u");
427
2
  ASSERT_FALSE(uSort.isUninterpretedSortParameterized());
428
4
  Sort sSort = d_solver.mkSortConstructorSort("s", 1);
429
4
  Sort siSort = sSort.instantiate({uSort});
430
2
  ASSERT_TRUE(siSort.isUninterpretedSortParameterized());
431
4
  Sort bvSort = d_solver.mkBitVectorSort(32);
432
4
  ASSERT_THROW(bvSort.isUninterpretedSortParameterized(), CVC4ApiException);
433
}
434
435
63
TEST_F(TestApiBlackSort, getUninterpretedSortParamSorts)
436
{
437
4
  Sort uSort = d_solver.mkUninterpretedSort("u");
438
2
  ASSERT_NO_THROW(uSort.getUninterpretedSortParamSorts());
439
4
  Sort sSort = d_solver.mkSortConstructorSort("s", 2);
440
4
  Sort siSort = sSort.instantiate({uSort, uSort});
441
2
  ASSERT_EQ(siSort.getUninterpretedSortParamSorts().size(), 2);
442
4
  Sort bvSort = d_solver.mkBitVectorSort(32);
443
4
  ASSERT_THROW(bvSort.getUninterpretedSortParamSorts(), CVC4ApiException);
444
}
445
446
63
TEST_F(TestApiBlackSort, getUninterpretedSortConstructorName)
447
{
448
4
  Sort sSort = d_solver.mkSortConstructorSort("s", 2);
449
2
  ASSERT_NO_THROW(sSort.getSortConstructorName());
450
4
  Sort bvSort = d_solver.mkBitVectorSort(32);
451
4
  ASSERT_THROW(bvSort.getSortConstructorName(), CVC4ApiException);
452
}
453
454
63
TEST_F(TestApiBlackSort, getUninterpretedSortConstructorArity)
455
{
456
4
  Sort sSort = d_solver.mkSortConstructorSort("s", 2);
457
2
  ASSERT_NO_THROW(sSort.getSortConstructorArity());
458
4
  Sort bvSort = d_solver.mkBitVectorSort(32);
459
4
  ASSERT_THROW(bvSort.getSortConstructorArity(), CVC4ApiException);
460
}
461
462
63
TEST_F(TestApiBlackSort, getBVSize)
463
{
464
4
  Sort bvSort = d_solver.mkBitVectorSort(32);
465
2
  ASSERT_NO_THROW(bvSort.getBVSize());
466
4
  Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
467
4
  ASSERT_THROW(setSort.getBVSize(), CVC4ApiException);
468
}
469
470
63
TEST_F(TestApiBlackSort, getFPExponentSize)
471
{
472
2
  if (CVC4::Configuration::isBuiltWithSymFPU())
473
  {
474
4
    Sort fpSort = d_solver.mkFloatingPointSort(4, 8);
475
2
    ASSERT_NO_THROW(fpSort.getFPExponentSize());
476
4
    Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
477
4
    ASSERT_THROW(setSort.getFPExponentSize(), CVC4ApiException);
478
  }
479
}
480
481
63
TEST_F(TestApiBlackSort, getFPSignificandSize)
482
{
483
2
  if (CVC4::Configuration::isBuiltWithSymFPU())
484
  {
485
4
    Sort fpSort = d_solver.mkFloatingPointSort(4, 8);
486
2
    ASSERT_NO_THROW(fpSort.getFPSignificandSize());
487
4
    Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
488
4
    ASSERT_THROW(setSort.getFPSignificandSize(), CVC4ApiException);
489
  }
490
}
491
492
63
TEST_F(TestApiBlackSort, getDatatypeParamSorts)
493
{
494
  // create parametric datatype, check should not fail
495
4
  Sort sort = d_solver.mkParamSort("T");
496
4
  DatatypeDecl paramDtypeSpec = d_solver.mkDatatypeDecl("paramlist", sort);
497
  DatatypeConstructorDecl paramCons =
498
4
      d_solver.mkDatatypeConstructorDecl("cons");
499
4
  DatatypeConstructorDecl paramNil = d_solver.mkDatatypeConstructorDecl("nil");
500
2
  paramCons.addSelector("head", sort);
501
2
  paramDtypeSpec.addConstructor(paramCons);
502
2
  paramDtypeSpec.addConstructor(paramNil);
503
4
  Sort paramDtypeSort = d_solver.mkDatatypeSort(paramDtypeSpec);
504
2
  ASSERT_NO_THROW(paramDtypeSort.getDatatypeParamSorts());
505
  // create non-parametric datatype sort, check should fail
506
4
  DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
507
4
  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
508
2
  cons.addSelector("head", d_solver.getIntegerSort());
509
2
  dtypeSpec.addConstructor(cons);
510
4
  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
511
2
  dtypeSpec.addConstructor(nil);
512
4
  Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
513
4
  ASSERT_THROW(dtypeSort.getDatatypeParamSorts(), CVC4ApiException);
514
}
515
516
63
TEST_F(TestApiBlackSort, getDatatypeArity)
517
{
518
  // create datatype sort, check should not 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
2
  ASSERT_NO_THROW(dtypeSort.getDatatypeArity());
527
  // create bv sort, check should fail
528
4
  Sort bvSort = d_solver.mkBitVectorSort(32);
529
4
  ASSERT_THROW(bvSort.getDatatypeArity(), CVC4ApiException);
530
}
531
532
63
TEST_F(TestApiBlackSort, getTupleLength)
533
{
534
  Sort tupleSort = d_solver.mkTupleSort(
535
4
      {d_solver.getIntegerSort(), d_solver.getIntegerSort()});
536
2
  ASSERT_NO_THROW(tupleSort.getTupleLength());
537
4
  Sort bvSort = d_solver.mkBitVectorSort(32);
538
4
  ASSERT_THROW(bvSort.getTupleLength(), CVC4ApiException);
539
}
540
541
63
TEST_F(TestApiBlackSort, getTupleSorts)
542
{
543
  Sort tupleSort = d_solver.mkTupleSort(
544
4
      {d_solver.getIntegerSort(), d_solver.getIntegerSort()});
545
2
  ASSERT_NO_THROW(tupleSort.getTupleSorts());
546
4
  Sort bvSort = d_solver.mkBitVectorSort(32);
547
4
  ASSERT_THROW(bvSort.getTupleSorts(), CVC4ApiException);
548
}
549
550
63
TEST_F(TestApiBlackSort, sortCompare)
551
{
552
4
  Sort boolSort = d_solver.getBooleanSort();
553
4
  Sort intSort = d_solver.getIntegerSort();
554
4
  Sort bvSort = d_solver.mkBitVectorSort(32);
555
4
  Sort bvSort2 = d_solver.mkBitVectorSort(32);
556
2
  ASSERT_TRUE(bvSort >= bvSort2);
557
2
  ASSERT_TRUE(bvSort <= bvSort2);
558
2
  ASSERT_TRUE((intSort > boolSort) != (intSort < boolSort));
559
2
  ASSERT_TRUE((intSort > bvSort || intSort == bvSort) == (intSort >= bvSort));
560
}
561
562
63
TEST_F(TestApiBlackSort, sortSubtyping)
563
{
564
4
  Sort intSort = d_solver.getIntegerSort();
565
4
  Sort realSort = d_solver.getRealSort();
566
2
  ASSERT_TRUE(intSort.isSubsortOf(realSort));
567
2
  ASSERT_FALSE(realSort.isSubsortOf(intSort));
568
2
  ASSERT_TRUE(intSort.isComparableTo(realSort));
569
2
  ASSERT_TRUE(realSort.isComparableTo(intSort));
570
571
4
  Sort arraySortII = d_solver.mkArraySort(intSort, intSort);
572
4
  Sort arraySortIR = d_solver.mkArraySort(intSort, realSort);
573
2
  ASSERT_FALSE(arraySortII.isComparableTo(intSort));
574
  // we do not support subtyping for arrays
575
2
  ASSERT_FALSE(arraySortII.isComparableTo(arraySortIR));
576
577
4
  Sort setSortI = d_solver.mkSetSort(intSort);
578
4
  Sort setSortR = d_solver.mkSetSort(realSort);
579
  // we don't support subtyping for sets
580
2
  ASSERT_FALSE(setSortI.isComparableTo(setSortR));
581
2
  ASSERT_FALSE(setSortI.isSubsortOf(setSortR));
582
2
  ASSERT_FALSE(setSortR.isComparableTo(setSortI));
583
2
  ASSERT_FALSE(setSortR.isSubsortOf(setSortI));
584
}
585
586
63
TEST_F(TestApiBlackSort, sortScopedToString)
587
{
588
4
  std::string name = "uninterp-sort";
589
4
  Sort bvsort8 = d_solver.mkBitVectorSort(8);
590
4
  Sort uninterp_sort = d_solver.mkUninterpretedSort(name);
591
2
  ASSERT_EQ(bvsort8.toString(), "(_ BitVec 8)");
592
2
  ASSERT_EQ(uninterp_sort.toString(), name);
593
4
  Solver solver2;
594
2
  ASSERT_EQ(bvsort8.toString(), "(_ BitVec 8)");
595
2
  ASSERT_EQ(uninterp_sort.toString(), name);
596
}
597
598
}  // namespace test
599
165
}  // namespace CVC4