diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2019-05-15 13:03:24 -0700 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2019-08-07 11:19:57 -0700 |
commit | 58cf0f8f5762c5e7994d84f8a20969632f2be796 (patch) | |
tree | 701a1a7c8a77521df4a534e12c4f9a9ba4e049b1 /test/unit | |
parent | 800845fab13fd153dc94f9951bf05c4cf0fd9d63 (diff) |
New C++ API: Add checks and tests for push/pop. (#3121)
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/api/solver_black.h | 42 |
1 files changed, 42 insertions, 0 deletions
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index 33ee51007..a82807b3b 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -84,6 +84,12 @@ class SolverBlack : public CxxTest::TestSuite void testDefineFunRec(); void testDefineFunsRec(); + void testPush1(); + void testPush2(); + void testPop1(); + void testPop2(); + void testPop3(); + void testSetInfo(); void testSetLogic(); void testSetOption(); @@ -879,6 +885,42 @@ void SolverBlack::testDefineFunsRec() CVC4ApiException&); } +void SolverBlack::testPush1() +{ + d_solver->setOption("incremental", "true"); + TS_ASSERT_THROWS_NOTHING(d_solver->push(1)); + TS_ASSERT_THROWS(d_solver->setOption("incremental", "false"), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->setOption("incremental", "true"), + CVC4ApiException&); +} + +void SolverBlack::testPush2() +{ + d_solver->setOption("incremental", "false"); + TS_ASSERT_THROWS(d_solver->push(1), CVC4ApiException&); +} + +void SolverBlack::testPop1() +{ + d_solver->setOption("incremental", "false"); + TS_ASSERT_THROWS(d_solver->pop(1), CVC4ApiException&); +} + +void SolverBlack::testPop2() +{ + d_solver->setOption("incremental", "true"); + TS_ASSERT_THROWS(d_solver->pop(1), CVC4ApiException&); +} + +void SolverBlack::testPop3() +{ + d_solver->setOption("incremental", "true"); + TS_ASSERT_THROWS_NOTHING(d_solver->push(1)); + TS_ASSERT_THROWS_NOTHING(d_solver->pop(1)); + TS_ASSERT_THROWS(d_solver->pop(1), CVC4ApiException&); +} + void SolverBlack::testSetInfo() { TS_ASSERT_THROWS(d_solver->setInfo("cvc4-lagic", "QF_BV"), CVC4ApiException&); |