diff options
Diffstat (limited to 'test/unit/api')
-rw-r--r-- | test/unit/api/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/unit/api/opterm_black.h | 57 | ||||
-rw-r--r-- | test/unit/api/solver_black.h | 117 |
3 files changed, 175 insertions, 0 deletions
diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt index eeab46f99..8a6be70b9 100644 --- a/test/unit/api/CMakeLists.txt +++ b/test/unit/api/CMakeLists.txt @@ -4,3 +4,4 @@ cvc4_add_unit_test_black(solver_black api) cvc4_add_unit_test_black(sort_black api) cvc4_add_unit_test_black(term_black api) +cvc4_add_unit_test_black(opterm_black api) diff --git a/test/unit/api/opterm_black.h b/test/unit/api/opterm_black.h new file mode 100644 index 000000000..637301dd3 --- /dev/null +++ b/test/unit/api/opterm_black.h @@ -0,0 +1,57 @@ +/********************* */ +/*! \file opterm_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 Term class + **/ + +#include <cxxtest/TestSuite.h> + +#include "api/cvc4cpp.h" + +using namespace CVC4::api; + +class OpTermBlack : public CxxTest::TestSuite +{ + public: + void setUp() override {} + void tearDown() override {} + + void testGetKind(); + void testGetSort(); + void testIsNull(); + + private: + Solver d_solver; +}; + +void OpTermBlack::testGetKind() +{ + OpTerm x; + TS_ASSERT_THROWS(x.getSort(), CVC4ApiException&); + x = d_solver.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 1); + TS_ASSERT_THROWS_NOTHING(x.getKind()); +} + +void OpTermBlack::testGetSort() +{ + OpTerm x; + TS_ASSERT_THROWS(x.getSort(), CVC4ApiException&); + x = d_solver.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 1); + TS_ASSERT_THROWS_NOTHING(x.getSort()); +} + +void OpTermBlack::testIsNull() +{ + OpTerm x; + TS_ASSERT(x.isNull()); + x = d_solver.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 1); + TS_ASSERT(!x.isNull()); +} diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index 538899a0f..b0249b8a0 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -26,17 +26,34 @@ class SolverBlack : public CxxTest::TestSuite void setUp() override; void tearDown() override; + void testGetBooleanSort(); + void testGetIntegerSort(); + void testGetRealSort(); + void testGetRegExpSort(); + void testGetStringSort(); + void testGetRoundingmodeSort(); + + void testMkArraySort(); void testMkBitVectorSort(); void testMkFloatingPointSort(); void testMkDatatypeSort(); void testMkFunctionSort(); + void testMkParamSort(); void testMkPredicateSort(); + void testMkRecordSort(); + void testMkSetSort(); + void testMkSortConstructorSort(); + void testMkUninterpretedSort(); void testMkTupleSort(); + void testDeclareFun(); void testDefineFun(); void testDefineFunRec(); void testDefineFunsRec(); + void testMkRegexpEmpty(); + void testMkRegexpSigma(); + private: Solver d_solver; }; @@ -45,6 +62,53 @@ void SolverBlack::setUp() {} void SolverBlack::tearDown() {} +void SolverBlack::testGetBooleanSort() +{ + TS_ASSERT_THROWS_NOTHING(d_solver.getBooleanSort()); +} + +void SolverBlack::testGetIntegerSort() +{ + TS_ASSERT_THROWS_NOTHING(d_solver.getIntegerSort()); +} + +void SolverBlack::testGetRealSort() +{ + TS_ASSERT_THROWS_NOTHING(d_solver.getRealSort()); +} + +void SolverBlack::testGetRegExpSort() +{ + TS_ASSERT_THROWS_NOTHING(d_solver.getRegExpSort()); +} + +void SolverBlack::testGetStringSort() +{ + TS_ASSERT_THROWS_NOTHING(d_solver.getStringSort()); +} + +void SolverBlack::testGetRoundingmodeSort() +{ + TS_ASSERT_THROWS_NOTHING(d_solver.getRoundingmodeSort()); +} + +void SolverBlack::testMkArraySort() +{ + Sort boolSort = d_solver.getBooleanSort(); + Sort intSort = d_solver.getIntegerSort(); + Sort realSort = d_solver.getRealSort(); + Sort bvSort = d_solver.mkBitVectorSort(32); + Sort fpSort = d_solver.mkFloatingPointSort(3, 5); + TS_ASSERT_THROWS_NOTHING(d_solver.mkArraySort(boolSort, boolSort)); + TS_ASSERT_THROWS_NOTHING(d_solver.mkArraySort(intSort, intSort)); + TS_ASSERT_THROWS_NOTHING(d_solver.mkArraySort(realSort, realSort)); + TS_ASSERT_THROWS_NOTHING(d_solver.mkArraySort(bvSort, bvSort)); + TS_ASSERT_THROWS_NOTHING(d_solver.mkArraySort(fpSort, fpSort)); + TS_ASSERT_THROWS_NOTHING(d_solver.mkArraySort(boolSort, intSort)); + TS_ASSERT_THROWS_NOTHING(d_solver.mkArraySort(realSort, bvSort)); + TS_ASSERT_THROWS_NOTHING(d_solver.mkArraySort(bvSort, fpSort)); +} + void SolverBlack::testMkBitVectorSort() { TS_ASSERT_THROWS_NOTHING(d_solver.mkBitVectorSort(32)); @@ -97,6 +161,12 @@ void SolverBlack::testMkFunctionSort() CVC4ApiException&); } +void SolverBlack::testMkParamSort() +{ + TS_ASSERT_THROWS_NOTHING(d_solver.mkParamSort("T")); + TS_ASSERT_THROWS_NOTHING(d_solver.mkParamSort("")); +} + void SolverBlack::testMkPredicateSort() { TS_ASSERT_THROWS_NOTHING( @@ -109,6 +179,37 @@ void SolverBlack::testMkPredicateSort() CVC4ApiException&); } +void SolverBlack::testMkRecordSort() +{ + std::vector<std::pair<std::string, Sort>> fields = { + std::make_pair("b", d_solver.getBooleanSort()), + std::make_pair("bv", d_solver.mkBitVectorSort(8)), + std::make_pair("i", d_solver.getIntegerSort())}; + std::vector<std::pair<std::string, Sort>> empty; + TS_ASSERT_THROWS_NOTHING(d_solver.mkRecordSort(fields)); + TS_ASSERT_THROWS_NOTHING(d_solver.mkRecordSort(empty)); +} + +void SolverBlack::testMkSetSort() +{ + TS_ASSERT_THROWS_NOTHING(d_solver.mkSetSort(d_solver.getBooleanSort())); + TS_ASSERT_THROWS_NOTHING(d_solver.mkSetSort(d_solver.getIntegerSort())); + TS_ASSERT_THROWS_NOTHING(d_solver.mkSetSort(d_solver.mkBitVectorSort(4))); +} + +void SolverBlack::testMkUninterpretedSort() +{ + TS_ASSERT_THROWS_NOTHING(d_solver.mkUninterpretedSort("u")); + TS_ASSERT_THROWS_NOTHING(d_solver.mkUninterpretedSort("")); +} + +void SolverBlack::testMkSortConstructorSort() +{ + TS_ASSERT_THROWS_NOTHING(d_solver.mkSortConstructorSort("s", 2)); + TS_ASSERT_THROWS_NOTHING(d_solver.mkSortConstructorSort("", 2)); + TS_ASSERT_THROWS(d_solver.mkSortConstructorSort("", 0), CVC4ApiException&); +} + void SolverBlack::testMkTupleSort() { TS_ASSERT_THROWS_NOTHING(d_solver.mkTupleSort({d_solver.getIntegerSort()})); @@ -228,3 +329,19 @@ void SolverBlack::testDefineFunsRec() d_solver.defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v4}), CVC4ApiException&); } + +void SolverBlack::testMkRegexpEmpty() +{ + Sort strSort = d_solver.getStringSort(); + Term s = d_solver.mkVar("s", strSort); + TS_ASSERT_THROWS_NOTHING( + d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpEmpty())); +} + +void SolverBlack::testMkRegexpSigma() +{ + Sort strSort = d_solver.getStringSort(); + Term s = d_solver.mkVar("s", strSort); + TS_ASSERT_THROWS_NOTHING( + d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpSigma())); +} |