test/unit/api/cpp/sort_black.cpp

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