Use symbol manager for unsat cores (#5468)

This PR uses the symbol manager for handling names for unsat cores.

This replaces interfaces in SmtEngine for managing expression names. It removes the SetExpressionName command.

1 files changed, 2 insertions, 28 deletions

diff --git a/src/smt/command.h b/src/smt/command.h
index 85897458d..96a6938d6 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -1221,8 +1221,8 @@ class CVC4_PUBLIC GetUnsatCoreCommand : public Command
       OutputLanguage language = language::output::LANG_AUTO) const override;
 
  protected:
-  /** The solver we were invoked with */
-  api::Solver* d_solver;
+  /** The symbol manager we were invoked with */
+  SymbolManager* d_sm;
   /** the result of the unsat core call */
   std::vector<api::Term> d_result;
 }; /* class GetUnsatCoreCommand */
@@ -1376,32 +1376,6 @@ class CVC4_PUBLIC GetOptionCommand : public Command
       OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class GetOptionCommand */
 
-// Set expression name command
-// Note this is not an official smt2 command
-// Conceptually:
-//   (assert (! expr :named name))
-// is converted to
-//   (assert expr)
-//   (set-expr-name expr name)
-class CVC4_PUBLIC SetExpressionNameCommand : public Command
-{
- protected:
-  api::Term d_term;
-  std::string d_name;
-
- public:
-  SetExpressionNameCommand(api::Term term, std::string name);
-
-  void invoke(api::Solver* solver, SymbolManager* sm) override;
-  Command* clone() const override;
-  std::string getCommandName() const override;
-  void toStream(
-      std::ostream& out,
-      int toDepth = -1,
-      size_t dag = 1,
-      OutputLanguage language = language::output::LANG_AUTO) const override;
-}; /* class SetExpressionNameCommand */
-
 class CVC4_PUBLIC DatatypeDeclarationCommand : public Command
 {
  private: