diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-05-14 16:17:54 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-05-14 23:17:54 +0000 |
commit | f1a65bef2675495f09603901a7166f20221b0449 (patch) | |
tree | a1ee3c1dda6638beddf7e3509a052aa06398793c /test | |
parent | 2769173850f78749a870ed051a894317141594fc (diff) |
Decouple parser creation from input selection (#6533)
This commit decouples the creation of a `Parser` instance from creating
an `Input` and setting the `Input` on the parser. This is a first step
in refactoring the parser infrastructure. A future PR will split the
parser class into three classes: `Parser`, `ParserState`, and
`InputParser`. The `Parser` and `InputParser` classes will be the
public-facing classes. The new `Parser` class will have methods to
create `InputParser`s from files, streams, and strings. `InputParser`s
will have methods to get commands/exprs from a given input. The
`ParserState` class will keep track of the state of the parser and will
be the internal interface for the parsers. The current `Parser` class is
used both publicly and internally, which is messy.
Diffstat (limited to 'test')
-rw-r--r-- | test/api/ouroborous.cpp | 9 | ||||
-rw-r--r-- | test/api/smt2_compliance.cpp | 8 | ||||
-rw-r--r-- | test/unit/parser/parser_black.cpp | 51 | ||||
-rw-r--r-- | test/unit/parser/parser_builder_black.cpp | 59 |
4 files changed, 64 insertions, 63 deletions
diff --git a/test/api/ouroborous.cpp b/test/api/ouroborous.cpp index b51982d59..c226da13b 100644 --- a/test/api/ouroborous.cpp +++ b/test/api/ouroborous.cpp @@ -102,10 +102,10 @@ std::string parse(std::string instr, solver.setOption("input-language", input_language); solver.setOption("output-language", output_language); SymbolManager symman(&solver); - Parser* parser = ParserBuilder(&solver, &symman, "internal-buffer") - .withStringInput(declarations) - .withInputLanguage(ilang) - .build(); + std::unique_ptr<Parser> parser( + ParserBuilder(&solver, &symman).withInputLanguage(ilang).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 // get the declarations while (Command* c = parser->nextCommand()) @@ -117,7 +117,6 @@ std::string parse(std::string instr, api::Term e = parser->nextExpression(); std::string s = e.toString(); assert(parser->nextExpression().isNull()); // next expr should be null - delete parser; return s; } diff --git a/test/api/smt2_compliance.cpp b/test/api/smt2_compliance.cpp index 431bde7d6..04b366cf0 100644 --- a/test/api/smt2_compliance.cpp +++ b/test/api/smt2_compliance.cpp @@ -60,8 +60,11 @@ void testGetInfo(api::Solver* solver, const char* s) { std::unique_ptr<SymbolManager> symman(new SymbolManager(solver)); - ParserBuilder pb(solver, symman.get(), "<internal>", solver->getOptions()); - Parser* p = pb.withStringInput(string("(get-info ") + s + ")").build(); + std::unique_ptr<Parser> p( + ParserBuilder(solver, symman.get(), solver->getOptions()).build()); + p->setInput(Input::newStringInput(language::input::LANG_SMTLIB_V2, + string("(get-info ") + s + ")", + "<internal>")); assert(p != NULL); Command* c = p->nextCommand(); assert(c != NULL); @@ -69,7 +72,6 @@ void testGetInfo(api::Solver* solver, const char* s) stringstream ss; c->invoke(solver, symman.get(), ss); assert(p->nextCommand() == NULL); - delete p; delete c; cout << ss.str() << endl << endl; } diff --git a/test/unit/parser/parser_black.cpp b/test/unit/parser/parser_black.cpp index b6c433663..78a67f6d0 100644 --- a/test/unit/parser/parser_black.cpp +++ b/test/unit/parser/parser_black.cpp @@ -86,11 +86,11 @@ class TestParserBlackParser : public TestInternal void tryGoodInput(const std::string goodInput) { d_symman.reset(new SymbolManager(d_solver.get())); - Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test") - .withStringInput(goodInput) - .withOptions(d_options) - .withInputLanguage(d_lang) - .build(); + std::unique_ptr<Parser> parser(ParserBuilder(d_solver.get(), d_symman.get()) + .withOptions(d_options) + .withInputLanguage(d_lang) + .build()); + parser->setInput(Input::newStringInput(d_lang, goodInput, "test")); ASSERT_FALSE(parser->done()); Command* cmd; while ((cmd = parser->nextCommand()) != NULL) @@ -100,18 +100,17 @@ class TestParserBlackParser : public TestInternal } ASSERT_TRUE(parser->done()); - delete parser; } void tryBadInput(const std::string badInput, bool strictMode = false) { d_symman.reset(new SymbolManager(d_solver.get())); - Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test") - .withStringInput(badInput) - .withOptions(d_options) - .withInputLanguage(d_lang) - .withStrictMode(strictMode) - .build(); + std::unique_ptr<Parser> parser(ParserBuilder(d_solver.get(), d_symman.get()) + .withOptions(d_options) + .withInputLanguage(d_lang) + .withStrictMode(strictMode) + .build()); + parser->setInput(Input::newStringInput(d_lang, badInput, "test")); ASSERT_THROW( { Command* cmd; @@ -123,23 +122,21 @@ class TestParserBlackParser : public TestInternal std::cout << "\nBad input succeeded:\n" << badInput << std::endl; }, ParserException); - delete parser; } void tryGoodExpr(const std::string goodExpr) { d_symman.reset(new SymbolManager(d_solver.get())); - Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test") - .withStringInput(goodExpr) - .withOptions(d_options) - .withInputLanguage(d_lang) - .build(); - + std::unique_ptr<Parser> parser(ParserBuilder(d_solver.get(), d_symman.get()) + .withOptions(d_options) + .withInputLanguage(d_lang) + .build()); + parser->setInput(Input::newStringInput(d_lang, goodExpr, "test")); if (d_lang == LANG_SMTLIB_V2) { /* Use QF_LIA to make multiplication ("*") available */ std::unique_ptr<Command> cmd( - static_cast<Smt2*>(parser)->setLogic("QF_LIA")); + static_cast<Smt2*>(parser.get())->setLogic("QF_LIA")); } ASSERT_FALSE(parser->done()); @@ -150,7 +147,6 @@ class TestParserBlackParser : public TestInternal e = parser->nextExpression(); ASSERT_TRUE(parser->done()); ASSERT_TRUE(e.isNull()); - delete parser; } /** @@ -165,12 +161,12 @@ class TestParserBlackParser : public TestInternal void tryBadExpr(const std::string badExpr, bool strictMode = false) { d_symman.reset(new SymbolManager(d_solver.get())); - Parser* parser = ParserBuilder(d_solver.get(), d_symman.get(), "test") - .withStringInput(badExpr) - .withOptions(d_options) - .withInputLanguage(d_lang) - .withStrictMode(strictMode) - .build(); + std::unique_ptr<Parser> parser(ParserBuilder(d_solver.get(), d_symman.get()) + .withOptions(d_options) + .withInputLanguage(d_lang) + .withStrictMode(strictMode) + .build()); + parser->setInput(Input::newStringInput(d_lang, badExpr, "test")); setupContext(*parser); ASSERT_FALSE(parser->done()); ASSERT_THROW(api::Term e = parser->nextExpression(); @@ -179,7 +175,6 @@ class TestParserBlackParser : public TestInternal << "Input: <<" << badExpr << ">>" << std::endl << "Output: <<" << e << ">>" << std::endl; , ParserException); - delete parser; } Options d_options; diff --git a/test/unit/parser/parser_builder_black.cpp b/test/unit/parser/parser_builder_black.cpp index 4ed036202..fa532f6b6 100644 --- a/test/unit/parser/parser_builder_black.cpp +++ b/test/unit/parser/parser_builder_black.cpp @@ -40,28 +40,19 @@ class TestParseBlackParserBuilder : public TestApi protected: void SetUp() override { d_symman.reset(new SymbolManager(&d_solver)); } - void checkEmptyInput(ParserBuilder& builder) + void checkEmptyInput(Parser* parser) { - Parser* parser = builder.build(); - ASSERT_NE(parser, nullptr); - api::Term e = parser->nextExpression(); ASSERT_TRUE(e.isNull()); - - delete parser; } - void checkTrueInput(ParserBuilder& builder) + void checkTrueInput(Parser* parser) { - Parser* parser = builder.build(); - ASSERT_NE(parser, nullptr); - api::Term e = parser->nextExpression(); ASSERT_EQ(e, d_solver.mkTrue()); e = parser->nextExpression(); ASSERT_TRUE(e.isNull()); - delete parser; } char* mkTemp() @@ -80,8 +71,11 @@ TEST_F(TestParseBlackParserBuilder, empty_file_input) char* filename = mkTemp(); ASSERT_NE(filename, nullptr); - checkEmptyInput(ParserBuilder(&d_solver, d_symman.get(), filename) - .withInputLanguage(LANG_CVC)); + std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get()) + .withInputLanguage(LANG_CVC) + .build()); + parser->setInput(Input::newFileInput(LANG_CVC, filename, false)); + checkEmptyInput(parser.get()); remove(filename); free(filename); @@ -95,8 +89,11 @@ TEST_F(TestParseBlackParserBuilder, simple_file_input) fs << "TRUE" << std::endl; fs.close(); - checkTrueInput(ParserBuilder(&d_solver, d_symman.get(), filename) - .withInputLanguage(LANG_CVC)); + std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get()) + .withInputLanguage(LANG_CVC) + .build()); + parser->setInput(Input::newFileInput(LANG_CVC, filename, false)); + checkTrueInput(parser.get()); remove(filename); free(filename); @@ -104,32 +101,40 @@ TEST_F(TestParseBlackParserBuilder, simple_file_input) TEST_F(TestParseBlackParserBuilder, empty_string_input) { - checkEmptyInput(ParserBuilder(&d_solver, d_symman.get(), "foo") - .withInputLanguage(LANG_CVC) - .withStringInput("")); + std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get()) + .withInputLanguage(LANG_CVC) + .build()); + parser->setInput(Input::newStringInput(LANG_CVC, "", "foo")); + checkEmptyInput(parser.get()); } TEST_F(TestParseBlackParserBuilder, true_string_input) { - checkTrueInput(ParserBuilder(&d_solver, d_symman.get(), "foo") - .withInputLanguage(LANG_CVC) - .withStringInput("TRUE")); + std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get()) + .withInputLanguage(LANG_CVC) + .build()); + parser->setInput(Input::newStringInput(LANG_CVC, "TRUE", "foo")); + checkTrueInput(parser.get()); } TEST_F(TestParseBlackParserBuilder, empty_stream_input) { std::stringstream ss("", std::ios_base::in); - checkEmptyInput(ParserBuilder(&d_solver, d_symman.get(), "foo") - .withInputLanguage(LANG_CVC) - .withStreamInput(ss)); + std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get()) + .withInputLanguage(LANG_CVC) + .build()); + 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); - checkTrueInput(ParserBuilder(&d_solver, d_symman.get(), "foo") - .withInputLanguage(LANG_CVC) - .withStreamInput(ss)); + std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get()) + .withInputLanguage(LANG_CVC) + .build()); + parser->setInput(Input::newStreamInput(LANG_CVC, ss, "foo")); + checkTrueInput(parser.get()); } } // namespace test |