From 3183ca6685f6b0dcca538efb72e6840a56479b60 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 27 Aug 2021 11:23:15 -0700 Subject: [PATCH] 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. --- src/main/driver_unified.cpp | 35 +++++------- src/main/interactive_shell.cpp | 68 +++++++++++------------ src/main/interactive_shell.h | 2 +- src/options/base_options.toml | 1 + src/options/options_handler.cpp | 8 +++ src/options/options_handler.h | 4 ++ src/parser/antlr_input.cpp | 49 ++++++++-------- src/parser/antlr_input.h | 3 +- src/parser/input.cpp | 6 +- src/parser/input.h | 6 +- src/parser/parser_builder.cpp | 46 ++++++--------- src/parser/parser_builder.h | 10 +--- src/parser/smt2/smt2.cpp | 9 +-- src/parser/smt2/smt2.h | 4 +- test/api/ouroborous.cpp | 8 ++- test/api/smt2_compliance.cpp | 8 +-- test/unit/parser/parser_black.cpp | 49 ++++++++-------- test/unit/parser/parser_builder_black.cpp | 36 ++++++------ 18 files changed, 167 insertions(+), 185 deletions(-) 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& 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& 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& solver) pExecutor->doCommand(cmd); } - ParserBuilder parserBuilder(pExecutor->getSolver(), - pExecutor->getSymbolManager(), - *opts); + ParserBuilder parserBuilder( + pExecutor->getSolver(), pExecutor->getSymbolManager(), true); std::unique_ptr 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 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& 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( - 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 symman(new SymbolManager(solver)); - std::unique_ptr p( - ParserBuilder(solver, symman.get(), solver->getOptions()).build()); - p->setInput(Input::newStringInput(Language::LANG_SMTLIB_V2_6, - string("(get-info ") + s + ")", - "")); + std::unique_ptr p(ParserBuilder(solver, symman.get(), true).build()); + p->setInput(Input::newStringInput( + "LANG_SMTLIB_V2_6", string("(get-info ") + s + ")", "")); 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(ParserBuilder(d_solver.get(), d_symman.get()) - .withOptions(d_solver->getOptions()) - .withInputLanguage(d_lang) - .build()); + std::unique_ptr 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(ParserBuilder(d_solver.get(), d_symman.get()) - .withOptions(d_solver->getOptions()) - .withInputLanguage(d_lang) - .withStrictMode(strictMode) - .build()); + std::unique_ptr 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(ParserBuilder(d_solver.get(), d_symman.get()) - .withOptions(d_solver->getOptions()) - .withInputLanguage(d_lang) - .build()); + std::unique_ptr 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 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(ParserBuilder(d_solver.get(), d_symman.get()) - .withOptions(d_solver->getOptions()) - .withInputLanguage(d_lang) - .withStrictMode(strictMode) - .build()); + std::unique_ptr 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 d_solver; std::unique_ptr 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(ParserBuilder(&d_solver, d_symman.get()) - .withInputLanguage(Language::LANG_CVC) + std::unique_ptr 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(ParserBuilder(&d_solver, d_symman.get()) - .withInputLanguage(Language::LANG_CVC) + std::unique_ptr 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(ParserBuilder(&d_solver, d_symman.get()) - .withInputLanguage(Language::LANG_CVC) + std::unique_ptr 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(ParserBuilder(&d_solver, d_symman.get()) - .withInputLanguage(Language::LANG_CVC) + std::unique_ptr 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(ParserBuilder(&d_solver, d_symman.get()) - .withInputLanguage(Language::LANG_CVC) + std::unique_ptr 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(ParserBuilder(&d_solver, d_symman.get()) - .withInputLanguage(Language::LANG_CVC) + std::unique_ptr 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()); } -- 2.30.2