From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 11 Nov 2020 18:56:03 +0000 (-0600)
Subject: Move symbol manager to src/expr/ (#5420)
X-Git-Tag: cvc5-1.0.0~2613
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=80930ce4f6d21b417028a5ec207ddfbd7d85e66d;p=cvc5.git

Move symbol manager to src/expr/ (#5420)

This is required since symbol manager will use context dependent data structures (in its cpp).

This is required since classes in src/parser/ are not allowed to include private headers.
---

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 1a06e9366..c1e39f47e 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -1128,6 +1128,7 @@ install(FILES
           expr/expr_iomanip.h
           expr/record.h
           expr/sequence.h
+          expr/symbol_manager.h
           expr/symbol_table.h
           expr/type.h
           expr/uninterpreted_constant.h
@@ -1151,7 +1152,6 @@ install(FILES
           parser/parser_builder.h
           parser/parser_exception.h
           parser/parse_op.h
-          parser/symbol_manager.h
         DESTINATION
           ${CMAKE_INSTALL_INCLUDEDIR}/cvc4/parser)
 install(FILES
diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index d7af52fec..fb3df5327 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -76,6 +76,8 @@ libcvc4_add_sources(
   proof_step_buffer.h
   skolem_manager.cpp
   skolem_manager.h
+  symbol_manager.cpp
+  symbol_manager.h
   symbol_table.cpp
   symbol_table.h
   tconv_seq_proof_generator.cpp
diff --git a/src/expr/symbol_manager.cpp b/src/expr/symbol_manager.cpp
new file mode 100644
index 000000000..ac3b5d211
--- /dev/null
+++ b/src/expr/symbol_manager.cpp
@@ -0,0 +1,75 @@
+/*********************                                                        */
+/*! \file symbol_manager.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 The symbol manager
+ **/
+
+#include "expr/symbol_manager.h"
+
+namespace CVC4 {
+
+SymbolManager::SymbolManager(api::Solver* s) : d_solver(s) {}
+
+SymbolTable* SymbolManager::getSymbolTable() { return &d_symtabAllocated; }
+
+bool SymbolManager::setExpressionName(api::Term t,
+                                      const std::string& name,
+                                      bool isAssertion)
+{
+  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;
+}
+
+bool SymbolManager::getExpressionName(api::Term t,
+                                      std::string& name,
+                                      bool isAssertion) const
+{
+  std::map<api::Term, std::string>::const_iterator it = d_names.find(t);
+  if (it == d_names.end())
+  {
+    return false;
+  }
+  if (isAssertion)
+  {
+    // must be an assertion name
+    if (d_namedAsserts.find(t) == d_namedAsserts.end())
+    {
+      return false;
+    }
+  }
+  name = it->second;
+  return true;
+}
+
+void SymbolManager::getExpressionNames(const std::vector<api::Term>& ts,
+                                       std::vector<std::string>& names,
+                                       bool areAssertions) const
+{
+  for (const api::Term& t : ts)
+  {
+    std::string name;
+    if (getExpressionName(t, name, areAssertions))
+    {
+      names.push_back(name);
+    }
+  }
+}
+
+}  // namespace CVC4
diff --git a/src/expr/symbol_manager.h b/src/expr/symbol_manager.h
new file mode 100644
index 000000000..4890ed994
--- /dev/null
+++ b/src/expr/symbol_manager.h
@@ -0,0 +1,103 @@
+/*********************                                                        */
+/*! \file symbol_manager.h
+ ** \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 The symbol manager
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef CVC4__EXPR__SYMBOL_MANAGER_H
+#define CVC4__EXPR__SYMBOL_MANAGER_H
+
+#include <map>
+#include <set>
+#include <string>
+
+#include "api/cvc4cpp.h"
+#include "expr/symbol_table.h"
+
+namespace CVC4 {
+
+/**
+ * Symbol manager, which manages:
+ * (1) The symbol table used by the parser,
+ * (2) Information related to the (! ... :named s) feature in SMT-LIB version 2.
+ *
+ * Like SymbolTable, this class currently lives in src/expr/ since it uses
+ * context-dependent data structures.
+ */
+class CVC4_PUBLIC SymbolManager
+{
+ public:
+  SymbolManager(api::Solver* s);
+  ~SymbolManager() {}
+  /** Get the underlying symbol table */
+  SymbolTable* getSymbolTable();
+  //---------------------------- named expressions
+  /** Set name of term t to name
+   *
+   * @param t The term to name
+   * @param name The given name
+   * @param isAssertion Whether t is being given a name in an assertion
+   * context. In particular, this is true if and only if there was an assertion
+   * command of the form (assert (! t :named name)).
+   * @return true if the name was set. This method may return false if t
+   * already has a name.
+   */
+  bool setExpressionName(api::Term t,
+                         const std::string& name,
+                         bool isAssertion = false);
+  /** Get name for term t
+   *
+   * @param t The term
+   * @param name The argument to update with the name of t
+   * @param isAssertion Whether we only wish to get the assertion name of t
+   * @return true if t has a name. If so, name is updated to that name.
+   * Otherwise, name is unchanged.
+   */
+  bool getExpressionName(api::Term t,
+                         std::string& name,
+                         bool isAssertion = false) const;
+  /**
+   * Convert list of terms to list of names. This adds to names the names of
+   * all terms in ts that has names. Terms that do not have names are not
+   * included.
+   *
+   * Notice that we do not distinguish what terms among those in ts have names.
+   * If the caller of this method wants more fine-grained information about what
+   * specific terms had names, then use the more fine grained interface above,
+   * per term.
+   *
+   * @param ts The terms
+   * @param names The name list
+   * @param areAssertions Whether we only wish to include assertion names
+   */
+  void getExpressionNames(const std::vector<api::Term>& ts,
+                          std::vector<std::string>& names,
+                          bool areAssertions = false) const;
+  //---------------------------- end named expressions
+
+ private:
+  /** The API Solver object. */
+  api::Solver* d_solver;
+  /**
+   * The declaration scope that is "owned" by this symbol manager.
+   */
+  SymbolTable d_symtabAllocated;
+  /** Map terms to names */
+  std::map<api::Term, std::string> d_names;
+  /** The set of terms with assertion names */
+  std::set<api::Term> d_namedAsserts;
+};
+
+}  // namespace CVC4
+
+#endif /* CVC4__EXPR__SYMBOL_MANAGER_H */
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 7b20f3a1a..be90be3f0 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -50,7 +50,7 @@ void printStatsIncremental(std::ostream& out, const std::string& prvsStatsString
 
 CommandExecutor::CommandExecutor(Options& options)
     : d_solver(new api::Solver(&options)),
-      d_symman(new parser::SymbolManager(d_solver.get())),
+      d_symman(new SymbolManager(d_solver.get())),
       d_smtEngine(d_solver->getSmtEngine()),
       d_options(options),
       d_stats("driver"),
@@ -200,7 +200,7 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
 }
 
 bool solverInvoke(api::Solver* solver,
-                  parser::SymbolManager* sm,
+                  SymbolManager* sm,
                   Command* cmd,
                   std::ostream* out)
 {
diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index 87748b1e5..acf9e45bb 100644
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -20,8 +20,8 @@
 
 #include "api/cvc4cpp.h"
 #include "expr/expr_manager.h"
+#include "expr/symbol_manager.h"
 #include "options/options.h"
-#include "parser/symbol_manager.h"
 #include "smt/smt_engine.h"
 #include "util/statistics_registry.h"
 
@@ -52,7 +52,7 @@ class CommandExecutor
    * Certain commands (e.g. reset-assertions) have a specific impact on the
    * symbol manager.
    */
-  std::unique_ptr<parser::SymbolManager> d_symman;
+  std::unique_ptr<SymbolManager> d_symman;
   SmtEngine* d_smtEngine;
   Options& d_options;
   StatisticsRegistry d_stats;
@@ -80,7 +80,7 @@ class CommandExecutor
   api::Solver* getSolver() { return d_solver.get(); }
 
   /** Get a pointer to the symbol manager owned by this CommandExecutor */
-  parser::SymbolManager* getSymbolManager() { return d_symman.get(); }
+  SymbolManager* getSymbolManager() { return d_symman.get(); }
 
   api::Result getResult() const { return d_result; }
   void reset();
@@ -117,7 +117,7 @@ private:
 }; /* class CommandExecutor */
 
 bool solverInvoke(api::Solver* solver,
-                  parser::SymbolManager* sm,
+                  SymbolManager* sm,
                   Command* cmd,
                   std::ostream* out);
 
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 8d482b08e..3586fce87 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -38,12 +38,12 @@
 
 #include "api/cvc4cpp.h"
 #include "base/output.h"
+#include "expr/symbol_manager.h"
 #include "options/language.h"
 #include "options/options.h"
 #include "parser/input.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
-#include "parser/symbol_manager.h"
 #include "smt/command.h"
 #include "theory/logic_info.h"
 
@@ -84,8 +84,7 @@ static set<string> s_declarations;
 
 #endif /* HAVE_LIBEDITLINE */
 
-InteractiveShell::InteractiveShell(api::Solver* solver,
-                                   parser::SymbolManager* sm)
+InteractiveShell::InteractiveShell(api::Solver* solver, SymbolManager* sm)
     : d_options(solver->getOptions()),
       d_in(*d_options.getIn()),
       d_out(*d_options.getOutConst()),
diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h
index b00f8a8f4..4d60d3445 100644
--- a/src/main/interactive_shell.h
+++ b/src/main/interactive_shell.h
@@ -33,9 +33,10 @@ class Solver;
 
 namespace parser {
   class Parser;
-  class SymbolManager;
 }/* CVC4::parser namespace */
 
+class SymbolManager;
+
 class CVC4_PUBLIC InteractiveShell
 {
   const Options& d_options;
@@ -51,7 +52,7 @@ class CVC4_PUBLIC InteractiveShell
   static const unsigned s_historyLimit = 500;
 
 public:
- InteractiveShell(api::Solver* solver, parser::SymbolManager* sm);
+ InteractiveShell(api::Solver* solver, SymbolManager* sm);
 
  /**
   * Close out the interactive session.
diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt
index 7b55c0915..8e69da34b 100644
--- a/src/parser/CMakeLists.txt
+++ b/src/parser/CMakeLists.txt
@@ -55,8 +55,6 @@ set(libcvc4parser_src_files
   smt2/smt2_input.h
   smt2/sygus_input.cpp
   smt2/sygus_input.h
-  symbol_manager.cpp
-  symbol_manager.h
   tptp/TptpLexer.c
   tptp/TptpParser.c
   tptp/tptp.cpp
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 405935165..c762fc117 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -26,11 +26,11 @@
 
 #include "api/cvc4cpp.h"
 #include "expr/kind.h"
+#include "expr/symbol_manager.h"
 #include "expr/symbol_table.h"
 #include "parser/input.h"
 #include "parser/parse_op.h"
 #include "parser/parser_exception.h"
-#include "parser/symbol_manager.h"
 #include "util/unsafe_interrupt_exception.h"
 
 namespace CVC4 {
diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h
index 9d62c12a3..bf205b13a 100644
--- a/src/parser/parser_builder.h
+++ b/src/parser/parser_builder.h
@@ -26,16 +26,16 @@
 
 namespace CVC4 {
 
-class Options;
-
 namespace api {
 class Solver;
 }
 
+class Options;
+class SymbolManager;
+
 namespace parser {
 
 class Parser;
-class SymbolManager;
 
 /**
  * A builder for input language parsers. <code>build()</code> can be
diff --git a/src/parser/symbol_manager.cpp b/src/parser/symbol_manager.cpp
deleted file mode 100644
index 32e17aea8..000000000
--- a/src/parser/symbol_manager.cpp
+++ /dev/null
@@ -1,77 +0,0 @@
-/*********************                                                        */
-/*! \file symbol_manager.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 The symbol manager
- **/
-
-#include "parser/symbol_manager.h"
-
-namespace CVC4 {
-namespace parser {
-
-SymbolManager::SymbolManager(api::Solver* s) : d_solver(s) {}
-
-SymbolTable* SymbolManager::getSymbolTable() { return &d_symtabAllocated; }
-
-bool SymbolManager::setExpressionName(api::Term t,
-                                      const std::string& name,
-                                      bool isAssertion)
-{
-  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;
-}
-
-bool SymbolManager::getExpressionName(api::Term t,
-                                      std::string& name,
-                                      bool isAssertion) const
-{
-  std::map<api::Term, std::string>::const_iterator it = d_names.find(t);
-  if (it == d_names.end())
-  {
-    return false;
-  }
-  if (isAssertion)
-  {
-    // must be an assertion name
-    if (d_namedAsserts.find(t) == d_namedAsserts.end())
-    {
-      return false;
-    }
-  }
-  name = it->second;
-  return true;
-}
-
-void SymbolManager::getExpressionNames(const std::vector<api::Term>& ts,
-                                       std::vector<std::string>& names,
-                                       bool areAssertions) const
-{
-  for (const api::Term& t : ts)
-  {
-    std::string name;
-    if (getExpressionName(t, name, areAssertions))
-    {
-      names.push_back(name);
-    }
-  }
-}
-
-}  // namespace parser
-}  // namespace CVC4
diff --git a/src/parser/symbol_manager.h b/src/parser/symbol_manager.h
deleted file mode 100644
index 20b0c80e4..000000000
--- a/src/parser/symbol_manager.h
+++ /dev/null
@@ -1,102 +0,0 @@
-/*********************                                                        */
-/*! \file symbol_manager.h
- ** \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 The symbol manager
- **/
-
-#include "cvc4parser_public.h"
-
-#ifndef CVC4__PARSER__SYMBOL_MANAGER_H
-#define CVC4__PARSER__SYMBOL_MANAGER_H
-
-#include <map>
-#include <set>
-#include <string>
-
-#include "api/cvc4cpp.h"
-#include "expr/symbol_table.h"
-
-namespace CVC4 {
-namespace parser {
-
-/**
- * Symbol manager, which manages:
- * (1) The symbol table used by the parser,
- * (2) Information related to the (! ... :named s) feature in SMT-LIB version 2.
- */
-class CVC4_PUBLIC SymbolManager
-{
- public:
-  SymbolManager(api::Solver* s);
-  ~SymbolManager() {}
-  /** Get the underlying symbol table */
-  SymbolTable* getSymbolTable();
-  //---------------------------- named expressions
-  /** Set name of term t to name
-   *
-   * @param t The term to name
-   * @param name The given name
-   * @param isAssertion Whether t is being given a name in an assertion
-   * context. In particular, this is true if and only if there was an assertion
-   * command of the form (assert (! t :named name)).
-   * @return true if the name was set. This method may return false if t
-   * already has a name.
-   */
-  bool setExpressionName(api::Term t,
-                         const std::string& name,
-                         bool isAssertion = false);
-  /** Get name for term t
-   *
-   * @param t The term
-   * @param name The argument to update with the name of t
-   * @param isAssertion Whether we only wish to get the assertion name of t
-   * @return true if t has a name. If so, name is updated to that name.
-   * Otherwise, name is unchanged.
-   */
-  bool getExpressionName(api::Term t,
-                         std::string& name,
-                         bool isAssertion = false) const;
-  /**
-   * Convert list of terms to list of names. This adds to names the names of
-   * all terms in ts that has names. Terms that do not have names are not
-   * included.
-   *
-   * Notice that we do not distinguish what terms among those in ts have names.
-   * If the caller of this method wants more fine-grained information about what
-   * specific terms had names, then use the more fine grained interface above,
-   * per term.
-   *
-   * @param ts The terms
-   * @param names The name list
-   * @param areAssertions Whether we only wish to include assertion names
-   */
-  void getExpressionNames(const std::vector<api::Term>& ts,
-                          std::vector<std::string>& names,
-                          bool areAssertions = false) const;
-  //---------------------------- end named expressions
-
- private:
-  /** The API Solver object. */
-  api::Solver* d_solver;
-  /**
-   * The declaration scope that is "owned" by this symbol manager.
-   */
-  SymbolTable d_symtabAllocated;
-  /** Map terms to names */
-  std::map<api::Term, std::string> d_names;
-  /** The set of terms with assertion names */
-  std::set<api::Term> d_namedAsserts;
-};
-
-}  // namespace parser
-}  // namespace CVC4
-
-#endif /* CVC4__PARSER__SYMBOL_MANAGER_H */
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 68c776536..f1490e2f9 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -28,10 +28,10 @@
 #include "base/output.h"
 #include "expr/expr_iomanip.h"
 #include "expr/node.h"
+#include "expr/symbol_manager.h"
 #include "expr/type.h"
 #include "options/options.h"
 #include "options/smt_options.h"
-#include "parser/symbol_manager.h"
 #include "printer/printer.h"
 #include "proof/unsat_core.h"
 #include "smt/dump.h"
@@ -176,9 +176,7 @@ bool Command::interrupted() const
          && dynamic_cast<const CommandInterrupted*>(d_commandStatus) != NULL;
 }
 
-void Command::invoke(api::Solver* solver,
-                     parser::SymbolManager* sm,
-                     std::ostream& out)
+void Command::invoke(api::Solver* solver, SymbolManager* sm, std::ostream& out)
 {
   invoke(solver, sm);
   if (!(isMuted() && ok()))
@@ -218,7 +216,7 @@ void Command::printResult(std::ostream& out, uint32_t verbosity) const
 
 EmptyCommand::EmptyCommand(std::string name) : d_name(name) {}
 std::string EmptyCommand::getName() const { return d_name; }
-void EmptyCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void EmptyCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   /* empty commands have no implementation */
   d_commandStatus = CommandSuccess::instance();
@@ -241,14 +239,14 @@ void EmptyCommand::toStream(std::ostream& out,
 
 EchoCommand::EchoCommand(std::string output) : d_output(output) {}
 std::string EchoCommand::getOutput() const { return d_output; }
-void EchoCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void EchoCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   /* we don't have an output stream here, nothing to do */
   d_commandStatus = CommandSuccess::instance();
 }
 
 void EchoCommand::invoke(api::Solver* solver,
-                         parser::SymbolManager* sm,
+                         SymbolManager* sm,
                          std::ostream& out)
 {
   out << d_output << std::endl;
@@ -281,7 +279,7 @@ AssertCommand::AssertCommand(const api::Term& t, bool inUnsatCore)
 }
 
 api::Term AssertCommand::getTerm() const { return d_term; }
-void AssertCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void AssertCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
@@ -317,7 +315,7 @@ void AssertCommand::toStream(std::ostream& out,
 /* class PushCommand                                                          */
 /* -------------------------------------------------------------------------- */
 
-void PushCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void PushCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
@@ -349,7 +347,7 @@ void PushCommand::toStream(std::ostream& out,
 /* class PopCommand                                                           */
 /* -------------------------------------------------------------------------- */
 
-void PopCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void PopCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
@@ -386,7 +384,7 @@ CheckSatCommand::CheckSatCommand() : d_term() {}
 CheckSatCommand::CheckSatCommand(const api::Term& term) : d_term(term) {}
 
 api::Term CheckSatCommand::getTerm() const { return d_term; }
-void CheckSatCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void CheckSatCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   Trace("dtview::command") << "* ~COMMAND: " << getCommandName() << "~"
                            << std::endl;
@@ -454,8 +452,7 @@ const std::vector<api::Term>& CheckSatAssumingCommand::getTerms() const
   return d_terms;
 }
 
-void CheckSatAssumingCommand::invoke(api::Solver* solver,
-                                     parser::SymbolManager* sm)
+void CheckSatAssumingCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   Trace("dtview::command") << "* ~COMMAND: (check-sat-assuming ( " << d_terms
                            << " )~" << std::endl;
@@ -520,7 +517,7 @@ QueryCommand::QueryCommand(const api::Term& t, bool inUnsatCore)
 }
 
 api::Term QueryCommand::getTerm() const { return d_term; }
-void QueryCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void QueryCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
@@ -577,8 +574,7 @@ DeclareSygusVarCommand::DeclareSygusVarCommand(const std::string& id,
 api::Term DeclareSygusVarCommand::getVar() const { return d_var; }
 api::Sort DeclareSygusVarCommand::getSort() const { return d_sort; }
 
-void DeclareSygusVarCommand::invoke(api::Solver* solver,
-                                    parser::SymbolManager* sm)
+void DeclareSygusVarCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   d_commandStatus = CommandSuccess::instance();
 }
@@ -633,7 +629,7 @@ bool SynthFunCommand::isInv() const { return d_isInv; }
 
 const api::Grammar* SynthFunCommand::getGrammar() const { return d_grammar; }
 
-void SynthFunCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void SynthFunCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   d_commandStatus = CommandSuccess::instance();
 }
@@ -672,8 +668,7 @@ SygusConstraintCommand::SygusConstraintCommand(const api::Term& t) : d_term(t)
 {
 }
 
-void SygusConstraintCommand::invoke(api::Solver* solver,
-                                    parser::SymbolManager* sm)
+void SygusConstraintCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
@@ -724,8 +719,7 @@ SygusInvConstraintCommand::SygusInvConstraintCommand(const api::Term& inv,
 {
 }
 
-void SygusInvConstraintCommand::invoke(api::Solver* solver,
-                                       parser::SymbolManager* sm)
+void SygusInvConstraintCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
@@ -771,7 +765,7 @@ void SygusInvConstraintCommand::toStream(std::ostream& out,
 /* class CheckSynthCommand                                                    */
 /* -------------------------------------------------------------------------- */
 
-void CheckSynthCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void CheckSynthCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
@@ -839,7 +833,7 @@ void CheckSynthCommand::toStream(std::ostream& out,
 /* class ResetCommand                                                         */
 /* -------------------------------------------------------------------------- */
 
-void ResetCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void ResetCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
@@ -867,8 +861,7 @@ void ResetCommand::toStream(std::ostream& out,
 /* class ResetAssertionsCommand                                               */
 /* -------------------------------------------------------------------------- */
 
-void ResetAssertionsCommand::invoke(api::Solver* solver,
-                                    parser::SymbolManager* sm)
+void ResetAssertionsCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
@@ -903,7 +896,7 @@ void ResetAssertionsCommand::toStream(std::ostream& out,
 /* class QuitCommand                                                          */
 /* -------------------------------------------------------------------------- */
 
-void QuitCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void QuitCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   Dump("benchmark") << *this;
   d_commandStatus = CommandSuccess::instance();
@@ -926,7 +919,7 @@ void QuitCommand::toStream(std::ostream& out,
 
 CommentCommand::CommentCommand(std::string comment) : d_comment(comment) {}
 std::string CommentCommand::getComment() const { return d_comment; }
-void CommentCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void CommentCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   Dump("benchmark") << *this;
   d_commandStatus = CommandSuccess::instance();
@@ -962,7 +955,7 @@ void CommandSequence::addCommand(Command* cmd)
 }
 
 void CommandSequence::clear() { d_commandSequence.clear(); }
-void CommandSequence::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void CommandSequence::invoke(api::Solver* solver, SymbolManager* sm)
 {
   for (; d_index < d_commandSequence.size(); ++d_index)
   {
@@ -981,7 +974,7 @@ void CommandSequence::invoke(api::Solver* solver, parser::SymbolManager* sm)
 }
 
 void CommandSequence::invoke(api::Solver* solver,
-                             parser::SymbolManager* sm,
+                             SymbolManager* sm,
                              std::ostream& out)
 {
   for (; d_index < d_commandSequence.size(); ++d_index)
@@ -1096,8 +1089,7 @@ void DeclareFunctionCommand::setPrintInModel(bool p)
   d_printInModelSetByUser = true;
 }
 
-void DeclareFunctionCommand::invoke(api::Solver* solver,
-                                    parser::SymbolManager* sm)
+void DeclareFunctionCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   d_commandStatus = CommandSuccess::instance();
 }
@@ -1138,7 +1130,7 @@ DeclareSortCommand::DeclareSortCommand(const std::string& id,
 
 size_t DeclareSortCommand::getArity() const { return d_arity; }
 api::Sort DeclareSortCommand::getSort() const { return d_sort; }
-void DeclareSortCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void DeclareSortCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   d_commandStatus = CommandSuccess::instance();
 }
@@ -1184,7 +1176,7 @@ const std::vector<api::Sort>& DefineSortCommand::getParameters() const
 }
 
 api::Sort DefineSortCommand::getSort() const { return d_sort; }
-void DefineSortCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void DefineSortCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   d_commandStatus = CommandSuccess::instance();
 }
@@ -1245,8 +1237,7 @@ const std::vector<api::Term>& DefineFunctionCommand::getFormals() const
 }
 
 api::Term DefineFunctionCommand::getFormula() const { return d_formula; }
-void DefineFunctionCommand::invoke(api::Solver* solver,
-                                   parser::SymbolManager* sm)
+void DefineFunctionCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
@@ -1301,8 +1292,7 @@ DefineNamedFunctionCommand::DefineNamedFunctionCommand(
 {
 }
 
-void DefineNamedFunctionCommand::invoke(api::Solver* solver,
-                                        parser::SymbolManager* sm)
+void DefineNamedFunctionCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   this->DefineFunctionCommand::invoke(solver, sm);
   if (!d_func.isNull() && d_func.getSort().isBoolean())
@@ -1374,8 +1364,7 @@ const std::vector<api::Term>& DefineFunctionRecCommand::getFormulas() const
   return d_formulas;
 }
 
-void DefineFunctionRecCommand::invoke(api::Solver* solver,
-                                      parser::SymbolManager* sm)
+void DefineFunctionRecCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
@@ -1427,7 +1416,7 @@ DeclareHeapCommand::DeclareHeapCommand(api::Sort locSort, api::Sort dataSort)
 api::Sort DeclareHeapCommand::getLocationSort() const { return d_locSort; }
 api::Sort DeclareHeapCommand::getDataSort() const { return d_dataSort; }
 
-void DeclareHeapCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void DeclareHeapCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   solver->declareSeparationHeap(d_locSort, d_dataSort);
 }
@@ -1485,8 +1474,7 @@ SetUserAttributeCommand::SetUserAttributeCommand(const std::string& attr,
 {
 }
 
-void SetUserAttributeCommand::invoke(api::Solver* solver,
-                                     parser::SymbolManager* sm)
+void SetUserAttributeCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
@@ -1531,7 +1519,7 @@ void SetUserAttributeCommand::toStream(std::ostream& out,
 
 SimplifyCommand::SimplifyCommand(api::Term term) : d_term(term) {}
 api::Term SimplifyCommand::getTerm() const { return d_term; }
-void SimplifyCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void SimplifyCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
@@ -1598,7 +1586,7 @@ const std::vector<api::Term>& GetValueCommand::getTerms() const
 {
   return d_terms;
 }
-void GetValueCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void GetValueCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
@@ -1664,8 +1652,7 @@ void GetValueCommand::toStream(std::ostream& out,
 /* -------------------------------------------------------------------------- */
 
 GetAssignmentCommand::GetAssignmentCommand() {}
-void GetAssignmentCommand::invoke(api::Solver* solver,
-                                  parser::SymbolManager* sm)
+void GetAssignmentCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
@@ -1735,7 +1722,7 @@ void GetAssignmentCommand::toStream(std::ostream& out,
 /* -------------------------------------------------------------------------- */
 
 GetModelCommand::GetModelCommand() : d_result(nullptr) {}
-void GetModelCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void GetModelCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
@@ -1796,7 +1783,7 @@ void GetModelCommand::toStream(std::ostream& out,
 /* -------------------------------------------------------------------------- */
 
 BlockModelCommand::BlockModelCommand() {}
-void BlockModelCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void BlockModelCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
@@ -1850,8 +1837,7 @@ const std::vector<api::Term>& BlockModelValuesCommand::getTerms() const
 {
   return d_terms;
 }
-void BlockModelValuesCommand::invoke(api::Solver* solver,
-                                     parser::SymbolManager* sm)
+void BlockModelValuesCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
@@ -1897,7 +1883,7 @@ void BlockModelValuesCommand::toStream(std::ostream& out,
 /* -------------------------------------------------------------------------- */
 
 GetProofCommand::GetProofCommand() {}
-void GetProofCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void GetProofCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   Unimplemented() << "Unimplemented get-proof\n";
 }
@@ -1923,8 +1909,7 @@ void GetProofCommand::toStream(std::ostream& out,
 /* -------------------------------------------------------------------------- */
 
 GetInstantiationsCommand::GetInstantiationsCommand() : d_solver(nullptr) {}
-void GetInstantiationsCommand::invoke(api::Solver* solver,
-                                      parser::SymbolManager* sm)
+void GetInstantiationsCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
@@ -1976,8 +1961,7 @@ void GetInstantiationsCommand::toStream(std::ostream& out,
 /* -------------------------------------------------------------------------- */
 
 GetSynthSolutionCommand::GetSynthSolutionCommand() : d_solver(nullptr) {}
-void GetSynthSolutionCommand::invoke(api::Solver* solver,
-                                     parser::SymbolManager* sm)
+void GetSynthSolutionCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
@@ -2047,7 +2031,7 @@ const api::Grammar* GetInterpolCommand::getGrammar() const
 
 api::Term GetInterpolCommand::getResult() const { return d_result; }
 
-void GetInterpolCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void GetInterpolCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
@@ -2138,7 +2122,7 @@ const api::Grammar* GetAbductCommand::getGrammar() const
 std::string GetAbductCommand::getAbductName() const { return d_name; }
 api::Term GetAbductCommand::getResult() const { return d_result; }
 
-void GetAbductCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void GetAbductCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
@@ -2215,7 +2199,7 @@ GetQuantifierEliminationCommand::GetQuantifierEliminationCommand(
 api::Term GetQuantifierEliminationCommand::getTerm() const { return d_term; }
 bool GetQuantifierEliminationCommand::getDoFull() const { return d_doFull; }
 void GetQuantifierEliminationCommand::invoke(api::Solver* solver,
-                                             parser::SymbolManager* sm)
+                                             SymbolManager* sm)
 {
   try
   {
@@ -2280,8 +2264,7 @@ void GetQuantifierEliminationCommand::toStream(std::ostream& out,
 
 GetUnsatAssumptionsCommand::GetUnsatAssumptionsCommand() {}
 
-void GetUnsatAssumptionsCommand::invoke(api::Solver* solver,
-                                        parser::SymbolManager* sm)
+void GetUnsatAssumptionsCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
@@ -2341,7 +2324,7 @@ void GetUnsatAssumptionsCommand::toStream(std::ostream& out,
 /* -------------------------------------------------------------------------- */
 
 GetUnsatCoreCommand::GetUnsatCoreCommand() {}
-void GetUnsatCoreCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void GetUnsatCoreCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
@@ -2406,8 +2389,7 @@ void GetUnsatCoreCommand::toStream(std::ostream& out,
 /* -------------------------------------------------------------------------- */
 
 GetAssertionsCommand::GetAssertionsCommand() {}
-void GetAssertionsCommand::invoke(api::Solver* solver,
-                                  parser::SymbolManager* sm)
+void GetAssertionsCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
@@ -2473,8 +2455,7 @@ BenchmarkStatus SetBenchmarkStatusCommand::getStatus() const
   return d_status;
 }
 
-void SetBenchmarkStatusCommand::invoke(api::Solver* solver,
-                                       parser::SymbolManager* sm)
+void SetBenchmarkStatusCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
@@ -2525,8 +2506,7 @@ SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic)
 }
 
 std::string SetBenchmarkLogicCommand::getLogic() const { return d_logic; }
-void SetBenchmarkLogicCommand::invoke(api::Solver* solver,
-                                      parser::SymbolManager* sm)
+void SetBenchmarkLogicCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
@@ -2568,7 +2548,7 @@ SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr)
 
 std::string SetInfoCommand::getFlag() const { return d_flag; }
 SExpr SetInfoCommand::getSExpr() const { return d_sexpr; }
-void SetInfoCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void SetInfoCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
@@ -2607,7 +2587,7 @@ void SetInfoCommand::toStream(std::ostream& out,
 
 GetInfoCommand::GetInfoCommand(std::string flag) : d_flag(flag) {}
 std::string GetInfoCommand::getFlag() const { return d_flag; }
-void GetInfoCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void GetInfoCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
@@ -2678,7 +2658,7 @@ SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr)
 
 std::string SetOptionCommand::getFlag() const { return d_flag; }
 SExpr SetOptionCommand::getSExpr() const { return d_sexpr; }
-void SetOptionCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void SetOptionCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
@@ -2716,7 +2696,7 @@ void SetOptionCommand::toStream(std::ostream& out,
 
 GetOptionCommand::GetOptionCommand(std::string flag) : d_flag(flag) {}
 std::string GetOptionCommand::getFlag() const { return d_flag; }
-void GetOptionCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
+void GetOptionCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
@@ -2773,8 +2753,7 @@ SetExpressionNameCommand::SetExpressionNameCommand(api::Term term,
 {
 }
 
-void SetExpressionNameCommand::invoke(api::Solver* solver,
-                                      parser::SymbolManager* sm)
+void SetExpressionNameCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   solver->getSmtEngine()->setExpressionName(d_term.getExpr(), d_name);
   d_commandStatus = CommandSuccess::instance();
@@ -2822,8 +2801,7 @@ const std::vector<api::Sort>& DatatypeDeclarationCommand::getDatatypes() const
   return d_datatypes;
 }
 
-void DatatypeDeclarationCommand::invoke(api::Solver* solver,
-                                        parser::SymbolManager* sm)
+void DatatypeDeclarationCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   d_commandStatus = CommandSuccess::instance();
 }
diff --git a/src/smt/command.h b/src/smt/command.h
index 310850b78..7d794cf3f 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -41,10 +41,7 @@ class Solver;
 class Term;
 }  // namespace api
 
-namespace parser {
 class SymbolManager;
-}
-
 class UnsatCore;
 class SmtEngine;
 class Command;
@@ -209,12 +206,12 @@ class CVC4_PUBLIC Command
   /**
    * Invoke the command on the solver and symbol manager sm.
    */
-  virtual void invoke(api::Solver* solver, parser::SymbolManager* sm) = 0;
+  virtual void invoke(api::Solver* solver, SymbolManager* sm) = 0;
   /**
    * Same as above, and prints the result to output stream out.
    */
   virtual void invoke(api::Solver* solver,
-                      parser::SymbolManager* sm,
+                      SymbolManager* sm,
                       std::ostream& out);
 
   virtual void toStream(
@@ -288,7 +285,7 @@ class CVC4_PUBLIC EmptyCommand : public Command
  public:
   EmptyCommand(std::string name = "");
   std::string getName() const;
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
@@ -308,9 +305,9 @@ class CVC4_PUBLIC EchoCommand : public Command
 
   std::string getOutput() const;
 
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   void invoke(api::Solver* solver,
-              parser::SymbolManager* sm,
+              SymbolManager* sm,
               std::ostream& out) override;
 
   Command* clone() const override;
@@ -336,7 +333,7 @@ class CVC4_PUBLIC AssertCommand : public Command
 
   api::Term getTerm() const;
 
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
 
   Command* clone() const override;
   std::string getCommandName() const override;
@@ -350,7 +347,7 @@ class CVC4_PUBLIC AssertCommand : public Command
 class CVC4_PUBLIC PushCommand : public Command
 {
  public:
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
@@ -363,7 +360,7 @@ class CVC4_PUBLIC PushCommand : public Command
 class CVC4_PUBLIC PopCommand : public Command
 {
  public:
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
@@ -381,7 +378,7 @@ class CVC4_PUBLIC DeclarationDefinitionCommand : public Command
  public:
   DeclarationDefinitionCommand(const std::string& id);
 
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override = 0;
+  void invoke(api::Solver* solver, SymbolManager* sm) override = 0;
   std::string getSymbol() const;
 }; /* class DeclarationDefinitionCommand */
 
@@ -401,7 +398,7 @@ class CVC4_PUBLIC DeclareFunctionCommand : public DeclarationDefinitionCommand
   bool getPrintInModelSetByUser() const;
   void setPrintInModel(bool p);
 
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
@@ -423,7 +420,7 @@ class CVC4_PUBLIC DeclareSortCommand : public DeclarationDefinitionCommand
   size_t getArity() const;
   api::Sort getSort() const;
 
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
@@ -448,7 +445,7 @@ class CVC4_PUBLIC DefineSortCommand : public DeclarationDefinitionCommand
   const std::vector<api::Sort>& getParameters() const;
   api::Sort getSort() const;
 
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
@@ -475,7 +472,7 @@ class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand
   const std::vector<api::Term>& getFormals() const;
   api::Term getFormula() const;
 
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
@@ -511,7 +508,7 @@ class CVC4_PUBLIC DefineNamedFunctionCommand : public DefineFunctionCommand
                              const std::vector<api::Term>& formals,
                              api::Term formula,
                              bool global);
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   void toStream(
       std::ostream& out,
@@ -541,7 +538,7 @@ class CVC4_PUBLIC DefineFunctionRecCommand : public Command
   const std::vector<std::vector<api::Term> >& getFormals() const;
   const std::vector<api::Term>& getFormulas() const;
 
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
@@ -576,7 +573,7 @@ class CVC4_PUBLIC DeclareHeapCommand : public Command
   DeclareHeapCommand(api::Sort locSort, api::Sort dataSort);
   api::Sort getLocationSort() const;
   api::Sort getDataSort() const;
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
@@ -607,7 +604,7 @@ class CVC4_PUBLIC SetUserAttributeCommand : public Command
                           api::Term term,
                           const std::string& value);
 
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
@@ -640,7 +637,7 @@ class CVC4_PUBLIC CheckSatCommand : public Command
 
   api::Term getTerm() const;
   api::Result getResult() const;
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
   Command* clone() const override;
   std::string getCommandName() const override;
@@ -668,7 +665,7 @@ class CVC4_PUBLIC CheckSatAssumingCommand : public Command
 
   const std::vector<api::Term>& getTerms() const;
   api::Result getResult() const;
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
   Command* clone() const override;
   std::string getCommandName() const override;
@@ -695,7 +692,7 @@ class CVC4_PUBLIC QueryCommand : public Command
 
   api::Term getTerm() const;
   api::Result getResult() const;
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
   Command* clone() const override;
   std::string getCommandName() const override;
@@ -722,7 +719,7 @@ class CVC4_PUBLIC DeclareSygusVarCommand : public DeclarationDefinitionCommand
    * The declared sygus variable is communicated to the SMT engine in case a
    * synthesis conjecture is built later on.
    */
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   /** creates a copy of this command */
   Command* clone() const override;
   /** returns this command's name */
@@ -771,7 +768,7 @@ class CVC4_PUBLIC SynthFunCommand : public DeclarationDefinitionCommand
    * The declared function-to-synthesize is communicated to the SMT engine in
    * case a synthesis conjecture is built later on.
    */
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   /** creates a copy of this command */
   Command* clone() const override;
   /** returns this command's name */
@@ -808,7 +805,7 @@ class CVC4_PUBLIC SygusConstraintCommand : public Command
    * The declared constraint is communicated to the SMT engine in case a
    * synthesis conjecture is built later on.
    */
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   /** creates a copy of this command */
   Command* clone() const override;
   /** returns this command's name */
@@ -851,7 +848,7 @@ class CVC4_PUBLIC SygusInvConstraintCommand : public Command
    * invariant constraint is built, in case an actual synthesis conjecture is
    * built later on.
    */
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   /** creates a copy of this command */
   Command* clone() const override;
   /** returns this command's name */
@@ -887,7 +884,7 @@ class CVC4_PUBLIC CheckSynthCommand : public Command
    * and then perform a satisfiability check, whose result is stored in
    * d_result.
    */
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   /** creates a copy of this command */
   Command* clone() const override;
   /** returns this command's name */
@@ -920,7 +917,7 @@ class CVC4_PUBLIC SimplifyCommand : public Command
 
   api::Term getTerm() const;
   api::Term getResult() const;
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
   Command* clone() const override;
   std::string getCommandName() const override;
@@ -943,7 +940,7 @@ class CVC4_PUBLIC GetValueCommand : public Command
 
   const std::vector<api::Term>& getTerms() const;
   api::Term getResult() const;
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
   Command* clone() const override;
   std::string getCommandName() const override;
@@ -963,7 +960,7 @@ class CVC4_PUBLIC GetAssignmentCommand : public Command
   GetAssignmentCommand();
 
   SExpr getResult() const;
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
   Command* clone() const override;
   std::string getCommandName() const override;
@@ -981,7 +978,7 @@ class CVC4_PUBLIC GetModelCommand : public Command
 
   // Model is private to the library -- for now
   // Model* getResult() const ;
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
   Command* clone() const override;
   std::string getCommandName() const override;
@@ -1001,7 +998,7 @@ class CVC4_PUBLIC BlockModelCommand : public Command
  public:
   BlockModelCommand();
 
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
@@ -1018,7 +1015,7 @@ class CVC4_PUBLIC BlockModelValuesCommand : public Command
   BlockModelValuesCommand(const std::vector<api::Term>& terms);
 
   const std::vector<api::Term>& getTerms() const;
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
@@ -1037,7 +1034,7 @@ class CVC4_PUBLIC GetProofCommand : public Command
  public:
   GetProofCommand();
 
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
@@ -1052,7 +1049,7 @@ class CVC4_PUBLIC GetInstantiationsCommand : public Command
  public:
   GetInstantiationsCommand();
 
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
   Command* clone() const override;
   std::string getCommandName() const override;
@@ -1071,7 +1068,7 @@ class CVC4_PUBLIC GetSynthSolutionCommand : public Command
  public:
   GetSynthSolutionCommand();
 
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
   Command* clone() const override;
   std::string getCommandName() const override;
@@ -1109,7 +1106,7 @@ class CVC4_PUBLIC GetInterpolCommand : public Command
    * query. */
   api::Term getResult() const;
 
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
   Command* clone() const override;
   std::string getCommandName() const override;
@@ -1160,7 +1157,7 @@ class CVC4_PUBLIC GetAbductCommand : public Command
    */
   api::Term getResult() const;
 
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
   Command* clone() const override;
   std::string getCommandName() const override;
@@ -1196,7 +1193,7 @@ class CVC4_PUBLIC GetQuantifierEliminationCommand : public Command
 
   api::Term getTerm() const;
   bool getDoFull() const;
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   api::Term getResult() const;
   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
 
@@ -1213,7 +1210,7 @@ class CVC4_PUBLIC GetUnsatAssumptionsCommand : public Command
 {
  public:
   GetUnsatAssumptionsCommand();
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   std::vector<api::Term> getResult() const;
   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
   Command* clone() const override;
@@ -1234,7 +1231,7 @@ class CVC4_PUBLIC GetUnsatCoreCommand : public Command
   GetUnsatCoreCommand();
   const std::vector<api::Term>& getUnsatCore() const;
 
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
 
   Command* clone() const override;
@@ -1260,7 +1257,7 @@ class CVC4_PUBLIC GetAssertionsCommand : public Command
  public:
   GetAssertionsCommand();
 
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   std::string getResult() const;
   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
   Command* clone() const override;
@@ -1282,7 +1279,7 @@ class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command
 
   BenchmarkStatus getStatus() const;
 
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
@@ -1301,7 +1298,7 @@ class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command
   SetBenchmarkLogicCommand(std::string logic);
 
   std::string getLogic() const;
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
@@ -1323,7 +1320,7 @@ class CVC4_PUBLIC SetInfoCommand : public Command
   std::string getFlag() const;
   SExpr getSExpr() const;
 
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
@@ -1345,7 +1342,7 @@ class CVC4_PUBLIC GetInfoCommand : public Command
   std::string getFlag() const;
   std::string getResult() const;
 
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
   Command* clone() const override;
   std::string getCommandName() const override;
@@ -1368,7 +1365,7 @@ class CVC4_PUBLIC SetOptionCommand : public Command
   std::string getFlag() const;
   SExpr getSExpr() const;
 
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
@@ -1390,7 +1387,7 @@ class CVC4_PUBLIC GetOptionCommand : public Command
   std::string getFlag() const;
   std::string getResult() const;
 
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
   Command* clone() const override;
   std::string getCommandName() const override;
@@ -1417,7 +1414,7 @@ class CVC4_PUBLIC SetExpressionNameCommand : public Command
  public:
   SetExpressionNameCommand(api::Term term, std::string name);
 
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
@@ -1437,7 +1434,7 @@ class CVC4_PUBLIC DatatypeDeclarationCommand : public Command
 
   DatatypeDeclarationCommand(const std::vector<api::Sort>& datatypes);
   const std::vector<api::Sort>& getDatatypes() const;
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
@@ -1451,7 +1448,7 @@ class CVC4_PUBLIC ResetCommand : public Command
 {
  public:
   ResetCommand() {}
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
@@ -1465,7 +1462,7 @@ class CVC4_PUBLIC ResetAssertionsCommand : public Command
 {
  public:
   ResetAssertionsCommand() {}
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
@@ -1479,7 +1476,7 @@ class CVC4_PUBLIC QuitCommand : public Command
 {
  public:
   QuitCommand() {}
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
@@ -1498,7 +1495,7 @@ class CVC4_PUBLIC CommentCommand : public Command
 
   std::string getComment() const;
 
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
@@ -1523,9 +1520,9 @@ class CVC4_PUBLIC CommandSequence : public Command
   void addCommand(Command* cmd);
   void clear();
 
-  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver, SymbolManager* sm) override;
   void invoke(api::Solver* solver,
-              parser::SymbolManager* sm,
+              SymbolManager* sm,
               std::ostream& out) override;
 
   typedef std::vector<Command*>::iterator iterator;
diff --git a/test/api/ouroborous.cpp b/test/api/ouroborous.cpp
index 5ed240233..efca53ab3 100644
--- a/test/api/ouroborous.cpp
+++ b/test/api/ouroborous.cpp
@@ -111,8 +111,7 @@ void runTestString(std::string instr, InputLanguage instrlang = input::LANG_SMTL
 int runTest() {
   std::unique_ptr<api::Solver> solver =
       std::unique_ptr<api::Solver>(new api::Solver());
-  std::unique_ptr<parser::SymbolManager> symman(
-      new parser::SymbolManager(solver.get()));
+  std::unique_ptr<SymbolManager> symman(new SymbolManager(solver.get()));
   psr = ParserBuilder(solver.get(), symman.get(), "internal-buffer")
             .withStringInput(declarations)
             .withInputLanguage(input::LANG_SMTLIB_V2)
diff --git a/test/api/smt2_compliance.cpp b/test/api/smt2_compliance.cpp
index 8adab327e..3738bd1b6 100644
--- a/test/api/smt2_compliance.cpp
+++ b/test/api/smt2_compliance.cpp
@@ -60,8 +60,7 @@ int main()
 
 void testGetInfo(api::Solver* solver, const char* s)
 {
-  std::unique_ptr<parser::SymbolManager> symman(
-      new parser::SymbolManager(solver));
+  std::unique_ptr<SymbolManager> symman(new SymbolManager(solver));
 
   ParserBuilder pb(solver, symman.get(), "<internal>", solver->getOptions());
   Parser* p = pb.withStringInput(string("(get-info ") + s + ")").build();
diff --git a/test/unit/main/interactive_shell_black.h b/test/unit/main/interactive_shell_black.h
index af6960ff7..993f24690 100644
--- a/test/unit/main/interactive_shell_black.h
+++ b/test/unit/main/interactive_shell_black.h
@@ -22,12 +22,12 @@
 
 #include "api/cvc4cpp.h"
 #include "expr/expr_manager.h"
+#include "expr/symbol_manager.h"
 #include "main/interactive_shell.h"
 #include "options/base_options.h"
 #include "options/language.h"
 #include "options/options.h"
 #include "parser/parser_builder.h"
-#include "parser/symbol_manager.h"
 #include "smt/command.h"
 
 using namespace CVC4;
@@ -45,7 +45,7 @@ class InteractiveShellBlack : public CxxTest::TestSuite
     d_options.set(options::inputLanguage, language::input::LANG_CVC4);
     d_symman.reset(nullptr);
     d_solver.reset(new api::Solver(&d_options));
-    d_symman.reset(new parser::SymbolManager(d_solver.get()));
+    d_symman.reset(new SymbolManager(d_solver.get()));
   }
 
   void tearDown() override
@@ -99,7 +99,7 @@ class InteractiveShellBlack : public CxxTest::TestSuite
 
  private:
   std::unique_ptr<api::Solver> d_solver;
-  std::unique_ptr<parser::SymbolManager> d_symman;
+  std::unique_ptr<SymbolManager> d_symman;
   Options d_options;
   stringstream* d_sin;
   stringstream* d_sout;
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index 2bdd5c950..3b0bbb139 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -23,13 +23,13 @@
 #include "base/output.h"
 #include "expr/expr.h"
 #include "expr/expr_manager.h"
+#include "expr/symbol_manager.h"
 #include "options/base_options.h"
 #include "options/language.h"
 #include "options/options.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
 #include "parser/smt2/smt2.h"
-#include "parser/symbol_manager.h"
 #include "smt/command.h"
 
 using namespace CVC4;
@@ -70,7 +70,7 @@ class ParserBlack
       //         Debug.on("parser-extra");
       //        cerr << "Testing good input: <<" << goodInput << ">>" << endl;
       //        istringstream stream(goodInputs[i]);
-      d_symman.reset(new parser::SymbolManager(d_solver.get()));
+      d_symman.reset(new SymbolManager(d_solver.get()));
       Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test")
                            .withStringInput(goodInput)
                            .withOptions(d_options)
@@ -102,7 +102,7 @@ class ParserBlack
     //      cerr << "Testing bad input: '" << badInput << "'\n";
     //      Debug.on("parser");
 
-    d_symman.reset(new parser::SymbolManager(d_solver.get()));
+    d_symman.reset(new SymbolManager(d_solver.get()));
     Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test")
                          .withStringInput(badInput)
                          .withOptions(d_options)
@@ -134,7 +134,7 @@ class ParserBlack
       // Debug.on("parser");
       //        istringstream stream(context + goodBooleanExprs[i]);
 
-      d_symman.reset(new parser::SymbolManager(d_solver.get()));
+      d_symman.reset(new SymbolManager(d_solver.get()));
       Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test")
                            .withStringInput(goodExpr)
                            .withOptions(d_options)
@@ -182,7 +182,7 @@ class ParserBlack
     //    Debug.on("parser-extra");
     //      cout << "Testing bad expr: '" << badExpr << "'\n";
 
-    d_symman.reset(new parser::SymbolManager(d_solver.get()));
+    d_symman.reset(new SymbolManager(d_solver.get()));
     Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test")
                          .withStringInput(badExpr)
                          .withOptions(d_options)
@@ -224,7 +224,7 @@ class ParserBlack
  private:
   InputLanguage d_lang;
   std::unique_ptr<api::Solver> d_solver;
-  std::unique_ptr<parser::SymbolManager> d_symman;
+  std::unique_ptr<SymbolManager> d_symman;
 
 }; /* class ParserBlack */
 
diff --git a/test/unit/parser/parser_builder_black.h b/test/unit/parser/parser_builder_black.h
index b8ec96836..c101542d0 100644
--- a/test/unit/parser/parser_builder_black.h
+++ b/test/unit/parser/parser_builder_black.h
@@ -25,10 +25,10 @@
 #include <iostream>
 
 #include "api/cvc4cpp.h"
+#include "expr/symbol_manager.h"
 #include "options/language.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
-#include "parser/symbol_manager.h"
 
 using namespace CVC4;
 using namespace CVC4::parser;
@@ -43,7 +43,7 @@ class ParserBuilderBlack : public CxxTest::TestSuite
     // ensure the old symbol manager is deleted
     d_symman.reset(nullptr);
     d_solver.reset(new api::Solver());
-    d_symman.reset(new parser::SymbolManager(d_solver.get()));
+    d_symman.reset(new SymbolManager(d_solver.get()));
   }
 
   void tearDown() override {}
@@ -134,6 +134,6 @@ class ParserBuilderBlack : public CxxTest::TestSuite
   }
 
   std::unique_ptr<api::Solver> d_solver;
-  std::unique_ptr<parser::SymbolManager> d_symman;
+  std::unique_ptr<SymbolManager> d_symman;
 
 }; // class ParserBuilderBlack