From a358ed3b520919acbb72fb9bcd2974ee4165f495 Mon Sep 17 00:00:00 2001 From: "Christopher L. Conway" Date: Wed, 12 May 2010 20:29:24 +0000 Subject: [PATCH] Adding ParserBuilder, reducing visibility of Parser and Input constructors Adding Smt2 subclass of Parser Checking for multiple calls to set-logic in SMT v2 --- src/main/main.cpp | 30 +++---- src/parser/Makefile.am | 2 + src/parser/input.h | 11 +-- src/parser/parser.h | 16 ++-- src/parser/parser_builder.cpp | 141 ++++++++++++++++++++++++++++++++ src/parser/parser_builder.h | 91 +++++++++++++++++++++ src/parser/smt2/Smt2.g | 13 +-- src/parser/smt2/smt2.cpp | 79 ++++++++++-------- src/parser/smt2/smt2.h | 31 ++++--- src/parser/smt2/smt2_input.cpp | 7 -- src/parser/smt2/smt2_input.h | 7 +- test/unit/parser/parser_black.h | 73 ++++++++++------- 12 files changed, 382 insertions(+), 119 deletions(-) create mode 100644 src/parser/parser_builder.cpp create mode 100644 src/parser/parser_builder.h diff --git a/src/main/main.cpp b/src/main/main.cpp index 19e1d0cff..a16db2411 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -22,8 +22,8 @@ #include "cvc4autoconfig.h" #include "main.h" #include "usage.h" -#include "parser/input.h" #include "parser/parser.h" +#include "parser/parser_builder.h" #include "expr/expr_manager.h" #include "smt/smt_engine.h" #include "expr/command.h" @@ -149,29 +149,19 @@ int runCvc4(int argc, char* argv[]) { } } - // Create the parser - Input* input; - /* TODO: Hack ANTLR3 to support input from streams */ -// if(inputFromStdin) { - // parser = Parser::getNewParser(&exprMgr, options.lang, cin, ""); -// } else { - input = Input::newFileInput(options.lang, argv[firstArgIndex], - options.memoryMap); -// } - Parser parser(&exprMgr, input); - - if(!options.semanticChecks || Configuration::isMuzzledBuild()) { - parser.disableChecks(); - } + ParserBuilder parserBuilder(options.lang, argv[firstArgIndex]); - if( options.strictParsing ) { - parser.enableStrictMode(); - } + Parser *parser = + parserBuilder.withExprManager(exprMgr) + .withMmap(options.memoryMap) + .withChecks(options.semanticChecks && !Configuration::isMuzzledBuild() ) + .withStrictMode( options.strictParsing ) + .build(); // Parse and execute commands until we are done Command* cmd; - while((cmd = parser.nextCommand())) { + while((cmd = parser->nextCommand())) { if( !options.parseOnly ) { doCommand(smt, cmd); } @@ -179,7 +169,7 @@ int runCvc4(int argc, char* argv[]) { } // Remove the parser - delete input; + delete parser; switch(lastResult.asSatisfiabilityResult().isSAT()) { diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index 7029c01e5..f95b01b8c 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -48,6 +48,8 @@ libcvc4parser_noinst_la_SOURCES = \ memory_mapped_input_buffer.cpp \ parser.h \ parser.cpp \ + parser_builder.h \ + parser_builder.cpp \ parser_options.h \ parser_exception.h diff --git a/src/parser/input.h b/src/parser/input.h index 114880bb0..ccae2d84b 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -75,6 +75,7 @@ class Parser; */ class CVC4_PUBLIC Input { friend class Parser; // for parseError, parseCommand, parseExpr + friend class ParserBuilder; /** The input stream. */ InputStream *d_inputStream; @@ -85,11 +86,6 @@ class CVC4_PUBLIC Input { Input(const Input& input) { Unimplemented("Copy constructor for Input."); } Input& operator=(const Input& input) { Unimplemented("operator= for Input."); } -public: - - /** Destructor. Frees the token stream and closes the input. */ - virtual ~Input(); - /** Create an input for the given file. * * @param lang the input language @@ -116,6 +112,11 @@ public: static Input* newStringInput(InputLanguage lang, const std::string& input, const std::string& name) throw (InputStreamException); +public: + + /** Destructor. Frees the token stream and closes the input. */ + virtual ~Input(); + protected: /** Create an input. diff --git a/src/parser/parser.h b/src/parser/parser.h index c191d9f39..e6e5a2250 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -95,6 +95,7 @@ inline std::string toString(SymbolType type) { * declarations. */ class CVC4_PUBLIC Parser { + friend class ParserBuilder; /** The expression manager */ ExprManager *d_exprManager; @@ -123,15 +124,20 @@ class CVC4_PUBLIC Parser { /** Lookup a symbol in the given namespace. */ Expr getSymbol(const std::string& var_name, SymbolType type); -public: - /** Create a parser state. +protected: + /** Create a parser state. NOTE: The parser takes "ownership" of the given + * input and will delete it on destruction. * * @param exprManager the expression manager to use when creating expressions * @param input the parser input */ Parser(ExprManager* exprManager, Input* input, bool strictMode = false); - virtual ~Parser() { } +public: + + virtual ~Parser() { + delete d_input; + } /** Get the associated ExprManager. */ inline ExprManager* getExprManager() const { @@ -145,9 +151,9 @@ public: /** Set the declaration scope manager for this input. NOTE: This should only be * called before parsing begins. Otherwise, previous declarations will be lost. */ - inline void setDeclarationScope(DeclarationScope declScope) { +/* inline void setDeclarationScope(DeclarationScope declScope) { d_declScope = declScope; - } + }*/ /** * Check if we are done -- either the end of input has been reached, or some diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp new file mode 100644 index 000000000..b2bb15a6a --- /dev/null +++ b/src/parser/parser_builder.cpp @@ -0,0 +1,141 @@ +/********************* */ +/** parser_builder.cpp + ** Original author: cconway + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** A builder for parsers. + **/ + +#include + +#include "parser_builder.h" +#include "expr/expr_manager.h" +#include "parser/input.h" +#include "parser/parser.h" +#include "parser/smt2/smt2.h" + +namespace CVC4 { + +namespace parser { + +/*class FileInputBuilder : public InputBuilder { + bool d_useMmap; +public: + FileInputBuilder(InputLanguage lang, const std::string& filename, bool useMmap) : + InputBuilder(lang,filename), + d_useMmap(useMmap) { + } + ParserBuilder& useMmap(); + + Input& build() { + return Input::newFileInput(d_lang,d_name,d_useMmap); + } +}; + +class StringInputBuilder : public InputBuilder { + std::string d_input; +public: + StringInputBuilder(InputLanguage lang, const std::string& input, const std::string& name) : + InputBuilder(lang,name), + d_input(input) { + } + + Input& build() { + return Input::newStringInput(lang,input,name); + } +};*/ + +ParserBuilder::ParserBuilder(InputLanguage lang, const std::string& filename) : + d_inputType(FILE_INPUT), + d_lang(lang), + d_filename(filename), + d_exprManager(NULL), + d_checksEnabled(true), + d_strictMode(false), + d_mmap(false) { +} + +Parser *ParserBuilder::build() throw (InputStreamException) { + Input *input; + switch( d_inputType ) { + case FILE_INPUT: + input = Input::newFileInput(d_lang,d_filename,d_mmap); + break; + case STRING_INPUT: + input = Input::newStringInput(d_lang,d_stringInput,d_filename); + break; + } + switch(d_lang) { + case LANG_SMTLIB_V2: + return new Smt2(d_exprManager, input, d_strictMode); + default: + return new Parser(d_exprManager, input, d_strictMode); + } +} + +/*ParserBuilder& ParserBuilder::disableChecks() { + d_checksEnabled = false; + return *this; +} + +ParserBuilder& ParserBuilder::disableMmap() { + d_mmap = false; + return *this; +} + +ParserBuilder& ParserBuilder::disableStrictMode() { + d_strictMode = false; + return *this; +} + +ParserBuilder& ParserBuilder::enableChecks() { + d_checksEnabled = true; + return *this; +} + +ParserBuilder& ParserBuilder::enableMmap() { + d_mmap = true; + return *this; +} + +ParserBuilder& ParserBuilder::enableStrictMode() { + d_strictMode = true; + return *this; +}*/ + +ParserBuilder& ParserBuilder::withChecks(bool flag) { + d_checksEnabled = flag; + return *this; +} + +ParserBuilder& ParserBuilder::withMmap(bool flag) { + d_mmap = flag; + return *this; +} + +ParserBuilder& ParserBuilder::withStrictMode(bool flag) { + d_strictMode = flag; + return *this; +} + +ParserBuilder& ParserBuilder::withExprManager(ExprManager& exprManager) { + d_exprManager = &exprManager; + return *this; +} + +ParserBuilder& ParserBuilder::withStringInput(const std::string& input) { + d_inputType = STRING_INPUT; + d_stringInput = input; + return *this; +} + +} /* namespace parser */ + +} /* namespace CVC4 */ diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h new file mode 100644 index 000000000..d0b8b7bb2 --- /dev/null +++ b/src/parser/parser_builder.h @@ -0,0 +1,91 @@ +/********************* */ +/** parser_builder.h + ** Original author: cconway + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** A builder for parsers. + **/ + +#include "cvc4parser_public.h" + +#ifndef __CVC4__PARSER__PARSER_BUILDER_H_ +#define __CVC4__PARSER__PARSER_BUILDER_H_ + +#include + +#include "parser/input.h" +#include "parser/parser_options.h" + +namespace CVC4 { + +class ExprManager; + +namespace parser { +/* + +class InputBuilder { +protected: + InputLanguage d_lang; + std::string d_name; +public: + InputBuilder(InputLanguage lang, const std::string& name) : + d_lang(lang), + d_name(name) { + } + virtual Input& build() = 0; +}; +*/ + +class Parser; + +class CVC4_PUBLIC ParserBuilder { + enum InputType { + FILE_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 expression manager */ + ExprManager *d_exprManager; + + /** Should semantic checks be enabled during parsing? */ + bool d_checksEnabled; + + /** Should we parse in strict mode? */ + bool d_strictMode; + + /** Should we memory-map a file input? */ + bool d_mmap; + +public: + ParserBuilder(InputLanguage lang, const std::string& filename); + Parser *build() throw (InputStreamException); + ParserBuilder& withChecks(bool flag = true); + ParserBuilder& withMmap(bool flag = true); + ParserBuilder& withStrictMode(bool flag = true); + ParserBuilder& withExprManager(ExprManager& exprManager); + ParserBuilder& withStringInput(const std::string& input); +}; + +} /* namespace parser */ + +} /* namespace CVC4 */ +#endif /* __CVC4__PARSER__PARSER_BUILDER_H_ */ diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index dec052859..105976628 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -52,14 +52,14 @@ options { @lexer::postinclude { #include -#include "parser/parser.h" +#include "parser/smt2/smt2.h" #include "parser/antlr_input.h" using namespace CVC4; using namespace CVC4::parser; #undef PARSER_STATE -#define PARSER_STATE ((Parser*)LEXER->super) +#define PARSER_STATE ((Smt2*)LEXER->super) } @parser::includes { @@ -89,7 +89,7 @@ using namespace CVC4::parser; /* These need to be macros so they can refer to the PARSER macro, which will be defined * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */ #undef PARSER_STATE -#define PARSER_STATE ((Parser*)PARSER->super) +#define PARSER_STATE ((Smt2*)PARSER->super) #undef EXPR_MANAGER #define EXPR_MANAGER PARSER_STATE->getExprManager() #undef MK_EXPR @@ -132,11 +132,14 @@ command returns [CVC4::Command* cmd] SET_LOGIC_TOK SYMBOL { name = AntlrInput::tokenText($SYMBOL); Debug("parser") << "set logic: '" << name << "' " << std::endl; - Smt2::setLogic(*PARSER_STATE,name); + if( PARSER_STATE->strictModeEnabled() && PARSER_STATE->logicIsSet() ) { + PARSER_STATE->parseError("Only one set-logic is allowed."); + } + PARSER_STATE->setLogic(name); $cmd = new SetBenchmarkLogicCommand(name); } | SET_INFO_TOK KEYWORD symbolicExpr[sexpr] { name = AntlrInput::tokenText($KEYWORD); - Smt2::setInfo(*PARSER_STATE,name,sexpr); + PARSER_STATE->setInfo(name,sexpr); cmd = new SetInfoCommand(name,sexpr); } | /* sort declaration */ DECLARE_SORT_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT] n=INTEGER_LITERAL diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 9fd6588bb..d7da84a43 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -39,15 +39,23 @@ Smt2::Logic Smt2::toLogic(const std::string& name) { return logicMap[name]; } -void Smt2::addArithmeticOperators(Parser& parser) { - parser.addOperator(kind::PLUS); - parser.addOperator(kind::MINUS); - parser.addOperator(kind::UMINUS); - parser.addOperator(kind::MULT); - parser.addOperator(kind::LT); - parser.addOperator(kind::LEQ); - parser.addOperator(kind::GT); - parser.addOperator(kind::GEQ); +Smt2::Smt2(ExprManager* exprManager, Input* input, bool strictMode) : + Parser(exprManager,input,strictMode), + d_logicSet(false) { + if( !strictModeEnabled() ) { + addTheory(Smt2::THEORY_CORE); + } +} + +void Smt2::addArithmeticOperators() { + addOperator(kind::PLUS); + addOperator(kind::MINUS); + addOperator(kind::UMINUS); + addOperator(kind::MULT); + addOperator(kind::LT); + addOperator(kind::LEQ); + addOperator(kind::GT); + addOperator(kind::GEQ); } /** @@ -56,34 +64,34 @@ void Smt2::addArithmeticOperators(Parser& parser) { * @param parser the CVC4 Parser object * @param theory the theory to open (e.g., Core, Ints) */ -void Smt2::addTheory(Parser& parser, Theory theory) { +void Smt2::addTheory(Theory theory) { switch(theory) { case THEORY_CORE: - parser.defineType("Bool", parser.getExprManager()->booleanType()); - parser.defineVar("true", parser.getExprManager()->mkConst(true)); - parser.defineVar("false", parser.getExprManager()->mkConst(false)); - parser.addOperator(kind::AND); - parser.addOperator(kind::EQUAL); - parser.addOperator(kind::IFF); - parser.addOperator(kind::IMPLIES); - parser.addOperator(kind::ITE); - parser.addOperator(kind::NOT); - parser.addOperator(kind::OR); - parser.addOperator(kind::XOR); + defineType("Bool", getExprManager()->booleanType()); + defineVar("true", getExprManager()->mkConst(true)); + defineVar("false", getExprManager()->mkConst(false)); + addOperator(kind::AND); + addOperator(kind::EQUAL); + addOperator(kind::IFF); + addOperator(kind::IMPLIES); + addOperator(kind::ITE); + addOperator(kind::NOT); + addOperator(kind::OR); + addOperator(kind::XOR); break; case THEORY_REALS_INTS: - parser.defineType("Real", parser.getExprManager()->realType()); + defineType("Real", getExprManager()->realType()); // falling-through on purpose, to add Ints part of RealsInts case THEORY_INTS: - parser.defineType("Int", parser.getExprManager()->integerType()); - addArithmeticOperators(parser); + defineType("Int", getExprManager()->integerType()); + addArithmeticOperators(); break; case THEORY_REALS: - parser.defineType("Real", parser.getExprManager()->realType()); - addArithmeticOperators(parser); + defineType("Real", getExprManager()->realType()); + addArithmeticOperators(); break; default: @@ -91,23 +99,30 @@ void Smt2::addTheory(Parser& parser, Theory theory) { } } +bool Smt2::logicIsSet() { + return d_logicSet; +} + /** * Sets the logic for the current benchmark. Declares any logic and theory symbols. * * @param parser the CVC4 Parser object * @param name the name of the logic (e.g., QF_UF, AUFLIA) */ -void Smt2::setLogic(Parser& parser, const std::string& name) { +void Smt2::setLogic(const std::string& name) { + d_logicSet = true; + d_logic = toLogic(name); + // Core theory belongs to every logic - addTheory(parser, THEORY_CORE); + addTheory(THEORY_CORE); - switch(toLogic(name)) { + switch(d_logic) { case QF_UF: - parser.addOperator(kind::APPLY_UF); + addOperator(kind::APPLY_UF); break; case QF_LRA: - addTheory(parser, THEORY_REALS); + addTheory(THEORY_REALS); break; default: @@ -115,7 +130,7 @@ void Smt2::setLogic(Parser& parser, const std::string& name) { } } -void Smt2::setInfo(Parser& parser, const std::string& flag, const SExpr& sexpr) { +void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) { // TODO: ??? } diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 715d3199f..0bb3020a3 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -22,6 +22,7 @@ namespace std { using namespace __gnu_cxx; } #include "util/hash.h" +#include "parser/parser.h" namespace CVC4 { @@ -29,9 +30,8 @@ class SExpr; namespace parser { -class Parser; - -class Smt2 { +class Smt2 : public Parser { + friend class ParserBuilder; public: enum Logic { @@ -51,14 +51,25 @@ public: THEORY_REALS_INTS, }; +private: + bool d_logicSet; + Logic d_logic; + +protected: + Smt2(ExprManager* exprManager, Input* input, bool strictMode = false); + +public: /** * Add theory symbols to the parser state. * * @param parser the CVC4 Parser object * @param theory the theory to open (e.g., Core, Ints) */ - static void - addTheory(Parser& parser, Theory theory); + void + addTheory(Theory theory); + + bool + logicIsSet(); /** * Sets the logic for the current benchmark. Declares any logic and theory symbols. @@ -66,17 +77,17 @@ public: * @param parser the CVC4 Parser object * @param name the name of the logic (e.g., QF_UF, AUFLIA) */ - static void - setLogic(Parser& parser, const std::string& name); + void + setLogic(const std::string& name); - static void - setInfo(Parser& parser, const std::string& flag, const SExpr& sexpr); + void + setInfo(const std::string& flag, const SExpr& sexpr); static Logic toLogic(const std::string& name); private: - static void addArithmeticOperators(Parser& parser); + void addArithmeticOperators(); static std::hash_map newLogicMap(); }; }/* CVC4::parser namespace */ diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp index 6d7a04800..5150ba010 100644 --- a/src/parser/smt2/smt2_input.cpp +++ b/src/parser/smt2/smt2_input.cpp @@ -65,12 +65,5 @@ Expr Smt2Input::parseExpr() throw (ParserException) { return d_pSmt2Parser->parseExpr(d_pSmt2Parser); } -void Smt2Input::setParser(Parser& parser) { - super::setParser(parser); - if( !parser.strictModeEnabled() ) { - Smt2::addTheory(parser,Smt2::THEORY_CORE); - } -} - }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h index c003a76ec..962e2a987 100644 --- a/src/parser/smt2/smt2_input.h +++ b/src/parser/smt2/smt2_input.h @@ -32,6 +32,8 @@ class ExprManager; namespace parser { +class Smt2; + class Smt2Input : public AntlrInput { typedef AntlrInput super; @@ -86,11 +88,6 @@ protected: */ Expr parseExpr() throw(ParserException); - /** Set the Parser object for this input. This implementation overrides the super-class - * implementation to add the core theory symbols to the parser state when strict - * mode is disabled. */ - virtual void setParser(Parser& parser); - };/* class Smt2Input */ }/* CVC4::parser namespace */ diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index 49ff24863..6f09820c5 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -19,8 +19,8 @@ #include "expr/expr.h" #include "expr/expr_manager.h" -#include "parser/input.h" #include "parser/parser.h" +#include "parser/parser_builder.h" #include "parser/smt2/smt2.h" #include "expr/command.h" #include "util/output.h" @@ -62,17 +62,20 @@ protected: // Debug.on("parser-extra"); // cerr << "Testing good input: <<" << goodInput << ">>" << endl; // istringstream stream(goodInputs[i]); - Input* input = Input::newStringInput(d_lang, goodInput, "test"); - Parser parser(d_exprManager, input); - TS_ASSERT( !parser.done() ); + ParserBuilder parserBuilder(d_lang,"test"); + Parser *parser = + parserBuilder.withStringInput(goodInput) + .withExprManager(*d_exprManager) + .build(); + TS_ASSERT( !parser->done() ); Command* cmd; - while((cmd = parser.nextCommand()) != NULL) { + while((cmd = parser->nextCommand()) != NULL) { Debug("parser") << "Parsed command: " << (*cmd) << endl; } - TS_ASSERT( parser.done() ); - delete input; - Debug.off("parser"); + TS_ASSERT( parser->done() ); + delete parser; +// Debug.off("parser"); // Debug.off("parser-extra"); } catch (Exception& e) { cout << "\nGood input failed:\n" << goodInput << endl @@ -85,14 +88,18 @@ protected: void tryBadInput(const string badInput, bool strictMode = false) { // cerr << "Testing bad input: '" << badInput << "'\n"; // Debug.on("parser"); - Input* input = Input::newStringInput(d_lang, badInput, "test"); - Parser parser(d_exprManager, input, strictMode); + ParserBuilder parserBuilder(d_lang,"test"); + Parser *parser = + parserBuilder.withStringInput(badInput) + .withExprManager(*d_exprManager) + .withStrictMode(strictMode) + .build(); TS_ASSERT_THROWS - ( while(parser.nextCommand()); + ( while(parser->nextCommand()); cout << "\nBad input succeeded:\n" << badInput << endl;, const ParserException& ); // Debug.off("parser"); - delete input; + delete parser; } void tryGoodExpr(const string goodExpr) { @@ -102,18 +109,20 @@ protected: // cerr << "Testing good expr: '" << goodExpr << "'\n"; // Debug.on("parser"); // istringstream stream(context + goodBooleanExprs[i]); - Input* input = Input::newStringInput(d_lang, - goodExpr, "test"); - Parser parser(d_exprManager, input); - TS_ASSERT( !parser.done() ); - setupContext(parser); - TS_ASSERT( !parser.done() ); - Expr e = parser.nextExpression(); + ParserBuilder parserBuilder(d_lang,"test"); + Parser *parser = + parserBuilder.withStringInput(goodExpr) + .withExprManager(*d_exprManager) + .build(); + TS_ASSERT( !parser->done() ); + setupContext(*parser); + TS_ASSERT( !parser->done() ); + Expr e = parser->nextExpression(); TS_ASSERT( !e.isNull() ); - e = parser.nextExpression(); - TS_ASSERT( parser.done() ); + e = parser->nextExpression(); + TS_ASSERT( parser->done() ); TS_ASSERT( e.isNull() ); - delete input; + delete parser; } catch (Exception& e) { cout << endl << "Good expr failed." << endl @@ -133,18 +142,22 @@ protected: // Debug.on("parser"); // Debug.on("parser-extra"); // cout << "Testing bad expr: '" << badExpr << "'\n"; - Input* input = Input::newStringInput(d_lang, badExpr, "test"); - Parser parser(d_exprManager, input, strictMode); - setupContext(parser); - TS_ASSERT( !parser.done() ); + ParserBuilder parserBuilder(d_lang,"test"); + Parser *parser = + parserBuilder.withStringInput(badExpr) + .withExprManager(*d_exprManager) + .withStrictMode(strictMode) + .build(); + setupContext(*parser); + TS_ASSERT( !parser->done() ); TS_ASSERT_THROWS - ( Expr e = parser.nextExpression(); + ( Expr e = parser->nextExpression(); cout << endl << "Bad expr succeeded." << endl << "Input: <<" << badExpr << ">>" << endl << "Output: <<" << e << ">>" << endl;, const ParserException& ); - delete input; + delete parser; // Debug.off("parser"); } @@ -266,8 +279,8 @@ class Smt2ParserTest : public CxxTest::TestSuite, public ParserBlack { public: Smt2ParserTest() : ParserBlack(LANG_SMTLIB_V2) { } - void setupContext(Parser& parser) { - Smt2::addTheory(parser,Smt2::THEORY_CORE); + void setupContext(Smt2& parser) { + parser.addTheory(Smt2::THEORY_CORE); super::setupContext(parser); } -- 2.30.2