New C++ API: Catch and throw recoverable exception. (#5122)

This allows to distinguish recoverable from non-recoverable exceptions,
and recover if possible.

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 125e33ba59cb128b18c354c585abfdb452d65706..08beec35a6a145806a9f16138a524d7ccdf8f214 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -807,6 +807,10 @@ class CVC4ApiExceptionStream
   {
 #define CVC4_API_SOLVER_TRY_CATCH_END                                          \
   }                                                                            \
+  catch (const CVC4::RecoverableModalException& e)                             \
+  {                                                                            \
+    throw CVC4ApiRecoverableException(e.getMessage());                         \
+  }                                                                            \
   catch (const CVC4::Exception& e) { throw CVC4ApiException(e.getMessage()); } \
   catch (const std::invalid_argument& e) { throw CVC4ApiException(e.what()); }
 

diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 841a8ee8a6e2c2cae997392cbe6d2a6fdd8a04d3..31ff13ba0aba7b860270942fd1e62ae692175885 100644 (file)
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -75,6 +75,16 @@ class CVC4_PUBLIC CVC4ApiException : public std::exception
   std::string d_msg;
 };
 
+class CVC4_PUBLIC CVC4ApiRecoverableException : public CVC4ApiException
+{
+ public:
+  CVC4ApiRecoverableException(const std::string& str) : CVC4ApiException(str) {}
+  CVC4ApiRecoverableException(const std::stringstream& stream)
+      : CVC4ApiException(stream.str())
+  {
+  }
+};
+
 /* -------------------------------------------------------------------------- */
 /* Result                                                                     */
 /* -------------------------------------------------------------------------- */

diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 8a4d878ef2a5e70a15dec66331b8478acdf021e1..666fdd86fd1eb58292171b91584c2e4dd15ad138 100644 (file)
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -27,6 +27,8 @@ class SolverBlack : public CxxTest::TestSuite
   void setUp() override;
   void tearDown() override;
 
+  void testRecoverableException();
+
   void testSupportsFloatingPoint();
 
   void testGetBooleanSort();
@@ -173,6 +175,14 @@ void SolverBlack::setUp() { d_solver.reset(new Solver()); }
 
 void SolverBlack::tearDown() { d_solver.reset(nullptr); }
 
+void SolverBlack::testRecoverableException()
+{
+  d_solver->setOption("produce-models", "true");
+  Term x = d_solver->mkConst(d_solver->getBooleanSort(), "x");
+  d_solver->assertFormula(x.eqTerm(x).notTerm());
+  TS_ASSERT_THROWS(d_solver->printModel(std::cout), CVC4ApiRecoverableException&);
+}
+
 void SolverBlack::testSupportsFloatingPoint()
 {
   if (d_solver->supportsFloatingPoint())