diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-10-11 06:11:46 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-10-11 06:11:46 -0500 |
commit | 3153e2d94d1b12562557d60305bcac52d3128b83 (patch) | |
tree | ef4740a54d489b61d92163024a8c516f38aae050 /src/printer | |
parent | 5e2c7c3a25d334c0068b423225f8ff7793260069 (diff) |
Move unsat core names to smt engine (#1192)
* Move unsat core names to SmtEnginePrivate. Adds a SetExpressionNameCommand to do this. Removes the names field from GetUnsatCoreCommand.
* Comment
* Pass expression names by reference.
* Update throw specifiers.
* Minor
* Switch expression names to CDMap, simplify interface for printing unsat core names.
* Revert throw specifier change.
* Minor simplifcations
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/printer.cpp | 7 | ||||
-rw-r--r-- | src/printer/printer.h | 3 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 10 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.h | 6 |
4 files changed, 12 insertions, 14 deletions
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 5e349d123..fd7a4ee19 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -84,17 +84,12 @@ 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) { AssertCommand cmd(*i); toStream(out, &cmd, -1, false, -1); out << std::endl; } -}/* Printer::toStream(UnsatCore, std::map<Expr, std::string>) */ +}/* Printer::toStream(UnsatCore) */ Printer* Printer::getPrinter(OutputLanguage lang) throw() { if(lang == language::output::LANG_AUTO) { diff --git a/src/printer/printer.h b/src/printer/printer.h index ec1f92604..ea4865fce 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -77,9 +77,6 @@ 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 */ }/* CVC4 namespace */ diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 147fefa04..0a8020651 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1141,13 +1141,15 @@ void Smt2Printer::toStream(std::ostream& out, const CommandStatus* s) const thro }/* Smt2Printer::toStream(CommandStatus*) */ -void Smt2Printer::toStream(std::ostream& out, const UnsatCore& core, const std::map<Expr, std::string>& names) const throw() { +void Smt2Printer::toStream(std::ostream& out, const UnsatCore& core) const throw() { out << "(" << std::endl; + SmtEngine * smt = core.getSmtEngine(); + Assert( smt!=NULL ); for(UnsatCore::const_iterator i = core.begin(); i != core.end(); ++i) { - map<Expr, string>::const_iterator j = names.find(*i); - if (j != names.end()) { + std::string name; + if (smt->getExpressionName(*i,name)) { // Named assertions always get printed - out << maybeQuoteSymbol((*j).second) << endl; + out << maybeQuoteSymbol(name) << endl; } else if (options::dumpUnsatCoresFull()) { // Unnamed assertions only get printed if the option is set out << *i << endl; diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index f6438ae87..b7e9e1f40 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -48,7 +48,11 @@ public: void toStream(std::ostream& out, const CommandStatus* s) 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 std::map<Expr, std::string>& names) const throw(); + /** print the unsat core to the stream out. + * We use the expression names that are stored in the SMT engine associated + * with the core (UnsatCore::getSmtEngine) for printing named assertions. + */ + void toStream(std::ostream& out, const UnsatCore& core) const throw(); };/* class Smt2Printer */ }/* CVC4::printer::smt2 namespace */ |