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, 5 insertions, 10 deletions

diff --git a/src/proof/unsat_core.cpp b/src/proof/unsat_core.cpp
index c8696868e..3e5e493f1 100644
--- a/src/proof/unsat_core.cpp
+++ b/src/proof/unsat_core.cpp
@@ -44,13 +44,6 @@ void UnsatCore::toStream(std::ostream& out) const {
   Printer::getPrinter(options::outputLanguage())->toStream(out, *this);
 }
 
-void UnsatCore::toStream(std::ostream& out, const std::map<Expr, std::string>& names) const {
-  Assert(d_smt != NULL);
-  smt::SmtScope smts(d_smt);
-  expr::ExprDag::Scope scope(out, false);
-  Printer::getPrinter(options::outputLanguage())->toStream(out, *this, names);
-}
-
 std::ostream& operator<<(std::ostream& out, const UnsatCore& core) {
   core.toStream(out);
   return out;
diff --git a/src/proof/unsat_core.h b/src/proof/unsat_core.h
index 6f03dfa5e..46a368372 100644
--- a/src/proof/unsat_core.h
+++ b/src/proof/unsat_core.h
@@ -52,7 +52,7 @@ public:
   ~UnsatCore() {}
 
   /** get the smt engine that this unsat core is hooked up to */
-  SmtEngine* getSmtEngine() { return d_smt; }
+  SmtEngine* getSmtEngine() const { return d_smt; }
 
   size_t size() const { return d_core.size(); }
 
@@ -61,9 +61,11 @@ public:
 
   const_iterator begin() const;
   const_iterator end() const;
-
+  
+  /** prints this UnsatCore object to the stream out.
+  * We use the expression names stored in the SmtEngine d_smt
+  */
   void toStream(std::ostream& out) const;
-  void toStream(std::ostream& out, const std::map<Expr, std::string>& names) const;
 
 };/* class UnsatCore */