From cd7680c5a23ade0bd8d7f0dfac4623ed318639bb Mon Sep 17 00:00:00 2001 From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> Date: Mon, 5 Oct 2020 20:11:44 -0500 Subject: [PATCH] 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. --- src/api/cvc4cpp.cpp | 27 +++++++++++++- src/smt/command.cpp | 36 +++++++++---------- src/smt/command.h | 3 +- .../regress0/smtlib/set-info-status.smt2 | 2 +- 4 files changed, 44 insertions(+), 24 deletions(-) diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 179eb672e..30e95714d 100644 --- 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 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 84bc5fc99..5edbe51e0 100644 --- 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 result; - for (const Expr& e : - solver->getSmtEngine()->getValues(api::termVectorToExprs(d_terms))) - { - result.push_back(Node::fromExpr(e)); - } + std::vector 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> assignments = - solver->getSmtEngine()->getAssignment(); + std::vector> assignments = + solver->getAssignment(); vector 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 32cf70602..81a736407 100644 --- 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 4bfa1766a..9c28d2a76 100644 --- 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 -- 2.30.2