diff options
Diffstat (limited to 'Solvers/dreal4/bazel-bin/dreal/smt2/parser.yy.cc')
-rwxr-xr-x | Solvers/dreal4/bazel-bin/dreal/smt2/parser.yy.cc | 2543 |
1 files changed, 0 insertions, 2543 deletions
diff --git a/Solvers/dreal4/bazel-bin/dreal/smt2/parser.yy.cc b/Solvers/dreal4/bazel-bin/dreal/smt2/parser.yy.cc deleted file mode 100755 index 36ea8970..00000000 --- a/Solvers/dreal4/bazel-bin/dreal/smt2/parser.yy.cc +++ /dev/null | |||
@@ -1,2543 +0,0 @@ | |||
1 | // A Bison parser, made by GNU Bison 3.5. | ||
2 | |||
3 | // Skeleton implementation for Bison LALR(1) parsers in C++ | ||
4 | |||
5 | // Copyright (C) 2002-2015, 2018-2019 Free Software Foundation, Inc. | ||
6 | |||
7 | // This program is free software: you can redistribute it and/or modify | ||
8 | // it under the terms of the GNU General Public License as published by | ||
9 | // the Free Software Foundation, either version 3 of the License, or | ||
10 | // (at your option) any later version. | ||
11 | |||
12 | // This program is distributed in the hope that it will be useful, | ||
13 | // but WITHOUT ANY WARRANTY; without even the implied warranty of | ||
14 | // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the | ||
15 | // GNU General Public License for more details. | ||
16 | |||
17 | // You should have received a copy of the GNU General Public License | ||
18 | // along with this program. If not, see <http://www.gnu.org/licenses/>. | ||
19 | |||
20 | // As a special exception, you may create a larger work that contains | ||
21 | // part or all of the Bison parser skeleton and distribute that work | ||
22 | // under terms of your choice, so long as that work isn't itself a | ||
23 | // parser generator using the skeleton or a modified version thereof | ||
24 | // as a parser skeleton. Alternatively, if you modify or redistribute | ||
25 | // the parser skeleton itself, you may (at your option) remove this | ||
26 | // special exception, which will cause the skeleton and the resulting | ||
27 | // Bison output files to be licensed under the GNU General Public | ||
28 | // License without this special exception. | ||
29 | |||
30 | // This special exception was added by the Free Software Foundation in | ||
31 | // version 2.2 of Bison. | ||
32 | |||
33 | // Undocumented macros, especially those whose name start with YY_, | ||
34 | // are private implementation details. Do not rely on them. | ||
35 | |||
36 | |||
37 | // Take the name prefix into account. | ||
38 | #define yylex dreallex | ||
39 | |||
40 | // First part of user prologue. | ||
41 | #line 1 "dreal/smt2/parser.yy" | ||
42 | |||
43 | |||
44 | #include <cmath> | ||
45 | #include <cstdint> | ||
46 | #include <iostream> | ||
47 | #include <stdexcept> | ||
48 | #include <string> | ||
49 | #include <tuple> | ||
50 | #include <utility> | ||
51 | |||
52 | #include "dreal/smt2/logic.h" | ||
53 | #include "dreal/smt2/sort.h" | ||
54 | #include "dreal/smt2/term.h" | ||
55 | #include "dreal/symbolic/symbolic.h" | ||
56 | #include "dreal/util/math.h" | ||
57 | |||
58 | #pragma GCC diagnostic push | ||
59 | #pragma GCC diagnostic ignored "-Wold-style-cast" | ||
60 | #pragma GCC diagnostic ignored "-Wdeprecated" | ||
61 | |||
62 | #ifdef __clang__ | ||
63 | #pragma clang diagnostic push | ||
64 | #pragma clang diagnostic ignored "-Wunknown-warning-option" | ||
65 | #pragma clang diagnostic ignored "-Wdtor-name" | ||
66 | #endif | ||
67 | |||
68 | /* void yyerror(SmtPrsr parser, const char *); */ | ||
69 | #define YYMAXDEPTH 1024 * 1024 | ||
70 | #line 108 "dreal/smt2/parser.yy" | ||
71 | |||
72 | |||
73 | #include "dreal/smt2/driver.h" | ||
74 | #include "dreal/smt2/scanner.h" | ||
75 | |||
76 | /* this "connects" the bison parser in the driver to the flex scanner class | ||
77 | * object. it defines the yylex() function call to pull the next token from the | ||
78 | * current lexer object of the driver context. */ | ||
79 | #undef yylex | ||
80 | #define yylex driver.scanner->lex | ||
81 | |||
82 | |||
83 | #line 84 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
84 | |||
85 | |||
86 | #include "parser.yy.hh" | ||
87 | |||
88 | |||
89 | |||
90 | |||
91 | #ifndef YY_ | ||
92 | # if defined YYENABLE_NLS && YYENABLE_NLS | ||
93 | # if ENABLE_NLS | ||
94 | # include <libintl.h> // FIXME: INFRINGES ON USER NAME SPACE. | ||
95 | # define YY_(msgid) dgettext ("bison-runtime", msgid) | ||
96 | # endif | ||
97 | # endif | ||
98 | # ifndef YY_ | ||
99 | # define YY_(msgid) msgid | ||
100 | # endif | ||
101 | #endif | ||
102 | |||
103 | // Whether we are compiled with exception support. | ||
104 | #ifndef YY_EXCEPTIONS | ||
105 | # if defined __GNUC__ && !defined __EXCEPTIONS | ||
106 | # define YY_EXCEPTIONS 0 | ||
107 | # else | ||
108 | # define YY_EXCEPTIONS 1 | ||
109 | # endif | ||
110 | #endif | ||
111 | |||
112 | #define YYRHSLOC(Rhs, K) ((Rhs)[K].location) | ||
113 | /* YYLLOC_DEFAULT -- Set CURRENT to span from RHS[1] to RHS[N]. | ||
114 | If N is 0, then set CURRENT to the empty location which ends | ||
115 | the previous symbol: RHS[0] (always defined). */ | ||
116 | |||
117 | # ifndef YYLLOC_DEFAULT | ||
118 | # define YYLLOC_DEFAULT(Current, Rhs, N) \ | ||
119 | do \ | ||
120 | if (N) \ | ||
121 | { \ | ||
122 | (Current).begin = YYRHSLOC (Rhs, 1).begin; \ | ||
123 | (Current).end = YYRHSLOC (Rhs, N).end; \ | ||
124 | } \ | ||
125 | else \ | ||
126 | { \ | ||
127 | (Current).begin = (Current).end = YYRHSLOC (Rhs, 0).end; \ | ||
128 | } \ | ||
129 | while (false) | ||
130 | # endif | ||
131 | |||
132 | |||
133 | // Enable debugging if requested. | ||
134 | #if DREALDEBUG | ||
135 | |||
136 | // A pseudo ostream that takes yydebug_ into account. | ||
137 | # define YYCDEBUG if (yydebug_) (*yycdebug_) | ||
138 | |||
139 | # define YY_SYMBOL_PRINT(Title, Symbol) \ | ||
140 | do { \ | ||
141 | if (yydebug_) \ | ||
142 | { \ | ||
143 | *yycdebug_ << Title << ' '; \ | ||
144 | yy_print_ (*yycdebug_, Symbol); \ | ||
145 | *yycdebug_ << '\n'; \ | ||
146 | } \ | ||
147 | } while (false) | ||
148 | |||
149 | # define YY_REDUCE_PRINT(Rule) \ | ||
150 | do { \ | ||
151 | if (yydebug_) \ | ||
152 | yy_reduce_print_ (Rule); \ | ||
153 | } while (false) | ||
154 | |||
155 | # define YY_STACK_PRINT() \ | ||
156 | do { \ | ||
157 | if (yydebug_) \ | ||
158 | yystack_print_ (); \ | ||
159 | } while (false) | ||
160 | |||
161 | #else // !DREALDEBUG | ||
162 | |||
163 | # define YYCDEBUG if (false) std::cerr | ||
164 | # define YY_SYMBOL_PRINT(Title, Symbol) YYUSE (Symbol) | ||
165 | # define YY_REDUCE_PRINT(Rule) static_cast<void> (0) | ||
166 | # define YY_STACK_PRINT() static_cast<void> (0) | ||
167 | |||
168 | #endif // !DREALDEBUG | ||
169 | |||
170 | #define yyerrok (yyerrstatus_ = 0) | ||
171 | #define yyclearin (yyla.clear ()) | ||
172 | |||
173 | #define YYACCEPT goto yyacceptlab | ||
174 | #define YYABORT goto yyabortlab | ||
175 | #define YYERROR goto yyerrorlab | ||
176 | #define YYRECOVERING() (!!yyerrstatus_) | ||
177 | |||
178 | namespace dreal { | ||
179 | #line 180 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
180 | |||
181 | |||
182 | /* Return YYSTR after stripping away unnecessary quotes and | ||
183 | backslashes, so that it's suitable for yyerror. The heuristic is | ||
184 | that double-quoting is unnecessary unless the string contains an | ||
185 | apostrophe, a comma, or backslash (other than backslash-backslash). | ||
186 | YYSTR is taken from yytname. */ | ||
187 | std::string | ||
188 | Smt2Parser::yytnamerr_ (const char *yystr) | ||
189 | { | ||
190 | if (*yystr == '"') | ||
191 | { | ||
192 | std::string yyr; | ||
193 | char const *yyp = yystr; | ||
194 | |||
195 | for (;;) | ||
196 | switch (*++yyp) | ||
197 | { | ||
198 | case '\'': | ||
199 | case ',': | ||
200 | goto do_not_strip_quotes; | ||
201 | |||
202 | case '\\': | ||
203 | if (*++yyp != '\\') | ||
204 | goto do_not_strip_quotes; | ||
205 | else | ||
206 | goto append; | ||
207 | |||
208 | append: | ||
209 | default: | ||
210 | yyr += *yyp; | ||
211 | break; | ||
212 | |||
213 | case '"': | ||
214 | return yyr; | ||
215 | } | ||
216 | do_not_strip_quotes: ; | ||
217 | } | ||
218 | |||
219 | return yystr; | ||
220 | } | ||
221 | |||
222 | |||
223 | /// Build a parser object. | ||
224 | Smt2Parser::Smt2Parser (class Smt2Driver& driver_yyarg) | ||
225 | #if DREALDEBUG | ||
226 | : yydebug_ (false), | ||
227 | yycdebug_ (&std::cerr), | ||
228 | #else | ||
229 | : | ||
230 | #endif | ||
231 | driver (driver_yyarg) | ||
232 | {} | ||
233 | |||
234 | Smt2Parser::~Smt2Parser () | ||
235 | {} | ||
236 | |||
237 | Smt2Parser::syntax_error::~syntax_error () YY_NOEXCEPT YY_NOTHROW | ||
238 | {} | ||
239 | |||
240 | /*---------------. | ||
241 | | Symbol types. | | ||
242 | `---------------*/ | ||
243 | |||
244 | // basic_symbol. | ||
245 | #if 201103L <= YY_CPLUSPLUS | ||
246 | template <typename Base> | ||
247 | Smt2Parser::basic_symbol<Base>::basic_symbol (basic_symbol&& that) | ||
248 | : Base (std::move (that)) | ||
249 | , value () | ||
250 | , location (std::move (that.location)) | ||
251 | { | ||
252 | switch (this->type_get ()) | ||
253 | { | ||
254 | case 109: // term | ||
255 | value.move< Term > (std::move (that.value)); | ||
256 | break; | ||
257 | |||
258 | case 113: // name_sort | ||
259 | value.move< Variable > (std::move (that.value)); | ||
260 | break; | ||
261 | |||
262 | case 79: // "hexfloat" | ||
263 | value.move< double > (std::move (that.value)); | ||
264 | break; | ||
265 | |||
266 | case 117: // sort | ||
267 | value.move< dreal::Sort > (std::move (that.value)); | ||
268 | break; | ||
269 | |||
270 | case 80: // "int64" | ||
271 | value.move< std::int64_t > (std::move (that.value)); | ||
272 | break; | ||
273 | |||
274 | case 115: // variable_sort_list | ||
275 | value.move< std::pair<Variables, Formula> > (std::move (that.value)); | ||
276 | break; | ||
277 | |||
278 | case 119: // var_binding | ||
279 | value.move< std::pair<std::string, Term> > (std::move (that.value)); | ||
280 | break; | ||
281 | |||
282 | case 78: // "double" | ||
283 | case 81: // "symbol" | ||
284 | case 82: // "keyword" | ||
285 | case 83: // "string" | ||
286 | value.move< std::string > (std::move (that.value)); | ||
287 | break; | ||
288 | |||
289 | case 116: // variable_sort | ||
290 | value.move< std::tuple<Variable, double, double> > (std::move (that.value)); | ||
291 | break; | ||
292 | |||
293 | case 108: // term_list | ||
294 | value.move< std::vector<Term> > (std::move (that.value)); | ||
295 | break; | ||
296 | |||
297 | case 114: // name_sort_list | ||
298 | value.move< std::vector<Variable> > (std::move (that.value)); | ||
299 | break; | ||
300 | |||
301 | case 118: // var_binding_list | ||
302 | value.move< std::vector<std::pair<std::string, Term>> > (std::move (that.value)); | ||
303 | break; | ||
304 | |||
305 | default: | ||
306 | break; | ||
307 | } | ||
308 | |||
309 | } | ||
310 | #endif | ||
311 | |||
312 | template <typename Base> | ||
313 | Smt2Parser::basic_symbol<Base>::basic_symbol (const basic_symbol& that) | ||
314 | : Base (that) | ||
315 | , value () | ||
316 | , location (that.location) | ||
317 | { | ||
318 | switch (this->type_get ()) | ||
319 | { | ||
320 | case 109: // term | ||
321 | value.copy< Term > (YY_MOVE (that.value)); | ||
322 | break; | ||
323 | |||
324 | case 113: // name_sort | ||
325 | value.copy< Variable > (YY_MOVE (that.value)); | ||
326 | break; | ||
327 | |||
328 | case 79: // "hexfloat" | ||
329 | value.copy< double > (YY_MOVE (that.value)); | ||
330 | break; | ||
331 | |||
332 | case 117: // sort | ||
333 | value.copy< dreal::Sort > (YY_MOVE (that.value)); | ||
334 | break; | ||
335 | |||
336 | case 80: // "int64" | ||
337 | value.copy< std::int64_t > (YY_MOVE (that.value)); | ||
338 | break; | ||
339 | |||
340 | case 115: // variable_sort_list | ||
341 | value.copy< std::pair<Variables, Formula> > (YY_MOVE (that.value)); | ||
342 | break; | ||
343 | |||
344 | case 119: // var_binding | ||
345 | value.copy< std::pair<std::string, Term> > (YY_MOVE (that.value)); | ||
346 | break; | ||
347 | |||
348 | case 78: // "double" | ||
349 | case 81: // "symbol" | ||
350 | case 82: // "keyword" | ||
351 | case 83: // "string" | ||
352 | value.copy< std::string > (YY_MOVE (that.value)); | ||
353 | break; | ||
354 | |||
355 | case 116: // variable_sort | ||
356 | value.copy< std::tuple<Variable, double, double> > (YY_MOVE (that.value)); | ||
357 | break; | ||
358 | |||
359 | case 108: // term_list | ||
360 | value.copy< std::vector<Term> > (YY_MOVE (that.value)); | ||
361 | break; | ||
362 | |||
363 | case 114: // name_sort_list | ||
364 | value.copy< std::vector<Variable> > (YY_MOVE (that.value)); | ||
365 | break; | ||
366 | |||
367 | case 118: // var_binding_list | ||
368 | value.copy< std::vector<std::pair<std::string, Term>> > (YY_MOVE (that.value)); | ||
369 | break; | ||
370 | |||
371 | default: | ||
372 | break; | ||
373 | } | ||
374 | |||
375 | } | ||
376 | |||
377 | |||
378 | |||
379 | template <typename Base> | ||
380 | bool | ||
381 | Smt2Parser::basic_symbol<Base>::empty () const YY_NOEXCEPT | ||
382 | { | ||
383 | return Base::type_get () == empty_symbol; | ||
384 | } | ||
385 | |||
386 | template <typename Base> | ||
387 | void | ||
388 | Smt2Parser::basic_symbol<Base>::move (basic_symbol& s) | ||
389 | { | ||
390 | super_type::move (s); | ||
391 | switch (this->type_get ()) | ||
392 | { | ||
393 | case 109: // term | ||
394 | value.move< Term > (YY_MOVE (s.value)); | ||
395 | break; | ||
396 | |||
397 | case 113: // name_sort | ||
398 | value.move< Variable > (YY_MOVE (s.value)); | ||
399 | break; | ||
400 | |||
401 | case 79: // "hexfloat" | ||
402 | value.move< double > (YY_MOVE (s.value)); | ||
403 | break; | ||
404 | |||
405 | case 117: // sort | ||
406 | value.move< dreal::Sort > (YY_MOVE (s.value)); | ||
407 | break; | ||
408 | |||
409 | case 80: // "int64" | ||
410 | value.move< std::int64_t > (YY_MOVE (s.value)); | ||
411 | break; | ||
412 | |||
413 | case 115: // variable_sort_list | ||
414 | value.move< std::pair<Variables, Formula> > (YY_MOVE (s.value)); | ||
415 | break; | ||
416 | |||
417 | case 119: // var_binding | ||
418 | value.move< std::pair<std::string, Term> > (YY_MOVE (s.value)); | ||
419 | break; | ||
420 | |||
421 | case 78: // "double" | ||
422 | case 81: // "symbol" | ||
423 | case 82: // "keyword" | ||
424 | case 83: // "string" | ||
425 | value.move< std::string > (YY_MOVE (s.value)); | ||
426 | break; | ||
427 | |||
428 | case 116: // variable_sort | ||
429 | value.move< std::tuple<Variable, double, double> > (YY_MOVE (s.value)); | ||
430 | break; | ||
431 | |||
432 | case 108: // term_list | ||
433 | value.move< std::vector<Term> > (YY_MOVE (s.value)); | ||
434 | break; | ||
435 | |||
436 | case 114: // name_sort_list | ||
437 | value.move< std::vector<Variable> > (YY_MOVE (s.value)); | ||
438 | break; | ||
439 | |||
440 | case 118: // var_binding_list | ||
441 | value.move< std::vector<std::pair<std::string, Term>> > (YY_MOVE (s.value)); | ||
442 | break; | ||
443 | |||
444 | default: | ||
445 | break; | ||
446 | } | ||
447 | |||
448 | location = YY_MOVE (s.location); | ||
449 | } | ||
450 | |||
451 | // by_type. | ||
452 | Smt2Parser::by_type::by_type () | ||
453 | : type (empty_symbol) | ||
454 | {} | ||
455 | |||
456 | #if 201103L <= YY_CPLUSPLUS | ||
457 | Smt2Parser::by_type::by_type (by_type&& that) | ||
458 | : type (that.type) | ||
459 | { | ||
460 | that.clear (); | ||
461 | } | ||
462 | #endif | ||
463 | |||
464 | Smt2Parser::by_type::by_type (const by_type& that) | ||
465 | : type (that.type) | ||
466 | {} | ||
467 | |||
468 | Smt2Parser::by_type::by_type (token_type t) | ||
469 | : type (yytranslate_ (t)) | ||
470 | {} | ||
471 | |||
472 | void | ||
473 | Smt2Parser::by_type::clear () | ||
474 | { | ||
475 | type = empty_symbol; | ||
476 | } | ||
477 | |||
478 | void | ||
479 | Smt2Parser::by_type::move (by_type& that) | ||
480 | { | ||
481 | type = that.type; | ||
482 | that.clear (); | ||
483 | } | ||
484 | |||
485 | int | ||
486 | Smt2Parser::by_type::type_get () const YY_NOEXCEPT | ||
487 | { | ||
488 | return type; | ||
489 | } | ||
490 | |||
491 | |||
492 | // by_state. | ||
493 | Smt2Parser::by_state::by_state () YY_NOEXCEPT | ||
494 | : state (empty_state) | ||
495 | {} | ||
496 | |||
497 | Smt2Parser::by_state::by_state (const by_state& that) YY_NOEXCEPT | ||
498 | : state (that.state) | ||
499 | {} | ||
500 | |||
501 | void | ||
502 | Smt2Parser::by_state::clear () YY_NOEXCEPT | ||
503 | { | ||
504 | state = empty_state; | ||
505 | } | ||
506 | |||
507 | void | ||
508 | Smt2Parser::by_state::move (by_state& that) | ||
509 | { | ||
510 | state = that.state; | ||
511 | that.clear (); | ||
512 | } | ||
513 | |||
514 | Smt2Parser::by_state::by_state (state_type s) YY_NOEXCEPT | ||
515 | : state (s) | ||
516 | {} | ||
517 | |||
518 | Smt2Parser::symbol_number_type | ||
519 | Smt2Parser::by_state::type_get () const YY_NOEXCEPT | ||
520 | { | ||
521 | if (state == empty_state) | ||
522 | return empty_symbol; | ||
523 | else | ||
524 | return yystos_[state]; | ||
525 | } | ||
526 | |||
527 | Smt2Parser::stack_symbol_type::stack_symbol_type () | ||
528 | {} | ||
529 | |||
530 | Smt2Parser::stack_symbol_type::stack_symbol_type (YY_RVREF (stack_symbol_type) that) | ||
531 | : super_type (YY_MOVE (that.state), YY_MOVE (that.location)) | ||
532 | { | ||
533 | switch (that.type_get ()) | ||
534 | { | ||
535 | case 109: // term | ||
536 | value.YY_MOVE_OR_COPY< Term > (YY_MOVE (that.value)); | ||
537 | break; | ||
538 | |||
539 | case 113: // name_sort | ||
540 | value.YY_MOVE_OR_COPY< Variable > (YY_MOVE (that.value)); | ||
541 | break; | ||
542 | |||
543 | case 79: // "hexfloat" | ||
544 | value.YY_MOVE_OR_COPY< double > (YY_MOVE (that.value)); | ||
545 | break; | ||
546 | |||
547 | case 117: // sort | ||
548 | value.YY_MOVE_OR_COPY< dreal::Sort > (YY_MOVE (that.value)); | ||
549 | break; | ||
550 | |||
551 | case 80: // "int64" | ||
552 | value.YY_MOVE_OR_COPY< std::int64_t > (YY_MOVE (that.value)); | ||
553 | break; | ||
554 | |||
555 | case 115: // variable_sort_list | ||
556 | value.YY_MOVE_OR_COPY< std::pair<Variables, Formula> > (YY_MOVE (that.value)); | ||
557 | break; | ||
558 | |||
559 | case 119: // var_binding | ||
560 | value.YY_MOVE_OR_COPY< std::pair<std::string, Term> > (YY_MOVE (that.value)); | ||
561 | break; | ||
562 | |||
563 | case 78: // "double" | ||
564 | case 81: // "symbol" | ||
565 | case 82: // "keyword" | ||
566 | case 83: // "string" | ||
567 | value.YY_MOVE_OR_COPY< std::string > (YY_MOVE (that.value)); | ||
568 | break; | ||
569 | |||
570 | case 116: // variable_sort | ||
571 | value.YY_MOVE_OR_COPY< std::tuple<Variable, double, double> > (YY_MOVE (that.value)); | ||
572 | break; | ||
573 | |||
574 | case 108: // term_list | ||
575 | value.YY_MOVE_OR_COPY< std::vector<Term> > (YY_MOVE (that.value)); | ||
576 | break; | ||
577 | |||
578 | case 114: // name_sort_list | ||
579 | value.YY_MOVE_OR_COPY< std::vector<Variable> > (YY_MOVE (that.value)); | ||
580 | break; | ||
581 | |||
582 | case 118: // var_binding_list | ||
583 | value.YY_MOVE_OR_COPY< std::vector<std::pair<std::string, Term>> > (YY_MOVE (that.value)); | ||
584 | break; | ||
585 | |||
586 | default: | ||
587 | break; | ||
588 | } | ||
589 | |||
590 | #if 201103L <= YY_CPLUSPLUS | ||
591 | // that is emptied. | ||
592 | that.state = empty_state; | ||
593 | #endif | ||
594 | } | ||
595 | |||
596 | Smt2Parser::stack_symbol_type::stack_symbol_type (state_type s, YY_MOVE_REF (symbol_type) that) | ||
597 | : super_type (s, YY_MOVE (that.location)) | ||
598 | { | ||
599 | switch (that.type_get ()) | ||
600 | { | ||
601 | case 109: // term | ||
602 | value.move< Term > (YY_MOVE (that.value)); | ||
603 | break; | ||
604 | |||
605 | case 113: // name_sort | ||
606 | value.move< Variable > (YY_MOVE (that.value)); | ||
607 | break; | ||
608 | |||
609 | case 79: // "hexfloat" | ||
610 | value.move< double > (YY_MOVE (that.value)); | ||
611 | break; | ||
612 | |||
613 | case 117: // sort | ||
614 | value.move< dreal::Sort > (YY_MOVE (that.value)); | ||
615 | break; | ||
616 | |||
617 | case 80: // "int64" | ||
618 | value.move< std::int64_t > (YY_MOVE (that.value)); | ||
619 | break; | ||
620 | |||
621 | case 115: // variable_sort_list | ||
622 | value.move< std::pair<Variables, Formula> > (YY_MOVE (that.value)); | ||
623 | break; | ||
624 | |||
625 | case 119: // var_binding | ||
626 | value.move< std::pair<std::string, Term> > (YY_MOVE (that.value)); | ||
627 | break; | ||
628 | |||
629 | case 78: // "double" | ||
630 | case 81: // "symbol" | ||
631 | case 82: // "keyword" | ||
632 | case 83: // "string" | ||
633 | value.move< std::string > (YY_MOVE (that.value)); | ||
634 | break; | ||
635 | |||
636 | case 116: // variable_sort | ||
637 | value.move< std::tuple<Variable, double, double> > (YY_MOVE (that.value)); | ||
638 | break; | ||
639 | |||
640 | case 108: // term_list | ||
641 | value.move< std::vector<Term> > (YY_MOVE (that.value)); | ||
642 | break; | ||
643 | |||
644 | case 114: // name_sort_list | ||
645 | value.move< std::vector<Variable> > (YY_MOVE (that.value)); | ||
646 | break; | ||
647 | |||
648 | case 118: // var_binding_list | ||
649 | value.move< std::vector<std::pair<std::string, Term>> > (YY_MOVE (that.value)); | ||
650 | break; | ||
651 | |||
652 | default: | ||
653 | break; | ||
654 | } | ||
655 | |||
656 | // that is emptied. | ||
657 | that.type = empty_symbol; | ||
658 | } | ||
659 | |||
660 | #if YY_CPLUSPLUS < 201103L | ||
661 | Smt2Parser::stack_symbol_type& | ||
662 | Smt2Parser::stack_symbol_type::operator= (const stack_symbol_type& that) | ||
663 | { | ||
664 | state = that.state; | ||
665 | switch (that.type_get ()) | ||
666 | { | ||
667 | case 109: // term | ||
668 | value.copy< Term > (that.value); | ||
669 | break; | ||
670 | |||
671 | case 113: // name_sort | ||
672 | value.copy< Variable > (that.value); | ||
673 | break; | ||
674 | |||
675 | case 79: // "hexfloat" | ||
676 | value.copy< double > (that.value); | ||
677 | break; | ||
678 | |||
679 | case 117: // sort | ||
680 | value.copy< dreal::Sort > (that.value); | ||
681 | break; | ||
682 | |||
683 | case 80: // "int64" | ||
684 | value.copy< std::int64_t > (that.value); | ||
685 | break; | ||
686 | |||
687 | case 115: // variable_sort_list | ||
688 | value.copy< std::pair<Variables, Formula> > (that.value); | ||
689 | break; | ||
690 | |||
691 | case 119: // var_binding | ||
692 | value.copy< std::pair<std::string, Term> > (that.value); | ||
693 | break; | ||
694 | |||
695 | case 78: // "double" | ||
696 | case 81: // "symbol" | ||
697 | case 82: // "keyword" | ||
698 | case 83: // "string" | ||
699 | value.copy< std::string > (that.value); | ||
700 | break; | ||
701 | |||
702 | case 116: // variable_sort | ||
703 | value.copy< std::tuple<Variable, double, double> > (that.value); | ||
704 | break; | ||
705 | |||
706 | case 108: // term_list | ||
707 | value.copy< std::vector<Term> > (that.value); | ||
708 | break; | ||
709 | |||
710 | case 114: // name_sort_list | ||
711 | value.copy< std::vector<Variable> > (that.value); | ||
712 | break; | ||
713 | |||
714 | case 118: // var_binding_list | ||
715 | value.copy< std::vector<std::pair<std::string, Term>> > (that.value); | ||
716 | break; | ||
717 | |||
718 | default: | ||
719 | break; | ||
720 | } | ||
721 | |||
722 | location = that.location; | ||
723 | return *this; | ||
724 | } | ||
725 | |||
726 | Smt2Parser::stack_symbol_type& | ||
727 | Smt2Parser::stack_symbol_type::operator= (stack_symbol_type& that) | ||
728 | { | ||
729 | state = that.state; | ||
730 | switch (that.type_get ()) | ||
731 | { | ||
732 | case 109: // term | ||
733 | value.move< Term > (that.value); | ||
734 | break; | ||
735 | |||
736 | case 113: // name_sort | ||
737 | value.move< Variable > (that.value); | ||
738 | break; | ||
739 | |||
740 | case 79: // "hexfloat" | ||
741 | value.move< double > (that.value); | ||
742 | break; | ||
743 | |||
744 | case 117: // sort | ||
745 | value.move< dreal::Sort > (that.value); | ||
746 | break; | ||
747 | |||
748 | case 80: // "int64" | ||
749 | value.move< std::int64_t > (that.value); | ||
750 | break; | ||
751 | |||
752 | case 115: // variable_sort_list | ||
753 | value.move< std::pair<Variables, Formula> > (that.value); | ||
754 | break; | ||
755 | |||
756 | case 119: // var_binding | ||
757 | value.move< std::pair<std::string, Term> > (that.value); | ||
758 | break; | ||
759 | |||
760 | case 78: // "double" | ||
761 | case 81: // "symbol" | ||
762 | case 82: // "keyword" | ||
763 | case 83: // "string" | ||
764 | value.move< std::string > (that.value); | ||
765 | break; | ||
766 | |||
767 | case 116: // variable_sort | ||
768 | value.move< std::tuple<Variable, double, double> > (that.value); | ||
769 | break; | ||
770 | |||
771 | case 108: // term_list | ||
772 | value.move< std::vector<Term> > (that.value); | ||
773 | break; | ||
774 | |||
775 | case 114: // name_sort_list | ||
776 | value.move< std::vector<Variable> > (that.value); | ||
777 | break; | ||
778 | |||
779 | case 118: // var_binding_list | ||
780 | value.move< std::vector<std::pair<std::string, Term>> > (that.value); | ||
781 | break; | ||
782 | |||
783 | default: | ||
784 | break; | ||
785 | } | ||
786 | |||
787 | location = that.location; | ||
788 | // that is emptied. | ||
789 | that.state = empty_state; | ||
790 | return *this; | ||
791 | } | ||
792 | #endif | ||
793 | |||
794 | template <typename Base> | ||
795 | void | ||
796 | Smt2Parser::yy_destroy_ (const char* yymsg, basic_symbol<Base>& yysym) const | ||
797 | { | ||
798 | if (yymsg) | ||
799 | YY_SYMBOL_PRINT (yymsg, yysym); | ||
800 | } | ||
801 | |||
802 | #if DREALDEBUG | ||
803 | template <typename Base> | ||
804 | void | ||
805 | Smt2Parser::yy_print_ (std::ostream& yyo, | ||
806 | const basic_symbol<Base>& yysym) const | ||
807 | { | ||
808 | std::ostream& yyoutput = yyo; | ||
809 | YYUSE (yyoutput); | ||
810 | symbol_number_type yytype = yysym.type_get (); | ||
811 | #if defined __GNUC__ && ! defined __clang__ && ! defined __ICC && __GNUC__ * 100 + __GNUC_MINOR__ <= 408 | ||
812 | // Avoid a (spurious) G++ 4.8 warning about "array subscript is | ||
813 | // below array bounds". | ||
814 | if (yysym.empty ()) | ||
815 | std::abort (); | ||
816 | #endif | ||
817 | yyo << (yytype < yyntokens_ ? "token" : "nterm") | ||
818 | << ' ' << yytname_[yytype] << " (" | ||
819 | << yysym.location << ": "; | ||
820 | YYUSE (yytype); | ||
821 | yyo << ')'; | ||
822 | } | ||
823 | #endif | ||
824 | |||
825 | void | ||
826 | Smt2Parser::yypush_ (const char* m, YY_MOVE_REF (stack_symbol_type) sym) | ||
827 | { | ||
828 | if (m) | ||
829 | YY_SYMBOL_PRINT (m, sym); | ||
830 | yystack_.push (YY_MOVE (sym)); | ||
831 | } | ||
832 | |||
833 | void | ||
834 | Smt2Parser::yypush_ (const char* m, state_type s, YY_MOVE_REF (symbol_type) sym) | ||
835 | { | ||
836 | #if 201103L <= YY_CPLUSPLUS | ||
837 | yypush_ (m, stack_symbol_type (s, std::move (sym))); | ||
838 | #else | ||
839 | stack_symbol_type ss (s, sym); | ||
840 | yypush_ (m, ss); | ||
841 | #endif | ||
842 | } | ||
843 | |||
844 | void | ||
845 | Smt2Parser::yypop_ (int n) | ||
846 | { | ||
847 | yystack_.pop (n); | ||
848 | } | ||
849 | |||
850 | #if DREALDEBUG | ||
851 | std::ostream& | ||
852 | Smt2Parser::debug_stream () const | ||
853 | { | ||
854 | return *yycdebug_; | ||
855 | } | ||
856 | |||
857 | void | ||
858 | Smt2Parser::set_debug_stream (std::ostream& o) | ||
859 | { | ||
860 | yycdebug_ = &o; | ||
861 | } | ||
862 | |||
863 | |||
864 | Smt2Parser::debug_level_type | ||
865 | Smt2Parser::debug_level () const | ||
866 | { | ||
867 | return yydebug_; | ||
868 | } | ||
869 | |||
870 | void | ||
871 | Smt2Parser::set_debug_level (debug_level_type l) | ||
872 | { | ||
873 | yydebug_ = l; | ||
874 | } | ||
875 | #endif // DREALDEBUG | ||
876 | |||
877 | Smt2Parser::state_type | ||
878 | Smt2Parser::yy_lr_goto_state_ (state_type yystate, int yysym) | ||
879 | { | ||
880 | int yyr = yypgoto_[yysym - yyntokens_] + yystate; | ||
881 | if (0 <= yyr && yyr <= yylast_ && yycheck_[yyr] == yystate) | ||
882 | return yytable_[yyr]; | ||
883 | else | ||
884 | return yydefgoto_[yysym - yyntokens_]; | ||
885 | } | ||
886 | |||
887 | bool | ||
888 | Smt2Parser::yy_pact_value_is_default_ (int yyvalue) | ||
889 | { | ||
890 | return yyvalue == yypact_ninf_; | ||
891 | } | ||
892 | |||
893 | bool | ||
894 | Smt2Parser::yy_table_value_is_error_ (int yyvalue) | ||
895 | { | ||
896 | return yyvalue == yytable_ninf_; | ||
897 | } | ||
898 | |||
899 | int | ||
900 | Smt2Parser::operator() () | ||
901 | { | ||
902 | return parse (); | ||
903 | } | ||
904 | |||
905 | int | ||
906 | Smt2Parser::parse () | ||
907 | { | ||
908 | int yyn; | ||
909 | /// Length of the RHS of the rule being reduced. | ||
910 | int yylen = 0; | ||
911 | |||
912 | // Error handling. | ||
913 | int yynerrs_ = 0; | ||
914 | int yyerrstatus_ = 0; | ||
915 | |||
916 | /// The lookahead symbol. | ||
917 | symbol_type yyla; | ||
918 | |||
919 | /// The locations where the error started and ended. | ||
920 | stack_symbol_type yyerror_range[3]; | ||
921 | |||
922 | /// The return value of parse (). | ||
923 | int yyresult; | ||
924 | |||
925 | #if YY_EXCEPTIONS | ||
926 | try | ||
927 | #endif // YY_EXCEPTIONS | ||
928 | { | ||
929 | YYCDEBUG << "Starting parse\n"; | ||
930 | |||
931 | |||
932 | // User initialization code. | ||
933 | #line 55 "dreal/smt2/parser.yy" | ||
934 | { | ||
935 | // initialize the initial location object | ||
936 | yyla.location.begin.filename = yyla.location.end.filename = &driver.mutable_streamname(); | ||
937 | } | ||
938 | |||
939 | #line 940 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
940 | |||
941 | |||
942 | /* Initialize the stack. The initial state will be set in | ||
943 | yynewstate, since the latter expects the semantical and the | ||
944 | location values to have been already stored, initialize these | ||
945 | stacks with a primary value. */ | ||
946 | yystack_.clear (); | ||
947 | yypush_ (YY_NULLPTR, 0, YY_MOVE (yyla)); | ||
948 | |||
949 | /*-----------------------------------------------. | ||
950 | | yynewstate -- push a new symbol on the stack. | | ||
951 | `-----------------------------------------------*/ | ||
952 | yynewstate: | ||
953 | YYCDEBUG << "Entering state " << int (yystack_[0].state) << '\n'; | ||
954 | |||
955 | // Accept? | ||
956 | if (yystack_[0].state == yyfinal_) | ||
957 | YYACCEPT; | ||
958 | |||
959 | goto yybackup; | ||
960 | |||
961 | |||
962 | /*-----------. | ||
963 | | yybackup. | | ||
964 | `-----------*/ | ||
965 | yybackup: | ||
966 | // Try to take a decision without lookahead. | ||
967 | yyn = yypact_[yystack_[0].state]; | ||
968 | if (yy_pact_value_is_default_ (yyn)) | ||
969 | goto yydefault; | ||
970 | |||
971 | // Read a lookahead token. | ||
972 | if (yyla.empty ()) | ||
973 | { | ||
974 | YYCDEBUG << "Reading a token: "; | ||
975 | #if YY_EXCEPTIONS | ||
976 | try | ||
977 | #endif // YY_EXCEPTIONS | ||
978 | { | ||
979 | yyla.type = yytranslate_ (yylex (&yyla.value, &yyla.location)); | ||
980 | } | ||
981 | #if YY_EXCEPTIONS | ||
982 | catch (const syntax_error& yyexc) | ||
983 | { | ||
984 | YYCDEBUG << "Caught exception: " << yyexc.what() << '\n'; | ||
985 | error (yyexc); | ||
986 | goto yyerrlab1; | ||
987 | } | ||
988 | #endif // YY_EXCEPTIONS | ||
989 | } | ||
990 | YY_SYMBOL_PRINT ("Next token is", yyla); | ||
991 | |||
992 | /* If the proper action on seeing token YYLA.TYPE is to reduce or | ||
993 | to detect an error, take that action. */ | ||
994 | yyn += yyla.type_get (); | ||
995 | if (yyn < 0 || yylast_ < yyn || yycheck_[yyn] != yyla.type_get ()) | ||
996 | { | ||
997 | goto yydefault; | ||
998 | } | ||
999 | |||
1000 | // Reduce or error. | ||
1001 | yyn = yytable_[yyn]; | ||
1002 | if (yyn <= 0) | ||
1003 | { | ||
1004 | if (yy_table_value_is_error_ (yyn)) | ||
1005 | goto yyerrlab; | ||
1006 | yyn = -yyn; | ||
1007 | goto yyreduce; | ||
1008 | } | ||
1009 | |||
1010 | // Count tokens shifted since error; after three, turn off error status. | ||
1011 | if (yyerrstatus_) | ||
1012 | --yyerrstatus_; | ||
1013 | |||
1014 | // Shift the lookahead token. | ||
1015 | yypush_ ("Shifting", static_cast<state_type> (yyn), YY_MOVE (yyla)); | ||
1016 | goto yynewstate; | ||
1017 | |||
1018 | |||
1019 | /*-----------------------------------------------------------. | ||
1020 | | yydefault -- do the default action for the current state. | | ||
1021 | `-----------------------------------------------------------*/ | ||
1022 | yydefault: | ||
1023 | yyn = yydefact_[yystack_[0].state]; | ||
1024 | if (yyn == 0) | ||
1025 | goto yyerrlab; | ||
1026 | goto yyreduce; | ||
1027 | |||
1028 | |||
1029 | /*-----------------------------. | ||
1030 | | yyreduce -- do a reduction. | | ||
1031 | `-----------------------------*/ | ||
1032 | yyreduce: | ||
1033 | yylen = yyr2_[yyn]; | ||
1034 | { | ||
1035 | stack_symbol_type yylhs; | ||
1036 | yylhs.state = yy_lr_goto_state_ (yystack_[yylen].state, yyr1_[yyn]); | ||
1037 | /* Variants are always initialized to an empty instance of the | ||
1038 | correct type. The default '$$ = $1' action is NOT applied | ||
1039 | when using variants. */ | ||
1040 | switch (yyr1_[yyn]) | ||
1041 | { | ||
1042 | case 109: // term | ||
1043 | yylhs.value.emplace< Term > (); | ||
1044 | break; | ||
1045 | |||
1046 | case 113: // name_sort | ||
1047 | yylhs.value.emplace< Variable > (); | ||
1048 | break; | ||
1049 | |||
1050 | case 79: // "hexfloat" | ||
1051 | yylhs.value.emplace< double > (); | ||
1052 | break; | ||
1053 | |||
1054 | case 117: // sort | ||
1055 | yylhs.value.emplace< dreal::Sort > (); | ||
1056 | break; | ||
1057 | |||
1058 | case 80: // "int64" | ||
1059 | yylhs.value.emplace< std::int64_t > (); | ||
1060 | break; | ||
1061 | |||
1062 | case 115: // variable_sort_list | ||
1063 | yylhs.value.emplace< std::pair<Variables, Formula> > (); | ||
1064 | break; | ||
1065 | |||
1066 | case 119: // var_binding | ||
1067 | yylhs.value.emplace< std::pair<std::string, Term> > (); | ||
1068 | break; | ||
1069 | |||
1070 | case 78: // "double" | ||
1071 | case 81: // "symbol" | ||
1072 | case 82: // "keyword" | ||
1073 | case 83: // "string" | ||
1074 | yylhs.value.emplace< std::string > (); | ||
1075 | break; | ||
1076 | |||
1077 | case 116: // variable_sort | ||
1078 | yylhs.value.emplace< std::tuple<Variable, double, double> > (); | ||
1079 | break; | ||
1080 | |||
1081 | case 108: // term_list | ||
1082 | yylhs.value.emplace< std::vector<Term> > (); | ||
1083 | break; | ||
1084 | |||
1085 | case 114: // name_sort_list | ||
1086 | yylhs.value.emplace< std::vector<Variable> > (); | ||
1087 | break; | ||
1088 | |||
1089 | case 118: // var_binding_list | ||
1090 | yylhs.value.emplace< std::vector<std::pair<std::string, Term>> > (); | ||
1091 | break; | ||
1092 | |||
1093 | default: | ||
1094 | break; | ||
1095 | } | ||
1096 | |||
1097 | |||
1098 | // Default location. | ||
1099 | { | ||
1100 | stack_type::slice range (yystack_, yylen); | ||
1101 | YYLLOC_DEFAULT (yylhs.location, range, yylen); | ||
1102 | yyerror_range[1].location = yylhs.location; | ||
1103 | } | ||
1104 | |||
1105 | // Perform the reduction. | ||
1106 | YY_REDUCE_PRINT (yyn); | ||
1107 | #if YY_EXCEPTIONS | ||
1108 | try | ||
1109 | #endif // YY_EXCEPTIONS | ||
1110 | { | ||
1111 | switch (yyn) | ||
1112 | { | ||
1113 | case 20: | ||
1114 | #line 148 "dreal/smt2/parser.yy" | ||
1115 | { | ||
1116 | driver.mutable_context().Assert(yystack_[1].value.as < Term > ().formula()); | ||
1117 | } | ||
1118 | #line 1119 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1119 | break; | ||
1120 | |||
1121 | case 21: | ||
1122 | #line 153 "dreal/smt2/parser.yy" | ||
1123 | { | ||
1124 | driver.CheckSat(); | ||
1125 | } | ||
1126 | #line 1127 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1127 | break; | ||
1128 | |||
1129 | case 22: | ||
1130 | #line 158 "dreal/smt2/parser.yy" | ||
1131 | { | ||
1132 | driver.DeclareVariable(yystack_[4].value.as < std::string > (), yystack_[1].value.as < dreal::Sort > ()); | ||
1133 | } | ||
1134 | #line 1135 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1135 | break; | ||
1136 | |||
1137 | case 23: | ||
1138 | #line 162 "dreal/smt2/parser.yy" | ||
1139 | { | ||
1140 | driver.DeclareVariable(yystack_[9].value.as < std::string > (), yystack_[6].value.as < dreal::Sort > (), yystack_[4].value.as < Term > (), yystack_[2].value.as < Term > ()); | ||
1141 | } | ||
1142 | #line 1143 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1143 | break; | ||
1144 | |||
1145 | case 24: | ||
1146 | #line 166 "dreal/smt2/parser.yy" | ||
1147 | { | ||
1148 | driver.DeclareVariable(yystack_[2].value.as < std::string > (), yystack_[1].value.as < dreal::Sort > ()); | ||
1149 | } | ||
1150 | #line 1151 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1151 | break; | ||
1152 | |||
1153 | case 25: | ||
1154 | #line 170 "dreal/smt2/parser.yy" | ||
1155 | { | ||
1156 | driver.DeclareVariable(yystack_[7].value.as < std::string > (), yystack_[6].value.as < dreal::Sort > (), yystack_[4].value.as < Term > (), yystack_[2].value.as < Term > ()); | ||
1157 | } | ||
1158 | #line 1159 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1159 | break; | ||
1160 | |||
1161 | case 26: | ||
1162 | #line 176 "dreal/smt2/parser.yy" | ||
1163 | { | ||
1164 | if (yystack_[5].value.as < std::vector<Variable> > ().empty()) { | ||
1165 | // No parameters - treat as variable, just like declare-fun. | ||
1166 | const Variable v{driver.DeclareVariable(yystack_[8].value.as < std::string > (), yystack_[3].value.as < dreal::Sort > ())}; | ||
1167 | if (yystack_[2].value.as < Term > ().type() == Term::Type::FORMULA) { | ||
1168 | driver.mutable_context().Assert(v == yystack_[2].value.as < Term > ().formula()); | ||
1169 | } else { | ||
1170 | driver.mutable_context().Assert(v == yystack_[2].value.as < Term > ().expression()); | ||
1171 | } | ||
1172 | } else { | ||
1173 | driver.DefineFun(yystack_[8].value.as < std::string > (), yystack_[5].value.as < std::vector<Variable> > (), yystack_[3].value.as < dreal::Sort > (), yystack_[2].value.as < Term > ()); | ||
1174 | } | ||
1175 | } | ||
1176 | #line 1177 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1177 | break; | ||
1178 | |||
1179 | case 27: | ||
1180 | #line 191 "dreal/smt2/parser.yy" | ||
1181 | { | ||
1182 | driver.mutable_context().Exit(); | ||
1183 | YYACCEPT; | ||
1184 | } | ||
1185 | #line 1186 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1186 | break; | ||
1187 | |||
1188 | case 28: | ||
1189 | #line 198 "dreal/smt2/parser.yy" | ||
1190 | { | ||
1191 | driver.GetModel(); | ||
1192 | } | ||
1193 | #line 1194 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1194 | break; | ||
1195 | |||
1196 | case 29: | ||
1197 | #line 204 "dreal/smt2/parser.yy" | ||
1198 | { | ||
1199 | driver.GetValue(yystack_[2].value.as < std::vector<Term> > ()); | ||
1200 | } | ||
1201 | #line 1202 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1202 | break; | ||
1203 | |||
1204 | case 30: | ||
1205 | #line 209 "dreal/smt2/parser.yy" | ||
1206 | { | ||
1207 | driver.mutable_context().Maximize(yystack_[1].value.as < Term > ().expression()); | ||
1208 | } | ||
1209 | #line 1210 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1210 | break; | ||
1211 | |||
1212 | case 31: | ||
1213 | #line 214 "dreal/smt2/parser.yy" | ||
1214 | { | ||
1215 | driver.mutable_context().Minimize(yystack_[1].value.as < Term > ().expression()); | ||
1216 | } | ||
1217 | #line 1218 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1218 | break; | ||
1219 | |||
1220 | case 32: | ||
1221 | #line 220 "dreal/smt2/parser.yy" | ||
1222 | { | ||
1223 | driver | ||
1224 | .mutable_context() | ||
1225 | .SetInfo(yystack_[2].value.as < std::string > (), yystack_[1].value.as < std::string > ()); | ||
1226 | } | ||
1227 | #line 1228 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1228 | break; | ||
1229 | |||
1230 | case 33: | ||
1231 | #line 225 "dreal/smt2/parser.yy" | ||
1232 | { | ||
1233 | driver | ||
1234 | .mutable_context() | ||
1235 | .SetInfo(yystack_[2].value.as < std::string > (), yystack_[1].value.as < std::string > ()); | ||
1236 | } | ||
1237 | #line 1238 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1238 | break; | ||
1239 | |||
1240 | case 34: | ||
1241 | #line 230 "dreal/smt2/parser.yy" | ||
1242 | { | ||
1243 | driver | ||
1244 | .mutable_context() | ||
1245 | .SetInfo(yystack_[2].value.as < std::string > (), std::stod(yystack_[1].value.as < std::string > ())); | ||
1246 | } | ||
1247 | #line 1248 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1248 | break; | ||
1249 | |||
1250 | case 35: | ||
1251 | #line 237 "dreal/smt2/parser.yy" | ||
1252 | { | ||
1253 | driver | ||
1254 | .mutable_context() | ||
1255 | .SetLogic(dreal::parse_logic(yystack_[1].value.as < std::string > ())); | ||
1256 | } | ||
1257 | #line 1258 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1258 | break; | ||
1259 | |||
1260 | case 36: | ||
1261 | #line 244 "dreal/smt2/parser.yy" | ||
1262 | { | ||
1263 | driver | ||
1264 | .mutable_context() | ||
1265 | .SetOption(yystack_[2].value.as < std::string > (), yystack_[1].value.as < std::string > ()); | ||
1266 | } | ||
1267 | #line 1268 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1268 | break; | ||
1269 | |||
1270 | case 37: | ||
1271 | #line 249 "dreal/smt2/parser.yy" | ||
1272 | { | ||
1273 | driver | ||
1274 | .mutable_context() | ||
1275 | .SetOption(yystack_[2].value.as < std::string > (), std::stod(yystack_[1].value.as < std::string > ())); | ||
1276 | } | ||
1277 | #line 1278 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1278 | break; | ||
1279 | |||
1280 | case 38: | ||
1281 | #line 254 "dreal/smt2/parser.yy" | ||
1282 | { | ||
1283 | driver | ||
1284 | .mutable_context() | ||
1285 | .SetOption(yystack_[2].value.as < std::string > (), "true"); | ||
1286 | } | ||
1287 | #line 1288 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1288 | break; | ||
1289 | |||
1290 | case 39: | ||
1291 | #line 259 "dreal/smt2/parser.yy" | ||
1292 | { | ||
1293 | driver | ||
1294 | .mutable_context() | ||
1295 | .SetOption(yystack_[2].value.as < std::string > (), "false"); | ||
1296 | } | ||
1297 | #line 1298 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1298 | break; | ||
1299 | |||
1300 | case 40: | ||
1301 | #line 267 "dreal/smt2/parser.yy" | ||
1302 | { | ||
1303 | driver | ||
1304 | .GetOption(yystack_[1].value.as < std::string > ()); | ||
1305 | } | ||
1306 | #line 1307 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1307 | break; | ||
1308 | |||
1309 | case 41: | ||
1310 | #line 274 "dreal/smt2/parser.yy" | ||
1311 | { | ||
1312 | driver.mutable_context().Push(convert_int64_to_int(yystack_[1].value.as < std::int64_t > ())); | ||
1313 | } | ||
1314 | #line 1315 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1315 | break; | ||
1316 | |||
1317 | case 42: | ||
1318 | #line 279 "dreal/smt2/parser.yy" | ||
1319 | { | ||
1320 | driver.mutable_context().Pop(convert_int64_to_int(yystack_[1].value.as < std::int64_t > ())); | ||
1321 | } | ||
1322 | #line 1323 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1323 | break; | ||
1324 | |||
1325 | case 43: | ||
1326 | #line 284 "dreal/smt2/parser.yy" | ||
1327 | { yylhs.value.as < std::vector<Term> > () = std::vector<Term>(1, yystack_[0].value.as < Term > ()); } | ||
1328 | #line 1329 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1329 | break; | ||
1330 | |||
1331 | case 44: | ||
1332 | #line 285 "dreal/smt2/parser.yy" | ||
1333 | { yystack_[1].value.as < std::vector<Term> > ().push_back(yystack_[0].value.as < Term > ()); yylhs.value.as < std::vector<Term> > () = yystack_[1].value.as < std::vector<Term> > (); } | ||
1334 | #line 1335 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1335 | break; | ||
1336 | |||
1337 | case 45: | ||
1338 | #line 288 "dreal/smt2/parser.yy" | ||
1339 | { yylhs.value.as < Term > () = Formula::True(); } | ||
1340 | #line 1341 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1341 | break; | ||
1342 | |||
1343 | case 46: | ||
1344 | #line 289 "dreal/smt2/parser.yy" | ||
1345 | { yylhs.value.as < Term > () = Formula::False(); } | ||
1346 | #line 1347 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1347 | break; | ||
1348 | |||
1349 | case 47: | ||
1350 | #line 290 "dreal/smt2/parser.yy" | ||
1351 | { | ||
1352 | const Term& t1 = yystack_[2].value.as < Term > (); | ||
1353 | const Term& t2 = yystack_[1].value.as < Term > (); | ||
1354 | if (t1.type() == Term::Type::EXPRESSION && | ||
1355 | t2.type() == Term::Type::EXPRESSION) { | ||
1356 | yylhs.value.as < Term > () = t1.expression() == t2.expression(); | ||
1357 | } else if (t1.type() == Term::Type::FORMULA && | ||
1358 | t2.type() == Term::Type::FORMULA) { | ||
1359 | // (f1 = f2) | ||
1360 | // -> (f1 ⇔ f2) | ||
1361 | // -> (f1 ∧ f2) ∨ (¬f1 ∧ ¬f2) | ||
1362 | yylhs.value.as < Term > () = t1.formula() == t2.formula(); | ||
1363 | } else { | ||
1364 | std::cerr << yystack_[4].location << " : Type mismatch in `t1 == t2`:" << std::endl | ||
1365 | << " t1 = " << t1 << std::endl | ||
1366 | << " t2 = " << t2 << std::endl; | ||
1367 | YYABORT; | ||
1368 | } | ||
1369 | } | ||
1370 | #line 1371 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1371 | break; | ||
1372 | |||
1373 | case 48: | ||
1374 | #line 309 "dreal/smt2/parser.yy" | ||
1375 | { yylhs.value.as < Term > () = yystack_[2].value.as < Term > ().expression() < yystack_[1].value.as < Term > ().expression(); } | ||
1376 | #line 1377 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1377 | break; | ||
1378 | |||
1379 | case 49: | ||
1380 | #line 310 "dreal/smt2/parser.yy" | ||
1381 | { yylhs.value.as < Term > () = yystack_[2].value.as < Term > ().expression() <= yystack_[1].value.as < Term > ().expression(); } | ||
1382 | #line 1383 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1383 | break; | ||
1384 | |||
1385 | case 50: | ||
1386 | #line 311 "dreal/smt2/parser.yy" | ||
1387 | { yylhs.value.as < Term > () = yystack_[2].value.as < Term > ().expression() > yystack_[1].value.as < Term > ().expression(); } | ||
1388 | #line 1389 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1389 | break; | ||
1390 | |||
1391 | case 51: | ||
1392 | #line 312 "dreal/smt2/parser.yy" | ||
1393 | { yylhs.value.as < Term > () = yystack_[2].value.as < Term > ().expression() >= yystack_[1].value.as < Term > ().expression(); } | ||
1394 | #line 1395 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1395 | break; | ||
1396 | |||
1397 | case 52: | ||
1398 | #line 313 "dreal/smt2/parser.yy" | ||
1399 | { | ||
1400 | Formula f = Formula::True(); | ||
1401 | for (const Term& t : yystack_[1].value.as < std::vector<Term> > ()) { | ||
1402 | f = f && t.formula(); | ||
1403 | } | ||
1404 | yylhs.value.as < Term > () = f; | ||
1405 | } | ||
1406 | #line 1407 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1407 | break; | ||
1408 | |||
1409 | case 53: | ||
1410 | #line 320 "dreal/smt2/parser.yy" | ||
1411 | { | ||
1412 | Formula f = Formula::False(); | ||
1413 | for (const Term& t : yystack_[1].value.as < std::vector<Term> > ()) { | ||
1414 | f = f || t.formula(); | ||
1415 | } | ||
1416 | yylhs.value.as < Term > () = f; | ||
1417 | } | ||
1418 | #line 1419 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1419 | break; | ||
1420 | |||
1421 | case 54: | ||
1422 | #line 327 "dreal/smt2/parser.yy" | ||
1423 | { | ||
1424 | Formula f = Formula::False(); | ||
1425 | for (const Term& t : yystack_[1].value.as < std::vector<Term> > ()) { | ||
1426 | f = (f && !t.formula()) || (!f && t.formula()); | ||
1427 | } | ||
1428 | yylhs.value.as < Term > () = f; | ||
1429 | } | ||
1430 | #line 1431 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1431 | break; | ||
1432 | |||
1433 | case 55: | ||
1434 | #line 334 "dreal/smt2/parser.yy" | ||
1435 | { | ||
1436 | yylhs.value.as < Term > () = !(yystack_[1].value.as < Term > ().formula()); | ||
1437 | } | ||
1438 | #line 1439 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1439 | break; | ||
1440 | |||
1441 | case 56: | ||
1442 | #line 337 "dreal/smt2/parser.yy" | ||
1443 | { | ||
1444 | yylhs.value.as < Term > () = !(yystack_[2].value.as < Term > ().formula()) || yystack_[1].value.as < Term > ().formula(); | ||
1445 | } | ||
1446 | #line 1447 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1447 | break; | ||
1448 | |||
1449 | case 57: | ||
1450 | #line 340 "dreal/smt2/parser.yy" | ||
1451 | { | ||
1452 | const Formula& cond = yystack_[3].value.as < Term > ().formula(); | ||
1453 | const Term& then_term = yystack_[2].value.as < Term > (); | ||
1454 | const Term& else_term = yystack_[1].value.as < Term > (); | ||
1455 | if (then_term.type() == Term::Type::EXPRESSION && | ||
1456 | else_term.type() == Term::Type::EXPRESSION) { | ||
1457 | const Expression& e1 = then_term.expression(); | ||
1458 | const Expression& e2 = else_term.expression(); | ||
1459 | yylhs.value.as < Term > () = if_then_else(cond, e1, e2); | ||
1460 | } else if (then_term.type() == Term::Type::FORMULA && | ||
1461 | else_term.type() == Term::Type::FORMULA) { | ||
1462 | // if(cond) then f1 else f2 | ||
1463 | // -> (cond => f1) ∧ (¬cond => f2) | ||
1464 | // -> (¬cond ∨ f1) ∧ (cond ∨ f2) | ||
1465 | const Formula& f1 = then_term.formula(); | ||
1466 | const Formula& f2 = else_term.formula(); | ||
1467 | yylhs.value.as < Term > () = (!cond || f1) && (cond || f2); | ||
1468 | } else { | ||
1469 | std::cerr << yystack_[5].location << " : Type mismatch in `if (c) then t1 else t2`:" << std::endl | ||
1470 | << " t1 = " << then_term << std::endl | ||
1471 | << " t2 = " << else_term << std::endl; | ||
1472 | YYABORT; | ||
1473 | } | ||
1474 | } | ||
1475 | #line 1476 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1476 | break; | ||
1477 | |||
1478 | case 58: | ||
1479 | #line 364 "dreal/smt2/parser.yy" | ||
1480 | { | ||
1481 | const Variables& vars = yystack_[4].value.as < std::pair<Variables, Formula> > ().first; | ||
1482 | const Formula& domain = yystack_[4].value.as < std::pair<Variables, Formula> > ().second; | ||
1483 | const Formula body = Smt2Driver::EliminateBooleanVariables(vars, yystack_[2].value.as < Term > ().formula()); | ||
1484 | const Variables quantified_variables = intersect(vars, body.GetFreeVariables()); | ||
1485 | if (quantified_variables.empty()) { | ||
1486 | yylhs.value.as < Term > () = body; | ||
1487 | } else { | ||
1488 | yylhs.value.as < Term > () = forall(quantified_variables, imply(domain, body)); | ||
1489 | } | ||
1490 | } | ||
1491 | #line 1492 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1492 | break; | ||
1493 | |||
1494 | case 59: | ||
1495 | #line 375 "dreal/smt2/parser.yy" | ||
1496 | { | ||
1497 | yylhs.value.as < Term > () = yystack_[2].value.as < Term > (); | ||
1498 | } | ||
1499 | #line 1500 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1500 | break; | ||
1501 | |||
1502 | case 60: | ||
1503 | #line 378 "dreal/smt2/parser.yy" | ||
1504 | { | ||
1505 | const Box::Interval i{StringToInterval(yystack_[0].value.as < std::string > ())}; | ||
1506 | const double parsed{std::stod(yystack_[0].value.as < std::string > ())}; | ||
1507 | if (i.diam() == 0) { | ||
1508 | // point => floating-point constant expression. | ||
1509 | yylhs.value.as < Term > () = i.mid(); | ||
1510 | } else { | ||
1511 | // interval => real constant expression. | ||
1512 | yylhs.value.as < Term > () = real_constant(i.lb(), i.ub(), i.lb() == parsed); | ||
1513 | } | ||
1514 | } | ||
1515 | #line 1516 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1516 | break; | ||
1517 | |||
1518 | case 61: | ||
1519 | #line 389 "dreal/smt2/parser.yy" | ||
1520 | { yylhs.value.as < Term > () = yystack_[0].value.as < double > (); } | ||
1521 | #line 1522 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1522 | break; | ||
1523 | |||
1524 | case 62: | ||
1525 | #line 390 "dreal/smt2/parser.yy" | ||
1526 | { yylhs.value.as < Term > () = convert_int64_to_double(yystack_[0].value.as < std::int64_t > ()); } | ||
1527 | #line 1528 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1528 | break; | ||
1529 | |||
1530 | case 63: | ||
1531 | #line 391 "dreal/smt2/parser.yy" | ||
1532 | { | ||
1533 | try { | ||
1534 | const Variable& var = driver.lookup_variable(yystack_[0].value.as < std::string > ()); | ||
1535 | if (var.get_type() == Variable::Type::BOOLEAN) { | ||
1536 | yylhs.value.as < Term > () = Formula(var); | ||
1537 | } else { | ||
1538 | yylhs.value.as < Term > () = Expression(var); | ||
1539 | } | ||
1540 | } catch (std::runtime_error& e) { | ||
1541 | std::cerr << yystack_[0].location << " : " << e.what() << std::endl; | ||
1542 | YYABORT; | ||
1543 | } | ||
1544 | } | ||
1545 | #line 1546 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1546 | break; | ||
1547 | |||
1548 | case 64: | ||
1549 | #line 404 "dreal/smt2/parser.yy" | ||
1550 | { | ||
1551 | yylhs.value.as < Term > () = yystack_[1].value.as < Term > (); | ||
1552 | } | ||
1553 | #line 1554 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1554 | break; | ||
1555 | |||
1556 | case 65: | ||
1557 | #line 407 "dreal/smt2/parser.yy" | ||
1558 | { | ||
1559 | for (const Term& term : yystack_[1].value.as < std::vector<Term> > ()) { | ||
1560 | yystack_[2].value.as < Term > ().mutable_expression() += term.expression(); | ||
1561 | } | ||
1562 | yylhs.value.as < Term > () = yystack_[2].value.as < Term > (); | ||
1563 | } | ||
1564 | #line 1565 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1565 | break; | ||
1566 | |||
1567 | case 66: | ||
1568 | #line 413 "dreal/smt2/parser.yy" | ||
1569 | { | ||
1570 | yylhs.value.as < Term > () = - yystack_[1].value.as < Term > ().expression(); | ||
1571 | } | ||
1572 | #line 1573 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1573 | break; | ||
1574 | |||
1575 | case 67: | ||
1576 | #line 416 "dreal/smt2/parser.yy" | ||
1577 | { | ||
1578 | for (const Term& term : yystack_[1].value.as < std::vector<Term> > ()) { | ||
1579 | yystack_[2].value.as < Term > ().mutable_expression() -= term.expression(); | ||
1580 | } | ||
1581 | yylhs.value.as < Term > () = yystack_[2].value.as < Term > (); | ||
1582 | } | ||
1583 | #line 1584 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1584 | break; | ||
1585 | |||
1586 | case 68: | ||
1587 | #line 422 "dreal/smt2/parser.yy" | ||
1588 | { | ||
1589 | for (const Term& term : yystack_[1].value.as < std::vector<Term> > ()) { | ||
1590 | yystack_[2].value.as < Term > ().mutable_expression() *= term.expression(); | ||
1591 | } | ||
1592 | yylhs.value.as < Term > () = yystack_[2].value.as < Term > (); | ||
1593 | } | ||
1594 | #line 1595 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1595 | break; | ||
1596 | |||
1597 | case 69: | ||
1598 | #line 428 "dreal/smt2/parser.yy" | ||
1599 | { | ||
1600 | for (const Term& term : yystack_[1].value.as < std::vector<Term> > ()) { | ||
1601 | yystack_[2].value.as < Term > ().mutable_expression() /= term.expression(); | ||
1602 | } | ||
1603 | yylhs.value.as < Term > () = yystack_[2].value.as < Term > (); | ||
1604 | } | ||
1605 | #line 1606 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1606 | break; | ||
1607 | |||
1608 | case 70: | ||
1609 | #line 434 "dreal/smt2/parser.yy" | ||
1610 | { | ||
1611 | yylhs.value.as < Term > () = exp(yystack_[1].value.as < Term > ().expression()); | ||
1612 | } | ||
1613 | #line 1614 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1614 | break; | ||
1615 | |||
1616 | case 71: | ||
1617 | #line 437 "dreal/smt2/parser.yy" | ||
1618 | { | ||
1619 | yylhs.value.as < Term > () = log(yystack_[1].value.as < Term > ().expression()); | ||
1620 | } | ||
1621 | #line 1622 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1622 | break; | ||
1623 | |||
1624 | case 72: | ||
1625 | #line 440 "dreal/smt2/parser.yy" | ||
1626 | { | ||
1627 | yylhs.value.as < Term > () = abs(yystack_[1].value.as < Term > ().expression()); | ||
1628 | } | ||
1629 | #line 1630 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1630 | break; | ||
1631 | |||
1632 | case 73: | ||
1633 | #line 443 "dreal/smt2/parser.yy" | ||
1634 | { | ||
1635 | yylhs.value.as < Term > () = sin(yystack_[1].value.as < Term > ().expression()); | ||
1636 | } | ||
1637 | #line 1638 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1638 | break; | ||
1639 | |||
1640 | case 74: | ||
1641 | #line 446 "dreal/smt2/parser.yy" | ||
1642 | { | ||
1643 | yylhs.value.as < Term > () = cos(yystack_[1].value.as < Term > ().expression()); | ||
1644 | } | ||
1645 | #line 1646 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1646 | break; | ||
1647 | |||
1648 | case 75: | ||
1649 | #line 449 "dreal/smt2/parser.yy" | ||
1650 | { | ||
1651 | yylhs.value.as < Term > () = tan(yystack_[1].value.as < Term > ().expression()); | ||
1652 | } | ||
1653 | #line 1654 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1654 | break; | ||
1655 | |||
1656 | case 76: | ||
1657 | #line 452 "dreal/smt2/parser.yy" | ||
1658 | { | ||
1659 | yylhs.value.as < Term > () = asin(yystack_[1].value.as < Term > ().expression()); | ||
1660 | } | ||
1661 | #line 1662 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1662 | break; | ||
1663 | |||
1664 | case 77: | ||
1665 | #line 455 "dreal/smt2/parser.yy" | ||
1666 | { | ||
1667 | yylhs.value.as < Term > () = acos(yystack_[1].value.as < Term > ().expression()); | ||
1668 | } | ||
1669 | #line 1670 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1670 | break; | ||
1671 | |||
1672 | case 78: | ||
1673 | #line 458 "dreal/smt2/parser.yy" | ||
1674 | { | ||
1675 | yylhs.value.as < Term > () = atan(yystack_[1].value.as < Term > ().expression()); | ||
1676 | } | ||
1677 | #line 1678 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1678 | break; | ||
1679 | |||
1680 | case 79: | ||
1681 | #line 461 "dreal/smt2/parser.yy" | ||
1682 | { | ||
1683 | yylhs.value.as < Term > () = atan2(yystack_[2].value.as < Term > ().expression(), yystack_[1].value.as < Term > ().expression()); | ||
1684 | } | ||
1685 | #line 1686 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1686 | break; | ||
1687 | |||
1688 | case 80: | ||
1689 | #line 464 "dreal/smt2/parser.yy" | ||
1690 | { | ||
1691 | yylhs.value.as < Term > () = sinh(yystack_[1].value.as < Term > ().expression()); | ||
1692 | } | ||
1693 | #line 1694 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1694 | break; | ||
1695 | |||
1696 | case 81: | ||
1697 | #line 467 "dreal/smt2/parser.yy" | ||
1698 | { | ||
1699 | yylhs.value.as < Term > () = cosh(yystack_[1].value.as < Term > ().expression()); | ||
1700 | } | ||
1701 | #line 1702 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1702 | break; | ||
1703 | |||
1704 | case 82: | ||
1705 | #line 470 "dreal/smt2/parser.yy" | ||
1706 | { | ||
1707 | yylhs.value.as < Term > () = tanh(yystack_[1].value.as < Term > ().expression()); | ||
1708 | } | ||
1709 | #line 1710 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1710 | break; | ||
1711 | |||
1712 | case 83: | ||
1713 | #line 473 "dreal/smt2/parser.yy" | ||
1714 | { | ||
1715 | yylhs.value.as < Term > () = min(yystack_[2].value.as < Term > ().expression(), yystack_[1].value.as < Term > ().expression()); | ||
1716 | } | ||
1717 | #line 1718 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1718 | break; | ||
1719 | |||
1720 | case 84: | ||
1721 | #line 476 "dreal/smt2/parser.yy" | ||
1722 | { | ||
1723 | yylhs.value.as < Term > () = max(yystack_[2].value.as < Term > ().expression(), yystack_[1].value.as < Term > ().expression()); | ||
1724 | } | ||
1725 | #line 1726 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1726 | break; | ||
1727 | |||
1728 | case 85: | ||
1729 | #line 479 "dreal/smt2/parser.yy" | ||
1730 | { | ||
1731 | yylhs.value.as < Term > () = sqrt(yystack_[1].value.as < Term > ().expression()); | ||
1732 | } | ||
1733 | #line 1734 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1734 | break; | ||
1735 | |||
1736 | case 86: | ||
1737 | #line 482 "dreal/smt2/parser.yy" | ||
1738 | { | ||
1739 | yylhs.value.as < Term > () = pow(yystack_[2].value.as < Term > ().expression(), yystack_[1].value.as < Term > ().expression()); | ||
1740 | } | ||
1741 | #line 1742 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1742 | break; | ||
1743 | |||
1744 | case 87: | ||
1745 | #line 485 "dreal/smt2/parser.yy" | ||
1746 | { | ||
1747 | yylhs.value.as < Term > () = driver.LookupFunction(yystack_[2].value.as < std::string > (), yystack_[1].value.as < std::vector<Term> > ()); | ||
1748 | } | ||
1749 | #line 1750 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1750 | break; | ||
1751 | |||
1752 | case 88: | ||
1753 | #line 490 "dreal/smt2/parser.yy" | ||
1754 | { | ||
1755 | // Locals must be bound simultaneously. | ||
1756 | for (auto& binding : yystack_[1].value.as < std::vector<std::pair<std::string, Term>> > ()) { | ||
1757 | const std::string& name{ binding.first }; | ||
1758 | const Term& term{ binding.second }; | ||
1759 | const bool is_formula = term.type() == Term::Type::FORMULA; | ||
1760 | const Sort sort = is_formula ? Sort::Bool : Sort::Real; | ||
1761 | const Variable v{ driver.DeclareLocalVariable(name, sort) }; | ||
1762 | if (is_formula) { | ||
1763 | const Formula fv{v}; | ||
1764 | const Formula& ft{ term.formula() }; | ||
1765 | driver.mutable_context().Assert((fv && ft) || (!fv && !ft)); | ||
1766 | } else { | ||
1767 | driver.mutable_context().Assert(Expression{v} == term.expression()); | ||
1768 | } | ||
1769 | } | ||
1770 | } | ||
1771 | #line 1772 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1772 | break; | ||
1773 | |||
1774 | case 89: | ||
1775 | #line 509 "dreal/smt2/parser.yy" | ||
1776 | { | ||
1777 | driver.PushScope(); | ||
1778 | } | ||
1779 | #line 1780 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1780 | break; | ||
1781 | |||
1782 | case 90: | ||
1783 | #line 514 "dreal/smt2/parser.yy" | ||
1784 | { | ||
1785 | driver.PopScope(); | ||
1786 | } | ||
1787 | #line 1788 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1788 | break; | ||
1789 | |||
1790 | case 91: | ||
1791 | #line 519 "dreal/smt2/parser.yy" | ||
1792 | { | ||
1793 | yylhs.value.as < Variable > () = Variable{driver.DeclareLocalVariable(yystack_[2].value.as < std::string > (), yystack_[1].value.as < dreal::Sort > ())}; | ||
1794 | } | ||
1795 | #line 1796 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1796 | break; | ||
1797 | |||
1798 | case 92: | ||
1799 | #line 524 "dreal/smt2/parser.yy" | ||
1800 | { yylhs.value.as < std::vector<Variable> > () = std::vector<Variable>{}; } | ||
1801 | #line 1802 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1802 | break; | ||
1803 | |||
1804 | case 93: | ||
1805 | #line 525 "dreal/smt2/parser.yy" | ||
1806 | { | ||
1807 | const Variable& v = yystack_[1].value.as < Variable > (); | ||
1808 | yystack_[0].value.as < std::vector<Variable> > ().push_back(v); | ||
1809 | yylhs.value.as < std::vector<Variable> > () = yystack_[0].value.as < std::vector<Variable> > (); | ||
1810 | } | ||
1811 | #line 1812 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1812 | break; | ||
1813 | |||
1814 | case 94: | ||
1815 | #line 533 "dreal/smt2/parser.yy" | ||
1816 | { yylhs.value.as < std::pair<Variables, Formula> > () = std::pair<Variables, Formula>(Variables{}, Formula::True()); } | ||
1817 | #line 1818 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1818 | break; | ||
1819 | |||
1820 | case 95: | ||
1821 | #line 534 "dreal/smt2/parser.yy" | ||
1822 | { | ||
1823 | const Variable& v = std::get<0>(yystack_[1].value.as < std::tuple<Variable, double, double> > ()); | ||
1824 | const double lb = std::get<1>(yystack_[1].value.as < std::tuple<Variable, double, double> > ()); | ||
1825 | const double ub = std::get<2>(yystack_[1].value.as < std::tuple<Variable, double, double> > ()); | ||
1826 | yystack_[0].value.as < std::pair<Variables, Formula> > ().first.insert(v); | ||
1827 | if (std::isfinite(lb)) { | ||
1828 | yystack_[0].value.as < std::pair<Variables, Formula> > ().second = yystack_[0].value.as < std::pair<Variables, Formula> > ().second && (lb <= v); | ||
1829 | } | ||
1830 | if (std::isfinite(ub)) { | ||
1831 | yystack_[0].value.as < std::pair<Variables, Formula> > ().second = yystack_[0].value.as < std::pair<Variables, Formula> > ().second && (v <= ub); | ||
1832 | } | ||
1833 | yylhs.value.as < std::pair<Variables, Formula> > () = yystack_[0].value.as < std::pair<Variables, Formula> > (); | ||
1834 | } | ||
1835 | #line 1836 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1836 | break; | ||
1837 | |||
1838 | case 96: | ||
1839 | #line 549 "dreal/smt2/parser.yy" | ||
1840 | { | ||
1841 | const Variable v = driver.RegisterVariable(yystack_[2].value.as < std::string > (), yystack_[1].value.as < dreal::Sort > ()); | ||
1842 | const double inf = std::numeric_limits<double>::infinity(); | ||
1843 | yylhs.value.as < std::tuple<Variable, double, double> > () = std::tuple<Variable, double, double>(v, -inf, inf); | ||
1844 | } | ||
1845 | #line 1846 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1846 | break; | ||
1847 | |||
1848 | case 97: | ||
1849 | #line 554 "dreal/smt2/parser.yy" | ||
1850 | { | ||
1851 | const Variable v = driver.RegisterVariable(yystack_[7].value.as < std::string > (), yystack_[6].value.as < dreal::Sort > ()); | ||
1852 | const double lb = yystack_[4].value.as < Term > ().expression().Evaluate(); | ||
1853 | const double ub = yystack_[2].value.as < Term > ().expression().Evaluate(); | ||
1854 | yylhs.value.as < std::tuple<Variable, double, double> > () = std::tuple<Variable, double, double>(v, lb, ub); | ||
1855 | } | ||
1856 | #line 1857 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1857 | break; | ||
1858 | |||
1859 | case 98: | ||
1860 | #line 562 "dreal/smt2/parser.yy" | ||
1861 | { yylhs.value.as < dreal::Sort > () = ParseSort(yystack_[0].value.as < std::string > ()); } | ||
1862 | #line 1863 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1863 | break; | ||
1864 | |||
1865 | case 99: | ||
1866 | #line 565 "dreal/smt2/parser.yy" | ||
1867 | { | ||
1868 | yylhs.value.as < std::vector<std::pair<std::string, Term>> > () = std::vector<std::pair<std::string, Term>>{}; | ||
1869 | } | ||
1870 | #line 1871 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1871 | break; | ||
1872 | |||
1873 | case 100: | ||
1874 | #line 568 "dreal/smt2/parser.yy" | ||
1875 | { | ||
1876 | yystack_[0].value.as < std::vector<std::pair<std::string, Term>> > ().push_back(yystack_[1].value.as < std::pair<std::string, Term> > ()); | ||
1877 | yylhs.value.as < std::vector<std::pair<std::string, Term>> > () = yystack_[0].value.as < std::vector<std::pair<std::string, Term>> > (); | ||
1878 | } | ||
1879 | #line 1880 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1880 | break; | ||
1881 | |||
1882 | case 101: | ||
1883 | #line 574 "dreal/smt2/parser.yy" | ||
1884 | { | ||
1885 | yylhs.value.as < std::pair<std::string, Term> > () = std::pair<std::string, Term>(yystack_[2].value.as < std::string > (), yystack_[1].value.as < Term > ()); | ||
1886 | } | ||
1887 | #line 1888 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1888 | break; | ||
1889 | |||
1890 | |||
1891 | #line 1892 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
1892 | |||
1893 | default: | ||
1894 | break; | ||
1895 | } | ||
1896 | } | ||
1897 | #if YY_EXCEPTIONS | ||
1898 | catch (const syntax_error& yyexc) | ||
1899 | { | ||
1900 | YYCDEBUG << "Caught exception: " << yyexc.what() << '\n'; | ||
1901 | error (yyexc); | ||
1902 | YYERROR; | ||
1903 | } | ||
1904 | #endif // YY_EXCEPTIONS | ||
1905 | YY_SYMBOL_PRINT ("-> $$ =", yylhs); | ||
1906 | yypop_ (yylen); | ||
1907 | yylen = 0; | ||
1908 | YY_STACK_PRINT (); | ||
1909 | |||
1910 | // Shift the result of the reduction. | ||
1911 | yypush_ (YY_NULLPTR, YY_MOVE (yylhs)); | ||
1912 | } | ||
1913 | goto yynewstate; | ||
1914 | |||
1915 | |||
1916 | /*--------------------------------------. | ||
1917 | | yyerrlab -- here on detecting error. | | ||
1918 | `--------------------------------------*/ | ||
1919 | yyerrlab: | ||
1920 | // If not already recovering from an error, report this error. | ||
1921 | if (!yyerrstatus_) | ||
1922 | { | ||
1923 | ++yynerrs_; | ||
1924 | error (yyla.location, yysyntax_error_ (yystack_[0].state, yyla)); | ||
1925 | } | ||
1926 | |||
1927 | |||
1928 | yyerror_range[1].location = yyla.location; | ||
1929 | if (yyerrstatus_ == 3) | ||
1930 | { | ||
1931 | /* If just tried and failed to reuse lookahead token after an | ||
1932 | error, discard it. */ | ||
1933 | |||
1934 | // Return failure if at end of input. | ||
1935 | if (yyla.type_get () == yyeof_) | ||
1936 | YYABORT; | ||
1937 | else if (!yyla.empty ()) | ||
1938 | { | ||
1939 | yy_destroy_ ("Error: discarding", yyla); | ||
1940 | yyla.clear (); | ||
1941 | } | ||
1942 | } | ||
1943 | |||
1944 | // Else will try to reuse lookahead token after shifting the error token. | ||
1945 | goto yyerrlab1; | ||
1946 | |||
1947 | |||
1948 | /*---------------------------------------------------. | ||
1949 | | yyerrorlab -- error raised explicitly by YYERROR. | | ||
1950 | `---------------------------------------------------*/ | ||
1951 | yyerrorlab: | ||
1952 | /* Pacify compilers when the user code never invokes YYERROR and | ||
1953 | the label yyerrorlab therefore never appears in user code. */ | ||
1954 | if (false) | ||
1955 | YYERROR; | ||
1956 | |||
1957 | /* Do not reclaim the symbols of the rule whose action triggered | ||
1958 | this YYERROR. */ | ||
1959 | yypop_ (yylen); | ||
1960 | yylen = 0; | ||
1961 | goto yyerrlab1; | ||
1962 | |||
1963 | |||
1964 | /*-------------------------------------------------------------. | ||
1965 | | yyerrlab1 -- common code for both syntax error and YYERROR. | | ||
1966 | `-------------------------------------------------------------*/ | ||
1967 | yyerrlab1: | ||
1968 | yyerrstatus_ = 3; // Each real token shifted decrements this. | ||
1969 | { | ||
1970 | stack_symbol_type error_token; | ||
1971 | for (;;) | ||
1972 | { | ||
1973 | yyn = yypact_[yystack_[0].state]; | ||
1974 | if (!yy_pact_value_is_default_ (yyn)) | ||
1975 | { | ||
1976 | yyn += yy_error_token_; | ||
1977 | if (0 <= yyn && yyn <= yylast_ && yycheck_[yyn] == yy_error_token_) | ||
1978 | { | ||
1979 | yyn = yytable_[yyn]; | ||
1980 | if (0 < yyn) | ||
1981 | break; | ||
1982 | } | ||
1983 | } | ||
1984 | |||
1985 | // Pop the current state because it cannot handle the error token. | ||
1986 | if (yystack_.size () == 1) | ||
1987 | YYABORT; | ||
1988 | |||
1989 | yyerror_range[1].location = yystack_[0].location; | ||
1990 | yy_destroy_ ("Error: popping", yystack_[0]); | ||
1991 | yypop_ (); | ||
1992 | YY_STACK_PRINT (); | ||
1993 | } | ||
1994 | |||
1995 | yyerror_range[2].location = yyla.location; | ||
1996 | YYLLOC_DEFAULT (error_token.location, yyerror_range, 2); | ||
1997 | |||
1998 | // Shift the error token. | ||
1999 | error_token.state = static_cast<state_type> (yyn); | ||
2000 | yypush_ ("Shifting", YY_MOVE (error_token)); | ||
2001 | } | ||
2002 | goto yynewstate; | ||
2003 | |||
2004 | |||
2005 | /*-------------------------------------. | ||
2006 | | yyacceptlab -- YYACCEPT comes here. | | ||
2007 | `-------------------------------------*/ | ||
2008 | yyacceptlab: | ||
2009 | yyresult = 0; | ||
2010 | goto yyreturn; | ||
2011 | |||
2012 | |||
2013 | /*-----------------------------------. | ||
2014 | | yyabortlab -- YYABORT comes here. | | ||
2015 | `-----------------------------------*/ | ||
2016 | yyabortlab: | ||
2017 | yyresult = 1; | ||
2018 | goto yyreturn; | ||
2019 | |||
2020 | |||
2021 | /*-----------------------------------------------------. | ||
2022 | | yyreturn -- parsing is finished, return the result. | | ||
2023 | `-----------------------------------------------------*/ | ||
2024 | yyreturn: | ||
2025 | if (!yyla.empty ()) | ||
2026 | yy_destroy_ ("Cleanup: discarding lookahead", yyla); | ||
2027 | |||
2028 | /* Do not reclaim the symbols of the rule whose action triggered | ||
2029 | this YYABORT or YYACCEPT. */ | ||
2030 | yypop_ (yylen); | ||
2031 | while (1 < yystack_.size ()) | ||
2032 | { | ||
2033 | yy_destroy_ ("Cleanup: popping", yystack_[0]); | ||
2034 | yypop_ (); | ||
2035 | } | ||
2036 | |||
2037 | return yyresult; | ||
2038 | } | ||
2039 | #if YY_EXCEPTIONS | ||
2040 | catch (...) | ||
2041 | { | ||
2042 | YYCDEBUG << "Exception caught: cleaning lookahead and stack\n"; | ||
2043 | // Do not try to display the values of the reclaimed symbols, | ||
2044 | // as their printers might throw an exception. | ||
2045 | if (!yyla.empty ()) | ||
2046 | yy_destroy_ (YY_NULLPTR, yyla); | ||
2047 | |||
2048 | while (1 < yystack_.size ()) | ||
2049 | { | ||
2050 | yy_destroy_ (YY_NULLPTR, yystack_[0]); | ||
2051 | yypop_ (); | ||
2052 | } | ||
2053 | throw; | ||
2054 | } | ||
2055 | #endif // YY_EXCEPTIONS | ||
2056 | } | ||
2057 | |||
2058 | void | ||
2059 | Smt2Parser::error (const syntax_error& yyexc) | ||
2060 | { | ||
2061 | error (yyexc.location, yyexc.what ()); | ||
2062 | } | ||
2063 | |||
2064 | // Generate an error message. | ||
2065 | std::string | ||
2066 | Smt2Parser::yysyntax_error_ (state_type yystate, const symbol_type& yyla) const | ||
2067 | { | ||
2068 | // Number of reported tokens (one for the "unexpected", one per | ||
2069 | // "expected"). | ||
2070 | std::ptrdiff_t yycount = 0; | ||
2071 | // Its maximum. | ||
2072 | enum { YYERROR_VERBOSE_ARGS_MAXIMUM = 5 }; | ||
2073 | // Arguments of yyformat. | ||
2074 | char const *yyarg[YYERROR_VERBOSE_ARGS_MAXIMUM]; | ||
2075 | |||
2076 | /* There are many possibilities here to consider: | ||
2077 | - If this state is a consistent state with a default action, then | ||
2078 | the only way this function was invoked is if the default action | ||
2079 | is an error action. In that case, don't check for expected | ||
2080 | tokens because there are none. | ||
2081 | - The only way there can be no lookahead present (in yyla) is | ||
2082 | if this state is a consistent state with a default action. | ||
2083 | Thus, detecting the absence of a lookahead is sufficient to | ||
2084 | determine that there is no unexpected or expected token to | ||
2085 | report. In that case, just report a simple "syntax error". | ||
2086 | - Don't assume there isn't a lookahead just because this state is | ||
2087 | a consistent state with a default action. There might have | ||
2088 | been a previous inconsistent state, consistent state with a | ||
2089 | non-default action, or user semantic action that manipulated | ||
2090 | yyla. (However, yyla is currently not documented for users.) | ||
2091 | - Of course, the expected token list depends on states to have | ||
2092 | correct lookahead information, and it depends on the parser not | ||
2093 | to perform extra reductions after fetching a lookahead from the | ||
2094 | scanner and before detecting a syntax error. Thus, state merging | ||
2095 | (from LALR or IELR) and default reductions corrupt the expected | ||
2096 | token list. However, the list is correct for canonical LR with | ||
2097 | one exception: it will still contain any token that will not be | ||
2098 | accepted due to an error action in a later state. | ||
2099 | */ | ||
2100 | if (!yyla.empty ()) | ||
2101 | { | ||
2102 | symbol_number_type yytoken = yyla.type_get (); | ||
2103 | yyarg[yycount++] = yytname_[yytoken]; | ||
2104 | |||
2105 | int yyn = yypact_[yystate]; | ||
2106 | if (!yy_pact_value_is_default_ (yyn)) | ||
2107 | { | ||
2108 | /* Start YYX at -YYN if negative to avoid negative indexes in | ||
2109 | YYCHECK. In other words, skip the first -YYN actions for | ||
2110 | this state because they are default actions. */ | ||
2111 | int yyxbegin = yyn < 0 ? -yyn : 0; | ||
2112 | // Stay within bounds of both yycheck and yytname. | ||
2113 | int yychecklim = yylast_ - yyn + 1; | ||
2114 | int yyxend = yychecklim < yyntokens_ ? yychecklim : yyntokens_; | ||
2115 | for (int yyx = yyxbegin; yyx < yyxend; ++yyx) | ||
2116 | if (yycheck_[yyx + yyn] == yyx && yyx != yy_error_token_ | ||
2117 | && !yy_table_value_is_error_ (yytable_[yyx + yyn])) | ||
2118 | { | ||
2119 | if (yycount == YYERROR_VERBOSE_ARGS_MAXIMUM) | ||
2120 | { | ||
2121 | yycount = 1; | ||
2122 | break; | ||
2123 | } | ||
2124 | else | ||
2125 | yyarg[yycount++] = yytname_[yyx]; | ||
2126 | } | ||
2127 | } | ||
2128 | } | ||
2129 | |||
2130 | char const* yyformat = YY_NULLPTR; | ||
2131 | switch (yycount) | ||
2132 | { | ||
2133 | #define YYCASE_(N, S) \ | ||
2134 | case N: \ | ||
2135 | yyformat = S; \ | ||
2136 | break | ||
2137 | default: // Avoid compiler warnings. | ||
2138 | YYCASE_ (0, YY_("syntax error")); | ||
2139 | YYCASE_ (1, YY_("syntax error, unexpected %s")); | ||
2140 | YYCASE_ (2, YY_("syntax error, unexpected %s, expecting %s")); | ||
2141 | YYCASE_ (3, YY_("syntax error, unexpected %s, expecting %s or %s")); | ||
2142 | YYCASE_ (4, YY_("syntax error, unexpected %s, expecting %s or %s or %s")); | ||
2143 | YYCASE_ (5, YY_("syntax error, unexpected %s, expecting %s or %s or %s or %s")); | ||
2144 | #undef YYCASE_ | ||
2145 | } | ||
2146 | |||
2147 | std::string yyres; | ||
2148 | // Argument number. | ||
2149 | std::ptrdiff_t yyi = 0; | ||
2150 | for (char const* yyp = yyformat; *yyp; ++yyp) | ||
2151 | if (yyp[0] == '%' && yyp[1] == 's' && yyi < yycount) | ||
2152 | { | ||
2153 | yyres += yytnamerr_ (yyarg[yyi++]); | ||
2154 | ++yyp; | ||
2155 | } | ||
2156 | else | ||
2157 | yyres += *yyp; | ||
2158 | return yyres; | ||
2159 | } | ||
2160 | |||
2161 | |||
2162 | const short Smt2Parser::yypact_ninf_ = -250; | ||
2163 | |||
2164 | const signed char Smt2Parser::yytable_ninf_ = -1; | ||
2165 | |||
2166 | const short | ||
2167 | Smt2Parser::yypact_[] = | ||
2168 | { | ||
2169 | -61, 1, 25, 28, -61, -250, -250, -250, -250, -250, | ||
2170 | -250, -250, -250, -250, -250, -250, -250, -250, -250, -250, | ||
2171 | 261, -53, -48, -47, -43, -46, -42, -12, -13, -8, | ||
2172 | -4, -1, 5, 6, 261, 261, -250, -250, -250, -250, | ||
2173 | -250, -250, -250, -250, -250, 209, 2, -250, 12, 10, | ||
2174 | -250, -250, -250, 13, 261, 14, 15, -54, 16, -60, | ||
2175 | 17, 26, -250, -250, 261, 261, 261, 261, 261, 261, | ||
2176 | 261, 261, 261, 261, 261, 261, 261, 261, 261, 261, | ||
2177 | 261, 261, 261, 261, 261, 261, 261, 261, 261, 261, | ||
2178 | 261, 261, 261, 261, 261, 261, 261, -250, -250, -82, | ||
2179 | 27, 29, -250, 11, -250, -250, -250, 30, 31, 33, | ||
2180 | -250, 34, 35, 38, 44, -250, -250, 48, 50, 76, | ||
2181 | 90, 261, 261, 261, 261, 261, 261, 261, 51, 56, | ||
2182 | 57, 58, 61, 63, 65, 77, 78, 261, 79, 80, | ||
2183 | 87, 261, 261, 88, 261, 98, 116, 124, 261, 95, | ||
2184 | 261, 146, -250, 261, 12, 102, 103, -250, -250, -250, | ||
2185 | -250, -250, -250, -250, -250, 105, 106, 261, -250, 217, | ||
2186 | -250, 225, 239, 247, 113, 114, 121, 122, 125, -250, | ||
2187 | -250, -250, -250, -250, -250, -250, -250, -250, 127, -250, | ||
2188 | -250, -250, 131, 132, -250, 134, -250, -250, -250, 138, | ||
2189 | -250, 261, -250, 100, -80, 54, 102, 144, -250, 110, | ||
2190 | 147, 105, 152, 150, 106, -250, -250, -250, -250, -250, | ||
2191 | -250, -250, -250, -250, -250, -250, -250, -250, -250, -250, | ||
2192 | 151, 261, -250, 261, 12, -250, 12, 12, 261, -250, | ||
2193 | 261, -250, -250, 154, -250, 9, 153, 156, 261, -75, | ||
2194 | -250, 157, -250, 158, 261, -250, -250, -250, 261, 159, | ||
2195 | -250, -250, 149, 160, 162, -250, 161, -250, 261, -250, | ||
2196 | 189, 165, -250 | ||
2197 | }; | ||
2198 | |||
2199 | const signed char | ||
2200 | Smt2Parser::yydefact_[] = | ||
2201 | { | ||
2202 | 0, 0, 0, 0, 3, 5, 6, 7, 8, 9, | ||
2203 | 10, 11, 12, 13, 16, 17, 18, 19, 15, 14, | ||
2204 | 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, | ||
2205 | 0, 0, 0, 0, 0, 0, 1, 2, 4, 45, | ||
2206 | 46, 60, 61, 62, 63, 0, 0, 21, 0, 0, | ||
2207 | 89, 27, 28, 0, 0, 0, 0, 0, 0, 0, | ||
2208 | 0, 0, 89, 89, 0, 0, 0, 0, 0, 0, | ||
2209 | 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, | ||
2210 | 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, | ||
2211 | 0, 0, 0, 0, 0, 0, 0, 20, 98, 0, | ||
2212 | 0, 0, 40, 0, 43, 42, 41, 0, 0, 0, | ||
2213 | 35, 0, 0, 0, 0, 30, 31, 0, 0, 0, | ||
2214 | 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, | ||
2215 | 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, | ||
2216 | 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, | ||
2217 | 0, 0, 24, 0, 0, 92, 0, 44, 34, 32, | ||
2218 | 33, 38, 39, 37, 36, 94, 99, 0, 64, 0, | ||
2219 | 66, 0, 0, 0, 0, 0, 0, 0, 0, 70, | ||
2220 | 71, 72, 73, 74, 75, 76, 77, 78, 0, 80, | ||
2221 | 81, 82, 0, 0, 85, 0, 52, 53, 54, 0, | ||
2222 | 55, 0, 87, 0, 0, 0, 92, 0, 29, 0, | ||
2223 | 0, 94, 0, 0, 99, 90, 65, 67, 68, 69, | ||
2224 | 47, 49, 51, 48, 50, 79, 83, 84, 86, 56, | ||
2225 | 0, 0, 22, 0, 0, 93, 0, 0, 0, 95, | ||
2226 | 0, 88, 100, 0, 57, 0, 0, 0, 0, 0, | ||
2227 | 90, 0, 59, 0, 0, 91, 90, 96, 0, 0, | ||
2228 | 101, 25, 0, 0, 0, 58, 0, 26, 0, 23, | ||
2229 | 0, 0, 97 | ||
2230 | }; | ||
2231 | |||
2232 | const short | ||
2233 | Smt2Parser::yypgoto_[] = | ||
2234 | { | ||
2235 | -250, -250, 243, -250, -250, -250, -250, -250, -250, -250, | ||
2236 | -250, -250, -250, -250, -250, -250, -250, -250, -250, 18, | ||
2237 | -20, -250, -50, -249, -250, 72, 81, -250, -152, 73, | ||
2238 | -250 | ||
2239 | }; | ||
2240 | |||
2241 | const short | ||
2242 | Smt2Parser::yydefgoto_[] = | ||
2243 | { | ||
2244 | -1, 2, 3, 4, 5, 6, 7, 8, 9, 10, | ||
2245 | 11, 12, 13, 14, 15, 16, 17, 18, 19, 103, | ||
2246 | 104, 167, 101, 243, 206, 207, 210, 211, 99, 213, | ||
2247 | 214 | ||
2248 | }; | ||
2249 | |||
2250 | const short | ||
2251 | Smt2Parser::yytable_[] = | ||
2252 | { | ||
2253 | 46, 259, 204, 152, 153, 232, 233, 263, 111, 112, | ||
2254 | 257, 258, 117, 118, 60, 61, 20, 21, 113, 22, | ||
2255 | 23, 114, 24, 1, 107, 36, 25, 108, 37, 109, | ||
2256 | 26, 27, 47, 48, 49, 28, 29, 30, 50, 51, | ||
2257 | 31, 32, 33, 52, 119, 120, 121, 122, 123, 124, | ||
2258 | 125, 126, 127, 128, 129, 130, 131, 132, 133, 134, | ||
2259 | 135, 136, 137, 138, 139, 140, 141, 142, 143, 144, | ||
2260 | 53, 54, 55, 148, 149, 150, 56, 34, 35, 39, | ||
2261 | 40, 57, 247, 157, 248, 249, 58, 97, 59, 41, | ||
2262 | 42, 43, 44, 98, 100, 45, 156, 253, 102, 105, | ||
2263 | 106, 110, 115, 174, 175, 176, 177, 178, 145, 146, | ||
2264 | 147, 116, 154, 155, 151, 158, 159, 188, 160, 161, | ||
2265 | 162, 192, 193, 163, 195, 157, 157, 157, 199, 164, | ||
2266 | 201, 157, 165, 203, 166, 234, 179, 169, 171, 172, | ||
2267 | 173, 180, 181, 182, 39, 40, 183, 215, 184, 157, | ||
2268 | 185, 157, 157, 157, 41, 42, 43, 44, 39, 40, | ||
2269 | 45, 168, 186, 187, 189, 190, 39, 40, 41, 42, | ||
2270 | 43, 44, 191, 194, 45, 170, 41, 42, 43, 44, | ||
2271 | 200, 230, 45, 196, 39, 40, 205, 231, 208, 209, | ||
2272 | 212, 237, 39, 40, 41, 42, 43, 44, 220, 221, | ||
2273 | 45, 197, 41, 42, 43, 44, 222, 223, 45, 198, | ||
2274 | 224, 245, 225, 246, 39, 40, 226, 227, 250, 228, | ||
2275 | 251, 62, 63, 229, 41, 42, 43, 44, 256, 236, | ||
2276 | 45, 202, 238, 240, 262, 241, 244, 266, 264, 252, | ||
2277 | 254, 255, 260, 261, 265, 267, 269, 38, 270, 268, | ||
2278 | 272, 64, 65, 66, 67, 68, 69, 70, 71, 72, | ||
2279 | 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, | ||
2280 | 83, 84, 85, 86, 87, 88, 89, 271, 235, 90, | ||
2281 | 91, 92, 93, 94, 95, 39, 40, 242, 0, 0, | ||
2282 | 96, 0, 239, 39, 40, 41, 42, 43, 44, 0, | ||
2283 | 0, 45, 216, 41, 42, 43, 44, 39, 40, 45, | ||
2284 | 217, 0, 0, 0, 0, 39, 40, 41, 42, 43, | ||
2285 | 44, 0, 0, 45, 218, 41, 42, 43, 44, 39, | ||
2286 | 40, 45, 219, 0, 0, 0, 0, 0, 0, 41, | ||
2287 | 42, 43, 44, 0, 0, 45 | ||
2288 | }; | ||
2289 | |||
2290 | const short | ||
2291 | Smt2Parser::yycheck_[] = | ||
2292 | { | ||
2293 | 20, 250, 154, 85, 86, 85, 86, 256, 68, 69, | ||
2294 | 85, 86, 62, 63, 34, 35, 15, 16, 78, 18, | ||
2295 | 19, 81, 21, 84, 78, 0, 25, 81, 0, 83, | ||
2296 | 29, 30, 85, 81, 81, 34, 35, 36, 81, 85, | ||
2297 | 39, 40, 41, 85, 64, 65, 66, 67, 68, 69, | ||
2298 | 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, | ||
2299 | 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, | ||
2300 | 82, 84, 80, 93, 94, 95, 80, 76, 77, 68, | ||
2301 | 69, 82, 234, 103, 236, 237, 81, 85, 82, 78, | ||
2302 | 79, 80, 81, 81, 84, 84, 85, 88, 85, 85, | ||
2303 | 85, 85, 85, 123, 124, 125, 126, 127, 90, 91, | ||
2304 | 92, 85, 85, 84, 96, 85, 85, 137, 85, 85, | ||
2305 | 85, 141, 142, 85, 144, 145, 146, 147, 148, 85, | ||
2306 | 150, 151, 84, 153, 84, 81, 85, 119, 120, 121, | ||
2307 | 122, 85, 85, 85, 68, 69, 85, 167, 85, 169, | ||
2308 | 85, 171, 172, 173, 78, 79, 80, 81, 68, 69, | ||
2309 | 84, 85, 85, 85, 85, 85, 68, 69, 78, 79, | ||
2310 | 80, 81, 85, 85, 84, 85, 78, 79, 80, 81, | ||
2311 | 85, 201, 84, 85, 68, 69, 84, 87, 85, 84, | ||
2312 | 84, 81, 68, 69, 78, 79, 80, 81, 85, 85, | ||
2313 | 84, 85, 78, 79, 80, 81, 85, 85, 84, 85, | ||
2314 | 85, 231, 85, 233, 68, 69, 85, 85, 238, 85, | ||
2315 | 240, 12, 13, 85, 78, 79, 80, 81, 248, 85, | ||
2316 | 84, 85, 85, 81, 254, 85, 85, 88, 258, 85, | ||
2317 | 87, 85, 85, 85, 85, 85, 85, 4, 268, 87, | ||
2318 | 85, 42, 43, 44, 45, 46, 47, 48, 49, 50, | ||
2319 | 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, | ||
2320 | 61, 62, 63, 64, 65, 66, 67, 88, 206, 70, | ||
2321 | 71, 72, 73, 74, 75, 68, 69, 214, -1, -1, | ||
2322 | 81, -1, 211, 68, 69, 78, 79, 80, 81, -1, | ||
2323 | -1, 84, 85, 78, 79, 80, 81, 68, 69, 84, | ||
2324 | 85, -1, -1, -1, -1, 68, 69, 78, 79, 80, | ||
2325 | 81, -1, -1, 84, 85, 78, 79, 80, 81, 68, | ||
2326 | 69, 84, 85, -1, -1, -1, -1, -1, -1, 78, | ||
2327 | 79, 80, 81, -1, -1, 84 | ||
2328 | }; | ||
2329 | |||
2330 | const signed char | ||
2331 | Smt2Parser::yystos_[] = | ||
2332 | { | ||
2333 | 0, 84, 90, 91, 92, 93, 94, 95, 96, 97, | ||
2334 | 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, | ||
2335 | 15, 16, 18, 19, 21, 25, 29, 30, 34, 35, | ||
2336 | 36, 39, 40, 41, 76, 77, 0, 0, 91, 68, | ||
2337 | 69, 78, 79, 80, 81, 84, 109, 85, 81, 81, | ||
2338 | 81, 85, 85, 82, 84, 80, 80, 82, 81, 82, | ||
2339 | 109, 109, 12, 13, 42, 43, 44, 45, 46, 47, | ||
2340 | 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, | ||
2341 | 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, | ||
2342 | 70, 71, 72, 73, 74, 75, 81, 85, 81, 117, | ||
2343 | 84, 111, 85, 108, 109, 85, 85, 78, 81, 83, | ||
2344 | 85, 68, 69, 78, 81, 85, 85, 111, 111, 109, | ||
2345 | 109, 109, 109, 109, 109, 109, 109, 109, 109, 109, | ||
2346 | 109, 109, 109, 109, 109, 109, 109, 109, 109, 109, | ||
2347 | 109, 109, 109, 109, 109, 108, 108, 108, 109, 109, | ||
2348 | 109, 108, 85, 86, 85, 84, 85, 109, 85, 85, | ||
2349 | 85, 85, 85, 85, 85, 84, 84, 110, 85, 108, | ||
2350 | 85, 108, 108, 108, 109, 109, 109, 109, 109, 85, | ||
2351 | 85, 85, 85, 85, 85, 85, 85, 85, 109, 85, | ||
2352 | 85, 85, 109, 109, 85, 109, 85, 85, 85, 109, | ||
2353 | 85, 109, 85, 109, 117, 84, 113, 114, 85, 84, | ||
2354 | 115, 116, 84, 118, 119, 109, 85, 85, 85, 85, | ||
2355 | 85, 85, 85, 85, 85, 85, 85, 85, 85, 85, | ||
2356 | 109, 87, 85, 86, 81, 114, 85, 81, 85, 115, | ||
2357 | 81, 85, 118, 112, 85, 109, 109, 117, 117, 117, | ||
2358 | 109, 109, 85, 88, 87, 85, 109, 85, 86, 112, | ||
2359 | 85, 85, 109, 112, 109, 85, 88, 85, 87, 85, | ||
2360 | 109, 88, 85 | ||
2361 | }; | ||
2362 | |||
2363 | const signed char | ||
2364 | Smt2Parser::yyr1_[] = | ||
2365 | { | ||
2366 | 0, 89, 90, 91, 91, 92, 92, 92, 92, 92, | ||
2367 | 92, 92, 92, 92, 92, 92, 92, 92, 92, 92, | ||
2368 | 93, 94, 95, 95, 95, 95, 96, 97, 98, 99, | ||
2369 | 100, 101, 102, 102, 102, 103, 104, 104, 104, 104, | ||
2370 | 105, 106, 107, 108, 108, 109, 109, 109, 109, 109, | ||
2371 | 109, 109, 109, 109, 109, 109, 109, 109, 109, 109, | ||
2372 | 109, 109, 109, 109, 109, 109, 109, 109, 109, 109, | ||
2373 | 109, 109, 109, 109, 109, 109, 109, 109, 109, 109, | ||
2374 | 109, 109, 109, 109, 109, 109, 109, 109, 110, 111, | ||
2375 | 112, 113, 114, 114, 115, 115, 116, 116, 117, 118, | ||
2376 | 118, 119 | ||
2377 | }; | ||
2378 | |||
2379 | const signed char | ||
2380 | Smt2Parser::yyr2_[] = | ||
2381 | { | ||
2382 | 0, 2, 2, 1, 2, 1, 1, 1, 1, 1, | ||
2383 | 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, | ||
2384 | 4, 3, 7, 12, 5, 10, 11, 3, 3, 6, | ||
2385 | 4, 4, 5, 5, 5, 4, 5, 5, 5, 5, | ||
2386 | 4, 4, 4, 1, 2, 1, 1, 5, 5, 5, | ||
2387 | 5, 5, 4, 4, 4, 4, 5, 6, 9, 7, | ||
2388 | 1, 1, 1, 1, 4, 5, 4, 5, 5, 5, | ||
2389 | 4, 4, 4, 4, 4, 4, 4, 4, 4, 5, | ||
2390 | 4, 4, 4, 5, 5, 4, 5, 4, 3, 0, | ||
2391 | 0, 4, 0, 2, 0, 2, 4, 9, 1, 0, | ||
2392 | 2, 4 | ||
2393 | }; | ||
2394 | |||
2395 | |||
2396 | |||
2397 | // YYTNAME[SYMBOL-NUM] -- String name of the symbol SYMBOL-NUM. | ||
2398 | // First, the terminals, then, starting at \a yyntokens_, nonterminals. | ||
2399 | const char* | ||
2400 | const Smt2Parser::yytname_[] = | ||
2401 | { | ||
2402 | "\"end of file\"", "error", "$undefined", "TK_EXCLAMATION", "TK_BINARY", | ||
2403 | "TK_DECIMAL", "TK_HEXADECIMAL", "TK_NUMERAL", "TK_STRING", | ||
2404 | "TK_UNDERSCORE", "TK_AS", "TK_EXISTS", "TK_FORALL", "TK_LET", "TK_PAR", | ||
2405 | "TK_ASSERT", "TK_CHECK_SAT", "TK_CHECK_SAT_ASSUMING", "TK_DECLARE_CONST", | ||
2406 | "TK_DECLARE_FUN", "TK_DECLARE_SORT", "TK_DEFINE_FUN", | ||
2407 | "TK_DEFINE_FUN_REC", "TK_DEFINE_SORT", "TK_ECHO", "TK_EXIT", | ||
2408 | "TK_GET_ASSERTIONS", "TK_GET_ASSIGNMENT", "TK_GET_INFO", "TK_GET_MODEL", | ||
2409 | "TK_GET_OPTION", "TK_GET_PROOF", "TK_GET_UNSAT_ASSUMPTIONS", | ||
2410 | "TK_GET_UNSAT_CORE", "TK_GET_VALUE", "TK_POP", "TK_PUSH", "TK_RESET", | ||
2411 | "TK_RESET_ASSERTIONS", "TK_SET_INFO", "TK_SET_LOGIC", "TK_SET_OPTION", | ||
2412 | "TK_PLUS", "TK_MINUS", "TK_TIMES", "TK_DIV", "TK_EQ", "TK_LTE", "TK_GTE", | ||
2413 | "TK_LT", "TK_GT", "TK_EXP", "TK_LOG", "TK_ABS", "TK_SIN", "TK_COS", | ||
2414 | "TK_TAN", "TK_ASIN", "TK_ACOS", "TK_ATAN", "TK_ATAN2", "TK_SINH", | ||
2415 | "TK_COSH", "TK_TANH", "TK_MIN", "TK_MAX", "TK_SQRT", "TK_POW", "TK_TRUE", | ||
2416 | "TK_FALSE", "TK_AND", "TK_OR", "TK_XOR", "TK_IMPLIES", "TK_NOT", | ||
2417 | "TK_ITE", "TK_MAXIMIZE", "TK_MINIMIZE", "\"double\"", "\"hexfloat\"", | ||
2418 | "\"int64\"", "\"symbol\"", "\"keyword\"", "\"string\"", "'('", "')'", | ||
2419 | "'['", "','", "']'", "$accept", "script", "command_list", "command", | ||
2420 | "command_assert", "command_check_sat", "command_declare_fun", | ||
2421 | "command_define_fun", "command_exit", "command_get_model", | ||
2422 | "command_get_value", "command_maximize", "command_minimize", | ||
2423 | "command_set_info", "command_set_logic", "command_set_option", | ||
2424 | "command_get_option", "command_push", "command_pop", "term_list", "term", | ||
2425 | "let_binding_list", "enter_scope", "exit_scope", "name_sort", | ||
2426 | "name_sort_list", "variable_sort_list", "variable_sort", "sort", | ||
2427 | "var_binding_list", "var_binding", YY_NULLPTR | ||
2428 | }; | ||
2429 | |||
2430 | #if DREALDEBUG | ||
2431 | const short | ||
2432 | Smt2Parser::yyrline_[] = | ||
2433 | { | ||
2434 | 0, 123, 123, 126, 127, 131, 132, 133, 134, 135, | ||
2435 | 136, 137, 138, 139, 140, 141, 142, 143, 144, 145, | ||
2436 | 148, 153, 158, 162, 166, 170, 176, 191, 198, 204, | ||
2437 | 209, 214, 220, 225, 230, 237, 244, 249, 254, 259, | ||
2438 | 267, 274, 279, 284, 285, 288, 289, 290, 309, 310, | ||
2439 | 311, 312, 313, 320, 327, 334, 337, 340, 364, 375, | ||
2440 | 378, 389, 390, 391, 404, 407, 413, 416, 422, 428, | ||
2441 | 434, 437, 440, 443, 446, 449, 452, 455, 458, 461, | ||
2442 | 464, 467, 470, 473, 476, 479, 482, 485, 490, 509, | ||
2443 | 514, 519, 524, 525, 533, 534, 549, 554, 562, 565, | ||
2444 | 568, 574 | ||
2445 | }; | ||
2446 | |||
2447 | // Print the state stack on the debug stream. | ||
2448 | void | ||
2449 | Smt2Parser::yystack_print_ () | ||
2450 | { | ||
2451 | *yycdebug_ << "Stack now"; | ||
2452 | for (stack_type::const_iterator | ||
2453 | i = yystack_.begin (), | ||
2454 | i_end = yystack_.end (); | ||
2455 | i != i_end; ++i) | ||
2456 | *yycdebug_ << ' ' << int (i->state); | ||
2457 | *yycdebug_ << '\n'; | ||
2458 | } | ||
2459 | |||
2460 | // Report on the debug stream that the rule \a yyrule is going to be reduced. | ||
2461 | void | ||
2462 | Smt2Parser::yy_reduce_print_ (int yyrule) | ||
2463 | { | ||
2464 | int yylno = yyrline_[yyrule]; | ||
2465 | int yynrhs = yyr2_[yyrule]; | ||
2466 | // Print the symbols being reduced, and their result. | ||
2467 | *yycdebug_ << "Reducing stack by rule " << yyrule - 1 | ||
2468 | << " (line " << yylno << "):\n"; | ||
2469 | // The symbols being reduced. | ||
2470 | for (int yyi = 0; yyi < yynrhs; yyi++) | ||
2471 | YY_SYMBOL_PRINT (" $" << yyi + 1 << " =", | ||
2472 | yystack_[(yynrhs) - (yyi + 1)]); | ||
2473 | } | ||
2474 | #endif // DREALDEBUG | ||
2475 | |||
2476 | Smt2Parser::token_number_type | ||
2477 | Smt2Parser::yytranslate_ (int t) | ||
2478 | { | ||
2479 | // YYTRANSLATE[TOKEN-NUM] -- Symbol number corresponding to | ||
2480 | // TOKEN-NUM as returned by yylex. | ||
2481 | static | ||
2482 | const token_number_type | ||
2483 | translate_table[] = | ||
2484 | { | ||
2485 | 0, 2, 2, 2, 2, 2, 2, 2, 2, 2, | ||
2486 | 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, | ||
2487 | 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, | ||
2488 | 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, | ||
2489 | 84, 85, 2, 2, 87, 2, 2, 2, 2, 2, | ||
2490 | 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, | ||
2491 | 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, | ||
2492 | 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, | ||
2493 | 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, | ||
2494 | 2, 86, 2, 88, 2, 2, 2, 2, 2, 2, | ||
2495 | 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, | ||
2496 | 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, | ||
2497 | 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, | ||
2498 | 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, | ||
2499 | 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, | ||
2500 | 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, | ||
2501 | 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, | ||
2502 | 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, | ||
2503 | 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, | ||
2504 | 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, | ||
2505 | 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, | ||
2506 | 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, | ||
2507 | 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, | ||
2508 | 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, | ||
2509 | 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, | ||
2510 | 2, 2, 2, 2, 2, 2, 1, 2, 3, 4, | ||
2511 | 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, | ||
2512 | 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, | ||
2513 | 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, | ||
2514 | 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, | ||
2515 | 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, | ||
2516 | 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, | ||
2517 | 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, | ||
2518 | 75, 76, 77, 78, 79, 80, 81, 82, 83 | ||
2519 | }; | ||
2520 | const int user_token_number_max_ = 338; | ||
2521 | |||
2522 | if (t <= 0) | ||
2523 | return yyeof_; | ||
2524 | else if (t <= user_token_number_max_) | ||
2525 | return translate_table[t]; | ||
2526 | else | ||
2527 | return yy_undef_token_; | ||
2528 | } | ||
2529 | |||
2530 | } // dreal | ||
2531 | #line 2532 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.cc" | ||
2532 | |||
2533 | #line 580 "dreal/smt2/parser.yy" | ||
2534 | /*** Additional Code ***/ | ||
2535 | void dreal::Smt2Parser::error(const Smt2Parser::location_type& l, | ||
2536 | const std::string& m) { | ||
2537 | driver.error(l, m); | ||
2538 | } | ||
2539 | |||
2540 | #ifdef __clang__ | ||
2541 | #pragma clang diagnostic pop | ||
2542 | #endif | ||
2543 | #pragma GCC diagnostic pop | ||