New C++ API: Add checks and tests for push/pop. (#3121)

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 60dbd6714c713ce86a1c61f4c70e93253cc848ed..bdb5f2f59f8e70d01ce3caadaec88a16818c82d4 100644 (file)
--- 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 dc275218f2df1935ce2619d4db25dc30546be09b..ead337862411f501fc3028a608d20c0b77740dbb 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -538,6 +538,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.
    */

diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 33ee510079bc738117a074c38bbaedb1ae2f2922..a82807b3ba7ad2efb0098b342a377797efc48763 100644 (file)
--- 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&);