From a72c7a26fda2b9c268912e618fd7d71164e4800a Mon Sep 17 00:00:00 2001 From: "Christopher L. Conway" Date: Wed, 28 Apr 2010 18:34:11 +0000 Subject: Refactoring Input/Parser code to support external manipulation of the parser state. --- src/parser/smt/Smt.g | 26 +++++++++++++------------- src/parser/smt/smt_input.cpp | 28 +++++++++------------------- src/parser/smt/smt_input.h | 19 ++++++++----------- 3 files changed, 30 insertions(+), 43 deletions(-) (limited to 'src/parser/smt') diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index 4539a6d43..cf22c5290 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -50,7 +50,7 @@ options { @parser::includes { #include "expr/command.h" -#include "parser/parser_state.h" +#include "parser/parser.h" namespace CVC4 { class Expr; @@ -61,8 +61,8 @@ namespace CVC4 { #include "expr/expr.h" #include "expr/kind.h" #include "expr/type.h" -#include "parser/antlr_input.h" -#include "parser/parser_state.h" +#include "parser/input.h" +#include "parser/parser.h" #include "util/integer.h" #include "util/output.h" #include "util/rational.h" @@ -74,7 +74,7 @@ using namespace CVC4::parser; /* These need to be macros so they can refer to the PARSER macro, which will be defined * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */ #undef PARSER_STATE -#define PARSER_STATE ((ParserState*)PARSER->super) +#define PARSER_STATE ((Parser*)PARSER->super) #undef EXPR_MANAGER #define EXPR_MANAGER PARSER_STATE->getExprManager() #undef MK_EXPR @@ -85,11 +85,11 @@ using namespace CVC4::parser; /** * Sets the logic for the current benchmark. Declares any logic symbols. * - * @param parserState pointer to the current parser state + * @param parser the CVC4 Parser object * @param name the name of the logic (e.g., QF_UF, AUFLIA) */ void -setLogic(ParserState *parserState, const std::string& name) { +setLogic(Parser *parser, const std::string& name) { if( name == "QF_UF" ) { parserState->mkSort("U"); } else if(name == "QF_LRA"){ @@ -174,7 +174,7 @@ benchAttribute returns [CVC4::Command* smt_command] */ annotatedFormula[CVC4::Expr& expr] @init { - Debug("parser") << "annotated formula: " << AntlrInput::tokenText(LT(1)) << std::endl; + Debug("parser") << "annotated formula: " << Input::tokenText(LT(1)) << std::endl; Kind kind; std::string name; std::vector args; /* = getExprVector(); */ @@ -236,11 +236,11 @@ annotatedFormula[CVC4::Expr& expr] | TRUE_TOK { expr = MK_CONST(true); } | FALSE_TOK { expr = MK_CONST(false); } | NUMERAL_TOK - { Integer num( AntlrInput::tokenText($NUMERAL_TOK) ); + { Integer num( Input::tokenText($NUMERAL_TOK) ); expr = MK_CONST(num); } | RATIONAL_TOK { // FIXME: This doesn't work because an SMT rational is not a valid GMP rational string - Rational rat( AntlrInput::tokenText($RATIONAL_TOK) ); + Rational rat( Input::tokenText($RATIONAL_TOK) ); expr = MK_CONST(rat); } // NOTE: Theory constants go here /* TODO: let, flet, quantifiers, arithmetic constants */ @@ -263,7 +263,7 @@ annotatedFormulas[std::vector& formulas, CVC4::Expr& expr] */ builtinOp[CVC4::Kind& kind] @init { - Debug("parser") << "builtin: " << AntlrInput::tokenText(LT(1)) << std::endl; + Debug("parser") << "builtin: " << Input::tokenText(LT(1)) << std::endl; } : NOT_TOK { $kind = CVC4::kind::NOT; } | IMPLIES_TOK { $kind = CVC4::kind::IMPLIES; } @@ -417,7 +417,7 @@ identifier[std::string& id, CVC4::parser::DeclarationCheck check, CVC4::parser::SymbolType type] : IDENTIFIER - { id = AntlrInput::tokenText($IDENTIFIER); + { id = Input::tokenText($IDENTIFIER); Debug("parser") << "identifier: " << id << " check? " << toString(check) << " type? " << toString(type) << std::endl; @@ -432,7 +432,7 @@ identifier[std::string& id, let_identifier[std::string& id, CVC4::parser::DeclarationCheck check] : LET_IDENTIFIER - { id = AntlrInput::tokenText($LET_IDENTIFIER); + { id = Input::tokenText($LET_IDENTIFIER); Debug("parser") << "let_identifier: " << id << " check? " << toString(check) << std::endl; PARSER_STATE->checkDeclaration(id, check, SYM_VARIABLE); } @@ -446,7 +446,7 @@ let_identifier[std::string& id, flet_identifier[std::string& id, CVC4::parser::DeclarationCheck check] : FLET_IDENTIFIER - { id = AntlrInput::tokenText($FLET_IDENTIFIER); + { id = Input::tokenText($FLET_IDENTIFIER); Debug("parser") << "flet_identifier: " << id << " check? " << toString(check) << std::endl; PARSER_STATE->checkDeclaration(id, check); } diff --git a/src/parser/smt/smt_input.cpp b/src/parser/smt/smt_input.cpp index 1bff3d18f..451310cfd 100644 --- a/src/parser/smt/smt_input.cpp +++ b/src/parser/smt/smt_input.cpp @@ -15,9 +15,10 @@ #include +#include "smt_input.h" #include "expr/expr_manager.h" +#include "parser/parser.h" #include "parser/parser_exception.h" -#include "parser/smt/smt_input.h" #include "parser/smt/generated/SmtLexer.h" #include "parser/smt/generated/SmtParser.h" @@ -25,20 +26,9 @@ namespace CVC4 { namespace parser { /* Use lookahead=2 */ -SmtInput::SmtInput(ExprManager* exprManager, const std::string& filename, - bool useMmap) : - AntlrInput(exprManager, filename, 2, useMmap) { - init(); -} - -SmtInput::SmtInput(ExprManager* exprManager, const std::string& input, - const std::string& name) : - AntlrInput(exprManager, input, name, 2) { - init(); -} - -void SmtInput::init() { - pANTLR3_INPUT_STREAM input = getInputStream(); +SmtInput::SmtInput(AntlrInputStream *inputStream) : + Input(inputStream, 2) { + pANTLR3_INPUT_STREAM input = inputStream->getAntlr3InputStream(); AlwaysAssert( input != NULL ); d_pSmtLexer = SmtLexerNew(input); @@ -46,7 +36,7 @@ void SmtInput::init() { throw ParserException("Failed to create SMT lexer."); } - setLexer( d_pSmtLexer->pLexer ); + setAntlr3Lexer( d_pSmtLexer->pLexer ); pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream(); AlwaysAssert( tokenStream != NULL ); @@ -56,7 +46,7 @@ void SmtInput::init() { throw ParserException("Failed to create SMT parser."); } - setParser(d_pSmtParser->pParser); + setAntlr3Parser(d_pSmtParser->pParser); } @@ -65,11 +55,11 @@ SmtInput::~SmtInput() { d_pSmtParser->free(d_pSmtParser); } -Command* SmtInput::doParseCommand() throw (ParserException) { +Command* SmtInput::parseCommand() throw (ParserException) { return d_pSmtParser->parseCommand(d_pSmtParser); } -Expr SmtInput::doParseExpr() throw (ParserException) { +Expr SmtInput::parseExpr() throw (ParserException) { return d_pSmtParser->parseExpr(d_pSmtParser); } diff --git a/src/parser/smt/smt_input.h b/src/parser/smt/smt_input.h index f93a1bf0d..e9f4d2578 100644 --- a/src/parser/smt/smt_input.h +++ b/src/parser/smt/smt_input.h @@ -18,7 +18,7 @@ #ifndef __CVC4__PARSER__SMT_INPUT_H #define __CVC4__PARSER__SMT_INPUT_H -#include "parser/antlr_input.h" +#include "parser/input.h" #include "parser/smt/generated/SmtLexer.h" #include "parser/smt/generated/SmtParser.h" @@ -32,7 +32,7 @@ class ExprManager; namespace parser { -class SmtInput : public AntlrInput { +class SmtInput : public Input { /** The ANTLR3 SMT lexer for the input. */ pSmtLexer d_pSmtLexer; @@ -43,14 +43,11 @@ class SmtInput : public AntlrInput { public: /** - * Create a file input. + * Create an input. * - * @param exprManager the manager to use when building expressions from the input - * @param filename the path of the file to read - * @param useMmap true if the input should use memory-mapped - * I/O; otherwise, the input will use the standard ANTLR3 I/O implementation. + * @param inputStream the input stream to use */ - SmtInput(ExprManager* exprManager, const std::string& filename, bool useMmap); + SmtInput(AntlrInputStream *inputStream); /** * Create a string input. @@ -59,7 +56,7 @@ public: * @param input the string to read * @param name the "filename" to use when reporting errors */ - SmtInput(ExprManager* exprManager, const std::string& input, const std::string& name); +// SmtInput(ExprManager* exprManager, const std::string& input, const std::string& name); /** Destructor. Frees the lexer and the parser. */ ~SmtInput(); @@ -72,7 +69,7 @@ protected: * * @throws ParserException if an error is encountered during parsing. */ - Command* doParseCommand() throw(ParserException); + Command* parseCommand() throw(ParserException); /** * Parse an expression from the input. Returns a null @@ -80,7 +77,7 @@ protected: * * @throws ParserException if an error is encountered during parsing. */ - Expr doParseExpr() throw(ParserException); + Expr parseExpr() throw(ParserException); private: -- cgit v1.2.3