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.

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);