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

2 files changed, 11 insertions, 5 deletions

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 */