From 4983832f0e72d1e1a01654a1f5c2d270d3db8602 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 19 Sep 2017 09:43:58 -0700 Subject: Fix issue #1074, improve non-fatal error handling (#1075) 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. --- src/base/modal_exception.h | 14 ++++++++++++++ 1 file changed, 14 insertions(+) (limited to 'src/base') 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 */ -- cgit v1.2.3