diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2019-02-11 09:04:54 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-02-11 09:04:54 -0800 |
commit | c86e0178bfaa662b6586d866c953a56f81cefe51 (patch) | |
tree | ac85369968820dbe825d0f8fd8c9920ed483a1b9 /test | |
parent | 104b28b4c16b90a819c8f79d60f94a42fb0c0261 (diff) |
New C++ API: Unit tests for declare* functions. (#2831)
Diffstat (limited to 'test')
-rw-r--r-- | test/unit/api/solver_black.h | 39 |
1 files changed, 39 insertions, 0 deletions
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index fcc68d981..169a9948d 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -76,7 +76,11 @@ class SolverBlack : public CxxTest::TestSuite void testMkUniverseSet(); void testMkVar(); + void testDeclareConst(); + void testDeclareDatatype(); void testDeclareFun(); + void testDeclareSort(); + void testDefineFun(); void testDefineFunRec(); void testDefineFunsRec(); @@ -733,6 +737,34 @@ void SolverBlack::testMkVar() TS_ASSERT_THROWS_NOTHING(d_solver->mkVar("", funSort)); } +void SolverBlack::testDeclareConst() +{ + Sort boolSort = d_solver->getBooleanSort(); + Sort intSort = d_solver->getIntegerSort(); + Sort funSort = d_solver->mkFunctionSort(intSort, boolSort); + TS_ASSERT_THROWS_NOTHING(d_solver->declareConst(std::string("b"), boolSort)); + TS_ASSERT_THROWS_NOTHING(d_solver->declareConst(std::string("i"), intSort)); + TS_ASSERT_THROWS_NOTHING(d_solver->declareConst("f", funSort)); + TS_ASSERT_THROWS_NOTHING(d_solver->declareConst("", funSort)); + TS_ASSERT_THROWS(d_solver->declareConst("a", Sort()), CVC4ApiException&); +} + +void SolverBlack::testDeclareDatatype() +{ + DatatypeConstructorDecl cons("cons"); + DatatypeConstructorDecl nil("nil"); + std::vector<DatatypeConstructorDecl> ctors1 = {nil}; + std::vector<DatatypeConstructorDecl> ctors2 = {cons, nil}; + std::vector<DatatypeConstructorDecl> ctors3; + TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string("a"), ctors1)); + TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string("b"), ctors2)); + TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string(""), ctors2)); + TS_ASSERT_THROWS(d_solver->declareDatatype(std::string("c"), ctors3), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->declareDatatype(std::string(""), ctors3), + CVC4ApiException&); +} + void SolverBlack::testDeclareFun() { Sort bvSort = d_solver->mkBitVectorSort(32); @@ -748,6 +780,13 @@ void SolverBlack::testDeclareFun() CVC4ApiException&); } +void SolverBlack::testDeclareSort() +{ + TS_ASSERT_THROWS_NOTHING(d_solver->declareSort("s", 0)); + TS_ASSERT_THROWS_NOTHING(d_solver->declareSort("s", 2)); + TS_ASSERT_THROWS_NOTHING(d_solver->declareSort("", 2)); +} + void SolverBlack::testDefineFun() { Sort bvSort = d_solver->mkBitVectorSort(32); |