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 \
--- /dev/null
+/*
+ * 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 <antlr3.h>
+#include <sstream>
+
+#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
#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 <vector>
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); }
@init {
std::vector<std::string> 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
/** Match the right-hand side of a declaration. Returns the type. */
declType[CVC4::Type& t, std::vector<std::string>& 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
@init {
Type t2;
std::vector<Type> 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]
CVC4::parser::DeclarationCheck check,
CVC4::parser::SymbolType type]
: IDENTIFIER
- { id = Input::tokenText($IDENTIFIER);
+ { id = AntlrInput::tokenText($IDENTIFIER);
PARSER_STATE->checkDeclaration(id, check, type); }
;
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]
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); }
*/
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]
;
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
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]
orFormula[CVC4::Expr& f]
@init {
std::vector<Expr> 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); }
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]
andFormula[CVC4::Expr& f]
@init {
std::vector<Expr> 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); }
*/
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]
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]
@init {
std::string name;
std::vector<Expr> 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
iteTerm[CVC4::Expr& f]
@init {
std::vector<Expr> 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); }
iteElseTerm[CVC4::Expr& f]
@init {
std::vector<Expr> 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); }
*/
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]
#include <antlr3.h>
#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"
/* Use lookahead=2 */
CvcInput::CvcInput(AntlrInputStream *inputStream) :
- Input(inputStream,2) {
+ AntlrInput(inputStream,2) {
pANTLR3_INPUT_STREAM input = inputStream->getAntlr3InputStream();
AlwaysAssert( input != NULL );
** [[ 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"
namespace parser {
-class CvcInput : public Input {
+class CvcInput : public AntlrInput {
/** The ANTLR3 CVC lexer for the input. */
pCvcLexer d_pCvcLexer;
** 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 <limits.h>
-#include <antlr3.h>
-
#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"
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 */
** 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 <antlr3.h>
#include <iostream>
#include <string>
#include <vector>
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 <code>true</code> 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;
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
- * <code>K</code> for an LL(k) grammar. */
- unsigned int d_lookahead;
-
- /** The ANTLR3 lexer associated with this input. This will be <code>NULL</code> initially. It
- * must be set by a call to <code>setLexer</code>, preferably in the subclass constructor. */
- pANTLR3_LEXER d_lexer;
-
- /** The ANTLR3 parser associated with this input. This will be <code>NULL</code> initially. It
- * must be set by a call to <code>setParser</code>, preferably in the subclass constructor.
- * The <code>super</code> field of <code>d_parser</code> will be set to <code>this</code> and
- * <code>reportError</code> will be set to <code>Input::reportError</code>. */
- 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 <code>setLexer</code>.
- * NOTE: We assume that we <em>can</em> 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 <em>can</em> free it on exit. No sharing! */
- AntlrInputStream *d_inputStream;
-
- /** Turns an ANTLR3 exception into a message for the user and calls <code>parseError</code>. */
- static void reportError(pANTLR3_BASE_RECOGNIZER recognizer);
-
- /** Builds a message for a lexer error and calls <code>parseError</code>. */
- 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.
*/
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
*/
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
- * <code>setLexer()</code>. */
- pANTLR3_COMMON_TOKEN_STREAM getTokenStream();
+ InputStream *getInputStream();
/** Parse a command from
* the input by invoking the implementation-specific parsing method. Returns
/**
* Throws a <code>ParserException</code> 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
*/
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 */
+++ /dev/null
-/*
- * 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 <antlr3.h>
-#include <sstream>
-
-#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
#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"
*/
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<Expr> args; /* = getExprVector(); */
| 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 */
;
*/
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; }
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;
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); }
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); }
#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"
/* Use lookahead=2 */
SmtInput::SmtInput(AntlrInputStream *inputStream) :
- Input(inputStream, 2) {
+ AntlrInput(inputStream, 2) {
pANTLR3_INPUT_STREAM input = inputStream->getAntlr3InputStream();
AlwaysAssert( input != NULL );
** [[ 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"
namespace parser {
-class SmtInput : public Input {
+class SmtInput : public AntlrInput {
/** The ANTLR3 SMT lexer for the input. */
pSmtLexer d_pSmtLexer;
#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"
| /* 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);
*/
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<Expr> args;
| 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
;
*/
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; }
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;
#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"
/* Use lookahead=2 */
Smt2Input::Smt2Input(AntlrInputStream *inputStream) :
- Input(inputStream, 2) {
+ AntlrInput(inputStream, 2) {
pANTLR3_INPUT_STREAM input = inputStream->getAntlr3InputStream();
AlwaysAssert( input != NULL );
** [[ 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"
namespace parser {
-class Smt2Input : public Input {
+class Smt2Input : public AntlrInput {
/** The ANTLR3 SMT2 lexer for the input. */
pSmt2Lexer d_pSmt2Lexer;
projects / cvc5.git / commitdiff