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.

14 files changed, 106 insertions, 276 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 47903ccae..c570dfdb4 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -219,8 +219,6 @@ libcvc4_add_sources(
   smt/dump.h
   smt/dump_manager.cpp
   smt/dump_manager.h
-  smt/expr_names.cpp
-  smt/expr_names.h
   smt/listeners.cpp
   smt/listeners.h
   smt/logic_exception.h
diff --git a/src/expr/symbol_manager.cpp b/src/expr/symbol_manager.cpp
index 75ffa4f62..a163e503d 100644
--- a/src/expr/symbol_manager.cpp
+++ b/src/expr/symbol_manager.cpp
@@ -77,18 +77,20 @@ bool SymbolManager::Implementation::setExpressionName(api::Term t,
                                                       const std::string& name,
                                                       bool isAssertion)
 {
+  Trace("sym-manager") << "set expression name: " << t << " -> " << name
+                       << ", isAssertion=" << isAssertion << std::endl;
   // cannot name subexpressions under quantifiers
   PrettyCheckArgument(
       !d_hasPushedScope.get(), name, "cannot name function in a scope");
+  if (isAssertion)
+  {
+    d_namedAsserts.insert(t);
+  }
   if (d_names.find(t) != d_names.end())
   {
     // already named assertion
     return false;
   }
-  if (isAssertion)
-  {
-    d_namedAsserts.insert(t);
-  }
   d_names[t] = name;
   return true;
 }
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 2b32afa15..f81bfc163 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -365,12 +365,7 @@ command [std::unique_ptr<CVC4::Command>* cmd]
         // set the expression name, if there was a named term
         std::pair<api::Term, std::string> namedTerm =
             PARSER_STATE->lastNamedTerm();
-        // TODO (projects-248)
-        // SYM_MAN->setExpressionName(namedTerm.first, namedTerm.second, true);
-        Command* csen =
-            new SetExpressionNameCommand(namedTerm.first, namedTerm.second);
-        csen->setMuted(true);
-        PARSER_STATE->preemptCommand(csen);
+        SYM_MAN->setExpressionName(namedTerm.first, namedTerm.second, true);
       }
     }
   | /* check-sat */
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index 8e29c25f1..71c1de2fa 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -121,6 +121,8 @@ using namespace CVC4::parser;
 #define PARSER_STATE ((Tptp*)PARSER->super)
 #undef SOLVER
 #define SOLVER PARSER_STATE->getSolver()
+#undef SYM_MAN
+#define SYM_MAN PARSER_STATE->getSymbolManager()
 #undef MK_TERM
 #define MK_TERM SOLVER->mkTerm
 #define UNSUPPORTED PARSER_STATE->unimplementedFeature
@@ -164,9 +166,7 @@ parseCommand returns [CVC4::Command* cmd = NULL]
       CVC4::api::Term aexpr = PARSER_STATE->getAssertionExpr(fr, expr);
       if( !aexpr.isNull() ){
         // set the expression name (e.g. used with unsat core printing)
-        Command* csen = new SetExpressionNameCommand(aexpr, name);
-        csen->setMuted(true);
-        PARSER_STATE->preemptCommand(csen);
+        SYM_MAN->setExpressionName(aexpr, name, true);
       }
       // make the command to assert the formula
       cmd = PARSER_STATE->makeAssertCommand(fr, aexpr, /* cnf == */ true, true);
@@ -178,9 +178,7 @@ parseCommand returns [CVC4::Command* cmd = NULL]
       CVC4::api::Term aexpr = PARSER_STATE->getAssertionExpr(fr,expr);
       if( !aexpr.isNull() ){
         // set the expression name (e.g. used with unsat core printing)
-        Command* csen = new SetExpressionNameCommand(aexpr, name);
-        csen->setMuted(true);
-        PARSER_STATE->preemptCommand(csen);
+        SYM_MAN->setExpressionName(aexpr, name, true);
       }
       // make the command to assert the formula
       cmd = PARSER_STATE->makeAssertCommand(fr, aexpr, /* cnf == */ false, true);
@@ -194,9 +192,7 @@ parseCommand returns [CVC4::Command* cmd = NULL]
         CVC4::api::Term aexpr = PARSER_STATE->getAssertionExpr(fr,expr);
         if( !aexpr.isNull() ){
           // set the expression name (e.g. used with unsat core printing)
-          Command* csen = new SetExpressionNameCommand(aexpr, name);
-          csen->setMuted(true);
-          PARSER_STATE->preemptCommand(csen);
+          SYM_MAN->setExpressionName(aexpr, name, true);
         }
         // make the command to assert the formula
         cmd = PARSER_STATE->makeAssertCommand(fr, aexpr, /* cnf == */ false, true);
@@ -219,9 +215,7 @@ parseCommand returns [CVC4::Command* cmd = NULL]
         if (!aexpr.isNull())
         {
           // set the expression name (e.g. used with unsat core printing)
-          Command* csen = new SetExpressionNameCommand(aexpr, name);
-          csen->setMuted(true);
-          PARSER_STATE->preemptCommand(csen);
+          SYM_MAN->setExpressionName(aexpr, name, true);
         }
         // make the command to assert the formula
         cmd = PARSER_STATE->makeAssertCommand(
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index bed6a890b..9eb5569e3 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1319,15 +1319,20 @@ void Smt2Printer::toStream(std::ostream& out, const CommandStatus* s) const
 void Smt2Printer::toStream(std::ostream& out, const UnsatCore& core) const
 {
   out << "(" << std::endl;
-  SmtEngine * smt = core.getSmtEngine();
-  Assert(smt != NULL);
-  for(UnsatCore::const_iterator i = core.begin(); i != core.end(); ++i) {
-    std::string name;
-    if (smt->getExpressionName(*i,name)) {
-      // Named assertions always get printed
-      out << CVC4::quoteSymbol(name) << endl;
-    } else if (options::dumpUnsatCoresFull()) {
-      // Unnamed assertions only get printed if the option is set
+  if (core.useNames())
+  {
+    // use the names
+    const std::vector<std::string>& cnames = core.getCoreNames();
+    for (const std::string& cn : cnames)
+    {
+      out << CVC4::quoteSymbol(cn) << std::endl;
+    }
+  }
+  else
+  {
+    // otherwise, use the formulas
+    for (UnsatCore::const_iterator i = core.begin(); i != core.end(); ++i)
+    {
       out << *i << endl;
     }
   }
diff --git a/src/printer/tptp/tptp_printer.cpp b/src/printer/tptp/tptp_printer.cpp
index 92bbc52e8..c93f3593a 100644
--- a/src/printer/tptp/tptp_printer.cpp
+++ b/src/printer/tptp/tptp_printer.cpp
@@ -71,15 +71,20 @@ void TptpPrinter::toStream(std::ostream& out,
 void TptpPrinter::toStream(std::ostream& out, const UnsatCore& core) const
 {
   out << "% SZS output start UnsatCore " << std::endl;
-  SmtEngine * smt = core.getSmtEngine();
-  Assert(smt != NULL);
-  for(UnsatCore::const_iterator i = core.begin(); i != core.end(); ++i) {
-    std::string name;
-    if (smt->getExpressionName(*i, name)) {
-      // Named assertions always get printed
-      out << name << endl;
-    } else if (options::dumpUnsatCoresFull()) {
-      // Unnamed assertions only get printed if the option is set
+  if (core.useNames())
+  {
+    // use the names
+    const std::vector<std::string>& cnames = core.getCoreNames();
+    for (const std::string& cn : cnames)
+    {
+      out << cn << std::endl;
+    }
+  }
+  else
+  {
+    // otherwise, use the formulas
+    for (UnsatCore::const_iterator i = core.begin(); i != core.end(); ++i)
+    {
       out << *i << endl;
     }
   }
diff --git a/src/proof/unsat_core.cpp b/src/proof/unsat_core.cpp
index cfa6dfb59..dd470b299 100644
--- a/src/proof/unsat_core.cpp
+++ b/src/proof/unsat_core.cpp
@@ -10,8 +10,6 @@
  ** directory for licensing information.\endverbatim
  **
  ** \brief Representation of unsat cores
- **
- ** Representation of unsat cores.
  **/
 
 #include "proof/unsat_core.h"
@@ -24,10 +22,24 @@
 
 namespace CVC4 {
 
-void UnsatCore::initMessage() const {
+UnsatCore::UnsatCore(const std::vector<Node>& core)
+    : d_useNames(false), d_core(core), d_names()
+{
   Debug("core") << "UnsatCore size " << d_core.size() << std::endl;
 }
 
+UnsatCore::UnsatCore(std::vector<std::string>& names)
+    : d_useNames(true), d_core(), d_names(names)
+{
+  Debug("core") << "UnsatCore (names) size " << d_names.size() << std::endl;
+}
+
+const std::vector<Node>& UnsatCore::getCore() const { return d_core; }
+const std::vector<std::string>& UnsatCore::getCoreNames() const
+{
+  return d_names;
+}
+
 UnsatCore::const_iterator UnsatCore::begin() const {
   return d_core.begin();
 }
@@ -37,8 +49,6 @@ UnsatCore::const_iterator UnsatCore::end() const {
 }
 
 void UnsatCore::toStream(std::ostream& out) const {
-  Assert(d_smt != NULL);
-  smt::SmtScope smts(d_smt);
   expr::ExprDag::Scope scope(out, false);
   Printer::getPrinter(options::outputLanguage())->toStream(out, *this);
 }
diff --git a/src/proof/unsat_core.h b/src/proof/unsat_core.h
index b0e3de24e..fb3401876 100644
--- a/src/proof/unsat_core.h
+++ b/src/proof/unsat_core.h
@@ -9,10 +9,7 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
+ ** \brief Representation of unsat cores.
  **/
 
 #include "cvc4_private.h"
@@ -27,44 +24,45 @@
 
 namespace CVC4 {
 
-class SmtEngine;
-
+/**
+ * An unsat core, which can optionally be initialized as a list of names
+ * or as a list of formulas.
+ */
 class UnsatCore
 {
-  /** The SmtEngine we're associated with */
-  SmtEngine* d_smt;
-
-  std::vector<Node> d_core;
-
-  void initMessage() const;
-
-public:
-  UnsatCore() : d_smt(NULL) {}
-
-  UnsatCore(SmtEngine* smt, const std::vector<Node>& core)
-      : d_smt(smt), d_core(core)
-  {
-    initMessage();
-  }
-
+ public:
+  UnsatCore() {}
+  /** Initialize using assertions */
+  UnsatCore(const std::vector<Node>& core);
+  /** Initialize using assertion names */
+  UnsatCore(std::vector<std::string>& names);
   ~UnsatCore() {}
 
-  /** get the smt engine that this unsat core is hooked up to */
-  SmtEngine* getSmtEngine() const { return d_smt; }
-
-  size_t size() const { return d_core.size(); }
+  /** Whether we are using names for this unsat core */
+  bool useNames() const { return d_useNames; }
+  /** Get the assertions in the unsat core */
+  const std::vector<Node>& getCore() const;
+  /** Get their names */
+  const std::vector<std::string>& getCoreNames() const;
 
   typedef std::vector<Node>::const_iterator iterator;
   typedef std::vector<Node>::const_iterator const_iterator;
 
   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
-  */
+
+  /**
+   * prints this UnsatCore object to the stream out.
+   */
   void toStream(std::ostream& out) const;
 
+ private:
+  /** Whether we are using names for this unsat core */
+  bool d_useNames;
+  /** The unsat core */
+  std::vector<Node> d_core;
+  /** The names of assertions in the above core */
+  std::vector<std::string> d_names;
 };/* class UnsatCore */
 
 /** Print the unsat core to stream out */
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index c8362fae1..717d423fe 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -2289,12 +2289,12 @@ void GetUnsatAssumptionsCommand::toStream(std::ostream& out,
 /* class GetUnsatCoreCommand                                                  */
 /* -------------------------------------------------------------------------- */
 
-GetUnsatCoreCommand::GetUnsatCoreCommand() {}
+GetUnsatCoreCommand::GetUnsatCoreCommand() : d_sm(nullptr) {}
 void GetUnsatCoreCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
-    d_solver = solver;
+    d_sm = sm;
     d_result = solver->getUnsatCore();
 
     d_commandStatus = CommandSuccess::instance();
@@ -2318,8 +2318,20 @@ void GetUnsatCoreCommand::printResult(std::ostream& out,
   }
   else
   {
-    UnsatCore ucr(d_solver->getSmtEngine(), api::termVectorToNodes(d_result));
-    ucr.toStream(out);
+    if (options::dumpUnsatCoresFull())
+    {
+      // use the assertions
+      UnsatCore ucr(api::termVectorToNodes(d_result));
+      ucr.toStream(out);
+    }
+    else
+    {
+      // otherwise, use the names
+      std::vector<std::string> names;
+      d_sm->getExpressionNames(d_result, names, true);
+      UnsatCore ucr(names);
+      ucr.toStream(out);
+    }
   }
 }
 
@@ -2332,7 +2344,7 @@ const std::vector<api::Term>& GetUnsatCoreCommand::getUnsatCore() const
 Command* GetUnsatCoreCommand::clone() const
 {
   GetUnsatCoreCommand* c = new GetUnsatCoreCommand;
-  c->d_solver = d_solver;
+  c->d_sm = d_sm;
   c->d_result = d_result;
   return c;
 }
@@ -2710,42 +2722,6 @@ void GetOptionCommand::toStream(std::ostream& out,
 }
 
 /* -------------------------------------------------------------------------- */
-/* class SetExpressionNameCommand                                             */
-/* -------------------------------------------------------------------------- */
-
-SetExpressionNameCommand::SetExpressionNameCommand(api::Term term,
-                                                   std::string name)
-    : d_term(term), d_name(name)
-{
-}
-
-void SetExpressionNameCommand::invoke(api::Solver* solver, SymbolManager* sm)
-{
-  solver->getSmtEngine()->setExpressionName(d_term.getExpr(), d_name);
-  d_commandStatus = CommandSuccess::instance();
-}
-
-Command* SetExpressionNameCommand::clone() const
-{
-  SetExpressionNameCommand* c = new SetExpressionNameCommand(d_term, d_name);
-  return c;
-}
-
-std::string SetExpressionNameCommand::getCommandName() const
-{
-  return "set-expr-name";
-}
-
-void SetExpressionNameCommand::toStream(std::ostream& out,
-                                        int toDepth,
-                                        size_t dag,
-                                        OutputLanguage language) const
-{
-  Printer::getPrinter(language)->toStreamCmdSetExpressionName(
-      out, d_term.getNode(), d_name);
-}
-
-/* -------------------------------------------------------------------------- */
 /* class DatatypeDeclarationCommand                                           */
 /* -------------------------------------------------------------------------- */
 
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:
diff --git a/src/smt/expr_names.cpp b/src/smt/expr_names.cpp
deleted file mode 100644
index ccced2cac..000000000
--- a/src/smt/expr_names.cpp
+++ /dev/null
@@ -1,39 +0,0 @@
-/*********************                                                        */
-/*! \file expr_names.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Utility for maintaining expression names.
- **/
-
-#include "smt/expr_names.h"
-
-namespace CVC4 {
-namespace smt {
-
-ExprNames::ExprNames(context::UserContext* u)
-    : d_exprNames(u)
-{
-}
-
-void ExprNames::setExpressionName(const Node& e, const std::string& name) {
-  d_exprNames[e] = name;
-}
-
-bool ExprNames::getExpressionName(const Node& e, std::string& name) const {
-  auto it = d_exprNames.find(e);
-  if(it!=d_exprNames.end()) {
-    name = (*it).second;
-    return true;
-  }
-  return false;
-}
-
-}  // namespace smt
-}  // namespace CVC4
diff --git a/src/smt/expr_names.h b/src/smt/expr_names.h
deleted file mode 100644
index 9a13b0c08..000000000
--- a/src/smt/expr_names.h
+++ /dev/null
@@ -1,59 +0,0 @@
-/*********************                                                        */
-/*! \file expr_names.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Aina Niemetz, Kshitij Bansal
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Utility for maintaining expression names.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef CVC4__SMT__EXPR_NAMES_H
-#define CVC4__SMT__EXPR_NAMES_H
-
-#include <string>
-
-#include "context/cdhashmap.h"
-#include "expr/node.h"
-
-namespace CVC4 {
-namespace smt {
-
-/**
- * This utility is responsible for maintaining names for expressions.
- */
-class ExprNames
-{
- public:
-  ExprNames(context::UserContext* u);
-  /**
-   * Get expression name.
-   *
-   * Return true if given expression has a name in the current context.
-   * If it returns true, the name of expression 'e' is stored in 'name'.
-   */
-  bool getExpressionName(const Node& e, std::string& name) const;
-
-  /**
-   * Set name of given expression 'e' to 'name'.
-   *
-   * This information is user-context-dependent.
-   * If 'e' already has a name, it is overwritten.
-   */
-  void setExpressionName(const Node& e, const std::string& name);
-
- private:
-  /** mapping from expressions to name */
-  context::CDHashMap< Node, std::string, NodeHashFunction > d_exprNames;
-};
-
-}  // namespace smt
-}  // namespace CVC4
-
-#endif
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 8aad05235..27bcdc036 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -38,7 +38,6 @@
 #include "smt/check_models.h"
 #include "smt/defined_function.h"
 #include "smt/dump_manager.h"
-#include "smt/expr_names.h"
 #include "smt/interpolation_solver.h"
 #include "smt/listeners.h"
 #include "smt/logic_request.h"
@@ -80,7 +79,6 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr)
       d_nodeManager(d_exprManager->getNodeManager()),
       d_absValues(new AbstractValues(d_nodeManager)),
       d_asserts(new Assertions(getUserContext(), *d_absValues.get())),
-      d_exprNames(new ExprNames(getUserContext())),
       d_dumpm(new DumpManager(getUserContext())),
       d_routListener(new ResourceOutListener(*this)),
       d_snmListener(new SmtNodeManagerListener(*d_dumpm.get(), d_outMgr)),
@@ -334,7 +332,6 @@ SmtEngine::~SmtEngine()
 
     d_absValues.reset(nullptr);
     d_asserts.reset(nullptr);
-    d_exprNames.reset(nullptr);
     d_dumpm.reset(nullptr);
 
     d_sygusSolver.reset(nullptr);
@@ -1391,7 +1388,7 @@ UnsatCore SmtEngine::getUnsatCoreInternal()
   }
 
   d_proofManager->traceUnsatCore();  // just to trigger core creation
-  return UnsatCore(this, d_proofManager->extractUnsatCore());
+  return UnsatCore(d_proofManager->extractUnsatCore());
 #else  /* IS_PROOFS_BUILD */
   throw ModalException(
       "This build of CVC4 doesn't have proof support (required for unsat "
@@ -1418,7 +1415,8 @@ void SmtEngine::checkUnsatCore() {
     coreChecker->declareSepHeap(sepLocType, sepDataType);
   }
 
-  Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions (size == " << core.size() << ")" << endl;
+  Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions"
+           << std::endl;
   for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) {
     Node assertionAfterExpansion = expandDefinitions(*i);
     Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i
@@ -1857,15 +1855,6 @@ CVC4::SExpr SmtEngine::getOption(const std::string& key) const
   return SExpr::parseAtom(d_options.getOption(key));
 }
 
-bool SmtEngine::getExpressionName(const Node& e, std::string& name) const {
-  return d_exprNames->getExpressionName(e, name);
-}
-
-void SmtEngine::setExpressionName(const Node& e, const std::string& name) {
-  Trace("smt-debug") << "Set expression name " << e << " to " << name << std::endl;
-  d_exprNames->setExpressionName(e,name);
-}
-
 Options& SmtEngine::getOptions() { return d_options; }
 
 const Options& SmtEngine::getOptions() const { return d_options; }
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index d8d2ea171..6c721b9b0 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -822,22 +822,6 @@ class CVC4_PUBLIC SmtEngine
                         const std::vector<Expr>& expr_values,
                         const std::string& str_value);
 
-  /**
-   * Get expression name.
-   *
-   * Return true if given expressoion has a name in the current context.
-   * If it returns true, the name of expression 'e' is stored in 'name'.
-   */
-  bool getExpressionName(const Node& e, std::string& name) const;
-
-  /**
-   * Set name of given expression 'e' to 'name'.
-   *
-   * This information is user-context-dependent.
-   * If 'e' already has a name, it is overwritten.
-   */
-  void setExpressionName(const Node& e, const std::string& name);
-
   /** Get the options object (const and non-const versions) */
   Options& getOptions();
   const Options& getOptions() const;
@@ -1049,8 +1033,6 @@ class CVC4_PUBLIC SmtEngine
   std::unique_ptr<smt::AbstractValues> d_absValues;
   /** Assertions manager */
   std::unique_ptr<smt::Assertions> d_asserts;
-  /** Expression names */
-  std::unique_ptr<smt::ExprNames> d_exprNames;
   /** The dump manager */
   std::unique_ptr<smt::DumpManager> d_dumpm;
   /** Resource out listener */