From f1a65bef2675495f09603901a7166f20221b0449 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 14 May 2021 16:17:54 -0700 Subject: [PATCH] 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. --- src/main/driver_unified.cpp | 24 ++++--- src/main/interactive_shell.cpp | 4 +- src/parser/cvc/cvc.h | 3 +- src/parser/parser.cpp | 8 +-- src/parser/parser.h | 11 ++-- src/parser/parser_builder.cpp | 79 +++-------------------- src/parser/parser_builder.h | 58 +---------------- src/parser/smt2/smt2.cpp | 3 +- src/parser/smt2/smt2.h | 1 - src/parser/tptp/tptp.cpp | 5 +- src/parser/tptp/tptp.h | 1 - test/api/ouroborous.cpp | 9 ++- test/api/smt2_compliance.cpp | 8 ++- test/unit/parser/parser_black.cpp | 51 +++++++-------- test/unit/parser/parser_builder_black.cpp | 59 +++++++++-------- 15 files changed, 103 insertions(+), 221 deletions(-) diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index f27bf03f0..a26ee3b73 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -259,16 +259,20 @@ int runCvc5(int argc, char* argv[], Options& opts) ParserBuilder parserBuilder(pExecutor->getSolver(), pExecutor->getSymbolManager(), - filename, opts); - + std::unique_ptr parser(parserBuilder.build()); if( inputFromStdin ) { - parserBuilder.withStreamInput(cin); + parser->setInput( + Input::newStreamInput(opts.getInputLanguage(), cin, filename)); + } + else + { + parser->setInput(Input::newFileInput( + opts.getInputLanguage(), filename, opts.getMemoryMap())); } vector< vector > allCommands; allCommands.push_back(vector()); - std::unique_ptr parser(parserBuilder.build()); int needReset = 0; // true if one of the commands was interrupted bool interrupted = false; @@ -411,14 +415,18 @@ int runCvc5(int argc, char* argv[], Options& opts) ParserBuilder parserBuilder(pExecutor->getSolver(), pExecutor->getSymbolManager(), - filename, opts); - + std::unique_ptr parser(parserBuilder.build()); if( inputFromStdin ) { - parserBuilder.withStreamInput(cin); + parser->setInput( + Input::newStreamInput(opts.getInputLanguage(), cin, filename)); + } + else + { + parser->setInput(Input::newFileInput( + opts.getInputLanguage(), filename, opts.getMemoryMap())); } - std::unique_ptr parser(parserBuilder.build()); bool interrupted = false; while (status) { diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index 516f9e621..8ca10799f 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -91,9 +91,9 @@ InteractiveShell::InteractiveShell(api::Solver* solver, SymbolManager* sm) d_out(*d_options.getOutConst()), d_quit(false) { - ParserBuilder parserBuilder(solver, sm, INPUT_FILENAME, d_options); + ParserBuilder parserBuilder(solver, sm, d_options); /* Create parser with bogus input. */ - d_parser = parserBuilder.withStringInput("").build(); + d_parser = parserBuilder.build(); if(d_options.wasSetByUserForceLogicString()) { LogicInfo tmp(d_options.getForceLogicString()); d_parser->forceLogic(tmp.getLogicString()); diff --git a/src/parser/cvc/cvc.h b/src/parser/cvc/cvc.h index e14f1bc7a..e20e041cc 100644 --- a/src/parser/cvc/cvc.h +++ b/src/parser/cvc/cvc.h @@ -38,10 +38,9 @@ class Cvc : public Parser protected: Cvc(api::Solver* solver, SymbolManager* sm, - Input* input, bool strictMode = false, bool parseOnly = false) - : Parser(solver, sm, input, strictMode, parseOnly) + : Parser(solver, sm, strictMode, parseOnly) { } }; diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 31f8517cd..f3a0d5c83 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -39,15 +39,13 @@ namespace parser { Parser::Parser(api::Solver* solver, SymbolManager* sm, - Input* input, bool strictMode, bool parseOnly) - : d_input(input), - d_symman(sm), + : d_symman(sm), d_symtab(sm->getSymbolTable()), d_assertionLevel(0), d_anonymousFunctionCount(0), - d_done(false), + d_done(true), d_checksEnabled(true), d_strictMode(strictMode), d_parseOnly(parseOnly), @@ -56,7 +54,6 @@ Parser::Parser(api::Solver* solver, d_forcedLogic(), d_solver(solver) { - d_input->setParser(*this); } Parser::~Parser() { @@ -66,7 +63,6 @@ Parser::~Parser() { delete command; } d_commandQueue.clear(); - delete d_input; } api::Solver* Parser::getSolver() const { return d_solver; } diff --git a/src/parser/parser.h b/src/parser/parser.h index 42baf98cd..b127221d7 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -19,6 +19,7 @@ #define CVC5__PARSER__PARSER_H #include +#include #include #include @@ -107,7 +108,7 @@ class CVC5_EXPORT Parser private: /** The input that we're parsing. */ - Input* d_input; + std::unique_ptr d_input; /** * Reference to the symbol manager, which manages the symbol table used by @@ -207,7 +208,6 @@ protected: */ Parser(api::Solver* solver, SymbolManager* sm, - Input* input, bool strictMode = false, bool parseOnly = false); @@ -219,17 +219,14 @@ public: api::Solver* getSolver() const; /** Get the associated input. */ - inline Input* getInput() const { - return d_input; - } + Input* getInput() const { return d_input.get(); } /** Get unresolved sorts */ inline std::set& getUnresolvedSorts() { return d_unresolved; } /** Deletes and replaces the current parser input. */ void setInput(Input* input) { - delete d_input; - d_input = input; + d_input.reset(input); d_input->setParser(*this); d_done = false; } diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index 220edb9d5..26a867f95 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -31,38 +31,29 @@ namespace cvc5 { namespace parser { -ParserBuilder::ParserBuilder(api::Solver* solver, - SymbolManager* sm, - const std::string& filename) - : d_filename(filename), d_solver(solver), d_symman(sm) +ParserBuilder::ParserBuilder(api::Solver* solver, SymbolManager* sm) + : d_solver(solver), d_symman(sm) { - init(solver, sm, filename); + init(solver, sm); } ParserBuilder::ParserBuilder(api::Solver* solver, SymbolManager* sm, - const std::string& filename, const Options& options) - : d_filename(filename), d_solver(solver), d_symman(sm) + : d_solver(solver), d_symman(sm) { - init(solver, sm, filename); + init(solver, sm); withOptions(options); } -void ParserBuilder::init(api::Solver* solver, - SymbolManager* sm, - const std::string& filename) +void ParserBuilder::init(api::Solver* solver, SymbolManager* sm) { - d_inputType = FILE_INPUT; d_lang = language::input::LANG_AUTO; - d_filename = filename; - d_streamInput = NULL; d_solver = solver; d_symman = sm; d_checksEnabled = true; d_strictMode = false; d_canIncludeFile = true; - d_mmap = false; d_parseOnly = false; d_logicIsForced = false; d_forcedLogic = ""; @@ -70,39 +61,23 @@ void ParserBuilder::init(api::Solver* solver, Parser* ParserBuilder::build() { - Input* input = NULL; - switch( d_inputType ) { - case FILE_INPUT: - input = Input::newFileInput(d_lang, d_filename, d_mmap); - break; - case STREAM_INPUT: - Assert(d_streamInput != NULL); - input = Input::newStreamInput(d_lang, *d_streamInput, d_filename); - break; - case STRING_INPUT: - input = Input::newStringInput(d_lang, d_stringInput, d_filename); - break; - } - - Assert(input != NULL); - Parser* parser = NULL; switch (d_lang) { case language::input::LANG_SYGUS_V2: - parser = new Smt2(d_solver, d_symman, input, d_strictMode, d_parseOnly); + parser = new Smt2(d_solver, d_symman, d_strictMode, d_parseOnly); break; case language::input::LANG_TPTP: - parser = new Tptp(d_solver, d_symman, input, d_strictMode, d_parseOnly); + parser = new Tptp(d_solver, d_symman, d_strictMode, d_parseOnly); break; default: if (language::isInputLang_smt2(d_lang)) { - parser = new Smt2(d_solver, d_symman, input, d_strictMode, d_parseOnly); + parser = new Smt2(d_solver, d_symman, d_strictMode, d_parseOnly); } else { - parser = new Cvc(d_solver, d_symman, input, d_strictMode, d_parseOnly); + parser = new Cvc(d_solver, d_symman, d_strictMode, d_parseOnly); } break; } @@ -131,32 +106,11 @@ ParserBuilder& ParserBuilder::withChecks(bool flag) { return *this; } -ParserBuilder& ParserBuilder::withSolver(api::Solver* solver) -{ - d_solver = solver; - return *this; -} - -ParserBuilder& ParserBuilder::withFileInput() { - d_inputType = FILE_INPUT; - return *this; -} - -ParserBuilder& ParserBuilder::withFilename(const std::string& filename) { - d_filename = filename; - return *this; -} - ParserBuilder& ParserBuilder::withInputLanguage(InputLanguage lang) { d_lang = lang; return *this; } -ParserBuilder& ParserBuilder::withMmap(bool flag) { - d_mmap = flag; - return *this; -} - ParserBuilder& ParserBuilder::withParseOnly(bool flag) { d_parseOnly = flag; return *this; @@ -166,7 +120,6 @@ ParserBuilder& ParserBuilder::withOptions(const Options& options) { ParserBuilder& retval = *this; retval = retval.withInputLanguage(options.getInputLanguage()) - .withMmap(options.getMemoryMap()) .withChecks(options.getSemanticChecks()) .withStrictMode(options.getStrictParsing()) .withParseOnly(options.getParseOnly()) @@ -194,17 +147,5 @@ ParserBuilder& ParserBuilder::withForcedLogic(const std::string& logic) { return *this; } -ParserBuilder& ParserBuilder::withStreamInput(std::istream& input) { - d_inputType = STREAM_INPUT; - d_streamInput = &input; - return *this; -} - -ParserBuilder& ParserBuilder::withStringInput(const std::string& input) { - d_inputType = STRING_INPUT; - d_stringInput = input; - return *this; -} - } // namespace parser } // namespace cvc5 diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h index b43da3548..992ca408a 100644 --- a/src/parser/parser_builder.h +++ b/src/parser/parser_builder.h @@ -44,27 +44,9 @@ class Parser; */ class CVC5_EXPORT ParserBuilder { - enum InputType { - FILE_INPUT, - STREAM_INPUT, - STRING_INPUT - }; - - /** The input type. */ - InputType d_inputType; - /** The input language */ InputLanguage d_lang; - /** The file name (may not exist) */ - std::string d_filename; - - /** The string input, if any. */ - std::string d_stringInput; - - /** The stream input, if any. */ - std::istream* d_streamInput; - /** The API Solver object. */ api::Solver* d_solver; @@ -80,9 +62,6 @@ class CVC5_EXPORT ParserBuilder /** Should we allow include-file commands? */ bool d_canIncludeFile; - /** Should we memory-map a file input? */ - bool d_mmap; - /** Are we parsing only? */ bool d_parseOnly; @@ -93,19 +72,14 @@ class CVC5_EXPORT ParserBuilder std::string d_forcedLogic; /** Initialize this parser builder */ - void init(api::Solver* solver, - SymbolManager* sm, - const std::string& filename); + void init(api::Solver* solver, SymbolManager* sm); public: /** Create a parser builder using the given Solver and filename. */ - ParserBuilder(api::Solver* solver, - SymbolManager* sm, - const std::string& filename); + ParserBuilder(api::Solver* solver, SymbolManager* sm); ParserBuilder(api::Solver* solver, SymbolManager* sm, - const std::string& filename, const Options& options); /** Build the parser, using the current settings. */ @@ -114,20 +88,6 @@ class CVC5_EXPORT ParserBuilder /** Should semantic checks be enabled in the parser? (Default: yes) */ ParserBuilder& withChecks(bool flag = true); - /** Set the Solver to use with the parser. */ - ParserBuilder& withSolver(api::Solver* solver); - - /** Set the parser to read a file for its input. (Default) */ - ParserBuilder& withFileInput(); - - /** - * Set the filename for use by the parser. If file input is used, - * this file will be opened and read by the parser. Otherwise, the - * filename string (possibly a non-existent path) will only be used - * in error messages. - */ - ParserBuilder& withFilename(const std::string& filename); - /** * Set the input language to be used by the parser. * @@ -135,14 +95,6 @@ class CVC5_EXPORT ParserBuilder */ ParserBuilder& withInputLanguage(InputLanguage lang); - /** - * Should the parser memory-map its input? This is only relevant if - * the parser will have a file input. - * - * (Default: no) - */ - ParserBuilder& withMmap(bool flag = true); - /** * Are we only parsing, or doing something with the resulting * commands and expressions? This setting affects whether the @@ -173,12 +125,6 @@ class CVC5_EXPORT ParserBuilder */ ParserBuilder& withIncludeFile(bool flag = true); - /** Set the parser to use the given stream for its input. */ - ParserBuilder& withStreamInput(std::istream& input); - - /** Set the parser to use the given string for its input. */ - ParserBuilder& withStringInput(const std::string& input); - /** Set the parser to use the given logic string. */ ParserBuilder& withForcedLogic(const std::string& logic); }; /* class ParserBuilder */ diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 2f19d16f0..a91c713d6 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -31,10 +31,9 @@ namespace parser { Smt2::Smt2(api::Solver* solver, SymbolManager* sm, - Input* input, bool strictMode, bool parseOnly) - : Parser(solver, sm, input, strictMode, parseOnly), + : Parser(solver, sm, strictMode, parseOnly), d_logicSet(false), d_seenSetLogic(false) { diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index e28ef955c..2dd4bf663 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -66,7 +66,6 @@ class Smt2 : public Parser protected: Smt2(api::Solver* solver, SymbolManager* sm, - Input* input, bool strictMode = false, bool parseOnly = false); diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index 01b4c1165..156f2e1e6 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -34,12 +34,9 @@ namespace parser { Tptp::Tptp(api::Solver* solver, SymbolManager* sm, - Input* input, bool strictMode, bool parseOnly) - : Parser(solver, sm, input, strictMode, parseOnly), - d_cnf(false), - d_fof(false) + : Parser(solver, sm, strictMode, parseOnly), d_cnf(false), d_fof(false) { addTheory(Tptp::THEORY_CORE); diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h index 0be74c79d..964c0bdfb 100644 --- a/src/parser/tptp/tptp.h +++ b/src/parser/tptp/tptp.h @@ -90,7 +90,6 @@ class Tptp : public Parser { protected: Tptp(api::Solver* solver, SymbolManager* sm, - Input* input, bool strictMode = false, bool parseOnly = false); 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( + 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 symman(new SymbolManager(solver)); - ParserBuilder pb(solver, symman.get(), "", solver->getOptions()); - Parser* p = pb.withStringInput(string("(get-info ") + s + ")").build(); + std::unique_ptr p( + ParserBuilder(solver, symman.get(), solver->getOptions()).build()); + p->setInput(Input::newStringInput(language::input::LANG_SMTLIB_V2, + string("(get-info ") + s + ")", + "")); 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(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(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(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 cmd( - static_cast(parser)->setLogic("QF_LIA")); + static_cast(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(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(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(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(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(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(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(ParserBuilder(&d_solver, d_symman.get()) + .withInputLanguage(LANG_CVC) + .build()); + parser->setInput(Input::newStreamInput(LANG_CVC, ss, "foo")); + checkTrueInput(parser.get()); } } // namespace test -- 2.30.2