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 7861bf7ae..8a4d878ef 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -48,6 +48,7 @@ class SolverBlack : public CxxTest::TestSuite void testMkPredicateSort(); void testMkRecordSort(); void testMkSetSort(); + void testMkBagSort(); void testMkSequenceSort(); void testMkSortConstructorSort(); void testMkTupleSort(); @@ -59,6 +60,7 @@ class SolverBlack : public CxxTest::TestSuite void testMkConst(); void testMkConstArray(); void testMkEmptySet(); + void testMkEmptyBag(); void testMkEmptySequence(); void testMkFalse(); void testMkFloatingPoint(); @@ -425,6 +427,16 @@ void SolverBlack::testMkSetSort() CVC4ApiException&); } +void SolverBlack::testMkBagSort() +{ + TS_ASSERT_THROWS_NOTHING(d_solver->mkBagSort(d_solver->getBooleanSort())); + TS_ASSERT_THROWS_NOTHING(d_solver->mkBagSort(d_solver->getIntegerSort())); + TS_ASSERT_THROWS_NOTHING(d_solver->mkBagSort(d_solver->mkBitVectorSort(4))); + Solver slv; + TS_ASSERT_THROWS(slv.mkBagSort(d_solver->mkBitVectorSort(4)), + CVC4ApiException&); +} + void SolverBlack::testMkSequenceSort() { TS_ASSERT_THROWS_NOTHING( @@ -596,6 +608,17 @@ void SolverBlack::testMkEmptySet() TS_ASSERT_THROWS(slv.mkEmptySet(s), CVC4ApiException&); } +void SolverBlack::testMkEmptyBag() +{ + Solver slv; + Sort s = d_solver->mkBagSort(d_solver->getBooleanSort()); + TS_ASSERT_THROWS_NOTHING(d_solver->mkEmptyBag(Sort())); + TS_ASSERT_THROWS_NOTHING(d_solver->mkEmptyBag(s)); + TS_ASSERT_THROWS(d_solver->mkEmptyBag(d_solver->getBooleanSort()), + CVC4ApiException&); + TS_ASSERT_THROWS(slv.mkEmptyBag(s), CVC4ApiException&); +} + void SolverBlack::testMkEmptySequence() { Solver slv; |