diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/api/ouroborous.cpp | 13 | ||||
-rw-r--r-- | test/api/smt2_compliance.cpp | 10 | ||||
-rw-r--r-- | test/unit/parser/parser_black.cpp | 23 | ||||
-rw-r--r-- | test/unit/parser/parser_builder_black.cpp | 35 |
4 files changed, 44 insertions, 37 deletions
diff --git a/test/api/ouroborous.cpp b/test/api/ouroborous.cpp index c226da13b..721f25db8 100644 --- a/test/api/ouroborous.cpp +++ b/test/api/ouroborous.cpp @@ -31,6 +31,7 @@ #include "api/cpp/cvc5.h" #include "options/set_language.h" +#include "parser/input_parser.h" #include "parser/parser.h" #include "parser/parser_builder.h" #include "smt/command.h" @@ -104,19 +105,19 @@ std::string parse(std::string instr, SymbolManager symman(&solver); std::unique_ptr<Parser> parser( ParserBuilder(&solver, &symman).withInputLanguage(ilang).build()); - parser->setInput( - Input::newStringInput(ilang, declarations, "internal-buffer")); + std::unique_ptr<InputParser> inputParser = + parser->parseString("internal-buffer", declarations); // we don't need to execute the commands, but we DO need to parse them to // get the declarations - while (Command* c = parser->nextCommand()) + while (Command* c = inputParser->nextCommand()) { delete c; } assert(parser->done()); // parser should be done - parser->setInput(Input::newStringInput(ilang, instr, "internal-buffer")); - api::Term e = parser->nextExpression(); + inputParser = parser->parseString("internal-buffer", instr); + api::Term e = inputParser->nextExpression(); std::string s = e.toString(); - assert(parser->nextExpression().isNull()); // next expr should be null + assert(inputParser->nextExpression().isNull()); // next expr should be null return s; } diff --git a/test/api/smt2_compliance.cpp b/test/api/smt2_compliance.cpp index 04b366cf0..90e13ef2d 100644 --- a/test/api/smt2_compliance.cpp +++ b/test/api/smt2_compliance.cpp @@ -20,6 +20,7 @@ #include "api/cpp/cvc5.h" #include "options/options.h" #include "options/set_language.h" +#include "parser/input_parser.h" #include "parser/parser.h" #include "parser/parser_builder.h" #include "smt/command.h" @@ -62,16 +63,15 @@ void testGetInfo(api::Solver* solver, const char* s) 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>")); + std::unique_ptr<InputParser> inputParser = + p->parseString("<internal>", string("(get-info ") + s + ")"); assert(p != NULL); - Command* c = p->nextCommand(); + Command* c = inputParser->nextCommand(); assert(c != NULL); cout << c << endl; stringstream ss; c->invoke(solver, symman.get(), ss); - assert(p->nextCommand() == NULL); + assert(inputParser->nextCommand() == NULL); delete c; cout << ss.str() << endl << endl; } diff --git a/test/unit/parser/parser_black.cpp b/test/unit/parser/parser_black.cpp index 78a67f6d0..a0cd0499e 100644 --- a/test/unit/parser/parser_black.cpp +++ b/test/unit/parser/parser_black.cpp @@ -21,6 +21,7 @@ #include "options/base_options.h" #include "options/language.h" #include "options/options.h" +#include "parser/input_parser.h" #include "parser/parser.h" #include "parser/parser_builder.h" #include "parser/smt2/smt2.h" @@ -90,10 +91,11 @@ class TestParserBlackParser : public TestInternal .withOptions(d_options) .withInputLanguage(d_lang) .build()); - parser->setInput(Input::newStringInput(d_lang, goodInput, "test")); + std::unique_ptr<InputParser> inputParser = + parser->parseString("test", goodInput); ASSERT_FALSE(parser->done()); Command* cmd; - while ((cmd = parser->nextCommand()) != NULL) + while ((cmd = inputParser->nextCommand()) != NULL) { Debug("parser") << "Parsed command: " << (*cmd) << std::endl; delete cmd; @@ -110,11 +112,12 @@ class TestParserBlackParser : public TestInternal .withInputLanguage(d_lang) .withStrictMode(strictMode) .build()); - parser->setInput(Input::newStringInput(d_lang, badInput, "test")); + std::unique_ptr<InputParser> inputParser = + parser->parseString("test", badInput); ASSERT_THROW( { Command* cmd; - while ((cmd = parser->nextCommand()) != NULL) + while ((cmd = inputParser->nextCommand()) != NULL) { Debug("parser") << "Parsed command: " << (*cmd) << std::endl; delete cmd; @@ -131,7 +134,8 @@ class TestParserBlackParser : public TestInternal .withOptions(d_options) .withInputLanguage(d_lang) .build()); - parser->setInput(Input::newStringInput(d_lang, goodExpr, "test")); + std::unique_ptr<InputParser> inputParser = + parser->parseString("test", goodExpr); if (d_lang == LANG_SMTLIB_V2) { /* Use QF_LIA to make multiplication ("*") available */ @@ -142,9 +146,9 @@ class TestParserBlackParser : public TestInternal ASSERT_FALSE(parser->done()); setupContext(*parser); ASSERT_FALSE(parser->done()); - api::Term e = parser->nextExpression(); + api::Term e = inputParser->nextExpression(); ASSERT_FALSE(e.isNull()); - e = parser->nextExpression(); + e = inputParser->nextExpression(); ASSERT_TRUE(parser->done()); ASSERT_TRUE(e.isNull()); } @@ -166,10 +170,11 @@ class TestParserBlackParser : public TestInternal .withInputLanguage(d_lang) .withStrictMode(strictMode) .build()); - parser->setInput(Input::newStringInput(d_lang, badExpr, "test")); + std::unique_ptr<InputParser> inputParser = + parser->parseString("test", badExpr); setupContext(*parser); ASSERT_FALSE(parser->done()); - ASSERT_THROW(api::Term e = parser->nextExpression(); + ASSERT_THROW(api::Term e = inputParser->nextExpression(); std::cout << std::endl << "Bad expr succeeded." << std::endl << "Input: <<" << badExpr << ">>" << std::endl diff --git a/test/unit/parser/parser_builder_black.cpp b/test/unit/parser/parser_builder_black.cpp index fa532f6b6..f8d29efbe 100644 --- a/test/unit/parser/parser_builder_black.cpp +++ b/test/unit/parser/parser_builder_black.cpp @@ -24,6 +24,7 @@ #include "api/cpp/cvc5.h" #include "expr/symbol_manager.h" #include "options/language.h" +#include "parser/input_parser.h" #include "parser/parser.h" #include "parser/parser_builder.h" #include "test_api.h" @@ -40,18 +41,18 @@ class TestParseBlackParserBuilder : public TestApi protected: void SetUp() override { d_symman.reset(new SymbolManager(&d_solver)); } - void checkEmptyInput(Parser* parser) + void checkEmptyInput(InputParser* inputParser) { - api::Term e = parser->nextExpression(); + api::Term e = inputParser->nextExpression(); ASSERT_TRUE(e.isNull()); } - void checkTrueInput(Parser* parser) + void checkTrueInput(InputParser* inputParser) { - api::Term e = parser->nextExpression(); + api::Term e = inputParser->nextExpression(); ASSERT_EQ(e, d_solver.mkTrue()); - e = parser->nextExpression(); + e = inputParser->nextExpression(); ASSERT_TRUE(e.isNull()); } @@ -74,8 +75,8 @@ TEST_F(TestParseBlackParserBuilder, empty_file_input) 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()); + std::unique_ptr<InputParser> inputParser = parser->parseFile(filename, false); + checkEmptyInput(inputParser.get()); remove(filename); free(filename); @@ -92,8 +93,8 @@ TEST_F(TestParseBlackParserBuilder, simple_file_input) 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()); + std::unique_ptr<InputParser> inputParser = parser->parseFile(filename, false); + checkTrueInput(inputParser.get()); remove(filename); free(filename); @@ -104,8 +105,8 @@ TEST_F(TestParseBlackParserBuilder, empty_string_input) 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()); + std::unique_ptr<InputParser> inputParser = parser->parseString("foo", ""); + checkEmptyInput(inputParser.get()); } TEST_F(TestParseBlackParserBuilder, true_string_input) @@ -113,8 +114,8 @@ TEST_F(TestParseBlackParserBuilder, true_string_input) 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()); + std::unique_ptr<InputParser> inputParser = parser->parseString("foo", "TRUE"); + checkTrueInput(inputParser.get()); } TEST_F(TestParseBlackParserBuilder, empty_stream_input) @@ -123,8 +124,8 @@ TEST_F(TestParseBlackParserBuilder, empty_stream_input) 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()); + std::unique_ptr<InputParser> inputParser = parser->parseStream("foo", ss); + checkEmptyInput(inputParser.get()); } TEST_F(TestParseBlackParserBuilder, true_stream_input) @@ -133,8 +134,8 @@ TEST_F(TestParseBlackParserBuilder, true_stream_input) 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()); + std::unique_ptr<InputParser> inputParser = parser->parseStream("foo", ss); + checkTrueInput(inputParser.get()); } } // namespace test |