diff options
-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 | ||||
-rw-r--r-- | test/regress/regress0/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/non-fatal-errors.smt2 | 29 | ||||
-rwxr-xr-x | test/regress/run_regression | 10 |
9 files changed, 115 insertions, 23 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); diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 1368dd067..dbff6cff1 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -69,7 +69,8 @@ SMT2_TESTS = \ hung10_itesdk_output1.smt2 \ hung13sdk_output2.smt2 \ declare-funs.smt2 \ - declare-fun-is-match.smt2 + declare-fun-is-match.smt2 \ + non-fatal-errors.smt2 # Regression tests for PL inputs CVC_TESTS = \ diff --git a/test/regress/regress0/non-fatal-errors.smt2 b/test/regress/regress0/non-fatal-errors.smt2 new file mode 100644 index 000000000..1e1865883 --- /dev/null +++ b/test/regress/regress0/non-fatal-errors.smt2 @@ -0,0 +1,29 @@ +; SCRUBBER: sed 's/".*"/""/g' +; EXPECT: success +; EXPECT: success +; EXPECT: success +; EXPECT: success +; EXPECT: success +; EXPECT: success +; EXPECT: success +; EXPECT: (error "") +; EXPECT: (error "") +; EXPECT: (error "") +; EXPECT: (error "") +; EXPECT: (error "") +; EXPECT: success +; EXPECT: sat +(set-option :print-success true) +(set-option :produce-unsat-cores true) +(set-option :produce-models true) +(set-option :produce-proofs true) +(set-option :produce-assignments true) +(set-logic UF) +(declare-fun p () Bool) +(get-unsat-core) +(get-value (p)) +(get-proof) +(get-model) +(get-assignment) +(assert true) +(check-sat) diff --git a/test/regress/run_regression b/test/regress/run_regression index 536a3e8a5..5d4165597 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -130,6 +130,15 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then fi elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then lang=smt2 + + # If this test case requires unsat cores but CVC4 is not built with proof + # support, skip it. Note: checking $CVC4_REGRESSION_ARGS instead of $proof + # here because $proof is not set for the second run. + requires_proof=`grep '(get-unsat-core)' "$benchmark"` + if [[ ! "$CVC4_REGRESSION_ARGS" = *"--proof"* ]] && [ -n "$requires_proof" ]; then + exit 77 + fi + if test -e "$benchmark.expect"; then scrubber=`grep '^% SCRUBBER: ' "$benchmark.expect" | sed 's,^% SCRUBBER: ,,'` errscrubber=`grep '^% ERROR-SCRUBBER: ' "$benchmark.expect" | sed 's,^% ERROR-SCRUBBER: ,,'` @@ -288,6 +297,7 @@ if [ "$proof" = yes ]; then fi fi fi + if [ -z "$expected_error" ]; then # in case expected stderr output is empty, make sure we don't differ # by a newline, which we would if we echo "" >"$experrfile" |