Consolidate language types (#7065)

This PR combines the two enums InputLanguage and OutputLanguage into a single Language type. It makes sure that AST is not used as input language using a predicate whenever the option is set.

8 files changed, 278 insertions, 345 deletions

diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp
index 6292b5982..b78659d39 100644
--- a/src/smt/assertions.cpp
+++ b/src/smt/assertions.cpp
@@ -121,7 +121,7 @@ void Assertions::initializeCheckSat(const std::vector<Node>& assumptions,
 void Assertions::assertFormula(const Node& n)
 {
   ensureBoolean(n);
-  bool maybeHasFv = language::isInputLangSygus(options::inputLanguage());
+  bool maybeHasFv = language::isLangSygus(options::inputLanguage());
   addFormula(n, true, false, false, maybeHasFv);
 }
 
@@ -185,7 +185,7 @@ void Assertions::addFormula(TNode n,
       else
       {
         se << "Cannot process assertion with free variable.";
-        if (language::isInputLangSygus(options::inputLanguage()))
+        if (language::isLangSygus(options::inputLanguage()))
         {
           // Common misuse of SyGuS is to use top-level assert instead of
           // constraint when defining the synthesis conjecture.
@@ -207,7 +207,7 @@ void Assertions::addDefineFunDefinition(Node n, bool global)
   {
     // Global definitions are asserted at check-sat-time because we have to
     // make sure that they are always present
-    Assert(!language::isInputLangSygus(options::inputLanguage()));
+    Assert(!language::isLangSygus(options::inputLanguage()));
     d_globalDefineFunLemmas->emplace_back(n);
   }
   else
@@ -215,7 +215,7 @@ void Assertions::addDefineFunDefinition(Node n, bool global)
     // We don't permit functions-to-synthesize within recursive function
     // definitions currently. Thus, we should check for free variables if the
     // input language is SyGuS.
-    bool maybeHasFv = language::isInputLangSygus(options::inputLanguage());
+    bool maybeHasFv = language::isLangSygus(options::inputLanguage());
     addFormula(n, true, false, true, maybeHasFv);
   }
 }
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 3dafdd7f0..e6be0a646 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -223,7 +223,7 @@ std::string Command::toString() const
   return ss.str();
 }
 
-void CommandStatus::toStream(std::ostream& out, OutputLanguage language) const
+void CommandStatus::toStream(std::ostream& out, Language language) const
 {
   Printer::getPrinter(language)->toStream(out, this);
 }
@@ -300,7 +300,7 @@ std::string EmptyCommand::getCommandName() const { return "empty"; }
 void EmptyCommand::toStream(std::ostream& out,
                             int toDepth,
                             size_t dag,
-                            OutputLanguage language) const
+                            Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdEmpty(out, d_name);
 }
@@ -347,7 +347,7 @@ std::string EchoCommand::getCommandName() const { return "echo"; }
 void EchoCommand::toStream(std::ostream& out,
                            int toDepth,
                            size_t dag,
-                           OutputLanguage language) const
+                           Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdEcho(out, d_output);
 }
@@ -383,7 +383,7 @@ std::string AssertCommand::getCommandName() const { return "assert"; }
 void AssertCommand::toStream(std::ostream& out,
                              int toDepth,
                              size_t dag,
-                             OutputLanguage language) const
+                             Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdAssert(out, termToNode(d_term));
 }
@@ -415,7 +415,7 @@ std::string PushCommand::getCommandName() const { return "push"; }
 void PushCommand::toStream(std::ostream& out,
                            int toDepth,
                            size_t dag,
-                           OutputLanguage language) const
+                           Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdPush(out);
 }
@@ -447,7 +447,7 @@ std::string PopCommand::getCommandName() const { return "pop"; }
 void PopCommand::toStream(std::ostream& out,
                           int toDepth,
                           size_t dag,
-                          OutputLanguage language) const
+                          Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdPop(out);
 }
@@ -504,7 +504,7 @@ std::string CheckSatCommand::getCommandName() const { return "check-sat"; }
 void CheckSatCommand::toStream(std::ostream& out,
                                int toDepth,
                                size_t dag,
-                               OutputLanguage language) const
+                               Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdCheckSat(out, termToNode(d_term));
 }
@@ -578,7 +578,7 @@ std::string CheckSatAssumingCommand::getCommandName() const
 void CheckSatAssumingCommand::toStream(std::ostream& out,
                                        int toDepth,
                                        size_t dag,
-                                       OutputLanguage language) const
+                                       Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdCheckSatAssuming(
       out, termVectorToNodes(d_terms));
@@ -629,7 +629,7 @@ std::string QueryCommand::getCommandName() const { return "query"; }
 void QueryCommand::toStream(std::ostream& out,
                             int toDepth,
                             size_t dag,
-                            OutputLanguage language) const
+                            Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdQuery(out, termToNode(d_term));
 }
@@ -666,7 +666,7 @@ std::string DeclareSygusVarCommand::getCommandName() const
 void DeclareSygusVarCommand::toStream(std::ostream& out,
                                       int toDepth,
                                       size_t dag,
-                                      OutputLanguage language) const
+                                      Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdDeclareVar(
       out, termToNode(d_var), sortToTypeNode(d_sort));
@@ -723,7 +723,7 @@ std::string SynthFunCommand::getCommandName() const
 void SynthFunCommand::toStream(std::ostream& out,
                                int toDepth,
                                size_t dag,
-                               OutputLanguage language) const
+                               Language language) const
 {
   std::vector<Node> nodeVars = termVectorToNodes(d_vars);
   Printer::getPrinter(language)->toStreamCmdSynthFun(
@@ -770,7 +770,7 @@ std::string SygusConstraintCommand::getCommandName() const
 void SygusConstraintCommand::toStream(std::ostream& out,
                                       int toDepth,
                                       size_t dag,
-                                      OutputLanguage language) const
+                                      Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdConstraint(out, termToNode(d_term));
 }
@@ -825,7 +825,7 @@ std::string SygusInvConstraintCommand::getCommandName() const
 void SygusInvConstraintCommand::toStream(std::ostream& out,
                                          int toDepth,
                                          size_t dag,
-                                         OutputLanguage language) const
+                                         Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdInvConstraint(
       out,
@@ -866,7 +866,7 @@ void CheckSynthCommand::invoke(api::Solver* solver, SymbolManager* sm)
     {
       std::vector<api::Term> synthFuns = sm->getFunctionsToSynthesize();
       d_solution << "(" << std::endl;
-      Printer* p = Printer::getPrinter(language::output::LANG_SYGUS_V2);
+      Printer* p = Printer::getPrinter(Language::LANG_SYGUS_V2);
       for (api::Term& f : synthFuns)
       {
         api::Term sol = solver->getSynthSolution(f);
@@ -916,7 +916,7 @@ std::string CheckSynthCommand::getCommandName() const { return "check-synth"; }
 void CheckSynthCommand::toStream(std::ostream& out,
                                  int toDepth,
                                  size_t dag,
-                                 OutputLanguage language) const
+                                 Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdCheckSynth(out);
 }
@@ -945,7 +945,7 @@ std::string ResetCommand::getCommandName() const { return "reset"; }
 void ResetCommand::toStream(std::ostream& out,
                             int toDepth,
                             size_t dag,
-                            OutputLanguage language) const
+                            Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdReset(out);
 }
@@ -981,7 +981,7 @@ std::string ResetAssertionsCommand::getCommandName() const
 void ResetAssertionsCommand::toStream(std::ostream& out,
                                       int toDepth,
                                       size_t dag,
-                                      OutputLanguage language) const
+                                      Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdResetAssertions(out);
 }
@@ -1002,7 +1002,7 @@ std::string QuitCommand::getCommandName() const { return "exit"; }
 void QuitCommand::toStream(std::ostream& out,
                            int toDepth,
                            size_t dag,
-                           OutputLanguage language) const
+                           Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdQuit(out);
 }
@@ -1025,7 +1025,7 @@ std::string CommentCommand::getCommandName() const { return "comment"; }
 void CommentCommand::toStream(std::ostream& out,
                               int toDepth,
                               size_t dag,
-                              OutputLanguage language) const
+                              Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdComment(out, d_comment);
 }
@@ -1123,7 +1123,7 @@ std::string CommandSequence::getCommandName() const { return "sequence"; }
 void CommandSequence::toStream(std::ostream& out,
                                int toDepth,
                                size_t dag,
-                               OutputLanguage language) const
+                               Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdCommandSequence(out,
                                                             d_commandSequence);
@@ -1136,7 +1136,7 @@ void CommandSequence::toStream(std::ostream& out,
 void DeclarationSequence::toStream(std::ostream& out,
                                    int toDepth,
                                    size_t dag,
-                                   OutputLanguage language) const
+                                   Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdDeclarationSequence(
       out, d_commandSequence);
@@ -1190,7 +1190,7 @@ std::string DeclareFunctionCommand::getCommandName() const
 void DeclareFunctionCommand::toStream(std::ostream& out,
                                       int toDepth,
                                       size_t dag,
-                                      OutputLanguage language) const
+                                      Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdDeclareFunction(
       out, d_func.toString(), sortToTypeNode(d_sort));
@@ -1241,7 +1241,7 @@ std::string DeclarePoolCommand::getCommandName() const
 void DeclarePoolCommand::toStream(std::ostream& out,
                                   int toDepth,
                                   size_t dag,
-                                  OutputLanguage language) const
+                                  Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdDeclarePool(
       out,
@@ -1283,7 +1283,7 @@ std::string DeclareSortCommand::getCommandName() const
 void DeclareSortCommand::toStream(std::ostream& out,
                                   int toDepth,
                                   size_t dag,
-                                  OutputLanguage language) const
+                                  Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdDeclareType(out,
                                                         sortToTypeNode(d_sort));
@@ -1326,7 +1326,7 @@ std::string DefineSortCommand::getCommandName() const { return "define-sort"; }
 void DefineSortCommand::toStream(std::ostream& out,
                                  int toDepth,
                                  size_t dag,
-                                 OutputLanguage language) const
+                                 Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdDefineType(
       out, d_symbol, sortVectorToTypeNodes(d_params), sortToTypeNode(d_sort));
@@ -1399,7 +1399,7 @@ std::string DefineFunctionCommand::getCommandName() const
 void DefineFunctionCommand::toStream(std::ostream& out,
                                      int toDepth,
                                      size_t dag,
-                                     OutputLanguage language) const
+                                     Language language) const
 {
   TypeNode rangeType = termToNode(d_func).getType();
   if (rangeType.isFunction())
@@ -1483,7 +1483,7 @@ std::string DefineFunctionRecCommand::getCommandName() const
 void DefineFunctionRecCommand::toStream(std::ostream& out,
                                         int toDepth,
                                         size_t dag,
-                                        OutputLanguage language) const
+                                        Language language) const
 {
   std::vector<std::vector<Node>> formals;
   formals.reserve(d_formals.size());
@@ -1524,7 +1524,7 @@ std::string DeclareHeapCommand::getCommandName() const
 void DeclareHeapCommand::toStream(std::ostream& out,
                                   int toDepth,
                                   size_t dag,
-                                  OutputLanguage language) const
+                                  Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdDeclareHeap(
       out, sortToTypeNode(d_locSort), sortToTypeNode(d_dataSort));
@@ -1578,7 +1578,7 @@ std::string SimplifyCommand::getCommandName() const { return "simplify"; }
 void SimplifyCommand::toStream(std::ostream& out,
                                int toDepth,
                                size_t dag,
-                               OutputLanguage language) const
+                               Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdSimplify(out, termToNode(d_term));
 }
@@ -1658,7 +1658,7 @@ std::string GetValueCommand::getCommandName() const { return "get-value"; }
 void GetValueCommand::toStream(std::ostream& out,
                                int toDepth,
                                size_t dag,
-                               OutputLanguage language) const
+                               Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdGetValue(
       out, termVectorToNodes(d_terms));
@@ -1739,7 +1739,7 @@ std::string GetAssignmentCommand::getCommandName() const
 void GetAssignmentCommand::toStream(std::ostream& out,
                                     int toDepth,
                                     size_t dag,
-                                    OutputLanguage language) const
+                                    Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdGetAssignment(out);
 }
@@ -1812,7 +1812,7 @@ std::string GetModelCommand::getCommandName() const { return "get-model"; }
 void GetModelCommand::toStream(std::ostream& out,
                                int toDepth,
                                size_t dag,
-                               OutputLanguage language) const
+                               Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdGetModel(out);
 }
@@ -1854,7 +1854,7 @@ std::string BlockModelCommand::getCommandName() const { return "block-model"; }
 void BlockModelCommand::toStream(std::ostream& out,
                                  int toDepth,
                                  size_t dag,
-                                 OutputLanguage language) const
+                                 Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdBlockModel(out);
 }
@@ -1911,7 +1911,7 @@ std::string BlockModelValuesCommand::getCommandName() const
 void BlockModelValuesCommand::toStream(std::ostream& out,
                                        int toDepth,
                                        size_t dag,
-                                       OutputLanguage language) const
+                                       Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdBlockModelValues(
       out, termVectorToNodes(d_terms));
@@ -1962,7 +1962,7 @@ std::string GetProofCommand::getCommandName() const { return "get-proof"; }
 void GetProofCommand::toStream(std::ostream& out,
                                int toDepth,
                                size_t dag,
-                               OutputLanguage language) const
+                               Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdGetProof(out);
 }
@@ -2022,7 +2022,7 @@ std::string GetInstantiationsCommand::getCommandName() const
 void GetInstantiationsCommand::toStream(std::ostream& out,
                                         int toDepth,
                                         size_t dag,
-                                        OutputLanguage language) const
+                                        Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdGetInstantiations(out);
 }
@@ -2111,7 +2111,7 @@ std::string GetInterpolCommand::getCommandName() const
 void GetInterpolCommand::toStream(std::ostream& out,
                                   int toDepth,
                                   size_t dag,
-                                  OutputLanguage language) const
+                                  Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdGetInterpol(
       out, d_name, termToNode(d_conj), grammarToTypeNode(d_sygus_grammar));
@@ -2196,7 +2196,7 @@ std::string GetAbductCommand::getCommandName() const { return "get-abduct"; }
 void GetAbductCommand::toStream(std::ostream& out,
                                 int toDepth,
                                 size_t dag,
-                                OutputLanguage language) const
+                                Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdGetAbduct(
       out, d_name, termToNode(d_conj), grammarToTypeNode(d_sygus_grammar));
@@ -2272,7 +2272,7 @@ std::string GetQuantifierEliminationCommand::getCommandName() const
 void GetQuantifierEliminationCommand::toStream(std::ostream& out,
                                                int toDepth,
                                                size_t dag,
-                                               OutputLanguage language) const
+                                               Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdGetQuantifierElimination(
       out, termToNode(d_term));
@@ -2334,7 +2334,7 @@ std::string GetUnsatAssumptionsCommand::getCommandName() const
 void GetUnsatAssumptionsCommand::toStream(std::ostream& out,
                                           int toDepth,
                                           size_t dag,
-                                          OutputLanguage language) const
+                                          Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdGetUnsatAssumptions(out);
 }
@@ -2411,7 +2411,7 @@ std::string GetUnsatCoreCommand::getCommandName() const
 void GetUnsatCoreCommand::toStream(std::ostream& out,
                                    int toDepth,
                                    size_t dag,
-                                   OutputLanguage language) const
+                                   Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdGetUnsatCore(out);
 }
@@ -2468,7 +2468,7 @@ std::string GetAssertionsCommand::getCommandName() const
 void GetAssertionsCommand::toStream(std::ostream& out,
                                     int toDepth,
                                     size_t dag,
-                                    OutputLanguage language) const
+                                    Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdGetAssertions(out);
 }
@@ -2515,7 +2515,7 @@ std::string SetBenchmarkStatusCommand::getCommandName() const
 void SetBenchmarkStatusCommand::toStream(std::ostream& out,
                                          int toDepth,
                                          size_t dag,
-                                         OutputLanguage language) const
+                                         Language language) const
 {
   Result::Sat status = Result::SAT_UNKNOWN;
   switch (d_status)
@@ -2564,7 +2564,7 @@ std::string SetBenchmarkLogicCommand::getCommandName() const
 void SetBenchmarkLogicCommand::toStream(std::ostream& out,
                                         int toDepth,
                                         size_t dag,
-                                        OutputLanguage language) const
+                                        Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdSetBenchmarkLogic(out, d_logic);
 }
@@ -2609,7 +2609,7 @@ std::string SetInfoCommand::getCommandName() const { return "set-info"; }
 void SetInfoCommand::toStream(std::ostream& out,
                               int toDepth,
                               size_t dag,
-                              OutputLanguage language) const
+                              Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdSetInfo(out, d_flag, d_value);
 }
@@ -2665,7 +2665,7 @@ std::string GetInfoCommand::getCommandName() const { return "get-info"; }
 void GetInfoCommand::toStream(std::ostream& out,
                               int toDepth,
                               size_t dag,
-                              OutputLanguage language) const
+                              Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdGetInfo(out, d_flag);
 }
@@ -2709,7 +2709,7 @@ std::string SetOptionCommand::getCommandName() const { return "set-option"; }
 void SetOptionCommand::toStream(std::ostream& out,
                                 int toDepth,
                                 size_t dag,
-                                OutputLanguage language) const
+                                Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdSetOption(out, d_flag, d_value);
 }
@@ -2762,7 +2762,7 @@ std::string GetOptionCommand::getCommandName() const { return "get-option"; }
 void GetOptionCommand::toStream(std::ostream& out,
                                 int toDepth,
                                 size_t dag,
-                                OutputLanguage language) const
+                                Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdGetOption(out, d_flag);
 }
@@ -2807,7 +2807,7 @@ std::string DatatypeDeclarationCommand::getCommandName() const
 void DatatypeDeclarationCommand::toStream(std::ostream& out,
                                           int toDepth,
                                           size_t dag,
-                                          OutputLanguage language) const
+                                          Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdDatatypeDeclaration(
       out, sortVectorToTypeNodes(d_datatypes));
diff --git a/src/smt/command.h b/src/smt/command.h
index b83da5825..d3e3679d2 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -130,7 +130,7 @@ class CVC5_EXPORT CommandStatus
  public:
   virtual ~CommandStatus() {}
   void toStream(std::ostream& out,
-                OutputLanguage language = language::output::LANG_AUTO) const;
+                Language language = Language::LANG_AUTO) const;
   virtual CommandStatus& clone() const = 0;
 }; /* class CommandStatus */
 
@@ -217,12 +217,11 @@ class CVC5_EXPORT Command
                       SymbolManager* sm,
                       std::ostream& out);
 
-  virtual void toStream(
-      std::ostream& out,
-      int toDepth = -1,
+  virtual void toStream(std::ostream& out,
+                        int toDepth = -1,
 
-      size_t dag = 1,
-      OutputLanguage language = language::output::LANG_AUTO) const = 0;
+                        size_t dag = 1,
+                        Language language = Language::LANG_AUTO) const = 0;
 
   std::string toString() const;
 
@@ -316,11 +315,10 @@ class CVC5_EXPORT EmptyCommand : public Command
   void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
-  void toStream(
-      std::ostream& out,
-      int toDepth = -1,
-      size_t dag = 1,
-      OutputLanguage language = language::output::LANG_AUTO) const override;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 
  protected:
   std::string d_name;
@@ -340,11 +338,10 @@ class CVC5_EXPORT EchoCommand : public Command
 
   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;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 
  protected:
   std::string d_output;
@@ -364,11 +361,10 @@ class CVC5_EXPORT AssertCommand : public Command
 
   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;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 }; /* class AssertCommand */
 
 class CVC5_EXPORT PushCommand : public Command
@@ -377,11 +373,10 @@ class CVC5_EXPORT PushCommand : public Command
   void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
-  void toStream(
-      std::ostream& out,
-      int toDepth = -1,
-      size_t dag = 1,
-      OutputLanguage language = language::output::LANG_AUTO) const override;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 }; /* class PushCommand */
 
 class CVC5_EXPORT PopCommand : public Command
@@ -390,11 +385,10 @@ class CVC5_EXPORT PopCommand : public Command
   void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
-  void toStream(
-      std::ostream& out,
-      int toDepth = -1,
-      size_t dag = 1,
-      OutputLanguage language = language::output::LANG_AUTO) const override;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 }; /* class PopCommand */
 
 class CVC5_EXPORT DeclarationDefinitionCommand : public Command
@@ -423,11 +417,10 @@ class CVC5_EXPORT DeclareFunctionCommand : public DeclarationDefinitionCommand
   void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
-  void toStream(
-      std::ostream& out,
-      int toDepth = -1,
-      size_t dag = 1,
-      OutputLanguage language = language::output::LANG_AUTO) const override;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 }; /* class DeclareFunctionCommand */
 
 class CVC5_EXPORT DeclarePoolCommand : public DeclarationDefinitionCommand
@@ -449,11 +442,10 @@ class CVC5_EXPORT DeclarePoolCommand : public DeclarationDefinitionCommand
   void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
-  void toStream(
-      std::ostream& out,
-      int toDepth = -1,
-      size_t dag = 1,
-      OutputLanguage language = language::output::LANG_AUTO) const override;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 }; /* class DeclarePoolCommand */
 
 class CVC5_EXPORT DeclareSortCommand : public DeclarationDefinitionCommand
@@ -471,11 +463,10 @@ class CVC5_EXPORT DeclareSortCommand : public DeclarationDefinitionCommand
   void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
-  void toStream(
-      std::ostream& out,
-      int toDepth = -1,
-      size_t dag = 1,
-      OutputLanguage language = language::output::LANG_AUTO) const override;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 }; /* class DeclareSortCommand */
 
 class CVC5_EXPORT DefineSortCommand : public DeclarationDefinitionCommand
@@ -496,11 +487,10 @@ class CVC5_EXPORT DefineSortCommand : public DeclarationDefinitionCommand
   void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
-  void toStream(
-      std::ostream& out,
-      int toDepth = -1,
-      size_t dag = 1,
-      OutputLanguage language = language::output::LANG_AUTO) const override;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 }; /* class DefineSortCommand */
 
 class CVC5_EXPORT DefineFunctionCommand : public DeclarationDefinitionCommand
@@ -523,11 +513,10 @@ class CVC5_EXPORT DefineFunctionCommand : public DeclarationDefinitionCommand
   void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
-  void toStream(
-      std::ostream& out,
-      int toDepth = -1,
-      size_t dag = 1,
-      OutputLanguage language = language::output::LANG_AUTO) const override;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 
  protected:
   /** The function we are defining */
@@ -567,11 +556,10 @@ class CVC5_EXPORT DefineFunctionRecCommand : public Command
   void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
-  void toStream(
-      std::ostream& out,
-      int toDepth = -1,
-      size_t dag = 1,
-      OutputLanguage language = language::output::LANG_AUTO) const override;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 
  protected:
   /** functions we are defining */
@@ -602,11 +590,10 @@ class CVC5_EXPORT DeclareHeapCommand : public Command
   void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
-  void toStream(
-      std::ostream& out,
-      int toDepth = -1,
-      size_t dag = 1,
-      OutputLanguage language = language::output::LANG_AUTO) const override;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 
  protected:
   /** The location sort */
@@ -631,11 +618,10 @@ class CVC5_EXPORT CheckSatCommand : public Command
   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;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 
  private:
   api::Term d_term;
@@ -659,11 +645,10 @@ class CVC5_EXPORT CheckSatAssumingCommand : public Command
   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;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 
  private:
   std::vector<api::Term> d_terms;
@@ -685,11 +670,10 @@ class CVC5_EXPORT QueryCommand : public Command
   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;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 }; /* class QueryCommand */
 
 /* ------------------- sygus commands  ------------------ */
@@ -714,11 +698,10 @@ class CVC5_EXPORT DeclareSygusVarCommand : public DeclarationDefinitionCommand
   /** returns this command's name */
   std::string getCommandName() const override;
   /** prints this command */
-  void toStream(
-      std::ostream& out,
-      int toDepth = -1,
-      size_t dag = 1,
-      OutputLanguage language = language::output::LANG_AUTO) const override;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 
  protected:
   /** the declared variable */
@@ -763,11 +746,10 @@ class CVC5_EXPORT SynthFunCommand : public DeclarationDefinitionCommand
   /** returns this command's name */
   std::string getCommandName() const override;
   /** prints this command */
-  void toStream(
-      std::ostream& out,
-      int toDepth = -1,
-      size_t dag = 1,
-      OutputLanguage language = language::output::LANG_AUTO) const override;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 
  protected:
   /** the function-to-synthesize */
@@ -800,11 +782,10 @@ class CVC5_EXPORT SygusConstraintCommand : public Command
   /** returns this command's name */
   std::string getCommandName() const override;
   /** prints this command */
-  void toStream(
-      std::ostream& out,
-      int toDepth = -1,
-      size_t dag = 1,
-      OutputLanguage language = language::output::LANG_AUTO) const override;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 
  protected:
   /** the declared constraint */
@@ -843,11 +824,10 @@ class CVC5_EXPORT SygusInvConstraintCommand : public Command
   /** returns this command's name */
   std::string getCommandName() const override;
   /** prints this command */
-  void toStream(
-      std::ostream& out,
-      int toDepth = -1,
-      size_t dag = 1,
-      OutputLanguage language = language::output::LANG_AUTO) const override;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 
  protected:
   /** the place holder predicates with which to build the actual constraint
@@ -879,11 +859,10 @@ class CVC5_EXPORT CheckSynthCommand : public Command
   /** returns this command's name */
   std::string getCommandName() const override;
   /** prints this command */
-  void toStream(
-      std::ostream& out,
-      int toDepth = -1,
-      size_t dag = 1,
-      OutputLanguage language = language::output::LANG_AUTO) const override;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 
  protected:
   /** result of the check-synth call */
@@ -910,11 +889,10 @@ class CVC5_EXPORT SimplifyCommand : public Command
   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;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 }; /* class SimplifyCommand */
 
 class CVC5_EXPORT GetValueCommand : public Command
@@ -933,11 +911,10 @@ class CVC5_EXPORT GetValueCommand : public Command
   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;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 }; /* class GetValueCommand */
 
 class CVC5_EXPORT GetAssignmentCommand : public Command
@@ -953,11 +930,10 @@ class CVC5_EXPORT GetAssignmentCommand : public Command
   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;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 }; /* class GetAssignmentCommand */
 
 class CVC5_EXPORT GetModelCommand : public Command
@@ -968,11 +944,10 @@ class CVC5_EXPORT GetModelCommand : public Command
   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;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 
  protected:
   smt::Model* d_result;
@@ -987,11 +962,10 @@ class CVC5_EXPORT BlockModelCommand : public Command
   void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
-  void toStream(
-      std::ostream& out,
-      int toDepth = -1,
-      size_t dag = 1,
-      OutputLanguage language = language::output::LANG_AUTO) const override;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 }; /* class BlockModelCommand */
 
 /** The command to block model values. */
@@ -1004,11 +978,10 @@ class CVC5_EXPORT BlockModelValuesCommand : public Command
   void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
-  void toStream(
-      std::ostream& out,
-      int toDepth = -1,
-      size_t dag = 1,
-      OutputLanguage language = language::output::LANG_AUTO) const override;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 
  protected:
   /** The terms we are blocking */
@@ -1026,11 +999,10 @@ class CVC5_EXPORT GetProofCommand : public Command
 
   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;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 
  private:
   /** the result of the getProof call */
@@ -1047,11 +1019,10 @@ class CVC5_EXPORT GetInstantiationsCommand : public Command
   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;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 
  protected:
   api::Solver* d_solver;
@@ -1085,11 +1056,10 @@ class CVC5_EXPORT GetInterpolCommand : public Command
   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;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 
  protected:
   /** The name of the interpolation predicate */
@@ -1136,11 +1106,10 @@ class CVC5_EXPORT GetAbductCommand : public Command
   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;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 
  protected:
   /** The name of the abduction predicate */
@@ -1174,11 +1143,10 @@ class CVC5_EXPORT GetQuantifierEliminationCommand : public Command
 
   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;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 }; /* class GetQuantifierEliminationCommand */
 
 class CVC5_EXPORT GetUnsatAssumptionsCommand : public Command
@@ -1190,11 +1158,10 @@ class CVC5_EXPORT GetUnsatAssumptionsCommand : public Command
   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;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 
  protected:
   std::vector<api::Term> d_result;
@@ -1211,11 +1178,10 @@ class CVC5_EXPORT GetUnsatCoreCommand : public Command
 
   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;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 
  protected:
   /** The symbol manager we were invoked with */
@@ -1237,11 +1203,10 @@ class CVC5_EXPORT GetAssertionsCommand : public Command
   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;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 }; /* class GetAssertionsCommand */
 
 class CVC5_EXPORT SetBenchmarkStatusCommand : public Command
@@ -1257,11 +1222,10 @@ class CVC5_EXPORT SetBenchmarkStatusCommand : public Command
   void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
-  void toStream(
-      std::ostream& out,
-      int toDepth = -1,
-      size_t dag = 1,
-      OutputLanguage language = language::output::LANG_AUTO) const override;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 }; /* class SetBenchmarkStatusCommand */
 
 class CVC5_EXPORT SetBenchmarkLogicCommand : public Command
@@ -1276,11 +1240,10 @@ class CVC5_EXPORT SetBenchmarkLogicCommand : public Command
   void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
-  void toStream(
-      std::ostream& out,
-      int toDepth = -1,
-      size_t dag = 1,
-      OutputLanguage language = language::output::LANG_AUTO) const override;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 }; /* class SetBenchmarkLogicCommand */
 
 class CVC5_EXPORT SetInfoCommand : public Command
@@ -1298,11 +1261,10 @@ class CVC5_EXPORT SetInfoCommand : public Command
   void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
-  void toStream(
-      std::ostream& out,
-      int toDepth = -1,
-      size_t dag = 1,
-      OutputLanguage language = language::output::LANG_AUTO) const override;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 }; /* class SetInfoCommand */
 
 class CVC5_EXPORT GetInfoCommand : public Command
@@ -1321,11 +1283,10 @@ class CVC5_EXPORT GetInfoCommand : public Command
   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;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 }; /* class GetInfoCommand */
 
 class CVC5_EXPORT SetOptionCommand : public Command
@@ -1343,11 +1304,10 @@ class CVC5_EXPORT SetOptionCommand : public Command
   void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
-  void toStream(
-      std::ostream& out,
-      int toDepth = -1,
-      size_t dag = 1,
-      OutputLanguage language = language::output::LANG_AUTO) const override;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 }; /* class SetOptionCommand */
 
 class CVC5_EXPORT GetOptionCommand : public Command
@@ -1366,11 +1326,10 @@ class CVC5_EXPORT GetOptionCommand : public Command
   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;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 }; /* class GetOptionCommand */
 
 class CVC5_EXPORT DatatypeDeclarationCommand : public Command
@@ -1386,11 +1345,10 @@ class CVC5_EXPORT DatatypeDeclarationCommand : public Command
   void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
-  void toStream(
-      std::ostream& out,
-      int toDepth = -1,
-      size_t dag = 1,
-      OutputLanguage language = language::output::LANG_AUTO) const override;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 }; /* class DatatypeDeclarationCommand */
 
 class CVC5_EXPORT ResetCommand : public Command
@@ -1400,11 +1358,10 @@ class CVC5_EXPORT ResetCommand : public Command
   void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
-  void toStream(
-      std::ostream& out,
-      int toDepth = -1,
-      size_t dag = 1,
-      OutputLanguage language = language::output::LANG_AUTO) const override;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 }; /* class ResetCommand */
 
 class CVC5_EXPORT ResetAssertionsCommand : public Command
@@ -1414,11 +1371,10 @@ class CVC5_EXPORT ResetAssertionsCommand : public Command
   void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
-  void toStream(
-      std::ostream& out,
-      int toDepth = -1,
-      size_t dag = 1,
-      OutputLanguage language = language::output::LANG_AUTO) const override;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 }; /* class ResetAssertionsCommand */
 
 class CVC5_EXPORT QuitCommand : public Command
@@ -1428,11 +1384,10 @@ class CVC5_EXPORT QuitCommand : public Command
   void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
-  void toStream(
-      std::ostream& out,
-      int toDepth = -1,
-      size_t dag = 1,
-      OutputLanguage language = language::output::LANG_AUTO) const override;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 }; /* class QuitCommand */
 
 class CVC5_EXPORT CommentCommand : public Command
@@ -1447,11 +1402,10 @@ class CVC5_EXPORT CommentCommand : public Command
   void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
   std::string getCommandName() const override;
-  void toStream(
-      std::ostream& out,
-      int toDepth = -1,
-      size_t dag = 1,
-      OutputLanguage language = language::output::LANG_AUTO) const override;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 }; /* class CommentCommand */
 
 class CVC5_EXPORT CommandSequence : public Command
@@ -1485,20 +1439,18 @@ class CVC5_EXPORT CommandSequence : public Command
 
   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;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 }; /* class CommandSequence */
 
 class CVC5_EXPORT DeclarationSequence : public CommandSequence
 {
-  void toStream(
-      std::ostream& out,
-      int toDepth = -1,
-      size_t dag = 1,
-      OutputLanguage language = language::output::LANG_AUTO) const override;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
 };
 
 }  // namespace cvc5
diff --git a/src/smt/node_command.cpp b/src/smt/node_command.cpp
index b3e747ecb..000107341 100644
--- a/src/smt/node_command.cpp
+++ b/src/smt/node_command.cpp
@@ -59,7 +59,7 @@ DeclareFunctionNodeCommand::DeclareFunctionNodeCommand(const std::string& id,
 void DeclareFunctionNodeCommand::toStream(std::ostream& out,
                                           int toDepth,
                                           size_t dag,
-                                          OutputLanguage language) const
+                                          Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdDeclareFunction(out, d_id, d_type);
 }
@@ -85,7 +85,7 @@ DeclareTypeNodeCommand::DeclareTypeNodeCommand(const std::string& id,
 void DeclareTypeNodeCommand::toStream(std::ostream& out,
                                       int toDepth,
                                       size_t dag,
-                                      OutputLanguage language) const
+                                      Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdDeclareType(out, d_type);
 }
@@ -112,7 +112,7 @@ DeclareDatatypeNodeCommand::DeclareDatatypeNodeCommand(
 void DeclareDatatypeNodeCommand::toStream(std::ostream& out,
                                           int toDepth,
                                           size_t dag,
-                                          OutputLanguage language) const
+                                          Language language) const
 {
   Printer::getPrinter(language)->toStreamCmdDatatypeDeclaration(out,
                                                                 d_datatypes);
@@ -139,7 +139,7 @@ DefineFunctionNodeCommand::DefineFunctionNodeCommand(
 void DefineFunctionNodeCommand::toStream(std::ostream& out,
                                          int toDepth,
                                          size_t dag,
-                                         OutputLanguage language) const
+                                         Language language) const
 {
   TypeNode tn = d_fun.getType();
   bool hasRange =
diff --git a/src/smt/node_command.h b/src/smt/node_command.h
index 0bd60fe9a..3399cb6fb 100644
--- a/src/smt/node_command.h
+++ b/src/smt/node_command.h
@@ -37,11 +37,10 @@ class NodeCommand
   virtual ~NodeCommand();
 
   /** Print this NodeCommand to output stream */
-  virtual void toStream(
-      std::ostream& out,
-      int toDepth = -1,
-      size_t dag = 1,
-      OutputLanguage language = language::output::LANG_AUTO) const = 0;
+  virtual void toStream(std::ostream& out,
+                        int toDepth = -1,
+                        size_t dag = 1,
+                        Language language = Language::LANG_AUTO) const = 0;
 
   /** Get a string representation of this NodeCommand */
   std::string toString() const;
@@ -60,11 +59,10 @@ class DeclareFunctionNodeCommand : public NodeCommand
 {
  public:
   DeclareFunctionNodeCommand(const std::string& id, Node fun, TypeNode type);
-  void toStream(
-      std::ostream& out,
-      int toDepth = -1,
-      size_t dag = 1,
-      OutputLanguage language = language::output::LANG_AUTO) const override;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
   NodeCommand* clone() const override;
   const Node& getFunction() const;
 
@@ -82,11 +80,10 @@ class DeclareDatatypeNodeCommand : public NodeCommand
 {
  public:
   DeclareDatatypeNodeCommand(const std::vector<TypeNode>& datatypes);
-  void toStream(
-      std::ostream& out,
-      int toDepth = -1,
-      size_t dag = 1,
-      OutputLanguage language = language::output::LANG_AUTO) const override;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
   NodeCommand* clone() const override;
 
  private:
@@ -101,11 +98,10 @@ class DeclareTypeNodeCommand : public NodeCommand
 {
  public:
   DeclareTypeNodeCommand(const std::string& id, size_t arity, TypeNode type);
-  void toStream(
-      std::ostream& out,
-      int toDepth = -1,
-      size_t dag = 1,
-      OutputLanguage language = language::output::LANG_AUTO) const override;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
   NodeCommand* clone() const override;
   const std::string getSymbol() const;
   const TypeNode& getType() const;
@@ -127,11 +123,10 @@ class DefineFunctionNodeCommand : public NodeCommand
                             Node fun,
                             const std::vector<Node>& formals,
                             Node formula);
-  void toStream(
-      std::ostream& out,
-      int toDepth = -1,
-      size_t dag = 1,
-      OutputLanguage language = language::output::LANG_AUTO) const override;
+  void toStream(std::ostream& out,
+                int toDepth = -1,
+                size_t dag = 1,
+                Language language = Language::LANG_AUTO) const override;
   NodeCommand* clone() const override;
 
  private:
diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp
index 5730ea062..fecf65275 100644
--- a/src/smt/optimization_solver.cpp
+++ b/src/smt/optimization_solver.cpp
@@ -33,8 +33,8 @@ namespace smt {
 std::ostream& operator<<(std::ostream& out, const OptimizationResult& result)
 {
   // check the output language first
-  OutputLanguage lang = language::SetLanguage::getLanguage(out);
-  if (!language::isOutputLang_smt2(lang))
+  Language lang = language::SetLanguage::getLanguage(out);
+  if (!language::isLangSmt2(lang))
   {
     Unimplemented()
         << "Only the SMTLib2 language supports optimization right now";
@@ -67,8 +67,8 @@ std::ostream& operator<<(std::ostream& out,
                          const OptimizationObjective& objective)
 {
   // check the output language first
-  OutputLanguage lang = language::SetLanguage::getLanguage(out);
-  if (!language::isOutputLang_smt2(lang))
+  Language lang = language::SetLanguage::getLanguage(out);
+  if (!language::isLangSmt2(lang))
   {
     Unimplemented()
         << "Only the SMTLib2 language supports optimization right now";
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index d158d5010..ec15e67e6 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -1006,7 +1006,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
 
 bool SetDefaults::isSygus(const Options& opts) const
 {
-  if (language::isInputLangSygus(opts.base.inputLanguage))
+  if (language::isLangSygus(opts.base.inputLanguage))
   {
     return true;
   }
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f55bfa88b..45056057d 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -438,7 +438,7 @@ void SmtEngine::setInfo(const std::string& key, const std::string& value)
   }
   else if (key == "smt-lib-version" && !getOptions().base.inputLanguageWasSetByUser)
   {
-    language::input::Language ilang = language::input::LANG_SMTLIB_V2_6;
+    Language ilang = Language::LANG_SMTLIB_V2_6;
 
     if (value != "2" && value != "2.6")
     {
@@ -450,7 +450,7 @@ void SmtEngine::setInfo(const std::string& key, const std::string& value)
     // also update the output language
     if (!getOptions().base.outputLanguageWasSetByUser)
     {
-      language::output::Language olang = language::toOutputLanguage(ilang);
+      Language olang = ilang;
       if (d_env->getOptions().base.outputLanguage != olang)
       {
         getOptions().base.outputLanguage = olang;
@@ -2022,21 +2022,7 @@ std::string SmtEngine::getOption(const std::string& key) const
     return nm->mkNode(Kind::SEXPR, result).toString();
   }
 
-  std::string atom = options::get(getOptions(), key);
-
-  if (atom != "true" && atom != "false")
-  {
-    try
-    {
-      Integer z(atom);
-    }
-    catch (std::invalid_argument&)
-    {
-      atom = "\"" + atom + "\"";
-    }
-  }
-
-  return atom;
+  return options::get(getOptions(), key);
 }
 
 Options& SmtEngine::getOptions() { return d_env->d_options; }