From 829b597108f64a97398c863d150905c6d203613f Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Sat, 23 Aug 2014 01:50:02 -0400 Subject: [PATCH] Unsat core printing. --- src/main/command_executor.cpp | 8 ++++---- src/main/command_executor_portfolio.cpp | 2 +- src/printer/printer.cpp | 7 +++++++ src/printer/printer.h | 3 +++ src/printer/smt2/smt2_printer.cpp | 7 +++++++ src/printer/smt2/smt2_printer.h | 3 ++- src/smt/smt_engine.cpp | 2 +- src/util/unsat_core.cpp | 6 +++++- src/util/unsat_core.h | 19 +++++++++++++++---- 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 d_core; public: - UnsatCore() {} + UnsatCore() : d_smt(NULL) {} template - 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::const_iterator iterator; typedef std::vector::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 */ -- 2.30.2