Recover from some exceptions. (#5203)

This PR replaces more calls to SmtEngine functions with calls to corresponding Solver functions in command.cpp. The PR also adds CVC4_API_RECOVERABLE_CHECK macro to use for recoverable exceptions.

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 179eb672e313a3e634b2c40c19fb6700e8525307..30e95714d29fdfb559f4224524138c825a3069ee 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -752,10 +752,35 @@ class CVC4ApiExceptionStream
   std::stringstream d_stream;
 };
 
+class CVC4ApiRecoverableExceptionStream
+{
+ public:
+  CVC4ApiRecoverableExceptionStream() {}
+  /* Note: This needs to be explicitly set to 'noexcept(false)' since it is
+   * a destructor that throws an exception and in C++11 all destructors
+   * default to noexcept(true) (else this triggers a call to std::terminate). */
+  ~CVC4ApiRecoverableExceptionStream() noexcept(false)
+  {
+    if (!std::uncaught_exception())
+    {
+      throw CVC4ApiRecoverableException(d_stream.str());
+    }
+  }
+
+  std::ostream& ostream() { return d_stream; }
+
+ private:
+  std::stringstream d_stream;
+};
+
 #define CVC4_API_CHECK(cond) \
   CVC4_PREDICT_TRUE(cond)    \
   ? (void)0 : OstreamVoider() & CVC4ApiExceptionStream().ostream()
 
+#define CVC4_API_RECOVERABLE_CHECK(cond) \
+  CVC4_PREDICT_TRUE(cond)                \
+  ? (void)0 : OstreamVoider() & CVC4ApiRecoverableExceptionStream().ostream()
+
 #define CVC4_API_CHECK_NOT_NULL                     \
   CVC4_API_CHECK(!isNullHelper())                   \
       << "Invalid call to '" << __PRETTY_FUNCTION__ \
@@ -5075,7 +5100,7 @@ std::vector<Term> Solver::getUnsatCore(void) const
   CVC4_API_CHECK(d_smtEngine->getOptions()[options::unsatCores])
       << "Cannot get unsat core unless explicitly enabled "
          "(try --produce-unsat-cores)";
-  CVC4_API_CHECK(d_smtEngine->getSmtMode() == SmtMode::UNSAT)
+  CVC4_API_RECOVERABLE_CHECK(d_smtEngine->getSmtMode() == SmtMode::UNSAT)
       << "Cannot get unsat core unless in unsat mode.";
   UnsatCore core = d_smtEngine->getUnsatCore();
   /* Can not use

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 84bc5fc99d071a1557b0ba560edb6a35e9c50699..5edbe51e04e4b07db5332b58bd9ea1640513cae1 100644 (file)
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1661,12 +1661,8 @@ void GetValueCommand::invoke(api::Solver* solver)
   {
     NodeManager* nm = solver->getNodeManager();
     smt::SmtScope scope(solver->getSmtEngine());
-    std::vector<Node> result;
-    for (const Expr& e :
-         solver->getSmtEngine()->getValues(api::termVectorToExprs(d_terms)))
-    {
-      result.push_back(Node::fromExpr(e));
-    }
+    std::vector<Node> result =
+        api::termVectorToNodes(solver->getValue(d_terms));
     Assert(result.size() == d_terms.size());
     for (int i = 0, size = d_terms.size(); i < size; i++)
     {
@@ -1688,7 +1684,7 @@ void GetValueCommand::invoke(api::Solver* solver)
     d_result = api::Term(solver, nm->mkNode(kind::SEXPR, result));
     d_commandStatus = CommandSuccess::instance();
   }
-  catch (RecoverableModalException& e)
+  catch (api::CVC4ApiRecoverableException& e)
   {
     d_commandStatus = new CommandRecoverableFailure(e.what());
   }
@@ -1744,8 +1740,8 @@ void GetAssignmentCommand::invoke(api::Solver* solver)
 {
   try
   {
-    std::vector<std::pair<Expr, Expr>> assignments =
-        solver->getSmtEngine()->getAssignment();
+    std::vector<std::pair<api::Term, api::Term>> assignments =
+        solver->getAssignment();
     vector<SExpr> sexprs;
     for (const auto& p : assignments)
     {
@@ -1757,7 +1753,7 @@ void GetAssignmentCommand::invoke(api::Solver* solver)
     d_result = SExpr(sexprs);
     d_commandStatus = CommandSuccess::instance();
   }
-  catch (RecoverableModalException& e)
+  catch (api::CVC4ApiRecoverableException& e)
   {
     d_commandStatus = new CommandRecoverableFailure(e.what());
   }
@@ -1810,13 +1806,12 @@ void GetAssignmentCommand::toStream(std::ostream& out,
 /* class GetModelCommand                                                      */
 /* -------------------------------------------------------------------------- */
 
-GetModelCommand::GetModelCommand() : d_result(nullptr), d_smtEngine(nullptr) {}
+GetModelCommand::GetModelCommand() : d_result(nullptr) {}
 void GetModelCommand::invoke(api::Solver* solver)
 {
   try
   {
     d_result = solver->getSmtEngine()->getModel();
-    d_smtEngine = solver->getSmtEngine();
     d_commandStatus = CommandSuccess::instance();
   }
   catch (RecoverableModalException& e)
@@ -1855,7 +1850,6 @@ Command* GetModelCommand::clone() const
 {
   GetModelCommand* c = new GetModelCommand();
   c->d_result = d_result;
-  c->d_smtEngine = d_smtEngine;
   return c;
 }
 
@@ -2056,12 +2050,12 @@ void GetInstantiationsCommand::toStream(std::ostream& out,
 /* class GetSynthSolutionCommand                                              */
 /* -------------------------------------------------------------------------- */
 
-GetSynthSolutionCommand::GetSynthSolutionCommand() : d_smtEngine(nullptr) {}
+GetSynthSolutionCommand::GetSynthSolutionCommand() : d_solver(nullptr) {}
 void GetSynthSolutionCommand::invoke(api::Solver* solver)
 {
   try
   {
-    d_smtEngine = solver->getSmtEngine();
+    d_solver = solver;
     d_commandStatus = CommandSuccess::instance();
   }
   catch (exception& e)
@@ -2079,14 +2073,14 @@ void GetSynthSolutionCommand::printResult(std::ostream& out,
   }
   else
   {
-    d_smtEngine->printSynthSolution(out);
+    d_solver->printSynthSolution(out);
   }
 }
 
 Command* GetSynthSolutionCommand::clone() const
 {
   GetSynthSolutionCommand* c = new GetSynthSolutionCommand();
-  c->d_smtEngine = d_smtEngine;
+  c->d_solver = d_solver;
   return c;
 }
 
@@ -2371,7 +2365,7 @@ void GetUnsatAssumptionsCommand::invoke(api::Solver* solver)
     d_result = solver->getUnsatAssumptions();
     d_commandStatus = CommandSuccess::instance();
   }
-  catch (RecoverableModalException& e)
+  catch (api::CVC4ApiRecoverableException& e)
   {
     d_commandStatus = new CommandRecoverableFailure(e.what());
   }
@@ -2429,10 +2423,12 @@ void GetUnsatCoreCommand::invoke(api::Solver* solver)
 {
   try
   {
-    d_result = solver->getSmtEngine()->getUnsatCore();
+    d_result = UnsatCore(solver->getSmtEngine(),
+                         api::termVectorToExprs(solver->getUnsatCore()));
+
     d_commandStatus = CommandSuccess::instance();
   }
-  catch (RecoverableModalException& e)
+  catch (api::CVC4ApiRecoverableException& e)
   {
     d_commandStatus = new CommandRecoverableFailure(e.what());
   }

diff --git a/src/smt/command.h b/src/smt/command.h
index 32cf70602c68fec4c3b93e3fe1c59c46d69b8e2b..81a736407dde3faf50e1e5b5228be3734ffcd40f 100644 (file)
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -996,7 +996,6 @@ class CVC4_PUBLIC GetModelCommand : public Command
 
  protected:
   Model* d_result;
-  SmtEngine* d_smtEngine;
 }; /* class GetModelCommand */
 
 /** The command to block models. */
@@ -1091,7 +1090,7 @@ class CVC4_PUBLIC GetSynthSolutionCommand : public Command
       OutputLanguage language = language::output::LANG_AUTO) const override;
 
  protected:
-  SmtEngine* d_smtEngine;
+  api::Solver* d_solver;
 }; /* class GetSynthSolutionCommand */
 
 /** The command (get-interpol s B (G)?)

diff --git a/test/regress/regress0/smtlib/set-info-status.smt2 b/test/regress/regress0/smtlib/set-info-status.smt2
index 4bfa1766afc865c9213cce00cd1bb6337fde44f5..9c28d2a769bbf4662e24949d1b04383e05f6bef5 100644 (file)
--- a/test/regress/regress0/smtlib/set-info-status.smt2
+++ b/test/regress/regress0/smtlib/set-info-status.smt2
@@ -1,4 +1,4 @@
-; EXPECT: (error "Cannot get an unsat core unless immediately preceded by UNSAT/ENTAILED response.")
+; EXPECT: (error "Cannot get unsat core unless in unsat mode.")
 ; EXPECT: sat
 ; EXPECT: sat
 ; EXPECT: unsat