Unsat core printing.

2 files changed, 20 insertions, 5 deletions

diff --git a/src/util/unsat_core.cpp b/src/util/unsat_core.cpp
index 27261635d..6344b3eda 100644
--- a/src/util/unsat_core.cpp
+++ b/src/util/unsat_core.cpp
@@ -16,6 +16,8 @@
 
 #include "util/unsat_core.h"
 #include "expr/command.h"
+#include "smt/smt_engine_scope.h"
+#include "printer/printer.h"
 
 namespace CVC4 {
 
@@ -34,7 +36,9 @@ void UnsatCore::toStream(std::ostream& out) const {
 }
 
 std::ostream& operator<<(std::ostream& out, const UnsatCore& core) {
-  core.toStream(out);
+  smt::SmtScope smts(core.d_smt);
+  Expr::dag::Scope scope(out, false);
+  Printer::getPrinter(options::outputLanguage())->toStream(out, core);
   return out;
 }
 
diff --git a/src/util/unsat_core.h b/src/util/unsat_core.h
index 51724b33b..c67a6e448 100644
--- a/src/util/unsat_core.h
+++ b/src/util/unsat_core.h
@@ -26,17 +26,30 @@
 
 namespace CVC4 {
 
+class SmtEngine;
+class UnsatCore;
+
+std::ostream& operator<<(std::ostream& out, const UnsatCore& core) CVC4_PUBLIC;
+
 class CVC4_PUBLIC UnsatCore {
+  friend std::ostream& operator<<(std::ostream&, const UnsatCore&);
+
+  /** The SmtEngine we're associated with */
+  SmtEngine* d_smt;
+
   std::vector<Expr> d_core;
 
 public:
-  UnsatCore() {}
+  UnsatCore() : d_smt(NULL) {}
 
   template <class T>
-  UnsatCore(T begin, T end) : d_core(begin, end) {}
+  UnsatCore(SmtEngine* smt, T begin, T end) : d_smt(smt), d_core(begin, end) {}
 
   ~UnsatCore() {}
 
+  /** get the smt engine that this unsat core is hooked up to */
+  SmtEngine* getSmtEngine() { return d_smt; }
+
   typedef std::vector<Expr>::const_iterator iterator;
   typedef std::vector<Expr>::const_iterator const_iterator;
 
@@ -47,8 +60,6 @@ public:
 
 };/* class UnsatCore */
 
-std::ostream& operator<<(std::ostream& out, const UnsatCore& core) CVC4_PUBLIC;
-
 }/* CVC4 namespace */
 
 #endif /* __CVC4__UNSAT_CORE_H */