Unsat core printing.

9 files changed, 45 insertions, 12 deletions

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 8f51c6d0d..950728fab 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -119,9 +119,9 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
     d_lastStatistics = ossCurStats.str();
   }
 
-  // dump the model/proof if option is set
+  // dump the model/proof/unsat core if option is set
   if(status) {
-    Command * g = NULL;
+    Command* g = NULL;
     if( d_options[options::produceModels] &&
         d_options[options::dumpModels] &&
         ( res.asSatisfiabilityResult() == Result::SAT ||
@@ -138,8 +138,8 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
                res.asSatisfiabilityResult() == Result::UNSAT ) {
       g = new GetUnsatCoreCommand();
     }
-    if( g ){
-      //set no time limit during dumping if applicable
+    if(g != NULL) {
+      // set no time limit during dumping if applicable
       if( d_options[options::forceNoLimitCpuWhileDump] ){
         setNoLimitCPU();
       }
diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index 4c3c7b6bd..8af0c452a 100644
--- a/src/main/command_executor_portfolio.cpp
+++ b/src/main/command_executor_portfolio.cpp
@@ -357,7 +357,7 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
 
     bool status = portfolioReturn.second;
 
-    // dump the model/proof if option is set
+    // dump the model/proof/unsat core if option is set
     if(status) {
       if( d_options[options::produceModels] &&
           d_options[options::dumpModels] &&
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index 8f0f50daa..7a90f5a49 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -153,4 +153,11 @@ 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() {
+  for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) {
+    toStream(out, Node::fromExpr(*i), -1, false, -1);
+    out << std::endl;
+  }
+}/* Printer::toStream(UnsatCore) */
+
 }/* CVC4 namespace */
diff --git a/src/printer/printer.h b/src/printer/printer.h
index beb2438e2..9a9ee19d1 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -103,6 +103,9 @@ public:
   /** Write a Model out to a stream with this Printer. */
   virtual void toStream(std::ostream& out, const Model& m) const throw();
 
+  /** Write an UnsatCore out to a stream with this Printer. */
+  virtual void toStream(std::ostream& out, const UnsatCore& core) const throw();
+
 };/* class Printer */
 
 /**
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 766db729a..543079576 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -771,6 +771,13 @@ 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);
+  out << ")" << endl;
+}
+
+
 void Smt2Printer::toStream(std::ostream& out, const Model& m) const throw() {
   out << "(model" << endl;
   this->Printer::toStream(out, m);
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index e86b3cb2b..e825d3f4c 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -37,7 +37,6 @@ class Smt2Printer : public CVC4::Printer {
 
   void toStream(std::ostream& out, TNode n, int toDepth, bool types) const throw();
   void toStream(std::ostream& out, const Model& m, const Command* c) const throw();
-  void toStream(std::ostream& out, const Model& m) const throw();
 public:
   Smt2Printer(Variant variant = no_variant) : d_variant(variant) { }
   using CVC4::Printer::toStream;
@@ -46,6 +45,8 @@ public:
   void toStream(std::ostream& out, const CommandStatus* s) const throw();
   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();
 };/* class Smt2Printer */
 
 }/* CVC4::printer::smt2 namespace */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 90caa1fb1..98ae6d3ce 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3969,7 +3969,7 @@ UnsatCore SmtEngine::getUnsatCore() throw(ModalException) {
   }
 
   d_proofManager->getProof(this);// just to trigger core creation
-  return UnsatCore(d_proofManager->begin_unsat_core(), d_proofManager->end_unsat_core());
+  return UnsatCore(this, d_proofManager->begin_unsat_core(), d_proofManager->end_unsat_core());
 #else /* CVC4_PROOF */
   throw ModalException("This build of CVC4 doesn't have proof support (required for unsat cores).");
 #endif /* CVC4_PROOF */
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 */