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.g122
1 files changed, 68 insertions, 54 deletions
diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g
index eb21283a3..ce61deae2 100644
--- a/src/parser/cvc/cvc_parser.g
+++ b/src/parser/cvc/cvc_parser.g
@@ -1,24 +1,39 @@
+/* cvc_parser.g
+ * Original author: dejan
+ * Major contributors:
+ * Minor contributors (to current version): none
+ * This file is part of the CVC4 prototype.
+ * Copyright (c) 2009 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 "util/command.h"
}
header "post_include_cpp" {
-#include <vector>
+#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.
+ * AntlrCvcParser class is the parser for the files in CVC format.
*/
class AntlrCvcParser extends Parser("AntlrParser");
options {
@@ -27,7 +42,7 @@ options {
defaultErrorHandler = false; // Skip the defaul error handling, just break with exceptions
k = 2;
}
-
+
/**
* Parses the next command.
* @return command or 0 if EOF
@@ -44,9 +59,9 @@ parseExpr returns [CVC4::Expr expr]
: expr = formula
| EOF
;
-
+
/**
- * Matches a command of the input. If a declaration, it will return an empty
+ * Matches a command of the input. If a declaration, it will return an empty
* command.
*/
command returns [CVC4::Command* cmd = 0]
@@ -58,36 +73,36 @@ command returns [CVC4::Command* cmd = 0]
| QUERY f = formula SEMICOLON { cmd = new QueryCommand(f); }
| CHECKSAT f = formula SEMICOLON { cmd = new CheckSatCommand(f); }
| CHECKSAT SEMICOLON { cmd = new CheckSatCommand(); }
- | identifierList[ids, CHECK_UNDECLARED] COLON type {
+ | identifierList[ids, CHECK_UNDECLARED] COLON type {
// FIXME: switch on type (may not be predicates)
vector<string> sorts;
- newPredicates(ids,sorts);
- cmd = new DeclarationCommand(ids);
+ newPredicates(ids,sorts);
+ cmd = new DeclarationCommand(ids);
}
SEMICOLON
- | EOF
+ | EOF
;
/**
- * Mathches a list of identifiers separated by a comma and puts them in the
+ * Mathches 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
+ * @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); }
+ : 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] returns [std::string id]
- : x:IDENTIFIER
+ : x:IDENTIFIER
{ id = x->getText(); }
{ checkDeclaration(id, check) }?
exception catch [antlr::SemanticException& ex] {
@@ -95,11 +110,11 @@ identifier[DeclarationCheck check = CHECK_NONE] returns [std::string id]
case CHECK_DECLARED: rethrow(ex, "Symbol " + id + " not declared");
case CHECK_UNDECLARED: rethrow(ex, "Symbol " + id + " already declared");
default: throw ex;
- }
- }
+ }
+ }
;
-
-/**
+
+/**
* Matches a type.
* TODO: parse more types
*/
@@ -107,10 +122,10 @@ type
: BOOLEAN
;
-/**
+/**
* Matches a CVC4 formula.
* @return the expression representing the formula
- */
+ */
formula returns [CVC4::Expr formula]
: formula = boolFormula
;
@@ -121,69 +136,69 @@ formula returns [CVC4::Expr formula]
* createPrecedenceExpr method to build the expression using the precedence
* and associativity of the operators.
* @return the expression representing the formula
- */
+ */
boolFormula returns [CVC4::Expr formula]
- : formula = boolAndFormula
+ : formula = boolAndFormula
;
/**
- * Matches a Boolean AND formula of a given kind by doing a recursive descent.
+ * Matches a Boolean AND formula of a given kind by doing a recursive descent.
*/
boolAndFormula returns [CVC4::Expr andFormula]
{
Expr e;
vector<Expr> exprs;
}
- : e = boolXorFormula { exprs.push_back(e); }
+ : e = boolXorFormula { exprs.push_back(e); }
( AND e = boolXorFormula { exprs.push_back(e); } )*
- {
- andFormula = (exprs.size() > 1 ? mkExpr(CVC4::AND, exprs) : exprs[0]);
- }
+ {
+ andFormula = (exprs.size() > 1 ? mkExpr(CVC4::AND, exprs) : exprs[0]);
+ }
;
/**
- * Matches a Boolean XOR formula of a given kind by doing a recursive descent.
+ * Matches a Boolean XOR formula of a given kind by doing a recursive descent.
*/
boolXorFormula returns [CVC4::Expr xorFormula]
{
Expr e;
vector<Expr> exprs;
}
- : e = boolOrFormula { exprs.push_back(e); }
+ : e = boolOrFormula { exprs.push_back(e); }
( XOR e = boolOrFormula { exprs.push_back(e); } )*
- {
- xorFormula = (exprs.size() > 1 ? mkExpr(CVC4::XOR, exprs) : exprs[0]);
- }
+ {
+ xorFormula = (exprs.size() > 1 ? mkExpr(CVC4::XOR, exprs) : exprs[0]);
+ }
;
/**
- * Matches a Boolean OR formula of a given kind by doing a recursive descent.
+ * Matches a Boolean OR formula of a given kind by doing a recursive descent.
*/
boolOrFormula returns [CVC4::Expr orFormula]
{
Expr e;
vector<Expr> exprs;
}
- : e = boolImpliesFormula { exprs.push_back(e); }
+ : e = boolImpliesFormula { exprs.push_back(e); }
( OR e = boolImpliesFormula { exprs.push_back(e); } )*
- {
- orFormula = (exprs.size() > 1 ? mkExpr(CVC4::OR, exprs) : exprs[0]);
- }
+ {
+ orFormula = (exprs.size() > 1 ? mkExpr(CVC4::OR, exprs) : exprs[0]);
+ }
;
/**
- * Matches a Boolean IMPLIES formula of a given kind by doing a recursive descent.
+ * Matches a Boolean IMPLIES formula of a given kind by doing a recursive descent.
*/
boolImpliesFormula returns [CVC4::Expr impliesFormula]
{
vector<Expr> exprs;
Expr e;
}
- : e = boolIffFormula { exprs.push_back(e); }
- ( IMPLIES e = boolIffFormula { exprs.push_back(e); }
+ : e = boolIffFormula { exprs.push_back(e); }
+ ( IMPLIES e = boolIffFormula { exprs.push_back(e); }
)*
{
- impliesFormula = exprs.back();
+ impliesFormula = exprs.back();
for (int i = exprs.size() - 2; i >= 0; -- i) {
impliesFormula = mkExpr(CVC4::IMPLIES, exprs[i], impliesFormula);
}
@@ -191,21 +206,21 @@ boolImpliesFormula returns [CVC4::Expr impliesFormula]
;
/**
- * Matches a Boolean IFF formula of a given kind by doing a recursive descent.
+ * Matches a Boolean IFF formula of a given kind by doing a recursive descent.
*/
boolIffFormula returns [CVC4::Expr iffFormula]
{
Expr e;
}
- : iffFormula = primaryBoolFormula
- ( IFF e = primaryBoolFormula
- { iffFormula = mkExpr(CVC4::IFF, iffFormula, e); }
+ : iffFormula = primaryBoolFormula
+ ( IFF e = primaryBoolFormula
+ { iffFormula = mkExpr(CVC4::IFF, iffFormula, e); }
)*
;
-
+
/**
- * Parses a primary Boolean formula. A primary Boolean formula is either a
- * Boolean atom (variables and predicates) a negation of a primary Boolean
+ * Parses a primary Boolean formula. A primary Boolean formula is either a
+ * Boolean atom (variables and predicates) a negation of a primary Boolean
* formula or a formula enclosed in parenthesis.
* @return the expression representing the formula
*/
@@ -247,7 +262,7 @@ iteElseFormula returns [CVC4::Expr formula]
/**
* Parses the Boolean atoms (variables and predicates).
* @return the expression representing the atom.
- */
+ */
boolAtom returns [CVC4::Expr atom]
{
string p;
@@ -259,13 +274,12 @@ boolAtom returns [CVC4::Expr atom]
| TRUE { atom = getTrueExpr(); }
| FALSE { atom = getFalseExpr(); }
;
-
+
/**
* Parses a predicate symbol (an identifier).
- * @param what kind of check to perform on the id
+ * @param what kind of check to perform on the id
* @return the predicate symol
*/
predicateSymbol[DeclarationCheck check = CHECK_NONE] returns [std::string pSymbol]
: pSymbol = identifier[check]
;
-
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback