From 58cf0f8f5762c5e7994d84f8a20969632f2be796 Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Wed, 15 May 2019 13:03:24 -0700
Subject: [PATCH] New C++ API: Add checks and tests for push/pop. (#3121)

---
 src/api/cvc4cpp.cpp          | 15 ++++++++++---
 src/smt/smt_engine.h         |  5 +++++
 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
@@ -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 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&);
-- 
2.30.2