diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/base/modal_exception.h | 14 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 22 | ||||
-rw-r--r-- | src/proof/unsat_core.cpp | 3 | ||||
-rw-r--r-- | src/smt/command.cpp | 10 | ||||
-rw-r--r-- | src/smt/command.h | 18 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 29 |
6 files changed, 74 insertions, 22 deletions
diff --git a/src/base/modal_exception.h b/src/base/modal_exception.h index fc1b8ac9e..0392ab470 100644 --- a/src/base/modal_exception.h +++ b/src/base/modal_exception.h @@ -42,6 +42,20 @@ public: } };/* class ModalException */ +/** + * Special case of ModalException that allows the execution of the solver to + * continue. + * + * TODO(#1108): This exception should not be needed anymore in future versions + * of the public API. + */ +class CVC4_PUBLIC RecoverableModalException : public CVC4::ModalException { + public: + RecoverableModalException(const std::string& msg) : ModalException(msg) {} + + RecoverableModalException(const char* msg) : ModalException(msg) {} +}; /* class RecoverableModalException */ + }/* CVC4 namespace */ #endif /* __CVC4__SMT__MODAL_EXCEPTION_H */ diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index ae65311de..105e2c0dd 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1114,11 +1114,11 @@ template <class T> static bool tryToStream(std::ostream& out, const CommandStatus* s, Variant v) throw(); void Smt2Printer::toStream(std::ostream& out, const CommandStatus* s) const throw() { - - if(tryToStream<CommandSuccess>(out, s, d_variant) || - tryToStream<CommandFailure>(out, s, d_variant) || - tryToStream<CommandUnsupported>(out, s, d_variant) || - tryToStream<CommandInterrupted>(out, s, d_variant)) { + if (tryToStream<CommandSuccess>(out, s, d_variant) || + tryToStream<CommandFailure>(out, s, d_variant) || + tryToStream<CommandRecoverableFailure>(out, s, d_variant) || + tryToStream<CommandUnsupported>(out, s, d_variant) || + tryToStream<CommandInterrupted>(out, s, d_variant)) { return; } @@ -1653,8 +1653,7 @@ static void toStream(std::ostream& out, const CommandUnsupported* s, Variant v) #endif /* CVC4_COMPETITION_MODE */ } -static void toStream(std::ostream& out, const CommandFailure* s, Variant v) throw() { - string message = s->getMessage(); +static void errorToStream(std::ostream& out, std::string message, Variant v) { // escape all double-quotes size_t pos = 0; while((pos = message.find('"', pos)) != string::npos) { @@ -1664,6 +1663,15 @@ static void toStream(std::ostream& out, const CommandFailure* s, Variant v) thro out << "(error \"" << message << "\")" << endl; } +static void toStream(std::ostream& out, const CommandFailure* s, Variant v) { + errorToStream(out, s->getMessage(), v); +} + +static void toStream(std::ostream& out, const CommandRecoverableFailure* s, + Variant v) { + errorToStream(out, s->getMessage(), v); +} + template <class T> static bool tryToStream(std::ostream& out, const CommandStatus* s, Variant v) throw() { if(typeid(*s) == typeid(T)) { diff --git a/src/proof/unsat_core.cpp b/src/proof/unsat_core.cpp index b056e0ef4..c8696868e 100644 --- a/src/proof/unsat_core.cpp +++ b/src/proof/unsat_core.cpp @@ -16,6 +16,7 @@ #include "proof/unsat_core.h" +#include "base/cvc4_assert.h" #include "expr/expr_iomanip.h" #include "options/base_options.h" #include "printer/printer.h" @@ -37,12 +38,14 @@ UnsatCore::const_iterator UnsatCore::end() const { } void UnsatCore::toStream(std::ostream& out) const { + Assert(d_smt != NULL); smt::SmtScope smts(d_smt); expr::ExprDag::Scope scope(out, false); Printer::getPrinter(options::outputLanguage())->toStream(out, *this); } void UnsatCore::toStream(std::ostream& out, const std::map<Expr, std::string>& names) const { + Assert(d_smt != NULL); smt::SmtScope smts(d_smt); expr::ExprDag::Scope scope(out, false); Printer::getPrinter(options::outputLanguage())->toStream(out, *this, names); diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 2ca8b1fe3..70302088b 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1023,6 +1023,8 @@ void GetValueCommand::invoke(SmtEngine* smtEngine) { } d_result = em->mkExpr(kind::SEXPR, result); d_commandStatus = CommandSuccess::instance(); + } catch (RecoverableModalException& e) { + d_commandStatus = new CommandRecoverableFailure(e.what()); } catch(UnsafeInterruptException& e) { d_commandStatus = new CommandInterrupted(); } catch(exception& e) { @@ -1072,6 +1074,8 @@ void GetAssignmentCommand::invoke(SmtEngine* smtEngine) { try { d_result = smtEngine->getAssignment(); d_commandStatus = CommandSuccess::instance(); + } catch (RecoverableModalException& e) { + d_commandStatus = new CommandRecoverableFailure(e.what()); } catch(UnsafeInterruptException& e) { d_commandStatus = new CommandInterrupted(); } catch(exception& e) { @@ -1117,6 +1121,8 @@ void GetModelCommand::invoke(SmtEngine* smtEngine) { d_result = smtEngine->getModel(); d_smtEngine = smtEngine; d_commandStatus = CommandSuccess::instance(); + } catch (RecoverableModalException& e) { + d_commandStatus = new CommandRecoverableFailure(e.what()); } catch(UnsafeInterruptException& e) { d_commandStatus = new CommandInterrupted(); } catch(exception& e) { @@ -1166,6 +1172,8 @@ void GetProofCommand::invoke(SmtEngine* smtEngine) { d_smtEngine = smtEngine; d_result = smtEngine->getProof(); d_commandStatus = CommandSuccess::instance(); + } catch (RecoverableModalException& e) { + d_commandStatus = new CommandRecoverableFailure(e.what()); } catch(UnsafeInterruptException& e) { d_commandStatus = new CommandInterrupted(); } catch(exception& e) { @@ -1352,6 +1360,8 @@ void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine) { try { d_result = smtEngine->getUnsatCore(); d_commandStatus = CommandSuccess::instance(); + } catch (RecoverableModalException& e) { + d_commandStatus = new CommandRecoverableFailure(e.what()); } catch(exception& e) { d_commandStatus = new CommandFailure(e.what()); } diff --git a/src/smt/command.h b/src/smt/command.h index 36e679885..2e0f4090e 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -189,6 +189,24 @@ public: std::string getMessage() const throw() { return d_message; } };/* class CommandFailure */ +/** + * The execution of the command resulted in a non-fatal error and further + * commands can be processed. This status is for example used when a user asks + * for an unsat core in a place that is not immediately preceded by an + * unsat/valid response. + */ +class CVC4_PUBLIC CommandRecoverableFailure : public CommandStatus { + std::string d_message; + + public: + CommandRecoverableFailure(std::string message) throw() : d_message(message) {} + CommandRecoverableFailure& clone() const { + return *new CommandRecoverableFailure(*this); + } + ~CommandRecoverableFailure() throw() {} + std::string getMessage() const throw() { return d_message; } +}; /* class CommandRecoverableFailure */ + class CVC4_PUBLIC Command { protected: /** diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index b1a0a1acd..db7c65291 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -4656,6 +4656,7 @@ Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, L return n.toExpr(); } +// TODO(#1108): Simplify the error reporting of this method. Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckingException, LogicException, UnsafeInterruptException) { Assert(ex.getExprManager() == d_exprManager); SmtScope smts(this); @@ -4675,9 +4676,7 @@ Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckin d_problemExtended) { const char* msg = "Cannot get value unless immediately preceded by SAT/INVALID or UNKNOWN response."; - //throw ModalException(msg); - Warning() << CommandFailure(msg); - return ex; + throw RecoverableModalException(msg); } // Substitute out any abstract values in ex. @@ -4767,6 +4766,7 @@ bool SmtEngine::addToAssignment(const Expr& ex) { return true; } +// TODO(#1108): Simplify the error reporting of this method. CVC4::SExpr SmtEngine::getAssignment() { Trace("smt") << "SMT getAssignment()" << endl; SmtScope smts(this); @@ -4786,9 +4786,7 @@ CVC4::SExpr SmtEngine::getAssignment() { const char* msg = "Cannot get the current assignment unless immediately " "preceded by SAT/INVALID or UNKNOWN response."; - //throw ModalException(msg); - Warning() << CommandFailure(msg); - return SExpr(vector<SExpr>()); + throw RecoverableModalException(msg); } if(d_assignments == NULL) { @@ -4867,6 +4865,7 @@ void SmtEngine::addToModelCommandAndDump(const Command& c, uint32_t flags, bool } } +// TODO(#1108): Simplify the error reporting of this method. Model* SmtEngine::getModel() { Trace("smt") << "SMT getModel()" << endl; SmtScope smts(this); @@ -4883,9 +4882,7 @@ Model* SmtEngine::getModel() { const char* msg = "Cannot get the current model unless immediately " "preceded by SAT/INVALID or UNKNOWN response."; - //throw ModalException(msg); - Warning() << CommandFailure(msg); - return NULL; + throw RecoverableModalException(msg); } if(!options::produceModels()) { const char* msg = @@ -5131,6 +5128,7 @@ void SmtEngine::checkModel(bool hardFailure) { Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" << endl; } +// TODO(#1108): Simplify the error reporting of this method. UnsatCore SmtEngine::getUnsatCore() { Trace("smt") << "SMT getUnsatCore()" << endl; SmtScope smts(this); @@ -5145,9 +5143,9 @@ UnsatCore SmtEngine::getUnsatCore() { if(d_status.isNull() || d_status.asSatisfiabilityResult() != Result::UNSAT || d_problemExtended) { - //throw ModalException("Cannot get an unsat core unless immediately preceded by UNSAT/VALID response."); - Warning() << CommandFailure("Cannot get an unsat core unless immediately preceded by UNSAT/VALID response."); - return UnsatCore(); + throw RecoverableModalException( + "Cannot get an unsat core unless immediately preceded by UNSAT/VALID " + "response."); } d_proofManager->traceUnsatCore();// just to trigger core creation @@ -5157,6 +5155,7 @@ UnsatCore SmtEngine::getUnsatCore() { #endif /* IS_PROOFS_BUILD */ } +// TODO(#1108): Simplify the error reporting of this method. Proof* SmtEngine::getProof() { Trace("smt") << "SMT getProof()" << endl; SmtScope smts(this); @@ -5171,9 +5170,9 @@ Proof* SmtEngine::getProof() { if(d_status.isNull() || d_status.asSatisfiabilityResult() != Result::UNSAT || d_problemExtended) { - //throw ModalException("Cannot get a proof unless immediately preceded by UNSAT/VALID response."); - Warning() << CommandFailure("Cannot get a proof unless immediately preceded by UNSAT/VALID response."); - return NULL; + throw RecoverableModalException( + "Cannot get a proof unless immediately preceded by UNSAT/VALID " + "response."); } return ProofManager::getProof(this); |