diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-10-18 15:19:10 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-10-18 15:19:10 -0500 |
commit | 9af7e38d6f0b3d01dea795a4847153047ac87f6e (patch) | |
tree | f16aed9383cead45ea321229560533f3c94b9566 /src/printer | |
parent | 6f18015fdcb824f46b969882aa45187b46306e97 (diff) |
Tptp unsat cores (#1228)
* Support unsat cores for TPTP.
* Fix assertion
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/tptp/tptp_printer.cpp | 19 | ||||
-rw-r--r-- | src/printer/tptp/tptp_printer.h | 5 |
2 files changed, 23 insertions, 1 deletions
diff --git a/src/printer/tptp/tptp_printer.cpp b/src/printer/tptp/tptp_printer.cpp index 5fc9b7ed8..102419ec4 100644 --- a/src/printer/tptp/tptp_printer.cpp +++ b/src/printer/tptp/tptp_printer.cpp @@ -23,6 +23,8 @@ #include "expr/expr.h" // for ExprSetDepth etc.. #include "expr/node_manager.h" // for VarNameAttr #include "options/language.h" // for LANG_AST +#include "options/smt_options.h" // for unsat cores +#include "smt/smt_engine.h" #include "smt/command.h" using namespace std; @@ -58,7 +60,22 @@ void TptpPrinter::toStream(std::ostream& out, const Model& m, const Command* c) // shouldn't be called; only the non-Command* version above should be Unreachable(); } - +void TptpPrinter::toStream(std::ostream& out, const UnsatCore& core) const throw() { + out << "% SZS output start UnsatCore " << std::endl; + SmtEngine * smt = core.getSmtEngine(); + Assert( smt!=NULL ); + for(UnsatCore::const_iterator i = core.begin(); i != core.end(); ++i) { + std::string name; + if (smt->getExpressionName(*i, name)) { + // Named assertions always get printed + out << name << endl; + } else if (options::dumpUnsatCoresFull()) { + // Unnamed assertions only get printed if the option is set + out << *i << endl; + } + } + out << "% SZS output end UnsatCore " << std::endl; +} }/* CVC4::printer::tptp namespace */ }/* CVC4::printer namespace */ diff --git a/src/printer/tptp/tptp_printer.h b/src/printer/tptp/tptp_printer.h index 7c8ddbd20..731885068 100644 --- a/src/printer/tptp/tptp_printer.h +++ b/src/printer/tptp/tptp_printer.h @@ -35,6 +35,11 @@ public: void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw(); void toStream(std::ostream& out, const CommandStatus* s) const throw(); void toStream(std::ostream& out, const Model& m) const throw(); + /** print unsat core to stream + * We use the expression names stored in the SMT engine associated with the unsat core + * with UnsatCore::getSmtEngine. + */ + void toStream(std::ostream& out, const UnsatCore& core) const throw(); };/* class TptpPrinter */ }/* CVC4::printer::tptp namespace */ |