diff options
| -rw-r--r-- | src/api/cvc4cpp.cpp | 15 | ||||
| -rw-r--r-- | src/smt/smt_engine.h | 5 | ||||
| -rw-r--r-- | test/unit/api/solver_black.h | 42 |
3 files changed, 59 insertions, 3 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 60dbd6714..bdb5f2f59 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -3330,12 +3330,17 @@ std::vector<Term> Solver::getValue(const std::vector<Term>& terms) const */ void Solver::pop(uint32_t nscopes) const { - // CHECK: incremental enabled? - // CHECK: nscopes <= d_smtEngine->d_userLevels.size() + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_CHECK(d_smtEngine->getOption("incremental").toString() == "true") + << "Cannot pop when not solving incrementally (use --incremental)"; + CVC4_API_CHECK(nscopes <= d_smtEngine->getNumUserLevels()) + << "Cannot pop beyond first pushed context"; + for (uint32_t n = 0; n < nscopes; ++n) { d_smtEngine->pop(); } + CVC4_API_SOLVER_TRY_CATCH_END; } void Solver::printModel(std::ostream& out) const @@ -3349,11 +3354,15 @@ void Solver::printModel(std::ostream& out) const */ void Solver::push(uint32_t nscopes) const { - // CHECK: incremental enabled? + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_CHECK(d_smtEngine->getOption("incremental").toString() == "true") + << "Cannot push when not solving incrementally (use --incremental)"; + for (uint32_t n = 0; n < nscopes; ++n) { d_smtEngine->push(); } + CVC4_API_SOLVER_TRY_CATCH_END; } /** diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index dc275218f..ead337862 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -539,6 +539,11 @@ class CVC4_PUBLIC SmtEngine { bool isFullyInited() { return d_fullyInited; } /** + * Return the user context level. + */ + size_t getNumUserLevels() { return d_userLevels.size(); } + + /** * Set the logic of the script. */ void setLogic( 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&); |