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.

1 files changed, 49 insertions, 49 deletions

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