From 24b44a8e559f1d89f309d611922098e667293920 Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Tue, 22 Sep 2020 21:25:07 -0700
Subject: [PATCH] New C++ API: Catch and throw recoverable exception. (#5122)

This allows to distinguish recoverable from non-recoverable exceptions,
and recover if possible.
---
 src/api/cvc4cpp.cpp          |  4 ++++
 src/api/cvc4cpp.h            | 10 ++++++++++
 test/unit/api/solver_black.h | 10 ++++++++++
 3 files changed, 24 insertions(+)

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 125e33ba5..08beec35a 100644
--- 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 841a8ee8a..31ff13ba0 100644
--- 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 8a4d878ef..666fdd86f 100644
--- 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())
-- 
2.30.2