From a72c7a26fda2b9c268912e618fd7d71164e4800a Mon Sep 17 00:00:00 2001 From: "Christopher L. Conway" Date: Wed, 28 Apr 2010 18:34:11 +0000 Subject: [PATCH] Refactoring Input/Parser code to support external manipulation of the parser state. --- src/main/main.cpp | 10 +- src/parser/Makefile.am | 11 +- src/parser/antlr_input.cpp | 163 ----------- src/parser/antlr_input.h | 138 ---------- src/parser/cvc/Cvc.g | 48 ++-- src/parser/cvc/cvc_input.cpp | 24 +- src/parser/cvc/cvc_input.h | 19 +- src/parser/input.cpp | 253 +++++++++++++----- src/parser/input.h | 233 ++++++++++------ ...lr_input_imports.cpp => input_imports.cpp} | 18 +- src/parser/{parser_state.cpp => parser.cpp} | 92 +++++-- src/parser/{parser_state.h => parser.h} | 39 ++- src/parser/smt/Smt.g | 26 +- src/parser/smt/smt_input.cpp | 28 +- src/parser/smt/smt_input.h | 19 +- src/parser/symbol_table.h | 105 -------- test/unit/Makefile.am | 4 +- .../parser/{parser_white.h => parser_black.h} | 75 +++--- 18 files changed, 567 insertions(+), 738 deletions(-) delete mode 100644 src/parser/antlr_input.cpp delete mode 100644 src/parser/antlr_input.h rename src/parser/{antlr_input_imports.cpp => input_imports.cpp} (95%) rename src/parser/{parser_state.cpp => parser.cpp} (67%) rename src/parser/{parser_state.h => parser.h} (89%) delete mode 100644 src/parser/symbol_table.h rename test/unit/parser/{parser_white.h => parser_black.h} (83%) diff --git a/src/main/main.cpp b/src/main/main.cpp index 819f7695e..bdf4f882b 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -23,6 +23,7 @@ #include "main.h" #include "usage.h" #include "parser/input.h" +#include "parser/parser.h" #include "expr/expr_manager.h" #include "smt/smt_engine.h" #include "expr/command.h" @@ -152,17 +153,18 @@ int runCvc4(int argc, char* argv[]) { // if(inputFromStdin) { // parser = Parser::getNewParser(&exprMgr, options.lang, cin, ""); // } else { - input = Input::newFileInput(&exprMgr, options.lang, argv[firstArgIndex], - options.memoryMap); + input = Input::newFileInput(options.lang, argv[firstArgIndex], + options.memoryMap); // } + Parser parser(&exprMgr, input); if(!options.semanticChecks) { - input->disableChecks(); + parser.disableChecks(); } // Parse and execute commands until we are done Command* cmd; - while((cmd = input->parseNextCommand())) { + while((cmd = parser.nextCommand())) { if( !options.parseOnly ) { doCommand(smt, cmd); } diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index 276266757..1464eeac0 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -34,20 +34,17 @@ libcvc4parser_noinst_la_LIBADD = \ libcvc4parser_la_SOURCES = libcvc4parser_noinst_la_SOURCES = \ - antlr_input.h \ - antlr_input.cpp \ - antlr_input_imports.cpp \ bounded_token_buffer.h \ bounded_token_buffer.cpp \ bounded_token_factory.h \ bounded_token_factory.cpp \ input.h \ input.cpp \ + input_imports.cpp \ memory_mapped_input_buffer.h \ memory_mapped_input_buffer.cpp \ + parser.h \ + parser.cpp \ parser_options.h \ - parser_exception.h \ - parser_state.h \ - parser_state.cpp \ - symbol_table.h + parser_exception.h diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp deleted file mode 100644 index 47420a015..000000000 --- a/src/parser/antlr_input.cpp +++ /dev/null @@ -1,163 +0,0 @@ -/********************* */ -/** antlr_input.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 super-class for ANTLR-generated input language parsers - **/ - -#include -#include - -#include "antlr_input.h" -#include "bounded_token_buffer.h" -#include "bounded_token_factory.h" -#include "memory_mapped_input_buffer.h" -#include "parser_exception.h" -#include "parser_state.h" - -#include "util/output.h" -#include "util/Assert.h" -#include "expr/command.h" -#include "expr/type.h" - -using namespace std; -using namespace CVC4; -using namespace CVC4::parser; -using namespace CVC4::kind; - -namespace CVC4 { -namespace parser { - -AntlrInput::AntlrInput(ExprManager* exprManager, const std::string& filename, unsigned int lookahead, bool useMmap) : - Input(exprManager, filename), - d_lookahead(lookahead), - d_lexer(NULL), - d_parser(NULL), - d_tokenStream(NULL) { - - if( useMmap ) { - d_input = MemoryMappedInputBufferNew(filename); - } else { - d_input = antlr3AsciiFileStreamNew((pANTLR3_UINT8) filename.c_str()); - } - if( d_input == NULL ) { - throw ParserException("Couldn't open file: " + filename); - } -} - -/* -AntlrParser::AntlrParser(ExprManager* exprManager, std::istream& input, const std::string& name, unsigned int lookahead) - Parser(exprManager,name), - d_lookahead(lookahead) { - -} -*/ - -AntlrInput::AntlrInput(ExprManager* exprManager, const std::string& input, const std::string& name, unsigned int lookahead) : - Input(exprManager,name), - d_lookahead(lookahead), - d_lexer(NULL), - d_parser(NULL), - d_tokenStream(NULL) { - char* inputStr = strdup(input.c_str()); - char* nameStr = strdup(name.c_str()); - if( inputStr==NULL || nameStr==NULL ) { - throw ParserException("Couldn't initialize string input: '" + input + "'"); - } - d_input = antlr3NewAsciiStringInPlaceStream((pANTLR3_UINT8)inputStr,input.size(),(pANTLR3_UINT8)nameStr); - if( d_input == NULL ) { - throw ParserException("Couldn't create input stream for string: '" + input + "'"); - } -} - -AntlrInput::~AntlrInput() { - d_tokenStream->free(d_tokenStream); - d_input->close(d_input); -} - -pANTLR3_INPUT_STREAM AntlrInput::getInputStream() { - return d_input; -} - -pANTLR3_COMMON_TOKEN_STREAM AntlrInput::getTokenStream() { - return d_tokenStream; -} - -void AntlrInput::lexerError(pANTLR3_BASE_RECOGNIZER recognizer) { - pANTLR3_LEXER lexer = (pANTLR3_LEXER)(recognizer->super); - AlwaysAssert(lexer!=NULL); - ParserState *parserState = (ParserState*)(lexer->super); - AlwaysAssert(parserState!=NULL); - - // Call the error display routine - parserState->parseError("Error finding next token."); -} - -void AntlrInput::parseError(const std::string& message) - throw (ParserException) { - Debug("parser") << "Throwing exception: " - << getParserState()->getFilename() << ":" - << d_lexer->getLine(d_lexer) << "." - << d_lexer->getCharPositionInLine(d_lexer) << ": " - << message << endl; - throw ParserException(message, getParserState()->getFilename(), - d_lexer->getLine(d_lexer), - d_lexer->getCharPositionInLine(d_lexer)); -} - - -void AntlrInput::setLexer(pANTLR3_LEXER pLexer) { - d_lexer = pLexer; - - pANTLR3_TOKEN_FACTORY pTokenFactory = d_lexer->rec->state->tokFactory; - if( pTokenFactory != NULL ) { - pTokenFactory->close(pTokenFactory); - } - - /* 2*lookahead should be sufficient, but we give ourselves some breathing room. */ - pTokenFactory = BoundedTokenFactoryNew(d_input, 2*d_lookahead); - if( pTokenFactory == NULL ) { - throw ParserException("Couldn't create token factory."); - } - d_lexer->rec->state->tokFactory = pTokenFactory; - - pBOUNDED_TOKEN_BUFFER buffer = BoundedTokenBufferSourceNew(d_lookahead, d_lexer->rec->state->tokSource); - if( buffer == NULL ) { - throw ParserException("Couldn't create token buffer."); - } - - d_tokenStream = buffer->commonTstream; - - // ANTLR isn't using super, AFAICT. - d_lexer->super = getParserState(); - // Override default lexer error reporting - d_lexer->rec->reportError = &lexerError; -} - -void AntlrInput::setParser(pANTLR3_PARSER pParser) { - d_parser = pParser; - // ANTLR isn't using super, AFAICT. - // We could also use @parser::context to add a field to the generated parser, but then - // it would have to be declared separately in every input's grammar and we'd have to - // pass it in as an address anyway. - d_parser->super = getParserState(); -// d_parser->rec->match = &match; - d_parser->rec->reportError = &reportError; - /* Don't try to recover from a parse error. */ - // [chris 4/5/2010] Not clear on why this cast is necessary, but I get an error if I remove it. - d_parser->rec->recoverFromMismatchedToken = - (void* (*)(ANTLR3_BASE_RECOGNIZER_struct*, ANTLR3_UINT32, ANTLR3_BITSET_LIST_struct*)) - d_parser->rec->mismatch; -} - - -}/* CVC4::parser namespace */ -}/* CVC4 namespace */ diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h deleted file mode 100644 index a36853d7b..000000000 --- a/src/parser/antlr_input.h +++ /dev/null @@ -1,138 +0,0 @@ -/********************* */ -/** antlr_input.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. - ** - ** Base for ANTLR parser classes. - **/ - -#include "cvc4parser_private.h" - -#ifndef __CVC4__PARSER__ANTLR_PARSER_H -#define __CVC4__PARSER__ANTLR_PARSER_H - -#include -#include -#include -#include - -#include "expr/expr.h" -#include "expr/expr_manager.h" -#include "parser/input.h" -#include "parser/symbol_table.h" -#include "util/Assert.h" - -namespace CVC4 { - -class Command; -class Type; -class FunctionType; - -namespace parser { - -/** - * Wrapper for an ANTLR parser that includes convenience methods to set up input and token streams. - */ -class AntlrInput : public Input { - /** The token lookahead used to lex and parse the input. This should usually be equal to - * K for an LL(k) grammar. */ - unsigned int d_lookahead; - - /** The ANTLR3 lexer associated with this input. This will be NULL initially. It - * must be set by a call to setLexer, preferably in the subclass constructor. */ - pANTLR3_LEXER d_lexer; - - /** The ANTLR3 parser associated with this input. This will be NULL initially. It - * must be set by a call to setParser, preferably in the subclass constructor. - * The super field of d_parser will be set to this and - * reportError will be set to AntlrInput::reportError. */ - pANTLR3_PARSER d_parser; - - /** The ANTLR3 token stream associated with this input. We only need this so we can free it on exit. - * This is set by setLexer. - * NOTE: We assume that we can free it on exit. No sharing! */ - pANTLR3_COMMON_TOKEN_STREAM d_tokenStream; - - /** The ANTLR3 token stream associated with this input. We only need this so we can free it on exit. - * NOTE: We assume that we can free it on exit. No sharing! */ - pANTLR3_INPUT_STREAM d_input; - - /** Turns an ANTLR3 exception into a message for the user and calls parseError. */ - static void reportError(pANTLR3_BASE_RECOGNIZER recognizer); - - /** Builds a message for a lexer error and calls parseError. */ - static void lexerError(pANTLR3_BASE_RECOGNIZER recognizer); - -public: - - /** Create a file input. - * - * @param exprManager the manager to use when building expressions from the input - * @param filename the path of the file to read - * @param lookahead the lookahead needed to parse the input (i.e., k for an LL(k) grammar) - * @param useMmap true if the input should use memory-mapped I/O; otherwise, the - * input will use the standard ANTLR3 I/O implementation. - */ - AntlrInput(ExprManager* exprManager, const std::string& filename, unsigned int lookahead, bool useMmap); - - /** Create an input from an istream. */ - // AntlrParser(ExprManager* em, std::istream& input, const std::string& name, unsigned int lookahead); - - /** Create a string input. - * - * @param exprManager the manager to use when building expressions from the input - * @param input the string to read - * @param name the "filename" to use when reporting errors - * @param lookahead the lookahead needed to parse the input (i.e., k for an LL(k) grammar) - */ - AntlrInput(ExprManager* exprManager, const std::string& input, const std::string& name, unsigned int lookahead); - - /** Destructor. Frees the token stream and closes the input. */ - ~AntlrInput(); - - /** Retrieve the text associated with a token. */ - inline static std::string tokenText(pANTLR3_COMMON_TOKEN token); - -protected: - - /** - * Throws a ParserException with the given message. - */ - void parseError(const std::string& msg) throw (ParserException); - - /** Retrieve the input stream for this parser. */ - pANTLR3_INPUT_STREAM getInputStream(); - /** Retrieve the token stream for this parser. Must not be called before - * setLexer(). */ - pANTLR3_COMMON_TOKEN_STREAM getTokenStream(); - - /** Set the ANTLR lexer for this parser. */ - void setLexer(pANTLR3_LEXER pLexer); - - /** Set the ANTLR parser implementation for this parser. */ - void setParser(pANTLR3_PARSER pParser); -}; - -std::string AntlrInput::tokenText(pANTLR3_COMMON_TOKEN token) { - ANTLR3_MARKER start = token->getStartIndex(token); - ANTLR3_MARKER end = token->getStopIndex(token); - /* start and end are boundary pointers. The text is a string - * of (end-start+1) bytes beginning at start. */ - std::string txt( (const char *)start, end-start+1 ); - Debug("parser-extra") << "tokenText: start=" << start << std::endl - << "end=" << end << std::endl - << "txt='" << txt << "'" << std::endl; - return txt; -} - -}/* CVC4::parser namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__PARSER__ANTLR_PARSER_H */ diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 3f4435966..94a8a6a32 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -48,7 +48,7 @@ options { @parser::includes { #include "expr/command.h" -#include "parser/parser_state.h" +#include "parser/parser.h" namespace CVC4 { class Expr; @@ -59,8 +59,8 @@ namespace CVC4 { #include "expr/expr.h" #include "expr/kind.h" #include "expr/type.h" -#include "parser/antlr_input.h" -#include "parser/parser_state.h" +#include "parser/input.h" +#include "parser/parser.h" #include "util/output.h" #include @@ -70,7 +70,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 ((ParserState*)PARSER->super) +#define PARSER_STATE ((Parser*)PARSER->super) #undef EXPR_MANAGER #define EXPR_MANAGER PARSER_STATE->getExprManager() #undef MK_EXPR @@ -104,7 +104,7 @@ parseCommand returns [CVC4::Command* cmd] command returns [CVC4::Command* cmd = 0] @init { Expr f; - Debug("parser-extra") << "command: " << AntlrInput::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "command: " << Input::tokenText(LT(1)) << std::endl; } : ASSERT_TOK formula[f] SEMICOLON { cmd = new AssertCommand(f); } | QUERY_TOK formula[f] SEMICOLON { cmd = new QueryCommand(f); } @@ -124,7 +124,7 @@ declaration[CVC4::Command*& cmd] @init { std::vector ids; Type t; - Debug("parser-extra") << "declaration: " << AntlrInput::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "declaration: " << Input::tokenText(LT(1)) << std::endl; } : // FIXME: These could be type or function declarations, if that matters. identifierList[ids, CHECK_UNDECLARED, SYM_VARIABLE] COLON declType[t,ids] SEMICOLON @@ -134,7 +134,7 @@ declaration[CVC4::Command*& cmd] /** Match the right-hand side of a declaration. Returns the type. */ declType[CVC4::Type& t, std::vector& idList] @init { - Debug("parser-extra") << "declType: " << AntlrInput::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "declType: " << Input::tokenText(LT(1)) << std::endl; } : /* A sort declaration (e.g., "T : TYPE") */ TYPE_TOK @@ -152,7 +152,7 @@ type[CVC4::Type& t] @init { Type t2; std::vector typeList; - Debug("parser-extra") << "type: " << AntlrInput::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "type: " << Input::tokenText(LT(1)) << std::endl; } : /* Simple type */ baseType[t] @@ -191,7 +191,7 @@ identifier[std::string& id, CVC4::parser::DeclarationCheck check, CVC4::parser::SymbolType type] : IDENTIFIER - { id = AntlrInput::tokenText($IDENTIFIER); + { id = Input::tokenText($IDENTIFIER); PARSER_STATE->checkDeclaration(id, check, type); } ; @@ -202,7 +202,7 @@ identifier[std::string& id, baseType[CVC4::Type& t] @init { std::string id; - Debug("parser-extra") << "base type: " << AntlrInput::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "base type: " << Input::tokenText(LT(1)) << std::endl; } : BOOLEAN_TOK { t = EXPR_MANAGER->booleanType(); } | typeSymbol[t] @@ -214,7 +214,7 @@ baseType[CVC4::Type& t] typeSymbol[CVC4::Type& t] @init { std::string id; - Debug("parser-extra") << "type symbol: " << AntlrInput::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "type symbol: " << Input::tokenText(LT(1)) << std::endl; } : identifier[id,CHECK_DECLARED,SYM_SORT] { t = PARSER_STATE->getSort(id); } @@ -226,7 +226,7 @@ typeSymbol[CVC4::Type& t] */ formula[CVC4::Expr& formula] @init { - Debug("parser-extra") << "formula: " << AntlrInput::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "formula: " << Input::tokenText(LT(1)) << std::endl; } : iffFormula[formula] ; @@ -250,7 +250,7 @@ formulaList[std::vector& formulas] iffFormula[CVC4::Expr& f] @init { Expr e; - Debug("parser-extra") << "<=> formula: " << AntlrInput::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "<=> formula: " << Input::tokenText(LT(1)) << std::endl; } : impliesFormula[f] ( IFF_TOK @@ -265,7 +265,7 @@ iffFormula[CVC4::Expr& f] impliesFormula[CVC4::Expr& f] @init { Expr e; - Debug("parser-extra") << "=> Formula: " << AntlrInput::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "=> Formula: " << Input::tokenText(LT(1)) << std::endl; } : orFormula[f] ( IMPLIES_TOK impliesFormula[e] @@ -279,7 +279,7 @@ impliesFormula[CVC4::Expr& f] orFormula[CVC4::Expr& f] @init { std::vector exprs; - Debug("parser-extra") << "OR Formula: " << AntlrInput::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "OR Formula: " << Input::tokenText(LT(1)) << std::endl; } : xorFormula[f] ( OR_TOK { exprs.push_back(f); } @@ -297,7 +297,7 @@ orFormula[CVC4::Expr& f] xorFormula[CVC4::Expr& f] @init { Expr e; - Debug("parser-extra") << "XOR formula: " << AntlrInput::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "XOR formula: " << Input::tokenText(LT(1)) << std::endl; } : andFormula[f] ( XOR_TOK andFormula[e] @@ -311,7 +311,7 @@ xorFormula[CVC4::Expr& f] andFormula[CVC4::Expr& f] @init { std::vector exprs; - Debug("parser-extra") << "AND Formula: " << AntlrInput::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "AND Formula: " << Input::tokenText(LT(1)) << std::endl; } : notFormula[f] ( AND_TOK { exprs.push_back(f); } @@ -329,7 +329,7 @@ andFormula[CVC4::Expr& f] */ notFormula[CVC4::Expr& f] @init { - Debug("parser-extra") << "NOT formula: " << AntlrInput::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "NOT formula: " << Input::tokenText(LT(1)) << std::endl; } : /* negation */ NOT_TOK notFormula[f] @@ -341,7 +341,7 @@ notFormula[CVC4::Expr& f] predFormula[CVC4::Expr& f] @init { Expr e; - Debug("parser-extra") << "predicate formula: " << AntlrInput::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "predicate formula: " << Input::tokenText(LT(1)) << std::endl; } : term[f] (EQUAL_TOK term[e] @@ -356,10 +356,10 @@ term[CVC4::Expr& f] @init { std::string name; std::vector args; - Debug("parser-extra") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "term: " << Input::tokenText(LT(1)) << std::endl; } : /* function application */ - // { isFunction(AntlrInput::tokenText(LT(1))) }? + // { isFunction(Input::tokenText(LT(1))) }? functionSymbol[f] { args.push_back( f ); } LPAREN formulaList[args] RPAREN @@ -387,7 +387,7 @@ term[CVC4::Expr& f] iteTerm[CVC4::Expr& f] @init { std::vector args; - Debug("parser-extra") << "ite: " << AntlrInput::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "ite: " << Input::tokenText(LT(1)) << std::endl; } : IF_TOK formula[f] { args.push_back(f); } THEN_TOK formula[f] { args.push_back(f); } @@ -402,7 +402,7 @@ iteTerm[CVC4::Expr& f] iteElseTerm[CVC4::Expr& f] @init { std::vector args; - Debug("parser-extra") << "else: " << AntlrInput::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "else: " << Input::tokenText(LT(1)) << std::endl; } : ELSE_TOK formula[f] | ELSEIF_TOK iteCondition = formula[f] { args.push_back(f); } @@ -418,7 +418,7 @@ iteElseTerm[CVC4::Expr& f] */ functionSymbol[CVC4::Expr& f] @init { - Debug("parser-extra") << "function symbol: " << AntlrInput::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "function symbol: " << Input::tokenText(LT(1)) << std::endl; std::string name; } : identifier[name,CHECK_DECLARED,SYM_VARIABLE] diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp index f247a651d..4595c52db 100644 --- a/src/parser/cvc/cvc_input.cpp +++ b/src/parser/cvc/cvc_input.cpp @@ -16,6 +16,7 @@ #include #include "expr/expr_manager.h" +#include "parser/input.h" #include "parser/parser_exception.h" #include "parser/cvc/cvc_input.h" #include "parser/cvc/generated/CvcLexer.h" @@ -25,18 +26,9 @@ namespace CVC4 { namespace parser { /* Use lookahead=2 */ -CvcInput::CvcInput(ExprManager* exprManager, const std::string& filename, bool useMmap) : - AntlrInput(exprManager,filename,2,useMmap) { - init(); -} - -CvcInput::CvcInput(ExprManager* exprManager, const std::string& input, const std::string& name) : - AntlrInput(exprManager,input,name,2) { - init(); -} - -void CvcInput::init() { - pANTLR3_INPUT_STREAM input = getInputStream(); +CvcInput::CvcInput(AntlrInputStream *inputStream) : + Input(inputStream,2) { + pANTLR3_INPUT_STREAM input = inputStream->getAntlr3InputStream(); AlwaysAssert( input != NULL ); d_pCvcLexer = CvcLexerNew(input); @@ -44,7 +36,7 @@ void CvcInput::init() { throw ParserException("Failed to create CVC lexer."); } - setLexer( d_pCvcLexer->pLexer ); + setAntlr3Lexer( d_pCvcLexer->pLexer ); pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream(); AlwaysAssert( tokenStream != NULL ); @@ -54,7 +46,7 @@ void CvcInput::init() { throw ParserException("Failed to create CVC parser."); } - setParser(d_pCvcParser->pParser); + setAntlr3Parser(d_pCvcParser->pParser); } @@ -63,11 +55,11 @@ CvcInput::~CvcInput() { d_pCvcParser->free(d_pCvcParser); } -Command* CvcInput::doParseCommand() throw (ParserException) { +Command* CvcInput::parseCommand() throw (ParserException) { return d_pCvcParser->parseCommand(d_pCvcParser); } -Expr CvcInput::doParseExpr() throw (ParserException) { +Expr CvcInput::parseExpr() throw (ParserException) { return d_pCvcParser->parseExpr(d_pCvcParser); } diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h index 4878d015e..0d264f606 100644 --- a/src/parser/cvc/cvc_input.h +++ b/src/parser/cvc/cvc_input.h @@ -18,7 +18,7 @@ #ifndef __CVC4__PARSER__CVC_INPUT_H #define __CVC4__PARSER__CVC_INPUT_H -#include "parser/antlr_input.h" +#include "parser/input.h" #include "parser/cvc/generated/CvcLexer.h" #include "parser/cvc/generated/CvcParser.h" @@ -32,7 +32,7 @@ class ExprManager; namespace parser { -class CvcInput : public AntlrInput { +class CvcInput : public Input { /** The ANTLR3 CVC lexer for the input. */ pCvcLexer d_pCvcLexer; @@ -41,14 +41,11 @@ class CvcInput : public AntlrInput { public: - /** Create a file input. + /** Create an input. * - * @param exprManager the manager to use when building expressions from the input - * @param filename the path of the file to read - * @param useMmap true if the input should use memory-mapped - * I/O; otherwise, the input will use the standard ANTLR3 I/O implementation. + * @param inputStream the input to parse */ - CvcInput(ExprManager* exprManager, const std::string& filename, bool useMmap); + CvcInput(AntlrInputStream *inputStream); /** Create a string input. * @@ -56,8 +53,10 @@ public: * @param input the string to read * @param name the "filename" to use when reporting errors */ +/* CvcInput(ExprManager* exprManager, const std::string& input, const std::string& name); +*/ /* Destructor. Frees the lexer and the parser. */ ~CvcInput(); @@ -69,14 +68,14 @@ protected: * * @throws ParserException if an error is encountered during parsing. */ - Command* doParseCommand() throw(ParserException); + Command* parseCommand() throw(ParserException); /** Parse an expression from the input. Returns a null Expr * if there is no expression there to parse. * * @throws ParserException if an error is encountered during parsing. */ - Expr doParseExpr() throw(ParserException); + Expr parseExpr() throw(ParserException); private: diff --git a/src/parser/input.cpp b/src/parser/input.cpp index fd1a4cbd6..5df017f16 100644 --- a/src/parser/input.cpp +++ b/src/parser/input.cpp @@ -1,7 +1,7 @@ /********************* */ /** input.cpp - ** Original author: dejan - ** Major contributors: mdeters, cconway + ** 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) @@ -10,113 +10,176 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** Parser implementation. + ** A super-class for ANTLR-generated input language parsers **/ -#include +#include +#include #include "input.h" +#include "bounded_token_buffer.h" +#include "bounded_token_factory.h" +#include "memory_mapped_input_buffer.h" #include "parser_exception.h" -#include "parser_options.h" -#include "parser_state.h" +#include "parser.h" + #include "expr/command.h" -#include "expr/expr.h" +#include "expr/type.h" #include "parser/cvc/cvc_input.h" #include "parser/smt/smt_input.h" #include "util/output.h" #include "util/Assert.h" using namespace std; +using namespace CVC4; +using namespace CVC4::parser; +using namespace CVC4::kind; namespace CVC4 { namespace parser { -bool Input::done() const { - return d_parserState->done(); +AntlrInputStream::AntlrInputStream(std::string name, pANTLR3_INPUT_STREAM input) : + d_name(name), + d_input(input) { } -void Input::disableChecks() { - d_parserState->disableChecks(); +AntlrInputStream::~AntlrInputStream() { + d_input->free(d_input); } -void Input::enableChecks() { - d_parserState->enableChecks(); +pANTLR3_INPUT_STREAM AntlrInputStream::getAntlr3InputStream() const { + return d_input; } -Command* Input::parseNextCommand() throw(ParserException) { - Debug("parser") << "parseNextCommand()" << std::endl; - Command* cmd = NULL; - if(!done()) { - try { - cmd = doParseCommand(); - if(cmd == NULL) { - d_parserState->setDone(); - } - } catch(ParserException& e) { - d_parserState->setDone(); - throw; - } +const std::string AntlrInputStream::getName() const { + return d_name; +} + +AntlrInputStream* AntlrInputStream::newFileInputStream(const std::string& name, bool useMmap) { + if( useMmap ) { + return new AntlrInputStream( name, MemoryMappedInputBufferNew(name) ); + } else { + return new AntlrInputStream( name, antlr3AsciiFileStreamNew((pANTLR3_UINT8) name.c_str()) ); } - Debug("parser") << "parseNextCommand() => " << cmd << std::endl; - return cmd; -} - -Expr Input::parseNextExpression() throw(ParserException) { - Debug("parser") << "parseNextExpression()" << std::endl; - Expr result; - if(!done()) { - try { - result = doParseExpr(); - if(result.isNull()) - d_parserState->setDone(); - } catch(ParserException& e) { - d_parserState->setDone(); - throw; +/* + if( d_inputStream == NULL ) { + throw ParserException("Couldn't open file: " + filename); } +*/ +} + +AntlrInputStream* AntlrInputStream::newStringInputStream(const std::string& input, const std::string& name) /*throw (InputStreamException) */{ + char* inputStr = strdup(input.c_str()); + char* nameStr = strdup(name.c_str()); +/* + if( inputStr==NULL || nameStr==NULL ) { + throw InputStreamException("Couldn't initialize string input: '" + input + "'"); } - Debug("parser") << "parseNextExpression() => " << result << std::endl; - return result; +*/ + return new AntlrInputStream( name, + antlr3NewAsciiStringInPlaceStream( + (pANTLR3_UINT8)inputStr,input.size(), + (pANTLR3_UINT8)nameStr) ); +} + + +Input::Input(AntlrInputStream *inputStream, unsigned int lookahead) : + d_lookahead(lookahead), + d_lexer(NULL), + d_parser(NULL), + d_tokenStream(NULL), + d_inputStream( inputStream ) { + +/* + if( useMmap ) { + d_inputStream = MemoryMappedInputBufferNew(filename); + } else { + d_inputStream = antlr3AsciiFileStreamNew((pANTLR3_UINT8) filename.c_str()); + } +*/ +/* + if( d_inputStream == NULL ) { + throw ParserException("Couldn't open file: " + filename); + } +*/ +} + +/* +AntlrParser::AntlrParser(ExprManager* exprManager, std::istream& input, const std::string& name, unsigned int lookahead) + Parser(exprManager,name), + d_lookahead(lookahead) { + } +*/ + +/* +Input::Input(ExprManager* exprManager, const std::string& input, const std::string& name, unsigned int lookahead) : + Input(exprManager,name), + d_lookahead(lookahead), + d_lexer(NULL), + d_parser(NULL), + d_tokenStream(NULL) { + + char* inputStr = strdup(input.c_str()); + char* nameStr = strdup(name.c_str()); + if( inputStr==NULL || nameStr==NULL ) { + throw ParserException("Couldn't initialize string input: '" + input + "'"); + } + d_inputStream = antlr3NewAsciiStringInPlaceStream((pANTLR3_UINT8)inputStr,input.size(),(pANTLR3_UINT8)nameStr); + if( d_inputStream == NULL ) { + throw ParserException("Couldn't create input stream for string: '" + input + "'"); + } -Input::Input(ExprManager* exprManager, const std::string& filename) { - d_parserState = new ParserState(exprManager,filename,this); } +*/ Input::~Input() { - delete d_parserState; + d_tokenStream->free(d_tokenStream); + delete d_inputStream; } -Input* Input::newFileInput(ExprManager* em, InputLanguage lang, - const std::string& filename, bool useMmap) { +AntlrInputStream *Input::getInputStream() { + return d_inputStream; +} - Input* input = 0; +pANTLR3_COMMON_TOKEN_STREAM Input::getTokenStream() { + return d_tokenStream; +} - switch(lang) { - case LANG_CVC4: - input = new CvcInput(em,filename,useMmap); - break; - case LANG_SMTLIB: - input = new SmtInput(em,filename,useMmap); - break; +void Input::lexerError(pANTLR3_BASE_RECOGNIZER recognizer) { + pANTLR3_LEXER lexer = (pANTLR3_LEXER)(recognizer->super); + AlwaysAssert(lexer!=NULL); + Parser *parser = (Parser*)(lexer->super); + AlwaysAssert(parser!=NULL); + Input *input = parser->getInput(); + AlwaysAssert(input!=NULL); - default: - Unhandled(lang); - } + // Call the error display routine + input->parseError("Error finding next token."); +} - return input; +Input* Input::newFileInput(InputLanguage lang, + const std::string& filename, bool useMmap) { + AntlrInputStream *inputStream = AntlrInputStream::newFileInputStream(filename,useMmap); + return newInput(lang,inputStream); } -Input* Input::newStringInput(ExprManager* em, InputLanguage lang, +Input* Input::newStringInput(InputLanguage lang, const std::string& str, const std::string& name) { - Input* input = 0; + AntlrInputStream *inputStream = AntlrInputStream::newStringInputStream(str,name); + return newInput(lang,inputStream); +} + +Input* Input::newInput(InputLanguage lang, AntlrInputStream *inputStream) { + Input* input; switch(lang) { case LANG_CVC4: { - input = new CvcInput(em,str,name); + input = new CvcInput(inputStream); break; } case LANG_SMTLIB: - input = new SmtInput(em,str,name); + input = new SmtInput(inputStream); break; default: @@ -125,5 +188,67 @@ Input* Input::newStringInput(ExprManager* em, InputLanguage lang, return input; } + +void Input::parseError(const std::string& message) + throw (ParserException) { + Debug("parser") << "Throwing exception: " + << d_inputStream->getName() << ":" + << d_lexer->getLine(d_lexer) << "." + << d_lexer->getCharPositionInLine(d_lexer) << ": " + << message << endl; + throw ParserException(message, d_inputStream->getName(), + d_lexer->getLine(d_lexer), + d_lexer->getCharPositionInLine(d_lexer)); +} + + +void Input::setAntlr3Lexer(pANTLR3_LEXER pLexer) { + d_lexer = pLexer; + + pANTLR3_TOKEN_FACTORY pTokenFactory = d_lexer->rec->state->tokFactory; + if( pTokenFactory != NULL ) { + pTokenFactory->close(pTokenFactory); + } + + /* 2*lookahead should be sufficient, but we give ourselves some breathing room. */ + pTokenFactory = BoundedTokenFactoryNew(d_inputStream->getAntlr3InputStream(), 2*d_lookahead); + if( pTokenFactory == NULL ) { + throw ParserException("Couldn't create token factory."); + } + d_lexer->rec->state->tokFactory = pTokenFactory; + + pBOUNDED_TOKEN_BUFFER buffer = BoundedTokenBufferSourceNew(d_lookahead, d_lexer->rec->state->tokSource); + if( buffer == NULL ) { + throw ParserException("Couldn't create token buffer."); + } + + d_tokenStream = buffer->commonTstream; + + // Override default lexer error reporting + d_lexer->rec->reportError = &lexerError; +} + +void Input::setParser(Parser *parser) { + // ANTLR isn't using super in the lexer or the parser, AFAICT. + // We could also use @lexer/parser::context to add a field to the generated + // objects, but then it would have to be declared separately in every + // language's grammar and we'd have to in the address of the field anyway. + d_lexer->super = parser; + d_parser->super = parser; + +} + +void Input::setAntlr3Parser(pANTLR3_PARSER pParser) { + d_parser = pParser; +// d_parser->rec->match = &match; + d_parser->rec->reportError = &reportError; + /* Don't try to recover from a parse error. */ + // [chris 4/5/2010] Not clear on why this cast is necessary, but I get an error if I remove it. + d_parser->rec->recoverFromMismatchedToken = + (void* (*)(ANTLR3_BASE_RECOGNIZER_struct*, ANTLR3_UINT32, ANTLR3_BITSET_LIST_struct*)) + d_parser->rec->mismatch; +} + + }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/input.h b/src/parser/input.h index a32416305..21c5c4869 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -2,7 +2,7 @@ /** input.h ** Original author: cconway ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** 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 @@ -10,157 +10,228 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** Parser abstraction. + ** Base for ANTLR parser classes. **/ -#include "cvc4parser_public.h" +#include "cvc4parser_private.h" -#ifndef __CVC4__PARSER__INPUT_H -#define __CVC4__PARSER__INPUT_H +#ifndef __CVC4__PARSER__ANTLR_INPUT_H +#define __CVC4__PARSER__ANTLR_INPUT_H +#include +#include #include +#include #include "expr/expr.h" +#include "expr/expr_manager.h" #include "parser/parser_exception.h" #include "parser/parser_options.h" +#include "util/Assert.h" namespace CVC4 { -// Forward declarations -class ExprManager; class Command; class Type; +class FunctionType; namespace parser { -class ParserState; +/** Wrapper around an ANTLR3 input stream. */ +class AntlrInputStream { + std::string d_name; + pANTLR3_INPUT_STREAM d_input; + + AntlrInputStream(std::string name,pANTLR3_INPUT_STREAM input); + /* This is private and throws an exception, because you should never use it. */ + AntlrInputStream(const AntlrInputStream& inputStream) { + Unimplemented("copy constructor for AntlrInputStream"); + } + /* This is private and throws an exception, because you should never use it. */ + AntlrInputStream& operator=(const AntlrInputStream& inputStream) { + Unimplemented("operator= for AntlrInputStream"); + } + +public: + + virtual ~AntlrInputStream(); + + pANTLR3_INPUT_STREAM getAntlr3InputStream() const; + const std::string getName() const; + + /** Create a file input. + * + * @param filename the path of the file to read + * @param useMmap true if the input should use memory-mapped I/O; otherwise, the + * input will use the standard ANTLR3 I/O implementation. + */ + static AntlrInputStream* newFileInputStream(const std::string& name, bool useMmap = false); + + /** Create an input from an istream. */ + // AntlrInputStream newInputStream(std::istream& input, const std::string& name); + + /** Create a string input. + * + * @param input the string to read + * @param name the "filename" to use when reporting errors + */ + static AntlrInputStream* newStringInputStream(const std::string& input, const std::string& name); +}; + +class Parser; /** - * An input to be parsed. This class serves two purposes: to the client, it provides - * the methods parseNextCommand and parseNextExpression to - * extract a stream of Command's and Expr's from the input; - * to the parser, it provides a repository for state data, like the variable symbol - * table, and a variety of convenience functions for updating and checking the state. - * - * An Input should be created using the static factory methods, - * e.g., newFileParser and newStringInput, and - * should be deleted when done. + * An input to be parsed. The static factory methods in this class (e.g., + * newFileInput, newStringInput) create a parser + * for the given input language and attach it to an input source of the + * appropriate type. */ class CVC4_PUBLIC Input { - friend class ParserState; + friend class Parser; // for parseError, parseCommand, parseExpr - /** Whether to de-allocate the input */ - // bool d_deleteInput; + /** The display name of the input (e.g., the filename). */ + std::string d_name; - ParserState *d_parserState; + /** The token lookahead used to lex and parse the input. This should usually be equal to + * K for an LL(k) grammar. */ + unsigned int d_lookahead; -public: + /** The ANTLR3 lexer associated with this input. This will be NULL initially. It + * must be set by a call to setLexer, preferably in the subclass constructor. */ + pANTLR3_LEXER d_lexer; - /** - * Create a new parser for the given file. - * @param exprManager the ExprManager to use - * @param filename the path of the file to parse - */ - Input(ExprManager* exprManager, const std::string& filename); + /** The ANTLR3 parser associated with this input. This will be NULL initially. It + * must be set by a call to setParser, preferably in the subclass constructor. + * The super field of d_parser will be set to this and + * reportError will be set to Input::reportError. */ + pANTLR3_PARSER d_parser; - /** - * Destructor. + /** The ANTLR3 token stream associated with this input. We only need this so we can free it on exit. + * This is set by setLexer. + * NOTE: We assume that we can free it on exit. No sharing! */ + pANTLR3_COMMON_TOKEN_STREAM d_tokenStream; + + /** The ANTLR3 input stream associated with this input. We only need this so we can free it on exit. + * NOTE: We assume that we can free it on exit. No sharing! */ + AntlrInputStream *d_inputStream; + + /** Turns an ANTLR3 exception into a message for the user and calls parseError. */ + static void reportError(pANTLR3_BASE_RECOGNIZER recognizer); + + /** Builds a message for a lexer error and calls parseError. */ + static void lexerError(pANTLR3_BASE_RECOGNIZER recognizer); + + /* Since we own d_tokenStream and it needs to be freed, we need to prevent + * copy construction and assignment. */ + 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 exprManager the ExprManager for creating expressions from the input * @param lang the input language * @param filename the input filename * @param useMmap true if the parser should use memory-mapped I/O (default: false) */ - static Input* newFileInput(ExprManager* exprManager, InputLanguage lang, const std::string& filename, bool useMmap=false); + static Input* newFileInput(InputLanguage lang, const std::string& filename, bool useMmap=false); + + /** Create an input for the given AntlrInputStream. NOTE: the new Input + * will take ownership of the input stream and delete it at destruction time. + * + * @param lang the input language + * @param inputStream the input stream + * + * */ + static Input* newInput(InputLanguage lang, AntlrInputStream *inputStream); /** Create an input for the given stream. * - * @param exprManager the ExprManager for creating expressions from the input * @param lang the input language * @param input the input stream * @param name the name of the stream, for use in error messages */ - //static Parser* getNewParser(ExprManager* exprManager, InputLanguage lang, std::istream& input, const std::string& name); + //static Parser* newStreamInput(InputLanguage lang, std::istream& input, const std::string& name); /** Create an input for the given string * - * @param exprManager the ExprManager for creating expressions from the input * @param lang the input language * @param input the input string * @param name the name of the stream, for use in error messages */ - static Input* newStringInput(ExprManager* exprManager, InputLanguage lang, const std::string& input, const std::string& name); + static Input* newStringInput(InputLanguage lang, const std::string& input, const std::string& name); - /** - * Check if we are done -- either the end of input has been reached, or some - * error has been encountered. - * @return true if parser is done - */ - bool done() const; + /** Retrieve the text associated with a token. */ + inline static std::string tokenText(pANTLR3_COMMON_TOKEN token); - /** Enable semantic checks during parsing. */ - void enableChecks(); - /** - * Disable semantic checks during parsing. Disabling checks may lead - * to crashes on bad inputs. - */ - void disableChecks(); - - /** - * Parse the next command of the input. If EOF is encountered a EmptyCommand - * is returned and done flag is set. +protected: + /** Create an input. This input takes ownership of the given input stream, + * and will delete it at destruction time. * - * @throws ParserException if an error is encountered during parsing. + * @param inputStream the input stream to use + * @param lookahead the lookahead needed to parse the input (i.e., k for + * an LL(k) grammar) */ - Command* parseNextCommand() throw(ParserException); + Input(AntlrInputStream *inputStream, unsigned int lookahead); - /** - * Parse the next expression of the stream. If EOF is encountered a null - * expression is returned and done flag is set. - * @return the parsed expression - * @throws ParserException if an error is encountered during parsing. - */ - Expr parseNextExpression() throw(ParserException); + /** Retrieve the input stream for this parser. */ + AntlrInputStream *getInputStream(); -protected: + /** Retrieve the token stream for this parser. Must not be called before + * setLexer(). */ + pANTLR3_COMMON_TOKEN_STREAM getTokenStream(); - /** Called by parseNextCommand to actually parse a command from + /** Parse a command from * the input by invoking the implementation-specific parsing method. Returns * NULL if there is no command there to parse. * * @throws ParserException if an error is encountered during parsing. */ - virtual Command* doParseCommand() throw(ParserException) = 0; + virtual Command* parseCommand() throw(ParserException) = 0; + + /** + * Throws a ParserException with the given message. + */ + void parseError(const std::string& msg) throw (ParserException); - /** Called by parseNextExpression to actually parse an + /** Parse an * expression from the input by invoking the implementation-specific * parsing method. Returns a null Expr if there is no * expression there to parse. * * @throws ParserException if an error is encountered during parsing. */ - virtual Expr doParseExpr() throw(ParserException) = 0; - - inline ParserState* getParserState() const { - return d_parserState; - } - -private: - - /** Throws a ParserException with the given error message. - * Implementations should fill in the ParserException with - * line number information, etc. */ - virtual void parseError(const std::string& msg) throw (ParserException) = 0; - -}; // end of class Input + virtual Expr parseExpr() throw(ParserException) = 0; + + /** Set the ANTLR3 lexer for this input. */ + void setAntlr3Lexer(pANTLR3_LEXER pLexer); + + /** Set the ANTLR3 parser implementation for this input. */ + void setAntlr3Parser(pANTLR3_PARSER pParser); + + /** Set the Parser object for this input. */ + void setParser(Parser *parser); +}; + +std::string Input::tokenText(pANTLR3_COMMON_TOKEN token) { + ANTLR3_MARKER start = token->getStartIndex(token); + ANTLR3_MARKER end = token->getStopIndex(token); + /* start and end are boundary pointers. The text is a string + * of (end-start+1) bytes beginning at start. */ + std::string txt( (const char *)start, end-start+1 ); + Debug("parser-extra") << "tokenText: start=" << start << std::endl + << "end=" << end << std::endl + << "txt='" << txt << "'" << std::endl; + return txt; +} }/* CVC4::parser namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__PARSER__INPUT_H */ +#endif /* __CVC4__PARSER__ANTLR_INPUT_H */ diff --git a/src/parser/antlr_input_imports.cpp b/src/parser/input_imports.cpp similarity index 95% rename from src/parser/antlr_input_imports.cpp rename to src/parser/input_imports.cpp index 3555ed06b..73d804f95 100644 --- a/src/parser/antlr_input_imports.cpp +++ b/src/parser/input_imports.cpp @@ -35,8 +35,8 @@ #include #include -#include "antlr_input.h" -#include "parser_state.h" +#include "input.h" +#include "parser.h" #include "util/Assert.h" using namespace std; @@ -62,10 +62,10 @@ namespace parser { /* *** CVC4 NOTE *** * This function is has been modified in not-completely-trivial ways from its * libantlr3c implementation to support more informative error messages and to - * invoke the error reporting mechanism of the AntlrInput class instead of the + * invoke the error reporting mechanism of the Input class instead of the * default error printer. */ -void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) { +void Input::reportError(pANTLR3_BASE_RECOGNIZER recognizer) { pANTLR3_EXCEPTION ex = recognizer->state->exception; pANTLR3_UINT8 * tokenNames = recognizer->state->tokenNames; stringstream ss; @@ -230,13 +230,15 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) { } // Now get ready to throw an exception - pANTLR3_PARSER parser = (pANTLR3_PARSER)(recognizer->super); + pANTLR3_PARSER antlr3Parser = (pANTLR3_PARSER)(recognizer->super); + AlwaysAssert(antlr3Parser!=NULL); + Parser *parser = (Parser*)(antlr3Parser->super); AlwaysAssert(parser!=NULL); - ParserState *parserState = (ParserState*)(parser->super); - AlwaysAssert(parserState!=NULL); + Input *input = parser->getInput(); + AlwaysAssert(input!=NULL); // Call the error display routine - parserState->parseError(ss.str()); + input->parseError(ss.str()); } } // namespace parser diff --git a/src/parser/parser_state.cpp b/src/parser/parser.cpp similarity index 67% rename from src/parser/parser_state.cpp rename to src/parser/parser.cpp index 204dd3469..01cc99c3d 100644 --- a/src/parser/parser_state.cpp +++ b/src/parser/parser.cpp @@ -1,5 +1,5 @@ /********************* */ -/** parser_state.cpp +/** parser.cpp ** Original author: cconway ** Major contributors: dejan, mdeters ** Minor contributors (to current version): none @@ -18,14 +18,14 @@ #include #include "input.h" +#include "parser.h" +#include "parser_exception.h" #include "expr/command.h" #include "expr/expr.h" #include "expr/kind.h" #include "expr/type.h" #include "util/output.h" #include "util/Assert.h" -#include "parser/parser_exception.h" -#include "parser/symbol_table.h" #include "parser/cvc/cvc_input.h" #include "parser/smt/smt_input.h" @@ -35,15 +35,15 @@ using namespace CVC4::kind; namespace CVC4 { namespace parser { -ParserState::ParserState(ExprManager* exprManager, const std::string& filename, Input* input) : +Parser::Parser(ExprManager* exprManager, Input* input) : d_exprManager(exprManager), d_input(input), - d_filename(filename), d_done(false), d_checksEnabled(true) { + d_input->setParser(this); } -Expr ParserState::getSymbol(const std::string& name, SymbolType type) { +Expr Parser::getSymbol(const std::string& name, SymbolType type) { Assert( isDeclared(name, type) ); switch( type ) { @@ -57,41 +57,41 @@ Expr ParserState::getSymbol(const std::string& name, SymbolType type) { } -Expr ParserState::getVariable(const std::string& name) { +Expr Parser::getVariable(const std::string& name) { return getSymbol(name, SYM_VARIABLE); } Type -ParserState::getType(const std::string& var_name, +Parser::getType(const std::string& var_name, SymbolType type) { Assert( isDeclared(var_name, type) ); Type t = getSymbol(var_name,type).getType(); return t; } -Type ParserState::getSort(const std::string& name) { +Type Parser::getSort(const std::string& name) { Assert( isDeclared(name, SYM_SORT) ); Type t = d_declScope.lookupType(name); return t; } /* Returns true if name is bound to a boolean variable. */ -bool ParserState::isBoolean(const std::string& name) { +bool Parser::isBoolean(const std::string& name) { return isDeclared(name, SYM_VARIABLE) && getType(name).isBoolean(); } /* Returns true if name is bound to a function. */ -bool ParserState::isFunction(const std::string& name) { +bool Parser::isFunction(const std::string& name) { return isDeclared(name, SYM_VARIABLE) && getType(name).isFunction(); } /* Returns true if name is bound to a function returning boolean. */ -bool ParserState::isPredicate(const std::string& name) { +bool Parser::isPredicate(const std::string& name) { return isDeclared(name, SYM_VARIABLE) && getType(name).isPredicate(); } Expr -ParserState::mkVar(const std::string& name, const Type& type) { +Parser::mkVar(const std::string& name, const Type& type) { Debug("parser") << "mkVar(" << name << "," << type << ")" << std::endl; Expr expr = d_exprManager->mkVar(name, type); defineVar(name,expr); @@ -99,7 +99,7 @@ ParserState::mkVar(const std::string& name, const Type& type) { } const std::vector -ParserState::mkVars(const std::vector names, +Parser::mkVars(const std::vector names, const Type& type) { std::vector vars; for(unsigned i = 0; i < names.size(); ++i) { @@ -109,24 +109,29 @@ ParserState::mkVars(const std::vector names, } void -ParserState::defineVar(const std::string& name, const Expr& val) { +Parser::defineVar(const std::string& name, const Expr& val) { Assert(!isDeclared(name)); d_declScope.bind(name,val); Assert(isDeclared(name)); } +void +Parser::defineType(const std::string& name, const Type& type) { + Assert( !isDeclared(name, SYM_SORT) ); + d_declScope.bindType(name,type); + Assert( isDeclared(name, SYM_SORT) ) ; +} + Type -ParserState::mkSort(const std::string& name) { +Parser::mkSort(const std::string& name) { Debug("parser") << "newSort(" << name << ")" << std::endl; - Assert( !isDeclared(name, SYM_SORT) ) ; Type type = d_exprManager->mkSort(name); - d_declScope.bindType(name, type); - Assert( isDeclared(name, SYM_SORT) ) ; + defineType(name,type); return type; } const std::vector -ParserState::mkSorts(const std::vector& names) { +Parser::mkSorts(const std::vector& names) { std::vector types; for(unsigned i = 0; i < names.size(); ++i) { types.push_back(mkSort(names[i])); @@ -134,7 +139,7 @@ ParserState::mkSorts(const std::vector& names) { return types; } -bool ParserState::isDeclared(const std::string& name, SymbolType type) { +bool Parser::isDeclared(const std::string& name, SymbolType type) { switch(type) { case SYM_VARIABLE: return d_declScope.isBound(name); @@ -145,7 +150,7 @@ bool ParserState::isDeclared(const std::string& name, SymbolType type) { } } -void ParserState::checkDeclaration(const std::string& varName, +void Parser::checkDeclaration(const std::string& varName, DeclarationCheck check, SymbolType type) throw (ParserException) { @@ -174,14 +179,14 @@ void ParserState::checkDeclaration(const std::string& varName, } } -void ParserState::checkFunction(const std::string& name) +void Parser::checkFunction(const std::string& name) throw (ParserException) { if( d_checksEnabled && !isFunction(name) ) { parseError("Expecting function symbol, found '" + name + "'"); } } -void ParserState::checkArity(Kind kind, unsigned int numArgs) +void Parser::checkArity(Kind kind, unsigned int numArgs) throw (ParserException) { if(!d_checksEnabled) { return; @@ -204,14 +209,49 @@ void ParserState::checkArity(Kind kind, unsigned int numArgs) } } -void ParserState::enableChecks() { +void Parser::enableChecks() { d_checksEnabled = true; } -void ParserState::disableChecks() { +void Parser::disableChecks() { d_checksEnabled = false; } +Command* Parser::nextCommand() throw(ParserException) { + Debug("parser") << "nextCommand()" << std::endl; + Command* cmd = NULL; + if(!done()) { + try { + cmd = d_input->parseCommand(); + if(cmd == NULL) { + setDone(); + } + } catch(ParserException& e) { + setDone(); + throw; + } + } + Debug("parser") << "nextCommand() => " << cmd << std::endl; + return cmd; +} + +Expr Parser::nextExpression() throw(ParserException) { + Debug("parser") << "nextExpression()" << std::endl; + Expr result; + if(!done()) { + try { + result = d_input->parseExpr(); + if(result.isNull()) + setDone(); + } catch(ParserException& e) { + setDone(); + throw; + } + } + Debug("parser") << "nextExpression() => " << result << std::endl; + return result; +} + }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/parser_state.h b/src/parser/parser.h similarity index 89% rename from src/parser/parser_state.h rename to src/parser/parser.h index 3ca9c2c0e..a84021c10 100644 --- a/src/parser/parser_state.h +++ b/src/parser/parser.h @@ -1,5 +1,5 @@ /********************* */ -/** parser_state.h +/** parser.h ** Original author: cconway ** Major contributors: none ** Minor contributors (to current version): mdeters @@ -20,13 +20,12 @@ #include +#include "input.h" +#include "parser_exception.h" +#include "parser_options.h" #include "expr/declaration_scope.h" #include "expr/expr.h" #include "expr/kind.h" -#include "parser/input.h" -#include "parser/parser_exception.h" -#include "parser/parser_options.h" -#include "parser/symbol_table.h" #include "util/Assert.h" namespace CVC4 { @@ -89,7 +88,12 @@ inline std::string toString(SymbolType type) { } } -class ParserState { +/** + * This class encapsulates all of the state of a parser, including the + * name of the file, line number and column information, and in-scope + * declarations. + */ +class CVC4_PUBLIC Parser { /** The expression manager */ ExprManager *d_exprManager; @@ -101,7 +105,7 @@ class ParserState { DeclarationScope d_declScope; /** The name of the input file. */ - std::string d_filename; +// std::string d_filename; /** Are we done */ bool d_done; @@ -114,7 +118,14 @@ class ParserState { Expr getSymbol(const std::string& var_name, SymbolType type); public: - ParserState(ExprManager* exprManager, const std::string& filename, Input* input); + /** Create a parser state. + * + * @param exprManager the expression manager to use when creating expressions + * @param input the parser input + */ + Parser(ExprManager* exprManager, Input* input); + + virtual ~Parser() { } /** Get the associated ExprManager. */ inline ExprManager* getExprManager() const { @@ -153,9 +164,11 @@ public: void disableChecks(); /** Get the name of the input file. */ +/* inline const std::string getFilename() { return d_filename; } +*/ /** * Sets the logic for the current benchmark. Declares any logic symbols. @@ -228,8 +241,9 @@ public: /** Create a new variable definition (e.g., from a let binding). */ void defineVar(const std::string& name, const Expr& val); - /** Remove a variable definition (e.g., from a let binding). */ - void undefineVar(const std::string& name); + + /** Create a new type definition. */ + void defineType(const std::string& name, const Type& type); /** * Creates a new sort with the given name. @@ -251,13 +265,16 @@ public: /** Is the symbol bound to a predicate? */ bool isPredicate(const std::string& name); + Command* nextCommand() throw(ParserException); + Expr nextExpression() throw(ParserException); + inline void parseError(const std::string& msg) throw (ParserException) { d_input->parseError(msg); } inline void pushScope() { d_declScope.pushScope(); } inline void popScope() { d_declScope.popScope(); } -}; // class ParserState +}; // class Parser } // namespace parser diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index 4539a6d43..cf22c5290 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -50,7 +50,7 @@ options { @parser::includes { #include "expr/command.h" -#include "parser/parser_state.h" +#include "parser/parser.h" namespace CVC4 { class Expr; @@ -61,8 +61,8 @@ namespace CVC4 { #include "expr/expr.h" #include "expr/kind.h" #include "expr/type.h" -#include "parser/antlr_input.h" -#include "parser/parser_state.h" +#include "parser/input.h" +#include "parser/parser.h" #include "util/integer.h" #include "util/output.h" #include "util/rational.h" @@ -74,7 +74,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 ((ParserState*)PARSER->super) +#define PARSER_STATE ((Parser*)PARSER->super) #undef EXPR_MANAGER #define EXPR_MANAGER PARSER_STATE->getExprManager() #undef MK_EXPR @@ -85,11 +85,11 @@ using namespace CVC4::parser; /** * Sets the logic for the current benchmark. Declares any logic symbols. * - * @param parserState pointer to the current parser state + * @param parser the CVC4 Parser object * @param name the name of the logic (e.g., QF_UF, AUFLIA) */ void -setLogic(ParserState *parserState, const std::string& name) { +setLogic(Parser *parser, const std::string& name) { if( name == "QF_UF" ) { parserState->mkSort("U"); } else if(name == "QF_LRA"){ @@ -174,7 +174,7 @@ benchAttribute returns [CVC4::Command* smt_command] */ annotatedFormula[CVC4::Expr& expr] @init { - Debug("parser") << "annotated formula: " << AntlrInput::tokenText(LT(1)) << std::endl; + Debug("parser") << "annotated formula: " << Input::tokenText(LT(1)) << std::endl; Kind kind; std::string name; std::vector args; /* = getExprVector(); */ @@ -236,11 +236,11 @@ annotatedFormula[CVC4::Expr& expr] | TRUE_TOK { expr = MK_CONST(true); } | FALSE_TOK { expr = MK_CONST(false); } | NUMERAL_TOK - { Integer num( AntlrInput::tokenText($NUMERAL_TOK) ); + { Integer num( Input::tokenText($NUMERAL_TOK) ); expr = MK_CONST(num); } | RATIONAL_TOK { // FIXME: This doesn't work because an SMT rational is not a valid GMP rational string - Rational rat( AntlrInput::tokenText($RATIONAL_TOK) ); + Rational rat( Input::tokenText($RATIONAL_TOK) ); expr = MK_CONST(rat); } // NOTE: Theory constants go here /* TODO: let, flet, quantifiers, arithmetic constants */ @@ -263,7 +263,7 @@ annotatedFormulas[std::vector& formulas, CVC4::Expr& expr] */ builtinOp[CVC4::Kind& kind] @init { - Debug("parser") << "builtin: " << AntlrInput::tokenText(LT(1)) << std::endl; + Debug("parser") << "builtin: " << Input::tokenText(LT(1)) << std::endl; } : NOT_TOK { $kind = CVC4::kind::NOT; } | IMPLIES_TOK { $kind = CVC4::kind::IMPLIES; } @@ -417,7 +417,7 @@ identifier[std::string& id, CVC4::parser::DeclarationCheck check, CVC4::parser::SymbolType type] : IDENTIFIER - { id = AntlrInput::tokenText($IDENTIFIER); + { id = Input::tokenText($IDENTIFIER); Debug("parser") << "identifier: " << id << " check? " << toString(check) << " type? " << toString(type) << std::endl; @@ -432,7 +432,7 @@ identifier[std::string& id, let_identifier[std::string& id, CVC4::parser::DeclarationCheck check] : LET_IDENTIFIER - { id = AntlrInput::tokenText($LET_IDENTIFIER); + { id = Input::tokenText($LET_IDENTIFIER); Debug("parser") << "let_identifier: " << id << " check? " << toString(check) << std::endl; PARSER_STATE->checkDeclaration(id, check, SYM_VARIABLE); } @@ -446,7 +446,7 @@ let_identifier[std::string& id, flet_identifier[std::string& id, CVC4::parser::DeclarationCheck check] : FLET_IDENTIFIER - { id = AntlrInput::tokenText($FLET_IDENTIFIER); + { id = Input::tokenText($FLET_IDENTIFIER); Debug("parser") << "flet_identifier: " << id << " check? " << toString(check) << std::endl; PARSER_STATE->checkDeclaration(id, check); } diff --git a/src/parser/smt/smt_input.cpp b/src/parser/smt/smt_input.cpp index 1bff3d18f..451310cfd 100644 --- a/src/parser/smt/smt_input.cpp +++ b/src/parser/smt/smt_input.cpp @@ -15,9 +15,10 @@ #include +#include "smt_input.h" #include "expr/expr_manager.h" +#include "parser/parser.h" #include "parser/parser_exception.h" -#include "parser/smt/smt_input.h" #include "parser/smt/generated/SmtLexer.h" #include "parser/smt/generated/SmtParser.h" @@ -25,20 +26,9 @@ namespace CVC4 { namespace parser { /* Use lookahead=2 */ -SmtInput::SmtInput(ExprManager* exprManager, const std::string& filename, - bool useMmap) : - AntlrInput(exprManager, filename, 2, useMmap) { - init(); -} - -SmtInput::SmtInput(ExprManager* exprManager, const std::string& input, - const std::string& name) : - AntlrInput(exprManager, input, name, 2) { - init(); -} - -void SmtInput::init() { - pANTLR3_INPUT_STREAM input = getInputStream(); +SmtInput::SmtInput(AntlrInputStream *inputStream) : + Input(inputStream, 2) { + pANTLR3_INPUT_STREAM input = inputStream->getAntlr3InputStream(); AlwaysAssert( input != NULL ); d_pSmtLexer = SmtLexerNew(input); @@ -46,7 +36,7 @@ void SmtInput::init() { throw ParserException("Failed to create SMT lexer."); } - setLexer( d_pSmtLexer->pLexer ); + setAntlr3Lexer( d_pSmtLexer->pLexer ); pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream(); AlwaysAssert( tokenStream != NULL ); @@ -56,7 +46,7 @@ void SmtInput::init() { throw ParserException("Failed to create SMT parser."); } - setParser(d_pSmtParser->pParser); + setAntlr3Parser(d_pSmtParser->pParser); } @@ -65,11 +55,11 @@ SmtInput::~SmtInput() { d_pSmtParser->free(d_pSmtParser); } -Command* SmtInput::doParseCommand() throw (ParserException) { +Command* SmtInput::parseCommand() throw (ParserException) { return d_pSmtParser->parseCommand(d_pSmtParser); } -Expr SmtInput::doParseExpr() throw (ParserException) { +Expr SmtInput::parseExpr() throw (ParserException) { return d_pSmtParser->parseExpr(d_pSmtParser); } diff --git a/src/parser/smt/smt_input.h b/src/parser/smt/smt_input.h index f93a1bf0d..e9f4d2578 100644 --- a/src/parser/smt/smt_input.h +++ b/src/parser/smt/smt_input.h @@ -18,7 +18,7 @@ #ifndef __CVC4__PARSER__SMT_INPUT_H #define __CVC4__PARSER__SMT_INPUT_H -#include "parser/antlr_input.h" +#include "parser/input.h" #include "parser/smt/generated/SmtLexer.h" #include "parser/smt/generated/SmtParser.h" @@ -32,7 +32,7 @@ class ExprManager; namespace parser { -class SmtInput : public AntlrInput { +class SmtInput : public Input { /** The ANTLR3 SMT lexer for the input. */ pSmtLexer d_pSmtLexer; @@ -43,14 +43,11 @@ class SmtInput : public AntlrInput { public: /** - * Create a file input. + * Create an input. * - * @param exprManager the manager to use when building expressions from the input - * @param filename the path of the file to read - * @param useMmap true if the input should use memory-mapped - * I/O; otherwise, the input will use the standard ANTLR3 I/O implementation. + * @param inputStream the input stream to use */ - SmtInput(ExprManager* exprManager, const std::string& filename, bool useMmap); + SmtInput(AntlrInputStream *inputStream); /** * Create a string input. @@ -59,7 +56,7 @@ public: * @param input the string to read * @param name the "filename" to use when reporting errors */ - SmtInput(ExprManager* exprManager, const std::string& input, const std::string& name); +// SmtInput(ExprManager* exprManager, const std::string& input, const std::string& name); /** Destructor. Frees the lexer and the parser. */ ~SmtInput(); @@ -72,7 +69,7 @@ protected: * * @throws ParserException if an error is encountered during parsing. */ - Command* doParseCommand() throw(ParserException); + Command* parseCommand() throw(ParserException); /** * Parse an expression from the input. Returns a null @@ -80,7 +77,7 @@ protected: * * @throws ParserException if an error is encountered during parsing. */ - Expr doParseExpr() throw(ParserException); + Expr parseExpr() throw(ParserException); private: diff --git a/src/parser/symbol_table.h b/src/parser/symbol_table.h deleted file mode 100644 index d6467f4e9..000000000 --- a/src/parser/symbol_table.h +++ /dev/null @@ -1,105 +0,0 @@ -/********************* */ -/** symbol_table.h - ** Original author: cconway - ** Major contributors: dejan, mdeters - ** 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 symbol table for the parsers' use. - **/ - -#include "cvc4parser_private.h" - -#ifndef __CVC4__PARSER__SYMBOL_TABLE_H -#define __CVC4__PARSER__SYMBOL_TABLE_H - -#include -#include - -#include - -#include "util/Assert.h" - -namespace CVC4 { -namespace parser { - -struct StringHashFunction { - size_t operator()(const std::string& str) const { - return __gnu_cxx::hash()(str.c_str()); - } -}; - -/** - * Generic symbol table for looking up variables by name. - */ -template -class SymbolTable { - -private: - - /** The name to expression bindings */ - typedef __gnu_cxx::hash_map - LookupTable; - - /** The table iterator */ - typedef typename LookupTable::iterator table_iterator; - /** The table iterator */ - typedef typename LookupTable::const_iterator const_table_iterator; - - /** Bindings for the names */ - LookupTable d_nameBindings; - -public: - - /** - * Bind the name of the variable to the given expression. If the variable - * has been bind before, this will redefine it until its undefined. - */ - void bindName(const std::string& name, const ObjectType& obj) throw () { - d_nameBindings[name] = obj; - Assert(isBound(name), "Expected name to be bound!"); - } - - /** - * Unbinds the last binding of the name to the expression. - */ - void unbindName(const std::string& name) throw () { - table_iterator find = d_nameBindings.find(name); - if(find != d_nameBindings.end()) { -/* - find->second.pop(); - if(find->second.empty()) { -*/ - d_nameBindings.erase(find); -/* }*/ - } - } - - /** - * Returns the last binding expression of the name. - * Requires the name to have a binding in the table. - */ - ObjectType getObject(const std::string& name) throw () { - table_iterator find = d_nameBindings.find(name); - Assert(find != d_nameBindings.end()); - return find->second; /*.top()*/ - } - - /** - * Returns true is name is bound to an expression. - */ - bool isBound(const std::string& name) const throw () { - const_table_iterator find = d_nameBindings.find(name); - return (find != d_nameBindings.end()); - } -}; - -}/* CVC4::parser namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__PARSER__SYMBOL_TABLE_H */ diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 1f56434c9..666d1c285 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -10,7 +10,7 @@ UNIT_TESTS = \ expr/attribute_white \ expr/attribute_black \ expr/declaration_scope_black \ - parser/parser_white \ + parser/parser_black \ context/context_black \ context/context_white \ context/context_mm_black \ @@ -37,7 +37,7 @@ if HAVE_CXXTESTGEN AM_CPPFLAGS = \ -I. "-I@CXXTEST@" "-I@top_srcdir@/src/include" "-I@top_srcdir@/src" \ - $(TEST_CPPFLAGS) + $(ANTLR_INCLUDES) $(TEST_CPPFLAGS) AM_CXXFLAGS = -Wall $(TEST_CXXFLAGS) AM_LDFLAGS = $(TEST_LDFLAGS) diff --git a/test/unit/parser/parser_white.h b/test/unit/parser/parser_black.h similarity index 83% rename from test/unit/parser/parser_white.h rename to test/unit/parser/parser_black.h index 1d19525d6..9a2864781 100644 --- a/test/unit/parser/parser_white.h +++ b/test/unit/parser/parser_black.h @@ -20,7 +20,7 @@ #include "expr/expr.h" #include "expr/expr_manager.h" #include "parser/input.h" -#include "parser/parser_state.h" +#include "parser/parser.h" #include "expr/command.h" #include "util/output.h" @@ -144,28 +144,28 @@ const string badSmtExprs[] = { const int numBadSmtExprs = sizeof(badSmtExprs) / sizeof(string); -class ParserWhite : public CxxTest::TestSuite { +class ParserBlack : public CxxTest::TestSuite { ExprManager *d_exprManager; /* Set up declaration context for expr inputs */ - void setupContext(ParserState* parserState) { + void setupContext(Parser& parser) { /* a, b, c: BOOLEAN */ - parserState->mkVar("a",d_exprManager->booleanType()); - parserState->mkVar("b",d_exprManager->booleanType()); - parserState->mkVar("c",d_exprManager->booleanType()); + parser.mkVar("a",d_exprManager->booleanType()); + parser.mkVar("b",d_exprManager->booleanType()); + parser.mkVar("c",d_exprManager->booleanType()); /* t, u, v: TYPE */ - Type t = parserState->mkSort("t"); - Type u = parserState->mkSort("u"); - Type v = parserState->mkSort("v"); + Type t = parser.mkSort("t"); + Type u = parser.mkSort("u"); + Type v = parser.mkSort("v"); /* f : t->u; g: u->v; h: v->t; */ - parserState->mkVar("f", d_exprManager->mkFunctionType(t,u)); - parserState->mkVar("g", d_exprManager->mkFunctionType(u,v)); - parserState->mkVar("h", d_exprManager->mkFunctionType(v,t)); + parser.mkVar("f", d_exprManager->mkFunctionType(t,u)); + parser.mkVar("g", d_exprManager->mkFunctionType(u,v)); + parser.mkVar("h", d_exprManager->mkFunctionType(v,t)); /* x:t; y:u; z:v; */ - parserState->mkVar("x",t); - parserState->mkVar("y",u); - parserState->mkVar("z",v); + parser.mkVar("x",t); + parser.mkVar("y",u); + parser.mkVar("z",v); } void tryGoodInputs(InputLanguage d_lang, const string goodInputs[], int numInputs) { @@ -175,15 +175,16 @@ class ParserWhite : public CxxTest::TestSuite { // Debug.on("parser-extra"); Debug("test") << "Testing good input: '" << goodInputs[i] << "'\n"; // istringstream stream(goodInputs[i]); - Input* parser = Input::newStringInput(d_exprManager, d_lang, goodInputs[i], "test"); - TS_ASSERT( !parser->done() ); + Input* input = Input::newStringInput(d_lang, goodInputs[i], "test"); + Parser parser(d_exprManager, input); + TS_ASSERT( !parser.done() ); Command* cmd; - while((cmd = parser->parseNextCommand())) { + while((cmd = parser.nextCommand()) != NULL) { // cout << "Parsed command: " << (*cmd) << endl; } - TS_ASSERT( parser->parseNextCommand() == NULL ); - TS_ASSERT( parser->done() ); - delete parser; + TS_ASSERT( parser.nextCommand() == NULL ); + TS_ASSERT( parser.done() ); + delete input; // Debug.off("parser"); // Debug.off("parser-extra"); } catch (Exception& e) { @@ -199,13 +200,14 @@ class ParserWhite : public CxxTest::TestSuite { for(int i = 0; i < numInputs; ++i) { // cout << "Testing bad input: '" << badInputs[i] << "'\n"; // Debug.on("parser"); - Input* parser = Input::newStringInput(d_exprManager, d_lang, badInputs[i], "test"); + Input* input = Input::newStringInput(d_lang, badInputs[i], "test"); + Parser parser(d_exprManager, input); TS_ASSERT_THROWS - ( while(parser->parseNextCommand()); + ( while(parser.nextCommand()); cout << "\nBad input succeeded:\n" << badInputs[i] << endl;, ParserException ); // Debug.off("parser"); - delete parser; + delete input; } } @@ -218,15 +220,16 @@ class ParserWhite : public CxxTest::TestSuite { // cout << "Testing good expr: '" << goodBooleanExprs[i] << "'\n"; // Debug.on("parser"); // istringstream stream(context + goodBooleanExprs[i]); - Input* input = Input::newStringInput(d_exprManager, d_lang, + Input* input = Input::newStringInput(d_lang, goodBooleanExprs[i], "test"); - TS_ASSERT( !input->done() ); - setupContext(input->getParserState()); - TS_ASSERT( !input->done() ); - Expr e = input->parseNextExpression(); + Parser parser(d_exprManager, input); + TS_ASSERT( !parser.done() ); + setupContext(parser); + TS_ASSERT( !parser.done() ); + Expr e = parser.nextExpression(); TS_ASSERT( !e.isNull() ); - e = input->parseNextExpression(); - TS_ASSERT( input->done() ); + e = parser.nextExpression(); + TS_ASSERT( parser.done() ); TS_ASSERT( e.isNull() ); delete input; } catch (Exception& e) { @@ -242,14 +245,14 @@ class ParserWhite : public CxxTest::TestSuite { for(int i = 0; i < numExprs; ++i) { // cout << "Testing bad expr: '" << badBooleanExprs[i] << "'\n"; // istringstream stream(context + badBooleanExprs[i]); - Input* input = Input::newStringInput(d_exprManager, d_lang, + Input* input = Input::newStringInput(d_lang, badBooleanExprs[i], "test"); + Parser parser(d_exprManager, input); - TS_ASSERT( !input->done() ); - setupContext(input->getParserState()); - TS_ASSERT( !input->done() ); + setupContext(parser); + TS_ASSERT( !parser.done() ); TS_ASSERT_THROWS - ( input->parseNextExpression(); + ( parser.nextExpression(); cout << "\nBad expr succeeded: " << badBooleanExprs[i] << endl;, ParserException ); delete input; -- 2.30.2