summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-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
-rw-r--r--test/regress/regress0/Makefile.am3
-rw-r--r--test/regress/regress0/non-fatal-errors.smt229
-rwxr-xr-xtest/regress/run_regression10
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"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback