Handle languages as strings in driver (#7074)

This PR moves the first chunk of code in the driver to use the proper options API for the language options. It is now handled as a string.

2 files changed, 41 insertions, 44 deletions

diff --git a/test/unit/parser/parser_black.cpp b/test/unit/parser/parser_black.cpp
index 42b7d41f7..17d4b963e 100644
--- a/test/unit/parser/parser_black.cpp
+++ b/test/unit/parser/parser_black.cpp
@@ -36,7 +36,7 @@ namespace test {
 class TestParserBlackParser : public TestInternal
 {
  protected:
-  TestParserBlackParser(Language lang) : d_lang(lang) {}
+  TestParserBlackParser(const std::string& lang) : d_lang(lang) {}
 
   virtual ~TestParserBlackParser() {}
 
@@ -78,10 +78,10 @@ class TestParserBlackParser : public TestInternal
   void tryGoodInput(const std::string goodInput)
   {
     d_symman.reset(new SymbolManager(d_solver.get()));
-    std::unique_ptr<Parser> parser(ParserBuilder(d_solver.get(), d_symman.get())
-                                       .withOptions(d_solver->getOptions())
-                                       .withInputLanguage(d_lang)
-                                       .build());
+    std::unique_ptr<Parser> parser(
+        ParserBuilder(d_solver.get(), d_symman.get(), true)
+            .withInputLanguage(d_lang)
+            .build());
     parser->setInput(Input::newStringInput(d_lang, goodInput, "test"));
     ASSERT_FALSE(parser->done());
     Command* cmd;
@@ -97,11 +97,11 @@ class TestParserBlackParser : public TestInternal
   void tryBadInput(const std::string badInput, bool strictMode = false)
   {
     d_symman.reset(new SymbolManager(d_solver.get()));
-    std::unique_ptr<Parser> parser(ParserBuilder(d_solver.get(), d_symman.get())
-                                       .withOptions(d_solver->getOptions())
-                                       .withInputLanguage(d_lang)
-                                       .withStrictMode(strictMode)
-                                       .build());
+    std::unique_ptr<Parser> parser(
+        ParserBuilder(d_solver.get(), d_symman.get(), true)
+            .withInputLanguage(d_lang)
+            .withStrictMode(strictMode)
+            .build());
     parser->setInput(Input::newStringInput(d_lang, badInput, "test"));
     ASSERT_THROW(
         {
@@ -119,12 +119,12 @@ class TestParserBlackParser : public TestInternal
   void tryGoodExpr(const std::string goodExpr)
   {
     d_symman.reset(new SymbolManager(d_solver.get()));
-    std::unique_ptr<Parser> parser(ParserBuilder(d_solver.get(), d_symman.get())
-                                       .withOptions(d_solver->getOptions())
-                                       .withInputLanguage(d_lang)
-                                       .build());
+    std::unique_ptr<Parser> parser(
+        ParserBuilder(d_solver.get(), d_symman.get(), true)
+            .withInputLanguage(d_lang)
+            .build());
     parser->setInput(Input::newStringInput(d_lang, goodExpr, "test"));
-    if (d_lang == Language::LANG_SMTLIB_V2_6)
+    if (d_lang == "LANG_SMTLIB_V2_6")
     {
       /* Use QF_LIA to make multiplication ("*") available */
       std::unique_ptr<Command> cmd(
@@ -153,11 +153,11 @@ class TestParserBlackParser : public TestInternal
   void tryBadExpr(const std::string badExpr, bool strictMode = false)
   {
     d_symman.reset(new SymbolManager(d_solver.get()));
-    std::unique_ptr<Parser> parser(ParserBuilder(d_solver.get(), d_symman.get())
-                                       .withOptions(d_solver->getOptions())
-                                       .withInputLanguage(d_lang)
-                                       .withStrictMode(strictMode)
-                                       .build());
+    std::unique_ptr<Parser> parser(
+        ParserBuilder(d_solver.get(), d_symman.get(), true)
+            .withInputLanguage(d_lang)
+            .withStrictMode(strictMode)
+            .build());
     parser->setInput(Input::newStringInput(d_lang, badExpr, "test"));
     setupContext(*parser);
     ASSERT_FALSE(parser->done());
@@ -169,7 +169,7 @@ class TestParserBlackParser : public TestInternal
                  , ParserException);
   }
 
-  Language d_lang;
+  std::string d_lang;
   std::unique_ptr<cvc5::api::Solver> d_solver;
   std::unique_ptr<SymbolManager> d_symman;
 };
@@ -179,7 +179,7 @@ class TestParserBlackParser : public TestInternal
 class TestParserBlackCvCParser : public TestParserBlackParser
 {
  protected:
-  TestParserBlackCvCParser() : TestParserBlackParser(Language::LANG_CVC) {}
+  TestParserBlackCvCParser() : TestParserBlackParser("LANG_CVC") {}
 };
 
 TEST_F(TestParserBlackCvCParser, good_inputs)
@@ -277,10 +277,7 @@ TEST_F(TestParserBlackCvCParser, bad_exprs)
 class TestParserBlackSmt2Parser : public TestParserBlackParser
 {
  protected:
-  TestParserBlackSmt2Parser()
-      : TestParserBlackParser(Language::LANG_SMTLIB_V2_6)
-  {
-  }
+  TestParserBlackSmt2Parser() : TestParserBlackParser("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 b941a4eda..1c493e6a2 100644
--- a/test/unit/parser/parser_builder_black.cpp
+++ b/test/unit/parser/parser_builder_black.cpp
@@ -70,10 +70,10 @@ TEST_F(TestParseBlackParserBuilder, empty_file_input)
   char* filename = mkTemp();
   ASSERT_NE(filename, nullptr);
 
-  std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get())
-                                     .withInputLanguage(Language::LANG_CVC)
+  std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get(), false)
+                                     .withInputLanguage("LANG_CVC")
                                      .build());
-  parser->setInput(Input::newFileInput(Language::LANG_CVC, filename, false));
+  parser->setInput(Input::newFileInput("LANG_CVC", filename, false));
   checkEmptyInput(parser.get());
 
   remove(filename);
@@ -88,10 +88,10 @@ TEST_F(TestParseBlackParserBuilder, simple_file_input)
   fs << "TRUE" << std::endl;
   fs.close();
 
-  std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get())
-                                     .withInputLanguage(Language::LANG_CVC)
+  std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get(), false)
+                                     .withInputLanguage("LANG_CVC")
                                      .build());
-  parser->setInput(Input::newFileInput(Language::LANG_CVC, filename, false));
+  parser->setInput(Input::newFileInput("LANG_CVC", filename, false));
   checkTrueInput(parser.get());
 
   remove(filename);
@@ -100,39 +100,39 @@ TEST_F(TestParseBlackParserBuilder, simple_file_input)
 
 TEST_F(TestParseBlackParserBuilder, empty_string_input)
 {
-  std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get())
-                                     .withInputLanguage(Language::LANG_CVC)
+  std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get(), false)
+                                     .withInputLanguage("LANG_CVC")
                                      .build());
-  parser->setInput(Input::newStringInput(Language::LANG_CVC, "", "foo"));
+  parser->setInput(Input::newStringInput("LANG_CVC", "", "foo"));
   checkEmptyInput(parser.get());
 }
 
 TEST_F(TestParseBlackParserBuilder, true_string_input)
 {
-  std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get())
-                                     .withInputLanguage(Language::LANG_CVC)
+  std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get(), false)
+                                     .withInputLanguage("LANG_CVC")
                                      .build());
-  parser->setInput(Input::newStringInput(Language::LANG_CVC, "TRUE", "foo"));
+  parser->setInput(Input::newStringInput("LANG_CVC", "TRUE", "foo"));
   checkTrueInput(parser.get());
 }
 
 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(Language::LANG_CVC)
+  std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get(), false)
+                                     .withInputLanguage("LANG_CVC")
                                      .build());
-  parser->setInput(Input::newStreamInput(Language::LANG_CVC, ss, "foo"));
+  parser->setInput(Input::newStreamInput("LANG_CVC", ss, "foo"));
   checkEmptyInput(parser.get());
 }
 
 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(Language::LANG_CVC)
+  std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get(), false)
+                                     .withInputLanguage("LANG_CVC")
                                      .build());
-  parser->setInput(Input::newStreamInput(Language::LANG_CVC, ss, "foo"));
+  parser->setInput(Input::newStreamInput("LANG_CVC", ss, "foo"));
   checkTrueInput(parser.get());
 }