summaryrefslogtreecommitdiff
path: root/src/parser/cvc/cvc_parser.g
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser/cvc/cvc_parser.g')
-rw-r--r--src/parser/cvc/cvc_parser.g386
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); }
- ;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback