Improved SMT-LIBv2 language support for unsat cores.

4 files changed, 26 insertions, 7 deletions

diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index 7a90f5a49..dd2e180e1 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -154,10 +154,16 @@ void Printer::toStream(std::ostream& out, const Model& m) const throw() {
 }/* Printer::toStream(Model) */
 
 void Printer::toStream(std::ostream& out, const UnsatCore& core) const throw() {
+  std::map<Expr, std::string> names;
+  toStream(out, core, names);
+}/* Printer::toStream(UnsatCore) */
+
+void Printer::toStream(std::ostream& out, const UnsatCore& core, const std::map<Expr, std::string>& names) const throw() {
   for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) {
-    toStream(out, Node::fromExpr(*i), -1, false, -1);
+    AssertCommand cmd(*i);
+    toStream(out, &cmd, -1, false, -1);
     out << std::endl;
   }
-}/* Printer::toStream(UnsatCore) */
+}/* Printer::toStream(UnsatCore, std::map<Expr, std::string>) */
 
 }/* CVC4 namespace */
diff --git a/src/printer/printer.h b/src/printer/printer.h
index 9a9ee19d1..e0b80ddfc 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -19,6 +19,9 @@
 #ifndef __CVC4__PRINTER__PRINTER_H
 #define __CVC4__PRINTER__PRINTER_H
 
+#include <map>
+#include <string>
+
 #include "util/language.h"
 #include "util/sexpr.h"
 #include "util/model.h"
@@ -106,6 +109,9 @@ public:
   /** Write an UnsatCore out to a stream with this Printer. */
   virtual void toStream(std::ostream& out, const UnsatCore& core) const throw();
 
+  /** Write an UnsatCore out to a stream with this Printer. */
+  virtual void toStream(std::ostream& out, const UnsatCore& core, const std::map<Expr, std::string>& names) const throw();
+
 };/* class Printer */
 
 /**
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 543079576..cb1fe87b2 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -771,11 +771,18 @@ void Smt2Printer::toStream(std::ostream& out, const CommandStatus* s) const thro
 }/* Smt2Printer::toStream(CommandStatus*) */
 
 
-void Smt2Printer::toStream(std::ostream& out, const UnsatCore& core) const throw() {
-  out << "(" << endl;
-  this->Printer::toStream(out, core);
+void Smt2Printer::toStream(std::ostream& out, const UnsatCore& core, const std::map<Expr, std::string>& names) const throw() {
+  out << "(" << std::endl;
+  for(UnsatCore::const_iterator i = core.begin(); i != core.end(); ++i) {
+    map<Expr, string>::const_iterator j = names.find(*i);
+    if(j == names.end()) {
+      out << *i << endl;
+    } else {
+      out << (*j).second << endl;
+    }
+  }
   out << ")" << endl;
-}
+}/* Smt2Printer::toStream(UnsatCore, map<Expr, string>) */
 
 
 void Smt2Printer::toStream(std::ostream& out, const Model& m) const throw() {
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index e825d3f4c..dbbc67fc2 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -46,7 +46,7 @@ public:
   void toStream(std::ostream& out, const Result& r) const throw();
   void toStream(std::ostream& out, const SExpr& sexpr) const throw();
   void toStream(std::ostream& out, const Model& m) const throw();
-  void toStream(std::ostream& out, const UnsatCore& core) const throw();
+  void toStream(std::ostream& out, const UnsatCore& core, const std::map<Expr, std::string>& names) const throw();
 };/* class Smt2Printer */
 
 }/* CVC4::printer::smt2 namespace */