From: Christopher L. Conway Date: Sat, 1 May 2010 20:44:09 +0000 (+0000) Subject: Fixing private/public header warnings in parser library X-Git-Tag: cvc5-1.0.0~9093 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d0affb22ebcd4cc7cc7dd6ec7a51233d8632d630;p=cvc5.git Fixing private/public header warnings in parser library --- diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index 380f40c6a..7029c01e5 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -35,13 +35,15 @@ 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 \ diff --git a/src/parser/antlr_input_imports.cpp b/src/parser/antlr_input_imports.cpp new file mode 100644 index 000000000..75944b21b --- /dev/null +++ b/src/parser/antlr_input_imports.cpp @@ -0,0 +1,245 @@ +/* + * The functions in this file are based on implementations in libantlr3c, + * with only minor CVC4-specific changes. + */ + +// [The "BSD licence"] +// Copyright (c) 2005-2009 Jim Idle, Temporal Wave LLC +// http://www.temporal-wave.com +// http://www.linkedin.com/in/jimidle +// +// All rights reserved. +// +// Redistribution and use in source and binary forms, with or without +// modification, are permitted provided that the following conditions +// are met: +// 1. Redistributions of source code must retain the above copyright +// notice, this list of conditions and the following disclaimer. +// 2. Redistributions in binary form must reproduce the above copyright +// notice, this list of conditions and the following disclaimer in the +// documentation and/or other materials provided with the distribution. +// 3. The name of the author may not be used to endorse or promote products +// derived from this software without specific prior written permission. +// +// THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR +// IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES +// OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. +// IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, +// INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT +// NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +// DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +// THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +// (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF +// THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + +#include +#include + +#include "antlr_input.h" +#include "parser.h" +#include "util/Assert.h" + +using namespace std; + +namespace CVC4 { +namespace parser { + +/// Report a recognition problem. +/// +/// This method sets errorRecovery to indicate the parser is recovering +/// not parsing. Once in recovery mode, no errors are generated. +/// To get out of recovery mode, the parser must successfully match +/// a token (after a resync). So it will go: +/// +/// 1. error occurs +/// 2. enter recovery mode, report error +/// 3. consume until token found in resynch set +/// 4. try to resume parsing +/// 5. next match() will reset errorRecovery mode +/// +/// If you override, make sure to update errorCount if you care about that. +/// +/* *** 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 Input class instead of the + * default error printer. + */ +void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) { + pANTLR3_EXCEPTION ex = recognizer->state->exception; + pANTLR3_UINT8 * tokenNames = recognizer->state->tokenNames; + stringstream ss; + + // Signal we are in error recovery now + recognizer->state->errorRecovery = ANTLR3_TRUE; + + // Indicate this recognizer had an error while processing. + recognizer->state->errorCount++; + + // Call the builtin error formatter + // recognizer->displayRecognitionError(recognizer, recognizer->state->tokenNames); + + /* TODO: Make error messages more useful, maybe by including more expected tokens and information + * about the current token. */ + switch(ex->type) { + case ANTLR3_UNWANTED_TOKEN_EXCEPTION: + + // Indicates that the recognizer was fed a token which seems to be + // spurious input. We can detect this when the token that follows + // this unwanted token would normally be part of the syntactically + // correct stream. Then we can see that the token we are looking at + // is just something that should not be there and throw this exception. + // + if(tokenNames == NULL) { + ss << "Unexpected token." ; + } else { + if(ex->expecting == ANTLR3_TOKEN_EOF) { + ss << "Expected end of file."; + } else { + ss << "Expected " << tokenNames[ex->expecting] + << ", found '" << tokenText((pANTLR3_COMMON_TOKEN)ex->token) << "'."; + } + } + break; + + case ANTLR3_MISSING_TOKEN_EXCEPTION: + + // Indicates that the recognizer detected that the token we just + // hit would be valid syntactically if preceded by a particular + // token. Perhaps a missing ';' at line end or a missing ',' in an + // expression list, and such like. + // + if(tokenNames == NULL) { + ss << "Missing token (" << ex->expecting << ")."; + } else { + if(ex->expecting == ANTLR3_TOKEN_EOF) { + ss << "Missing end of file marker."; + } else { + ss << "Missing " << tokenNames[ex->expecting] << "."; + } + } + break; + + case ANTLR3_RECOGNITION_EXCEPTION: + + // Indicates that the recognizer received a token + // in the input that was not predicted. This is the basic exception type + // from which all others are derived. So we assume it was a syntax error. + // You may get this if there are not more tokens and more are needed + // to complete a parse for instance. + // + ss <<"Syntax error."; + break; + + case ANTLR3_MISMATCHED_TOKEN_EXCEPTION: + + // We were expecting to see one thing and got another. This is the + // most common error if we could not detect a missing or unwanted token. + // Here you can spend your efforts to + // derive more useful error messages based on the expected + // token set and the last token and so on. The error following + // bitmaps do a good job of reducing the set that we were looking + // for down to something small. Knowing what you are parsing may be + // able to allow you to be even more specific about an error. + // + if(tokenNames == NULL) { + ss << "Syntax error."; + } else { + if(ex->expecting == ANTLR3_TOKEN_EOF) { + ss << "Expected end of file."; + } else { + ss << "Expected " << tokenNames[ex->expecting] << "."; + } + } + break; + + case ANTLR3_NO_VIABLE_ALT_EXCEPTION: + // We could not pick any alt decision from the input given + // so god knows what happened - however when you examine your grammar, + // you should. It means that at the point where the current token occurred + // that the DFA indicates nowhere to go from here. + // + ss << "Unexpected token: '" << tokenText((pANTLR3_COMMON_TOKEN)ex->token) << "'."; + break; + + case ANTLR3_MISMATCHED_SET_EXCEPTION: + + { + ANTLR3_UINT32 count; + ANTLR3_UINT32 bit; + ANTLR3_UINT32 size; + ANTLR3_UINT32 numbits; + pANTLR3_BITSET errBits; + + // This means we were able to deal with one of a set of + // possible tokens at this point, but we did not see any + // member of that set. + // + ss << "Unexpected input: '" << tokenText((pANTLR3_COMMON_TOKEN)ex->token) + << "'. Expected one of: "; + + // What tokens could we have accepted at this point in the + // parse? + // + count = 0; + errBits = antlr3BitsetLoad(ex->expectingSet); + numbits = errBits->numBits(errBits); + size = errBits->size(errBits); + + if(size > 0) { + // However many tokens we could have dealt with here, it is usually + // not useful to print ALL of the set here. I arbitrarily chose 8 + // here, but you should do whatever makes sense for you of course. + // No token number 0, so look for bit 1 and on. + // + for(bit = 1; bit < numbits && count < 8 && count < size; bit++) { + // TODO: This doesn;t look right - should be asking if the bit is set!! + // + if(tokenNames[bit]) { + if( count++ > 0 ) { + ss << ", "; + } + ss << tokenNames[bit]; + } + } + } else { + Unreachable("Parse error with empty set of expected tokens."); + } + } + break; + + case ANTLR3_EARLY_EXIT_EXCEPTION: + + // We entered a loop requiring a number of token sequences + // but found a token that ended that sequence earlier than + // we should have done. + // + ss << "Sequence terminated early by token: '" + << tokenText((pANTLR3_COMMON_TOKEN)ex->token) << "'."; + break; + + default: + + // We don't handle any other exceptions here, but you can + // if you wish. If we get an exception that hits this point + // then we are just going to report what we know about the + // token. + // + Unhandled("Unexpected exception in parser."); + break; + } + + // Now get ready to throw an exception + pANTLR3_PARSER antlr3Parser = (pANTLR3_PARSER)(recognizer->super); + AlwaysAssert(antlr3Parser!=NULL); + Parser *parser = (Parser*)(antlr3Parser->super); + AlwaysAssert(parser!=NULL); + AntlrInput *input = (AntlrInput*) parser->getInput() ; + AlwaysAssert(input!=NULL); + + // Call the error display routine + input->parseError(ss.str()); +} + +} // namespace parser +} // namespace CVC4 diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 94a8a6a32..a53604efa 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -59,7 +59,7 @@ namespace CVC4 { #include "expr/expr.h" #include "expr/kind.h" #include "expr/type.h" -#include "parser/input.h" +#include "parser/antlr_input.h" #include "parser/parser.h" #include "util/output.h" #include @@ -104,7 +104,7 @@ parseCommand returns [CVC4::Command* cmd] command returns [CVC4::Command* cmd = 0] @init { Expr f; - Debug("parser-extra") << "command: " << Input::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "command: " << AntlrInput::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: " << Input::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "declaration: " << AntlrInput::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: " << Input::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "declType: " << AntlrInput::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: " << Input::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "type: " << AntlrInput::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 = Input::tokenText($IDENTIFIER); + { id = AntlrInput::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: " << Input::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "base type: " << AntlrInput::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: " << Input::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "type symbol: " << AntlrInput::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: " << Input::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "formula: " << AntlrInput::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: " << Input::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "<=> formula: " << AntlrInput::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: " << Input::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "=> Formula: " << AntlrInput::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: " << Input::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "OR Formula: " << AntlrInput::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: " << Input::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "XOR formula: " << AntlrInput::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: " << Input::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "AND Formula: " << AntlrInput::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: " << Input::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "NOT formula: " << AntlrInput::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: " << Input::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "predicate formula: " << AntlrInput::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: " << Input::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl; } : /* function application */ - // { isFunction(Input::tokenText(LT(1))) }? + // { isFunction(AntlrInput::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: " << Input::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "ite: " << AntlrInput::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: " << Input::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "else: " << AntlrInput::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: " << Input::tokenText(LT(1)) << std::endl; + Debug("parser-extra") << "function symbol: " << AntlrInput::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 4595c52db..48936a4c9 100644 --- a/src/parser/cvc/cvc_input.cpp +++ b/src/parser/cvc/cvc_input.cpp @@ -16,7 +16,7 @@ #include #include "expr/expr_manager.h" -#include "parser/input.h" +#include "parser/antlr_input.h" #include "parser/parser_exception.h" #include "parser/cvc/cvc_input.h" #include "parser/cvc/generated/CvcLexer.h" @@ -27,7 +27,7 @@ namespace parser { /* Use lookahead=2 */ CvcInput::CvcInput(AntlrInputStream *inputStream) : - Input(inputStream,2) { + AntlrInput(inputStream,2) { pANTLR3_INPUT_STREAM input = inputStream->getAntlr3InputStream(); AlwaysAssert( input != NULL ); diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h index 0d264f606..ad7110bed 100644 --- a/src/parser/cvc/cvc_input.h +++ b/src/parser/cvc/cvc_input.h @@ -13,12 +13,12 @@ ** [[ Add file-specific comments here ]] **/ -#include "cvc4parser_public.h" +#include "cvc4parser_private.h" #ifndef __CVC4__PARSER__CVC_INPUT_H #define __CVC4__PARSER__CVC_INPUT_H -#include "parser/input.h" +#include "parser/antlr_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 Input { +class CvcInput : public AntlrInput { /** The ANTLR3 CVC lexer for the input. */ pCvcLexer d_pCvcLexer; diff --git a/src/parser/input.cpp b/src/parser/input.cpp index 33bee84a6..3c1747759 100644 --- a/src/parser/input.cpp +++ b/src/parser/input.cpp @@ -10,24 +10,16 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** A super-class for ANTLR-generated input language parsers + ** A super-class for input language parsers **/ -#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.h" #include "expr/command.h" #include "expr/type.h" -#include "parser/cvc/cvc_input.h" -#include "parser/smt/smt_input.h" -#include "parser/smt2/smt2_input.h" +#include "parser/antlr_input.h" #include "util/output.h" #include "util/Assert.h" @@ -39,221 +31,33 @@ using namespace CVC4::kind; namespace CVC4 { namespace parser { -AntlrInputStream::AntlrInputStream(std::string name, pANTLR3_INPUT_STREAM input) : - d_name(name), - d_input(input) { -} - -AntlrInputStream::~AntlrInputStream() { - d_input->free(d_input); -} - -pANTLR3_INPUT_STREAM AntlrInputStream::getAntlr3InputStream() const { - return d_input; -} - -const std::string AntlrInputStream::getName() const { +const std::string InputStream::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()) ); - } -/* - 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 + "'"); - } -*/ - 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), +Input::Input(InputStream *inputStream) : 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() { - d_tokenStream->free(d_tokenStream); delete d_inputStream; } -AntlrInputStream *Input::getInputStream() { +InputStream *Input::getInputStream() { return d_inputStream; } -pANTLR3_COMMON_TOKEN_STREAM Input::getTokenStream() { - return d_tokenStream; -} - -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); - - // Call the error display routine - input->parseError("Error finding next token."); -} - Input* Input::newFileInput(InputLanguage lang, const std::string& filename, bool useMmap) { AntlrInputStream *inputStream = AntlrInputStream::newFileInputStream(filename,useMmap); - return newInput(lang,inputStream); + return AntlrInput::newInput(lang,inputStream); } Input* Input::newStringInput(InputLanguage lang, const std::string& str, const std::string& name) { 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(inputStream); - break; - } - case LANG_SMTLIB: - input = new SmtInput(inputStream); - break; - - case LANG_SMTLIB_V2: - input = new Smt2Input(inputStream); - break; - - default: - Unhandled(lang); - } - return input; + return AntlrInput::newInput(lang,inputStream); } - -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 ecc2063db..80849c034 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -10,15 +10,14 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** Base for ANTLR parser classes. + ** Base for parser inputs. **/ -#include "cvc4parser_private.h" +#include "cvc4parser_public.h" -#ifndef __CVC4__PARSER__ANTLR_INPUT_H -#define __CVC4__PARSER__ANTLR_INPUT_H +#ifndef __CVC4__PARSER__INPUT_H +#define __CVC4__PARSER__INPUT_H -#include #include #include #include @@ -38,44 +37,25 @@ class FunctionType; namespace parser { /** Wrapper around an ANTLR3 input stream. */ -class AntlrInputStream { +class InputStream { + + /** The name of this input stream. */ 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"); +protected: + + /** Initialize the input stream with a name. */ + InputStream(std::string name) : + d_name(name) { } public: - virtual ~AntlrInputStream(); + /** Do-nothing destructor. */ + virtual ~InputStream() { } - pANTLR3_INPUT_STREAM getAntlr3InputStream() const; + /** Get the name of this input stream. */ 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; @@ -89,37 +69,8 @@ class Parser; class CVC4_PUBLIC Input { friend class Parser; // for parseError, parseCommand, parseExpr - /** The display name of the input (e.g., the filename). */ - std::string d_name; - - /** 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 Input::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 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); + /** The input stream. */ + InputStream *d_inputStream; /* Since we own d_tokenStream and it needs to be freed, we need to prevent * copy construction and assignment. @@ -140,15 +91,6 @@ public: */ 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 lang the input language @@ -165,30 +107,16 @@ public: */ static Input* newStringInput(InputLanguage lang, const std::string& input, const std::string& name); - /** Retrieve the text associated with a token. */ - inline static std::string tokenText(pANTLR3_COMMON_TOKEN token); - /** Retrieve an Integer from the text of a token */ - inline static Integer tokenToInteger( pANTLR3_COMMON_TOKEN token ); - /** Retrieve a Rational from the text of a token */ - inline static Rational tokenToRational(pANTLR3_COMMON_TOKEN token); - protected: - /** Create an input. This input takes ownership of the given input stream, - * and will delete it at destruction time. + + /** Create an input. * - * @param inputStream the input stream to use - * @param lookahead the lookahead needed to parse the input (i.e., k for - * an LL(k) grammar) + * @param inputStream the input stream */ - Input(AntlrInputStream *inputStream, unsigned int lookahead); - + Input(InputStream* inputStream); /** Retrieve the input stream for this parser. */ - AntlrInputStream *getInputStream(); - - /** Retrieve the token stream for this parser. Must not be called before - * setLexer(). */ - pANTLR3_COMMON_TOKEN_STREAM getTokenStream(); + InputStream *getInputStream(); /** Parse a command from * the input by invoking the implementation-specific parsing method. Returns @@ -201,7 +129,7 @@ protected: /** * Throws a ParserException with the given message. */ - void parseError(const std::string& msg) throw (ParserException); + virtual void parseError(const std::string& msg) throw (ParserException) = 0; /** Parse an * expression from the input by invoking the implementation-specific @@ -212,38 +140,10 @@ protected: */ 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); + virtual void setParser(Parser *parser) = 0; }; -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; -} - -Integer Input::tokenToInteger(pANTLR3_COMMON_TOKEN token) { - Integer i( tokenText(token) ); - return i; -} - -Rational Input::tokenToRational(pANTLR3_COMMON_TOKEN token) { - Rational r( tokenText(token) ); - return r; -} - }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/input_imports.cpp b/src/parser/input_imports.cpp deleted file mode 100644 index 73d804f95..000000000 --- a/src/parser/input_imports.cpp +++ /dev/null @@ -1,245 +0,0 @@ -/* - * The functions in this file are based on implementations in libantlr3c, - * with only minor CVC4-specific changes. - */ - -// [The "BSD licence"] -// Copyright (c) 2005-2009 Jim Idle, Temporal Wave LLC -// http://www.temporal-wave.com -// http://www.linkedin.com/in/jimidle -// -// All rights reserved. -// -// Redistribution and use in source and binary forms, with or without -// modification, are permitted provided that the following conditions -// are met: -// 1. Redistributions of source code must retain the above copyright -// notice, this list of conditions and the following disclaimer. -// 2. Redistributions in binary form must reproduce the above copyright -// notice, this list of conditions and the following disclaimer in the -// documentation and/or other materials provided with the distribution. -// 3. The name of the author may not be used to endorse or promote products -// derived from this software without specific prior written permission. -// -// THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR -// IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES -// OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. -// IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, -// INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT -// NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, -// DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY -// THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT -// (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF -// THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. - -#include -#include - -#include "input.h" -#include "parser.h" -#include "util/Assert.h" - -using namespace std; - -namespace CVC4 { -namespace parser { - -/// Report a recognition problem. -/// -/// This method sets errorRecovery to indicate the parser is recovering -/// not parsing. Once in recovery mode, no errors are generated. -/// To get out of recovery mode, the parser must successfully match -/// a token (after a resync). So it will go: -/// -/// 1. error occurs -/// 2. enter recovery mode, report error -/// 3. consume until token found in resynch set -/// 4. try to resume parsing -/// 5. next match() will reset errorRecovery mode -/// -/// If you override, make sure to update errorCount if you care about that. -/// -/* *** 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 Input class instead of the - * default error printer. - */ -void Input::reportError(pANTLR3_BASE_RECOGNIZER recognizer) { - pANTLR3_EXCEPTION ex = recognizer->state->exception; - pANTLR3_UINT8 * tokenNames = recognizer->state->tokenNames; - stringstream ss; - - // Signal we are in error recovery now - recognizer->state->errorRecovery = ANTLR3_TRUE; - - // Indicate this recognizer had an error while processing. - recognizer->state->errorCount++; - - // Call the builtin error formatter - // recognizer->displayRecognitionError(recognizer, recognizer->state->tokenNames); - - /* TODO: Make error messages more useful, maybe by including more expected tokens and information - * about the current token. */ - switch(ex->type) { - case ANTLR3_UNWANTED_TOKEN_EXCEPTION: - - // Indicates that the recognizer was fed a token which seems to be - // spurious input. We can detect this when the token that follows - // this unwanted token would normally be part of the syntactically - // correct stream. Then we can see that the token we are looking at - // is just something that should not be there and throw this exception. - // - if(tokenNames == NULL) { - ss << "Unexpected token." ; - } else { - if(ex->expecting == ANTLR3_TOKEN_EOF) { - ss << "Expected end of file."; - } else { - ss << "Expected " << tokenNames[ex->expecting] - << ", found '" << tokenText((pANTLR3_COMMON_TOKEN)ex->token) << "'."; - } - } - break; - - case ANTLR3_MISSING_TOKEN_EXCEPTION: - - // Indicates that the recognizer detected that the token we just - // hit would be valid syntactically if preceded by a particular - // token. Perhaps a missing ';' at line end or a missing ',' in an - // expression list, and such like. - // - if(tokenNames == NULL) { - ss << "Missing token (" << ex->expecting << ")."; - } else { - if(ex->expecting == ANTLR3_TOKEN_EOF) { - ss << "Missing end of file marker."; - } else { - ss << "Missing " << tokenNames[ex->expecting] << "."; - } - } - break; - - case ANTLR3_RECOGNITION_EXCEPTION: - - // Indicates that the recognizer received a token - // in the input that was not predicted. This is the basic exception type - // from which all others are derived. So we assume it was a syntax error. - // You may get this if there are not more tokens and more are needed - // to complete a parse for instance. - // - ss <<"Syntax error."; - break; - - case ANTLR3_MISMATCHED_TOKEN_EXCEPTION: - - // We were expecting to see one thing and got another. This is the - // most common error if we could not detect a missing or unwanted token. - // Here you can spend your efforts to - // derive more useful error messages based on the expected - // token set and the last token and so on. The error following - // bitmaps do a good job of reducing the set that we were looking - // for down to something small. Knowing what you are parsing may be - // able to allow you to be even more specific about an error. - // - if(tokenNames == NULL) { - ss << "Syntax error."; - } else { - if(ex->expecting == ANTLR3_TOKEN_EOF) { - ss << "Expected end of file."; - } else { - ss << "Expected " << tokenNames[ex->expecting] << "."; - } - } - break; - - case ANTLR3_NO_VIABLE_ALT_EXCEPTION: - // We could not pick any alt decision from the input given - // so god knows what happened - however when you examine your grammar, - // you should. It means that at the point where the current token occurred - // that the DFA indicates nowhere to go from here. - // - ss << "Unexpected token: '" << tokenText((pANTLR3_COMMON_TOKEN)ex->token) << "'."; - break; - - case ANTLR3_MISMATCHED_SET_EXCEPTION: - - { - ANTLR3_UINT32 count; - ANTLR3_UINT32 bit; - ANTLR3_UINT32 size; - ANTLR3_UINT32 numbits; - pANTLR3_BITSET errBits; - - // This means we were able to deal with one of a set of - // possible tokens at this point, but we did not see any - // member of that set. - // - ss << "Unexpected input: '" << tokenText((pANTLR3_COMMON_TOKEN)ex->token) - << "'. Expected one of: "; - - // What tokens could we have accepted at this point in the - // parse? - // - count = 0; - errBits = antlr3BitsetLoad(ex->expectingSet); - numbits = errBits->numBits(errBits); - size = errBits->size(errBits); - - if(size > 0) { - // However many tokens we could have dealt with here, it is usually - // not useful to print ALL of the set here. I arbitrarily chose 8 - // here, but you should do whatever makes sense for you of course. - // No token number 0, so look for bit 1 and on. - // - for(bit = 1; bit < numbits && count < 8 && count < size; bit++) { - // TODO: This doesn;t look right - should be asking if the bit is set!! - // - if(tokenNames[bit]) { - if( count++ > 0 ) { - ss << ", "; - } - ss << tokenNames[bit]; - } - } - } else { - Unreachable("Parse error with empty set of expected tokens."); - } - } - break; - - case ANTLR3_EARLY_EXIT_EXCEPTION: - - // We entered a loop requiring a number of token sequences - // but found a token that ended that sequence earlier than - // we should have done. - // - ss << "Sequence terminated early by token: '" - << tokenText((pANTLR3_COMMON_TOKEN)ex->token) << "'."; - break; - - default: - - // We don't handle any other exceptions here, but you can - // if you wish. If we get an exception that hits this point - // then we are just going to report what we know about the - // token. - // - Unhandled("Unexpected exception in parser."); - break; - } - - // Now get ready to throw an exception - pANTLR3_PARSER antlr3Parser = (pANTLR3_PARSER)(recognizer->super); - AlwaysAssert(antlr3Parser!=NULL); - Parser *parser = (Parser*)(antlr3Parser->super); - AlwaysAssert(parser!=NULL); - Input *input = parser->getInput(); - AlwaysAssert(input!=NULL); - - // Call the error display routine - input->parseError(ss.str()); -} - -} // namespace parser -} // namespace CVC4 diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index 5cd94ec0d..bc2ecb661 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -61,7 +61,7 @@ namespace CVC4 { #include "expr/expr.h" #include "expr/kind.h" #include "expr/type.h" -#include "parser/input.h" +#include "parser/antlr_input.h" #include "parser/parser.h" #include "util/integer.h" #include "util/output.h" @@ -174,7 +174,7 @@ benchAttribute returns [CVC4::Command* smt_command] */ annotatedFormula[CVC4::Expr& expr] @init { - Debug("parser") << "annotated formula: " << Input::tokenText(LT(1)) << std::endl; + Debug("parser") << "annotated formula: " << AntlrInput::tokenText(LT(1)) << std::endl; Kind kind; std::string name; std::vector args; /* = getExprVector(); */ @@ -235,10 +235,10 @@ annotatedFormula[CVC4::Expr& expr] | TRUE_TOK { expr = MK_CONST(true); } | FALSE_TOK { expr = MK_CONST(false); } | NUMERAL_TOK - { expr = MK_CONST( Input::tokenToInteger($NUMERAL_TOK) ); } + { expr = MK_CONST( AntlrInput::tokenToInteger($NUMERAL_TOK) ); } | RATIONAL_TOK { // FIXME: This doesn't work because an SMT rational is not a valid GMP rational string - expr = MK_CONST( Input::tokenToRational($RATIONAL_TOK) ); } + expr = MK_CONST( AntlrInput::tokenToRational($RATIONAL_TOK) ); } // NOTE: Theory constants go here /* TODO: quantifiers, arithmetic constants */ ; @@ -260,7 +260,7 @@ annotatedFormulas[std::vector& formulas, CVC4::Expr& expr] */ builtinOp[CVC4::Kind& kind] @init { - Debug("parser") << "builtin: " << Input::tokenText(LT(1)) << std::endl; + Debug("parser") << "builtin: " << AntlrInput::tokenText(LT(1)) << std::endl; } : NOT_TOK { $kind = CVC4::kind::NOT; } | IMPLIES_TOK { $kind = CVC4::kind::IMPLIES; } @@ -422,7 +422,7 @@ identifier[std::string& id, CVC4::parser::DeclarationCheck check, CVC4::parser::SymbolType type] : IDENTIFIER - { id = Input::tokenText($IDENTIFIER); + { id = AntlrInput::tokenText($IDENTIFIER); Debug("parser") << "identifier: " << id << " check? " << toString(check) << " type? " << toString(type) << std::endl; @@ -437,7 +437,7 @@ identifier[std::string& id, let_identifier[std::string& id, CVC4::parser::DeclarationCheck check] : LET_IDENTIFIER - { id = Input::tokenText($LET_IDENTIFIER); + { id = AntlrInput::tokenText($LET_IDENTIFIER); Debug("parser") << "let_identifier: " << id << " check? " << toString(check) << std::endl; PARSER_STATE->checkDeclaration(id, check, SYM_VARIABLE); } @@ -451,7 +451,7 @@ let_identifier[std::string& id, flet_identifier[std::string& id, CVC4::parser::DeclarationCheck check] : FLET_IDENTIFIER - { id = Input::tokenText($FLET_IDENTIFIER); + { id = AntlrInput::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 451310cfd..520e6a6d6 100644 --- a/src/parser/smt/smt_input.cpp +++ b/src/parser/smt/smt_input.cpp @@ -17,6 +17,7 @@ #include "smt_input.h" #include "expr/expr_manager.h" +#include "parser/input.h" #include "parser/parser.h" #include "parser/parser_exception.h" #include "parser/smt/generated/SmtLexer.h" @@ -27,7 +28,7 @@ namespace parser { /* Use lookahead=2 */ SmtInput::SmtInput(AntlrInputStream *inputStream) : - Input(inputStream, 2) { + AntlrInput(inputStream, 2) { pANTLR3_INPUT_STREAM input = inputStream->getAntlr3InputStream(); AlwaysAssert( input != NULL ); diff --git a/src/parser/smt/smt_input.h b/src/parser/smt/smt_input.h index e9f4d2578..429f4dad5 100644 --- a/src/parser/smt/smt_input.h +++ b/src/parser/smt/smt_input.h @@ -13,12 +13,12 @@ ** [[ Add file-specific comments here ]] **/ -#include "cvc4parser_public.h" +#include "cvc4parser_private.h" #ifndef __CVC4__PARSER__SMT_INPUT_H #define __CVC4__PARSER__SMT_INPUT_H -#include "parser/input.h" +#include "parser/antlr_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 Input { +class SmtInput : public AntlrInput { /** The ANTLR3 SMT lexer for the input. */ pSmtLexer d_pSmtLexer; diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 422e4b19e..9b5b83a76 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -61,7 +61,7 @@ namespace CVC4 { #include "expr/expr.h" #include "expr/kind.h" #include "expr/type.h" -#include "parser/input.h" +#include "parser/antlr_input.h" #include "parser/parser.h" #include "util/integer.h" #include "util/output.h" @@ -142,7 +142,7 @@ command returns [CVC4::Command* cmd] | /* sort declaration */ DECLARE_SORT_TOK identifier[name,CHECK_UNDECLARED,SYM_SORT] n=NUMERAL_TOK { Debug("parser") << "declare sort: '" << name << "' arity=" << n << std::endl; - if( Input::tokenToInteger(n) > 0 ) { + if( AntlrInput::tokenToInteger(n) > 0 ) { Unimplemented("Parameterized user sorts."); } PARSER_STATE->mkSort(name); @@ -172,7 +172,7 @@ command returns [CVC4::Command* cmd] */ term[CVC4::Expr& expr] @init { - Debug("parser") << "term: " << Input::tokenText(LT(1)) << std::endl; + Debug("parser") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl; Kind kind; std::string name; std::vector args; @@ -226,10 +226,10 @@ term[CVC4::Expr& expr] | TRUE_TOK { expr = MK_CONST(true); } | FALSE_TOK { expr = MK_CONST(false); } | NUMERAL_TOK - { expr = MK_CONST( Input::tokenToInteger($NUMERAL_TOK) ); } + { expr = MK_CONST( AntlrInput::tokenToInteger($NUMERAL_TOK) ); } | RATIONAL_TOK { // FIXME: This doesn't work because an SMT rational is not a valid GMP rational string - expr = MK_CONST( Input::tokenToRational($RATIONAL_TOK) ); } + expr = MK_CONST( AntlrInput::tokenToRational($RATIONAL_TOK) ); } // NOTE: Theory constants go here ; @@ -250,7 +250,7 @@ termList[std::vector& formulas, CVC4::Expr& expr] */ builtinOp[CVC4::Kind& kind] @init { - Debug("parser") << "builtin: " << Input::tokenText(LT(1)) << std::endl; + Debug("parser") << "builtin: " << AntlrInput::tokenText(LT(1)) << std::endl; } : NOT_TOK { $kind = CVC4::kind::NOT; } | IMPLIES_TOK { $kind = CVC4::kind::IMPLIES; } @@ -341,7 +341,7 @@ identifier[std::string& id, CVC4::parser::DeclarationCheck check, CVC4::parser::SymbolType type] : IDENTIFIER - { id = Input::tokenText($IDENTIFIER); + { id = AntlrInput::tokenText($IDENTIFIER); Debug("parser") << "identifier: " << id << " check? " << toString(check) << " type? " << toString(type) << std::endl; diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp index 5db4a9bd7..f962578e9 100644 --- a/src/parser/smt2/smt2_input.cpp +++ b/src/parser/smt2/smt2_input.cpp @@ -17,6 +17,7 @@ #include "smt2_input.h" #include "expr/expr_manager.h" +#include "parser/input.h" #include "parser/parser.h" #include "parser/parser_exception.h" #include "parser/smt2/generated/Smt2Lexer.h" @@ -27,7 +28,7 @@ namespace parser { /* Use lookahead=2 */ Smt2Input::Smt2Input(AntlrInputStream *inputStream) : - Input(inputStream, 2) { + AntlrInput(inputStream, 2) { pANTLR3_INPUT_STREAM input = inputStream->getAntlr3InputStream(); AlwaysAssert( input != NULL ); diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h index 48fcb7956..2937d4ed8 100644 --- a/src/parser/smt2/smt2_input.h +++ b/src/parser/smt2/smt2_input.h @@ -13,12 +13,12 @@ ** [[ Add file-specific comments here ]] **/ -#include "cvc4parser_public.h" +#include "cvc4parser_private.h" #ifndef __CVC4__PARSER__SMT2_INPUT_H #define __CVC4__PARSER__SMT2_INPUT_H -#include "parser/input.h" +#include "parser/antlr_input.h" #include "parser/smt2/generated/Smt2Lexer.h" #include "parser/smt2/generated/Smt2Parser.h" @@ -32,7 +32,7 @@ class ExprManager; namespace parser { -class Smt2Input : public Input { +class Smt2Input : public AntlrInput { /** The ANTLR3 SMT2 lexer for the input. */ pSmt2Lexer d_pSmt2Lexer;