blob: b1aeaa57071a1c4391f8f2ae4e7c91295c391758 (
plain)
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
|
%{/********************* -*- C++ -*- */
/** smtlib.ypp
** 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.
**
** This file contains the bison code for the parser that reads in CVC
** commands in SMT-LIB language.
**/
#include "cvc4.h"
#include "parser_state.h"
// Exported shared data
namespace CVC4 {
namespace parser {
extern ParserState* _global_parser_state;
}
}
using namespace std;
using namespace CVC4;
using namespace CVC4::parser;
// Suppress the bogus warning suppression in bison (it generates compile error)
#undef __GNUC_MINOR__
/** stuff that lives in smtlib_scanner.lpp */
extern int smtliblex(void);
/** Error call */
int smtliberror(const char *s) { return _global_parser_state->parseError(s); }
#define YYLTYPE_IS_TRIVIAL 1
#define YYMAXDEPTH 10485760
%}
%union {
std::string *p_string;
std::vector<std::string> *p_string_vector;
CVC4::Expr *p_expression;
std::vector<CVC4::Expr> *p_expression_vector;
CVC4::Command *p_command;
CVC4::CommandSequence *p_command_sequence;
CVC4::parser::ParserState::BenchmarkStatus d_bench_status;
CVC4::Kind d_kind;
};
%token <p_string> NUMERAL_TOK
%token <p_string> SYM_TOK
%token <p_string> STRING_TOK
%token <p_string> USER_VAL_TOK
%token TRUE_TOK
%token FALSE_TOK
%token ITE_TOK
%token NOT_TOK
%token IMPLIES_TOK
%token IF_THEN_ELSE_TOK
%token AND_TOK
%token OR_TOK
%token XOR_TOK
%token IFF_TOK
%token LET_TOK
%token FLET_TOK
%token NOTES_TOK
%token LOGIC_TOK
%token SAT_TOK
%token UNSAT_TOK
%token UNKNOWN_TOK
%token ASSUMPTION_TOK
%token FORMULA_TOK
%token STATUS_TOK
%token BENCHMARK_TOK
%token EXTRASORTS_TOK
%token EXTRAFUNS_TOK
%token EXTRAPREDS_TOK
%token DISTINCT_TOK
%token COLON_TOK
%token LBRACKET_TOK
%token RBRACKET_TOK
%token LPAREN_TOK
%token RPAREN_TOK
%token DOLLAR_TOK
%token QUESTION_TOK
%token EOF_TOK
%type <p_string> bench_name logic_name pred_symb attribute user_value
%type <d_bench_status> status
%type <p_expression> an_formula an_atom prop_atom
%type <p_expression_vector> an_formulas;
%type <d_kind> connective;
%type <p_command> bench_attribute
%type <p_command_sequence> bench_attributes
%start benchmark
%%
benchmark:
LPAREN_TOK BENCHMARK_TOK bench_name bench_attributes RPAREN_TOK {
_global_parser_state->setBenchmarkName(*$3);
_global_parser_state->setCommand($4);
}
| EOF_TOK { _global_parser_state->setCommand(new EmptyCommand()); }
;
bench_name: SYM_TOK;
bench_attributes:
bench_attribute { $$ = new CommandSequence($1); }
| bench_attributes bench_attribute { $$ = $1; $$->addCommand($2); }
;
bench_attribute:
COLON_TOK FORMULA_TOK an_formula { $$ = new CheckSatCommand(*$3); delete $3; }
| COLON_TOK STATUS_TOK status { $$ = new EmptyCommand(); _global_parser_state->setBenchmarkStatus($3); }
| COLON_TOK LOGIC_TOK logic_name { $$ = new EmptyCommand(); _global_parser_state->setBenchmarkLogic(*$3); delete $3; }
| COLON_TOK EXTRAPREDS_TOK LPAREN_TOK pred_symb_decls RPAREN_TOK { $$ = new EmptyCommand(); }
| annotation { $$ = new EmptyCommand(); }
;
logic_name: SYM_TOK;
status:
SAT_TOK { $$ = ParserState::SATISFIABLE; }
| UNSAT_TOK { $$ = ParserState::UNSATISFIABLE; }
| UNKNOWN_TOK { $$ = ParserState::UNKNOWN; }
;
pred_symb_decls:
pred_symb_decl
| pred_symb_decls pred_symb_decl
;
pred_symb_decl:
LPAREN_TOK pred_sig annotations RPAREN_TOK
| LPAREN_TOK pred_sig RPAREN_TOK
;
pred_sig:
pred_symb { _global_parser_state->declareNewPredicate(*$1); delete $1; }
;
an_formulas:
an_formula { $$ = new vector<Expr>; $$->push_back(*$1); delete $1; }
| an_formulas an_formula { $$ = $1; $$->push_back(*$2); delete $2; }
;
an_formula:
an_atom
| LPAREN_TOK connective an_formulas RPAREN_TOK { $$ = _global_parser_state->newExpression($2, *$3); delete $3; }
;
connective:
NOT_TOK { $$ = NOT; }
| IMPLIES_TOK { $$ = IMPLIES; }
| IF_THEN_ELSE_TOK { $$ = ITE; }
| AND_TOK { $$ = AND; }
| OR_TOK { $$ = OR; }
| XOR_TOK { $$ = XOR; }
| IFF_TOK { $$ = IFF; }
;
an_atom: prop_atom;
prop_atom:
TRUE_TOK { $$ = _global_parser_state->getNewTrue(); }
| FALSE_TOK { $$ = _global_parser_state->getNewFalse(); }
| pred_symb { $$ = _global_parser_state->getNewVariableByName(*$1); delete $1; }
;
annotations:
annotation
| annotations annotation
;
annotation:
attribute { delete $1; }
| attribute user_value { delete $1; delete $2; }
;
user_value: USER_VAL_TOK;
pred_symb: SYM_TOK;
attribute:
COLON_TOK SYM_TOK { $$ = $2; }
;
%%
|
