diff options
Diffstat (limited to 'src/parser/cvc')
-rw-r--r-- | src/parser/cvc/.gitignore | 4 | ||||
-rw-r--r-- | src/parser/cvc/Cvc.g | 496 | ||||
-rw-r--r-- | src/parser/cvc/Makefile.am | 46 | ||||
-rw-r--r-- | src/parser/cvc/cvc_input.cpp | 73 | ||||
-rw-r--r-- | src/parser/cvc/cvc_input.h | 48 | ||||
-rw-r--r-- | src/parser/cvc/cvc_lexer.g | 151 | ||||
-rw-r--r-- | src/parser/cvc/cvc_parser.g | 386 |
7 files changed, 643 insertions, 561 deletions
diff --git a/src/parser/cvc/.gitignore b/src/parser/cvc/.gitignore new file mode 100644 index 000000000..7fd0cf319 --- /dev/null +++ b/src/parser/cvc/.gitignore @@ -0,0 +1,4 @@ +/.deps +/stamp-generated +/generated +/Makefile.in diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g new file mode 100644 index 000000000..a9dff77bf --- /dev/null +++ b/src/parser/cvc/Cvc.g @@ -0,0 +1,496 @@ +/* ******************* */ +/* Cvc.g + ** Original author: cconway + ** Major contributors: dejan, mdeters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** Parser for CVC-LIB input language. + **/ + +grammar Cvc; + +options { + language = 'C'; // C output for antlr +// defaultErrorHandler = false; // Skip the default error handling, just break with exceptions + k = 2; +} + +@header { +/** + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + **/ +} + +@lexer::includes { +/* This improves performance by ~10 percent on big inputs. + * This option is only valid if we know the input is ASCII (or some 8-bit encoding). + * If we know the input is UTF-16, we can use ANTLR3_INLINE_INPUT_UTF16. + * Otherwise, we have to let the lexer detect the encoding at runtime. + */ +#define ANTLR3_INLINE_INPUT_ASCII +} + +@parser::includes { +#include "expr/command.h" +#include "parser/input.h" + +namespace CVC4 { + class Expr; +namespace parser { + class CvcInput; +} +} + +extern +void SetCvcInput(CVC4::parser::CvcInput* input); + +} + +@parser::postinclude { +#include "expr/expr.h" +#include "expr/kind.h" +#include "expr/type.h" +#include "parser/input.h" +#include "parser/cvc/cvc_input.h" +#include "util/output.h" +#include <vector> + +using namespace CVC4; +using namespace CVC4::parser; +} + +@members { +static CVC4::parser::CvcInput *input; + +extern +void SetCvcInput(CVC4::parser::CvcInput* _input) { + input = _input; +} +} + +/** + * Parses an expression. + * @return the parsed expression + */ +parseExpr returns [CVC4::Expr expr] + : formula[expr] + | EOF + ; + +/** + * Parses a command (the whole benchmark) + * @return the command of the benchmark + */ +parseCommand returns [CVC4::Command* cmd] + : c = command { $cmd = c; } + ; + +/** + * Matches a command of the input. If a declaration, it will return an empty + * command. + */ +command returns [CVC4::Command* cmd = 0] +@init { + Expr f; + 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); } + | CHECKSAT_TOK formula[f] SEMICOLON { cmd = new CheckSatCommand(f); } + | CHECKSAT_TOK SEMICOLON { cmd = new CheckSatCommand(input->getTrueExpr()); } + | PUSH_TOK SEMICOLON { cmd = new PushCommand(); } + | POP_TOK SEMICOLON { cmd = new PopCommand(); } + | declaration[cmd] + | EOF + ; + +/** + * Match a declaration + */ + +declaration[CVC4::Command*& cmd] +@init { + std::vector<std::string> ids; + Type* t; + 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 + { cmd = new DeclarationCommand(ids,t); } + ; + +/** 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: " << AntlrInput::tokenText(LT(1)) << std::endl; +} + : /* A sort declaration (e.g., "T : TYPE") */ + TYPE_TOK { input->newSorts(idList); t = input->kindType(); } + | /* A variable declaration */ + type[t] { input->mkVars(idList,t); } + ; + +/** + * Match the type in a declaration and do the declaration binding. + * TODO: Actually parse sorts into Type objects. + */ +type[CVC4::Type*& t] +@init { + std::vector<Type*> typeList; + Debug("parser-extra") << "type: " << AntlrInput::tokenText(LT(1)) << std::endl; +} + : /* Simple type */ + baseType[t] + | /* Single-parameter function type */ + baseType[t] { typeList.push_back(t); } + ARROW_TOK baseType[t] + { t = input->functionType(typeList,t); } + | /* Multi-parameter function type */ + LPAREN baseType[t] + { typeList.push_back(t); } + (COMMA baseType[t] { typeList.push_back(t); } )+ + RPAREN ARROW_TOK baseType[t] + { t = input->functionType(typeList,t); } + ; + +/** + * Matches a list of identifiers separated by a comma and puts them in the + * given list. + * @param idList the list to fill with identifiers. + * @param check what kinds of check to perform on the symbols + */ +identifierList[std::vector<std::string>& idList, + CVC4::parser::DeclarationCheck check, + CVC4::parser::SymbolType type] +@init { + std::string id; +} + : identifier[id,check,type] { idList.push_back(id); } + (COMMA identifier[id,check,type] { idList.push_back(id); })* + ; + + +/** + * Matches an identifier and returns a string. + */ +identifier[std::string& id, + CVC4::parser::DeclarationCheck check, + CVC4::parser::SymbolType type] + : IDENTIFIER + { id = AntlrInput::tokenText($IDENTIFIER); + input->checkDeclaration(id, check, type); } + ; + +/** + * Matches a type. + * TODO: parse more types + */ +baseType[CVC4::Type*& t] +@init { + std::string id; + Debug("parser-extra") << "base type: " << AntlrInput::tokenText(LT(1)) << std::endl; +} + : BOOLEAN_TOK { t = input->booleanType(); } + | typeSymbol[t] + ; + +/** + * Matches a type identifier + */ +typeSymbol[CVC4::Type*& t] +@init { + std::string id; + Debug("parser-extra") << "type symbol: " << AntlrInput::tokenText(LT(1)) << std::endl; +} + : identifier[id,CHECK_DECLARED,SYM_SORT] + { t = input->getSort(id); } + ; + +/** + * Matches a CVC4 formula. + * @return the expression representing the formula + */ +formula[CVC4::Expr& formula] +@init { + Debug("parser-extra") << "formula: " << AntlrInput::tokenText(LT(1)) << std::endl; +} + : iffFormula[formula] + ; + +/** + * Matches a comma-separated list of formulas + */ +formulaList[std::vector<CVC4::Expr>& formulas] +@init { + Expr f; +} + : formula[f] { formulas.push_back(f); } + ( COMMA formula[f] + { formulas.push_back(f); } + )* + ; + +/** + * Matches a Boolean IFF formula (right-associative) + */ +iffFormula[CVC4::Expr& f] +@init { + Expr e; + Debug("parser-extra") << "<=> formula: " << AntlrInput::tokenText(LT(1)) << std::endl; +} + : impliesFormula[f] + ( IFF_TOK + iffFormula[e] + { f = input->mkExpr(CVC4::kind::IFF, f, e); } + )? + ; + +/** + * Matches a Boolean IMPLIES formula (right-associative) + */ +impliesFormula[CVC4::Expr& f] +@init { + Expr e; + Debug("parser-extra") << "=> Formula: " << AntlrInput::tokenText(LT(1)) << std::endl; +} + : orFormula[f] + ( IMPLIES_TOK impliesFormula[e] + { f = input->mkExpr(CVC4::kind::IMPLIES, f, e); } + )? + ; + +/** + * Matches a Boolean OR formula (left-associative) + */ +orFormula[CVC4::Expr& f] +@init { + std::vector<Expr> exprs; + Debug("parser-extra") << "OR Formula: " << AntlrInput::tokenText(LT(1)) << std::endl; +} + : xorFormula[f] + ( OR_TOK { exprs.push_back(f); } + xorFormula[f] { exprs.push_back(f); } )* + { + if( exprs.size() > 0 ) { + f = input->mkExpr(CVC4::kind::OR, exprs); + } + } + ; + +/** + * Matches a Boolean XOR formula (left-associative) + */ +xorFormula[CVC4::Expr& f] +@init { + Expr e; + Debug("parser-extra") << "XOR formula: " << AntlrInput::tokenText(LT(1)) << std::endl; +} + : andFormula[f] + ( XOR_TOK andFormula[e] + { f = input->mkExpr(CVC4::kind::XOR,f, e); } + )* + ; + +/** + * Matches a Boolean AND formula (left-associative) + */ +andFormula[CVC4::Expr& f] +@init { + std::vector<Expr> exprs; + Debug("parser-extra") << "AND Formula: " << AntlrInput::tokenText(LT(1)) << std::endl; +} + : notFormula[f] + ( AND_TOK { exprs.push_back(f); } + notFormula[f] { exprs.push_back(f); } )* + { + if( exprs.size() > 0 ) { + f = input->mkExpr(CVC4::kind::AND, exprs); + } + } + ; + +/** + * Parses a NOT formula. + * @return the expression representing the formula + */ +notFormula[CVC4::Expr& f] +@init { + Debug("parser-extra") << "NOT formula: " << AntlrInput::tokenText(LT(1)) << std::endl; +} + : /* negation */ + NOT_TOK notFormula[f] + { f = input->mkExpr(CVC4::kind::NOT, f); } + | /* a boolean atom */ + predFormula[f] + ; + +predFormula[CVC4::Expr& f] +@init { + Expr e; + Debug("parser-extra") << "predicate formula: " << AntlrInput::tokenText(LT(1)) << std::endl; +} + : term[f] + (EQUAL_TOK term[e] + { f = input->mkExpr(CVC4::kind::EQUAL, f, e); } + )? + ; // TODO: lt, gt, etc. + +/** + * Parses a term. + */ +term[CVC4::Expr& f] +@init { + std::string name; + std::vector<Expr> args; + Debug("parser-extra") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl; +} + : /* function application */ + // { isFunction(AntlrInput::tokenText(LT(1))) }? + functionSymbol[f] + { args.push_back( f ); } + LPAREN formulaList[args] RPAREN + // TODO: check arity + { f = input->mkExpr(CVC4::kind::APPLY_UF, args); } + + | /* if-then-else */ + iteTerm[f] + + | /* parenthesized sub-formula */ + LPAREN formula[f] RPAREN + + /* constants */ + | TRUE_TOK { f = input->getTrueExpr(); } + | FALSE_TOK { f = input->getFalseExpr(); } + + | /* variable */ + identifier[name,CHECK_DECLARED,SYM_VARIABLE] + { f = input->getVariable(name); } + ; + +/** + * Parses an ITE term. + */ +iteTerm[CVC4::Expr& f] +@init { + std::vector<Expr> args; + 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[f] { args.push_back(f); } + ENDIF_TOK + { f = input->mkExpr(CVC4::kind::ITE, args); } + ; + +/** + * Parses the else part of the ITE, i.e. ELSE f, or ELSIF b THEN f1 ... + */ +iteElseTerm[CVC4::Expr& f] +@init { + std::vector<Expr> args; + Debug("parser-extra") << "else: " << AntlrInput::tokenText(LT(1)) << std::endl; +} + : ELSE_TOK formula[f] + | ELSEIF_TOK iteCondition = formula[f] { args.push_back(f); } + THEN_TOK iteThen = formula[f] { args.push_back(f); } + iteElse = iteElseTerm[f] { args.push_back(f); } + { f = input->mkExpr(CVC4::kind::ITE, args); } + ; + +/** + * Parses a function symbol (an identifier). + * @param what kind of check to perform on the id + * @return the predicate symol + */ +functionSymbol[CVC4::Expr& f] +@init { + Debug("parser-extra") << "function symbol: " << AntlrInput::tokenText(LT(1)) << std::endl; + std::string name; +} + : identifier[name,CHECK_DECLARED,SYM_FUNCTION] + { input->checkFunction(name); + f = input->getFunction(name); } + ; + + +// Keywords + +AND_TOK : 'AND'; +ASSERT_TOK : 'ASSERT'; +BOOLEAN_TOK : 'BOOLEAN'; +CHECKSAT_TOK : 'CHECKSAT'; +ECHO_TOK : 'ECHO'; +ELSEIF_TOK : 'ELSIF'; +ELSE_TOK : 'ELSE'; +ENDIF_TOK : 'ENDIF'; +FALSE_TOK : 'FALSE'; +IF_TOK : 'IF'; +NOT_TOK : 'NOT'; +OR_TOK : 'OR'; +POPTO_TOK : 'POPTO'; +POP_TOK : 'POP'; +PRINT_TOK : 'PRINT'; +PUSH_TOK : 'PUSH'; +QUERY_TOK : 'QUERY'; +THEN_TOK : 'THEN'; +TRUE_TOK : 'TRUE'; +TYPE_TOK : 'TYPE'; +XOR_TOK : 'XOR'; + +// Symbols + +COLON : ':'; +COMMA : ','; +LPAREN : '('; +RPAREN : ')'; +SEMICOLON : ';'; + +// Operators + +IMPLIES_TOK : '=>'; +IFF_TOK : '<=>'; +ARROW_TOK : '->'; +EQUAL_TOK : '='; + +/** + * Matches an identifier from the input. An identifier is a sequence of letters, + * digits and "_", "'", "." symbols, starting with a letter. + */ +IDENTIFIER : ALPHA (ALPHA | DIGIT | '_' | '\'' | '.')*; + +/** + * Matches a numeral from the input (non-empty sequence of digits). + */ +NUMERAL: (DIGIT)+; + +/** + * Matches any letter ('a'-'z' and 'A'-'Z'). + */ +fragment ALPHA : 'a'..'z' | 'A'..'Z'; + +/** + * Matches the digits (0-9) + */ +fragment DIGIT : '0'..'9'; + +/** + * Matches and skips whitespace in the input and ignores it. + */ +WHITESPACE : (' ' | '\t' | '\f' | '\r' | '\n') { $channel = HIDDEN;; }; + +/** + * Matches the comments and ignores them + */ +COMMENT : '%' (~('\n' | '\r'))* { $channel = HIDDEN;; }; + diff --git a/src/parser/cvc/Makefile.am b/src/parser/cvc/Makefile.am index c1b5f752e..f02c9345c 100644 --- a/src/parser/cvc/Makefile.am +++ b/src/parser/cvc/Makefile.am @@ -1,30 +1,30 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4PARSERLIB \ - -I@srcdir@/../../include -I@srcdir@/../.. + -I@srcdir@/../../include -I@srcdir@/../.. $(ANTLR_INCLUDES) AM_CXXFLAGS = -Wall -fvisibility=hidden +# Compile generated C files using C++ compiler +CC=$(CXX) noinst_LTLIBRARIES = libparsercvc.la ANTLR_TOKEN_STUFF = \ - @srcdir@/generated/CvcVocabularyTokenTypes.hpp \ - @srcdir@/generated/CvcVocabularyTokenTypes.txt \ - @srcdir@/generated/AntlrCvcParserTokenTypes.hpp \ - @srcdir@/generated/AntlrCvcParserTokenTypes.txt + @srcdir@/generated/Cvc.tokens ANTLR_LEXER_STUFF = \ - @srcdir@/generated/AntlrCvcLexer.hpp \ - @srcdir@/generated/AntlrCvcLexer.cpp \ - $(ANTLR_TOKEN_STUFF) + @srcdir@/generated/CvcLexer.h \ + @srcdir@/generated/CvcLexer.c \ + $(ANTLR_TOKEN_STUFF) ANTLR_PARSER_STUFF = \ - @srcdir@/generated/AntlrCvcParser.hpp \ - @srcdir@/generated/AntlrCvcParser.cpp + @srcdir@/generated/CvcParser.h \ + @srcdir@/generated/CvcParser.c ANTLR_STUFF = \ - $(ANTLR_LEXER_STUFF) \ - $(ANTLR_PARSER_STUFF) + $(ANTLR_LEXER_STUFF) \ + $(ANTLR_PARSER_STUFF) libparsercvc_la_SOURCES = \ - cvc_lexer.g \ - cvc_parser.g \ - $(ANTLR_STUFF) + Cvc.g \ + cvc_input.h \ + cvc_input.cpp \ + $(ANTLR_STUFF) BUILT_SOURCES = $(ANTLR_STUFF) dist-hook: $(ANTLR_STUFF) @@ -36,16 +36,14 @@ maintainer-clean-local: @srcdir@/stamp-generated: mkdir -p @srcdir@/generated touch @srcdir@/stamp-generated + # antlr doesn't overwrite output files, it just leaves them. So we have to delete them first. -@srcdir@/generated/AntlrCvcLexer.hpp: cvc_lexer.g @srcdir@/stamp-generated - $(AM_V_at)-rm -f $(ANTLR_LEXER_STUFF) - $(AM_V_GEN)$(ANTLR) -o "@srcdir@/generated" "@srcdir@/cvc_lexer.g" -@srcdir@/generated/AntlrCvcLexer.cpp $(ANTLR_TOKEN_STUFF): @srcdir@/generated/AntlrCvcLexer.hpp -# doesn't actually depend on the lexer, but if we're doing parallel +@srcdir@/generated/CvcLexer.h: Cvc.g @srcdir@/stamp-generated + -rm -f $(ANTLR_STUFF) + $(ANTLR) -o "@srcdir@/generated" "@srcdir@/Cvc.g" + +# These don't actually depend on CvcLexer.h, but if we're doing parallel # make and the lexer needs to be rebuilt, we have to keep the rules # from running in parallel (since the token files will be deleted & # recreated) -@srcdir@/generated/AntlrCvcParser.hpp: cvc_parser.g cvc_lexer.g $(ANTLR_TOKEN_STUFF) @srcdir@/stamp-generated - $(AM_V_at)-rm -f $(ANTLR_PARSER_STUFF) - $(AM_V_GEN)$(ANTLR) -o "@srcdir@/generated" "@srcdir@/cvc_parser.g" -@srcdir@/generated/AntlrCvcParser.cpp: @srcdir@/generated/AntlrCvcParser.hpp +@srcdir@/generated/CvcLexer.c @srcdir@/generated/CvcParser.h @srcdir@/generated/CvcParser.c $(ANTLR_TOKEN_STUFF): @srcdir@/generated/CvcLexer.h diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp new file mode 100644 index 000000000..9de608aae --- /dev/null +++ b/src/parser/cvc/cvc_input.cpp @@ -0,0 +1,73 @@ +/* + * cvc_parser.cpp + * + * Created on: Mar 5, 2010 + * Author: chris + */ + +#include <antlr3.h> + +#include "expr/expr_manager.h" +#include "parser/parser_exception.h" +#include "parser/cvc/cvc_input.h" +#include "parser/cvc/generated/CvcLexer.h" +#include "parser/cvc/generated/CvcParser.h" + +namespace CVC4 { +namespace parser { + +/* Use lookahead=2 */ +CvcInput::CvcInput(ExprManager* exprManager, const std::string& filename, bool useMmap) : + AntlrInput(exprManager,filename,2,useMmap) { + init(); +} + +CvcInput::CvcInput(ExprManager* exprManager, const std::string& input, const std::string& name) : + AntlrInput(exprManager,input,name,2) { + init(); +} + +void CvcInput::init() { + pANTLR3_INPUT_STREAM input = getInputStream(); + AlwaysAssert( input != NULL ); + + d_pCvcLexer = CvcLexerNew(input); + if( d_pCvcLexer == NULL ) { + throw ParserException("Failed to create CVC lexer."); + } + + setLexer( d_pCvcLexer->pLexer ); + + pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream(); + AlwaysAssert( tokenStream != NULL ); + + d_pCvcParser = CvcParserNew(tokenStream); + if( d_pCvcParser == NULL ) { + throw ParserException("Failed to create CVC parser."); + } + + setParser(d_pCvcParser->pParser); + SetCvcInput(this); +} + + +CvcInput::~CvcInput() { + d_pCvcLexer->free(d_pCvcLexer); + d_pCvcParser->free(d_pCvcParser); +} + +Command* CvcInput::doParseCommand() throw (ParserException) { + return d_pCvcParser->parseCommand(d_pCvcParser); +} + +Expr CvcInput::doParseExpr() throw (ParserException) { + return d_pCvcParser->parseExpr(d_pCvcParser); +} + +pANTLR3_LEXER CvcInput::getLexer() { + return d_pCvcLexer->pLexer; +} + +} // namespace parser + +} // namespace CVC4 diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h new file mode 100644 index 000000000..659123401 --- /dev/null +++ b/src/parser/cvc/cvc_input.h @@ -0,0 +1,48 @@ +/* + * cvc_parser.h + * + * Created on: Mar 5, 2010 + * Author: chris + */ + +#ifndef CVC_PARSER_H_ +#define CVC_PARSER_H_ + +#include "parser/antlr_input.h" +#include "parser/cvc/generated/CvcLexer.h" +#include "parser/cvc/generated/CvcParser.h" + +// extern void CvcParserSetAntlrParser(CVC4::parser::AntlrParser* newAntlrParser); + +namespace CVC4 { + +class Command; +class Expr; +class ExprManager; + +namespace parser { + +class CvcInput : public AntlrInput { +public: + CvcInput(ExprManager* exprManager, const std::string& filename, bool useMmap); + CvcInput(ExprManager* exprManager, const std::string& input, const std::string& name); + ~CvcInput(); + +protected: + Command* doParseCommand() throw(ParserException); + Expr doParseExpr() throw(ParserException); + pANTLR3_LEXER getLexer(); + pANTLR3_LEXER createLexer(pANTLR3_INPUT_STREAM input); + pANTLR3_PARSER createParser(pANTLR3_COMMON_TOKEN_STREAM tokenStream); + +private: + void init(); + pCvcLexer d_pCvcLexer; + pCvcParser d_pCvcParser; +}; // class CvcInput + +} // namespace parser + +} // namespace CVC4 + +#endif /* CVC_PARSER_H_ */ diff --git a/src/parser/cvc/cvc_lexer.g b/src/parser/cvc/cvc_lexer.g deleted file mode 100644 index b5bf90015..000000000 --- a/src/parser/cvc/cvc_lexer.g +++ /dev/null @@ -1,151 +0,0 @@ -/* ******************* */ -/* cvc_lexer.g - ** Original author: dejan - ** Major contributors: mdeters - ** Minor contributors (to current version): cconway - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information. - ** - ** Lexer for CVC presentation language. - **/ - -options { - language = "Cpp"; // C++ output for antlr - namespaceStd = "std"; // Cosmetic option to get rid of long defines in generated code - namespaceAntlr = "antlr"; // Cosmetic option to get rid of long defines in generated code - namespace = "CVC4::parser"; // Wrap everything in the smtparser namespace -} - -/** - * AntlrCvcLexer class is a stream tokenizer (lexer) for the CVC language. - */ -class AntlrCvcLexer extends Lexer; - -options { - exportVocab = CvcVocabulary; // Name of the shared token vocabulary - testLiterals = false; // Do not check for literals by default - defaultErrorHandler = false; // Skip the defaul error handling, just break with exceptions - k = 2; -} - -/* - * The tokens that might match with the identifiers go here. Otherwise define - * them below. - */ -tokens { - // Types - BOOLEAN = "BOOLEAN"; - TYPE = "TYPE"; - // Boolean oparators - AND = "AND"; - IF = "IF"; - THEN = "THEN"; - ELSE = "ELSE"; - ELSEIF = "ELSIF"; - ENDIF = "ENDIF"; - NOT = "NOT"; - OR = "OR"; - TRUE = "TRUE"; - FALSE = "FALSE"; - XOR = "XOR"; - // Commands - ASSERT = "ASSERT"; - QUERY = "QUERY"; - CHECKSAT = "CHECKSAT"; - PRINT = "PRINT"; - ECHO = "ECHO"; - - PUSH = "PUSH"; - POP = "POP"; - POPTO = "POPTO"; -} - -// Operators -COMMA : ','; -IMPLIES : "=>"; -IFF : "<=>"; -RIGHT_ARROW : "->"; -EQUAL : "="; - -/** - * Matches any letter ('a'-'z' and 'A'-'Z'). - */ -protected -ALPHA options { paraphrase = "a letter"; } - : 'a'..'z' - | 'A'..'Z' - ; - -/** - * Matches the digits (0-9) - */ -protected -DIGIT options { paraphrase = "a digit"; } - : '0'..'9' - ; - -/** - * Matches the ':' - */ -COLON options { paraphrase = "a colon"; } - : ':' - ; - -/** - * Matches the 'l' - */ -SEMICOLON options { paraphrase = "a semicolon"; } - : ';' - ; - -/** - * Matches an identifier from the input. An identifier is a sequence of letters, - * digits and "_", "'", "." symbols, starting with a letter. - */ -IDENTIFIER options { paraphrase = "an identifier"; testLiterals = true; } - : ALPHA (ALPHA | DIGIT | '_' | '\'' | '.')* - ; - -/** - * Matches the left bracket ('('). - */ -LPAREN options { paraphrase = "a left parenthesis '('"; } - : '('; - -/** - * Matches the right bracket ('('). - */ -RPAREN options { paraphrase = "a right parenthesis ')'"; } - : ')'; - -/** - * Matches and skips whitespace in the input and ignores it. - */ -WHITESPACE options { paraphrase = "whitespace"; } - : (' ' | '\t' | '\f') { $setType(antlr::Token::SKIP); } - ; - -/** - * Matches and skips the newline symbols in the input. - */ -NEWLINE options { paraphrase = "a newline"; } - : ('\r' '\n' | '\r' | '\n') { $setType(antlr::Token::SKIP); newline(); } - ; - -/** - * Matches the comments and ignores them - */ -COMMENT options { paraphrase = "comment"; } - : '%' (~('\n' | '\r'))* { $setType(antlr::Token::SKIP); } - ; - -/** - * Matches a numeral from the input (non-empty sequence of digits). - */ -NUMERAL options { paraphrase = "a numeral"; } - : (DIGIT)+ - ; diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g deleted file mode 100644 index acf0394d0..000000000 --- a/src/parser/cvc/cvc_parser.g +++ /dev/null @@ -1,386 +0,0 @@ -/* ******************* */ -/* cvc_parser.g - ** Original author: dejan - ** Major contributors: cconway - ** Minor contributors (to current version): mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information. - ** - ** Parser for CVC presentation language. - **/ - -header "post_include_hpp" { -#include "parser/antlr_parser.h" -#include "expr/command.h" -#include "expr/type.h" -#include "util/output.h" -} - -header "post_include_cpp" { -#include <vector> - -using namespace std; -using namespace CVC4; -using namespace CVC4::parser; -} - -options { - language = "Cpp"; // C++ output for antlr - namespaceStd = "std"; // Cosmetic option to get rid of long defines in generated code - namespaceAntlr = "antlr"; // Cosmetic option to get rid of long defines in generated code - namespace = "CVC4::parser"; // Wrap everything in the smtparser namespace -} - -/** - * AntlrCvcParser class is the parser for the files in CVC format. - */ -class AntlrCvcParser extends Parser("AntlrParser"); -options { - genHashLines = true; // Include line number information - importVocab = CvcVocabulary; // Import the common vocabulary - defaultErrorHandler = false; // Skip the defaul error handling, just break with exceptions - k = 2; -} - -/** - * Parses the next command. - * @return command or 0 if EOF - */ -parseCommand returns [CVC4::Command* cmd] - : cmd = command - ; - -/** - * Parses the next expression. - * @return the parsed expression (null expression if EOF) - */ -parseExpr returns [CVC4::Expr expr] - : expr = formula - | EOF - ; - -/** - * Matches a command of the input. If a declaration, it will return an empty - * command. - */ -command returns [CVC4::Command* cmd = 0] -{ - Expr f; - Debug("parser") << "command: " << LT(1)->getText() << endl; -} - : ASSERT f = formula SEMICOLON { cmd = new AssertCommand(f); } - | QUERY f = formula SEMICOLON { cmd = new QueryCommand(f); } - | CHECKSAT f = formula SEMICOLON { cmd = new CheckSatCommand(f); } - | CHECKSAT SEMICOLON { cmd = new CheckSatCommand(getTrueExpr()); } - | PUSH SEMICOLON { cmd = new PushCommand(); } - | POP SEMICOLON { cmd = new PopCommand(); } - | cmd = declaration - | EOF - ; - -/** - * Match a declaration - */ - -declaration returns [CVC4::DeclarationCommand* cmd] -{ - vector<string> ids; - Type* t; - Debug("parser") << "declaration: " << LT(1)->getText() << endl; -} - : identifierList[ids, CHECK_UNDECLARED] COLON t = declType[ids] SEMICOLON - { cmd = new DeclarationCommand(ids,t); } - ; - -/** Match the right-hand side of a declaration. Returns the type. */ -declType[std::vector<std::string>& idList] returns [CVC4::Type* t] -{ - Debug("parser") << "declType: " << LT(1)->getText() << endl; -} - : /* A sort declaration (e.g., "T : TYPE") */ - TYPE { newSorts(idList); t = kindType(); } - | /* A variable declaration */ - t = type { mkVars(idList,t); } - ; - -/** - * Match the type in a declaration and do the declaration binding. - * TODO: Actually parse sorts into Type objects. - */ -type returns [CVC4::Type* t] -{ - Type *t1, *t2; - Debug("parser") << "type: " << LT(1)->getText() << endl; -} - : /* Simple type */ - t = baseType - | /* Single-parameter function type */ - t1 = baseType RIGHT_ARROW t2 = baseType - { t = functionType(t1,t2); } - | /* Multi-parameter function type */ - LPAREN t1 = baseType - { std::vector<Type*> argTypes; - argTypes.push_back(t1); } - (COMMA t1 = baseType { argTypes.push_back(t1); } )+ - RPAREN RIGHT_ARROW t2 = baseType - { t = functionType(argTypes,t2); } - ; - -/** - * Matches a list of identifiers separated by a comma and puts them in the - * given list. - * @param idList the list to fill with identifiers. - * @param check what kinds of check to perform on the symbols - */ -identifierList[std::vector<std::string>& idList, - DeclarationCheck check = CHECK_NONE] -{ - string id; -} - : id = identifier[check] { idList.push_back(id); } - (COMMA id = identifier[check] { idList.push_back(id); })* - ; - - -/** - * Matches an identifier and returns a string. - */ -identifier[DeclarationCheck check = CHECK_NONE, - SymbolType type = SYM_VARIABLE] -returns [std::string id] - : x:IDENTIFIER - { id = x->getText(); - checkDeclaration(id, check, type); } - ; - -/** - * Matches a type. - * TODO: parse more types - */ -baseType returns [CVC4::Type* t] -{ - std::string id; - Debug("parser") << "base type: " << LT(1)->getText() << endl; -} - : BOOLEAN { t = booleanType(); } - | t = typeSymbol - ; - -/** - * Matches a type identifier - */ -typeSymbol returns [CVC4::Type* t] -{ - std::string id; - Debug("parser") << "type symbol: " << LT(1)->getText() << endl; -} - : id = identifier[CHECK_DECLARED,SYM_SORT] - { t = getSort(id); } - ; - -/** - * Matches a CVC4 formula. - * @return the expression representing the formula - */ -formula returns [CVC4::Expr formula] -{ - Debug("parser") << "formula: " << LT(1)->getText() << endl; -} - : formula = iffFormula - ; - -/** - * Matches a comma-separated list of formulas - */ -formulaList[std::vector<CVC4::Expr>& formulas] -{ - Expr f; -} - : f = formula { formulas.push_back(f); } - ( COMMA f = formula - { formulas.push_back(f); } - )* - ; - -/** - * Matches a Boolean IFF formula (right-associative) - */ -iffFormula returns [CVC4::Expr f] -{ - Expr e; - Debug("parser") << "<=> formula: " << LT(1)->getText() << endl; -} - : f = impliesFormula - ( IFF e = iffFormula - { f = mkExpr(CVC4::kind::IFF, f, e); } - )? - ; - -/** - * Matches a Boolean IMPLIES formula (right-associative) - */ -impliesFormula returns [CVC4::Expr f] -{ - Expr e; - Debug("parser") << "=> Formula: " << LT(1)->getText() << endl; -} - : f = orFormula - ( IMPLIES e = impliesFormula - { f = mkExpr(CVC4::kind::IMPLIES, f, e); } - )? - ; - -/** - * Matches a Boolean OR formula (left-associative) - */ -orFormula returns [CVC4::Expr f] -{ - Expr e; - vector<Expr> exprs; - Debug("parser") << "OR Formula: " << LT(1)->getText() << endl; -} - : e = xorFormula { exprs.push_back(e); } - ( OR e = xorFormula { exprs.push_back(e); } )* - { - f = (exprs.size() > 1 ? mkExpr(CVC4::kind::OR, exprs) : exprs[0]); - } - ; - -/** - * Matches a Boolean XOR formula (left-associative) - */ -xorFormula returns [CVC4::Expr f] -{ - Expr e; - Debug("parser") << "XOR formula: " << LT(1)->getText() << endl; -} - : f = andFormula - ( XOR e = andFormula - { f = mkExpr(CVC4::kind::XOR,f, e); } - )* - ; - -/** - * Matches a Boolean AND formula (left-associative) - */ -andFormula returns [CVC4::Expr f] -{ - Expr e; - vector<Expr> exprs; - Debug("parser") << "AND Formula: " << LT(1)->getText() << endl; -} - : e = notFormula { exprs.push_back(e); } - ( AND e = notFormula { exprs.push_back(e); } )* - { - f = (exprs.size() > 1 ? mkExpr(CVC4::kind::AND, exprs) : exprs[0]); - } - ; - -/** - * Parses a NOT formula. - * @return the expression representing the formula - */ -notFormula returns [CVC4::Expr f] -{ - Debug("parser") << "NOT formula: " << LT(1)->getText() << endl; -} - : /* negation */ - NOT f = notFormula - { f = mkExpr(CVC4::kind::NOT, f); } - | /* a boolean atom */ - f = predFormula - ; - -predFormula returns [CVC4::Expr f] -{ - Debug("parser") << "predicate formula: " << LT(1)->getText() << endl; -} - : { Expr e; } - f = term - (EQUAL e = term - { f = mkExpr(CVC4::kind::EQUAL, f, e); } - )? - ; // TODO: lt, gt, etc. - -/** - * Parses a term. - */ -term returns [CVC4::Expr t] -{ - std::string name; - Debug("parser") << "term: " << LT(1)->getText() << endl; -} - : /* function application */ - // { isFunction(LT(1)->getText()) }? - { Expr f; - std::vector<CVC4::Expr> args; } - f = functionSymbol[CHECK_DECLARED] - { args.push_back( f ); } - - LPAREN formulaList[args] RPAREN - // TODO: check arity - { t = mkExpr(CVC4::kind::APPLY_UF, args); } - - | /* if-then-else */ - t = iteTerm - - | /* parenthesized sub-formula */ - LPAREN t = formula RPAREN - - /* constants */ - | TRUE { t = getTrueExpr(); } - | FALSE { t = getFalseExpr(); } - - | /* variable */ - name = identifier[CHECK_DECLARED] - { t = getVariable(name); } - ; - -/** - * Parses an ITE term. - */ -iteTerm returns [CVC4::Expr t] -{ - Expr iteCondition, iteThen, iteElse; - Debug("parser") << "ite: " << LT(1)->getText() << endl; -} - : IF iteCondition = formula - THEN iteThen = formula - iteElse = iteElseTerm - ENDIF - { t = mkExpr(CVC4::kind::ITE, iteCondition, iteThen, iteElse); } - ; - -/** - * Parses the else part of the ITE, i.e. ELSE f, or ELSIF b THEN f1 ... - */ -iteElseTerm returns [CVC4::Expr t] -{ - Expr iteCondition, iteThen, iteElse; - Debug("parser") << "else: " << LT(1)->getText() << endl; -} - : ELSE t = formula - | ELSEIF iteCondition = formula - THEN iteThen = formula - iteElse = iteElseTerm - { t = mkExpr(CVC4::kind::ITE, iteCondition, iteThen, iteElse); } - ; - -/** - * Parses a function symbol (an identifier). - * @param what kind of check to perform on the id - * @return the predicate symol - */ -functionSymbol[DeclarationCheck check = CHECK_NONE] returns [CVC4::Expr f] -{ - Debug("parser") << "function symbol: " << LT(1)->getText() << endl; - std::string name; -} - : name = identifier[check,SYM_FUNCTION] - { checkFunction(name); - f = getFunction(name); } - ; |