Improved SMT-LIBv2 language support for unsat cores.

2 files changed, 14 insertions, 3 deletions

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index a07076281..a3f5170fa 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -1121,6 +1121,9 @@ std::string GetInstantiationsCommand::getCommandName() const throw() {
 GetUnsatCoreCommand::GetUnsatCoreCommand() throw() {
 }
 
+GetUnsatCoreCommand::GetUnsatCoreCommand(const std::map<Expr, std::string>& names) throw() : d_names(names) {
+}
+
 void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine) throw() {
   try {
     d_result = smtEngine->getUnsatCore();
@@ -1134,18 +1137,23 @@ void GetUnsatCoreCommand::printResult(std::ostream& out, uint32_t verbosity) con
   if(! ok()) {
     this->Command::printResult(out, verbosity);
   } else {
-    d_result.toStream(out);
+    d_result.toStream(out, d_names);
   }
 }
 
+const UnsatCore& GetUnsatCoreCommand::getUnsatCore() const throw() {
+  // of course, this will be empty if the command hasn't been invoked yet
+  return d_result;
+}
+
 Command* GetUnsatCoreCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
-  GetUnsatCoreCommand* c = new GetUnsatCoreCommand();
+  GetUnsatCoreCommand* c = new GetUnsatCoreCommand(d_names);
   c->d_result = d_result;
   return c;
 }
 
 Command* GetUnsatCoreCommand::clone() const {
-  GetUnsatCoreCommand* c = new GetUnsatCoreCommand();
+  GetUnsatCoreCommand* c = new GetUnsatCoreCommand(d_names);
   c->d_result = d_result;
   return c;
 }
diff --git a/src/expr/command.h b/src/expr/command.h
index e84c53d09..4d2957b7c 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -602,11 +602,14 @@ public:
 class CVC4_PUBLIC GetUnsatCoreCommand : public Command {
 protected:
   UnsatCore d_result;
+  std::map<Expr, std::string> d_names;
 public:
   GetUnsatCoreCommand() throw();
+  GetUnsatCoreCommand(const std::map<Expr, std::string>& names) throw();
   ~GetUnsatCoreCommand() throw() {}
   void invoke(SmtEngine* smtEngine) throw();
   void printResult(std::ostream& out, uint32_t verbosity = 2) const throw();
+  const UnsatCore& getUnsatCore() const throw();
   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
   Command* clone() const;
   std::string getCommandName() const throw();