1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
|
header "post_include_hpp" {
#include "parser/antlr_parser.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;
vector<string> ids;
}
: 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(); }
| identifierList[ids, CHECK_UNDECLARED] COLON type {
// [chris 12/15/2009] FIXME: decls may not be BOOLEAN
newPredicates(ids);
cmd = new DeclarationCommand(ids);
}
SEMICOLON
| EOF
;
/**
* 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
*/
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] returns [std::string id]
: x:IDENTIFIER { checkDeclation(x->getText(), check) }?
{
id = x->getText();
}
exception catch [antlr::SemanticException& ex] {
switch (check) {
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
*/
type
: BOOLEAN
;
/**
* Matches a CVC4 formula.
* @return the expression representing the formula
*/
formula returns [CVC4::Expr formula]
: formula = boolFormula
;
/**
* Matches a CVC4 basic Boolean formula (AND, OR, NOT...). It parses the list of
* operands (primaryBoolFormulas) and operators (Kinds) and then calls the
* 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]
{
vector<Expr> formulas;
vector<Kind> kinds;
Expr f;
Kind k;
}
: f = primaryBoolFormula { formulas.push_back(f); }
( k = boolOperator { kinds.push_back(k); } f = primaryBoolFormula { formulas.push_back(f); } )*
{
// Create the expression based on precedences
formula = createPrecedenceExpr(formulas, kinds);
}
;
/**
* 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
*/
primaryBoolFormula returns [CVC4::Expr formula]
: formula = boolAtom
| NOT formula = primaryBoolFormula { formula = mkExpr(CVC4::NOT, formula); }
| LPAREN formula = boolFormula RPAREN
;
/**
* Parses the Boolean operators and returns the corresponding CVC4 expression
* kind.
* @param the kind of the Boolean operator
*/
boolOperator returns [CVC4::Kind kind]
: IMPLIES { kind = CVC4::IMPLIES; }
| AND { kind = CVC4::AND; }
| OR { kind = CVC4::OR; }
| XOR { kind = CVC4::XOR; }
| IFF { kind = CVC4::IFF; }
;
/**
* Parses the Boolean atoms (variables and predicates).
* @return the expression representing the atom.
*/
boolAtom returns [CVC4::Expr atom]
{
string p;
}
: p = predicateSymbol[CHECK_DECLARED] { atom = getVariable(p); }
exception catch [antlr::SemanticException ex] {
rethrow(ex, "Undeclared variable " + p);
}
| TRUE { atom = getTrueExpr(); }
| FALSE { atom = getFalseExpr(); }
;
/**
* Parses a predicate symbol (an identifier).
* @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]
;
|
