diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-03-30 20:22:33 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-03-30 20:22:33 +0000 |
commit | 8730e9320a833a9eb0e65074f9988950b7424c0c (patch) | |
tree | 1cb09404256743e208fece079ba473595e05edcd /src/parser/cvc/cvc_parser.g | |
parent | 8c87c05ac56a5f29b2ae1e658f2d7d3b7b588163 (diff) |
Merging from branches/antlr3 (r246:354)
Diffstat (limited to 'src/parser/cvc/cvc_parser.g')
-rw-r--r-- | src/parser/cvc/cvc_parser.g | 386 |
1 files changed, 0 insertions, 386 deletions
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); } - ; |