aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/dreal4/bazel-bin/dreal/smt2/parser.yy.cc
diff options
context:
space:
mode:
Diffstat (limited to 'Solvers/dreal4/bazel-bin/dreal/smt2/parser.yy.cc')
-rwxr-xr-xSolvers/dreal4/bazel-bin/dreal/smt2/parser.yy.cc2543
1 files changed, 2543 insertions, 0 deletions
diff --git a/Solvers/dreal4/bazel-bin/dreal/smt2/parser.yy.cc b/Solvers/dreal4/bazel-bin/dreal/smt2/parser.yy.cc
new file mode 100755
index 00000000..36ea8970
--- /dev/null
+++ b/Solvers/dreal4/bazel-bin/dreal/smt2/parser.yy.cc
@@ -0,0 +1,2543 @@
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
178namespace 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 ***/
2535void 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
generated by cgit v1.2.3-54-g00ecf (git 2.45.0) at 2024-05-06 00:00:20 +0000