Pass symbol manager to commands (#5410)

This PR passes the symbol manager to Command::invoke.

There are no behavior changes in this PR. This is in preparation for reimplementing several features in the parser related to symbols.

4 files changed, 167 insertions, 208 deletions

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index a56210fb1..7b20f3a1a 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -119,9 +119,10 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
 {
   bool status = true;
   if(d_options.getVerbosity() >= -1) {
-    status = solverInvoke(d_solver.get(), cmd, d_options.getOut());
+    status =
+        solverInvoke(d_solver.get(), d_symman.get(), cmd, d_options.getOut());
   } else {
-    status = solverInvoke(d_solver.get(), cmd, nullptr);
+    status = solverInvoke(d_solver.get(), d_symman.get(), cmd, nullptr);
   }
 
   api::Result res;
@@ -198,15 +199,18 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
   return status;
 }
 
-bool solverInvoke(api::Solver* solver, Command* cmd, std::ostream* out)
+bool solverInvoke(api::Solver* solver,
+                  parser::SymbolManager* sm,
+                  Command* cmd,
+                  std::ostream* out)
 {
   if (out == NULL)
   {
-    cmd->invoke(solver);
+    cmd->invoke(solver, sm);
   }
   else
   {
-    cmd->invoke(solver, *out);
+    cmd->invoke(solver, sm, *out);
   }
   // ignore the error if the command-verbosity is 0 for this command
   std::string commandName =
diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index c3c310380..87748b1e5 100644
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -116,7 +116,10 @@ private:
 
 }; /* class CommandExecutor */
 
-bool solverInvoke(api::Solver* solver, Command* cmd, std::ostream* out);
+bool solverInvoke(api::Solver* solver,
+                  parser::SymbolManager* sm,
+                  Command* cmd,
+                  std::ostream* out);
 
 }/* CVC4::main namespace */
 }/* CVC4 namespace */
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index b33fe5ad9..68c776536 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -31,6 +31,7 @@
 #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"
@@ -175,9 +176,11 @@ bool Command::interrupted() const
          && dynamic_cast<const CommandInterrupted*>(d_commandStatus) != NULL;
 }
 
-void Command::invoke(api::Solver* solver, std::ostream& out)
+void Command::invoke(api::Solver* solver,
+                     parser::SymbolManager* sm,
+                     std::ostream& out)
 {
-  invoke(solver);
+  invoke(solver, sm);
   if (!(isMuted() && ok()))
   {
     printResult(
@@ -215,7 +218,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)
+void EmptyCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
 {
   /* empty commands have no implementation */
   d_commandStatus = CommandSuccess::instance();
@@ -226,7 +229,6 @@ std::string EmptyCommand::getCommandName() const { return "empty"; }
 
 void EmptyCommand::toStream(std::ostream& out,
                             int toDepth,
-
                             size_t dag,
                             OutputLanguage language) const
 {
@@ -239,13 +241,15 @@ 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)
+void EchoCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
 {
   /* we don't have an output stream here, nothing to do */
   d_commandStatus = CommandSuccess::instance();
 }
 
-void EchoCommand::invoke(api::Solver* solver, std::ostream& out)
+void EchoCommand::invoke(api::Solver* solver,
+                         parser::SymbolManager* sm,
+                         std::ostream& out)
 {
   out << d_output << std::endl;
   Trace("dtview::command") << "* ~COMMAND: echo |" << d_output << "|~"
@@ -261,7 +265,6 @@ std::string EchoCommand::getCommandName() const { return "echo"; }
 
 void EchoCommand::toStream(std::ostream& out,
                            int toDepth,
-
                            size_t dag,
                            OutputLanguage language) const
 {
@@ -278,7 +281,7 @@ AssertCommand::AssertCommand(const api::Term& t, bool inUnsatCore)
 }
 
 api::Term AssertCommand::getTerm() const { return d_term; }
-void AssertCommand::invoke(api::Solver* solver)
+void AssertCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
 {
   try
   {
@@ -304,7 +307,6 @@ std::string AssertCommand::getCommandName() const { return "assert"; }
 
 void AssertCommand::toStream(std::ostream& out,
                              int toDepth,
-
                              size_t dag,
                              OutputLanguage language) const
 {
@@ -315,7 +317,7 @@ void AssertCommand::toStream(std::ostream& out,
 /* class PushCommand                                                          */
 /* -------------------------------------------------------------------------- */
 
-void PushCommand::invoke(api::Solver* solver)
+void PushCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
 {
   try
   {
@@ -337,7 +339,6 @@ std::string PushCommand::getCommandName() const { return "push"; }
 
 void PushCommand::toStream(std::ostream& out,
                            int toDepth,
-
                            size_t dag,
                            OutputLanguage language) const
 {
@@ -348,7 +349,7 @@ void PushCommand::toStream(std::ostream& out,
 /* class PopCommand                                                           */
 /* -------------------------------------------------------------------------- */
 
-void PopCommand::invoke(api::Solver* solver)
+void PopCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
 {
   try
   {
@@ -370,7 +371,6 @@ std::string PopCommand::getCommandName() const { return "pop"; }
 
 void PopCommand::toStream(std::ostream& out,
                           int toDepth,
-
                           size_t dag,
                           OutputLanguage language) const
 {
@@ -386,7 +386,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)
+void CheckSatCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
 {
   Trace("dtview::command") << "* ~COMMAND: " << getCommandName() << "~"
                            << std::endl;
@@ -428,7 +428,6 @@ std::string CheckSatCommand::getCommandName() const { return "check-sat"; }
 
 void CheckSatCommand::toStream(std::ostream& out,
                                int toDepth,
-
                                size_t dag,
                                OutputLanguage language) const
 {
@@ -455,7 +454,8 @@ const std::vector<api::Term>& CheckSatAssumingCommand::getTerms() const
   return d_terms;
 }
 
-void CheckSatAssumingCommand::invoke(api::Solver* solver)
+void CheckSatAssumingCommand::invoke(api::Solver* solver,
+                                     parser::SymbolManager* sm)
 {
   Trace("dtview::command") << "* ~COMMAND: (check-sat-assuming ( " << d_terms
                            << " )~" << std::endl;
@@ -503,7 +503,6 @@ std::string CheckSatAssumingCommand::getCommandName() const
 
 void CheckSatAssumingCommand::toStream(std::ostream& out,
                                        int toDepth,
-
                                        size_t dag,
                                        OutputLanguage language) const
 {
@@ -521,7 +520,7 @@ QueryCommand::QueryCommand(const api::Term& t, bool inUnsatCore)
 }
 
 api::Term QueryCommand::getTerm() const { return d_term; }
-void QueryCommand::invoke(api::Solver* solver)
+void QueryCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
 {
   try
   {
@@ -558,7 +557,6 @@ std::string QueryCommand::getCommandName() const { return "query"; }
 
 void QueryCommand::toStream(std::ostream& out,
                             int toDepth,
-
                             size_t dag,
                             OutputLanguage language) const
 {
@@ -579,7 +577,8 @@ 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)
+void DeclareSygusVarCommand::invoke(api::Solver* solver,
+                                    parser::SymbolManager* sm)
 {
   d_commandStatus = CommandSuccess::instance();
 }
@@ -596,7 +595,6 @@ std::string DeclareSygusVarCommand::getCommandName() const
 
 void DeclareSygusVarCommand::toStream(std::ostream& out,
                                       int toDepth,
-
                                       size_t dag,
                                       OutputLanguage language) const
 {
@@ -635,7 +633,7 @@ bool SynthFunCommand::isInv() const { return d_isInv; }
 
 const api::Grammar* SynthFunCommand::getGrammar() const { return d_grammar; }
 
-void SynthFunCommand::invoke(api::Solver* solver)
+void SynthFunCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
 {
   d_commandStatus = CommandSuccess::instance();
 }
@@ -653,7 +651,6 @@ std::string SynthFunCommand::getCommandName() const
 
 void SynthFunCommand::toStream(std::ostream& out,
                                int toDepth,
-
                                size_t dag,
                                OutputLanguage language) const
 {
@@ -675,7 +672,8 @@ SygusConstraintCommand::SygusConstraintCommand(const api::Term& t) : d_term(t)
 {
 }
 
-void SygusConstraintCommand::invoke(api::Solver* solver)
+void SygusConstraintCommand::invoke(api::Solver* solver,
+                                    parser::SymbolManager* sm)
 {
   try
   {
@@ -702,7 +700,6 @@ std::string SygusConstraintCommand::getCommandName() const
 
 void SygusConstraintCommand::toStream(std::ostream& out,
                                       int toDepth,
-
                                       size_t dag,
                                       OutputLanguage language) const
 {
@@ -727,7 +724,8 @@ SygusInvConstraintCommand::SygusInvConstraintCommand(const api::Term& inv,
 {
 }
 
-void SygusInvConstraintCommand::invoke(api::Solver* solver)
+void SygusInvConstraintCommand::invoke(api::Solver* solver,
+                                       parser::SymbolManager* sm)
 {
   try
   {
@@ -758,7 +756,6 @@ std::string SygusInvConstraintCommand::getCommandName() const
 
 void SygusInvConstraintCommand::toStream(std::ostream& out,
                                          int toDepth,
-
                                          size_t dag,
                                          OutputLanguage language) const
 {
@@ -774,7 +771,7 @@ void SygusInvConstraintCommand::toStream(std::ostream& out,
 /* class CheckSynthCommand                                                    */
 /* -------------------------------------------------------------------------- */
 
-void CheckSynthCommand::invoke(api::Solver* solver)
+void CheckSynthCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
 {
   try
   {
@@ -832,7 +829,6 @@ std::string CheckSynthCommand::getCommandName() const { return "check-synth"; }
 
 void CheckSynthCommand::toStream(std::ostream& out,
                                  int toDepth,
-
                                  size_t dag,
                                  OutputLanguage language) const
 {
@@ -843,7 +839,7 @@ void CheckSynthCommand::toStream(std::ostream& out,
 /* class ResetCommand                                                         */
 /* -------------------------------------------------------------------------- */
 
-void ResetCommand::invoke(api::Solver* solver)
+void ResetCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
 {
   try
   {
@@ -861,7 +857,6 @@ std::string ResetCommand::getCommandName() const { return "reset"; }
 
 void ResetCommand::toStream(std::ostream& out,
                             int toDepth,
-
                             size_t dag,
                             OutputLanguage language) const
 {
@@ -872,7 +867,8 @@ void ResetCommand::toStream(std::ostream& out,
 /* class ResetAssertionsCommand                                               */
 /* -------------------------------------------------------------------------- */
 
-void ResetAssertionsCommand::invoke(api::Solver* solver)
+void ResetAssertionsCommand::invoke(api::Solver* solver,
+                                    parser::SymbolManager* sm)
 {
   try
   {
@@ -897,7 +893,6 @@ std::string ResetAssertionsCommand::getCommandName() const
 
 void ResetAssertionsCommand::toStream(std::ostream& out,
                                       int toDepth,
-
                                       size_t dag,
                                       OutputLanguage language) const
 {
@@ -908,7 +903,7 @@ void ResetAssertionsCommand::toStream(std::ostream& out,
 /* class QuitCommand                                                          */
 /* -------------------------------------------------------------------------- */
 
-void QuitCommand::invoke(api::Solver* solver)
+void QuitCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
 {
   Dump("benchmark") << *this;
   d_commandStatus = CommandSuccess::instance();
@@ -919,7 +914,6 @@ std::string QuitCommand::getCommandName() const { return "exit"; }
 
 void QuitCommand::toStream(std::ostream& out,
                            int toDepth,
-
                            size_t dag,
                            OutputLanguage language) const
 {
@@ -932,7 +926,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)
+void CommentCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
 {
   Dump("benchmark") << *this;
   d_commandStatus = CommandSuccess::instance();
@@ -943,7 +937,6 @@ std::string CommentCommand::getCommandName() const { return "comment"; }
 
 void CommentCommand::toStream(std::ostream& out,
                               int toDepth,
-
                               size_t dag,
                               OutputLanguage language) const
 {
@@ -969,11 +962,11 @@ void CommandSequence::addCommand(Command* cmd)
 }
 
 void CommandSequence::clear() { d_commandSequence.clear(); }
-void CommandSequence::invoke(api::Solver* solver)
+void CommandSequence::invoke(api::Solver* solver, parser::SymbolManager* sm)
 {
   for (; d_index < d_commandSequence.size(); ++d_index)
   {
-    d_commandSequence[d_index]->invoke(solver);
+    d_commandSequence[d_index]->invoke(solver, sm);
     if (!d_commandSequence[d_index]->ok())
     {
       // abort execution
@@ -987,11 +980,13 @@ void CommandSequence::invoke(api::Solver* solver)
   d_commandStatus = CommandSuccess::instance();
 }
 
-void CommandSequence::invoke(api::Solver* solver, std::ostream& out)
+void CommandSequence::invoke(api::Solver* solver,
+                             parser::SymbolManager* sm,
+                             std::ostream& out)
 {
   for (; d_index < d_commandSequence.size(); ++d_index)
   {
-    d_commandSequence[d_index]->invoke(solver, out);
+    d_commandSequence[d_index]->invoke(solver, sm, out);
     if (!d_commandSequence[d_index]->ok())
     {
       // abort execution
@@ -1040,7 +1035,6 @@ std::string CommandSequence::getCommandName() const { return "sequence"; }
 
 void CommandSequence::toStream(std::ostream& out,
                                int toDepth,
-
                                size_t dag,
                                OutputLanguage language) const
 {
@@ -1054,7 +1048,6 @@ void CommandSequence::toStream(std::ostream& out,
 
 void DeclarationSequence::toStream(std::ostream& out,
                                    int toDepth,
-
                                    size_t dag,
                                    OutputLanguage language) const
 {
@@ -1103,7 +1096,8 @@ void DeclareFunctionCommand::setPrintInModel(bool p)
   d_printInModelSetByUser = true;
 }
 
-void DeclareFunctionCommand::invoke(api::Solver* solver)
+void DeclareFunctionCommand::invoke(api::Solver* solver,
+                                    parser::SymbolManager* sm)
 {
   d_commandStatus = CommandSuccess::instance();
 }
@@ -1124,7 +1118,6 @@ std::string DeclareFunctionCommand::getCommandName() const
 
 void DeclareFunctionCommand::toStream(std::ostream& out,
                                       int toDepth,
-
                                       size_t dag,
                                       OutputLanguage language) const
 {
@@ -1145,7 +1138,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)
+void DeclareSortCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
 {
   d_commandStatus = CommandSuccess::instance();
 }
@@ -1162,7 +1155,6 @@ std::string DeclareSortCommand::getCommandName() const
 
 void DeclareSortCommand::toStream(std::ostream& out,
                                   int toDepth,
-
                                   size_t dag,
                                   OutputLanguage language) const
 {
@@ -1192,7 +1184,7 @@ const std::vector<api::Sort>& DefineSortCommand::getParameters() const
 }
 
 api::Sort DefineSortCommand::getSort() const { return d_sort; }
-void DefineSortCommand::invoke(api::Solver* solver)
+void DefineSortCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
 {
   d_commandStatus = CommandSuccess::instance();
 }
@@ -1206,7 +1198,6 @@ std::string DefineSortCommand::getCommandName() const { return "define-sort"; }
 
 void DefineSortCommand::toStream(std::ostream& out,
                                  int toDepth,
-
                                  size_t dag,
                                  OutputLanguage language) const
 {
@@ -1254,7 +1245,8 @@ const std::vector<api::Term>& DefineFunctionCommand::getFormals() const
 }
 
 api::Term DefineFunctionCommand::getFormula() const { return d_formula; }
-void DefineFunctionCommand::invoke(api::Solver* solver)
+void DefineFunctionCommand::invoke(api::Solver* solver,
+                                   parser::SymbolManager* sm)
 {
   try
   {
@@ -1283,7 +1275,6 @@ std::string DefineFunctionCommand::getCommandName() const
 
 void DefineFunctionCommand::toStream(std::ostream& out,
                                      int toDepth,
-
                                      size_t dag,
                                      OutputLanguage language) const
 {
@@ -1310,9 +1301,10 @@ DefineNamedFunctionCommand::DefineNamedFunctionCommand(
 {
 }
 
-void DefineNamedFunctionCommand::invoke(api::Solver* solver)
+void DefineNamedFunctionCommand::invoke(api::Solver* solver,
+                                        parser::SymbolManager* sm)
 {
-  this->DefineFunctionCommand::invoke(solver);
+  this->DefineFunctionCommand::invoke(solver, sm);
   if (!d_func.isNull() && d_func.getSort().isBoolean())
   {
     solver->getSmtEngine()->addToAssignment(d_func.getExpr());
@@ -1328,7 +1320,6 @@ Command* DefineNamedFunctionCommand::clone() const
 
 void DefineNamedFunctionCommand::toStream(std::ostream& out,
                                           int toDepth,
-
                                           size_t dag,
                                           OutputLanguage language) const
 {
@@ -1383,7 +1374,8 @@ const std::vector<api::Term>& DefineFunctionRecCommand::getFormulas() const
   return d_formulas;
 }
 
-void DefineFunctionRecCommand::invoke(api::Solver* solver)
+void DefineFunctionRecCommand::invoke(api::Solver* solver,
+                                      parser::SymbolManager* sm)
 {
   try
   {
@@ -1408,7 +1400,6 @@ std::string DefineFunctionRecCommand::getCommandName() const
 
 void DefineFunctionRecCommand::toStream(std::ostream& out,
                                         int toDepth,
-
                                         size_t dag,
                                         OutputLanguage language) const
 {
@@ -1436,7 +1427,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)
+void DeclareHeapCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
 {
   solver->declareSeparationHeap(d_locSort, d_dataSort);
 }
@@ -1494,7 +1485,8 @@ SetUserAttributeCommand::SetUserAttributeCommand(const std::string& attr,
 {
 }
 
-void SetUserAttributeCommand::invoke(api::Solver* solver)
+void SetUserAttributeCommand::invoke(api::Solver* solver,
+                                     parser::SymbolManager* sm)
 {
   try
   {
@@ -1526,7 +1518,6 @@ std::string SetUserAttributeCommand::getCommandName() const
 
 void SetUserAttributeCommand::toStream(std::ostream& out,
                                        int toDepth,
-
                                        size_t dag,
                                        OutputLanguage language) const
 {
@@ -1540,7 +1531,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)
+void SimplifyCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
 {
   try
   {
@@ -1581,7 +1572,6 @@ std::string SimplifyCommand::getCommandName() const { return "simplify"; }
 
 void SimplifyCommand::toStream(std::ostream& out,
                                int toDepth,
-
                                size_t dag,
                                OutputLanguage language) const
 {
@@ -1608,7 +1598,7 @@ const std::vector<api::Term>& GetValueCommand::getTerms() const
 {
   return d_terms;
 }
-void GetValueCommand::invoke(api::Solver* solver)
+void GetValueCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
 {
   try
   {
@@ -1662,7 +1652,6 @@ std::string GetValueCommand::getCommandName() const { return "get-value"; }
 
 void GetValueCommand::toStream(std::ostream& out,
                                int toDepth,
-
                                size_t dag,
                                OutputLanguage language) const
 {
@@ -1675,7 +1664,8 @@ void GetValueCommand::toStream(std::ostream& out,
 /* -------------------------------------------------------------------------- */
 
 GetAssignmentCommand::GetAssignmentCommand() {}
-void GetAssignmentCommand::invoke(api::Solver* solver)
+void GetAssignmentCommand::invoke(api::Solver* solver,
+                                  parser::SymbolManager* sm)
 {
   try
   {
@@ -1734,7 +1724,6 @@ std::string GetAssignmentCommand::getCommandName() const
 
 void GetAssignmentCommand::toStream(std::ostream& out,
                                     int toDepth,
-
                                     size_t dag,
                                     OutputLanguage language) const
 {
@@ -1746,7 +1735,7 @@ void GetAssignmentCommand::toStream(std::ostream& out,
 /* -------------------------------------------------------------------------- */
 
 GetModelCommand::GetModelCommand() : d_result(nullptr) {}
-void GetModelCommand::invoke(api::Solver* solver)
+void GetModelCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
 {
   try
   {
@@ -1796,7 +1785,6 @@ std::string GetModelCommand::getCommandName() const { return "get-model"; }
 
 void GetModelCommand::toStream(std::ostream& out,
                                int toDepth,
-
                                size_t dag,
                                OutputLanguage language) const
 {
@@ -1808,7 +1796,7 @@ void GetModelCommand::toStream(std::ostream& out,
 /* -------------------------------------------------------------------------- */
 
 BlockModelCommand::BlockModelCommand() {}
-void BlockModelCommand::invoke(api::Solver* solver)
+void BlockModelCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
 {
   try
   {
@@ -1839,7 +1827,6 @@ std::string BlockModelCommand::getCommandName() const { return "block-model"; }
 
 void BlockModelCommand::toStream(std::ostream& out,
                                  int toDepth,
-
                                  size_t dag,
                                  OutputLanguage language) const
 {
@@ -1863,7 +1850,8 @@ const std::vector<api::Term>& BlockModelValuesCommand::getTerms() const
 {
   return d_terms;
 }
-void BlockModelValuesCommand::invoke(api::Solver* solver)
+void BlockModelValuesCommand::invoke(api::Solver* solver,
+                                     parser::SymbolManager* sm)
 {
   try
   {
@@ -1897,7 +1885,6 @@ std::string BlockModelValuesCommand::getCommandName() const
 
 void BlockModelValuesCommand::toStream(std::ostream& out,
                                        int toDepth,
-
                                        size_t dag,
                                        OutputLanguage language) const
 {
@@ -1910,7 +1897,7 @@ void BlockModelValuesCommand::toStream(std::ostream& out,
 /* -------------------------------------------------------------------------- */
 
 GetProofCommand::GetProofCommand() {}
-void GetProofCommand::invoke(api::Solver* solver)
+void GetProofCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
 {
   Unimplemented() << "Unimplemented get-proof\n";
 }
@@ -1925,7 +1912,6 @@ std::string GetProofCommand::getCommandName() const { return "get-proof"; }
 
 void GetProofCommand::toStream(std::ostream& out,
                                int toDepth,
-
                                size_t dag,
                                OutputLanguage language) const
 {
@@ -1937,7 +1923,8 @@ void GetProofCommand::toStream(std::ostream& out,
 /* -------------------------------------------------------------------------- */
 
 GetInstantiationsCommand::GetInstantiationsCommand() : d_solver(nullptr) {}
-void GetInstantiationsCommand::invoke(api::Solver* solver)
+void GetInstantiationsCommand::invoke(api::Solver* solver,
+                                      parser::SymbolManager* sm)
 {
   try
   {
@@ -1978,7 +1965,6 @@ std::string GetInstantiationsCommand::getCommandName() const
 
 void GetInstantiationsCommand::toStream(std::ostream& out,
                                         int toDepth,
-
                                         size_t dag,
                                         OutputLanguage language) const
 {
@@ -1990,7 +1976,8 @@ void GetInstantiationsCommand::toStream(std::ostream& out,
 /* -------------------------------------------------------------------------- */
 
 GetSynthSolutionCommand::GetSynthSolutionCommand() : d_solver(nullptr) {}
-void GetSynthSolutionCommand::invoke(api::Solver* solver)
+void GetSynthSolutionCommand::invoke(api::Solver* solver,
+                                     parser::SymbolManager* sm)
 {
   try
   {
@@ -2030,7 +2017,6 @@ std::string GetSynthSolutionCommand::getCommandName() const
 
 void GetSynthSolutionCommand::toStream(std::ostream& out,
                                        int toDepth,
-
                                        size_t dag,
                                        OutputLanguage language) const
 {
@@ -2061,7 +2047,7 @@ const api::Grammar* GetInterpolCommand::getGrammar() const
 
 api::Term GetInterpolCommand::getResult() const { return d_result; }
 
-void GetInterpolCommand::invoke(api::Solver* solver)
+void GetInterpolCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
 {
   try
   {
@@ -2120,7 +2106,6 @@ std::string GetInterpolCommand::getCommandName() const
 
 void GetInterpolCommand::toStream(std::ostream& out,
                                   int toDepth,
-
                                   size_t dag,
                                   OutputLanguage language) const
 {
@@ -2153,7 +2138,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)
+void GetAbductCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
 {
   try
   {
@@ -2206,7 +2191,6 @@ std::string GetAbductCommand::getCommandName() const { return "get-abduct"; }
 
 void GetAbductCommand::toStream(std::ostream& out,
                                 int toDepth,
-
                                 size_t dag,
                                 OutputLanguage language) const
 {
@@ -2230,7 +2214,8 @@ GetQuantifierEliminationCommand::GetQuantifierEliminationCommand(
 
 api::Term GetQuantifierEliminationCommand::getTerm() const { return d_term; }
 bool GetQuantifierEliminationCommand::getDoFull() const { return d_doFull; }
-void GetQuantifierEliminationCommand::invoke(api::Solver* solver)
+void GetQuantifierEliminationCommand::invoke(api::Solver* solver,
+                                             parser::SymbolManager* sm)
 {
   try
   {
@@ -2282,7 +2267,6 @@ std::string GetQuantifierEliminationCommand::getCommandName() const
 
 void GetQuantifierEliminationCommand::toStream(std::ostream& out,
                                                int toDepth,
-
                                                size_t dag,
                                                OutputLanguage language) const
 {
@@ -2296,7 +2280,8 @@ void GetQuantifierEliminationCommand::toStream(std::ostream& out,
 
 GetUnsatAssumptionsCommand::GetUnsatAssumptionsCommand() {}
 
-void GetUnsatAssumptionsCommand::invoke(api::Solver* solver)
+void GetUnsatAssumptionsCommand::invoke(api::Solver* solver,
+                                        parser::SymbolManager* sm)
 {
   try
   {
@@ -2345,7 +2330,6 @@ std::string GetUnsatAssumptionsCommand::getCommandName() const
 
 void GetUnsatAssumptionsCommand::toStream(std::ostream& out,
                                           int toDepth,
-
                                           size_t dag,
                                           OutputLanguage language) const
 {
@@ -2357,7 +2341,7 @@ void GetUnsatAssumptionsCommand::toStream(std::ostream& out,
 /* -------------------------------------------------------------------------- */
 
 GetUnsatCoreCommand::GetUnsatCoreCommand() {}
-void GetUnsatCoreCommand::invoke(api::Solver* solver)
+void GetUnsatCoreCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
 {
   try
   {
@@ -2411,7 +2395,6 @@ std::string GetUnsatCoreCommand::getCommandName() const
 
 void GetUnsatCoreCommand::toStream(std::ostream& out,
                                    int toDepth,
-
                                    size_t dag,
                                    OutputLanguage language) const
 {
@@ -2423,7 +2406,8 @@ void GetUnsatCoreCommand::toStream(std::ostream& out,
 /* -------------------------------------------------------------------------- */
 
 GetAssertionsCommand::GetAssertionsCommand() {}
-void GetAssertionsCommand::invoke(api::Solver* solver)
+void GetAssertionsCommand::invoke(api::Solver* solver,
+                                  parser::SymbolManager* sm)
 {
   try
   {
@@ -2469,7 +2453,6 @@ std::string GetAssertionsCommand::getCommandName() const
 
 void GetAssertionsCommand::toStream(std::ostream& out,
                                     int toDepth,
-
                                     size_t dag,
                                     OutputLanguage language) const
 {
@@ -2490,7 +2473,8 @@ BenchmarkStatus SetBenchmarkStatusCommand::getStatus() const
   return d_status;
 }
 
-void SetBenchmarkStatusCommand::invoke(api::Solver* solver)
+void SetBenchmarkStatusCommand::invoke(api::Solver* solver,
+                                       parser::SymbolManager* sm)
 {
   try
   {
@@ -2517,7 +2501,6 @@ std::string SetBenchmarkStatusCommand::getCommandName() const
 
 void SetBenchmarkStatusCommand::toStream(std::ostream& out,
                                          int toDepth,
-
                                          size_t dag,
                                          OutputLanguage language) const
 {
@@ -2542,7 +2525,8 @@ SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic)
 }
 
 std::string SetBenchmarkLogicCommand::getLogic() const { return d_logic; }
-void SetBenchmarkLogicCommand::invoke(api::Solver* solver)
+void SetBenchmarkLogicCommand::invoke(api::Solver* solver,
+                                      parser::SymbolManager* sm)
 {
   try
   {
@@ -2567,7 +2551,6 @@ std::string SetBenchmarkLogicCommand::getCommandName() const
 
 void SetBenchmarkLogicCommand::toStream(std::ostream& out,
                                         int toDepth,
-
                                         size_t dag,
                                         OutputLanguage language) const
 {
@@ -2585,7 +2568,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)
+void SetInfoCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
 {
   try
   {
@@ -2612,7 +2595,6 @@ std::string SetInfoCommand::getCommandName() const { return "set-info"; }
 
 void SetInfoCommand::toStream(std::ostream& out,
                               int toDepth,
-
                               size_t dag,
                               OutputLanguage language) const
 {
@@ -2625,7 +2607,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)
+void GetInfoCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
 {
   try
   {
@@ -2679,7 +2661,6 @@ std::string GetInfoCommand::getCommandName() const { return "get-info"; }
 
 void GetInfoCommand::toStream(std::ostream& out,
                               int toDepth,
-
                               size_t dag,
                               OutputLanguage language) const
 {
@@ -2697,7 +2678,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)
+void SetOptionCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
 {
   try
   {
@@ -2723,7 +2704,6 @@ std::string SetOptionCommand::getCommandName() const { return "set-option"; }
 
 void SetOptionCommand::toStream(std::ostream& out,
                                 int toDepth,
-
                                 size_t dag,
                                 OutputLanguage language) const
 {
@@ -2736,7 +2716,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)
+void GetOptionCommand::invoke(api::Solver* solver, parser::SymbolManager* sm)
 {
   try
   {
@@ -2777,7 +2757,6 @@ std::string GetOptionCommand::getCommandName() const { return "get-option"; }
 
 void GetOptionCommand::toStream(std::ostream& out,
                                 int toDepth,
-
                                 size_t dag,
                                 OutputLanguage language) const
 {
@@ -2794,7 +2773,8 @@ SetExpressionNameCommand::SetExpressionNameCommand(api::Term term,
 {
 }
 
-void SetExpressionNameCommand::invoke(api::Solver* solver)
+void SetExpressionNameCommand::invoke(api::Solver* solver,
+                                      parser::SymbolManager* sm)
 {
   solver->getSmtEngine()->setExpressionName(d_term.getExpr(), d_name);
   d_commandStatus = CommandSuccess::instance();
@@ -2813,7 +2793,6 @@ std::string SetExpressionNameCommand::getCommandName() const
 
 void SetExpressionNameCommand::toStream(std::ostream& out,
                                         int toDepth,
-
                                         size_t dag,
                                         OutputLanguage language) const
 {
@@ -2843,7 +2822,8 @@ const std::vector<api::Sort>& DatatypeDeclarationCommand::getDatatypes() const
   return d_datatypes;
 }
 
-void DatatypeDeclarationCommand::invoke(api::Solver* solver)
+void DatatypeDeclarationCommand::invoke(api::Solver* solver,
+                                        parser::SymbolManager* sm)
 {
   d_commandStatus = CommandSuccess::instance();
 }
@@ -2860,7 +2840,6 @@ std::string DatatypeDeclarationCommand::getCommandName() const
 
 void DatatypeDeclarationCommand::toStream(std::ostream& out,
                                           int toDepth,
-
                                           size_t dag,
                                           OutputLanguage language) const
 {
diff --git a/src/smt/command.h b/src/smt/command.h
index 438f9febb..310850b78 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -41,6 +41,10 @@ class Solver;
 class Term;
 }  // namespace api
 
+namespace parser {
+class SymbolManager;
+}
+
 class UnsatCore;
 class SmtEngine;
 class Command;
@@ -202,8 +206,16 @@ class CVC4_PUBLIC Command
 
   virtual ~Command();
 
-  virtual void invoke(api::Solver* solver) = 0;
-  virtual void invoke(api::Solver* solver, std::ostream& out);
+  /**
+   * Invoke the command on the solver and symbol manager sm.
+   */
+  virtual void invoke(api::Solver* solver, parser::SymbolManager* sm) = 0;
+  /**
+   * Same as above, and prints the result to output stream out.
+   */
+  virtual void invoke(api::Solver* solver,
+                      parser::SymbolManager* sm,
+                      std::ostream& out);
 
   virtual void toStream(
       std::ostream& out,
@@ -276,13 +288,12 @@ class CVC4_PUBLIC EmptyCommand : public Command
  public:
   EmptyCommand(std::string name = "");
   std::string getName() const;
-  void invoke(api::Solver* solver) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 
@@ -297,15 +308,16 @@ class CVC4_PUBLIC EchoCommand : public Command
 
   std::string getOutput() const;
 
-  void invoke(api::Solver* solver) override;
-  void invoke(api::Solver* solver, std::ostream& out) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver,
+              parser::SymbolManager* sm,
+              std::ostream& out) override;
 
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 
@@ -324,14 +336,13 @@ class CVC4_PUBLIC AssertCommand : public Command
 
   api::Term getTerm() const;
 
-  void invoke(api::Solver* solver) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
 
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class AssertCommand */
@@ -339,13 +350,12 @@ class CVC4_PUBLIC AssertCommand : public Command
 class CVC4_PUBLIC PushCommand : public Command
 {
  public:
-  void invoke(api::Solver* solver) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class PushCommand */
@@ -353,13 +363,12 @@ class CVC4_PUBLIC PushCommand : public Command
 class CVC4_PUBLIC PopCommand : public Command
 {
  public:
-  void invoke(api::Solver* solver) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class PopCommand */
@@ -372,7 +381,7 @@ class CVC4_PUBLIC DeclarationDefinitionCommand : public Command
  public:
   DeclarationDefinitionCommand(const std::string& id);
 
-  void invoke(api::Solver* solver) override = 0;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override = 0;
   std::string getSymbol() const;
 }; /* class DeclarationDefinitionCommand */
 
@@ -392,13 +401,12 @@ class CVC4_PUBLIC DeclareFunctionCommand : public DeclarationDefinitionCommand
   bool getPrintInModelSetByUser() const;
   void setPrintInModel(bool p);
 
-  void invoke(api::Solver* solver) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class DeclareFunctionCommand */
@@ -415,13 +423,12 @@ class CVC4_PUBLIC DeclareSortCommand : public DeclarationDefinitionCommand
   size_t getArity() const;
   api::Sort getSort() const;
 
-  void invoke(api::Solver* solver) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class DeclareSortCommand */
@@ -441,13 +448,12 @@ class CVC4_PUBLIC DefineSortCommand : public DeclarationDefinitionCommand
   const std::vector<api::Sort>& getParameters() const;
   api::Sort getSort() const;
 
-  void invoke(api::Solver* solver) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class DefineSortCommand */
@@ -469,13 +475,12 @@ class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand
   const std::vector<api::Term>& getFormals() const;
   api::Term getFormula() const;
 
-  void invoke(api::Solver* solver) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 
@@ -506,7 +511,7 @@ class CVC4_PUBLIC DefineNamedFunctionCommand : public DefineFunctionCommand
                              const std::vector<api::Term>& formals,
                              api::Term formula,
                              bool global);
-  void invoke(api::Solver* solver) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   Command* clone() const override;
   void toStream(
       std::ostream& out,
@@ -536,13 +541,12 @@ 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) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 
@@ -572,7 +576,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) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
@@ -603,13 +607,12 @@ class CVC4_PUBLIC SetUserAttributeCommand : public Command
                           api::Term term,
                           const std::string& value);
 
-  void invoke(api::Solver* solver) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 
@@ -637,14 +640,13 @@ class CVC4_PUBLIC CheckSatCommand : public Command
 
   api::Term getTerm() const;
   api::Result getResult() const;
-  void invoke(api::Solver* solver) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 
@@ -666,14 +668,13 @@ class CVC4_PUBLIC CheckSatAssumingCommand : public Command
 
   const std::vector<api::Term>& getTerms() const;
   api::Result getResult() const;
-  void invoke(api::Solver* solver) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 
@@ -694,14 +695,13 @@ class CVC4_PUBLIC QueryCommand : public Command
 
   api::Term getTerm() const;
   api::Result getResult() const;
-  void invoke(api::Solver* solver) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class QueryCommand */
@@ -722,7 +722,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) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   /** creates a copy of this command */
   Command* clone() const override;
   /** returns this command's name */
@@ -731,7 +731,6 @@ class CVC4_PUBLIC DeclareSygusVarCommand : public DeclarationDefinitionCommand
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 
@@ -772,7 +771,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) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   /** creates a copy of this command */
   Command* clone() const override;
   /** returns this command's name */
@@ -781,7 +780,6 @@ class CVC4_PUBLIC SynthFunCommand : public DeclarationDefinitionCommand
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 
@@ -810,7 +808,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) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   /** creates a copy of this command */
   Command* clone() const override;
   /** returns this command's name */
@@ -819,7 +817,6 @@ class CVC4_PUBLIC SygusConstraintCommand : public Command
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 
@@ -854,7 +851,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) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   /** creates a copy of this command */
   Command* clone() const override;
   /** returns this command's name */
@@ -863,7 +860,6 @@ class CVC4_PUBLIC SygusInvConstraintCommand : public Command
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 
@@ -891,7 +887,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) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   /** creates a copy of this command */
   Command* clone() const override;
   /** returns this command's name */
@@ -900,7 +896,6 @@ class CVC4_PUBLIC CheckSynthCommand : public Command
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 
@@ -925,14 +920,13 @@ class CVC4_PUBLIC SimplifyCommand : public Command
 
   api::Term getTerm() const;
   api::Term getResult() const;
-  void invoke(api::Solver* solver) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class SimplifyCommand */
@@ -949,14 +943,13 @@ class CVC4_PUBLIC GetValueCommand : public Command
 
   const std::vector<api::Term>& getTerms() const;
   api::Term getResult() const;
-  void invoke(api::Solver* solver) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class GetValueCommand */
@@ -970,14 +963,13 @@ class CVC4_PUBLIC GetAssignmentCommand : public Command
   GetAssignmentCommand();
 
   SExpr getResult() const;
-  void invoke(api::Solver* solver) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class GetAssignmentCommand */
@@ -989,14 +981,13 @@ class CVC4_PUBLIC GetModelCommand : public Command
 
   // Model is private to the library -- for now
   // Model* getResult() const ;
-  void invoke(api::Solver* solver) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 
@@ -1010,13 +1001,12 @@ class CVC4_PUBLIC BlockModelCommand : public Command
  public:
   BlockModelCommand();
 
-  void invoke(api::Solver* solver) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class BlockModelCommand */
@@ -1028,13 +1018,12 @@ 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) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 
@@ -1048,13 +1037,12 @@ class CVC4_PUBLIC GetProofCommand : public Command
  public:
   GetProofCommand();
 
-  void invoke(api::Solver* solver) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class GetProofCommand */
@@ -1064,14 +1052,13 @@ class CVC4_PUBLIC GetInstantiationsCommand : public Command
  public:
   GetInstantiationsCommand();
 
-  void invoke(api::Solver* solver) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 
@@ -1084,14 +1071,13 @@ class CVC4_PUBLIC GetSynthSolutionCommand : public Command
  public:
   GetSynthSolutionCommand();
 
-  void invoke(api::Solver* solver) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 
@@ -1123,14 +1109,13 @@ class CVC4_PUBLIC GetInterpolCommand : public Command
    * query. */
   api::Term getResult() const;
 
-  void invoke(api::Solver* solver) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 
@@ -1175,14 +1160,13 @@ class CVC4_PUBLIC GetAbductCommand : public Command
    */
   api::Term getResult() const;
 
-  void invoke(api::Solver* solver) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 
@@ -1212,7 +1196,7 @@ class CVC4_PUBLIC GetQuantifierEliminationCommand : public Command
 
   api::Term getTerm() const;
   bool getDoFull() const;
-  void invoke(api::Solver* solver) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   api::Term getResult() const;
   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
 
@@ -1221,7 +1205,6 @@ class CVC4_PUBLIC GetQuantifierEliminationCommand : public Command
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class GetQuantifierEliminationCommand */
@@ -1230,7 +1213,7 @@ class CVC4_PUBLIC GetUnsatAssumptionsCommand : public Command
 {
  public:
   GetUnsatAssumptionsCommand();
-  void invoke(api::Solver* solver) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   std::vector<api::Term> getResult() const;
   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
   Command* clone() const override;
@@ -1238,7 +1221,6 @@ class CVC4_PUBLIC GetUnsatAssumptionsCommand : public Command
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 
@@ -1252,7 +1234,7 @@ class CVC4_PUBLIC GetUnsatCoreCommand : public Command
   GetUnsatCoreCommand();
   const std::vector<api::Term>& getUnsatCore() const;
 
-  void invoke(api::Solver* solver) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
 
   Command* clone() const override;
@@ -1260,7 +1242,6 @@ class CVC4_PUBLIC GetUnsatCoreCommand : public Command
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 
@@ -1279,7 +1260,7 @@ class CVC4_PUBLIC GetAssertionsCommand : public Command
  public:
   GetAssertionsCommand();
 
-  void invoke(api::Solver* solver) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   std::string getResult() const;
   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
   Command* clone() const override;
@@ -1301,7 +1282,7 @@ class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command
 
   BenchmarkStatus getStatus() const;
 
-  void invoke(api::Solver* solver) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
@@ -1320,7 +1301,7 @@ class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command
   SetBenchmarkLogicCommand(std::string logic);
 
   std::string getLogic() const;
-  void invoke(api::Solver* solver) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
@@ -1342,7 +1323,7 @@ class CVC4_PUBLIC SetInfoCommand : public Command
   std::string getFlag() const;
   SExpr getSExpr() const;
 
-  void invoke(api::Solver* solver) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
@@ -1364,7 +1345,7 @@ class CVC4_PUBLIC GetInfoCommand : public Command
   std::string getFlag() const;
   std::string getResult() const;
 
-  void invoke(api::Solver* solver) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
   Command* clone() const override;
   std::string getCommandName() const override;
@@ -1387,13 +1368,12 @@ class CVC4_PUBLIC SetOptionCommand : public Command
   std::string getFlag() const;
   SExpr getSExpr() const;
 
-  void invoke(api::Solver* solver) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class SetOptionCommand */
@@ -1410,14 +1390,13 @@ class CVC4_PUBLIC GetOptionCommand : public Command
   std::string getFlag() const;
   std::string getResult() const;
 
-  void invoke(api::Solver* solver) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class GetOptionCommand */
@@ -1438,13 +1417,12 @@ class CVC4_PUBLIC SetExpressionNameCommand : public Command
  public:
   SetExpressionNameCommand(api::Term term, std::string name);
 
-  void invoke(api::Solver* solver) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class SetExpressionNameCommand */
@@ -1459,13 +1437,12 @@ 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) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class DatatypeDeclarationCommand */
@@ -1474,13 +1451,12 @@ class CVC4_PUBLIC ResetCommand : public Command
 {
  public:
   ResetCommand() {}
-  void invoke(api::Solver* solver) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class ResetCommand */
@@ -1489,13 +1465,12 @@ class CVC4_PUBLIC ResetAssertionsCommand : public Command
 {
  public:
   ResetAssertionsCommand() {}
-  void invoke(api::Solver* solver) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class ResetAssertionsCommand */
@@ -1504,13 +1479,12 @@ class CVC4_PUBLIC QuitCommand : public Command
 {
  public:
   QuitCommand() {}
-  void invoke(api::Solver* solver) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class QuitCommand */
@@ -1524,13 +1498,12 @@ class CVC4_PUBLIC CommentCommand : public Command
 
   std::string getComment() const;
 
-  void invoke(api::Solver* solver) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class CommentCommand */
@@ -1550,8 +1523,10 @@ class CVC4_PUBLIC CommandSequence : public Command
   void addCommand(Command* cmd);
   void clear();
 
-  void invoke(api::Solver* solver) override;
-  void invoke(api::Solver* solver, std::ostream& out) override;
+  void invoke(api::Solver* solver, parser::SymbolManager* sm) override;
+  void invoke(api::Solver* solver,
+              parser::SymbolManager* sm,
+              std::ostream& out) override;
 
   typedef std::vector<Command*>::iterator iterator;
   typedef std::vector<Command*>::const_iterator const_iterator;
@@ -1567,7 +1542,6 @@ class CVC4_PUBLIC CommandSequence : public Command
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 }; /* class CommandSequence */
@@ -1577,7 +1551,6 @@ class CVC4_PUBLIC DeclarationSequence : public CommandSequence
   void toStream(
       std::ostream& out,
       int toDepth = -1,
-
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
 };