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

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