diff options
Diffstat (limited to 'Solvers/dreal4/bazel-bin/dreal/smt2/parser.yy.hh')
-rwxr-xr-x | Solvers/dreal4/bazel-bin/dreal/smt2/parser.yy.hh | 2532 |
1 files changed, 2532 insertions, 0 deletions
diff --git a/Solvers/dreal4/bazel-bin/dreal/smt2/parser.yy.hh b/Solvers/dreal4/bazel-bin/dreal/smt2/parser.yy.hh new file mode 100755 index 00000000..d432b396 --- /dev/null +++ b/Solvers/dreal4/bazel-bin/dreal/smt2/parser.yy.hh | |||
@@ -0,0 +1,2532 @@ | |||
1 | // A Bison parser, made by GNU Bison 3.5. | ||
2 | |||
3 | // Skeleton interface 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 | |||
34 | /** | ||
35 | ** \file bazel-out/k8-opt/bin/dreal/smt2/parser.yy.hh | ||
36 | ** Define the dreal::parser class. | ||
37 | */ | ||
38 | |||
39 | // C++ LALR(1) parser skeleton written by Akim Demaille. | ||
40 | |||
41 | // Undocumented macros, especially those whose name start with YY_, | ||
42 | // are private implementation details. Do not rely on them. | ||
43 | |||
44 | #ifndef YY_DREAL_BAZEL_OUT_K8_OPT_BIN_DREAL_SMT2_PARSER_YY_HH_INCLUDED | ||
45 | # define YY_DREAL_BAZEL_OUT_K8_OPT_BIN_DREAL_SMT2_PARSER_YY_HH_INCLUDED | ||
46 | |||
47 | |||
48 | # include <cstdlib> // std::abort | ||
49 | # include <iostream> | ||
50 | # include <stdexcept> | ||
51 | # include <string> | ||
52 | # include <vector> | ||
53 | |||
54 | #if defined __cplusplus | ||
55 | # define YY_CPLUSPLUS __cplusplus | ||
56 | #else | ||
57 | # define YY_CPLUSPLUS 199711L | ||
58 | #endif | ||
59 | |||
60 | // Support move semantics when possible. | ||
61 | #if 201103L <= YY_CPLUSPLUS | ||
62 | # define YY_MOVE std::move | ||
63 | # define YY_MOVE_OR_COPY move | ||
64 | # define YY_MOVE_REF(Type) Type&& | ||
65 | # define YY_RVREF(Type) Type&& | ||
66 | # define YY_COPY(Type) Type | ||
67 | #else | ||
68 | # define YY_MOVE | ||
69 | # define YY_MOVE_OR_COPY copy | ||
70 | # define YY_MOVE_REF(Type) Type& | ||
71 | # define YY_RVREF(Type) const Type& | ||
72 | # define YY_COPY(Type) const Type& | ||
73 | #endif | ||
74 | |||
75 | // Support noexcept when possible. | ||
76 | #if 201103L <= YY_CPLUSPLUS | ||
77 | # define YY_NOEXCEPT noexcept | ||
78 | # define YY_NOTHROW | ||
79 | #else | ||
80 | # define YY_NOEXCEPT | ||
81 | # define YY_NOTHROW throw () | ||
82 | #endif | ||
83 | |||
84 | // Support constexpr when possible. | ||
85 | #if 201703 <= YY_CPLUSPLUS | ||
86 | # define YY_CONSTEXPR constexpr | ||
87 | #else | ||
88 | # define YY_CONSTEXPR | ||
89 | #endif | ||
90 | # include "location.hh" | ||
91 | |||
92 | #ifndef YY_ASSERT | ||
93 | # include <cassert> | ||
94 | # define YY_ASSERT assert | ||
95 | #endif | ||
96 | |||
97 | |||
98 | #ifndef YY_ATTRIBUTE_PURE | ||
99 | # if defined __GNUC__ && 2 < __GNUC__ + (96 <= __GNUC_MINOR__) | ||
100 | # define YY_ATTRIBUTE_PURE __attribute__ ((__pure__)) | ||
101 | # else | ||
102 | # define YY_ATTRIBUTE_PURE | ||
103 | # endif | ||
104 | #endif | ||
105 | |||
106 | #ifndef YY_ATTRIBUTE_UNUSED | ||
107 | # if defined __GNUC__ && 2 < __GNUC__ + (7 <= __GNUC_MINOR__) | ||
108 | # define YY_ATTRIBUTE_UNUSED __attribute__ ((__unused__)) | ||
109 | # else | ||
110 | # define YY_ATTRIBUTE_UNUSED | ||
111 | # endif | ||
112 | #endif | ||
113 | |||
114 | /* Suppress unused-variable warnings by "using" E. */ | ||
115 | #if ! defined lint || defined __GNUC__ | ||
116 | # define YYUSE(E) ((void) (E)) | ||
117 | #else | ||
118 | # define YYUSE(E) /* empty */ | ||
119 | #endif | ||
120 | |||
121 | #if defined __GNUC__ && ! defined __ICC && 407 <= __GNUC__ * 100 + __GNUC_MINOR__ | ||
122 | /* Suppress an incorrect diagnostic about yylval being uninitialized. */ | ||
123 | # define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN \ | ||
124 | _Pragma ("GCC diagnostic push") \ | ||
125 | _Pragma ("GCC diagnostic ignored \"-Wuninitialized\"") \ | ||
126 | _Pragma ("GCC diagnostic ignored \"-Wmaybe-uninitialized\"") | ||
127 | # define YY_IGNORE_MAYBE_UNINITIALIZED_END \ | ||
128 | _Pragma ("GCC diagnostic pop") | ||
129 | #else | ||
130 | # define YY_INITIAL_VALUE(Value) Value | ||
131 | #endif | ||
132 | #ifndef YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN | ||
133 | # define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN | ||
134 | # define YY_IGNORE_MAYBE_UNINITIALIZED_END | ||
135 | #endif | ||
136 | #ifndef YY_INITIAL_VALUE | ||
137 | # define YY_INITIAL_VALUE(Value) /* Nothing. */ | ||
138 | #endif | ||
139 | |||
140 | #if defined __cplusplus && defined __GNUC__ && ! defined __ICC && 6 <= __GNUC__ | ||
141 | # define YY_IGNORE_USELESS_CAST_BEGIN \ | ||
142 | _Pragma ("GCC diagnostic push") \ | ||
143 | _Pragma ("GCC diagnostic ignored \"-Wuseless-cast\"") | ||
144 | # define YY_IGNORE_USELESS_CAST_END \ | ||
145 | _Pragma ("GCC diagnostic pop") | ||
146 | #endif | ||
147 | #ifndef YY_IGNORE_USELESS_CAST_BEGIN | ||
148 | # define YY_IGNORE_USELESS_CAST_BEGIN | ||
149 | # define YY_IGNORE_USELESS_CAST_END | ||
150 | #endif | ||
151 | |||
152 | # ifndef YY_CAST | ||
153 | # ifdef __cplusplus | ||
154 | # define YY_CAST(Type, Val) static_cast<Type> (Val) | ||
155 | # define YY_REINTERPRET_CAST(Type, Val) reinterpret_cast<Type> (Val) | ||
156 | # else | ||
157 | # define YY_CAST(Type, Val) ((Type) (Val)) | ||
158 | # define YY_REINTERPRET_CAST(Type, Val) ((Type) (Val)) | ||
159 | # endif | ||
160 | # endif | ||
161 | # ifndef YY_NULLPTR | ||
162 | # if defined __cplusplus | ||
163 | # if 201103L <= __cplusplus | ||
164 | # define YY_NULLPTR nullptr | ||
165 | # else | ||
166 | # define YY_NULLPTR 0 | ||
167 | # endif | ||
168 | # else | ||
169 | # define YY_NULLPTR ((void*)0) | ||
170 | # endif | ||
171 | # endif | ||
172 | |||
173 | /* Debug traces. */ | ||
174 | #ifndef DREALDEBUG | ||
175 | # if defined YYDEBUG | ||
176 | #if YYDEBUG | ||
177 | # define DREALDEBUG 1 | ||
178 | # else | ||
179 | # define DREALDEBUG 0 | ||
180 | # endif | ||
181 | # else /* ! defined YYDEBUG */ | ||
182 | # define DREALDEBUG 1 | ||
183 | # endif /* ! defined YYDEBUG */ | ||
184 | #endif /* ! defined DREALDEBUG */ | ||
185 | |||
186 | namespace dreal { | ||
187 | #line 188 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.hh" | ||
188 | |||
189 | |||
190 | |||
191 | |||
192 | /// A Bison parser. | ||
193 | class Smt2Parser | ||
194 | { | ||
195 | public: | ||
196 | #ifndef DREALSTYPE | ||
197 | /// A buffer to store and retrieve objects. | ||
198 | /// | ||
199 | /// Sort of a variant, but does not keep track of the nature | ||
200 | /// of the stored data, since that knowledge is available | ||
201 | /// via the current parser state. | ||
202 | class semantic_type | ||
203 | { | ||
204 | public: | ||
205 | /// Type of *this. | ||
206 | typedef semantic_type self_type; | ||
207 | |||
208 | /// Empty construction. | ||
209 | semantic_type () YY_NOEXCEPT | ||
210 | : yybuffer_ () | ||
211 | {} | ||
212 | |||
213 | /// Construct and fill. | ||
214 | template <typename T> | ||
215 | semantic_type (YY_RVREF (T) t) | ||
216 | { | ||
217 | YY_ASSERT (sizeof (T) <= size); | ||
218 | new (yyas_<T> ()) T (YY_MOVE (t)); | ||
219 | } | ||
220 | |||
221 | /// Destruction, allowed only if empty. | ||
222 | ~semantic_type () YY_NOEXCEPT | ||
223 | {} | ||
224 | |||
225 | # if 201103L <= YY_CPLUSPLUS | ||
226 | /// Instantiate a \a T in here from \a t. | ||
227 | template <typename T, typename... U> | ||
228 | T& | ||
229 | emplace (U&&... u) | ||
230 | { | ||
231 | return *new (yyas_<T> ()) T (std::forward <U>(u)...); | ||
232 | } | ||
233 | # else | ||
234 | /// Instantiate an empty \a T in here. | ||
235 | template <typename T> | ||
236 | T& | ||
237 | emplace () | ||
238 | { | ||
239 | return *new (yyas_<T> ()) T (); | ||
240 | } | ||
241 | |||
242 | /// Instantiate a \a T in here from \a t. | ||
243 | template <typename T> | ||
244 | T& | ||
245 | emplace (const T& t) | ||
246 | { | ||
247 | return *new (yyas_<T> ()) T (t); | ||
248 | } | ||
249 | # endif | ||
250 | |||
251 | /// Instantiate an empty \a T in here. | ||
252 | /// Obsolete, use emplace. | ||
253 | template <typename T> | ||
254 | T& | ||
255 | build () | ||
256 | { | ||
257 | return emplace<T> (); | ||
258 | } | ||
259 | |||
260 | /// Instantiate a \a T in here from \a t. | ||
261 | /// Obsolete, use emplace. | ||
262 | template <typename T> | ||
263 | T& | ||
264 | build (const T& t) | ||
265 | { | ||
266 | return emplace<T> (t); | ||
267 | } | ||
268 | |||
269 | /// Accessor to a built \a T. | ||
270 | template <typename T> | ||
271 | T& | ||
272 | as () YY_NOEXCEPT | ||
273 | { | ||
274 | return *yyas_<T> (); | ||
275 | } | ||
276 | |||
277 | /// Const accessor to a built \a T (for %printer). | ||
278 | template <typename T> | ||
279 | const T& | ||
280 | as () const YY_NOEXCEPT | ||
281 | { | ||
282 | return *yyas_<T> (); | ||
283 | } | ||
284 | |||
285 | /// Swap the content with \a that, of same type. | ||
286 | /// | ||
287 | /// Both variants must be built beforehand, because swapping the actual | ||
288 | /// data requires reading it (with as()), and this is not possible on | ||
289 | /// unconstructed variants: it would require some dynamic testing, which | ||
290 | /// should not be the variant's responsibility. | ||
291 | /// Swapping between built and (possibly) non-built is done with | ||
292 | /// self_type::move (). | ||
293 | template <typename T> | ||
294 | void | ||
295 | swap (self_type& that) YY_NOEXCEPT | ||
296 | { | ||
297 | std::swap (as<T> (), that.as<T> ()); | ||
298 | } | ||
299 | |||
300 | /// Move the content of \a that to this. | ||
301 | /// | ||
302 | /// Destroys \a that. | ||
303 | template <typename T> | ||
304 | void | ||
305 | move (self_type& that) | ||
306 | { | ||
307 | # if 201103L <= YY_CPLUSPLUS | ||
308 | emplace<T> (std::move (that.as<T> ())); | ||
309 | # else | ||
310 | emplace<T> (); | ||
311 | swap<T> (that); | ||
312 | # endif | ||
313 | that.destroy<T> (); | ||
314 | } | ||
315 | |||
316 | # if 201103L <= YY_CPLUSPLUS | ||
317 | /// Move the content of \a that to this. | ||
318 | template <typename T> | ||
319 | void | ||
320 | move (self_type&& that) | ||
321 | { | ||
322 | emplace<T> (std::move (that.as<T> ())); | ||
323 | that.destroy<T> (); | ||
324 | } | ||
325 | #endif | ||
326 | |||
327 | /// Copy the content of \a that to this. | ||
328 | template <typename T> | ||
329 | void | ||
330 | copy (const self_type& that) | ||
331 | { | ||
332 | emplace<T> (that.as<T> ()); | ||
333 | } | ||
334 | |||
335 | /// Destroy the stored \a T. | ||
336 | template <typename T> | ||
337 | void | ||
338 | destroy () | ||
339 | { | ||
340 | as<T> ().~T (); | ||
341 | } | ||
342 | |||
343 | private: | ||
344 | /// Prohibit blind copies. | ||
345 | self_type& operator= (const self_type&); | ||
346 | semantic_type (const self_type&); | ||
347 | |||
348 | /// Accessor to raw memory as \a T. | ||
349 | template <typename T> | ||
350 | T* | ||
351 | yyas_ () YY_NOEXCEPT | ||
352 | { | ||
353 | void *yyp = yybuffer_.yyraw; | ||
354 | return static_cast<T*> (yyp); | ||
355 | } | ||
356 | |||
357 | /// Const accessor to raw memory as \a T. | ||
358 | template <typename T> | ||
359 | const T* | ||
360 | yyas_ () const YY_NOEXCEPT | ||
361 | { | ||
362 | const void *yyp = yybuffer_.yyraw; | ||
363 | return static_cast<const T*> (yyp); | ||
364 | } | ||
365 | |||
366 | /// An auxiliary type to compute the largest semantic type. | ||
367 | union union_type | ||
368 | { | ||
369 | // term | ||
370 | char dummy1[sizeof (Term)]; | ||
371 | |||
372 | // name_sort | ||
373 | char dummy2[sizeof (Variable)]; | ||
374 | |||
375 | // "hexfloat" | ||
376 | char dummy3[sizeof (double)]; | ||
377 | |||
378 | // sort | ||
379 | char dummy4[sizeof (dreal::Sort)]; | ||
380 | |||
381 | // "int64" | ||
382 | char dummy5[sizeof (std::int64_t)]; | ||
383 | |||
384 | // variable_sort_list | ||
385 | char dummy6[sizeof (std::pair<Variables, Formula>)]; | ||
386 | |||
387 | // var_binding | ||
388 | char dummy7[sizeof (std::pair<std::string, Term>)]; | ||
389 | |||
390 | // "double" | ||
391 | // "symbol" | ||
392 | // "keyword" | ||
393 | // "string" | ||
394 | char dummy8[sizeof (std::string)]; | ||
395 | |||
396 | // variable_sort | ||
397 | char dummy9[sizeof (std::tuple<Variable, double, double>)]; | ||
398 | |||
399 | // term_list | ||
400 | char dummy10[sizeof (std::vector<Term>)]; | ||
401 | |||
402 | // name_sort_list | ||
403 | char dummy11[sizeof (std::vector<Variable>)]; | ||
404 | |||
405 | // var_binding_list | ||
406 | char dummy12[sizeof (std::vector<std::pair<std::string, Term>>)]; | ||
407 | }; | ||
408 | |||
409 | /// The size of the largest semantic type. | ||
410 | enum { size = sizeof (union_type) }; | ||
411 | |||
412 | /// A buffer to store semantic values. | ||
413 | union | ||
414 | { | ||
415 | /// Strongest alignment constraints. | ||
416 | long double yyalign_me; | ||
417 | /// A buffer large enough to store any of the semantic values. | ||
418 | char yyraw[size]; | ||
419 | } yybuffer_; | ||
420 | }; | ||
421 | |||
422 | #else | ||
423 | typedef DREALSTYPE semantic_type; | ||
424 | #endif | ||
425 | /// Symbol locations. | ||
426 | typedef location location_type; | ||
427 | |||
428 | /// Syntax errors thrown from user actions. | ||
429 | struct syntax_error : std::runtime_error | ||
430 | { | ||
431 | syntax_error (const location_type& l, const std::string& m) | ||
432 | : std::runtime_error (m) | ||
433 | , location (l) | ||
434 | {} | ||
435 | |||
436 | syntax_error (const syntax_error& s) | ||
437 | : std::runtime_error (s.what ()) | ||
438 | , location (s.location) | ||
439 | {} | ||
440 | |||
441 | ~syntax_error () YY_NOEXCEPT YY_NOTHROW; | ||
442 | |||
443 | location_type location; | ||
444 | }; | ||
445 | |||
446 | /// Tokens. | ||
447 | struct token | ||
448 | { | ||
449 | enum yytokentype | ||
450 | { | ||
451 | END = 0, | ||
452 | TK_EXCLAMATION = 258, | ||
453 | TK_BINARY = 259, | ||
454 | TK_DECIMAL = 260, | ||
455 | TK_HEXADECIMAL = 261, | ||
456 | TK_NUMERAL = 262, | ||
457 | TK_STRING = 263, | ||
458 | TK_UNDERSCORE = 264, | ||
459 | TK_AS = 265, | ||
460 | TK_EXISTS = 266, | ||
461 | TK_FORALL = 267, | ||
462 | TK_LET = 268, | ||
463 | TK_PAR = 269, | ||
464 | TK_ASSERT = 270, | ||
465 | TK_CHECK_SAT = 271, | ||
466 | TK_CHECK_SAT_ASSUMING = 272, | ||
467 | TK_DECLARE_CONST = 273, | ||
468 | TK_DECLARE_FUN = 274, | ||
469 | TK_DECLARE_SORT = 275, | ||
470 | TK_DEFINE_FUN = 276, | ||
471 | TK_DEFINE_FUN_REC = 277, | ||
472 | TK_DEFINE_SORT = 278, | ||
473 | TK_ECHO = 279, | ||
474 | TK_EXIT = 280, | ||
475 | TK_GET_ASSERTIONS = 281, | ||
476 | TK_GET_ASSIGNMENT = 282, | ||
477 | TK_GET_INFO = 283, | ||
478 | TK_GET_MODEL = 284, | ||
479 | TK_GET_OPTION = 285, | ||
480 | TK_GET_PROOF = 286, | ||
481 | TK_GET_UNSAT_ASSUMPTIONS = 287, | ||
482 | TK_GET_UNSAT_CORE = 288, | ||
483 | TK_GET_VALUE = 289, | ||
484 | TK_POP = 290, | ||
485 | TK_PUSH = 291, | ||
486 | TK_RESET = 292, | ||
487 | TK_RESET_ASSERTIONS = 293, | ||
488 | TK_SET_INFO = 294, | ||
489 | TK_SET_LOGIC = 295, | ||
490 | TK_SET_OPTION = 296, | ||
491 | TK_PLUS = 297, | ||
492 | TK_MINUS = 298, | ||
493 | TK_TIMES = 299, | ||
494 | TK_DIV = 300, | ||
495 | TK_EQ = 301, | ||
496 | TK_LTE = 302, | ||
497 | TK_GTE = 303, | ||
498 | TK_LT = 304, | ||
499 | TK_GT = 305, | ||
500 | TK_EXP = 306, | ||
501 | TK_LOG = 307, | ||
502 | TK_ABS = 308, | ||
503 | TK_SIN = 309, | ||
504 | TK_COS = 310, | ||
505 | TK_TAN = 311, | ||
506 | TK_ASIN = 312, | ||
507 | TK_ACOS = 313, | ||
508 | TK_ATAN = 314, | ||
509 | TK_ATAN2 = 315, | ||
510 | TK_SINH = 316, | ||
511 | TK_COSH = 317, | ||
512 | TK_TANH = 318, | ||
513 | TK_MIN = 319, | ||
514 | TK_MAX = 320, | ||
515 | TK_SQRT = 321, | ||
516 | TK_POW = 322, | ||
517 | TK_TRUE = 323, | ||
518 | TK_FALSE = 324, | ||
519 | TK_AND = 325, | ||
520 | TK_OR = 326, | ||
521 | TK_XOR = 327, | ||
522 | TK_IMPLIES = 328, | ||
523 | TK_NOT = 329, | ||
524 | TK_ITE = 330, | ||
525 | TK_MAXIMIZE = 331, | ||
526 | TK_MINIMIZE = 332, | ||
527 | DOUBLE = 333, | ||
528 | HEXFLOAT = 334, | ||
529 | INT = 335, | ||
530 | SYMBOL = 336, | ||
531 | KEYWORD = 337, | ||
532 | STRING = 338 | ||
533 | }; | ||
534 | }; | ||
535 | |||
536 | /// (External) token type, as returned by yylex. | ||
537 | typedef token::yytokentype token_type; | ||
538 | |||
539 | /// Symbol type: an internal symbol number. | ||
540 | typedef int symbol_number_type; | ||
541 | |||
542 | /// The symbol type number to denote an empty symbol. | ||
543 | enum { empty_symbol = -2 }; | ||
544 | |||
545 | /// Internal symbol number for tokens (subsumed by symbol_number_type). | ||
546 | typedef signed char token_number_type; | ||
547 | |||
548 | /// A complete symbol. | ||
549 | /// | ||
550 | /// Expects its Base type to provide access to the symbol type | ||
551 | /// via type_get (). | ||
552 | /// | ||
553 | /// Provide access to semantic value and location. | ||
554 | template <typename Base> | ||
555 | struct basic_symbol : Base | ||
556 | { | ||
557 | /// Alias to Base. | ||
558 | typedef Base super_type; | ||
559 | |||
560 | /// Default constructor. | ||
561 | basic_symbol () | ||
562 | : value () | ||
563 | , location () | ||
564 | {} | ||
565 | |||
566 | #if 201103L <= YY_CPLUSPLUS | ||
567 | /// Move constructor. | ||
568 | basic_symbol (basic_symbol&& that); | ||
569 | #endif | ||
570 | |||
571 | /// Copy constructor. | ||
572 | basic_symbol (const basic_symbol& that); | ||
573 | |||
574 | /// Constructor for valueless symbols, and symbols from each type. | ||
575 | #if 201103L <= YY_CPLUSPLUS | ||
576 | basic_symbol (typename Base::kind_type t, location_type&& l) | ||
577 | : Base (t) | ||
578 | , location (std::move (l)) | ||
579 | {} | ||
580 | #else | ||
581 | basic_symbol (typename Base::kind_type t, const location_type& l) | ||
582 | : Base (t) | ||
583 | , location (l) | ||
584 | {} | ||
585 | #endif | ||
586 | #if 201103L <= YY_CPLUSPLUS | ||
587 | basic_symbol (typename Base::kind_type t, Term&& v, location_type&& l) | ||
588 | : Base (t) | ||
589 | , value (std::move (v)) | ||
590 | , location (std::move (l)) | ||
591 | {} | ||
592 | #else | ||
593 | basic_symbol (typename Base::kind_type t, const Term& v, const location_type& l) | ||
594 | : Base (t) | ||
595 | , value (v) | ||
596 | , location (l) | ||
597 | {} | ||
598 | #endif | ||
599 | #if 201103L <= YY_CPLUSPLUS | ||
600 | basic_symbol (typename Base::kind_type t, Variable&& v, location_type&& l) | ||
601 | : Base (t) | ||
602 | , value (std::move (v)) | ||
603 | , location (std::move (l)) | ||
604 | {} | ||
605 | #else | ||
606 | basic_symbol (typename Base::kind_type t, const Variable& v, const location_type& l) | ||
607 | : Base (t) | ||
608 | , value (v) | ||
609 | , location (l) | ||
610 | {} | ||
611 | #endif | ||
612 | #if 201103L <= YY_CPLUSPLUS | ||
613 | basic_symbol (typename Base::kind_type t, double&& v, location_type&& l) | ||
614 | : Base (t) | ||
615 | , value (std::move (v)) | ||
616 | , location (std::move (l)) | ||
617 | {} | ||
618 | #else | ||
619 | basic_symbol (typename Base::kind_type t, const double& v, const location_type& l) | ||
620 | : Base (t) | ||
621 | , value (v) | ||
622 | , location (l) | ||
623 | {} | ||
624 | #endif | ||
625 | #if 201103L <= YY_CPLUSPLUS | ||
626 | basic_symbol (typename Base::kind_type t, dreal::Sort&& v, location_type&& l) | ||
627 | : Base (t) | ||
628 | , value (std::move (v)) | ||
629 | , location (std::move (l)) | ||
630 | {} | ||
631 | #else | ||
632 | basic_symbol (typename Base::kind_type t, const dreal::Sort& v, const location_type& l) | ||
633 | : Base (t) | ||
634 | , value (v) | ||
635 | , location (l) | ||
636 | {} | ||
637 | #endif | ||
638 | #if 201103L <= YY_CPLUSPLUS | ||
639 | basic_symbol (typename Base::kind_type t, std::int64_t&& v, location_type&& l) | ||
640 | : Base (t) | ||
641 | , value (std::move (v)) | ||
642 | , location (std::move (l)) | ||
643 | {} | ||
644 | #else | ||
645 | basic_symbol (typename Base::kind_type t, const std::int64_t& v, const location_type& l) | ||
646 | : Base (t) | ||
647 | , value (v) | ||
648 | , location (l) | ||
649 | {} | ||
650 | #endif | ||
651 | #if 201103L <= YY_CPLUSPLUS | ||
652 | basic_symbol (typename Base::kind_type t, std::pair<Variables, Formula>&& v, location_type&& l) | ||
653 | : Base (t) | ||
654 | , value (std::move (v)) | ||
655 | , location (std::move (l)) | ||
656 | {} | ||
657 | #else | ||
658 | basic_symbol (typename Base::kind_type t, const std::pair<Variables, Formula>& v, const location_type& l) | ||
659 | : Base (t) | ||
660 | , value (v) | ||
661 | , location (l) | ||
662 | {} | ||
663 | #endif | ||
664 | #if 201103L <= YY_CPLUSPLUS | ||
665 | basic_symbol (typename Base::kind_type t, std::pair<std::string, Term>&& v, location_type&& l) | ||
666 | : Base (t) | ||
667 | , value (std::move (v)) | ||
668 | , location (std::move (l)) | ||
669 | {} | ||
670 | #else | ||
671 | basic_symbol (typename Base::kind_type t, const std::pair<std::string, Term>& v, const location_type& l) | ||
672 | : Base (t) | ||
673 | , value (v) | ||
674 | , location (l) | ||
675 | {} | ||
676 | #endif | ||
677 | #if 201103L <= YY_CPLUSPLUS | ||
678 | basic_symbol (typename Base::kind_type t, std::string&& v, location_type&& l) | ||
679 | : Base (t) | ||
680 | , value (std::move (v)) | ||
681 | , location (std::move (l)) | ||
682 | {} | ||
683 | #else | ||
684 | basic_symbol (typename Base::kind_type t, const std::string& v, const location_type& l) | ||
685 | : Base (t) | ||
686 | , value (v) | ||
687 | , location (l) | ||
688 | {} | ||
689 | #endif | ||
690 | #if 201103L <= YY_CPLUSPLUS | ||
691 | basic_symbol (typename Base::kind_type t, std::tuple<Variable, double, double>&& v, location_type&& l) | ||
692 | : Base (t) | ||
693 | , value (std::move (v)) | ||
694 | , location (std::move (l)) | ||
695 | {} | ||
696 | #else | ||
697 | basic_symbol (typename Base::kind_type t, const std::tuple<Variable, double, double>& v, const location_type& l) | ||
698 | : Base (t) | ||
699 | , value (v) | ||
700 | , location (l) | ||
701 | {} | ||
702 | #endif | ||
703 | #if 201103L <= YY_CPLUSPLUS | ||
704 | basic_symbol (typename Base::kind_type t, std::vector<Term>&& v, location_type&& l) | ||
705 | : Base (t) | ||
706 | , value (std::move (v)) | ||
707 | , location (std::move (l)) | ||
708 | {} | ||
709 | #else | ||
710 | basic_symbol (typename Base::kind_type t, const std::vector<Term>& v, const location_type& l) | ||
711 | : Base (t) | ||
712 | , value (v) | ||
713 | , location (l) | ||
714 | {} | ||
715 | #endif | ||
716 | #if 201103L <= YY_CPLUSPLUS | ||
717 | basic_symbol (typename Base::kind_type t, std::vector<Variable>&& v, location_type&& l) | ||
718 | : Base (t) | ||
719 | , value (std::move (v)) | ||
720 | , location (std::move (l)) | ||
721 | {} | ||
722 | #else | ||
723 | basic_symbol (typename Base::kind_type t, const std::vector<Variable>& v, const location_type& l) | ||
724 | : Base (t) | ||
725 | , value (v) | ||
726 | , location (l) | ||
727 | {} | ||
728 | #endif | ||
729 | #if 201103L <= YY_CPLUSPLUS | ||
730 | basic_symbol (typename Base::kind_type t, std::vector<std::pair<std::string, Term>>&& v, location_type&& l) | ||
731 | : Base (t) | ||
732 | , value (std::move (v)) | ||
733 | , location (std::move (l)) | ||
734 | {} | ||
735 | #else | ||
736 | basic_symbol (typename Base::kind_type t, const std::vector<std::pair<std::string, Term>>& v, const location_type& l) | ||
737 | : Base (t) | ||
738 | , value (v) | ||
739 | , location (l) | ||
740 | {} | ||
741 | #endif | ||
742 | |||
743 | /// Destroy the symbol. | ||
744 | ~basic_symbol () | ||
745 | { | ||
746 | clear (); | ||
747 | } | ||
748 | |||
749 | /// Destroy contents, and record that is empty. | ||
750 | void clear () | ||
751 | { | ||
752 | // User destructor. | ||
753 | symbol_number_type yytype = this->type_get (); | ||
754 | basic_symbol<Base>& yysym = *this; | ||
755 | (void) yysym; | ||
756 | switch (yytype) | ||
757 | { | ||
758 | default: | ||
759 | break; | ||
760 | } | ||
761 | |||
762 | // Type destructor. | ||
763 | switch (yytype) | ||
764 | { | ||
765 | case 109: // term | ||
766 | value.template destroy< Term > (); | ||
767 | break; | ||
768 | |||
769 | case 113: // name_sort | ||
770 | value.template destroy< Variable > (); | ||
771 | break; | ||
772 | |||
773 | case 79: // "hexfloat" | ||
774 | value.template destroy< double > (); | ||
775 | break; | ||
776 | |||
777 | case 117: // sort | ||
778 | value.template destroy< dreal::Sort > (); | ||
779 | break; | ||
780 | |||
781 | case 80: // "int64" | ||
782 | value.template destroy< std::int64_t > (); | ||
783 | break; | ||
784 | |||
785 | case 115: // variable_sort_list | ||
786 | value.template destroy< std::pair<Variables, Formula> > (); | ||
787 | break; | ||
788 | |||
789 | case 119: // var_binding | ||
790 | value.template destroy< std::pair<std::string, Term> > (); | ||
791 | break; | ||
792 | |||
793 | case 78: // "double" | ||
794 | case 81: // "symbol" | ||
795 | case 82: // "keyword" | ||
796 | case 83: // "string" | ||
797 | value.template destroy< std::string > (); | ||
798 | break; | ||
799 | |||
800 | case 116: // variable_sort | ||
801 | value.template destroy< std::tuple<Variable, double, double> > (); | ||
802 | break; | ||
803 | |||
804 | case 108: // term_list | ||
805 | value.template destroy< std::vector<Term> > (); | ||
806 | break; | ||
807 | |||
808 | case 114: // name_sort_list | ||
809 | value.template destroy< std::vector<Variable> > (); | ||
810 | break; | ||
811 | |||
812 | case 118: // var_binding_list | ||
813 | value.template destroy< std::vector<std::pair<std::string, Term>> > (); | ||
814 | break; | ||
815 | |||
816 | default: | ||
817 | break; | ||
818 | } | ||
819 | |||
820 | Base::clear (); | ||
821 | } | ||
822 | |||
823 | /// Whether empty. | ||
824 | bool empty () const YY_NOEXCEPT; | ||
825 | |||
826 | /// Destructive move, \a s is emptied into this. | ||
827 | void move (basic_symbol& s); | ||
828 | |||
829 | /// The semantic value. | ||
830 | semantic_type value; | ||
831 | |||
832 | /// The location. | ||
833 | location_type location; | ||
834 | |||
835 | private: | ||
836 | #if YY_CPLUSPLUS < 201103L | ||
837 | /// Assignment operator. | ||
838 | basic_symbol& operator= (const basic_symbol& that); | ||
839 | #endif | ||
840 | }; | ||
841 | |||
842 | /// Type access provider for token (enum) based symbols. | ||
843 | struct by_type | ||
844 | { | ||
845 | /// Default constructor. | ||
846 | by_type (); | ||
847 | |||
848 | #if 201103L <= YY_CPLUSPLUS | ||
849 | /// Move constructor. | ||
850 | by_type (by_type&& that); | ||
851 | #endif | ||
852 | |||
853 | /// Copy constructor. | ||
854 | by_type (const by_type& that); | ||
855 | |||
856 | /// The symbol type as needed by the constructor. | ||
857 | typedef token_type kind_type; | ||
858 | |||
859 | /// Constructor from (external) token numbers. | ||
860 | by_type (kind_type t); | ||
861 | |||
862 | /// Record that this symbol is empty. | ||
863 | void clear (); | ||
864 | |||
865 | /// Steal the symbol type from \a that. | ||
866 | void move (by_type& that); | ||
867 | |||
868 | /// The (internal) type number (corresponding to \a type). | ||
869 | /// \a empty when empty. | ||
870 | symbol_number_type type_get () const YY_NOEXCEPT; | ||
871 | |||
872 | /// The symbol type. | ||
873 | /// \a empty_symbol when empty. | ||
874 | /// An int, not token_number_type, to be able to store empty_symbol. | ||
875 | int type; | ||
876 | }; | ||
877 | |||
878 | /// "External" symbols: returned by the scanner. | ||
879 | struct symbol_type : basic_symbol<by_type> | ||
880 | { | ||
881 | /// Superclass. | ||
882 | typedef basic_symbol<by_type> super_type; | ||
883 | |||
884 | /// Empty symbol. | ||
885 | symbol_type () {} | ||
886 | |||
887 | /// Constructor for valueless symbols, and symbols from each type. | ||
888 | #if 201103L <= YY_CPLUSPLUS | ||
889 | symbol_type (int tok, location_type l) | ||
890 | : super_type(token_type (tok), std::move (l)) | ||
891 | { | ||
892 | YY_ASSERT (tok == token::END || tok == token::TK_EXCLAMATION || tok == token::TK_BINARY || tok == token::TK_DECIMAL || tok == token::TK_HEXADECIMAL || tok == token::TK_NUMERAL || tok == token::TK_STRING || tok == token::TK_UNDERSCORE || tok == token::TK_AS || tok == token::TK_EXISTS || tok == token::TK_FORALL || tok == token::TK_LET || tok == token::TK_PAR || tok == token::TK_ASSERT || tok == token::TK_CHECK_SAT || tok == token::TK_CHECK_SAT_ASSUMING || tok == token::TK_DECLARE_CONST || tok == token::TK_DECLARE_FUN || tok == token::TK_DECLARE_SORT || tok == token::TK_DEFINE_FUN || tok == token::TK_DEFINE_FUN_REC || tok == token::TK_DEFINE_SORT || tok == token::TK_ECHO || tok == token::TK_EXIT || tok == token::TK_GET_ASSERTIONS || tok == token::TK_GET_ASSIGNMENT || tok == token::TK_GET_INFO || tok == token::TK_GET_MODEL || tok == token::TK_GET_OPTION || tok == token::TK_GET_PROOF || tok == token::TK_GET_UNSAT_ASSUMPTIONS || tok == token::TK_GET_UNSAT_CORE || tok == token::TK_GET_VALUE || tok == token::TK_POP || tok == token::TK_PUSH || tok == token::TK_RESET || tok == token::TK_RESET_ASSERTIONS || tok == token::TK_SET_INFO || tok == token::TK_SET_LOGIC || tok == token::TK_SET_OPTION || tok == token::TK_PLUS || tok == token::TK_MINUS || tok == token::TK_TIMES || tok == token::TK_DIV || tok == token::TK_EQ || tok == token::TK_LTE || tok == token::TK_GTE || tok == token::TK_LT || tok == token::TK_GT || tok == token::TK_EXP || tok == token::TK_LOG || tok == token::TK_ABS || tok == token::TK_SIN || tok == token::TK_COS || tok == token::TK_TAN || tok == token::TK_ASIN || tok == token::TK_ACOS || tok == token::TK_ATAN || tok == token::TK_ATAN2 || tok == token::TK_SINH || tok == token::TK_COSH || tok == token::TK_TANH || tok == token::TK_MIN || tok == token::TK_MAX || tok == token::TK_SQRT || tok == token::TK_POW || tok == token::TK_TRUE || tok == token::TK_FALSE || tok == token::TK_AND || tok == token::TK_OR || tok == token::TK_XOR || tok == token::TK_IMPLIES || tok == token::TK_NOT || tok == token::TK_ITE || tok == token::TK_MAXIMIZE || tok == token::TK_MINIMIZE || tok == 40 || tok == 41 || tok == 91 || tok == 44 || tok == 93); | ||
893 | } | ||
894 | #else | ||
895 | symbol_type (int tok, const location_type& l) | ||
896 | : super_type(token_type (tok), l) | ||
897 | { | ||
898 | YY_ASSERT (tok == token::END || tok == token::TK_EXCLAMATION || tok == token::TK_BINARY || tok == token::TK_DECIMAL || tok == token::TK_HEXADECIMAL || tok == token::TK_NUMERAL || tok == token::TK_STRING || tok == token::TK_UNDERSCORE || tok == token::TK_AS || tok == token::TK_EXISTS || tok == token::TK_FORALL || tok == token::TK_LET || tok == token::TK_PAR || tok == token::TK_ASSERT || tok == token::TK_CHECK_SAT || tok == token::TK_CHECK_SAT_ASSUMING || tok == token::TK_DECLARE_CONST || tok == token::TK_DECLARE_FUN || tok == token::TK_DECLARE_SORT || tok == token::TK_DEFINE_FUN || tok == token::TK_DEFINE_FUN_REC || tok == token::TK_DEFINE_SORT || tok == token::TK_ECHO || tok == token::TK_EXIT || tok == token::TK_GET_ASSERTIONS || tok == token::TK_GET_ASSIGNMENT || tok == token::TK_GET_INFO || tok == token::TK_GET_MODEL || tok == token::TK_GET_OPTION || tok == token::TK_GET_PROOF || tok == token::TK_GET_UNSAT_ASSUMPTIONS || tok == token::TK_GET_UNSAT_CORE || tok == token::TK_GET_VALUE || tok == token::TK_POP || tok == token::TK_PUSH || tok == token::TK_RESET || tok == token::TK_RESET_ASSERTIONS || tok == token::TK_SET_INFO || tok == token::TK_SET_LOGIC || tok == token::TK_SET_OPTION || tok == token::TK_PLUS || tok == token::TK_MINUS || tok == token::TK_TIMES || tok == token::TK_DIV || tok == token::TK_EQ || tok == token::TK_LTE || tok == token::TK_GTE || tok == token::TK_LT || tok == token::TK_GT || tok == token::TK_EXP || tok == token::TK_LOG || tok == token::TK_ABS || tok == token::TK_SIN || tok == token::TK_COS || tok == token::TK_TAN || tok == token::TK_ASIN || tok == token::TK_ACOS || tok == token::TK_ATAN || tok == token::TK_ATAN2 || tok == token::TK_SINH || tok == token::TK_COSH || tok == token::TK_TANH || tok == token::TK_MIN || tok == token::TK_MAX || tok == token::TK_SQRT || tok == token::TK_POW || tok == token::TK_TRUE || tok == token::TK_FALSE || tok == token::TK_AND || tok == token::TK_OR || tok == token::TK_XOR || tok == token::TK_IMPLIES || tok == token::TK_NOT || tok == token::TK_ITE || tok == token::TK_MAXIMIZE || tok == token::TK_MINIMIZE || tok == 40 || tok == 41 || tok == 91 || tok == 44 || tok == 93); | ||
899 | } | ||
900 | #endif | ||
901 | #if 201103L <= YY_CPLUSPLUS | ||
902 | symbol_type (int tok, double v, location_type l) | ||
903 | : super_type(token_type (tok), std::move (v), std::move (l)) | ||
904 | { | ||
905 | YY_ASSERT (tok == token::HEXFLOAT); | ||
906 | } | ||
907 | #else | ||
908 | symbol_type (int tok, const double& v, const location_type& l) | ||
909 | : super_type(token_type (tok), v, l) | ||
910 | { | ||
911 | YY_ASSERT (tok == token::HEXFLOAT); | ||
912 | } | ||
913 | #endif | ||
914 | #if 201103L <= YY_CPLUSPLUS | ||
915 | symbol_type (int tok, std::int64_t v, location_type l) | ||
916 | : super_type(token_type (tok), std::move (v), std::move (l)) | ||
917 | { | ||
918 | YY_ASSERT (tok == token::INT); | ||
919 | } | ||
920 | #else | ||
921 | symbol_type (int tok, const std::int64_t& v, const location_type& l) | ||
922 | : super_type(token_type (tok), v, l) | ||
923 | { | ||
924 | YY_ASSERT (tok == token::INT); | ||
925 | } | ||
926 | #endif | ||
927 | #if 201103L <= YY_CPLUSPLUS | ||
928 | symbol_type (int tok, std::string v, location_type l) | ||
929 | : super_type(token_type (tok), std::move (v), std::move (l)) | ||
930 | { | ||
931 | YY_ASSERT (tok == token::DOUBLE || tok == token::SYMBOL || tok == token::KEYWORD || tok == token::STRING); | ||
932 | } | ||
933 | #else | ||
934 | symbol_type (int tok, const std::string& v, const location_type& l) | ||
935 | : super_type(token_type (tok), v, l) | ||
936 | { | ||
937 | YY_ASSERT (tok == token::DOUBLE || tok == token::SYMBOL || tok == token::KEYWORD || tok == token::STRING); | ||
938 | } | ||
939 | #endif | ||
940 | }; | ||
941 | |||
942 | /// Build a parser object. | ||
943 | Smt2Parser (class Smt2Driver& driver_yyarg); | ||
944 | virtual ~Smt2Parser (); | ||
945 | |||
946 | /// Parse. An alias for parse (). | ||
947 | /// \returns 0 iff parsing succeeded. | ||
948 | int operator() (); | ||
949 | |||
950 | /// Parse. | ||
951 | /// \returns 0 iff parsing succeeded. | ||
952 | virtual int parse (); | ||
953 | |||
954 | #if DREALDEBUG | ||
955 | /// The current debugging stream. | ||
956 | std::ostream& debug_stream () const YY_ATTRIBUTE_PURE; | ||
957 | /// Set the current debugging stream. | ||
958 | void set_debug_stream (std::ostream &); | ||
959 | |||
960 | /// Type for debugging levels. | ||
961 | typedef int debug_level_type; | ||
962 | /// The current debugging level. | ||
963 | debug_level_type debug_level () const YY_ATTRIBUTE_PURE; | ||
964 | /// Set the current debugging level. | ||
965 | void set_debug_level (debug_level_type l); | ||
966 | #endif | ||
967 | |||
968 | /// Report a syntax error. | ||
969 | /// \param loc where the syntax error is found. | ||
970 | /// \param msg a description of the syntax error. | ||
971 | virtual void error (const location_type& loc, const std::string& msg); | ||
972 | |||
973 | /// Report a syntax error. | ||
974 | void error (const syntax_error& err); | ||
975 | |||
976 | // Implementation of make_symbol for each symbol type. | ||
977 | #if 201103L <= YY_CPLUSPLUS | ||
978 | static | ||
979 | symbol_type | ||
980 | make_END (location_type l) | ||
981 | { | ||
982 | return symbol_type (token::END, std::move (l)); | ||
983 | } | ||
984 | #else | ||
985 | static | ||
986 | symbol_type | ||
987 | make_END (const location_type& l) | ||
988 | { | ||
989 | return symbol_type (token::END, l); | ||
990 | } | ||
991 | #endif | ||
992 | #if 201103L <= YY_CPLUSPLUS | ||
993 | static | ||
994 | symbol_type | ||
995 | make_TK_EXCLAMATION (location_type l) | ||
996 | { | ||
997 | return symbol_type (token::TK_EXCLAMATION, std::move (l)); | ||
998 | } | ||
999 | #else | ||
1000 | static | ||
1001 | symbol_type | ||
1002 | make_TK_EXCLAMATION (const location_type& l) | ||
1003 | { | ||
1004 | return symbol_type (token::TK_EXCLAMATION, l); | ||
1005 | } | ||
1006 | #endif | ||
1007 | #if 201103L <= YY_CPLUSPLUS | ||
1008 | static | ||
1009 | symbol_type | ||
1010 | make_TK_BINARY (location_type l) | ||
1011 | { | ||
1012 | return symbol_type (token::TK_BINARY, std::move (l)); | ||
1013 | } | ||
1014 | #else | ||
1015 | static | ||
1016 | symbol_type | ||
1017 | make_TK_BINARY (const location_type& l) | ||
1018 | { | ||
1019 | return symbol_type (token::TK_BINARY, l); | ||
1020 | } | ||
1021 | #endif | ||
1022 | #if 201103L <= YY_CPLUSPLUS | ||
1023 | static | ||
1024 | symbol_type | ||
1025 | make_TK_DECIMAL (location_type l) | ||
1026 | { | ||
1027 | return symbol_type (token::TK_DECIMAL, std::move (l)); | ||
1028 | } | ||
1029 | #else | ||
1030 | static | ||
1031 | symbol_type | ||
1032 | make_TK_DECIMAL (const location_type& l) | ||
1033 | { | ||
1034 | return symbol_type (token::TK_DECIMAL, l); | ||
1035 | } | ||
1036 | #endif | ||
1037 | #if 201103L <= YY_CPLUSPLUS | ||
1038 | static | ||
1039 | symbol_type | ||
1040 | make_TK_HEXADECIMAL (location_type l) | ||
1041 | { | ||
1042 | return symbol_type (token::TK_HEXADECIMAL, std::move (l)); | ||
1043 | } | ||
1044 | #else | ||
1045 | static | ||
1046 | symbol_type | ||
1047 | make_TK_HEXADECIMAL (const location_type& l) | ||
1048 | { | ||
1049 | return symbol_type (token::TK_HEXADECIMAL, l); | ||
1050 | } | ||
1051 | #endif | ||
1052 | #if 201103L <= YY_CPLUSPLUS | ||
1053 | static | ||
1054 | symbol_type | ||
1055 | make_TK_NUMERAL (location_type l) | ||
1056 | { | ||
1057 | return symbol_type (token::TK_NUMERAL, std::move (l)); | ||
1058 | } | ||
1059 | #else | ||
1060 | static | ||
1061 | symbol_type | ||
1062 | make_TK_NUMERAL (const location_type& l) | ||
1063 | { | ||
1064 | return symbol_type (token::TK_NUMERAL, l); | ||
1065 | } | ||
1066 | #endif | ||
1067 | #if 201103L <= YY_CPLUSPLUS | ||
1068 | static | ||
1069 | symbol_type | ||
1070 | make_TK_STRING (location_type l) | ||
1071 | { | ||
1072 | return symbol_type (token::TK_STRING, std::move (l)); | ||
1073 | } | ||
1074 | #else | ||
1075 | static | ||
1076 | symbol_type | ||
1077 | make_TK_STRING (const location_type& l) | ||
1078 | { | ||
1079 | return symbol_type (token::TK_STRING, l); | ||
1080 | } | ||
1081 | #endif | ||
1082 | #if 201103L <= YY_CPLUSPLUS | ||
1083 | static | ||
1084 | symbol_type | ||
1085 | make_TK_UNDERSCORE (location_type l) | ||
1086 | { | ||
1087 | return symbol_type (token::TK_UNDERSCORE, std::move (l)); | ||
1088 | } | ||
1089 | #else | ||
1090 | static | ||
1091 | symbol_type | ||
1092 | make_TK_UNDERSCORE (const location_type& l) | ||
1093 | { | ||
1094 | return symbol_type (token::TK_UNDERSCORE, l); | ||
1095 | } | ||
1096 | #endif | ||
1097 | #if 201103L <= YY_CPLUSPLUS | ||
1098 | static | ||
1099 | symbol_type | ||
1100 | make_TK_AS (location_type l) | ||
1101 | { | ||
1102 | return symbol_type (token::TK_AS, std::move (l)); | ||
1103 | } | ||
1104 | #else | ||
1105 | static | ||
1106 | symbol_type | ||
1107 | make_TK_AS (const location_type& l) | ||
1108 | { | ||
1109 | return symbol_type (token::TK_AS, l); | ||
1110 | } | ||
1111 | #endif | ||
1112 | #if 201103L <= YY_CPLUSPLUS | ||
1113 | static | ||
1114 | symbol_type | ||
1115 | make_TK_EXISTS (location_type l) | ||
1116 | { | ||
1117 | return symbol_type (token::TK_EXISTS, std::move (l)); | ||
1118 | } | ||
1119 | #else | ||
1120 | static | ||
1121 | symbol_type | ||
1122 | make_TK_EXISTS (const location_type& l) | ||
1123 | { | ||
1124 | return symbol_type (token::TK_EXISTS, l); | ||
1125 | } | ||
1126 | #endif | ||
1127 | #if 201103L <= YY_CPLUSPLUS | ||
1128 | static | ||
1129 | symbol_type | ||
1130 | make_TK_FORALL (location_type l) | ||
1131 | { | ||
1132 | return symbol_type (token::TK_FORALL, std::move (l)); | ||
1133 | } | ||
1134 | #else | ||
1135 | static | ||
1136 | symbol_type | ||
1137 | make_TK_FORALL (const location_type& l) | ||
1138 | { | ||
1139 | return symbol_type (token::TK_FORALL, l); | ||
1140 | } | ||
1141 | #endif | ||
1142 | #if 201103L <= YY_CPLUSPLUS | ||
1143 | static | ||
1144 | symbol_type | ||
1145 | make_TK_LET (location_type l) | ||
1146 | { | ||
1147 | return symbol_type (token::TK_LET, std::move (l)); | ||
1148 | } | ||
1149 | #else | ||
1150 | static | ||
1151 | symbol_type | ||
1152 | make_TK_LET (const location_type& l) | ||
1153 | { | ||
1154 | return symbol_type (token::TK_LET, l); | ||
1155 | } | ||
1156 | #endif | ||
1157 | #if 201103L <= YY_CPLUSPLUS | ||
1158 | static | ||
1159 | symbol_type | ||
1160 | make_TK_PAR (location_type l) | ||
1161 | { | ||
1162 | return symbol_type (token::TK_PAR, std::move (l)); | ||
1163 | } | ||
1164 | #else | ||
1165 | static | ||
1166 | symbol_type | ||
1167 | make_TK_PAR (const location_type& l) | ||
1168 | { | ||
1169 | return symbol_type (token::TK_PAR, l); | ||
1170 | } | ||
1171 | #endif | ||
1172 | #if 201103L <= YY_CPLUSPLUS | ||
1173 | static | ||
1174 | symbol_type | ||
1175 | make_TK_ASSERT (location_type l) | ||
1176 | { | ||
1177 | return symbol_type (token::TK_ASSERT, std::move (l)); | ||
1178 | } | ||
1179 | #else | ||
1180 | static | ||
1181 | symbol_type | ||
1182 | make_TK_ASSERT (const location_type& l) | ||
1183 | { | ||
1184 | return symbol_type (token::TK_ASSERT, l); | ||
1185 | } | ||
1186 | #endif | ||
1187 | #if 201103L <= YY_CPLUSPLUS | ||
1188 | static | ||
1189 | symbol_type | ||
1190 | make_TK_CHECK_SAT (location_type l) | ||
1191 | { | ||
1192 | return symbol_type (token::TK_CHECK_SAT, std::move (l)); | ||
1193 | } | ||
1194 | #else | ||
1195 | static | ||
1196 | symbol_type | ||
1197 | make_TK_CHECK_SAT (const location_type& l) | ||
1198 | { | ||
1199 | return symbol_type (token::TK_CHECK_SAT, l); | ||
1200 | } | ||
1201 | #endif | ||
1202 | #if 201103L <= YY_CPLUSPLUS | ||
1203 | static | ||
1204 | symbol_type | ||
1205 | make_TK_CHECK_SAT_ASSUMING (location_type l) | ||
1206 | { | ||
1207 | return symbol_type (token::TK_CHECK_SAT_ASSUMING, std::move (l)); | ||
1208 | } | ||
1209 | #else | ||
1210 | static | ||
1211 | symbol_type | ||
1212 | make_TK_CHECK_SAT_ASSUMING (const location_type& l) | ||
1213 | { | ||
1214 | return symbol_type (token::TK_CHECK_SAT_ASSUMING, l); | ||
1215 | } | ||
1216 | #endif | ||
1217 | #if 201103L <= YY_CPLUSPLUS | ||
1218 | static | ||
1219 | symbol_type | ||
1220 | make_TK_DECLARE_CONST (location_type l) | ||
1221 | { | ||
1222 | return symbol_type (token::TK_DECLARE_CONST, std::move (l)); | ||
1223 | } | ||
1224 | #else | ||
1225 | static | ||
1226 | symbol_type | ||
1227 | make_TK_DECLARE_CONST (const location_type& l) | ||
1228 | { | ||
1229 | return symbol_type (token::TK_DECLARE_CONST, l); | ||
1230 | } | ||
1231 | #endif | ||
1232 | #if 201103L <= YY_CPLUSPLUS | ||
1233 | static | ||
1234 | symbol_type | ||
1235 | make_TK_DECLARE_FUN (location_type l) | ||
1236 | { | ||
1237 | return symbol_type (token::TK_DECLARE_FUN, std::move (l)); | ||
1238 | } | ||
1239 | #else | ||
1240 | static | ||
1241 | symbol_type | ||
1242 | make_TK_DECLARE_FUN (const location_type& l) | ||
1243 | { | ||
1244 | return symbol_type (token::TK_DECLARE_FUN, l); | ||
1245 | } | ||
1246 | #endif | ||
1247 | #if 201103L <= YY_CPLUSPLUS | ||
1248 | static | ||
1249 | symbol_type | ||
1250 | make_TK_DECLARE_SORT (location_type l) | ||
1251 | { | ||
1252 | return symbol_type (token::TK_DECLARE_SORT, std::move (l)); | ||
1253 | } | ||
1254 | #else | ||
1255 | static | ||
1256 | symbol_type | ||
1257 | make_TK_DECLARE_SORT (const location_type& l) | ||
1258 | { | ||
1259 | return symbol_type (token::TK_DECLARE_SORT, l); | ||
1260 | } | ||
1261 | #endif | ||
1262 | #if 201103L <= YY_CPLUSPLUS | ||
1263 | static | ||
1264 | symbol_type | ||
1265 | make_TK_DEFINE_FUN (location_type l) | ||
1266 | { | ||
1267 | return symbol_type (token::TK_DEFINE_FUN, std::move (l)); | ||
1268 | } | ||
1269 | #else | ||
1270 | static | ||
1271 | symbol_type | ||
1272 | make_TK_DEFINE_FUN (const location_type& l) | ||
1273 | { | ||
1274 | return symbol_type (token::TK_DEFINE_FUN, l); | ||
1275 | } | ||
1276 | #endif | ||
1277 | #if 201103L <= YY_CPLUSPLUS | ||
1278 | static | ||
1279 | symbol_type | ||
1280 | make_TK_DEFINE_FUN_REC (location_type l) | ||
1281 | { | ||
1282 | return symbol_type (token::TK_DEFINE_FUN_REC, std::move (l)); | ||
1283 | } | ||
1284 | #else | ||
1285 | static | ||
1286 | symbol_type | ||
1287 | make_TK_DEFINE_FUN_REC (const location_type& l) | ||
1288 | { | ||
1289 | return symbol_type (token::TK_DEFINE_FUN_REC, l); | ||
1290 | } | ||
1291 | #endif | ||
1292 | #if 201103L <= YY_CPLUSPLUS | ||
1293 | static | ||
1294 | symbol_type | ||
1295 | make_TK_DEFINE_SORT (location_type l) | ||
1296 | { | ||
1297 | return symbol_type (token::TK_DEFINE_SORT, std::move (l)); | ||
1298 | } | ||
1299 | #else | ||
1300 | static | ||
1301 | symbol_type | ||
1302 | make_TK_DEFINE_SORT (const location_type& l) | ||
1303 | { | ||
1304 | return symbol_type (token::TK_DEFINE_SORT, l); | ||
1305 | } | ||
1306 | #endif | ||
1307 | #if 201103L <= YY_CPLUSPLUS | ||
1308 | static | ||
1309 | symbol_type | ||
1310 | make_TK_ECHO (location_type l) | ||
1311 | { | ||
1312 | return symbol_type (token::TK_ECHO, std::move (l)); | ||
1313 | } | ||
1314 | #else | ||
1315 | static | ||
1316 | symbol_type | ||
1317 | make_TK_ECHO (const location_type& l) | ||
1318 | { | ||
1319 | return symbol_type (token::TK_ECHO, l); | ||
1320 | } | ||
1321 | #endif | ||
1322 | #if 201103L <= YY_CPLUSPLUS | ||
1323 | static | ||
1324 | symbol_type | ||
1325 | make_TK_EXIT (location_type l) | ||
1326 | { | ||
1327 | return symbol_type (token::TK_EXIT, std::move (l)); | ||
1328 | } | ||
1329 | #else | ||
1330 | static | ||
1331 | symbol_type | ||
1332 | make_TK_EXIT (const location_type& l) | ||
1333 | { | ||
1334 | return symbol_type (token::TK_EXIT, l); | ||
1335 | } | ||
1336 | #endif | ||
1337 | #if 201103L <= YY_CPLUSPLUS | ||
1338 | static | ||
1339 | symbol_type | ||
1340 | make_TK_GET_ASSERTIONS (location_type l) | ||
1341 | { | ||
1342 | return symbol_type (token::TK_GET_ASSERTIONS, std::move (l)); | ||
1343 | } | ||
1344 | #else | ||
1345 | static | ||
1346 | symbol_type | ||
1347 | make_TK_GET_ASSERTIONS (const location_type& l) | ||
1348 | { | ||
1349 | return symbol_type (token::TK_GET_ASSERTIONS, l); | ||
1350 | } | ||
1351 | #endif | ||
1352 | #if 201103L <= YY_CPLUSPLUS | ||
1353 | static | ||
1354 | symbol_type | ||
1355 | make_TK_GET_ASSIGNMENT (location_type l) | ||
1356 | { | ||
1357 | return symbol_type (token::TK_GET_ASSIGNMENT, std::move (l)); | ||
1358 | } | ||
1359 | #else | ||
1360 | static | ||
1361 | symbol_type | ||
1362 | make_TK_GET_ASSIGNMENT (const location_type& l) | ||
1363 | { | ||
1364 | return symbol_type (token::TK_GET_ASSIGNMENT, l); | ||
1365 | } | ||
1366 | #endif | ||
1367 | #if 201103L <= YY_CPLUSPLUS | ||
1368 | static | ||
1369 | symbol_type | ||
1370 | make_TK_GET_INFO (location_type l) | ||
1371 | { | ||
1372 | return symbol_type (token::TK_GET_INFO, std::move (l)); | ||
1373 | } | ||
1374 | #else | ||
1375 | static | ||
1376 | symbol_type | ||
1377 | make_TK_GET_INFO (const location_type& l) | ||
1378 | { | ||
1379 | return symbol_type (token::TK_GET_INFO, l); | ||
1380 | } | ||
1381 | #endif | ||
1382 | #if 201103L <= YY_CPLUSPLUS | ||
1383 | static | ||
1384 | symbol_type | ||
1385 | make_TK_GET_MODEL (location_type l) | ||
1386 | { | ||
1387 | return symbol_type (token::TK_GET_MODEL, std::move (l)); | ||
1388 | } | ||
1389 | #else | ||
1390 | static | ||
1391 | symbol_type | ||
1392 | make_TK_GET_MODEL (const location_type& l) | ||
1393 | { | ||
1394 | return symbol_type (token::TK_GET_MODEL, l); | ||
1395 | } | ||
1396 | #endif | ||
1397 | #if 201103L <= YY_CPLUSPLUS | ||
1398 | static | ||
1399 | symbol_type | ||
1400 | make_TK_GET_OPTION (location_type l) | ||
1401 | { | ||
1402 | return symbol_type (token::TK_GET_OPTION, std::move (l)); | ||
1403 | } | ||
1404 | #else | ||
1405 | static | ||
1406 | symbol_type | ||
1407 | make_TK_GET_OPTION (const location_type& l) | ||
1408 | { | ||
1409 | return symbol_type (token::TK_GET_OPTION, l); | ||
1410 | } | ||
1411 | #endif | ||
1412 | #if 201103L <= YY_CPLUSPLUS | ||
1413 | static | ||
1414 | symbol_type | ||
1415 | make_TK_GET_PROOF (location_type l) | ||
1416 | { | ||
1417 | return symbol_type (token::TK_GET_PROOF, std::move (l)); | ||
1418 | } | ||
1419 | #else | ||
1420 | static | ||
1421 | symbol_type | ||
1422 | make_TK_GET_PROOF (const location_type& l) | ||
1423 | { | ||
1424 | return symbol_type (token::TK_GET_PROOF, l); | ||
1425 | } | ||
1426 | #endif | ||
1427 | #if 201103L <= YY_CPLUSPLUS | ||
1428 | static | ||
1429 | symbol_type | ||
1430 | make_TK_GET_UNSAT_ASSUMPTIONS (location_type l) | ||
1431 | { | ||
1432 | return symbol_type (token::TK_GET_UNSAT_ASSUMPTIONS, std::move (l)); | ||
1433 | } | ||
1434 | #else | ||
1435 | static | ||
1436 | symbol_type | ||
1437 | make_TK_GET_UNSAT_ASSUMPTIONS (const location_type& l) | ||
1438 | { | ||
1439 | return symbol_type (token::TK_GET_UNSAT_ASSUMPTIONS, l); | ||
1440 | } | ||
1441 | #endif | ||
1442 | #if 201103L <= YY_CPLUSPLUS | ||
1443 | static | ||
1444 | symbol_type | ||
1445 | make_TK_GET_UNSAT_CORE (location_type l) | ||
1446 | { | ||
1447 | return symbol_type (token::TK_GET_UNSAT_CORE, std::move (l)); | ||
1448 | } | ||
1449 | #else | ||
1450 | static | ||
1451 | symbol_type | ||
1452 | make_TK_GET_UNSAT_CORE (const location_type& l) | ||
1453 | { | ||
1454 | return symbol_type (token::TK_GET_UNSAT_CORE, l); | ||
1455 | } | ||
1456 | #endif | ||
1457 | #if 201103L <= YY_CPLUSPLUS | ||
1458 | static | ||
1459 | symbol_type | ||
1460 | make_TK_GET_VALUE (location_type l) | ||
1461 | { | ||
1462 | return symbol_type (token::TK_GET_VALUE, std::move (l)); | ||
1463 | } | ||
1464 | #else | ||
1465 | static | ||
1466 | symbol_type | ||
1467 | make_TK_GET_VALUE (const location_type& l) | ||
1468 | { | ||
1469 | return symbol_type (token::TK_GET_VALUE, l); | ||
1470 | } | ||
1471 | #endif | ||
1472 | #if 201103L <= YY_CPLUSPLUS | ||
1473 | static | ||
1474 | symbol_type | ||
1475 | make_TK_POP (location_type l) | ||
1476 | { | ||
1477 | return symbol_type (token::TK_POP, std::move (l)); | ||
1478 | } | ||
1479 | #else | ||
1480 | static | ||
1481 | symbol_type | ||
1482 | make_TK_POP (const location_type& l) | ||
1483 | { | ||
1484 | return symbol_type (token::TK_POP, l); | ||
1485 | } | ||
1486 | #endif | ||
1487 | #if 201103L <= YY_CPLUSPLUS | ||
1488 | static | ||
1489 | symbol_type | ||
1490 | make_TK_PUSH (location_type l) | ||
1491 | { | ||
1492 | return symbol_type (token::TK_PUSH, std::move (l)); | ||
1493 | } | ||
1494 | #else | ||
1495 | static | ||
1496 | symbol_type | ||
1497 | make_TK_PUSH (const location_type& l) | ||
1498 | { | ||
1499 | return symbol_type (token::TK_PUSH, l); | ||
1500 | } | ||
1501 | #endif | ||
1502 | #if 201103L <= YY_CPLUSPLUS | ||
1503 | static | ||
1504 | symbol_type | ||
1505 | make_TK_RESET (location_type l) | ||
1506 | { | ||
1507 | return symbol_type (token::TK_RESET, std::move (l)); | ||
1508 | } | ||
1509 | #else | ||
1510 | static | ||
1511 | symbol_type | ||
1512 | make_TK_RESET (const location_type& l) | ||
1513 | { | ||
1514 | return symbol_type (token::TK_RESET, l); | ||
1515 | } | ||
1516 | #endif | ||
1517 | #if 201103L <= YY_CPLUSPLUS | ||
1518 | static | ||
1519 | symbol_type | ||
1520 | make_TK_RESET_ASSERTIONS (location_type l) | ||
1521 | { | ||
1522 | return symbol_type (token::TK_RESET_ASSERTIONS, std::move (l)); | ||
1523 | } | ||
1524 | #else | ||
1525 | static | ||
1526 | symbol_type | ||
1527 | make_TK_RESET_ASSERTIONS (const location_type& l) | ||
1528 | { | ||
1529 | return symbol_type (token::TK_RESET_ASSERTIONS, l); | ||
1530 | } | ||
1531 | #endif | ||
1532 | #if 201103L <= YY_CPLUSPLUS | ||
1533 | static | ||
1534 | symbol_type | ||
1535 | make_TK_SET_INFO (location_type l) | ||
1536 | { | ||
1537 | return symbol_type (token::TK_SET_INFO, std::move (l)); | ||
1538 | } | ||
1539 | #else | ||
1540 | static | ||
1541 | symbol_type | ||
1542 | make_TK_SET_INFO (const location_type& l) | ||
1543 | { | ||
1544 | return symbol_type (token::TK_SET_INFO, l); | ||
1545 | } | ||
1546 | #endif | ||
1547 | #if 201103L <= YY_CPLUSPLUS | ||
1548 | static | ||
1549 | symbol_type | ||
1550 | make_TK_SET_LOGIC (location_type l) | ||
1551 | { | ||
1552 | return symbol_type (token::TK_SET_LOGIC, std::move (l)); | ||
1553 | } | ||
1554 | #else | ||
1555 | static | ||
1556 | symbol_type | ||
1557 | make_TK_SET_LOGIC (const location_type& l) | ||
1558 | { | ||
1559 | return symbol_type (token::TK_SET_LOGIC, l); | ||
1560 | } | ||
1561 | #endif | ||
1562 | #if 201103L <= YY_CPLUSPLUS | ||
1563 | static | ||
1564 | symbol_type | ||
1565 | make_TK_SET_OPTION (location_type l) | ||
1566 | { | ||
1567 | return symbol_type (token::TK_SET_OPTION, std::move (l)); | ||
1568 | } | ||
1569 | #else | ||
1570 | static | ||
1571 | symbol_type | ||
1572 | make_TK_SET_OPTION (const location_type& l) | ||
1573 | { | ||
1574 | return symbol_type (token::TK_SET_OPTION, l); | ||
1575 | } | ||
1576 | #endif | ||
1577 | #if 201103L <= YY_CPLUSPLUS | ||
1578 | static | ||
1579 | symbol_type | ||
1580 | make_TK_PLUS (location_type l) | ||
1581 | { | ||
1582 | return symbol_type (token::TK_PLUS, std::move (l)); | ||
1583 | } | ||
1584 | #else | ||
1585 | static | ||
1586 | symbol_type | ||
1587 | make_TK_PLUS (const location_type& l) | ||
1588 | { | ||
1589 | return symbol_type (token::TK_PLUS, l); | ||
1590 | } | ||
1591 | #endif | ||
1592 | #if 201103L <= YY_CPLUSPLUS | ||
1593 | static | ||
1594 | symbol_type | ||
1595 | make_TK_MINUS (location_type l) | ||
1596 | { | ||
1597 | return symbol_type (token::TK_MINUS, std::move (l)); | ||
1598 | } | ||
1599 | #else | ||
1600 | static | ||
1601 | symbol_type | ||
1602 | make_TK_MINUS (const location_type& l) | ||
1603 | { | ||
1604 | return symbol_type (token::TK_MINUS, l); | ||
1605 | } | ||
1606 | #endif | ||
1607 | #if 201103L <= YY_CPLUSPLUS | ||
1608 | static | ||
1609 | symbol_type | ||
1610 | make_TK_TIMES (location_type l) | ||
1611 | { | ||
1612 | return symbol_type (token::TK_TIMES, std::move (l)); | ||
1613 | } | ||
1614 | #else | ||
1615 | static | ||
1616 | symbol_type | ||
1617 | make_TK_TIMES (const location_type& l) | ||
1618 | { | ||
1619 | return symbol_type (token::TK_TIMES, l); | ||
1620 | } | ||
1621 | #endif | ||
1622 | #if 201103L <= YY_CPLUSPLUS | ||
1623 | static | ||
1624 | symbol_type | ||
1625 | make_TK_DIV (location_type l) | ||
1626 | { | ||
1627 | return symbol_type (token::TK_DIV, std::move (l)); | ||
1628 | } | ||
1629 | #else | ||
1630 | static | ||
1631 | symbol_type | ||
1632 | make_TK_DIV (const location_type& l) | ||
1633 | { | ||
1634 | return symbol_type (token::TK_DIV, l); | ||
1635 | } | ||
1636 | #endif | ||
1637 | #if 201103L <= YY_CPLUSPLUS | ||
1638 | static | ||
1639 | symbol_type | ||
1640 | make_TK_EQ (location_type l) | ||
1641 | { | ||
1642 | return symbol_type (token::TK_EQ, std::move (l)); | ||
1643 | } | ||
1644 | #else | ||
1645 | static | ||
1646 | symbol_type | ||
1647 | make_TK_EQ (const location_type& l) | ||
1648 | { | ||
1649 | return symbol_type (token::TK_EQ, l); | ||
1650 | } | ||
1651 | #endif | ||
1652 | #if 201103L <= YY_CPLUSPLUS | ||
1653 | static | ||
1654 | symbol_type | ||
1655 | make_TK_LTE (location_type l) | ||
1656 | { | ||
1657 | return symbol_type (token::TK_LTE, std::move (l)); | ||
1658 | } | ||
1659 | #else | ||
1660 | static | ||
1661 | symbol_type | ||
1662 | make_TK_LTE (const location_type& l) | ||
1663 | { | ||
1664 | return symbol_type (token::TK_LTE, l); | ||
1665 | } | ||
1666 | #endif | ||
1667 | #if 201103L <= YY_CPLUSPLUS | ||
1668 | static | ||
1669 | symbol_type | ||
1670 | make_TK_GTE (location_type l) | ||
1671 | { | ||
1672 | return symbol_type (token::TK_GTE, std::move (l)); | ||
1673 | } | ||
1674 | #else | ||
1675 | static | ||
1676 | symbol_type | ||
1677 | make_TK_GTE (const location_type& l) | ||
1678 | { | ||
1679 | return symbol_type (token::TK_GTE, l); | ||
1680 | } | ||
1681 | #endif | ||
1682 | #if 201103L <= YY_CPLUSPLUS | ||
1683 | static | ||
1684 | symbol_type | ||
1685 | make_TK_LT (location_type l) | ||
1686 | { | ||
1687 | return symbol_type (token::TK_LT, std::move (l)); | ||
1688 | } | ||
1689 | #else | ||
1690 | static | ||
1691 | symbol_type | ||
1692 | make_TK_LT (const location_type& l) | ||
1693 | { | ||
1694 | return symbol_type (token::TK_LT, l); | ||
1695 | } | ||
1696 | #endif | ||
1697 | #if 201103L <= YY_CPLUSPLUS | ||
1698 | static | ||
1699 | symbol_type | ||
1700 | make_TK_GT (location_type l) | ||
1701 | { | ||
1702 | return symbol_type (token::TK_GT, std::move (l)); | ||
1703 | } | ||
1704 | #else | ||
1705 | static | ||
1706 | symbol_type | ||
1707 | make_TK_GT (const location_type& l) | ||
1708 | { | ||
1709 | return symbol_type (token::TK_GT, l); | ||
1710 | } | ||
1711 | #endif | ||
1712 | #if 201103L <= YY_CPLUSPLUS | ||
1713 | static | ||
1714 | symbol_type | ||
1715 | make_TK_EXP (location_type l) | ||
1716 | { | ||
1717 | return symbol_type (token::TK_EXP, std::move (l)); | ||
1718 | } | ||
1719 | #else | ||
1720 | static | ||
1721 | symbol_type | ||
1722 | make_TK_EXP (const location_type& l) | ||
1723 | { | ||
1724 | return symbol_type (token::TK_EXP, l); | ||
1725 | } | ||
1726 | #endif | ||
1727 | #if 201103L <= YY_CPLUSPLUS | ||
1728 | static | ||
1729 | symbol_type | ||
1730 | make_TK_LOG (location_type l) | ||
1731 | { | ||
1732 | return symbol_type (token::TK_LOG, std::move (l)); | ||
1733 | } | ||
1734 | #else | ||
1735 | static | ||
1736 | symbol_type | ||
1737 | make_TK_LOG (const location_type& l) | ||
1738 | { | ||
1739 | return symbol_type (token::TK_LOG, l); | ||
1740 | } | ||
1741 | #endif | ||
1742 | #if 201103L <= YY_CPLUSPLUS | ||
1743 | static | ||
1744 | symbol_type | ||
1745 | make_TK_ABS (location_type l) | ||
1746 | { | ||
1747 | return symbol_type (token::TK_ABS, std::move (l)); | ||
1748 | } | ||
1749 | #else | ||
1750 | static | ||
1751 | symbol_type | ||
1752 | make_TK_ABS (const location_type& l) | ||
1753 | { | ||
1754 | return symbol_type (token::TK_ABS, l); | ||
1755 | } | ||
1756 | #endif | ||
1757 | #if 201103L <= YY_CPLUSPLUS | ||
1758 | static | ||
1759 | symbol_type | ||
1760 | make_TK_SIN (location_type l) | ||
1761 | { | ||
1762 | return symbol_type (token::TK_SIN, std::move (l)); | ||
1763 | } | ||
1764 | #else | ||
1765 | static | ||
1766 | symbol_type | ||
1767 | make_TK_SIN (const location_type& l) | ||
1768 | { | ||
1769 | return symbol_type (token::TK_SIN, l); | ||
1770 | } | ||
1771 | #endif | ||
1772 | #if 201103L <= YY_CPLUSPLUS | ||
1773 | static | ||
1774 | symbol_type | ||
1775 | make_TK_COS (location_type l) | ||
1776 | { | ||
1777 | return symbol_type (token::TK_COS, std::move (l)); | ||
1778 | } | ||
1779 | #else | ||
1780 | static | ||
1781 | symbol_type | ||
1782 | make_TK_COS (const location_type& l) | ||
1783 | { | ||
1784 | return symbol_type (token::TK_COS, l); | ||
1785 | } | ||
1786 | #endif | ||
1787 | #if 201103L <= YY_CPLUSPLUS | ||
1788 | static | ||
1789 | symbol_type | ||
1790 | make_TK_TAN (location_type l) | ||
1791 | { | ||
1792 | return symbol_type (token::TK_TAN, std::move (l)); | ||
1793 | } | ||
1794 | #else | ||
1795 | static | ||
1796 | symbol_type | ||
1797 | make_TK_TAN (const location_type& l) | ||
1798 | { | ||
1799 | return symbol_type (token::TK_TAN, l); | ||
1800 | } | ||
1801 | #endif | ||
1802 | #if 201103L <= YY_CPLUSPLUS | ||
1803 | static | ||
1804 | symbol_type | ||
1805 | make_TK_ASIN (location_type l) | ||
1806 | { | ||
1807 | return symbol_type (token::TK_ASIN, std::move (l)); | ||
1808 | } | ||
1809 | #else | ||
1810 | static | ||
1811 | symbol_type | ||
1812 | make_TK_ASIN (const location_type& l) | ||
1813 | { | ||
1814 | return symbol_type (token::TK_ASIN, l); | ||
1815 | } | ||
1816 | #endif | ||
1817 | #if 201103L <= YY_CPLUSPLUS | ||
1818 | static | ||
1819 | symbol_type | ||
1820 | make_TK_ACOS (location_type l) | ||
1821 | { | ||
1822 | return symbol_type (token::TK_ACOS, std::move (l)); | ||
1823 | } | ||
1824 | #else | ||
1825 | static | ||
1826 | symbol_type | ||
1827 | make_TK_ACOS (const location_type& l) | ||
1828 | { | ||
1829 | return symbol_type (token::TK_ACOS, l); | ||
1830 | } | ||
1831 | #endif | ||
1832 | #if 201103L <= YY_CPLUSPLUS | ||
1833 | static | ||
1834 | symbol_type | ||
1835 | make_TK_ATAN (location_type l) | ||
1836 | { | ||
1837 | return symbol_type (token::TK_ATAN, std::move (l)); | ||
1838 | } | ||
1839 | #else | ||
1840 | static | ||
1841 | symbol_type | ||
1842 | make_TK_ATAN (const location_type& l) | ||
1843 | { | ||
1844 | return symbol_type (token::TK_ATAN, l); | ||
1845 | } | ||
1846 | #endif | ||
1847 | #if 201103L <= YY_CPLUSPLUS | ||
1848 | static | ||
1849 | symbol_type | ||
1850 | make_TK_ATAN2 (location_type l) | ||
1851 | { | ||
1852 | return symbol_type (token::TK_ATAN2, std::move (l)); | ||
1853 | } | ||
1854 | #else | ||
1855 | static | ||
1856 | symbol_type | ||
1857 | make_TK_ATAN2 (const location_type& l) | ||
1858 | { | ||
1859 | return symbol_type (token::TK_ATAN2, l); | ||
1860 | } | ||
1861 | #endif | ||
1862 | #if 201103L <= YY_CPLUSPLUS | ||
1863 | static | ||
1864 | symbol_type | ||
1865 | make_TK_SINH (location_type l) | ||
1866 | { | ||
1867 | return symbol_type (token::TK_SINH, std::move (l)); | ||
1868 | } | ||
1869 | #else | ||
1870 | static | ||
1871 | symbol_type | ||
1872 | make_TK_SINH (const location_type& l) | ||
1873 | { | ||
1874 | return symbol_type (token::TK_SINH, l); | ||
1875 | } | ||
1876 | #endif | ||
1877 | #if 201103L <= YY_CPLUSPLUS | ||
1878 | static | ||
1879 | symbol_type | ||
1880 | make_TK_COSH (location_type l) | ||
1881 | { | ||
1882 | return symbol_type (token::TK_COSH, std::move (l)); | ||
1883 | } | ||
1884 | #else | ||
1885 | static | ||
1886 | symbol_type | ||
1887 | make_TK_COSH (const location_type& l) | ||
1888 | { | ||
1889 | return symbol_type (token::TK_COSH, l); | ||
1890 | } | ||
1891 | #endif | ||
1892 | #if 201103L <= YY_CPLUSPLUS | ||
1893 | static | ||
1894 | symbol_type | ||
1895 | make_TK_TANH (location_type l) | ||
1896 | { | ||
1897 | return symbol_type (token::TK_TANH, std::move (l)); | ||
1898 | } | ||
1899 | #else | ||
1900 | static | ||
1901 | symbol_type | ||
1902 | make_TK_TANH (const location_type& l) | ||
1903 | { | ||
1904 | return symbol_type (token::TK_TANH, l); | ||
1905 | } | ||
1906 | #endif | ||
1907 | #if 201103L <= YY_CPLUSPLUS | ||
1908 | static | ||
1909 | symbol_type | ||
1910 | make_TK_MIN (location_type l) | ||
1911 | { | ||
1912 | return symbol_type (token::TK_MIN, std::move (l)); | ||
1913 | } | ||
1914 | #else | ||
1915 | static | ||
1916 | symbol_type | ||
1917 | make_TK_MIN (const location_type& l) | ||
1918 | { | ||
1919 | return symbol_type (token::TK_MIN, l); | ||
1920 | } | ||
1921 | #endif | ||
1922 | #if 201103L <= YY_CPLUSPLUS | ||
1923 | static | ||
1924 | symbol_type | ||
1925 | make_TK_MAX (location_type l) | ||
1926 | { | ||
1927 | return symbol_type (token::TK_MAX, std::move (l)); | ||
1928 | } | ||
1929 | #else | ||
1930 | static | ||
1931 | symbol_type | ||
1932 | make_TK_MAX (const location_type& l) | ||
1933 | { | ||
1934 | return symbol_type (token::TK_MAX, l); | ||
1935 | } | ||
1936 | #endif | ||
1937 | #if 201103L <= YY_CPLUSPLUS | ||
1938 | static | ||
1939 | symbol_type | ||
1940 | make_TK_SQRT (location_type l) | ||
1941 | { | ||
1942 | return symbol_type (token::TK_SQRT, std::move (l)); | ||
1943 | } | ||
1944 | #else | ||
1945 | static | ||
1946 | symbol_type | ||
1947 | make_TK_SQRT (const location_type& l) | ||
1948 | { | ||
1949 | return symbol_type (token::TK_SQRT, l); | ||
1950 | } | ||
1951 | #endif | ||
1952 | #if 201103L <= YY_CPLUSPLUS | ||
1953 | static | ||
1954 | symbol_type | ||
1955 | make_TK_POW (location_type l) | ||
1956 | { | ||
1957 | return symbol_type (token::TK_POW, std::move (l)); | ||
1958 | } | ||
1959 | #else | ||
1960 | static | ||
1961 | symbol_type | ||
1962 | make_TK_POW (const location_type& l) | ||
1963 | { | ||
1964 | return symbol_type (token::TK_POW, l); | ||
1965 | } | ||
1966 | #endif | ||
1967 | #if 201103L <= YY_CPLUSPLUS | ||
1968 | static | ||
1969 | symbol_type | ||
1970 | make_TK_TRUE (location_type l) | ||
1971 | { | ||
1972 | return symbol_type (token::TK_TRUE, std::move (l)); | ||
1973 | } | ||
1974 | #else | ||
1975 | static | ||
1976 | symbol_type | ||
1977 | make_TK_TRUE (const location_type& l) | ||
1978 | { | ||
1979 | return symbol_type (token::TK_TRUE, l); | ||
1980 | } | ||
1981 | #endif | ||
1982 | #if 201103L <= YY_CPLUSPLUS | ||
1983 | static | ||
1984 | symbol_type | ||
1985 | make_TK_FALSE (location_type l) | ||
1986 | { | ||
1987 | return symbol_type (token::TK_FALSE, std::move (l)); | ||
1988 | } | ||
1989 | #else | ||
1990 | static | ||
1991 | symbol_type | ||
1992 | make_TK_FALSE (const location_type& l) | ||
1993 | { | ||
1994 | return symbol_type (token::TK_FALSE, l); | ||
1995 | } | ||
1996 | #endif | ||
1997 | #if 201103L <= YY_CPLUSPLUS | ||
1998 | static | ||
1999 | symbol_type | ||
2000 | make_TK_AND (location_type l) | ||
2001 | { | ||
2002 | return symbol_type (token::TK_AND, std::move (l)); | ||
2003 | } | ||
2004 | #else | ||
2005 | static | ||
2006 | symbol_type | ||
2007 | make_TK_AND (const location_type& l) | ||
2008 | { | ||
2009 | return symbol_type (token::TK_AND, l); | ||
2010 | } | ||
2011 | #endif | ||
2012 | #if 201103L <= YY_CPLUSPLUS | ||
2013 | static | ||
2014 | symbol_type | ||
2015 | make_TK_OR (location_type l) | ||
2016 | { | ||
2017 | return symbol_type (token::TK_OR, std::move (l)); | ||
2018 | } | ||
2019 | #else | ||
2020 | static | ||
2021 | symbol_type | ||
2022 | make_TK_OR (const location_type& l) | ||
2023 | { | ||
2024 | return symbol_type (token::TK_OR, l); | ||
2025 | } | ||
2026 | #endif | ||
2027 | #if 201103L <= YY_CPLUSPLUS | ||
2028 | static | ||
2029 | symbol_type | ||
2030 | make_TK_XOR (location_type l) | ||
2031 | { | ||
2032 | return symbol_type (token::TK_XOR, std::move (l)); | ||
2033 | } | ||
2034 | #else | ||
2035 | static | ||
2036 | symbol_type | ||
2037 | make_TK_XOR (const location_type& l) | ||
2038 | { | ||
2039 | return symbol_type (token::TK_XOR, l); | ||
2040 | } | ||
2041 | #endif | ||
2042 | #if 201103L <= YY_CPLUSPLUS | ||
2043 | static | ||
2044 | symbol_type | ||
2045 | make_TK_IMPLIES (location_type l) | ||
2046 | { | ||
2047 | return symbol_type (token::TK_IMPLIES, std::move (l)); | ||
2048 | } | ||
2049 | #else | ||
2050 | static | ||
2051 | symbol_type | ||
2052 | make_TK_IMPLIES (const location_type& l) | ||
2053 | { | ||
2054 | return symbol_type (token::TK_IMPLIES, l); | ||
2055 | } | ||
2056 | #endif | ||
2057 | #if 201103L <= YY_CPLUSPLUS | ||
2058 | static | ||
2059 | symbol_type | ||
2060 | make_TK_NOT (location_type l) | ||
2061 | { | ||
2062 | return symbol_type (token::TK_NOT, std::move (l)); | ||
2063 | } | ||
2064 | #else | ||
2065 | static | ||
2066 | symbol_type | ||
2067 | make_TK_NOT (const location_type& l) | ||
2068 | { | ||
2069 | return symbol_type (token::TK_NOT, l); | ||
2070 | } | ||
2071 | #endif | ||
2072 | #if 201103L <= YY_CPLUSPLUS | ||
2073 | static | ||
2074 | symbol_type | ||
2075 | make_TK_ITE (location_type l) | ||
2076 | { | ||
2077 | return symbol_type (token::TK_ITE, std::move (l)); | ||
2078 | } | ||
2079 | #else | ||
2080 | static | ||
2081 | symbol_type | ||
2082 | make_TK_ITE (const location_type& l) | ||
2083 | { | ||
2084 | return symbol_type (token::TK_ITE, l); | ||
2085 | } | ||
2086 | #endif | ||
2087 | #if 201103L <= YY_CPLUSPLUS | ||
2088 | static | ||
2089 | symbol_type | ||
2090 | make_TK_MAXIMIZE (location_type l) | ||
2091 | { | ||
2092 | return symbol_type (token::TK_MAXIMIZE, std::move (l)); | ||
2093 | } | ||
2094 | #else | ||
2095 | static | ||
2096 | symbol_type | ||
2097 | make_TK_MAXIMIZE (const location_type& l) | ||
2098 | { | ||
2099 | return symbol_type (token::TK_MAXIMIZE, l); | ||
2100 | } | ||
2101 | #endif | ||
2102 | #if 201103L <= YY_CPLUSPLUS | ||
2103 | static | ||
2104 | symbol_type | ||
2105 | make_TK_MINIMIZE (location_type l) | ||
2106 | { | ||
2107 | return symbol_type (token::TK_MINIMIZE, std::move (l)); | ||
2108 | } | ||
2109 | #else | ||
2110 | static | ||
2111 | symbol_type | ||
2112 | make_TK_MINIMIZE (const location_type& l) | ||
2113 | { | ||
2114 | return symbol_type (token::TK_MINIMIZE, l); | ||
2115 | } | ||
2116 | #endif | ||
2117 | #if 201103L <= YY_CPLUSPLUS | ||
2118 | static | ||
2119 | symbol_type | ||
2120 | make_DOUBLE (std::string v, location_type l) | ||
2121 | { | ||
2122 | return symbol_type (token::DOUBLE, std::move (v), std::move (l)); | ||
2123 | } | ||
2124 | #else | ||
2125 | static | ||
2126 | symbol_type | ||
2127 | make_DOUBLE (const std::string& v, const location_type& l) | ||
2128 | { | ||
2129 | return symbol_type (token::DOUBLE, v, l); | ||
2130 | } | ||
2131 | #endif | ||
2132 | #if 201103L <= YY_CPLUSPLUS | ||
2133 | static | ||
2134 | symbol_type | ||
2135 | make_HEXFLOAT (double v, location_type l) | ||
2136 | { | ||
2137 | return symbol_type (token::HEXFLOAT, std::move (v), std::move (l)); | ||
2138 | } | ||
2139 | #else | ||
2140 | static | ||
2141 | symbol_type | ||
2142 | make_HEXFLOAT (const double& v, const location_type& l) | ||
2143 | { | ||
2144 | return symbol_type (token::HEXFLOAT, v, l); | ||
2145 | } | ||
2146 | #endif | ||
2147 | #if 201103L <= YY_CPLUSPLUS | ||
2148 | static | ||
2149 | symbol_type | ||
2150 | make_INT (std::int64_t v, location_type l) | ||
2151 | { | ||
2152 | return symbol_type (token::INT, std::move (v), std::move (l)); | ||
2153 | } | ||
2154 | #else | ||
2155 | static | ||
2156 | symbol_type | ||
2157 | make_INT (const std::int64_t& v, const location_type& l) | ||
2158 | { | ||
2159 | return symbol_type (token::INT, v, l); | ||
2160 | } | ||
2161 | #endif | ||
2162 | #if 201103L <= YY_CPLUSPLUS | ||
2163 | static | ||
2164 | symbol_type | ||
2165 | make_SYMBOL (std::string v, location_type l) | ||
2166 | { | ||
2167 | return symbol_type (token::SYMBOL, std::move (v), std::move (l)); | ||
2168 | } | ||
2169 | #else | ||
2170 | static | ||
2171 | symbol_type | ||
2172 | make_SYMBOL (const std::string& v, const location_type& l) | ||
2173 | { | ||
2174 | return symbol_type (token::SYMBOL, v, l); | ||
2175 | } | ||
2176 | #endif | ||
2177 | #if 201103L <= YY_CPLUSPLUS | ||
2178 | static | ||
2179 | symbol_type | ||
2180 | make_KEYWORD (std::string v, location_type l) | ||
2181 | { | ||
2182 | return symbol_type (token::KEYWORD, std::move (v), std::move (l)); | ||
2183 | } | ||
2184 | #else | ||
2185 | static | ||
2186 | symbol_type | ||
2187 | make_KEYWORD (const std::string& v, const location_type& l) | ||
2188 | { | ||
2189 | return symbol_type (token::KEYWORD, v, l); | ||
2190 | } | ||
2191 | #endif | ||
2192 | #if 201103L <= YY_CPLUSPLUS | ||
2193 | static | ||
2194 | symbol_type | ||
2195 | make_STRING (std::string v, location_type l) | ||
2196 | { | ||
2197 | return symbol_type (token::STRING, std::move (v), std::move (l)); | ||
2198 | } | ||
2199 | #else | ||
2200 | static | ||
2201 | symbol_type | ||
2202 | make_STRING (const std::string& v, const location_type& l) | ||
2203 | { | ||
2204 | return symbol_type (token::STRING, v, l); | ||
2205 | } | ||
2206 | #endif | ||
2207 | |||
2208 | |||
2209 | private: | ||
2210 | /// This class is not copyable. | ||
2211 | Smt2Parser (const Smt2Parser&); | ||
2212 | Smt2Parser& operator= (const Smt2Parser&); | ||
2213 | |||
2214 | /// Stored state numbers (used for stacks). | ||
2215 | typedef short state_type; | ||
2216 | |||
2217 | /// Generate an error message. | ||
2218 | /// \param yystate the state where the error occurred. | ||
2219 | /// \param yyla the lookahead token. | ||
2220 | virtual std::string yysyntax_error_ (state_type yystate, | ||
2221 | const symbol_type& yyla) const; | ||
2222 | |||
2223 | /// Compute post-reduction state. | ||
2224 | /// \param yystate the current state | ||
2225 | /// \param yysym the nonterminal to push on the stack | ||
2226 | static state_type yy_lr_goto_state_ (state_type yystate, int yysym); | ||
2227 | |||
2228 | /// Whether the given \c yypact_ value indicates a defaulted state. | ||
2229 | /// \param yyvalue the value to check | ||
2230 | static bool yy_pact_value_is_default_ (int yyvalue); | ||
2231 | |||
2232 | /// Whether the given \c yytable_ value indicates a syntax error. | ||
2233 | /// \param yyvalue the value to check | ||
2234 | static bool yy_table_value_is_error_ (int yyvalue); | ||
2235 | |||
2236 | static const short yypact_ninf_; | ||
2237 | static const signed char yytable_ninf_; | ||
2238 | |||
2239 | /// Convert a scanner token number \a t to a symbol number. | ||
2240 | /// In theory \a t should be a token_type, but character literals | ||
2241 | /// are valid, yet not members of the token_type enum. | ||
2242 | static token_number_type yytranslate_ (int t); | ||
2243 | |||
2244 | // Tables. | ||
2245 | // YYPACT[STATE-NUM] -- Index in YYTABLE of the portion describing | ||
2246 | // STATE-NUM. | ||
2247 | static const short yypact_[]; | ||
2248 | |||
2249 | // YYDEFACT[STATE-NUM] -- Default reduction number in state STATE-NUM. | ||
2250 | // Performed when YYTABLE does not specify something else to do. Zero | ||
2251 | // means the default is an error. | ||
2252 | static const signed char yydefact_[]; | ||
2253 | |||
2254 | // YYPGOTO[NTERM-NUM]. | ||
2255 | static const short yypgoto_[]; | ||
2256 | |||
2257 | // YYDEFGOTO[NTERM-NUM]. | ||
2258 | static const short yydefgoto_[]; | ||
2259 | |||
2260 | // YYTABLE[YYPACT[STATE-NUM]] -- What to do in state STATE-NUM. If | ||
2261 | // positive, shift that token. If negative, reduce the rule whose | ||
2262 | // number is the opposite. If YYTABLE_NINF, syntax error. | ||
2263 | static const short yytable_[]; | ||
2264 | |||
2265 | static const short yycheck_[]; | ||
2266 | |||
2267 | // YYSTOS[STATE-NUM] -- The (internal number of the) accessing | ||
2268 | // symbol of state STATE-NUM. | ||
2269 | static const signed char yystos_[]; | ||
2270 | |||
2271 | // YYR1[YYN] -- Symbol number of symbol that rule YYN derives. | ||
2272 | static const signed char yyr1_[]; | ||
2273 | |||
2274 | // YYR2[YYN] -- Number of symbols on the right hand side of rule YYN. | ||
2275 | static const signed char yyr2_[]; | ||
2276 | |||
2277 | |||
2278 | /// Convert the symbol name \a n to a form suitable for a diagnostic. | ||
2279 | static std::string yytnamerr_ (const char *n); | ||
2280 | |||
2281 | |||
2282 | /// For a symbol, its name in clear. | ||
2283 | static const char* const yytname_[]; | ||
2284 | #if DREALDEBUG | ||
2285 | // YYRLINE[YYN] -- Source line where rule number YYN was defined. | ||
2286 | static const short yyrline_[]; | ||
2287 | /// Report on the debug stream that the rule \a r is going to be reduced. | ||
2288 | virtual void yy_reduce_print_ (int r); | ||
2289 | /// Print the state stack on the debug stream. | ||
2290 | virtual void yystack_print_ (); | ||
2291 | |||
2292 | /// Debugging level. | ||
2293 | int yydebug_; | ||
2294 | /// Debug stream. | ||
2295 | std::ostream* yycdebug_; | ||
2296 | |||
2297 | /// \brief Display a symbol type, value and location. | ||
2298 | /// \param yyo The output stream. | ||
2299 | /// \param yysym The symbol. | ||
2300 | template <typename Base> | ||
2301 | void yy_print_ (std::ostream& yyo, const basic_symbol<Base>& yysym) const; | ||
2302 | #endif | ||
2303 | |||
2304 | /// \brief Reclaim the memory associated to a symbol. | ||
2305 | /// \param yymsg Why this token is reclaimed. | ||
2306 | /// If null, print nothing. | ||
2307 | /// \param yysym The symbol. | ||
2308 | template <typename Base> | ||
2309 | void yy_destroy_ (const char* yymsg, basic_symbol<Base>& yysym) const; | ||
2310 | |||
2311 | private: | ||
2312 | /// Type access provider for state based symbols. | ||
2313 | struct by_state | ||
2314 | { | ||
2315 | /// Default constructor. | ||
2316 | by_state () YY_NOEXCEPT; | ||
2317 | |||
2318 | /// The symbol type as needed by the constructor. | ||
2319 | typedef state_type kind_type; | ||
2320 | |||
2321 | /// Constructor. | ||
2322 | by_state (kind_type s) YY_NOEXCEPT; | ||
2323 | |||
2324 | /// Copy constructor. | ||
2325 | by_state (const by_state& that) YY_NOEXCEPT; | ||
2326 | |||
2327 | /// Record that this symbol is empty. | ||
2328 | void clear () YY_NOEXCEPT; | ||
2329 | |||
2330 | /// Steal the symbol type from \a that. | ||
2331 | void move (by_state& that); | ||
2332 | |||
2333 | /// The (internal) type number (corresponding to \a state). | ||
2334 | /// \a empty_symbol when empty. | ||
2335 | symbol_number_type type_get () const YY_NOEXCEPT; | ||
2336 | |||
2337 | /// The state number used to denote an empty symbol. | ||
2338 | /// We use the initial state, as it does not have a value. | ||
2339 | enum { empty_state = 0 }; | ||
2340 | |||
2341 | /// The state. | ||
2342 | /// \a empty when empty. | ||
2343 | state_type state; | ||
2344 | }; | ||
2345 | |||
2346 | /// "Internal" symbol: element of the stack. | ||
2347 | struct stack_symbol_type : basic_symbol<by_state> | ||
2348 | { | ||
2349 | /// Superclass. | ||
2350 | typedef basic_symbol<by_state> super_type; | ||
2351 | /// Construct an empty symbol. | ||
2352 | stack_symbol_type (); | ||
2353 | /// Move or copy construction. | ||
2354 | stack_symbol_type (YY_RVREF (stack_symbol_type) that); | ||
2355 | /// Steal the contents from \a sym to build this. | ||
2356 | stack_symbol_type (state_type s, YY_MOVE_REF (symbol_type) sym); | ||
2357 | #if YY_CPLUSPLUS < 201103L | ||
2358 | /// Assignment, needed by push_back by some old implementations. | ||
2359 | /// Moves the contents of that. | ||
2360 | stack_symbol_type& operator= (stack_symbol_type& that); | ||
2361 | |||
2362 | /// Assignment, needed by push_back by other implementations. | ||
2363 | /// Needed by some other old implementations. | ||
2364 | stack_symbol_type& operator= (const stack_symbol_type& that); | ||
2365 | #endif | ||
2366 | }; | ||
2367 | |||
2368 | /// A stack with random access from its top. | ||
2369 | template <typename T, typename S = std::vector<T> > | ||
2370 | class stack | ||
2371 | { | ||
2372 | public: | ||
2373 | // Hide our reversed order. | ||
2374 | typedef typename S::reverse_iterator iterator; | ||
2375 | typedef typename S::const_reverse_iterator const_iterator; | ||
2376 | typedef typename S::size_type size_type; | ||
2377 | typedef typename std::ptrdiff_t index_type; | ||
2378 | |||
2379 | stack (size_type n = 200) | ||
2380 | : seq_ (n) | ||
2381 | {} | ||
2382 | |||
2383 | /// Random access. | ||
2384 | /// | ||
2385 | /// Index 0 returns the topmost element. | ||
2386 | const T& | ||
2387 | operator[] (index_type i) const | ||
2388 | { | ||
2389 | return seq_[size_type (size () - 1 - i)]; | ||
2390 | } | ||
2391 | |||
2392 | /// Random access. | ||
2393 | /// | ||
2394 | /// Index 0 returns the topmost element. | ||
2395 | T& | ||
2396 | operator[] (index_type i) | ||
2397 | { | ||
2398 | return seq_[size_type (size () - 1 - i)]; | ||
2399 | } | ||
2400 | |||
2401 | /// Steal the contents of \a t. | ||
2402 | /// | ||
2403 | /// Close to move-semantics. | ||
2404 | void | ||
2405 | push (YY_MOVE_REF (T) t) | ||
2406 | { | ||
2407 | seq_.push_back (T ()); | ||
2408 | operator[] (0).move (t); | ||
2409 | } | ||
2410 | |||
2411 | /// Pop elements from the stack. | ||
2412 | void | ||
2413 | pop (std::ptrdiff_t n = 1) YY_NOEXCEPT | ||
2414 | { | ||
2415 | for (; 0 < n; --n) | ||
2416 | seq_.pop_back (); | ||
2417 | } | ||
2418 | |||
2419 | /// Pop all elements from the stack. | ||
2420 | void | ||
2421 | clear () YY_NOEXCEPT | ||
2422 | { | ||
2423 | seq_.clear (); | ||
2424 | } | ||
2425 | |||
2426 | /// Number of elements on the stack. | ||
2427 | index_type | ||
2428 | size () const YY_NOEXCEPT | ||
2429 | { | ||
2430 | return index_type (seq_.size ()); | ||
2431 | } | ||
2432 | |||
2433 | std::ptrdiff_t | ||
2434 | ssize () const YY_NOEXCEPT | ||
2435 | { | ||
2436 | return std::ptrdiff_t (size ()); | ||
2437 | } | ||
2438 | |||
2439 | /// Iterator on top of the stack (going downwards). | ||
2440 | const_iterator | ||
2441 | begin () const YY_NOEXCEPT | ||
2442 | { | ||
2443 | return seq_.rbegin (); | ||
2444 | } | ||
2445 | |||
2446 | /// Bottom of the stack. | ||
2447 | const_iterator | ||
2448 | end () const YY_NOEXCEPT | ||
2449 | { | ||
2450 | return seq_.rend (); | ||
2451 | } | ||
2452 | |||
2453 | /// Present a slice of the top of a stack. | ||
2454 | class slice | ||
2455 | { | ||
2456 | public: | ||
2457 | slice (const stack& stack, index_type range) | ||
2458 | : stack_ (stack) | ||
2459 | , range_ (range) | ||
2460 | {} | ||
2461 | |||
2462 | const T& | ||
2463 | operator[] (index_type i) const | ||
2464 | { | ||
2465 | return stack_[range_ - i]; | ||
2466 | } | ||
2467 | |||
2468 | private: | ||
2469 | const stack& stack_; | ||
2470 | index_type range_; | ||
2471 | }; | ||
2472 | |||
2473 | private: | ||
2474 | stack (const stack&); | ||
2475 | stack& operator= (const stack&); | ||
2476 | /// The wrapped container. | ||
2477 | S seq_; | ||
2478 | }; | ||
2479 | |||
2480 | |||
2481 | /// Stack type. | ||
2482 | typedef stack<stack_symbol_type> stack_type; | ||
2483 | |||
2484 | /// The stack. | ||
2485 | stack_type yystack_; | ||
2486 | |||
2487 | /// Push a new state on the stack. | ||
2488 | /// \param m a debug message to display | ||
2489 | /// if null, no trace is output. | ||
2490 | /// \param sym the symbol | ||
2491 | /// \warning the contents of \a s.value is stolen. | ||
2492 | void yypush_ (const char* m, YY_MOVE_REF (stack_symbol_type) sym); | ||
2493 | |||
2494 | /// Push a new look ahead token on the state on the stack. | ||
2495 | /// \param m a debug message to display | ||
2496 | /// if null, no trace is output. | ||
2497 | /// \param s the state | ||
2498 | /// \param sym the symbol (for its value and location). | ||
2499 | /// \warning the contents of \a sym.value is stolen. | ||
2500 | void yypush_ (const char* m, state_type s, YY_MOVE_REF (symbol_type) sym); | ||
2501 | |||
2502 | /// Pop \a n symbols from the stack. | ||
2503 | void yypop_ (int n = 1); | ||
2504 | |||
2505 | /// Some specific tokens. | ||
2506 | static const token_number_type yy_error_token_ = 1; | ||
2507 | static const token_number_type yy_undef_token_ = 2; | ||
2508 | |||
2509 | /// Constants. | ||
2510 | enum | ||
2511 | { | ||
2512 | yyeof_ = 0, | ||
2513 | yylast_ = 345, ///< Last index in yytable_. | ||
2514 | yynnts_ = 31, ///< Number of nonterminal symbols. | ||
2515 | yyfinal_ = 36, ///< Termination state number. | ||
2516 | yyntokens_ = 89 ///< Number of tokens. | ||
2517 | }; | ||
2518 | |||
2519 | |||
2520 | // User arguments. | ||
2521 | class Smt2Driver& driver; | ||
2522 | }; | ||
2523 | |||
2524 | |||
2525 | } // dreal | ||
2526 | #line 2527 "bazel-out/k8-opt/bin/dreal/smt2/parser.yy.hh" | ||
2527 | |||
2528 | |||
2529 | |||
2530 | |||
2531 | |||
2532 | #endif // !YY_DREAL_BAZEL_OUT_K8_OPT_BIN_DREAL_SMT2_PARSER_YY_HH_INCLUDED | ||