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
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
|
/*
* antlr_parser.h
*
* Created on: Nov 30, 2009
* Author: dejan
*/
#ifndef CVC4_PARSER_H_
#define CVC4_PARSER_H_
#include <vector>
#include <string>
#include <iostream>
#include <antlr/LLkParser.hpp>
#include <antlr/SemanticException.hpp>
#include "expr/expr.h"
#include "expr/expr_manager.h"
#include "util/command.h"
#include "util/assert.h"
#include "parser/symbol_table.h"
namespace CVC4 {
namespace parser {
/**
* Wrapper of the ANTLR parser that includes convenience methods that interacts
* with the expression manager. The grammars should have as little C++ code as
* possible and all the state and actuall functionality (besides parsing) should
* go into this class.
*/
class AntlrParser : public antlr::LLkParser {
public:
/** The status an SMT benchmark can have */
enum BenchmarkStatus {
/** Benchmark is satisfiable */
SMT_SATISFIABLE,
/** Benchmark is unsatisfiable */
SMT_UNSATISFIABLE,
/** The status of the benchmark is unknown */
SMT_UNKNOWN
};
/**
* Set's the expression manager to use when creating/managing expression.
* @param expr_manager the expression manager
*/
void setExpressionManager(ExprManager* expr_manager);
protected:
/**
* Class constructor, just tunnels the construction to the antlr
* LLkParser class.
*
* @param state the shared input state
* @param k lookahead
*/
AntlrParser(const antlr::ParserSharedInputState& state, int k);
/**
* Class constructor, just tunnels the construction to the antlr
* LLkParser class.
*
* @param tokenBuf the token buffer to use in parsing
* @param k lookahead
*/
AntlrParser(antlr::TokenBuffer& tokenBuf, int k);
/**
* Class constructor, just tunnels the construction to the antlr
* LLkParser class.
*
* @param lexer the lexer to use in parsing
* @param k lookahead
*/
AntlrParser(antlr::TokenStream& lexer, int k);
/**
* Renames the antlr semantic expression to a given message.
*/
void rethrow(antlr::SemanticException& e, std::string msg) throw (antlr::SemanticException);
/**
* Returns a variable, given a name and a type.
* @param var_name the name of the variable
* @return the variable expression
*/
Expr getVariable(std::string var_name);
/**
* Types of symbols.
*/
enum SymbolType {
/** Variables */
SYM_VARIABLE,
/** Predicates */
SYM_PREDICATE,
/** Functions */
SYM_FUNCTION
};
/**
* Checks if the variable has been declared.
* @param the variable name
*/
bool isDeclared(std::string var_name, SymbolType type = SYM_VARIABLE);
/**
* Returns the true expression.
* @return the true expression
*/
Expr getTrueExpr() const;
/**
* Returns the false expression.
* @return the false expression
*/
Expr getFalseExpr() const;
/**
* Creates a new unary CVC4 expression using the expression manager.
* @param kind the kind of the expression
* @param child the child
*/
Expr newExpression(Kind kind, const Expr& child);
/**
* Creates a new binary CVC4 expression using the expression manager.
* @param kind the kind of the expression
* @param children the children of the expression
*/
Expr newExpression(Kind kind, const Expr& child_1, const Expr& child_2);
/**
* Creates a new CVC4 expression using the expression manager.
* @param kind the kind of the expression
* @param children the children of the expression
*/
Expr newExpression(Kind kind, const std::vector<Expr>& children);
/**
* Creates a new expression based on the given string of expressions and kinds.
* The expression is created so that it respects the kinds precedence table.
*/
Expr createPrecedenceExpr(const std::vector<Expr>& exprs, const std::vector<Kind>& kinds);
/**
* Creates a new predicated over the given sorts.
* @param p_name the name of the predicate
* @param p_sorts the arity sorts
*/
void newPredicate(std::string p_name, const std::vector<std::string>& p_sorts);
/**
* Creates new predicates of given types.
* @param p_names the names of the predicates
*/
void newPredicates(const std::vector<std::string>& p_names);
/**
* Sets the status of the benchmark.
* @param status the status of the benchmark
*/
void setBenchmarkStatus(BenchmarkStatus status);
/**
* Returns the status of the parsed benchmark.
* @return the status of the parsed banchmark
*/
BenchmarkStatus getBenchmarkStatus() const;
/**
* Adds the extra sorts to the signature of the benchmark.
* @param extra_sorts the sorts to add
*/
void addExtraSorts(const std::vector<std::string>& extra_sorts);
/**
* Returns the precedence rank of the kind.
*/
static unsigned getPrecedence(Kind kind);
private:
unsigned findPivot(const std::vector<Kind>& kinds, unsigned start_index, unsigned end_index) const;
/**
* Creates a new expression based on the given string of expressions and kinds.
* The expression is created so that it respects the kinds precedence table.
*/
Expr createPrecedenceExpr(const std::vector<Expr>& exprs, const std::vector<Kind>& kinds, unsigned start_index, unsigned end_index);
/** The status of the benchmark */
BenchmarkStatus d_benchmark_status;
/** The expression manager */
ExprManager* d_expr_manager;
/** The symbol table lookup */
SymbolTable<Expr> d_var_symbol_table;
};
std::ostream& operator<<(std::ostream& out, AntlrParser::BenchmarkStatus status);
}/* CVC4::parser namespace */
}/* CVC4 namespace */
#endif /* CVC4_PARSER_H_ */
|
