diff options
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/printer.cpp | 10 | ||||
-rw-r--r-- | src/printer/printer.h | 6 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 15 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.h | 2 |
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 */ |