diff options
author | Gereon Kremer <nafur42@gmail.com> | 2021-08-27 11:23:15 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-08-27 18:23:15 +0000 |
commit | 3183ca6685f6b0dcca538efb72e6840a56479b60 (patch) | |
tree | e6c51d6175d4a56c7849aa4f965ed49b743f0607 /test | |
parent | a698b522d619c800a3401c7294cf1c6c663d7acc (diff) |
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.
Diffstat (limited to 'test')
-rw-r--r-- | test/api/ouroborous.cpp | 8 | ||||
-rw-r--r-- | test/api/smt2_compliance.cpp | 8 | ||||
-rw-r--r-- | test/unit/parser/parser_black.cpp | 49 | ||||
-rw-r--r-- | test/unit/parser/parser_builder_black.cpp | 36 |
4 files changed, 49 insertions, 52 deletions
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()); } |