diff options
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/parser/parser_black.cpp | 49 | ||||
-rw-r--r-- | test/unit/parser/parser_builder_black.cpp | 36 |
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()); } |