Commit
54d24c786d6a843cc72dfb5e377603349ea5e420 was
changing CVC4 to handle certain non-fatal errors
(such as calling get-unsat-core without a proceding
unsat check-sat command) without terminating the
solver. In the case of get-unsat-cores, the changes
lead to the solver crashing because it was trying to
print an unsat core initialized with the default
constructor, so the member variable d_smt was NULL,
which lead to a dereference of a null pointer.
One of the issues of the way non-fatal errors were
handled was that the error reporting was done in the
invoke() method of the command instead of the
printResult() method, which lead to the error
described above and other issues such as a call to
get-value printing a value after reporting an error.
This commit aims to improve the design by adding a
RecoverableModalException for errors that the solver
can recover from and CommandRecoverableFailure to
communicate that a command failed in a way that does
not prohibit the solver from continuing to execute.
The exception RecoverableModalException is thrown by
the SMTEngine and the commands catch it and turn it
into a CommandRecoverableFailure. The commit changes
all error conditions from the commit above and adds a
regression test for them.
}
};/* 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 */
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;
}
#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) {
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)) {
#include "proof/unsat_core.h"
+#include "base/cvc4_assert.h"
#include "expr/expr_iomanip.h"
#include "options/base_options.h"
#include "printer/printer.h"
}
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);
}
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) {
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) {
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) {
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) {
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());
}
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:
/**
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);
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.
return true;
}
+// TODO(#1108): Simplify the error reporting of this method.
CVC4::SExpr SmtEngine::getAssignment() {
Trace("smt") << "SMT getAssignment()" << endl;
SmtScope smts(this);
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) {
}
}
+// TODO(#1108): Simplify the error reporting of this method.
Model* SmtEngine::getModel() {
Trace("smt") << "SMT getModel()" << endl;
SmtScope smts(this);
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 =
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);
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
#endif /* IS_PROOFS_BUILD */
}
+// TODO(#1108): Simplify the error reporting of this method.
Proof* SmtEngine::getProof() {
Trace("smt") << "SMT getProof()" << endl;
SmtScope smts(this);
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);
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 = \
--- /dev/null
+; 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)
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: ,,'`
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"
projects / cvc5.git / commitdiff