Add support for SMT-LIB v2.5 command get-unsat-assumptions (#1653)

1 files changed, 61 insertions, 0 deletions

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index e61ea868f..c77c4ed02 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1841,6 +1841,67 @@ std::string GetQuantifierEliminationCommand::getCommandName() const
 }
 
 /* -------------------------------------------------------------------------- */
+/* class GetUnsatAssumptionsCommand                                           */
+/* -------------------------------------------------------------------------- */
+
+GetUnsatAssumptionsCommand::GetUnsatAssumptionsCommand() {}
+
+void GetUnsatAssumptionsCommand::invoke(SmtEngine* smtEngine)
+{
+  try
+  {
+    d_result = smtEngine->getUnsatAssumptions();
+    d_commandStatus = CommandSuccess::instance();
+  }
+  catch (RecoverableModalException& e)
+  {
+    d_commandStatus = new CommandRecoverableFailure(e.what());
+  }
+  catch (exception& e)
+  {
+    d_commandStatus = new CommandFailure(e.what());
+  }
+}
+
+std::vector<Expr> GetUnsatAssumptionsCommand::getResult() const
+{
+  return d_result;
+}
+
+void GetUnsatAssumptionsCommand::printResult(std::ostream& out,
+                                             uint32_t verbosity) const
+{
+  if (!ok())
+  {
+    this->Command::printResult(out, verbosity);
+  }
+  else
+  {
+    out << d_result << endl;
+  }
+}
+
+Command* GetUnsatAssumptionsCommand::exportTo(
+    ExprManager* exprManager, ExprManagerMapCollection& variableMap)
+{
+  GetUnsatAssumptionsCommand* c = new GetUnsatAssumptionsCommand;
+  c->d_result = d_result;
+  return c;
+}
+
+Command* GetUnsatAssumptionsCommand::clone() const
+{
+  GetUnsatAssumptionsCommand* c = new GetUnsatAssumptionsCommand;
+  c->d_result = d_result;
+  return c;
+}
+
+std::string GetUnsatAssumptionsCommand::getCommandName() const
+{
+  return "get-unsat-assumptions";
+}
+
+/* -------------------------------------------------------------------------- */
 /* class GetUnsatCoreCommand                                                  */
 /* -------------------------------------------------------------------------- */