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.

9 files changed, 38 insertions, 37 deletions

diff --git a/test/api/ouroborous.cpp b/test/api/ouroborous.cpp
index c226da13b..92e58085d 100644
--- a/test/api/ouroborous.cpp
+++ b/test/api/ouroborous.cpp
@@ -96,8 +96,8 @@ std::string parse(std::string instr,
   }
 
   api::Solver solver;
-  InputLanguage ilang =
-      input_language == "smt2" ? input::LANG_SMTLIB_V2 : input::LANG_CVC;
+  Language ilang = input_language == "smt2" ? Language::LANG_SMTLIB_V2_6
+                                            : Language::LANG_CVC;
 
   solver.setOption("input-language", input_language);
   solver.setOption("output-language", output_language);
@@ -129,19 +129,19 @@ std::string translate(std::string instr,
 
   std::cout << "==============================================" << std::endl
             << "translating from "
-            << (input_language == "smt2" ? input::LANG_SMTLIB_V2
-                                         : input::LANG_CVC)
+            << (input_language == "smt2" ? Language::LANG_SMTLIB_V2_6
+                                         : Language::LANG_CVC)
             << " to "
-            << (output_language == "smt2" ? output::LANG_SMTLIB_V2
-                                          : output::LANG_CVC)
+            << (output_language == "smt2" ? Language::LANG_SMTLIB_V2_6
+                                          : Language::LANG_CVC)
             << " this string:" << std::endl
             << instr << std::endl;
   std::string outstr = parse(instr, input_language, output_language);
   std::cout << "got this:" << std::endl
             << outstr << std::endl
             << "reparsing as "
-            << (output_language == "smt2" ? input::LANG_SMTLIB_V2
-                                          : input::LANG_CVC)
+            << (output_language == "smt2" ? Language::LANG_SMTLIB_V2_6
+                                          : Language::LANG_CVC)
             << std::endl;
   std::string poutstr = parse(outstr, output_language, output_language);
   assert(outstr == poutstr);
@@ -155,7 +155,7 @@ void runTestString(std::string instr, std::string instr_language)
 {
   std::cout << std::endl
             << "starting with: " << instr << std::endl
-            << "   in language " << input::LANG_SMTLIB_V2 << std::endl;
+            << "   in language " << Language::LANG_SMTLIB_V2_6 << std::endl;
   std::string smt2str = translate(instr, instr_language, "smt2");
   std::cout << "in SMT2      : " << smt2str << std::endl;
   std::string cvcstr = translate(smt2str, "smt2", "cvc");
diff --git a/test/api/smt2_compliance.cpp b/test/api/smt2_compliance.cpp
index b96f436c6..921d7585f 100644
--- a/test/api/smt2_compliance.cpp
+++ b/test/api/smt2_compliance.cpp
@@ -35,7 +35,7 @@ void testGetInfo(api::Solver* solver, const char* s);
 
 int main()
 {
-  cout << language::SetLanguage(language::output::LANG_SMTLIB_V2);
+  cout << language::SetLanguage(Language::LANG_SMTLIB_V2_6);
 
   std::unique_ptr<api::Solver> solver = std::make_unique<api::Solver>();
   solver->setOption("input-language", "smtlib2");
@@ -61,7 +61,7 @@ void testGetInfo(api::Solver* solver, const char* s)
 
   std::unique_ptr<Parser> p(
       ParserBuilder(solver, symman.get(), solver->getOptions()).build());
-  p->setInput(Input::newStringInput(language::input::LANG_SMTLIB_V2,
+  p->setInput(Input::newStringInput(Language::LANG_SMTLIB_V2_6,
                                     string("(get-info ") + s + ")",
                                     "<internal>"));
   assert(p != NULL);
diff --git a/test/regress/regress0/lang_opts_2_6_1.smt2 b/test/regress/regress0/lang_opts_2_6_1.smt2
index 9701df455..19c0eb10b 100644
--- a/test/regress/regress0/lang_opts_2_6_1.smt2
+++ b/test/regress/regress0/lang_opts_2_6_1.smt2
@@ -2,6 +2,6 @@
 ; than the language specified in the input file.
 ;
 ; COMMAND-LINE: --lang=smt2.6
-; EXPECT: "LANG_SMTLIB_V2_6"
+; EXPECT: LANG_SMTLIB_V2_6
 (set-info :smt-lib-version 2.6)
 (get-option :input-language)
diff --git a/test/regress/regress0/options/set-and-get-options.smt2 b/test/regress/regress0/options/set-and-get-options.smt2
index 478e3d523..6b07dfc1c 100644
--- a/test/regress/regress0/options/set-and-get-options.smt2
+++ b/test/regress/regress0/options/set-and-get-options.smt2
@@ -3,7 +3,7 @@
 ; EXPECT: true
 ; EXPECT: false
 ; EXPECT: 15
-; EXPECT: "SimplificationMode::NONE"
+; EXPECT: SimplificationMode::NONE
 
 (get-option :command-verbosity)
 (set-option :command-verbosity (* 1))
diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp
index 45801798b..0001b3723 100644
--- a/test/unit/node/node_black.cpp
+++ b/test/unit/node/node_black.cpp
@@ -67,7 +67,7 @@ class TestNodeBlackNode : public TestNode
     TestNode::SetUp();
     // setup an SMT engine so that options are in scope
     Options opts;
-    opts.base.outputLanguage = OutputLanguage::LANG_AST;
+    opts.base.outputLanguage = Language::LANG_AST;
     opts.base.outputLanguageWasSetByUser = true;
     d_smt.reset(new SmtEngine(d_nodeManager.get(), &opts));
   }
@@ -643,7 +643,7 @@ TEST_F(TestNodeBlackNode, dagifier)
       OR, {fffx_eq_x, fffx_eq_y, fx_eq_gx, x_eq_y, fgx_eq_gy});
 
   std::stringstream sstr;
-  sstr << Node::setdepth(-1) << Node::setlanguage(language::output::LANG_CVC);
+  sstr << Node::setdepth(-1) << Node::setlanguage(Language::LANG_CVC);
   sstr << Node::dag(false) << n;  // never dagify
   ASSERT_EQ(sstr.str(),
             "(f(f(f(x))) = x) OR (f(f(f(x))) = y) OR (f(x) = g(x)) OR (x = "
diff --git a/test/unit/parser/parser_black.cpp b/test/unit/parser/parser_black.cpp
index 8c8ef15d7..42b7d41f7 100644
--- a/test/unit/parser/parser_black.cpp
+++ b/test/unit/parser/parser_black.cpp
@@ -30,14 +30,13 @@
 namespace cvc5 {
 
 using namespace parser;
-using namespace language::input;
 
 namespace test {
 
 class TestParserBlackParser : public TestInternal
 {
  protected:
-  TestParserBlackParser(InputLanguage lang) : d_lang(lang) {}
+  TestParserBlackParser(Language lang) : d_lang(lang) {}
 
   virtual ~TestParserBlackParser() {}
 
@@ -125,7 +124,7 @@ class TestParserBlackParser : public TestInternal
                                        .withInputLanguage(d_lang)
                                        .build());
     parser->setInput(Input::newStringInput(d_lang, goodExpr, "test"));
-    if (d_lang == LANG_SMTLIB_V2)
+    if (d_lang == Language::LANG_SMTLIB_V2_6)
     {
       /* Use QF_LIA to make multiplication ("*") available */
       std::unique_ptr<Command> cmd(
@@ -170,7 +169,7 @@ class TestParserBlackParser : public TestInternal
                  , ParserException);
   }
 
-  InputLanguage d_lang;
+  Language d_lang;
   std::unique_ptr<cvc5::api::Solver> d_solver;
   std::unique_ptr<SymbolManager> d_symman;
 };
@@ -180,7 +179,7 @@ class TestParserBlackParser : public TestInternal
 class TestParserBlackCvCParser : public TestParserBlackParser
 {
  protected:
-  TestParserBlackCvCParser() : TestParserBlackParser(LANG_CVC) {}
+  TestParserBlackCvCParser() : TestParserBlackParser(Language::LANG_CVC) {}
 };
 
 TEST_F(TestParserBlackCvCParser, good_inputs)
@@ -278,7 +277,10 @@ TEST_F(TestParserBlackCvCParser, bad_exprs)
 class TestParserBlackSmt2Parser : public TestParserBlackParser
 {
  protected:
-  TestParserBlackSmt2Parser() : TestParserBlackParser(LANG_SMTLIB_V2) {}
+  TestParserBlackSmt2Parser()
+      : TestParserBlackParser(Language::LANG_SMTLIB_V2_6)
+  {
+  }
 };
 
 TEST_F(TestParserBlackSmt2Parser, good_inputs)
diff --git a/test/unit/parser/parser_builder_black.cpp b/test/unit/parser/parser_builder_black.cpp
index fa532f6b6..b941a4eda 100644
--- a/test/unit/parser/parser_builder_black.cpp
+++ b/test/unit/parser/parser_builder_black.cpp
@@ -31,7 +31,6 @@
 namespace cvc5 {
 
 using namespace parser;
-using namespace language::input;
 
 namespace test {
 
@@ -72,9 +71,9 @@ TEST_F(TestParseBlackParserBuilder, empty_file_input)
   ASSERT_NE(filename, nullptr);
 
   std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get())
-                                     .withInputLanguage(LANG_CVC)
+                                     .withInputLanguage(Language::LANG_CVC)
                                      .build());
-  parser->setInput(Input::newFileInput(LANG_CVC, filename, false));
+  parser->setInput(Input::newFileInput(Language::LANG_CVC, filename, false));
   checkEmptyInput(parser.get());
 
   remove(filename);
@@ -90,9 +89,9 @@ TEST_F(TestParseBlackParserBuilder, simple_file_input)
   fs.close();
 
   std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get())
-                                     .withInputLanguage(LANG_CVC)
+                                     .withInputLanguage(Language::LANG_CVC)
                                      .build());
-  parser->setInput(Input::newFileInput(LANG_CVC, filename, false));
+  parser->setInput(Input::newFileInput(Language::LANG_CVC, filename, false));
   checkTrueInput(parser.get());
 
   remove(filename);
@@ -102,18 +101,18 @@ TEST_F(TestParseBlackParserBuilder, simple_file_input)
 TEST_F(TestParseBlackParserBuilder, empty_string_input)
 {
   std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get())
-                                     .withInputLanguage(LANG_CVC)
+                                     .withInputLanguage(Language::LANG_CVC)
                                      .build());
-  parser->setInput(Input::newStringInput(LANG_CVC, "", "foo"));
+  parser->setInput(Input::newStringInput(Language::LANG_CVC, "", "foo"));
   checkEmptyInput(parser.get());
 }
 
 TEST_F(TestParseBlackParserBuilder, true_string_input)
 {
   std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get())
-                                     .withInputLanguage(LANG_CVC)
+                                     .withInputLanguage(Language::LANG_CVC)
                                      .build());
-  parser->setInput(Input::newStringInput(LANG_CVC, "TRUE", "foo"));
+  parser->setInput(Input::newStringInput(Language::LANG_CVC, "TRUE", "foo"));
   checkTrueInput(parser.get());
 }
 
@@ -121,9 +120,9 @@ TEST_F(TestParseBlackParserBuilder, empty_stream_input)
 {
   std::stringstream ss("", std::ios_base::in);
   std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get())
-                                     .withInputLanguage(LANG_CVC)
+                                     .withInputLanguage(Language::LANG_CVC)
                                      .build());
-  parser->setInput(Input::newStreamInput(LANG_CVC, ss, "foo"));
+  parser->setInput(Input::newStreamInput(Language::LANG_CVC, ss, "foo"));
   checkEmptyInput(parser.get());
 }
 
@@ -131,9 +130,9 @@ TEST_F(TestParseBlackParserBuilder, true_stream_input)
 {
   std::stringstream ss("TRUE", std::ios_base::in);
   std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get())
-                                     .withInputLanguage(LANG_CVC)
+                                     .withInputLanguage(Language::LANG_CVC)
                                      .build());
-  parser->setInput(Input::newStreamInput(LANG_CVC, ss, "foo"));
+  parser->setInput(Input::newStreamInput(Language::LANG_CVC, ss, "foo"));
   checkTrueInput(parser.get());
 }
 
diff --git a/test/unit/printer/smt2_printer_black.cpp b/test/unit/printer/smt2_printer_black.cpp
index 6b778989a..3d9c3ca2c 100644
--- a/test/unit/printer/smt2_printer_black.cpp
+++ b/test/unit/printer/smt2_printer_black.cpp
@@ -36,8 +36,8 @@ class TestPrinterBlackSmt2 : public TestSmt
   void checkToString(TNode n, const std::string& expected)
   {
     std::stringstream ss;
-    ss << Node::setdepth(-1)
-       << Node::setlanguage(language::output::LANG_SMTLIB_V2_6) << n;
+    ss << Node::setdepth(-1) << Node::setlanguage(Language::LANG_SMTLIB_V2_6)
+       << n;
     ASSERT_EQ(ss.str(), expected);
   }
 };
diff --git a/test/unit/util/boolean_simplification_black.cpp b/test/unit/util/boolean_simplification_black.cpp
index d7447f230..b9b9834e3 100644
--- a/test/unit/util/boolean_simplification_black.cpp
+++ b/test/unit/util/boolean_simplification_black.cpp
@@ -72,7 +72,7 @@ class TestUtilBlackBooleanSimplification : public TestNode
     Assert(BooleanSimplification::DUPLICATE_REMOVAL_THRESHOLD >= 10);
 
     std::cout << expr::ExprSetDepth(-1)
-              << language::SetLanguage(language::output::LANG_CVC);
+              << language::SetLanguage(Language::LANG_CVC);
   }
 
   // assert equality up to commuting children