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.

1 files changed, 18 insertions, 0 deletions

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:
   /**