summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/base/modal_exception.h14
-rw-r--r--src/printer/smt2/smt2_printer.cpp22
-rw-r--r--src/proof/unsat_core.cpp3
-rw-r--r--src/smt/command.cpp10
-rw-r--r--src/smt/command.h18
-rw-r--r--src/smt/smt_engine.cpp29
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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback