From: Gereon Kremer <nafur42@gmail.com>
Date: Fri, 27 Aug 2021 18:23:15 +0000 (-0700)
Subject: Handle languages as strings in driver (#7074)
X-Git-Tag: cvc5-1.0.0~1325
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3183ca6685f6b0dcca538efb72e6840a56479b60;p=cvc5.git

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.
---

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index de6f614e1..f68545d00 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -158,32 +158,32 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver)
   }
   const char* filename = filenameStr.c_str();
 
-  if (opts->base.inputLanguage == Language::LANG_AUTO)
+  if (solver->getOption("input-language") == "LANG_AUTO")
   {
     if( inputFromStdin ) {
       // We can't do any fancy detection on stdin
-      opts->base.inputLanguage = Language::LANG_CVC;
+      solver->setOption("input-language", "cvc");
     } else {
       size_t len = filenameStr.size();
       if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
-        opts->base.inputLanguage = Language::LANG_SMTLIB_V2_6;
+        solver->setOption("input-language", "smt2");
       } else if((len >= 2 && !strcmp(".p", filename + len - 2))
                 || (len >= 5 && !strcmp(".tptp", filename + len - 5))) {
-        opts->base.inputLanguage = Language::LANG_TPTP;
+        solver->setOption("input-language", "tptp");
       } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
                 || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
-        opts->base.inputLanguage = Language::LANG_CVC;
+        solver->setOption("input-language", "cvc");
       } else if((len >= 3 && !strcmp(".sy", filename + len - 3))
                 || (len >= 3 && !strcmp(".sl", filename + len - 3))) {
         // version 2 sygus is the default
-        opts->base.inputLanguage = Language::LANG_SYGUS_V2;
+        solver->setOption("input-language", "sygus2");
       }
     }
   }
 
-  if (opts->base.outputLanguage == Language::LANG_AUTO)
+  if (solver->getOption("output-language") == "LANG_AUTO")
   {
-    opts->base.outputLanguage = opts->base.inputLanguage;
+    solver->setOption("output-language", solver->getOption("input-language"));
   }
   pExecutor->storeOptionsAsOriginal();
 
@@ -197,11 +197,6 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver)
     WarningChannel.setStream(&cvc5::null_os);
   }
 
-  // important even for muzzled builds (to get result output right)
-  (*opts->base.out)
-      << language::SetLanguage(opts->base.outputLanguage);
-
-
   int returnValue = 0;
   {
     // notify SmtEngine that we are starting to parse
@@ -259,19 +254,19 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver)
         pExecutor->doCommand(cmd);
       }
 
-      ParserBuilder parserBuilder(pExecutor->getSolver(),
-                                  pExecutor->getSymbolManager(),
-                                  *opts);
+      ParserBuilder parserBuilder(
+          pExecutor->getSolver(), pExecutor->getSymbolManager(), true);
       std::unique_ptr<Parser> parser(parserBuilder.build());
       if( inputFromStdin ) {
         parser->setInput(Input::newStreamInput(
-            opts->base.inputLanguage, cin, filename));
+            solver->getOption("input-language"), cin, filename));
       }
       else
       {
-        parser->setInput(Input::newFileInput(opts->base.inputLanguage,
-                                             filename,
-                                             opts->parser.memoryMap));
+        parser->setInput(
+            Input::newFileInput(solver->getOption("input-language"),
+                                filename,
+                                solver->getOption("mmap") == "true"));
       }
 
       bool interrupted = false;
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 14a507aee..8cb40cfdb 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -91,17 +91,17 @@ static set<string> s_declarations;
 #endif /* HAVE_LIBEDITLINE */
 
 InteractiveShell::InteractiveShell(api::Solver* solver, SymbolManager* sm)
-    : d_options(solver->getOptions()),
-      d_in(*d_options.base.in),
-      d_out(*d_options.base.out),
+    : d_solver(solver),
+      d_in(*solver->getOptions().base.in),
+      d_out(*solver->getOptions().base.out),
       d_quit(false)
 {
-  ParserBuilder parserBuilder(solver, sm, d_options);
+  ParserBuilder parserBuilder(solver, sm, true);
   /* Create parser with bogus input. */
   d_parser = parserBuilder.build();
-  if (d_options.parser.forceLogicStringWasSetByUser)
+  if (d_solver->getOptions().parser.forceLogicStringWasSetByUser)
   {
-    LogicInfo tmp(d_options.parser.forceLogicString);
+    LogicInfo tmp(d_solver->getOption("force-logic"));
     d_parser->forceLogic(tmp.getLogicString());
   }
 
@@ -116,34 +116,30 @@ InteractiveShell::InteractiveShell(api::Solver* solver, SymbolManager* sm)
 #endif /* EDITLINE_COMPENTRY_FUNC_RETURNS_CHARP */
     ::using_history();
 
-    Language lang = d_options.base.inputLanguage;
-    switch(lang) {
-      case Language::LANG_CVC:
-        d_historyFilename = string(getenv("HOME")) + "/.cvc5_history";
-        commandsBegin = cvc_commands;
-        commandsEnd =
-            cvc_commands + sizeof(cvc_commands) / sizeof(*cvc_commands);
-        break;
-      case Language::LANG_TPTP:
-        d_historyFilename = string(getenv("HOME")) + "/.cvc5_history_tptp";
-        commandsBegin = tptp_commands;
-        commandsEnd =
-            tptp_commands + sizeof(tptp_commands) / sizeof(*tptp_commands);
-        break;
-      default:
-        if (language::isLangSmt2(lang))
-        {
-          d_historyFilename = string(getenv("HOME")) + "/.cvc5_history_smtlib2";
-          commandsBegin = smt2_commands;
-          commandsEnd =
-              smt2_commands + sizeof(smt2_commands) / sizeof(*smt2_commands);
-        }
-        else
-        {
-          std::stringstream ss;
-          ss << "internal error: unhandled language " << lang;
-          throw Exception(ss.str());
-        }
+    std::string lang = solver->getOption("input-language");
+    if (lang == "LANG_CVC")
+    {
+      d_historyFilename = string(getenv("HOME")) + "/.cvc5_history";
+      commandsBegin = cvc_commands;
+      commandsEnd = cvc_commands + sizeof(cvc_commands) / sizeof(*cvc_commands);
+    }
+    else if (lang == "LANG_TPTP")
+    {
+      d_historyFilename = string(getenv("HOME")) + "/.cvc5_history_tptp";
+      commandsBegin = tptp_commands;
+      commandsEnd =
+          tptp_commands + sizeof(tptp_commands) / sizeof(*tptp_commands);
+    }
+    else if (lang == "LANG_SMTLIB_V2_6")
+    {
+      d_historyFilename = string(getenv("HOME")) + "/.cvc5_history_smtlib2";
+      commandsBegin = smt2_commands;
+      commandsEnd =
+          smt2_commands + sizeof(smt2_commands) / sizeof(*smt2_commands);
+    }
+    else
+    {
+      throw Exception("internal error: unhandled language " + lang);
     }
     d_usingEditline = true;
     int err = ::read_history(d_historyFilename.c_str());
@@ -313,7 +309,7 @@ restart:
   }
 
   d_parser->setInput(Input::newStringInput(
-      d_options.base.inputLanguage, input, INPUT_FILENAME));
+      d_solver->getOption("input-language"), input, INPUT_FILENAME));
 
   /* There may be more than one command in the input. Build up a
      sequence. */
@@ -364,7 +360,7 @@ restart:
   }
   catch (ParserException& pe)
   {
-    if (language::isLangSmt2(d_options.base.outputLanguage))
+    if (d_solver->getOption("output-language") == "LANG_SMTLIB_V2_6")
     {
       d_out << "(error \"" << pe << "\")" << endl;
     }
diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h
index cf5f22b51..d4736470f 100644
--- a/src/main/interactive_shell.h
+++ b/src/main/interactive_shell.h
@@ -40,7 +40,7 @@ class SymbolManager;
 
 class InteractiveShell
 {
-  const Options& d_options;
+  api::Solver* d_solver;
   std::istream& d_in;
   std::ostream& d_out;
   parser::Parser* d_parser;
diff --git a/src/options/base_options.toml b/src/options/base_options.toml
index a049348a6..bf0134200 100644
--- a/src/options/base_options.toml
+++ b/src/options/base_options.toml
@@ -49,6 +49,7 @@ public = true
   type       = "Language"
   default    = "Language::LANG_AUTO"
   handler    = "stringToLanguage"
+  predicates = ["applyOutputLanguage"]
   includes   = ["options/language.h"]
   help       = "force output language (default is \"auto\"; see --output-lang help)"
 
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 149aa767b..1b6cff519 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -34,6 +34,7 @@
 #include "options/didyoumean.h"
 #include "options/language.h"
 #include "options/option_exception.h"
+#include "options/set_language.h"
 #include "options/smt_options.h"
 #include "options/theory_options.h"
 #include "smt/command.h"
@@ -513,6 +514,13 @@ Language OptionsHandler::stringToLanguage(const std::string& option,
   Unreachable();
 }
 
+void OptionsHandler::applyOutputLanguage(const std::string& option,
+                                         const std::string& flag,
+                                         Language lang)
+{
+  d_options->base.out << language::SetLanguage(lang);
+}
+
 void OptionsHandler::languageIsNotAST(const std::string& option,
                                       const std::string& flag,
                                       Language lang)
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 3b8eb724f..0d625c5da 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -153,6 +153,10 @@ public:
   Language stringToLanguage(const std::string& option,
                             const std::string& flag,
                             const std::string& optarg);
+  /** Apply the output language to the default output stream */
+  void applyOutputLanguage(const std::string& option,
+                           const std::string& flag,
+                           Language lang);
   /** Check that lang is not LANG_AST (which is not allowed as input language). */
   void languageIsNotAST(const std::string& option,
                         const std::string& flag,
diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index 6d5cbb5cc..c190fe7f0 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -185,35 +185,30 @@ AntlrInputStream::newStringInputStream(const std::string& input,
   return new AntlrInputStream(name, inputStream, false, input_duplicate, NULL);
 }
 
-AntlrInput* AntlrInput::newInput(Language lang, AntlrInputStream& inputStream)
+AntlrInput* AntlrInput::newInput(const std::string& lang,
+                                 AntlrInputStream& inputStream)
 {
-  AntlrInput* input;
-
-  switch(lang) {
-    case Language::LANG_CVC:
-    {
-      input = new CvcInput(inputStream);
-      break;
-    }
-
-    case Language::LANG_SYGUS_V2: input = new SygusInput(inputStream); break;
-
-    case Language::LANG_TPTP: input = new TptpInput(inputStream); break;
-
-    default:
-      if (language::isLangSmt2(lang))
-      {
-        input = new Smt2Input(inputStream);
-      }
-      else
-      {
-        std::stringstream ss;
-        ss << "unable to detect input file format, try --lang ";
-        throw InputStreamException(ss.str());
-      }
+  if (lang == "LANG_CVC")
+  {
+    return new CvcInput(inputStream);
+  }
+  else if (lang == "LANG_SYGUS_V2")
+  {
+    return new SygusInput(inputStream);
+  }
+  else if (lang == "LANG_TPTP")
+  {
+    return new TptpInput(inputStream);
+  }
+  else if (lang == "LANG_SMTLIB_V2_6")
+  {
+    return new Smt2Input(inputStream);
+  }
+  else
+  {
+    throw InputStreamException(
+        "unable to detect input file format, try --lang ");
   }
-
-  return input;
 }
 
 AntlrInput::AntlrInput(AntlrInputStream& inputStream, unsigned int lookahead) :
diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h
index 52650f561..7799d279d 100644
--- a/src/parser/antlr_input.h
+++ b/src/parser/antlr_input.h
@@ -155,7 +155,8 @@ public:
    * @param inputStream the input stream
    *
    * */
-  static AntlrInput* newInput(Language lang, AntlrInputStream& inputStream);
+  static AntlrInput* newInput(const std::string& lang,
+                              AntlrInputStream& inputStream);
 
   /** Retrieve the text associated with a token. */
   static std::string tokenText(pANTLR3_COMMON_TOKEN token);
diff --git a/src/parser/input.cpp b/src/parser/input.cpp
index 9d4c65eae..c8c005b36 100644
--- a/src/parser/input.cpp
+++ b/src/parser/input.cpp
@@ -51,7 +51,7 @@ InputStream *Input::getInputStream() {
   return d_inputStream;
 }
 
-Input* Input::newFileInput(Language lang,
+Input* Input::newFileInput(const std::string& lang,
                            const std::string& filename,
                            bool useMmap)
 {
@@ -60,7 +60,7 @@ Input* Input::newFileInput(Language lang,
   return AntlrInput::newInput(lang, *inputStream);
 }
 
-Input* Input::newStreamInput(Language lang,
+Input* Input::newStreamInput(const std::string& lang,
                              std::istream& input,
                              const std::string& name)
 {
@@ -69,7 +69,7 @@ Input* Input::newStreamInput(Language lang,
   return AntlrInput::newInput(lang, *inputStream);
 }
 
-Input* Input::newStringInput(Language lang,
+Input* Input::newStringInput(const std::string& lang,
                              const std::string& str,
                              const std::string& name)
 {
diff --git a/src/parser/input.h b/src/parser/input.h
index 94bbe1d8a..7d7254339 100644
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -100,7 +100,7 @@ class CVC5_EXPORT Input
     * @param filename the input filename
     * @param useMmap true if the parser should use memory-mapped I/O (default: false)
     */
-  static Input* newFileInput(Language lang,
+  static Input* newFileInput(const std::string& lang,
                              const std::string& filename,
                              bool useMmap = false);
 
@@ -113,7 +113,7 @@ class CVC5_EXPORT Input
    * (false, the default, means that the entire Input might be read
    * before being lexed and parsed)
    */
-  static Input* newStreamInput(Language lang,
+  static Input* newStreamInput(const std::string& lang,
                                std::istream& input,
                                const std::string& name);
 
@@ -123,7 +123,7 @@ class CVC5_EXPORT Input
    * @param input the input string
    * @param name the name of the stream, for use in error messages
    */
-  static Input* newStringInput(Language lang,
+  static Input* newStringInput(const std::string& lang,
                                const std::string& input,
                                const std::string& name);
 
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index 1ac03fb83..665836402 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -33,24 +33,21 @@
 namespace cvc5 {
 namespace parser {
 
-ParserBuilder::ParserBuilder(api::Solver* solver, SymbolManager* sm)
-    : d_solver(solver), d_symman(sm)
-{
-  init(solver, sm);
-}
-
 ParserBuilder::ParserBuilder(api::Solver* solver,
                              SymbolManager* sm,
-                             const Options& options)
+                             bool useOptions)
     : d_solver(solver), d_symman(sm)
 {
   init(solver, sm);
-  withOptions(options);
+  if (useOptions)
+  {
+    withOptions(solver->getOptions());
+  }
 }
 
 void ParserBuilder::init(api::Solver* solver, SymbolManager* sm)
 {
-  d_lang = Language::LANG_AUTO;
+  d_lang = "LANG_AUTO";
   d_solver = solver;
   d_symman = sm;
   d_checksEnabled = true;
@@ -64,24 +61,17 @@ void ParserBuilder::init(api::Solver* solver, SymbolManager* sm)
 Parser* ParserBuilder::build()
 {
   Parser* parser = NULL;
-  switch (d_lang)
+  if (d_lang == "LANG_SYGUS_V2" || d_lang == "LANG_SMTLIB_V2_6")
+  {
+    parser = new Smt2(d_solver, d_symman, d_strictMode, d_parseOnly);
+  }
+  else if (d_lang == "LANG_TPTP")
+  {
+    parser = new Tptp(d_solver, d_symman, d_strictMode, d_parseOnly);
+  }
+  else
   {
-    case Language::LANG_SYGUS_V2:
-      parser = new Smt2(d_solver, d_symman, d_strictMode, d_parseOnly);
-      break;
-    case Language::LANG_TPTP:
-      parser = new Tptp(d_solver, d_symman, d_strictMode, d_parseOnly);
-      break;
-    default:
-      if (language::isLangSmt2(d_lang))
-      {
-        parser = new Smt2(d_solver, d_symman, d_strictMode, d_parseOnly);
-      }
-      else
-      {
-        parser = new Cvc(d_solver, d_symman, d_strictMode, d_parseOnly);
-      }
-      break;
+    parser = new Cvc(d_solver, d_symman, d_strictMode, d_parseOnly);
   }
 
   if( d_checksEnabled ) {
@@ -108,7 +98,7 @@ ParserBuilder& ParserBuilder::withChecks(bool flag) {
   return *this;
 }
 
-ParserBuilder& ParserBuilder::withInputLanguage(Language lang)
+ParserBuilder& ParserBuilder::withInputLanguage(const std::string& lang)
 {
   d_lang = lang;
   return *this;
@@ -122,7 +112,7 @@ ParserBuilder& ParserBuilder::withParseOnly(bool flag) {
 ParserBuilder& ParserBuilder::withOptions(const Options& opts)
 {
   ParserBuilder& retval = *this;
-  retval = retval.withInputLanguage(opts.base.inputLanguage)
+  retval = retval.withInputLanguage(d_solver->getOption("input-language"))
                .withChecks(opts.parser.semanticChecks)
                .withStrictMode(opts.parser.strictParsing)
                .withParseOnly(opts.base.parseOnly)
diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h
index 61819a8f9..23a9daae2 100644
--- a/src/parser/parser_builder.h
+++ b/src/parser/parser_builder.h
@@ -45,7 +45,7 @@ class Parser;
 class CVC5_EXPORT ParserBuilder
 {
   /** The input language */
-  Language d_lang;
+  std::string d_lang;
 
   /** The API Solver object. */
   api::Solver* d_solver;
@@ -76,11 +76,7 @@ class CVC5_EXPORT ParserBuilder
 
  public:
   /** Create a parser builder using the given Solver and filename. */
-  ParserBuilder(api::Solver* solver, SymbolManager* sm);
-
-  ParserBuilder(api::Solver* solver,
-                SymbolManager* sm,
-                const Options& options);
+  ParserBuilder(api::Solver* solver, SymbolManager* sm, bool useOptions);
 
   /** Build the parser, using the current settings. */
   Parser* build();
@@ -93,7 +89,7 @@ class CVC5_EXPORT ParserBuilder
    *
    * (Default: LANG_AUTO)
    */
-  ParserBuilder& withInputLanguage(Language lang);
+  ParserBuilder& withInputLanguage(const std::string& lang);
 
   /**
    * Are we only parsing, or doing something with the resulting
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index fe777fe27..39492a98c 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -334,7 +334,7 @@ api::Term Smt2::getExpressionForNameAndType(const std::string& name,
 
 bool Smt2::getTesterName(api::Term cons, std::string& name)
 {
-  if ((v2_6() || sygus_v2()) && strictModeEnabled())
+  if ((v2_6() || sygus()) && strictModeEnabled())
   {
     // 2.6 or above uses indexed tester symbols, if we are in strict mode,
     // we do not automatically define is-cons for constructor cons.
@@ -711,9 +711,10 @@ api::Grammar* Smt2::mkGrammar(const std::vector<api::Term>& boundVars,
   return d_allocGrammars.back().get();
 }
 
-bool Smt2::sygus() const { return language::isLangSygus(getLanguage()); }
-
-bool Smt2::sygus_v2() const { return getLanguage() == Language::LANG_SYGUS_V2; }
+bool Smt2::sygus() const
+{
+  return d_solver->getOption("input-language") == "LANG_SYGUS_V2";
+}
 
 void Smt2::checkThatLogicIsSet()
 {
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 50b4a4efc..c3f93708d 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -230,12 +230,10 @@ class Smt2 : public Parser
    */
   bool v2_6(bool exact = false) const
   {
-    return language::isLangSmt2(getLanguage());
+    return d_solver->getOption("input-language") == "LANG_SMTLIB_V2_6";
   }
   /** Are we using a sygus language? */
   bool sygus() const;
-  /** Are we using the sygus version 2.0 format? */
-  bool sygus_v2() const;
 
   /**
    * Returns true if the language that we are parsing (SMT-LIB version >=2.5
diff --git a/test/api/ouroborous.cpp b/test/api/ouroborous.cpp
index 92e58085d..06b6e320b 100644
--- a/test/api/ouroborous.cpp
+++ b/test/api/ouroborous.cpp
@@ -96,14 +96,16 @@ std::string parse(std::string instr,
   }
 
   api::Solver solver;
-  Language ilang = input_language == "smt2" ? Language::LANG_SMTLIB_V2_6
-                                            : Language::LANG_CVC;
+  std::string ilang =
+      input_language == "smt2" ? "LANG_SMTLIB_V2_6" : "LANG_CVC";
 
   solver.setOption("input-language", input_language);
   solver.setOption("output-language", output_language);
   SymbolManager symman(&solver);
   std::unique_ptr<Parser> parser(
-      ParserBuilder(&solver, &symman).withInputLanguage(ilang).build());
+      ParserBuilder(&solver, &symman, false)
+          .withInputLanguage(solver.getOption("input-language"))
+          .build());
   parser->setInput(
       Input::newStringInput(ilang, declarations, "internal-buffer"));
   // we don't need to execute the commands, but we DO need to parse them to
diff --git a/test/api/smt2_compliance.cpp b/test/api/smt2_compliance.cpp
index 921d7585f..888f722a7 100644
--- a/test/api/smt2_compliance.cpp
+++ b/test/api/smt2_compliance.cpp
@@ -59,11 +59,9 @@ void testGetInfo(api::Solver* solver, const char* s)
 {
   std::unique_ptr<SymbolManager> symman(new SymbolManager(solver));
 
-  std::unique_ptr<Parser> p(
-      ParserBuilder(solver, symman.get(), solver->getOptions()).build());
-  p->setInput(Input::newStringInput(Language::LANG_SMTLIB_V2_6,
-                                    string("(get-info ") + s + ")",
-                                    "<internal>"));
+  std::unique_ptr<Parser> p(ParserBuilder(solver, symman.get(), true).build());
+  p->setInput(Input::newStringInput(
+      "LANG_SMTLIB_V2_6", string("(get-info ") + s + ")", "<internal>"));
   assert(p != NULL);
   Command* c = p->nextCommand();
   assert(c != NULL);
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());
 }