#-----------------------------------------------------------------------------#
# 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)
+++ /dev/null
-/********************* */
-/*! \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 <cxxtest/TestSuite.h>
-
-#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<Sort>{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<Sort>{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&);
-}
--- /dev/null
+/********************* */
+/*! \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 <cxxtest/TestSuite.h>
+
+#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&);
+}
--- /dev/null
+/********************* */
+/*! \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 <cxxtest/TestSuite.h>
+
+#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<Sort>{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<Sort>{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&);
+}
projects / cvc5.git / commitdiff