diff options
Diffstat (limited to 'test/unit/api/solver_black.h')
-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); |