diff options
Diffstat (limited to 'test/unit/api/solver_black.h')
-rw-r--r-- | test/unit/api/solver_black.h | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index ddff63352..4a7b74c8e 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -46,6 +46,7 @@ class SolverBlack : public CxxTest::TestSuite void testMkPredicateSort(); void testMkRecordSort(); void testMkSetSort(); + void testMkSequenceSort(); void testMkSortConstructorSort(); void testMkTupleSort(); void testMkUninterpretedSort(); @@ -56,6 +57,7 @@ class SolverBlack : public CxxTest::TestSuite void testMkConst(); void testMkConstArray(); void testMkEmptySet(); + void testMkEmptySequence(); void testMkFalse(); void testMkFloatingPoint(); void testMkNaN(); @@ -388,6 +390,17 @@ void SolverBlack::testMkSetSort() CVC4ApiException&); } +void SolverBlack::testMkSequenceSort() +{ + TS_ASSERT_THROWS_NOTHING( + d_solver->mkSequenceSort(d_solver->getBooleanSort())); + TS_ASSERT_THROWS_NOTHING(d_solver->mkSequenceSort( + d_solver->mkSequenceSort(d_solver->getIntegerSort()))); + Solver slv; + TS_ASSERT_THROWS(slv.mkSequenceSort(d_solver->getIntegerSort()), + CVC4ApiException&); +} + void SolverBlack::testMkUninterpretedSort() { TS_ASSERT_THROWS_NOTHING(d_solver->mkUninterpretedSort("u")); @@ -540,6 +553,16 @@ void SolverBlack::testMkEmptySet() TS_ASSERT_THROWS(slv.mkEmptySet(s), CVC4ApiException&); } +void SolverBlack::testMkEmptySequence() +{ + Solver slv; + Sort s = d_solver->mkSequenceSort(d_solver->getBooleanSort()); + TS_ASSERT_THROWS_NOTHING(d_solver->mkEmptySequence(s)); + TS_ASSERT_THROWS_NOTHING( + d_solver->mkEmptySequence(d_solver->getBooleanSort())); + TS_ASSERT_THROWS(slv.mkEmptySequence(s), CVC4ApiException&); +} + void SolverBlack::testMkFalse() { TS_ASSERT_THROWS_NOTHING(d_solver->mkFalse()); |