From 0c1f01ec53885dc9c1fb600da0481ba7e1393df5 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Mon, 5 Nov 2018 09:43:29 -0800 Subject: [PATCH] New C++ API: Split unit tests. (#2688) --- test/unit/api/CMakeLists.txt | 3 +- test/unit/api/api_guards_black.h | 473 ------------------------------- test/unit/api/solver_black.h | 230 +++++++++++++++ test/unit/api/sort_black.h | 279 ++++++++++++++++++ 4 files changed, 511 insertions(+), 474 deletions(-) delete mode 100644 test/unit/api/api_guards_black.h create mode 100644 test/unit/api/solver_black.h create mode 100644 test/unit/api/sort_black.h diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt index 025575e41..eeab46f99 100644 --- a/test/unit/api/CMakeLists.txt +++ b/test/unit/api/CMakeLists.txt @@ -1,5 +1,6 @@ #-----------------------------------------------------------------------------# # Add unit tests -cvc4_add_unit_test_black(api_guards_black api) +cvc4_add_unit_test_black(solver_black api) +cvc4_add_unit_test_black(sort_black api) cvc4_add_unit_test_black(term_black api) diff --git a/test/unit/api/api_guards_black.h b/test/unit/api/api_guards_black.h deleted file mode 100644 index 777ce81f1..000000000 --- a/test/unit/api/api_guards_black.h +++ /dev/null @@ -1,473 +0,0 @@ -/********************* */ -/*! \file api_guards_black.h - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Black box testing of the guards of the C++ API functions. - ** - ** Black box testing of the guards of the C++ API functions. - **/ - -#include - -#include "api/cvc4cpp.h" - -using namespace CVC4::api; - -class ApiGuardsBlack : public CxxTest::TestSuite -{ - public: - void setUp() override; - void tearDown() override; - - void testSolverMkBitVectorSort(); - void testSolverMkFloatingPointSort(); - void testSolverMkDatatypeSort(); - void testSolverMkFunctionSort(); - void testSolverMkPredicateSort(); - void testSolverMkTupleSort(); - void testSortGetDatatype(); - void testSortInstantiate(); - void testSortGetFunctionArity(); - void testSortGetFunctionDomainSorts(); - void testSortGetFunctionCodomainSort(); - void testSortGetArrayIndexSort(); - void testSortGetArrayElementSort(); - void testSortGetSetElementSort(); - void testSortGetUninterpretedSortName(); - void testSortIsUninterpretedSortParameterized(); - void testSortGetUninterpretedSortParamSorts(); - void testSortGetUninterpretedSortConstructorName(); - void testSortGetUninterpretedSortConstructorArity(); - void testSortGetBVSize(); - void testSortGetFPExponentSize(); - void testSortGetFPSignificandSize(); - void testSortGetDatatypeParamSorts(); - void testSortGetDatatypeArity(); - void testSortGetTupleLength(); - void testSortGetTupleSorts(); - void testSolverDeclareFun(); - void testSolverDefineFun(); - void testSolverDefineFunRec(); - void testSolverDefineFunsRec(); - - private: - Solver d_solver; -}; - -void ApiGuardsBlack::setUp() {} - -void ApiGuardsBlack::tearDown() {} - -void ApiGuardsBlack::testSolverMkBitVectorSort() -{ - TS_ASSERT_THROWS_NOTHING(d_solver.mkBitVectorSort(32)); - TS_ASSERT_THROWS(d_solver.mkBitVectorSort(0), CVC4ApiException&); -} - -void ApiGuardsBlack::testSolverMkFloatingPointSort() -{ - TS_ASSERT_THROWS_NOTHING(d_solver.mkFloatingPointSort(4, 8)); - TS_ASSERT_THROWS(d_solver.mkFloatingPointSort(0, 8), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkFloatingPointSort(4, 0), CVC4ApiException&); -} - -void ApiGuardsBlack::testSolverMkDatatypeSort() -{ - DatatypeDecl dtypeSpec("list"); - DatatypeConstructorDecl cons("cons"); - DatatypeSelectorDecl head("head", d_solver.getIntegerSort()); - cons.addSelector(head); - dtypeSpec.addConstructor(cons); - DatatypeConstructorDecl nil("nil"); - dtypeSpec.addConstructor(nil); - TS_ASSERT_THROWS_NOTHING(d_solver.mkDatatypeSort(dtypeSpec)); - DatatypeDecl throwsDtypeSpec("list"); - TS_ASSERT_THROWS(d_solver.mkDatatypeSort(throwsDtypeSpec), CVC4ApiException&); -} - -void ApiGuardsBlack::testSolverMkFunctionSort() -{ - TS_ASSERT_THROWS_NOTHING(d_solver.mkFunctionSort( - d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort())); - Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), - d_solver.getIntegerSort()); - TS_ASSERT_THROWS(d_solver.mkFunctionSort(funSort, d_solver.getIntegerSort()), - CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkFunctionSort(d_solver.getIntegerSort(), funSort), - CVC4ApiException&); - TS_ASSERT_THROWS_NOTHING(d_solver.mkFunctionSort( - {d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort()}, - d_solver.getIntegerSort())); - Sort funSort2 = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), - d_solver.getIntegerSort()); - TS_ASSERT_THROWS( - d_solver.mkFunctionSort({funSort2, d_solver.mkUninterpretedSort("u")}, - d_solver.getIntegerSort()), - CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.mkFunctionSort({d_solver.getIntegerSort(), - d_solver.mkUninterpretedSort("u")}, - funSort2), - CVC4ApiException&); -} - -void ApiGuardsBlack::testSolverMkPredicateSort() -{ - TS_ASSERT_THROWS_NOTHING( - d_solver.mkPredicateSort({d_solver.getIntegerSort()})); - TS_ASSERT_THROWS(d_solver.mkPredicateSort({}), CVC4ApiException&); - Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), - d_solver.getIntegerSort()); - TS_ASSERT_THROWS( - d_solver.mkPredicateSort({d_solver.getIntegerSort(), funSort}), - CVC4ApiException&); -} - -void ApiGuardsBlack::testSolverMkTupleSort() -{ - TS_ASSERT_THROWS_NOTHING(d_solver.mkTupleSort({d_solver.getIntegerSort()})); - Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), - d_solver.getIntegerSort()); - TS_ASSERT_THROWS(d_solver.mkTupleSort({d_solver.getIntegerSort(), funSort}), - CVC4ApiException&); -} - -void ApiGuardsBlack::testSortGetDatatype() -{ - // create datatype sort, check should not fail - DatatypeDecl dtypeSpec("list"); - DatatypeConstructorDecl cons("cons"); - DatatypeSelectorDecl head("head", d_solver.getIntegerSort()); - cons.addSelector(head); - dtypeSpec.addConstructor(cons); - DatatypeConstructorDecl nil("nil"); - dtypeSpec.addConstructor(nil); - Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); - TS_ASSERT_THROWS_NOTHING(dtypeSort.getDatatype()); - // create bv sort, check should fail - Sort bvSort = d_solver.mkBitVectorSort(32); - TS_ASSERT_THROWS(bvSort.getDatatype(), CVC4ApiException&); -} - -void ApiGuardsBlack::testSortInstantiate() -{ - // instantiate parametric datatype, check should not fail - Sort sort = d_solver.mkParamSort("T"); - DatatypeDecl paramDtypeSpec("paramlist", sort); - DatatypeConstructorDecl paramCons("cons"); - DatatypeConstructorDecl paramNil("nil"); - DatatypeSelectorDecl paramHead("head", sort); - paramCons.addSelector(paramHead); - paramDtypeSpec.addConstructor(paramCons); - paramDtypeSpec.addConstructor(paramNil); - Sort paramDtypeSort = d_solver.mkDatatypeSort(paramDtypeSpec); - TS_ASSERT_THROWS_NOTHING( - paramDtypeSort.instantiate(std::vector{d_solver.getIntegerSort()})); - // instantiate non-parametric datatype sort, check should fail - DatatypeDecl dtypeSpec("list"); - DatatypeConstructorDecl cons("cons"); - DatatypeSelectorDecl head("head", d_solver.getIntegerSort()); - cons.addSelector(head); - dtypeSpec.addConstructor(cons); - DatatypeConstructorDecl nil("nil"); - dtypeSpec.addConstructor(nil); - Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); - TS_ASSERT_THROWS( - dtypeSort.instantiate(std::vector{d_solver.getIntegerSort()}), - CVC4ApiException&); -} - -void ApiGuardsBlack::testSortGetFunctionArity() -{ - Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), - d_solver.getIntegerSort()); - TS_ASSERT_THROWS_NOTHING(funSort.getFunctionArity()); - Sort bvSort = d_solver.mkBitVectorSort(32); - TS_ASSERT_THROWS(bvSort.getFunctionArity(), CVC4ApiException&); -} - -void ApiGuardsBlack::testSortGetFunctionDomainSorts() -{ - Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), - d_solver.getIntegerSort()); - TS_ASSERT_THROWS_NOTHING(funSort.getFunctionDomainSorts()); - Sort bvSort = d_solver.mkBitVectorSort(32); - TS_ASSERT_THROWS(bvSort.getFunctionDomainSorts(), CVC4ApiException&); -} - -void ApiGuardsBlack::testSortGetFunctionCodomainSort() -{ - Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), - d_solver.getIntegerSort()); - TS_ASSERT_THROWS_NOTHING(funSort.getFunctionCodomainSort()); - Sort bvSort = d_solver.mkBitVectorSort(32); - TS_ASSERT_THROWS(bvSort.getFunctionCodomainSort(), CVC4ApiException&); -} - -void ApiGuardsBlack::testSortGetArrayIndexSort() -{ - Sort elementSort = d_solver.mkBitVectorSort(32); - Sort indexSort = d_solver.mkBitVectorSort(32); - Sort arraySort = d_solver.mkArraySort(indexSort, elementSort); - TS_ASSERT_THROWS_NOTHING(arraySort.getArrayIndexSort()); - TS_ASSERT_THROWS(indexSort.getArrayIndexSort(), CVC4ApiException&); -} - -void ApiGuardsBlack::testSortGetArrayElementSort() -{ - Sort elementSort = d_solver.mkBitVectorSort(32); - Sort indexSort = d_solver.mkBitVectorSort(32); - Sort arraySort = d_solver.mkArraySort(indexSort, elementSort); - TS_ASSERT_THROWS_NOTHING(arraySort.getArrayElementSort()); - TS_ASSERT_THROWS(indexSort.getArrayElementSort(), CVC4ApiException&); -} - -void ApiGuardsBlack::testSortGetSetElementSort() -{ - Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); - TS_ASSERT_THROWS_NOTHING(setSort.getSetElementSort()); - Sort bvSort = d_solver.mkBitVectorSort(32); - TS_ASSERT_THROWS(bvSort.getSetElementSort(), CVC4ApiException&); -} - -void ApiGuardsBlack::testSortGetUninterpretedSortName() -{ - Sort uSort = d_solver.mkUninterpretedSort("u"); - TS_ASSERT_THROWS_NOTHING(uSort.getUninterpretedSortName()); - Sort bvSort = d_solver.mkBitVectorSort(32); - TS_ASSERT_THROWS(bvSort.getUninterpretedSortName(), CVC4ApiException&); -} - -void ApiGuardsBlack::testSortIsUninterpretedSortParameterized() -{ - Sort uSort = d_solver.mkUninterpretedSort("u"); - TS_ASSERT_THROWS_NOTHING(uSort.isUninterpretedSortParameterized()); - Sort bvSort = d_solver.mkBitVectorSort(32); - TS_ASSERT_THROWS(bvSort.isUninterpretedSortParameterized(), - CVC4ApiException&); -} - -void ApiGuardsBlack::testSortGetUninterpretedSortParamSorts() -{ - Sort uSort = d_solver.mkUninterpretedSort("u"); - TS_ASSERT_THROWS_NOTHING(uSort.getUninterpretedSortParamSorts()); - Sort bvSort = d_solver.mkBitVectorSort(32); - TS_ASSERT_THROWS(bvSort.getUninterpretedSortParamSorts(), CVC4ApiException&); -} - -void ApiGuardsBlack::testSortGetUninterpretedSortConstructorName() -{ - Sort sSort = d_solver.mkSortConstructorSort("s", 2); - TS_ASSERT_THROWS_NOTHING(sSort.getSortConstructorName()); - Sort bvSort = d_solver.mkBitVectorSort(32); - TS_ASSERT_THROWS(bvSort.getSortConstructorName(), CVC4ApiException&); -} - -void ApiGuardsBlack::testSortGetUninterpretedSortConstructorArity() -{ - Sort sSort = d_solver.mkSortConstructorSort("s", 2); - TS_ASSERT_THROWS_NOTHING(sSort.getSortConstructorArity()); - Sort bvSort = d_solver.mkBitVectorSort(32); - TS_ASSERT_THROWS(bvSort.getSortConstructorArity(), CVC4ApiException&); -} - -void ApiGuardsBlack::testSortGetBVSize() -{ - Sort bvSort = d_solver.mkBitVectorSort(32); - TS_ASSERT_THROWS_NOTHING(bvSort.getBVSize()); - Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); - TS_ASSERT_THROWS(setSort.getBVSize(), CVC4ApiException&); -} - -void ApiGuardsBlack::testSortGetFPExponentSize() -{ - Sort fpSort = d_solver.mkFloatingPointSort(4, 8); - TS_ASSERT_THROWS_NOTHING(fpSort.getFPExponentSize()); - Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); - TS_ASSERT_THROWS(setSort.getFPExponentSize(), CVC4ApiException&); -} - -void ApiGuardsBlack::testSortGetFPSignificandSize() -{ - Sort fpSort = d_solver.mkFloatingPointSort(4, 8); - TS_ASSERT_THROWS_NOTHING(fpSort.getFPSignificandSize()); - Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); - TS_ASSERT_THROWS(setSort.getFPSignificandSize(), CVC4ApiException&); -} - -void ApiGuardsBlack::testSortGetDatatypeParamSorts() -{ - // create parametric datatype, check should not fail - Sort sort = d_solver.mkParamSort("T"); - DatatypeDecl paramDtypeSpec("paramlist", sort); - DatatypeConstructorDecl paramCons("cons"); - DatatypeConstructorDecl paramNil("nil"); - DatatypeSelectorDecl paramHead("head", sort); - paramCons.addSelector(paramHead); - paramDtypeSpec.addConstructor(paramCons); - paramDtypeSpec.addConstructor(paramNil); - Sort paramDtypeSort = d_solver.mkDatatypeSort(paramDtypeSpec); - TS_ASSERT_THROWS_NOTHING(paramDtypeSort.getDatatypeParamSorts()); - // create non-parametric datatype sort, check should fail - DatatypeDecl dtypeSpec("list"); - DatatypeConstructorDecl cons("cons"); - DatatypeSelectorDecl head("head", d_solver.getIntegerSort()); - cons.addSelector(head); - dtypeSpec.addConstructor(cons); - DatatypeConstructorDecl nil("nil"); - dtypeSpec.addConstructor(nil); - Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); - TS_ASSERT_THROWS(dtypeSort.getDatatypeParamSorts(), CVC4ApiException&); -} - -void ApiGuardsBlack::testSortGetDatatypeArity() -{ - // create datatype sort, check should not fail - DatatypeDecl dtypeSpec("list"); - DatatypeConstructorDecl cons("cons"); - DatatypeSelectorDecl head("head", d_solver.getIntegerSort()); - cons.addSelector(head); - dtypeSpec.addConstructor(cons); - DatatypeConstructorDecl nil("nil"); - dtypeSpec.addConstructor(nil); - Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); - TS_ASSERT_THROWS_NOTHING(dtypeSort.getDatatypeArity()); - // create bv sort, check should fail - Sort bvSort = d_solver.mkBitVectorSort(32); - TS_ASSERT_THROWS(bvSort.getDatatypeArity(), CVC4ApiException&); -} - -void ApiGuardsBlack::testSortGetTupleLength() -{ - Sort tupleSort = d_solver.mkTupleSort( - {d_solver.getIntegerSort(), d_solver.getIntegerSort()}); - TS_ASSERT_THROWS_NOTHING(tupleSort.getTupleLength()); - Sort bvSort = d_solver.mkBitVectorSort(32); - TS_ASSERT_THROWS(bvSort.getTupleLength(), CVC4ApiException&); -} - -void ApiGuardsBlack::testSortGetTupleSorts() -{ - Sort tupleSort = d_solver.mkTupleSort( - {d_solver.getIntegerSort(), d_solver.getIntegerSort()}); - TS_ASSERT_THROWS_NOTHING(tupleSort.getTupleSorts()); - Sort bvSort = d_solver.mkBitVectorSort(32); - TS_ASSERT_THROWS(bvSort.getTupleSorts(), CVC4ApiException&); -} - -void ApiGuardsBlack::testSolverDeclareFun() -{ - Sort bvSort = d_solver.mkBitVectorSort(32); - Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), - d_solver.getIntegerSort()); - TS_ASSERT_THROWS_NOTHING(d_solver.declareFun("f1", bvSort)); - TS_ASSERT_THROWS_NOTHING(d_solver.declareFun("f2", funSort)); - TS_ASSERT_THROWS_NOTHING( - d_solver.declareFun("f3", {bvSort, d_solver.getIntegerSort()}, bvSort)); - TS_ASSERT_THROWS(d_solver.declareFun("f4", {bvSort, funSort}, bvSort), - CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.declareFun("f5", {bvSort, bvSort}, funSort), - CVC4ApiException&); -} - -void ApiGuardsBlack::testSolverDefineFun() -{ - Sort bvSort = d_solver.mkBitVectorSort(32); - Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort); - Sort funSort2 = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), - d_solver.getIntegerSort()); - Term b1 = d_solver.mkBoundVar("b1", bvSort); - Term b11 = d_solver.mkBoundVar("b1", bvSort); - Term b2 = d_solver.mkBoundVar("b2", d_solver.getIntegerSort()); - Term b3 = d_solver.mkBoundVar("b3", funSort2); - Term v1 = d_solver.mkBoundVar("v1", bvSort); - Term v2 = d_solver.mkBoundVar("v2", d_solver.getIntegerSort()); - Term v3 = d_solver.mkVar("v3", funSort2); - Term f1 = d_solver.declareFun("f1", funSort1); - Term f2 = d_solver.declareFun("f2", funSort2); - Term f3 = d_solver.declareFun("f3", bvSort); - TS_ASSERT_THROWS_NOTHING(d_solver.defineFun("f", {}, bvSort, v1)); - TS_ASSERT_THROWS_NOTHING(d_solver.defineFun("ff", {b1, b2}, bvSort, v1)); - TS_ASSERT_THROWS_NOTHING(d_solver.defineFun(f1, {b1, b11}, v1)); - TS_ASSERT_THROWS(d_solver.defineFun("fff", {b1}, bvSort, v3), - CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFun("ffff", {b1}, funSort2, v3), - CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFun("fffff", {b1, b3}, bvSort, v1), - CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFun(f1, {b1}, v1), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFun(f1, {b1, b11}, v2), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFun(f1, {b1, b11}, v3), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFun(f2, {b1}, v2), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFun(f3, {b1}, v1), CVC4ApiException&); -} - -void ApiGuardsBlack::testSolverDefineFunRec() -{ - Sort bvSort = d_solver.mkBitVectorSort(32); - Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort); - Sort funSort2 = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), - d_solver.getIntegerSort()); - Term b1 = d_solver.mkBoundVar("b1", bvSort); - Term b11 = d_solver.mkBoundVar("b1", bvSort); - Term b2 = d_solver.mkBoundVar("b2", d_solver.getIntegerSort()); - Term b3 = d_solver.mkBoundVar("b3", funSort2); - Term v1 = d_solver.mkBoundVar("v1", bvSort); - Term v2 = d_solver.mkBoundVar("v2", d_solver.getIntegerSort()); - Term v3 = d_solver.mkVar("v3", funSort2); - Term f1 = d_solver.declareFun("f1", funSort1); - Term f2 = d_solver.declareFun("f2", funSort2); - Term f3 = d_solver.declareFun("f3", bvSort); - TS_ASSERT_THROWS_NOTHING(d_solver.defineFunRec("f", {}, bvSort, v1)); - TS_ASSERT_THROWS_NOTHING(d_solver.defineFunRec("ff", {b1, b2}, bvSort, v1)); - TS_ASSERT_THROWS_NOTHING(d_solver.defineFunRec(f1, {b1, b11}, v1)); - TS_ASSERT_THROWS(d_solver.defineFunRec("fff", {b1}, bvSort, v3), - CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFunRec("ffff", {b1}, funSort2, v3), - CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFunRec("fffff", {b1, b3}, bvSort, v1), - CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFunRec(f1, {b1}, v1), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFunRec(f1, {b1, b11}, v2), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFunRec(f1, {b1, b11}, v3), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFunRec(f2, {b1}, v2), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFunRec(f3, {b1}, v1), CVC4ApiException&); -} - -void ApiGuardsBlack::testSolverDefineFunsRec() -{ - Sort uSort = d_solver.mkUninterpretedSort("u"); - Sort bvSort = d_solver.mkBitVectorSort(32); - Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort); - Sort funSort2 = d_solver.mkFunctionSort(uSort, d_solver.getIntegerSort()); - Term b1 = d_solver.mkBoundVar("b1", bvSort); - Term b11 = d_solver.mkBoundVar("b1", bvSort); - Term b2 = d_solver.mkBoundVar("b2", d_solver.getIntegerSort()); - Term b3 = d_solver.mkBoundVar("b3", funSort2); - Term b4 = d_solver.mkBoundVar("b4", uSort); - Term v1 = d_solver.mkBoundVar("v1", bvSort); - Term v2 = d_solver.mkBoundVar("v2", d_solver.getIntegerSort()); - Term v3 = d_solver.mkVar("v3", funSort2); - Term v4 = d_solver.mkVar("v4", uSort); - Term f1 = d_solver.declareFun("f1", funSort1); - Term f2 = d_solver.declareFun("f2", funSort2); - Term f3 = d_solver.declareFun("f3", bvSort); - TS_ASSERT_THROWS_NOTHING( - d_solver.defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v2})); - TS_ASSERT_THROWS( - d_solver.defineFunsRec({f1, f3}, {{b1, b11}, {b4}}, {v1, v2}), - CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFunsRec({f1, f2}, {{b1}, {b4}}, {v1, v2}), - CVC4ApiException&); - TS_ASSERT_THROWS(d_solver.defineFunsRec({f1, f2}, {{b1, b2}, {b4}}, {v1, v2}), - CVC4ApiException&); - TS_ASSERT_THROWS( - d_solver.defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v4}), - CVC4ApiException&); -} diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h new file mode 100644 index 000000000..538899a0f --- /dev/null +++ b/test/unit/api/solver_black.h @@ -0,0 +1,230 @@ +/********************* */ +/*! \file api_guards_black.h + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Black box testing of the guards of the C++ API functions. + ** + ** Black box testing of the guards of the C++ API functions. + **/ + +#include + +#include "api/cvc4cpp.h" + +using namespace CVC4::api; + +class SolverBlack : public CxxTest::TestSuite +{ + public: + void setUp() override; + void tearDown() override; + + void testMkBitVectorSort(); + void testMkFloatingPointSort(); + void testMkDatatypeSort(); + void testMkFunctionSort(); + void testMkPredicateSort(); + void testMkTupleSort(); + void testDeclareFun(); + void testDefineFun(); + void testDefineFunRec(); + void testDefineFunsRec(); + + private: + Solver d_solver; +}; + +void SolverBlack::setUp() {} + +void SolverBlack::tearDown() {} + +void SolverBlack::testMkBitVectorSort() +{ + TS_ASSERT_THROWS_NOTHING(d_solver.mkBitVectorSort(32)); + TS_ASSERT_THROWS(d_solver.mkBitVectorSort(0), CVC4ApiException&); +} + +void SolverBlack::testMkFloatingPointSort() +{ + TS_ASSERT_THROWS_NOTHING(d_solver.mkFloatingPointSort(4, 8)); + TS_ASSERT_THROWS(d_solver.mkFloatingPointSort(0, 8), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.mkFloatingPointSort(4, 0), CVC4ApiException&); +} + +void SolverBlack::testMkDatatypeSort() +{ + DatatypeDecl dtypeSpec("list"); + DatatypeConstructorDecl cons("cons"); + DatatypeSelectorDecl head("head", d_solver.getIntegerSort()); + cons.addSelector(head); + dtypeSpec.addConstructor(cons); + DatatypeConstructorDecl nil("nil"); + dtypeSpec.addConstructor(nil); + TS_ASSERT_THROWS_NOTHING(d_solver.mkDatatypeSort(dtypeSpec)); + DatatypeDecl throwsDtypeSpec("list"); + TS_ASSERT_THROWS(d_solver.mkDatatypeSort(throwsDtypeSpec), CVC4ApiException&); +} + +void SolverBlack::testMkFunctionSort() +{ + TS_ASSERT_THROWS_NOTHING(d_solver.mkFunctionSort( + d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort())); + Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), + d_solver.getIntegerSort()); + TS_ASSERT_THROWS(d_solver.mkFunctionSort(funSort, d_solver.getIntegerSort()), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.mkFunctionSort(d_solver.getIntegerSort(), funSort), + CVC4ApiException&); + TS_ASSERT_THROWS_NOTHING(d_solver.mkFunctionSort( + {d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort()}, + d_solver.getIntegerSort())); + Sort funSort2 = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), + d_solver.getIntegerSort()); + TS_ASSERT_THROWS( + d_solver.mkFunctionSort({funSort2, d_solver.mkUninterpretedSort("u")}, + d_solver.getIntegerSort()), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.mkFunctionSort({d_solver.getIntegerSort(), + d_solver.mkUninterpretedSort("u")}, + funSort2), + CVC4ApiException&); +} + +void SolverBlack::testMkPredicateSort() +{ + TS_ASSERT_THROWS_NOTHING( + d_solver.mkPredicateSort({d_solver.getIntegerSort()})); + TS_ASSERT_THROWS(d_solver.mkPredicateSort({}), CVC4ApiException&); + Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), + d_solver.getIntegerSort()); + TS_ASSERT_THROWS( + d_solver.mkPredicateSort({d_solver.getIntegerSort(), funSort}), + CVC4ApiException&); +} + +void SolverBlack::testMkTupleSort() +{ + TS_ASSERT_THROWS_NOTHING(d_solver.mkTupleSort({d_solver.getIntegerSort()})); + Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), + d_solver.getIntegerSort()); + TS_ASSERT_THROWS(d_solver.mkTupleSort({d_solver.getIntegerSort(), funSort}), + CVC4ApiException&); +} + +void SolverBlack::testDeclareFun() +{ + Sort bvSort = d_solver.mkBitVectorSort(32); + Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), + d_solver.getIntegerSort()); + TS_ASSERT_THROWS_NOTHING(d_solver.declareFun("f1", bvSort)); + TS_ASSERT_THROWS_NOTHING(d_solver.declareFun("f2", funSort)); + TS_ASSERT_THROWS_NOTHING( + d_solver.declareFun("f3", {bvSort, d_solver.getIntegerSort()}, bvSort)); + TS_ASSERT_THROWS(d_solver.declareFun("f4", {bvSort, funSort}, bvSort), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.declareFun("f5", {bvSort, bvSort}, funSort), + CVC4ApiException&); +} + +void SolverBlack::testDefineFun() +{ + Sort bvSort = d_solver.mkBitVectorSort(32); + Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort); + Sort funSort2 = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), + d_solver.getIntegerSort()); + Term b1 = d_solver.mkBoundVar("b1", bvSort); + Term b11 = d_solver.mkBoundVar("b1", bvSort); + Term b2 = d_solver.mkBoundVar("b2", d_solver.getIntegerSort()); + Term b3 = d_solver.mkBoundVar("b3", funSort2); + Term v1 = d_solver.mkBoundVar("v1", bvSort); + Term v2 = d_solver.mkBoundVar("v2", d_solver.getIntegerSort()); + Term v3 = d_solver.mkVar("v3", funSort2); + Term f1 = d_solver.declareFun("f1", funSort1); + Term f2 = d_solver.declareFun("f2", funSort2); + Term f3 = d_solver.declareFun("f3", bvSort); + TS_ASSERT_THROWS_NOTHING(d_solver.defineFun("f", {}, bvSort, v1)); + TS_ASSERT_THROWS_NOTHING(d_solver.defineFun("ff", {b1, b2}, bvSort, v1)); + TS_ASSERT_THROWS_NOTHING(d_solver.defineFun(f1, {b1, b11}, v1)); + TS_ASSERT_THROWS(d_solver.defineFun("fff", {b1}, bvSort, v3), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFun("ffff", {b1}, funSort2, v3), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFun("fffff", {b1, b3}, bvSort, v1), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFun(f1, {b1}, v1), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFun(f1, {b1, b11}, v2), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFun(f1, {b1, b11}, v3), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFun(f2, {b1}, v2), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFun(f3, {b1}, v1), CVC4ApiException&); +} + +void SolverBlack::testDefineFunRec() +{ + Sort bvSort = d_solver.mkBitVectorSort(32); + Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort); + Sort funSort2 = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), + d_solver.getIntegerSort()); + Term b1 = d_solver.mkBoundVar("b1", bvSort); + Term b11 = d_solver.mkBoundVar("b1", bvSort); + Term b2 = d_solver.mkBoundVar("b2", d_solver.getIntegerSort()); + Term b3 = d_solver.mkBoundVar("b3", funSort2); + Term v1 = d_solver.mkBoundVar("v1", bvSort); + Term v2 = d_solver.mkBoundVar("v2", d_solver.getIntegerSort()); + Term v3 = d_solver.mkVar("v3", funSort2); + Term f1 = d_solver.declareFun("f1", funSort1); + Term f2 = d_solver.declareFun("f2", funSort2); + Term f3 = d_solver.declareFun("f3", bvSort); + TS_ASSERT_THROWS_NOTHING(d_solver.defineFunRec("f", {}, bvSort, v1)); + TS_ASSERT_THROWS_NOTHING(d_solver.defineFunRec("ff", {b1, b2}, bvSort, v1)); + TS_ASSERT_THROWS_NOTHING(d_solver.defineFunRec(f1, {b1, b11}, v1)); + TS_ASSERT_THROWS(d_solver.defineFunRec("fff", {b1}, bvSort, v3), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFunRec("ffff", {b1}, funSort2, v3), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFunRec("fffff", {b1, b3}, bvSort, v1), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFunRec(f1, {b1}, v1), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFunRec(f1, {b1, b11}, v2), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFunRec(f1, {b1, b11}, v3), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFunRec(f2, {b1}, v2), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFunRec(f3, {b1}, v1), CVC4ApiException&); +} + +void SolverBlack::testDefineFunsRec() +{ + Sort uSort = d_solver.mkUninterpretedSort("u"); + Sort bvSort = d_solver.mkBitVectorSort(32); + Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort); + Sort funSort2 = d_solver.mkFunctionSort(uSort, d_solver.getIntegerSort()); + Term b1 = d_solver.mkBoundVar("b1", bvSort); + Term b11 = d_solver.mkBoundVar("b1", bvSort); + Term b2 = d_solver.mkBoundVar("b2", d_solver.getIntegerSort()); + Term b3 = d_solver.mkBoundVar("b3", funSort2); + Term b4 = d_solver.mkBoundVar("b4", uSort); + Term v1 = d_solver.mkBoundVar("v1", bvSort); + Term v2 = d_solver.mkBoundVar("v2", d_solver.getIntegerSort()); + Term v3 = d_solver.mkVar("v3", funSort2); + Term v4 = d_solver.mkVar("v4", uSort); + Term f1 = d_solver.declareFun("f1", funSort1); + Term f2 = d_solver.declareFun("f2", funSort2); + Term f3 = d_solver.declareFun("f3", bvSort); + TS_ASSERT_THROWS_NOTHING( + d_solver.defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v2})); + TS_ASSERT_THROWS( + d_solver.defineFunsRec({f1, f3}, {{b1, b11}, {b4}}, {v1, v2}), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFunsRec({f1, f2}, {{b1}, {b4}}, {v1, v2}), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver.defineFunsRec({f1, f2}, {{b1, b2}, {b4}}, {v1, v2}), + CVC4ApiException&); + TS_ASSERT_THROWS( + d_solver.defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v4}), + CVC4ApiException&); +} diff --git a/test/unit/api/sort_black.h b/test/unit/api/sort_black.h new file mode 100644 index 000000000..d9337e627 --- /dev/null +++ b/test/unit/api/sort_black.h @@ -0,0 +1,279 @@ +/********************* */ +/*! \file api_guards_black.h + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Black box testing of the guards of the C++ API functions. + ** + ** Black box testing of the guards of the C++ API functions. + **/ + +#include + +#include "api/cvc4cpp.h" + +using namespace CVC4::api; + +class SortBlack : public CxxTest::TestSuite +{ + public: + void setUp() override; + void tearDown() override; + + void testGetDatatype(); + void testInstantiate(); + void testGetFunctionArity(); + void testGetFunctionDomainSorts(); + void testGetFunctionCodomainSort(); + void testGetArrayIndexSort(); + void testGetArrayElementSort(); + void testGetSetElementSort(); + void testGetUninterpretedSortName(); + void testIsUninterpretedSortParameterized(); + void testGetUninterpretedSortParamSorts(); + void testGetUninterpretedSortConstructorName(); + void testGetUninterpretedSortConstructorArity(); + void testGetBVSize(); + void testGetFPExponentSize(); + void testGetFPSignificandSize(); + void testGetDatatypeParamSorts(); + void testGetDatatypeArity(); + void testGetTupleLength(); + void testGetTupleSorts(); + + private: + Solver d_solver; +}; + +void SortBlack::setUp() {} + +void SortBlack::tearDown() {} + +void SortBlack::testGetDatatype() +{ + // create datatype sort, check should not fail + DatatypeDecl dtypeSpec("list"); + DatatypeConstructorDecl cons("cons"); + DatatypeSelectorDecl head("head", d_solver.getIntegerSort()); + cons.addSelector(head); + dtypeSpec.addConstructor(cons); + DatatypeConstructorDecl nil("nil"); + dtypeSpec.addConstructor(nil); + Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); + TS_ASSERT_THROWS_NOTHING(dtypeSort.getDatatype()); + // create bv sort, check should fail + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS(bvSort.getDatatype(), CVC4ApiException&); +} + +void SortBlack::testInstantiate() +{ + // instantiate parametric datatype, check should not fail + Sort sort = d_solver.mkParamSort("T"); + DatatypeDecl paramDtypeSpec("paramlist", sort); + DatatypeConstructorDecl paramCons("cons"); + DatatypeConstructorDecl paramNil("nil"); + DatatypeSelectorDecl paramHead("head", sort); + paramCons.addSelector(paramHead); + paramDtypeSpec.addConstructor(paramCons); + paramDtypeSpec.addConstructor(paramNil); + Sort paramDtypeSort = d_solver.mkDatatypeSort(paramDtypeSpec); + TS_ASSERT_THROWS_NOTHING( + paramDtypeSort.instantiate(std::vector{d_solver.getIntegerSort()})); + // instantiate non-parametric datatype sort, check should fail + DatatypeDecl dtypeSpec("list"); + DatatypeConstructorDecl cons("cons"); + DatatypeSelectorDecl head("head", d_solver.getIntegerSort()); + cons.addSelector(head); + dtypeSpec.addConstructor(cons); + DatatypeConstructorDecl nil("nil"); + dtypeSpec.addConstructor(nil); + Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); + TS_ASSERT_THROWS( + dtypeSort.instantiate(std::vector{d_solver.getIntegerSort()}), + CVC4ApiException&); +} + +void SortBlack::testGetFunctionArity() +{ + Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), + d_solver.getIntegerSort()); + TS_ASSERT_THROWS_NOTHING(funSort.getFunctionArity()); + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS(bvSort.getFunctionArity(), CVC4ApiException&); +} + +void SortBlack::testGetFunctionDomainSorts() +{ + Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), + d_solver.getIntegerSort()); + TS_ASSERT_THROWS_NOTHING(funSort.getFunctionDomainSorts()); + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS(bvSort.getFunctionDomainSorts(), CVC4ApiException&); +} + +void SortBlack::testGetFunctionCodomainSort() +{ + Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), + d_solver.getIntegerSort()); + TS_ASSERT_THROWS_NOTHING(funSort.getFunctionCodomainSort()); + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS(bvSort.getFunctionCodomainSort(), CVC4ApiException&); +} + +void SortBlack::testGetArrayIndexSort() +{ + Sort elementSort = d_solver.mkBitVectorSort(32); + Sort indexSort = d_solver.mkBitVectorSort(32); + Sort arraySort = d_solver.mkArraySort(indexSort, elementSort); + TS_ASSERT_THROWS_NOTHING(arraySort.getArrayIndexSort()); + TS_ASSERT_THROWS(indexSort.getArrayIndexSort(), CVC4ApiException&); +} + +void SortBlack::testGetArrayElementSort() +{ + Sort elementSort = d_solver.mkBitVectorSort(32); + Sort indexSort = d_solver.mkBitVectorSort(32); + Sort arraySort = d_solver.mkArraySort(indexSort, elementSort); + TS_ASSERT_THROWS_NOTHING(arraySort.getArrayElementSort()); + TS_ASSERT_THROWS(indexSort.getArrayElementSort(), CVC4ApiException&); +} + +void SortBlack::testGetSetElementSort() +{ + Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); + TS_ASSERT_THROWS_NOTHING(setSort.getSetElementSort()); + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS(bvSort.getSetElementSort(), CVC4ApiException&); +} + +void SortBlack::testGetUninterpretedSortName() +{ + Sort uSort = d_solver.mkUninterpretedSort("u"); + TS_ASSERT_THROWS_NOTHING(uSort.getUninterpretedSortName()); + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS(bvSort.getUninterpretedSortName(), CVC4ApiException&); +} + +void SortBlack::testIsUninterpretedSortParameterized() +{ + Sort uSort = d_solver.mkUninterpretedSort("u"); + TS_ASSERT_THROWS_NOTHING(uSort.isUninterpretedSortParameterized()); + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS(bvSort.isUninterpretedSortParameterized(), + CVC4ApiException&); +} + +void SortBlack::testGetUninterpretedSortParamSorts() +{ + Sort uSort = d_solver.mkUninterpretedSort("u"); + TS_ASSERT_THROWS_NOTHING(uSort.getUninterpretedSortParamSorts()); + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS(bvSort.getUninterpretedSortParamSorts(), CVC4ApiException&); +} + +void SortBlack::testGetUninterpretedSortConstructorName() +{ + Sort sSort = d_solver.mkSortConstructorSort("s", 2); + TS_ASSERT_THROWS_NOTHING(sSort.getSortConstructorName()); + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS(bvSort.getSortConstructorName(), CVC4ApiException&); +} + +void SortBlack::testGetUninterpretedSortConstructorArity() +{ + Sort sSort = d_solver.mkSortConstructorSort("s", 2); + TS_ASSERT_THROWS_NOTHING(sSort.getSortConstructorArity()); + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS(bvSort.getSortConstructorArity(), CVC4ApiException&); +} + +void SortBlack::testGetBVSize() +{ + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS_NOTHING(bvSort.getBVSize()); + Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); + TS_ASSERT_THROWS(setSort.getBVSize(), CVC4ApiException&); +} + +void SortBlack::testGetFPExponentSize() +{ + Sort fpSort = d_solver.mkFloatingPointSort(4, 8); + TS_ASSERT_THROWS_NOTHING(fpSort.getFPExponentSize()); + Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); + TS_ASSERT_THROWS(setSort.getFPExponentSize(), CVC4ApiException&); +} + +void SortBlack::testGetFPSignificandSize() +{ + Sort fpSort = d_solver.mkFloatingPointSort(4, 8); + TS_ASSERT_THROWS_NOTHING(fpSort.getFPSignificandSize()); + Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); + TS_ASSERT_THROWS(setSort.getFPSignificandSize(), CVC4ApiException&); +} + +void SortBlack::testGetDatatypeParamSorts() +{ + // create parametric datatype, check should not fail + Sort sort = d_solver.mkParamSort("T"); + DatatypeDecl paramDtypeSpec("paramlist", sort); + DatatypeConstructorDecl paramCons("cons"); + DatatypeConstructorDecl paramNil("nil"); + DatatypeSelectorDecl paramHead("head", sort); + paramCons.addSelector(paramHead); + paramDtypeSpec.addConstructor(paramCons); + paramDtypeSpec.addConstructor(paramNil); + Sort paramDtypeSort = d_solver.mkDatatypeSort(paramDtypeSpec); + TS_ASSERT_THROWS_NOTHING(paramDtypeSort.getDatatypeParamSorts()); + // create non-parametric datatype sort, check should fail + DatatypeDecl dtypeSpec("list"); + DatatypeConstructorDecl cons("cons"); + DatatypeSelectorDecl head("head", d_solver.getIntegerSort()); + cons.addSelector(head); + dtypeSpec.addConstructor(cons); + DatatypeConstructorDecl nil("nil"); + dtypeSpec.addConstructor(nil); + Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); + TS_ASSERT_THROWS(dtypeSort.getDatatypeParamSorts(), CVC4ApiException&); +} + +void SortBlack::testGetDatatypeArity() +{ + // create datatype sort, check should not fail + DatatypeDecl dtypeSpec("list"); + DatatypeConstructorDecl cons("cons"); + DatatypeSelectorDecl head("head", d_solver.getIntegerSort()); + cons.addSelector(head); + dtypeSpec.addConstructor(cons); + DatatypeConstructorDecl nil("nil"); + dtypeSpec.addConstructor(nil); + Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); + TS_ASSERT_THROWS_NOTHING(dtypeSort.getDatatypeArity()); + // create bv sort, check should fail + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS(bvSort.getDatatypeArity(), CVC4ApiException&); +} + +void SortBlack::testGetTupleLength() +{ + Sort tupleSort = d_solver.mkTupleSort( + {d_solver.getIntegerSort(), d_solver.getIntegerSort()}); + TS_ASSERT_THROWS_NOTHING(tupleSort.getTupleLength()); + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS(bvSort.getTupleLength(), CVC4ApiException&); +} + +void SortBlack::testGetTupleSorts() +{ + Sort tupleSort = d_solver.mkTupleSort( + {d_solver.getIntegerSort(), d_solver.getIntegerSort()}); + TS_ASSERT_THROWS_NOTHING(tupleSort.getTupleSorts()); + Sort bvSort = d_solver.mkBitVectorSort(32); + TS_ASSERT_THROWS(bvSort.getTupleSorts(), CVC4ApiException&); +} -- 2.30.2