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.

1 files changed, 70 insertions, 97 deletions

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;
 };