Add symbol manager (#5380)

This add the symbol manager class, which is a Term-level utility, separate of the API. This class manages things like expression and assertion names, which is intentionally done outside the solver.

The symbol manager is intended to live at the same level as the Solver. When parsing input, the symbol manager will be used to model any interaction of e.g. named expressions and assertions. It also stores the symbol table of the parser.

This PR adds the basic interface for the symbol manager and passes it to the parser.

Later PRs will migrate the functionality for named expression out of e.g. SmtEngine and into SymbolManager. Commands will take Solver+SymbolManager instead of Solver. This will allow the parser to be fully migrated to the new API.

Marking "complex" since this impacts further design of the parser and the code that lives in src/main.

FYI @4tXJ7f

23 files changed, 325 insertions, 61 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index c6b41e94a..7f89b4de3 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -1150,6 +1150,7 @@ 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/main/command_executor.cpp b/src/main/command_executor.cpp
index c91b0455c..a56210fb1 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -50,6 +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_smtEngine(d_solver->getSmtEngine()),
       d_options(options),
       d_stats("driver"),
diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index d7899020e..c3c310380 100644
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -21,6 +21,7 @@
 #include "api/cvc4cpp.h"
 #include "expr/expr_manager.h"
 #include "options/options.h"
+#include "parser/symbol_manager.h"
 #include "smt/smt_engine.h"
 #include "util/statistics_registry.h"
 
@@ -28,10 +29,6 @@ namespace CVC4 {
 
 class Command;
 
-namespace api {
-class Solver;
-}
-
 namespace main {
 
 class CommandExecutor
@@ -40,7 +37,22 @@ class CommandExecutor
   std::string d_lastStatistics;
 
  protected:
+  /**
+   * The solver object, which is allocated by this class and is used for
+   * executing most commands (e.g. check-sat).
+   */
   std::unique_ptr<api::Solver> d_solver;
+  /**
+   * The symbol manager, which is allocated by this class. This manages
+   * all things related to definitions of symbols and their impact on behaviors
+   * for commands (e.g. get-unsat-core, get-model, get-assignment), as well
+   * as tracking expression names. Note the symbol manager is independent from
+   * the parser, which uses this symbol manager given a text input.
+   *
+   * Certain commands (e.g. reset-assertions) have a specific impact on the
+   * symbol manager.
+   */
+  std::unique_ptr<parser::SymbolManager> d_symman;
   SmtEngine* d_smtEngine;
   Options& d_options;
   StatisticsRegistry d_stats;
@@ -67,6 +79,9 @@ class CommandExecutor
   /** Get a pointer to the solver object owned by this 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(); }
+
   api::Result getResult() const { return d_result; }
   void reset();
 
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 9fff51b93..673c5ddd9 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -213,7 +213,8 @@ int runCvc4(int argc, char* argv[], Options& opts) {
         cmd->setMuted(true);
         pExecutor->doCommand(cmd);
       }
-      InteractiveShell shell(pExecutor->getSolver());
+      InteractiveShell shell(pExecutor->getSolver(),
+                             pExecutor->getSymbolManager());
       if(opts.getInteractivePrompt()) {
         Message() << Configuration::getPackageName()
                   << " " << Configuration::getVersionString();
@@ -258,7 +259,10 @@ int runCvc4(int argc, char* argv[], Options& opts) {
         // pExecutor->doCommand(cmd);
       }
 
-      ParserBuilder parserBuilder(pExecutor->getSolver(), filename, opts);
+      ParserBuilder parserBuilder(pExecutor->getSolver(),
+                                  pExecutor->getSymbolManager(),
+                                  filename,
+                                  opts);
 
       if( inputFromStdin ) {
 #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
@@ -411,7 +415,10 @@ int runCvc4(int argc, char* argv[], Options& opts) {
         pExecutor->doCommand(cmd);
       }
 
-      ParserBuilder parserBuilder(pExecutor->getSolver(), filename, opts);
+      ParserBuilder parserBuilder(pExecutor->getSolver(),
+                                  pExecutor->getSymbolManager(),
+                                  filename,
+                                  opts);
 
       if( inputFromStdin ) {
 #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index b798d03ee..8d482b08e 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -43,6 +43,7 @@
 #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"
 
@@ -83,13 +84,14 @@ static set<string> s_declarations;
 
 #endif /* HAVE_LIBEDITLINE */
 
-InteractiveShell::InteractiveShell(api::Solver* solver)
+InteractiveShell::InteractiveShell(api::Solver* solver,
+                                   parser::SymbolManager* sm)
     : d_options(solver->getOptions()),
       d_in(*d_options.getIn()),
       d_out(*d_options.getOutConst()),
       d_quit(false)
 {
-  ParserBuilder parserBuilder(solver, INPUT_FILENAME, d_options);
+  ParserBuilder parserBuilder(solver, sm, INPUT_FILENAME, d_options);
   /* Create parser with bogus input. */
   d_parser = parserBuilder.withStringInput("").build();
   if(d_options.wasSetByUserForceLogicString()) {
diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h
index 36e6068a4..b00f8a8f4 100644
--- a/src/main/interactive_shell.h
+++ b/src/main/interactive_shell.h
@@ -33,6 +33,7 @@ class Solver;
 
 namespace parser {
   class Parser;
+  class SymbolManager;
 }/* CVC4::parser namespace */
 
 class CVC4_PUBLIC InteractiveShell
@@ -50,7 +51,7 @@ class CVC4_PUBLIC InteractiveShell
   static const unsigned s_historyLimit = 500;
 
 public:
- InteractiveShell(api::Solver* solver);
+ InteractiveShell(api::Solver* solver, parser::SymbolManager* sm);
 
  /**
   * Close out the interactive session.
diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt
index 8e69da34b..7b55c0915 100644
--- a/src/parser/CMakeLists.txt
+++ b/src/parser/CMakeLists.txt
@@ -55,6 +55,8 @@ 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/cvc/cvc.h b/src/parser/cvc/cvc.h
index c9e3345d7..7214b6455 100644
--- a/src/parser/cvc/cvc.h
+++ b/src/parser/cvc/cvc.h
@@ -38,10 +38,11 @@ class Cvc : public Parser
 
  protected:
   Cvc(api::Solver* solver,
+      SymbolManager* sm,
       Input* input,
       bool strictMode = false,
       bool parseOnly = false)
-      : Parser(solver, input, strictMode, parseOnly)
+      : Parser(solver, sm, input, strictMode, parseOnly)
   {
   }
 };
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index af2faa505..710381f9b 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -42,12 +42,13 @@ namespace CVC4 {
 namespace parser {
 
 Parser::Parser(api::Solver* solver,
+               SymbolManager* sm,
                Input* input,
                bool strictMode,
                bool parseOnly)
     : d_input(input),
-      d_symtabAllocated(),
-      d_symtab(&d_symtabAllocated),
+      d_symman(sm),
+      d_symtab(sm->getSymbolTable()),
       d_assertionLevel(0),
       d_globalDeclarations(false),
       d_anonymousFunctionCount(0),
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 260ab33cf..405935165 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -30,6 +30,7 @@
 #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 {
@@ -109,16 +110,13 @@ private:
  Input* d_input;
 
  /**
-  * The declaration scope that is "owned" by this parser.  May or
-  * may not be the current declaration scope in use.
+  * Reference to the symbol manager, which manages the symbol table used by
+  * this parser.
   */
- SymbolTable d_symtabAllocated;
+ SymbolManager* d_symman;
 
  /**
-  * This current symbol table used by this parser.  Initially points
-  * to d_symtabAllocated, but can be changed (making this parser
-  * delegate its definitions and lookups to another parser).
-  * See useDeclarationsFrom().
+  * This current symbol table used by this parser, from symbol manager.
   */
  SymbolTable* d_symtab;
 
@@ -215,7 +213,8 @@ protected:
   * @attention The parser takes "ownership" of the given
   * input and will delete it on destruction.
   *
-  * @param the solver API object
+  * @param solver solver API object
+  * @param symm reference to the symbol manager
   * @param input the parser input
   * @param strictMode whether to incorporate strict(er) compliance checks
   * @param parseOnly whether we are parsing only (and therefore certain checks
@@ -223,6 +222,7 @@ protected:
   * unimplementedFeature())
   */
  Parser(api::Solver* solver,
+        SymbolManager* sm,
         Input* input,
         bool strictMode = false,
         bool parseOnly = false);
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index ac8190a17..9adb46af1 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -33,28 +33,34 @@
 namespace CVC4 {
 namespace parser {
 
-ParserBuilder::ParserBuilder(api::Solver* solver, const std::string& filename)
-    : d_filename(filename), d_solver(solver)
+ParserBuilder::ParserBuilder(api::Solver* solver,
+                             SymbolManager* sm,
+                             const std::string& filename)
+    : d_filename(filename), d_solver(solver), d_symman(sm)
 {
-  init(solver, filename);
+  init(solver, sm, filename);
 }
 
 ParserBuilder::ParserBuilder(api::Solver* solver,
+                             SymbolManager* sm,
                              const std::string& filename,
                              const Options& options)
-    : d_filename(filename), d_solver(solver)
+    : d_filename(filename), d_solver(solver), d_symman(sm)
 {
-  init(solver, filename);
+  init(solver, sm, filename);
   withOptions(options);
 }
 
-void ParserBuilder::init(api::Solver* solver, const std::string& filename)
+void ParserBuilder::init(api::Solver* solver,
+                         SymbolManager* sm,
+                         const std::string& filename)
 {
   d_inputType = FILE_INPUT;
   d_lang = language::input::LANG_AUTO;
   d_filename = filename;
   d_streamInput = NULL;
   d_solver = solver;
+  d_symman = sm;
   d_checksEnabled = true;
   d_strictMode = false;
   d_canIncludeFile = true;
@@ -90,19 +96,19 @@ Parser* ParserBuilder::build()
   switch (d_lang)
   {
     case language::input::LANG_SYGUS_V2:
-      parser = new Smt2(d_solver, input, d_strictMode, d_parseOnly);
+      parser = new Smt2(d_solver, d_symman, input, d_strictMode, d_parseOnly);
       break;
     case language::input::LANG_TPTP:
-      parser = new Tptp(d_solver, input, d_strictMode, d_parseOnly);
+      parser = new Tptp(d_solver, d_symman, input, d_strictMode, d_parseOnly);
       break;
     default:
       if (language::isInputLang_smt2(d_lang))
       {
-        parser = new Smt2(d_solver, input, d_strictMode, d_parseOnly);
+        parser = new Smt2(d_solver, d_symman, input, d_strictMode, d_parseOnly);
       }
       else
       {
-        parser = new Cvc(d_solver, input, d_strictMode, d_parseOnly);
+        parser = new Cvc(d_solver, d_symman, input, d_strictMode, d_parseOnly);
       }
       break;
   }
diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h
index 7eab196b8..9d62c12a3 100644
--- a/src/parser/parser_builder.h
+++ b/src/parser/parser_builder.h
@@ -35,6 +35,7 @@ class Solver;
 namespace parser {
 
 class Parser;
+class SymbolManager;
 
 /**
  * A builder for input language parsers. <code>build()</code> can be
@@ -67,6 +68,9 @@ class CVC4_PUBLIC ParserBuilder {
   /** The API Solver object. */
   api::Solver* d_solver;
 
+  /** The symbol manager */
+  SymbolManager* d_symman;
+
   /** Should semantic checks be enabled during parsing? */
   bool d_checksEnabled;
 
@@ -89,13 +93,18 @@ class CVC4_PUBLIC ParserBuilder {
   std::string d_forcedLogic;
 
   /** Initialize this parser builder */
-  void init(api::Solver* solver, const std::string& filename);
+  void init(api::Solver* solver,
+            SymbolManager* sm,
+            const std::string& filename);
 
  public:
   /** Create a parser builder using the given Solver and filename. */
-  ParserBuilder(api::Solver* solver, const std::string& filename);
+  ParserBuilder(api::Solver* solver,
+                SymbolManager* sm,
+                const std::string& filename);
 
   ParserBuilder(api::Solver* solver,
+                SymbolManager* sm,
                 const std::string& filename,
                 const Options& options);
 
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index a8a2eb27a..1decb3b1c 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -32,8 +32,12 @@
 namespace CVC4 {
 namespace parser {
 
-Smt2::Smt2(api::Solver* solver, Input* input, bool strictMode, bool parseOnly)
-    : Parser(solver, input, strictMode, parseOnly),
+Smt2::Smt2(api::Solver* solver,
+           SymbolManager* sm,
+           Input* input,
+           bool strictMode,
+           bool parseOnly)
+    : Parser(solver, sm, input, strictMode, parseOnly),
       d_logicSet(false),
       d_seenSetLogic(false)
 {
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 1aa0ebac7..eeedbec55 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -68,6 +68,7 @@ class Smt2 : public Parser
 
  protected:
   Smt2(api::Solver* solver,
+       SymbolManager* sm,
        Input* input,
        bool strictMode = false,
        bool parseOnly = false);
diff --git a/src/parser/symbol_manager.cpp b/src/parser/symbol_manager.cpp
new file mode 100644
index 000000000..32e17aea8
--- /dev/null
+++ b/src/parser/symbol_manager.cpp
@@ -0,0 +1,77 @@
+/*********************                                                        */
+/*! \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
new file mode 100644
index 000000000..20b0c80e4
--- /dev/null
+++ b/src/parser/symbol_manager.h
@@ -0,0 +1,102 @@
+/*********************                                                        */
+/*! \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/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index 066970fe3..f80b9c3c8 100644
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -33,8 +33,14 @@
 namespace CVC4 {
 namespace parser {
 
-Tptp::Tptp(api::Solver* solver, Input* input, bool strictMode, bool parseOnly)
-    : Parser(solver, input, strictMode, parseOnly), d_cnf(false), d_fof(false)
+Tptp::Tptp(api::Solver* solver,
+           SymbolManager* sm,
+           Input* input,
+           bool strictMode,
+           bool parseOnly)
+    : Parser(solver, sm, input, strictMode, parseOnly),
+      d_cnf(false),
+      d_fof(false)
 {
   addTheory(Tptp::THEORY_CORE);
 
diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h
index 0cd45847c..ca4dd61bf 100644
--- a/src/parser/tptp/tptp.h
+++ b/src/parser/tptp/tptp.h
@@ -92,6 +92,7 @@ class Tptp : public Parser {
 
  protected:
   Tptp(api::Solver* solver,
+       SymbolManager* sm,
        Input* input,
        bool strictMode = false,
        bool parseOnly = false);
diff --git a/test/api/ouroborous.cpp b/test/api/ouroborous.cpp
index 5ddc3ec26..5ed240233 100644
--- a/test/api/ouroborous.cpp
+++ b/test/api/ouroborous.cpp
@@ -111,7 +111,9 @@ 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());
-  psr = ParserBuilder(solver.get(), "internal-buffer")
+  std::unique_ptr<parser::SymbolManager> symman(
+      new parser::SymbolManager(solver.get()));
+  psr = ParserBuilder(solver.get(), symman.get(), "internal-buffer")
             .withStringInput(declarations)
             .withInputLanguage(input::LANG_SMTLIB_V2)
             .build();
diff --git a/test/api/smt2_compliance.cpp b/test/api/smt2_compliance.cpp
index e5781cfaa..7f9035636 100644
--- a/test/api/smt2_compliance.cpp
+++ b/test/api/smt2_compliance.cpp
@@ -43,7 +43,6 @@ int main()
 
   std::unique_ptr<api::Solver> solver =
       std::unique_ptr<api::Solver>(new api::Solver(&opts));
-
   testGetInfo(solver.get(), ":error-behavior");
   testGetInfo(solver.get(), ":name");
   testGetInfo(solver.get(), ":authors");
@@ -61,7 +60,10 @@ int main()
 
 void testGetInfo(api::Solver* solver, const char* s)
 {
-  ParserBuilder pb(solver, "<internal>", solver->getOptions());
+  std::unique_ptr<parser::SymbolManager> symman(
+      new parser::SymbolManager(solver));
+
+  ParserBuilder pb(solver, symman.get(), "<internal>", solver->getOptions());
   Parser* p = pb.withStringInput(string("(get-info ") + s + ")").build();
   assert(p != NULL);
   Command* c = p->nextCommand();
diff --git a/test/unit/main/interactive_shell_black.h b/test/unit/main/interactive_shell_black.h
index 417cfa94d..af6960ff7 100644
--- a/test/unit/main/interactive_shell_black.h
+++ b/test/unit/main/interactive_shell_black.h
@@ -27,6 +27,7 @@
 #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;
@@ -42,7 +43,9 @@ class InteractiveShellBlack : public CxxTest::TestSuite
     d_options.set(options::in, d_sin);
     d_options.set(options::out, d_sout);
     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()));
   }
 
   void tearDown() override
@@ -53,18 +56,18 @@ class InteractiveShellBlack : public CxxTest::TestSuite
 
   void testAssertTrue() {
     *d_sin << "ASSERT TRUE;\n" << flush;
-    InteractiveShell shell(d_solver.get());
+    InteractiveShell shell(d_solver.get(), d_symman.get());
     countCommands( shell, 1, 1 );
   }
 
   void testQueryFalse() {
     *d_sin << "QUERY FALSE;\n" << flush;
-    InteractiveShell shell(d_solver.get());
+    InteractiveShell shell(d_solver.get(), d_symman.get());
     countCommands( shell, 1, 1 );
   }
 
   void testDefUse() {
-    InteractiveShell shell(d_solver.get());
+    InteractiveShell shell(d_solver.get(), d_symman.get());
     *d_sin << "x : REAL; ASSERT x > 0;\n" << flush;
     /* readCommand may return a sequence, so we can't say for sure
        whether it will return 1 or 2... */
@@ -72,7 +75,7 @@ class InteractiveShellBlack : public CxxTest::TestSuite
   }
 
   void testDefUse2() {
-    InteractiveShell shell(d_solver.get());
+    InteractiveShell shell(d_solver.get(), d_symman.get());
     /* readCommand may return a sequence, see above. */
     *d_sin << "x : REAL;\n" << flush;
     Command* tmp = shell.readCommand();
@@ -82,20 +85,21 @@ class InteractiveShellBlack : public CxxTest::TestSuite
   }
 
   void testEmptyLine() {
-    InteractiveShell shell(d_solver.get());
+    InteractiveShell shell(d_solver.get(), d_symman.get());
     *d_sin << flush;
     countCommands(shell,0,0);
   }
 
   void testRepeatedEmptyLines() {
     *d_sin << "\n\n\n";
-    InteractiveShell shell(d_solver.get());
+    InteractiveShell shell(d_solver.get(), d_symman.get());
     /* Might return up to four empties, might return nothing */
     countCommands( shell, 0, 3 );
   }
 
  private:
   std::unique_ptr<api::Solver> d_solver;
+  std::unique_ptr<parser::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 dfe2ee138..2bdd5c950 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -29,9 +29,9 @@
 #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;
 using namespace CVC4::parser;
 using namespace CVC4::language::input;
@@ -70,7 +70,8 @@ class ParserBlack
       //         Debug.on("parser-extra");
       //        cerr << "Testing good input: <<" << goodInput << ">>" << endl;
       //        istringstream stream(goodInputs[i]);
-      Parser* parser = ParserBuilder(d_solver.get(), "test")
+      d_symman.reset(new parser::SymbolManager(d_solver.get()));
+      Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test")
                            .withStringInput(goodInput)
                            .withOptions(d_options)
                            .withInputLanguage(d_lang)
@@ -101,7 +102,8 @@ class ParserBlack
     //      cerr << "Testing bad input: '" << badInput << "'\n";
     //      Debug.on("parser");
 
-    Parser* parser = ParserBuilder(d_solver.get(), "test")
+    d_symman.reset(new parser::SymbolManager(d_solver.get()));
+    Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test")
                          .withStringInput(badInput)
                          .withOptions(d_options)
                          .withInputLanguage(d_lang)
@@ -132,7 +134,8 @@ class ParserBlack
       // Debug.on("parser");
       //        istringstream stream(context + goodBooleanExprs[i]);
 
-      Parser* parser = ParserBuilder(d_solver.get(), "test")
+      d_symman.reset(new parser::SymbolManager(d_solver.get()));
+      Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test")
                            .withStringInput(goodExpr)
                            .withOptions(d_options)
                            .withInputLanguage(d_lang)
@@ -179,7 +182,8 @@ class ParserBlack
     //    Debug.on("parser-extra");
     //      cout << "Testing bad expr: '" << badExpr << "'\n";
 
-    Parser* parser = ParserBuilder(d_solver.get(), "test")
+    d_symman.reset(new parser::SymbolManager(d_solver.get()));
+    Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test")
                          .withStringInput(badExpr)
                          .withOptions(d_options)
                          .withInputLanguage(d_lang)
@@ -206,14 +210,21 @@ class ParserBlack
   void setUp()
   {
     d_options.set(options::parseOnly, true);
+    // ensure the old symbol manager is deleted
+    d_symman.reset(nullptr);
     d_solver.reset(new api::Solver(&d_options));
   }
 
-  void tearDown() { d_solver.reset(nullptr); }
+  void tearDown()
+  {
+    d_symman.reset(nullptr);
+    d_solver.reset(nullptr);
+  }
 
  private:
   InputLanguage d_lang;
   std::unique_ptr<api::Solver> d_solver;
+  std::unique_ptr<parser::SymbolManager> d_symman;
 
 }; /* class ParserBlack */
 
diff --git a/test/unit/parser/parser_builder_black.h b/test/unit/parser/parser_builder_black.h
index 003424397..b8ec96836 100644
--- a/test/unit/parser/parser_builder_black.h
+++ b/test/unit/parser/parser_builder_black.h
@@ -28,6 +28,7 @@
 #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;
@@ -37,7 +38,13 @@ using namespace std;
 class ParserBuilderBlack : public CxxTest::TestSuite
 {
  public:
-  void setUp() override { d_solver.reset(new api::Solver()); }
+  void setUp() override
+  {
+    // 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()));
+  }
 
   void tearDown() override {}
 
@@ -45,8 +52,8 @@ class ParserBuilderBlack : public CxxTest::TestSuite
   {
     char *filename = mkTemp();
 
-    checkEmptyInput(
-        ParserBuilder(d_solver.get(), filename).withInputLanguage(LANG_CVC4));
+    checkEmptyInput(ParserBuilder(d_solver.get(), d_symman.get(), filename)
+                        .withInputLanguage(LANG_CVC4));
 
     remove(filename);
     free(filename);
@@ -59,35 +66,35 @@ class ParserBuilderBlack : public CxxTest::TestSuite
     fs << "TRUE" << std::endl;
     fs.close();
 
-    checkTrueInput(
-        ParserBuilder(d_solver.get(), filename).withInputLanguage(LANG_CVC4));
+    checkTrueInput(ParserBuilder(d_solver.get(), d_symman.get(), filename)
+                       .withInputLanguage(LANG_CVC4));
 
     remove(filename);
     free(filename);
   }
 
   void testEmptyStringInput() {
-    checkEmptyInput(ParserBuilder(d_solver.get(), "foo")
+    checkEmptyInput(ParserBuilder(d_solver.get(), d_symman.get(), "foo")
                         .withInputLanguage(LANG_CVC4)
                         .withStringInput(""));
   }
 
   void testTrueStringInput() {
-    checkTrueInput(ParserBuilder(d_solver.get(), "foo")
+    checkTrueInput(ParserBuilder(d_solver.get(), d_symman.get(), "foo")
                        .withInputLanguage(LANG_CVC4)
                        .withStringInput("TRUE"));
   }
 
   void testEmptyStreamInput() {
     stringstream ss( "", ios_base::in );
-    checkEmptyInput(ParserBuilder(d_solver.get(), "foo")
+    checkEmptyInput(ParserBuilder(d_solver.get(), d_symman.get(), "foo")
                         .withInputLanguage(LANG_CVC4)
                         .withStreamInput(ss));
   }
 
   void testTrueStreamInput() {
     stringstream ss( "TRUE", ios_base::in );
-    checkTrueInput(ParserBuilder(d_solver.get(), "foo")
+    checkTrueInput(ParserBuilder(d_solver.get(), d_symman.get(), "foo")
                        .withInputLanguage(LANG_CVC4)
                        .withStreamInput(ss));
   }
@@ -127,5 +134,6 @@ class ParserBuilderBlack : public CxxTest::TestSuite
   }
 
   std::unique_ptr<api::Solver> d_solver;
+  std::unique_ptr<parser::SymbolManager> d_symman;
 
 }; // class ParserBuilderBlack