test/unit/api/sort_black.h

   1 /*********************                                                        */
   2 /*! \file sort_black.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Aina Niemetz
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 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 <cxxtest/TestSuite.h>
  18
  19 #include "api/cvc4cpp.h"
  20
  21 using namespace CVC4::api;
  22
  23 class SortBlack : public CxxTest::TestSuite
  24 {
  25  public:
  26   void setUp() override;
  27   void tearDown() override;
  28
  29   void testGetDatatype();
  30   void testDatatypeSorts();
  31   void testInstantiate();
  32   void testGetFunctionArity();
  33   void testGetFunctionDomainSorts();
  34   void testGetFunctionCodomainSort();
  35   void testGetArrayIndexSort();
  36   void testGetArrayElementSort();
  37   void testGetSetElementSort();
  38   void testGetUninterpretedSortName();
  39   void testIsUninterpretedSortParameterized();
  40   void testGetUninterpretedSortParamSorts();
  41   void testGetUninterpretedSortConstructorName();
  42   void testGetUninterpretedSortConstructorArity();
  43   void testGetBVSize();
  44   void testGetFPExponentSize();
  45   void testGetFPSignificandSize();
  46   void testGetDatatypeParamSorts();
  47   void testGetDatatypeArity();
  48   void testGetTupleLength();
  49   void testGetTupleSorts();
  50
  51   void testSortCompare();
  52   void testSortSubtyping();
  53
  54  private:
  55   Solver d_solver;
  56 };
  57
  58 void SortBlack::setUp() {}
  59
  60 void SortBlack::tearDown() {}
  61
  62 void SortBlack::testGetDatatype()
  63 {
  64   // create datatype sort, check should not fail
  65   DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
  66   DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
  67   cons.addSelector("head", d_solver.getIntegerSort());
  68   dtypeSpec.addConstructor(cons);
  69   DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
  70   dtypeSpec.addConstructor(nil);
  71   Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
  72   TS_ASSERT_THROWS_NOTHING(dtypeSort.getDatatype());
  73   // create bv sort, check should fail
  74   Sort bvSort = d_solver.mkBitVectorSort(32);
  75   TS_ASSERT_THROWS(bvSort.getDatatype(), CVC4ApiException&);
  76 }
  77
  78 void SortBlack::testDatatypeSorts()
  79 {
  80   Sort intSort = d_solver.getIntegerSort();
  81   // create datatype sort to test
  82   DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
  83   DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
  84   cons.addSelector("head", intSort);
  85   cons.addSelectorSelf("tail");
  86   dtypeSpec.addConstructor(cons);
  87   DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
  88   dtypeSpec.addConstructor(nil);
  89   Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
  90   Datatype dt = dtypeSort.getDatatype();
  91   TS_ASSERT(!dtypeSort.isConstructor());
  92   TS_ASSERT_THROWS(dtypeSort.getConstructorCodomainSort(), CVC4ApiException&);
  93   TS_ASSERT_THROWS(dtypeSort.getConstructorDomainSorts(), CVC4ApiException&);
  94   TS_ASSERT_THROWS(dtypeSort.getConstructorArity(), CVC4ApiException&);
  95
  96   // get constructor
  97   DatatypeConstructor dcons = dt[0];
  98   Term consTerm = dcons.getConstructorTerm();
  99   Sort consSort = consTerm.getSort();
 100   TS_ASSERT(consSort.isConstructor());
 101   TS_ASSERT(!consSort.isTester());
 102   TS_ASSERT(!consSort.isSelector());
 103   TS_ASSERT(consSort.getConstructorArity() == 2);
 104   std::vector<Sort> consDomSorts = consSort.getConstructorDomainSorts();
 105   TS_ASSERT(consDomSorts[0] == intSort);
 106   TS_ASSERT(consDomSorts[1] == dtypeSort);
 107   TS_ASSERT(consSort.getConstructorCodomainSort() == dtypeSort);
 108
 109   // get tester
 110   Term isConsTerm = dcons.getTesterTerm();
 111   TS_ASSERT(isConsTerm.getSort().isTester());
 112
 113   // get selector
 114   DatatypeSelector dselTail = dcons[1];
 115   Term tailTerm = dselTail.getSelectorTerm();
 116   TS_ASSERT(tailTerm.getSort().isSelector());
 117 }
 118
 119 void SortBlack::testInstantiate()
 120 {
 121   // instantiate parametric datatype, check should not fail
 122   Sort sort = d_solver.mkParamSort("T");
 123   DatatypeDecl paramDtypeSpec = d_solver.mkDatatypeDecl("paramlist", sort);
 124   DatatypeConstructorDecl paramCons =
 125       d_solver.mkDatatypeConstructorDecl("cons");
 126   DatatypeConstructorDecl paramNil = d_solver.mkDatatypeConstructorDecl("nil");
 127   paramCons.addSelector("head", sort);
 128   paramDtypeSpec.addConstructor(paramCons);
 129   paramDtypeSpec.addConstructor(paramNil);
 130   Sort paramDtypeSort = d_solver.mkDatatypeSort(paramDtypeSpec);
 131   TS_ASSERT_THROWS_NOTHING(
 132       paramDtypeSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()}));
 133   // instantiate non-parametric datatype sort, check should fail
 134   DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
 135   DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
 136   cons.addSelector("head", d_solver.getIntegerSort());
 137   dtypeSpec.addConstructor(cons);
 138   DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
 139   dtypeSpec.addConstructor(nil);
 140   Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
 141   TS_ASSERT_THROWS(
 142       dtypeSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()}),
 143       CVC4ApiException&);
 144 }
 145
 146 void SortBlack::testGetFunctionArity()
 147 {
 148   Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
 149                                          d_solver.getIntegerSort());
 150   TS_ASSERT_THROWS_NOTHING(funSort.getFunctionArity());
 151   Sort bvSort = d_solver.mkBitVectorSort(32);
 152   TS_ASSERT_THROWS(bvSort.getFunctionArity(), CVC4ApiException&);
 153 }
 154
 155 void SortBlack::testGetFunctionDomainSorts()
 156 {
 157   Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
 158                                          d_solver.getIntegerSort());
 159   TS_ASSERT_THROWS_NOTHING(funSort.getFunctionDomainSorts());
 160   Sort bvSort = d_solver.mkBitVectorSort(32);
 161   TS_ASSERT_THROWS(bvSort.getFunctionDomainSorts(), CVC4ApiException&);
 162 }
 163
 164 void SortBlack::testGetFunctionCodomainSort()
 165 {
 166   Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
 167                                          d_solver.getIntegerSort());
 168   TS_ASSERT_THROWS_NOTHING(funSort.getFunctionCodomainSort());
 169   Sort bvSort = d_solver.mkBitVectorSort(32);
 170   TS_ASSERT_THROWS(bvSort.getFunctionCodomainSort(), CVC4ApiException&);
 171 }
 172
 173 void SortBlack::testGetArrayIndexSort()
 174 {
 175   Sort elementSort = d_solver.mkBitVectorSort(32);
 176   Sort indexSort = d_solver.mkBitVectorSort(32);
 177   Sort arraySort = d_solver.mkArraySort(indexSort, elementSort);
 178   TS_ASSERT_THROWS_NOTHING(arraySort.getArrayIndexSort());
 179   TS_ASSERT_THROWS(indexSort.getArrayIndexSort(), CVC4ApiException&);
 180 }
 181
 182 void SortBlack::testGetArrayElementSort()
 183 {
 184   Sort elementSort = d_solver.mkBitVectorSort(32);
 185   Sort indexSort = d_solver.mkBitVectorSort(32);
 186   Sort arraySort = d_solver.mkArraySort(indexSort, elementSort);
 187   TS_ASSERT_THROWS_NOTHING(arraySort.getArrayElementSort());
 188   TS_ASSERT_THROWS(indexSort.getArrayElementSort(), CVC4ApiException&);
 189 }
 190
 191 void SortBlack::testGetSetElementSort()
 192 {
 193   Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
 194   TS_ASSERT_THROWS_NOTHING(setSort.getSetElementSort());
 195   Sort bvSort = d_solver.mkBitVectorSort(32);
 196   TS_ASSERT_THROWS(bvSort.getSetElementSort(), CVC4ApiException&);
 197 }
 198
 199 void SortBlack::testGetUninterpretedSortName()
 200 {
 201   Sort uSort = d_solver.mkUninterpretedSort("u");
 202   TS_ASSERT_THROWS_NOTHING(uSort.getUninterpretedSortName());
 203   Sort bvSort = d_solver.mkBitVectorSort(32);
 204   TS_ASSERT_THROWS(bvSort.getUninterpretedSortName(), CVC4ApiException&);
 205 }
 206
 207 void SortBlack::testIsUninterpretedSortParameterized()
 208 {
 209   Sort uSort = d_solver.mkUninterpretedSort("u");
 210   TS_ASSERT_THROWS_NOTHING(uSort.isUninterpretedSortParameterized());
 211   Sort bvSort = d_solver.mkBitVectorSort(32);
 212   TS_ASSERT_THROWS(bvSort.isUninterpretedSortParameterized(),
 213                    CVC4ApiException&);
 214 }
 215
 216 void SortBlack::testGetUninterpretedSortParamSorts()
 217 {
 218   Sort uSort = d_solver.mkUninterpretedSort("u");
 219   TS_ASSERT_THROWS_NOTHING(uSort.getUninterpretedSortParamSorts());
 220   Sort bvSort = d_solver.mkBitVectorSort(32);
 221   TS_ASSERT_THROWS(bvSort.getUninterpretedSortParamSorts(), CVC4ApiException&);
 222 }
 223
 224 void SortBlack::testGetUninterpretedSortConstructorName()
 225 {
 226   Sort sSort = d_solver.mkSortConstructorSort("s", 2);
 227   TS_ASSERT_THROWS_NOTHING(sSort.getSortConstructorName());
 228   Sort bvSort = d_solver.mkBitVectorSort(32);
 229   TS_ASSERT_THROWS(bvSort.getSortConstructorName(), CVC4ApiException&);
 230 }
 231
 232 void SortBlack::testGetUninterpretedSortConstructorArity()
 233 {
 234   Sort sSort = d_solver.mkSortConstructorSort("s", 2);
 235   TS_ASSERT_THROWS_NOTHING(sSort.getSortConstructorArity());
 236   Sort bvSort = d_solver.mkBitVectorSort(32);
 237   TS_ASSERT_THROWS(bvSort.getSortConstructorArity(), CVC4ApiException&);
 238 }
 239
 240 void SortBlack::testGetBVSize()
 241 {
 242   Sort bvSort = d_solver.mkBitVectorSort(32);
 243   TS_ASSERT_THROWS_NOTHING(bvSort.getBVSize());
 244   Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
 245   TS_ASSERT_THROWS(setSort.getBVSize(), CVC4ApiException&);
 246 }
 247
 248 void SortBlack::testGetFPExponentSize()
 249 {
 250   Sort fpSort = d_solver.mkFloatingPointSort(4, 8);
 251   TS_ASSERT_THROWS_NOTHING(fpSort.getFPExponentSize());
 252   Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
 253   TS_ASSERT_THROWS(setSort.getFPExponentSize(), CVC4ApiException&);
 254 }
 255
 256 void SortBlack::testGetFPSignificandSize()
 257 {
 258   Sort fpSort = d_solver.mkFloatingPointSort(4, 8);
 259   TS_ASSERT_THROWS_NOTHING(fpSort.getFPSignificandSize());
 260   Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
 261   TS_ASSERT_THROWS(setSort.getFPSignificandSize(), CVC4ApiException&);
 262 }
 263
 264 void SortBlack::testGetDatatypeParamSorts()
 265 {
 266   // create parametric datatype, check should not fail
 267   Sort sort = d_solver.mkParamSort("T");
 268   DatatypeDecl paramDtypeSpec = d_solver.mkDatatypeDecl("paramlist", sort);
 269   DatatypeConstructorDecl paramCons =
 270       d_solver.mkDatatypeConstructorDecl("cons");
 271   DatatypeConstructorDecl paramNil = d_solver.mkDatatypeConstructorDecl("nil");
 272   paramCons.addSelector("head", sort);
 273   paramDtypeSpec.addConstructor(paramCons);
 274   paramDtypeSpec.addConstructor(paramNil);
 275   Sort paramDtypeSort = d_solver.mkDatatypeSort(paramDtypeSpec);
 276   TS_ASSERT_THROWS_NOTHING(paramDtypeSort.getDatatypeParamSorts());
 277   // create non-parametric datatype sort, check should fail
 278   DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
 279   DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
 280   cons.addSelector("head", d_solver.getIntegerSort());
 281   dtypeSpec.addConstructor(cons);
 282   DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
 283   dtypeSpec.addConstructor(nil);
 284   Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
 285   TS_ASSERT_THROWS(dtypeSort.getDatatypeParamSorts(), CVC4ApiException&);
 286 }
 287
 288 void SortBlack::testGetDatatypeArity()
 289 {
 290   // create datatype sort, check should not fail
 291   DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
 292   DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
 293   cons.addSelector("head", d_solver.getIntegerSort());
 294   dtypeSpec.addConstructor(cons);
 295   DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
 296   dtypeSpec.addConstructor(nil);
 297   Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
 298   TS_ASSERT_THROWS_NOTHING(dtypeSort.getDatatypeArity());
 299   // create bv sort, check should fail
 300   Sort bvSort = d_solver.mkBitVectorSort(32);
 301   TS_ASSERT_THROWS(bvSort.getDatatypeArity(), CVC4ApiException&);
 302 }
 303
 304 void SortBlack::testGetTupleLength()
 305 {
 306   Sort tupleSort = d_solver.mkTupleSort(
 307       {d_solver.getIntegerSort(), d_solver.getIntegerSort()});
 308   TS_ASSERT_THROWS_NOTHING(tupleSort.getTupleLength());
 309   Sort bvSort = d_solver.mkBitVectorSort(32);
 310   TS_ASSERT_THROWS(bvSort.getTupleLength(), CVC4ApiException&);
 311 }
 312
 313 void SortBlack::testGetTupleSorts()
 314 {
 315   Sort tupleSort = d_solver.mkTupleSort(
 316       {d_solver.getIntegerSort(), d_solver.getIntegerSort()});
 317   TS_ASSERT_THROWS_NOTHING(tupleSort.getTupleSorts());
 318   Sort bvSort = d_solver.mkBitVectorSort(32);
 319   TS_ASSERT_THROWS(bvSort.getTupleSorts(), CVC4ApiException&);
 320 }
 321
 322 void SortBlack::testSortCompare()
 323 {
 324   Sort boolSort = d_solver.getBooleanSort();
 325   Sort intSort = d_solver.getIntegerSort();
 326   Sort bvSort = d_solver.mkBitVectorSort(32);
 327   Sort bvSort2 = d_solver.mkBitVectorSort(32);
 328   TS_ASSERT(bvSort >= bvSort2);
 329   TS_ASSERT(bvSort <= bvSort2);
 330   TS_ASSERT((intSort > boolSort) != (intSort < boolSort));
 331   TS_ASSERT((intSort > bvSort || intSort == bvSort) == (intSort >= bvSort));
 332 }
 333
 334 void SortBlack::testSortSubtyping()
 335 {
 336   Sort intSort = d_solver.getIntegerSort();
 337   Sort realSort = d_solver.getRealSort();
 338   TS_ASSERT(intSort.isSubsortOf(realSort));
 339   TS_ASSERT(!realSort.isSubsortOf(intSort));
 340   TS_ASSERT(intSort.isComparableTo(realSort));
 341   TS_ASSERT(realSort.isComparableTo(intSort));
 342
 343   Sort arraySortII = d_solver.mkArraySort(intSort, intSort);
 344   Sort arraySortIR = d_solver.mkArraySort(intSort, realSort);
 345   TS_ASSERT(!arraySortII.isComparableTo(intSort));
 346   // we do not support subtyping for arrays
 347   TS_ASSERT(!arraySortII.isComparableTo(arraySortIR));
 348
 349   Sort setSortI = d_solver.mkSetSort(intSort);
 350   Sort setSortR = d_solver.mkSetSort(realSort);
 351   // we support subtyping for sets
 352   TS_ASSERT(setSortI.isSubsortOf(setSortR));
 353   TS_ASSERT(setSortR.isComparableTo(setSortI));
 354 }