aboutsummaryrefslogtreecommitdiffstats
path: root/Solvers/dreal4/bazel-bin/dreal/smt2/scanner.ll.cc
diff options
context:
space:
mode:
Diffstat (limited to 'Solvers/dreal4/bazel-bin/dreal/smt2/scanner.ll.cc')
-rwxr-xr-xSolvers/dreal4/bazel-bin/dreal/smt2/scanner.ll.cc2854
1 files changed, 2854 insertions, 0 deletions
diff --git a/Solvers/dreal4/bazel-bin/dreal/smt2/scanner.ll.cc b/Solvers/dreal4/bazel-bin/dreal/smt2/scanner.ll.cc
new file mode 100755
index 00000000..29c5e52d
--- /dev/null
+++ b/Solvers/dreal4/bazel-bin/dreal/smt2/scanner.ll.cc
@@ -0,0 +1,2854 @@
1#line 1 "bazel-out/k8-opt/bin/dreal/smt2/scanner.ll.cc"
2
3#line 3 "bazel-out/k8-opt/bin/dreal/smt2/scanner.ll.cc"
4
5#define YY_INT_ALIGNED short int
6
7/* A lexical scanner generated by flex */
8
9/* %not-for-header */
10/* %if-c-only */
11/* %if-not-reentrant */
12/* %endif */
13/* %endif */
14/* %ok-for-header */
15
16#define FLEX_SCANNER
17#define YY_FLEX_MAJOR_VERSION 2
18#define YY_FLEX_MINOR_VERSION 6
19#define YY_FLEX_SUBMINOR_VERSION 4
20#if YY_FLEX_SUBMINOR_VERSION > 0
21#define FLEX_BETA
22#endif
23
24/* %if-c++-only */
25 /* The c++ scanner is a mess. The FlexLexer.h header file relies on the
26 * following macro. This is required in order to pass the c++-multiple-scanners
27 * test in the regression suite. We get reports that it breaks inheritance.
28 * We will address this in a future release of flex, or omit the C++ scanner
29 * altogether.
30 */
31 #define yyFlexLexer Smt2FlexLexer
32/* %endif */
33
34/* %if-c-only */
35/* %endif */
36
37#ifdef yyalloc
38#define Smt2alloc_ALREADY_DEFINED
39#else
40#define yyalloc Smt2alloc
41#endif
42
43#ifdef yyrealloc
44#define Smt2realloc_ALREADY_DEFINED
45#else
46#define yyrealloc Smt2realloc
47#endif
48
49#ifdef yyfree
50#define Smt2free_ALREADY_DEFINED
51#else
52#define yyfree Smt2free
53#endif
54
55/* %if-c-only */
56/* %endif */
57
58/* First, we deal with platform-specific or compiler-specific issues. */
59
60/* begin standard C headers. */
61/* %if-c-only */
62/* %endif */
63
64/* %if-tables-serialization */
65/* %endif */
66/* end standard C headers. */
67
68/* %if-c-or-c++ */
69/* flex integer type definitions */
70
71#ifndef FLEXINT_H
72#define FLEXINT_H
73
74/* C99 systems have <inttypes.h>. Non-C99 systems may or may not. */
75
76#if defined (__STDC_VERSION__) && __STDC_VERSION__ >= 199901L
77
78/* C99 says to define __STDC_LIMIT_MACROS before including stdint.h,
79 * if you want the limit (max/min) macros for int types.
80 */
81#ifndef __STDC_LIMIT_MACROS
82#define __STDC_LIMIT_MACROS 1
83#endif
84
85#include <inttypes.h>
86typedef int8_t flex_int8_t;
87typedef uint8_t flex_uint8_t;
88typedef int16_t flex_int16_t;
89typedef uint16_t flex_uint16_t;
90typedef int32_t flex_int32_t;
91typedef uint32_t flex_uint32_t;
92#else
93typedef signed char flex_int8_t;
94typedef short int flex_int16_t;
95typedef int flex_int32_t;
96typedef unsigned char flex_uint8_t;
97typedef unsigned short int flex_uint16_t;
98typedef unsigned int flex_uint32_t;
99
100/* Limits of integral types. */
101#ifndef INT8_MIN
102#define INT8_MIN (-128)
103#endif
104#ifndef INT16_MIN
105#define INT16_MIN (-32767-1)
106#endif
107#ifndef INT32_MIN
108#define INT32_MIN (-2147483647-1)
109#endif
110#ifndef INT8_MAX
111#define INT8_MAX (127)
112#endif
113#ifndef INT16_MAX
114#define INT16_MAX (32767)
115#endif
116#ifndef INT32_MAX
117#define INT32_MAX (2147483647)
118#endif
119#ifndef UINT8_MAX
120#define UINT8_MAX (255U)
121#endif
122#ifndef UINT16_MAX
123#define UINT16_MAX (65535U)
124#endif
125#ifndef UINT32_MAX
126#define UINT32_MAX (4294967295U)
127#endif
128
129#ifndef SIZE_MAX
130#define SIZE_MAX (~(size_t)0)
131#endif
132
133#endif /* ! C99 */
134
135#endif /* ! FLEXINT_H */
136
137/* %endif */
138
139/* begin standard C++ headers. */
140/* %if-c++-only */
141#include <iostream>
142#include <errno.h>
143#include <cstdlib>
144#include <cstdio>
145#include <cstring>
146/* end standard C++ headers. */
147/* %endif */
148
149/* TODO: this is always defined, so inline it */
150#define yyconst const
151
152#if defined(__GNUC__) && __GNUC__ >= 3
153#define yynoreturn __attribute__((__noreturn__))
154#else
155#define yynoreturn
156#endif
157
158/* %not-for-header */
159/* Returned upon end-of-file. */
160#define YY_NULL 0
161/* %ok-for-header */
162
163/* %not-for-header */
164/* Promotes a possibly negative, possibly signed char to an
165 * integer in range [0..255] for use as an array index.
166 */
167#define YY_SC_TO_UI(c) ((YY_CHAR) (c))
168/* %ok-for-header */
169
170/* %if-reentrant */
171/* %endif */
172
173/* %if-not-reentrant */
174
175/* %endif */
176
177/* Enter a start condition. This macro really ought to take a parameter,
178 * but we do it the disgusting crufty way forced on us by the ()-less
179 * definition of BEGIN.
180 */
181#define BEGIN (yy_start) = 1 + 2 *
182/* Translate the current start state into a value that can be later handed
183 * to BEGIN to return to the state. The YYSTATE alias is for lex
184 * compatibility.
185 */
186#define YY_START (((yy_start) - 1) / 2)
187#define YYSTATE YY_START
188/* Action number for EOF rule of a given start state. */
189#define YY_STATE_EOF(state) (YY_END_OF_BUFFER + state + 1)
190/* Special action meaning "start processing a new file". */
191#define YY_NEW_FILE yyrestart( yyin )
192#define YY_END_OF_BUFFER_CHAR 0
193
194/* Size of default input buffer. */
195#ifndef YY_BUF_SIZE
196#ifdef __ia64__
197/* On IA-64, the buffer size is 16k, not 8k.
198 * Moreover, YY_BUF_SIZE is 2*YY_READ_BUF_SIZE in the general case.
199 * Ditto for the __ia64__ case accordingly.
200 */
201#define YY_BUF_SIZE 32768
202#else
203#define YY_BUF_SIZE 16384
204#endif /* __ia64__ */
205#endif
206
207/* The state buf must be large enough to hold one state per character in the main buffer.
208 */
209#define YY_STATE_BUF_SIZE ((YY_BUF_SIZE + 2) * sizeof(yy_state_type))
210
211#ifndef YY_TYPEDEF_YY_BUFFER_STATE
212#define YY_TYPEDEF_YY_BUFFER_STATE
213typedef struct yy_buffer_state *YY_BUFFER_STATE;
214#endif
215
216#ifndef YY_TYPEDEF_YY_SIZE_T
217#define YY_TYPEDEF_YY_SIZE_T
218typedef size_t yy_size_t;
219#endif
220
221/* %if-not-reentrant */
222extern int yyleng;
223/* %endif */
224
225/* %if-c-only */
226/* %if-not-reentrant */
227/* %endif */
228/* %endif */
229
230#define EOB_ACT_CONTINUE_SCAN 0
231#define EOB_ACT_END_OF_FILE 1
232#define EOB_ACT_LAST_MATCH 2
233
234 /* Note: We specifically omit the test for yy_rule_can_match_eol because it requires
235 * access to the local variable yy_act. Since yyless() is a macro, it would break
236 * existing scanners that call yyless() from OUTSIDE yylex.
237 * One obvious solution it to make yy_act a global. I tried that, and saw
238 * a 5% performance hit in a non-yylineno scanner, because yy_act is
239 * normally declared as a register variable-- so it is not worth it.
240 */
241 #define YY_LESS_LINENO(n) \
242 do { \
243 int yyl;\
244 for ( yyl = n; yyl < yyleng; ++yyl )\
245 if ( yytext[yyl] == '\n' )\
246 --yylineno;\
247 }while(0)
248 #define YY_LINENO_REWIND_TO(dst) \
249 do {\
250 const char *p;\
251 for ( p = yy_cp-1; p >= (dst); --p)\
252 if ( *p == '\n' )\
253 --yylineno;\
254 }while(0)
255
256/* Return all but the first "n" matched characters back to the input stream. */
257#define yyless(n) \
258 do \
259 { \
260 /* Undo effects of setting up yytext. */ \
261 int yyless_macro_arg = (n); \
262 YY_LESS_LINENO(yyless_macro_arg);\
263 *yy_cp = (yy_hold_char); \
264 YY_RESTORE_YY_MORE_OFFSET \
265 (yy_c_buf_p) = yy_cp = yy_bp + yyless_macro_arg - YY_MORE_ADJ; \
266 YY_DO_BEFORE_ACTION; /* set up yytext again */ \
267 } \
268 while ( 0 )
269#define unput(c) yyunput( c, (yytext_ptr) )
270
271#ifndef YY_STRUCT_YY_BUFFER_STATE
272#define YY_STRUCT_YY_BUFFER_STATE
273struct yy_buffer_state
274 {
275/* %if-c-only */
276/* %endif */
277
278/* %if-c++-only */
279 std::streambuf* yy_input_file;
280/* %endif */
281
282 char *yy_ch_buf; /* input buffer */
283 char *yy_buf_pos; /* current position in input buffer */
284
285 /* Size of input buffer in bytes, not including room for EOB
286 * characters.
287 */
288 int yy_buf_size;
289
290 /* Number of characters read into yy_ch_buf, not including EOB
291 * characters.
292 */
293 int yy_n_chars;
294
295 /* Whether we "own" the buffer - i.e., we know we created it,
296 * and can realloc() it to grow it, and should free() it to
297 * delete it.
298 */
299 int yy_is_our_buffer;
300
301 /* Whether this is an "interactive" input source; if so, and
302 * if we're using stdio for input, then we want to use getc()
303 * instead of fread(), to make sure we stop fetching input after
304 * each newline.
305 */
306 int yy_is_interactive;
307
308 /* Whether we're considered to be at the beginning of a line.
309 * If so, '^' rules will be active on the next match, otherwise
310 * not.
311 */
312 int yy_at_bol;
313
314 int yy_bs_lineno; /**< The line count. */
315 int yy_bs_column; /**< The column count. */
316
317 /* Whether to try to fill the input buffer when we reach the
318 * end of it.
319 */
320 int yy_fill_buffer;
321
322 int yy_buffer_status;
323
324#define YY_BUFFER_NEW 0
325#define YY_BUFFER_NORMAL 1
326 /* When an EOF's been seen but there's still some text to process
327 * then we mark the buffer as YY_EOF_PENDING, to indicate that we
328 * shouldn't try reading from the input source any more. We might
329 * still have a bunch of tokens to match, though, because of
330 * possible backing-up.
331 *
332 * When we actually see the EOF, we change the status to "new"
333 * (via yyrestart()), so that the user can continue scanning by
334 * just pointing yyin at a new input file.
335 */
336#define YY_BUFFER_EOF_PENDING 2
337
338 };
339#endif /* !YY_STRUCT_YY_BUFFER_STATE */
340
341/* %if-c-only Standard (non-C++) definition */
342/* %not-for-header */
343/* %if-not-reentrant */
344/* %endif */
345/* %ok-for-header */
346
347/* %endif */
348
349/* We provide macros for accessing buffer states in case in the
350 * future we want to put the buffer states in a more general
351 * "scanner state".
352 *
353 * Returns the top of the stack, or NULL.
354 */
355#define YY_CURRENT_BUFFER ( (yy_buffer_stack) \
356 ? (yy_buffer_stack)[(yy_buffer_stack_top)] \
357 : NULL)
358/* Same as previous macro, but useful when we know that the buffer stack is not
359 * NULL or when we need an lvalue. For internal use only.
360 */
361#define YY_CURRENT_BUFFER_LVALUE (yy_buffer_stack)[(yy_buffer_stack_top)]
362
363/* %if-c-only Standard (non-C++) definition */
364/* %if-not-reentrant */
365/* %not-for-header */
366/* %ok-for-header */
367
368/* %endif */
369/* %endif */
370
371void *yyalloc ( yy_size_t );
372void *yyrealloc ( void *, yy_size_t );
373void yyfree ( void * );
374
375#define yy_new_buffer yy_create_buffer
376#define yy_set_interactive(is_interactive) \
377 { \
378 if ( ! YY_CURRENT_BUFFER ){ \
379 yyensure_buffer_stack (); \
380 YY_CURRENT_BUFFER_LVALUE = \
381 yy_create_buffer( yyin, YY_BUF_SIZE ); \
382 } \
383 YY_CURRENT_BUFFER_LVALUE->yy_is_interactive = is_interactive; \
384 }
385#define yy_set_bol(at_bol) \
386 { \
387 if ( ! YY_CURRENT_BUFFER ){\
388 yyensure_buffer_stack (); \
389 YY_CURRENT_BUFFER_LVALUE = \
390 yy_create_buffer( yyin, YY_BUF_SIZE ); \
391 } \
392 YY_CURRENT_BUFFER_LVALUE->yy_at_bol = at_bol; \
393 }
394#define YY_AT_BOL() (YY_CURRENT_BUFFER_LVALUE->yy_at_bol)
395
396/* %% [1.0] yytext/yyin/yyout/yy_state_type/yylineno etc. def's & init go here */
397/* Begin user sect3 */
398
399#define FLEX_DEBUG
400typedef flex_uint8_t YY_CHAR;
401
402#define yytext_ptr yytext
403#define YY_INTERACTIVE
404
405#include <FlexLexer.h>
406
407/* %% [1.5] DFA */
408
409/* %if-c-only Standard (non-C++) definition */
410/* %endif */
411
412/* Done after the current pattern has been matched and before the
413 * corresponding action - sets up yytext.
414 */
415#define YY_DO_BEFORE_ACTION \
416 (yytext_ptr) = yy_bp; \
417/* %% [2.0] code to fiddle yytext and yyleng for yymore() goes here \ */\
418 (yytext_ptr) -= (yy_more_len); \
419 yyleng = (int) (yy_cp - (yytext_ptr)); \
420 (yy_hold_char) = *yy_cp; \
421 *yy_cp = '\0'; \
422/* %% [3.0] code to copy yytext_ptr to yytext[] goes here, if %array \ */\
423 (yy_c_buf_p) = yy_cp;
424/* %% [4.0] data tables for the DFA and the user's section 1 definitions go here */
425#define YY_NUM_RULES 96
426#define YY_END_OF_BUFFER 97
427/* This struct is not used in this scanner,
428 but its presence is necessary. */
429struct yy_trans_info
430 {
431 flex_int32_t yy_verify;
432 flex_int32_t yy_nxt;
433 };
434static const flex_int16_t yy_accept[383] =
435 { 0,
436 0, 0, 0, 0, 0, 0, 97, 95, 77, 78,
437 2, 85, 83, 43, 41, 42, 83, 44, 79, 79,
438 95, 95, 48, 45, 49, 83, 83, 83, 83, 83,
439 68, 8, 83, 83, 83, 83, 83, 83, 83, 83,
440 83, 83, 83, 83, 83, 83, 83, 83, 90, 89,
441 87, 87, 88, 94, 91, 91, 93, 92, 77, 83,
442 83, 79, 79, 80, 81, 80, 0, 0, 79, 84,
443 0, 1, 1, 46, 76, 47, 83, 83, 83, 83,
444 83, 83, 83, 83, 83, 9, 83, 83, 83, 83,
445 83, 83, 83, 83, 83, 83, 83, 83, 83, 83,
446
447 83, 72, 83, 83, 83, 83, 83, 83, 83, 83,
448 83, 83, 87, 86, 91, 81, 80, 83, 83, 79,
449 80, 0, 80, 0, 82, 84, 83, 83, 83, 83,
450 83, 52, 83, 71, 83, 83, 83, 83, 83, 54,
451 83, 83, 83, 83, 50, 83, 83, 83, 75, 12,
452 51, 64, 63, 74, 13, 34, 68, 83, 83, 83,
453 53, 83, 55, 83, 73, 83, 80, 83, 82, 82,
454 82, 0, 83, 83, 83, 83, 83, 57, 83, 83,
455 83, 56, 83, 58, 83, 61, 83, 83, 23, 83,
456 24, 83, 83, 83, 83, 83, 35, 83, 83, 60,
457
458 67, 62, 69, 82, 82, 83, 0, 82, 83, 83,
459 83, 83, 83, 83, 83, 83, 83, 59, 83, 83,
460 83, 83, 70, 83, 83, 83, 83, 83, 83, 83,
461 83, 83, 83, 36, 83, 83, 83, 83, 82, 3,
462 83, 83, 83, 7, 58, 14, 83, 83, 83, 10,
463 11, 83, 83, 83, 83, 83, 83, 83, 83, 83,
464 83, 83, 83, 83, 4, 83, 6, 83, 83, 83,
465 83, 83, 83, 83, 83, 83, 83, 83, 83, 83,
466 83, 83, 83, 83, 83, 83, 83, 83, 83, 83,
467 27, 83, 83, 83, 83, 83, 65, 66, 83, 38,
468
469 83, 83, 83, 15, 83, 83, 83, 83, 83, 83,
470 83, 28, 83, 30, 83, 33, 83, 39, 83, 83,
471 83, 83, 83, 83, 20, 83, 83, 83, 29, 83,
472 83, 40, 5, 83, 83, 18, 83, 83, 22, 83,
473 83, 83, 83, 83, 83, 83, 19, 83, 83, 83,
474 83, 83, 83, 83, 17, 83, 83, 83, 83, 83,
475 83, 83, 21, 25, 26, 83, 32, 83, 83, 83,
476 83, 83, 83, 37, 83, 83, 16, 83, 83, 83,
477 31, 0
478 } ;
479
480static const YY_CHAR yy_ec[256] =
481 { 0,
482 1, 1, 1, 1, 1, 1, 1, 1, 2, 3,
483 1, 1, 4, 1, 1, 1, 1, 1, 1, 1,
484 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
485 1, 2, 5, 6, 1, 7, 7, 7, 1, 1,
486 1, 8, 9, 1, 10, 11, 12, 13, 14, 15,
487 14, 14, 14, 14, 14, 14, 14, 16, 17, 18,
488 19, 20, 7, 7, 21, 22, 23, 24, 25, 26,
489 27, 28, 29, 30, 30, 31, 32, 33, 30, 34,
490 30, 35, 36, 37, 38, 30, 30, 39, 40, 30,
491 1, 41, 1, 42, 43, 1, 44, 45, 46, 47,
492
493 48, 49, 50, 51, 52, 30, 53, 54, 55, 56,
494 57, 58, 59, 60, 61, 62, 63, 64, 65, 66,
495 30, 67, 1, 68, 1, 7, 1, 1, 1, 1,
496 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
497 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
498 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
499 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
500 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
501 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
502 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
503
504 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
505 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
506 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
507 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
508 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
509 1, 1, 1, 1, 1
510 } ;
511
512static const YY_CHAR yy_meta[69] =
513 { 0,
514 1, 1, 1, 1, 2, 1, 2, 2, 2, 2,
515 3, 2, 4, 4, 4, 1, 1, 2, 2, 2,
516 5, 5, 5, 5, 5, 5, 2, 2, 2, 2,
517 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
518 1, 2, 2, 5, 5, 5, 5, 5, 5, 2,
519 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
520 2, 2, 2, 2, 2, 2, 2, 1
521 } ;
522
523static const flex_int16_t yy_base[391] =
524 { 0,
525 0, 0, 66, 70, 74, 76, 594, 595, 79, 595,
526 0, 595, 0, 0, 71, 76, 79, 0, 84, 89,
527 0, 102, 574, 572, 572, 561, 564, 563, 549, 549,
528 0, 0, 65, 50, 537, 42, 72, 536, 521, 65,
529 68, 525, 521, 84, 532, 86, 75, 522, 595, 595,
530 127, 136, 572, 595, 145, 148, 595, 595, 151, 0,
531 143, 148, 153, 156, 161, 169, 176, 566, 184, 0,
532 189, 199, 202, 0, 0, 0, 543, 552, 535, 541,
533 537, 510, 513, 522, 522, 72, 523, 518, 504, 97,
534 513, 102, 509, 502, 499, 512, 497, 508, 491, 500,
535
536 493, 0, 494, 107, 492, 491, 489, 494, 489, 492,
537 484, 486, 204, 595, 207, 205, 210, 224, 248, 216,
538 229, 232, 235, 0, 202, 0, 524, 515, 522, 517,
539 512, 0, 479, 0, 154, 483, 490, 481, 490, 484,
540 480, 481, 475, 190, 0, 470, 486, 519, 0, 0,
541 0, 476, 475, 0, 0, 0, 0, 475, 477, 514,
542 472, 460, 470, 472, 0, 242, 252, 285, 257, 154,
543 244, 266, 484, 486, 493, 481, 482, 0, 457, 461,
544 468, 0, 451, 495, 456, 0, 464, 451, 0, 444,
545 0, 457, 450, 261, 448, 447, 0, 439, 230, 0,
546
547 0, 0, 0, 254, 256, 313, 322, 325, 460, 478,
548 473, 476, 469, 434, 438, 437, 430, 0, 481, 430,
549 441, 427, 0, 433, 425, 429, 427, 425, 422, 425,
550 436, 427, 426, 467, 420, 418, 416, 328, 331, 0,
551 442, 449, 440, 0, 455, 0, 408, 420, 457, 0,
552 0, 405, 416, 417, 401, 405, 400, 406, 392, 391,
553 413, 407, 405, 392, 0, 424, 0, 408, 441, 179,
554 23, 393, 401, 396, 390, 402, 382, 396, 395, 381,
555 384, 388, 387, 406, 375, 240, 373, 378, 374, 383,
556 0, 378, 374, 381, 367, 380, 0, 0, 366, 0,
557
558 380, 368, 403, 413, 365, 358, 363, 363, 358, 355,
559 360, 0, 359, 0, 404, 0, 365, 0, 356, 380,
560 366, 353, 352, 347, 396, 343, 352, 348, 0, 133,
561 342, 0, 0, 340, 339, 0, 337, 338, 0, 340,
562 348, 334, 337, 331, 331, 329, 0, 342, 333, 332,
563 326, 326, 333, 321, 0, 337, 321, 319, 317, 331,
564 306, 266, 0, 0, 0, 265, 0, 261, 252, 245,
565 224, 227, 191, 0, 176, 170, 0, 79, 62, 35,
566 0, 595, 346, 351, 355, 359, 364, 367, 371, 373
567 } ;
568
569static const flex_int16_t yy_def[391] =
570 { 0,
571 382, 1, 383, 383, 384, 384, 382, 382, 382, 382,
572 385, 382, 385, 385, 385, 385, 385, 385, 382, 382,
573 386, 387, 385, 385, 385, 385, 385, 385, 385, 385,
574 385, 385, 385, 385, 385, 385, 385, 385, 385, 385,
575 385, 385, 385, 385, 385, 385, 385, 385, 382, 382,
576 382, 382, 382, 382, 382, 382, 382, 382, 382, 385,
577 385, 385, 385, 385, 382, 382, 382, 388, 382, 389,
578 387, 382, 387, 385, 385, 385, 385, 385, 385, 385,
579 385, 385, 385, 385, 385, 385, 385, 385, 385, 385,
580 385, 385, 385, 385, 385, 385, 385, 385, 385, 385,
581
582 385, 385, 385, 385, 385, 385, 385, 385, 385, 385,
583 385, 385, 382, 382, 382, 385, 385, 385, 385, 385,
584 382, 382, 382, 390, 388, 389, 385, 385, 385, 385,
585 385, 385, 385, 385, 385, 385, 385, 385, 385, 385,
586 385, 385, 385, 385, 385, 385, 385, 385, 385, 385,
587 385, 385, 385, 385, 385, 385, 385, 385, 385, 385,
588 385, 385, 385, 385, 385, 385, 385, 385, 119, 390,
589 390, 382, 385, 385, 385, 385, 385, 385, 385, 385,
590 385, 385, 385, 385, 385, 385, 385, 385, 385, 385,
591 385, 385, 385, 385, 385, 385, 385, 385, 385, 385,
592
593 385, 385, 385, 168, 168, 385, 382, 382, 385, 385,
594 385, 385, 385, 385, 385, 385, 385, 385, 385, 385,
595 385, 385, 385, 385, 385, 385, 385, 385, 385, 385,
596 385, 385, 385, 385, 385, 385, 385, 385, 385, 385,
597 385, 385, 385, 385, 385, 385, 385, 385, 385, 385,
598 385, 385, 385, 385, 385, 385, 385, 385, 385, 385,
599 385, 385, 385, 385, 385, 385, 385, 385, 385, 385,
600 385, 385, 385, 385, 385, 385, 385, 385, 385, 385,
601 385, 385, 385, 385, 385, 385, 385, 385, 385, 385,
602 385, 385, 385, 385, 385, 385, 385, 385, 385, 385,
603
604 385, 385, 385, 385, 385, 385, 385, 385, 385, 385,
605 385, 385, 385, 385, 385, 385, 385, 385, 385, 385,
606 385, 385, 385, 385, 385, 385, 385, 385, 385, 385,
607 385, 385, 385, 385, 385, 385, 385, 385, 385, 385,
608 385, 385, 385, 385, 385, 385, 385, 385, 385, 385,
609 385, 385, 385, 385, 385, 385, 385, 385, 385, 385,
610 385, 385, 385, 385, 385, 385, 385, 385, 385, 385,
611 385, 385, 385, 385, 385, 385, 385, 385, 385, 385,
612 385, 0, 382, 382, 382, 382, 382, 382, 382, 382
613 } ;
614
615static const flex_int16_t yy_nxt[664] =
616 { 0,
617 8, 9, 10, 9, 11, 12, 13, 14, 15, 16,
618 17, 18, 19, 20, 20, 21, 22, 23, 24, 25,
619 13, 26, 13, 27, 13, 13, 13, 28, 13, 13,
620 13, 13, 29, 13, 13, 30, 13, 13, 13, 13,
621 8, 31, 32, 33, 13, 34, 35, 36, 37, 38,
622 13, 39, 13, 40, 41, 42, 43, 44, 13, 45,
623 46, 47, 13, 13, 13, 48, 13, 49, 51, 52,
624 289, 53, 51, 52, 290, 53, 55, 56, 55, 56,
625 59, 61, 59, 62, 63, 63, 61, 91, 62, 63,
626 63, 64, 64, 64, 65, 381, 66, 66, 66, 65,
627
628 88, 69, 69, 69, 72, 73, 89, 92, 67, 82,
629 83, 99, 97, 67, 57, 93, 57, 380, 110, 100,
630 84, 98, 68, 136, 85, 86, 87, 103, 94, 113,
631 113, 67, 137, 107, 111, 379, 67, 108, 113, 113,
632 104, 58, 141, 58, 109, 142, 105, 115, 115, 68,
633 115, 115, 59, 144, 59, 64, 64, 64, 116, 145,
634 117, 117, 117, 116, 156, 120, 120, 120, 64, 64,
635 64, 157, 118, 121, 121, 121, 342, 118, 343, 65,
636 118, 66, 66, 66, 122, 122, 119, 172, 123, 123,
637 123, 72, 73, 67, 65, 118, 69, 69, 69, 179,
638
639 118, 72, 72, 118, 72, 73, 113, 113, 67, 115,
640 115, 172, 171, 119, 180, 181, 67, 64, 64, 64,
641 116, 378, 117, 117, 117, 377, 116, 287, 120, 120,
642 120, 67, 166, 166, 118, 172, 167, 167, 167, 288,
643 118, 121, 121, 121, 123, 123, 123, 123, 123, 123,
644 190, 191, 376, 67, 167, 167, 167, 118, 168, 172,
645 169, 169, 169, 118, 167, 167, 167, 205, 169, 169,
646 169, 169, 169, 169, 207, 207, 67, 172, 208, 208,
647 208, 235, 375, 236, 374, 305, 237, 206, 306, 206,
648 206, 169, 169, 169, 169, 169, 169, 204, 204, 204,
649
650 307, 172, 373, 372, 225, 204, 204, 204, 204, 204,
651 204, 206, 226, 206, 206, 227, 371, 228, 229, 370,
652 369, 238, 238, 230, 231, 239, 239, 239, 204, 204,
653 204, 204, 204, 204, 208, 208, 208, 208, 208, 208,
654 239, 239, 239, 239, 239, 239, 50, 50, 50, 50,
655 50, 54, 54, 54, 54, 54, 60, 60, 60, 60,
656 70, 70, 368, 70, 71, 71, 71, 71, 71, 125,
657 125, 125, 126, 126, 126, 126, 170, 170, 367, 366,
658 365, 364, 363, 362, 361, 360, 359, 358, 357, 356,
659 355, 354, 353, 352, 351, 350, 349, 348, 347, 346,
660
661 345, 344, 341, 340, 339, 338, 337, 336, 335, 334,
662 333, 332, 331, 330, 329, 328, 327, 326, 325, 324,
663 323, 322, 321, 320, 319, 318, 317, 316, 315, 314,
664 313, 312, 311, 310, 309, 308, 304, 303, 302, 301,
665 300, 299, 298, 297, 296, 295, 294, 293, 292, 291,
666 286, 285, 284, 283, 282, 281, 280, 279, 278, 277,
667 276, 275, 274, 273, 272, 271, 270, 269, 268, 218,
668 267, 266, 265, 264, 263, 262, 261, 260, 259, 258,
669 257, 256, 255, 254, 253, 252, 251, 250, 249, 248,
670 247, 246, 245, 182, 178, 244, 243, 242, 241, 240,
671
672 234, 233, 232, 224, 223, 222, 221, 220, 219, 218,
673 217, 216, 215, 214, 213, 212, 211, 210, 209, 203,
674 202, 201, 200, 199, 198, 197, 196, 195, 194, 193,
675 192, 189, 188, 187, 186, 185, 184, 183, 182, 178,
676 177, 176, 175, 174, 173, 165, 164, 163, 162, 161,
677 160, 159, 158, 155, 154, 153, 152, 151, 150, 149,
678 148, 147, 146, 143, 140, 139, 138, 135, 134, 133,
679 132, 131, 130, 129, 128, 127, 124, 114, 112, 106,
680 102, 101, 96, 95, 90, 81, 80, 79, 78, 77,
681 76, 75, 74, 382, 7, 382, 382, 382, 382, 382,
682
683 382, 382, 382, 382, 382, 382, 382, 382, 382, 382,
684 382, 382, 382, 382, 382, 382, 382, 382, 382, 382,
685 382, 382, 382, 382, 382, 382, 382, 382, 382, 382,
686 382, 382, 382, 382, 382, 382, 382, 382, 382, 382,
687 382, 382, 382, 382, 382, 382, 382, 382, 382, 382,
688 382, 382, 382, 382, 382, 382, 382, 382, 382, 382,
689 382, 382, 382
690 } ;
691
692static const flex_int16_t yy_chk[664] =
693 { 0,
694 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
695 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
696 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
697 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
698 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
699 1, 1, 1, 1, 1, 1, 1, 1, 1, 1,
700 1, 1, 1, 1, 1, 1, 1, 1, 3, 3,
701 271, 3, 4, 4, 271, 4, 5, 5, 6, 6,
702 9, 15, 9, 15, 15, 15, 16, 36, 16, 16,
703 16, 17, 17, 17, 19, 380, 19, 19, 19, 20,
704
705 34, 20, 20, 20, 22, 22, 34, 36, 19, 33,
706 33, 41, 40, 20, 5, 37, 6, 379, 47, 41,
707 33, 40, 19, 86, 33, 33, 33, 44, 37, 51,
708 51, 19, 86, 46, 47, 378, 20, 46, 52, 52,
709 44, 5, 90, 6, 46, 90, 44, 55, 55, 19,
710 56, 56, 59, 92, 59, 61, 61, 61, 62, 92,
711 62, 62, 62, 63, 104, 63, 63, 63, 64, 64,
712 64, 104, 62, 65, 65, 65, 330, 63, 330, 66,
713 64, 66, 66, 66, 67, 67, 62, 170, 67, 67,
714 67, 71, 71, 66, 69, 62, 69, 69, 69, 135,
715
716 63, 72, 72, 64, 73, 73, 113, 113, 69, 115,
717 115, 170, 125, 62, 135, 135, 66, 116, 116, 116,
718 117, 376, 117, 117, 117, 375, 120, 270, 120, 120,
719 120, 69, 118, 118, 117, 125, 118, 118, 118, 270,
720 120, 121, 121, 121, 122, 122, 122, 123, 123, 123,
721 144, 144, 373, 121, 166, 166, 166, 117, 119, 125,
722 119, 119, 119, 120, 167, 167, 167, 169, 119, 119,
723 119, 119, 119, 119, 172, 172, 121, 171, 172, 172,
724 172, 199, 372, 199, 371, 286, 199, 204, 286, 205,
725 169, 119, 119, 119, 119, 119, 119, 168, 168, 168,
726
727 286, 171, 370, 369, 194, 168, 168, 168, 168, 168,
728 168, 204, 194, 205, 169, 194, 368, 194, 194, 366,
729 362, 206, 206, 194, 194, 206, 206, 206, 168, 168,
730 168, 168, 168, 168, 207, 207, 207, 208, 208, 208,
731 238, 238, 238, 239, 239, 239, 383, 383, 383, 383,
732 383, 384, 384, 384, 384, 384, 385, 385, 385, 385,
733 386, 386, 361, 386, 387, 387, 387, 387, 387, 388,
734 388, 388, 389, 389, 389, 389, 390, 390, 360, 359,
735 358, 357, 356, 354, 353, 352, 351, 350, 349, 348,
736 346, 345, 344, 343, 342, 341, 340, 338, 337, 335,
737
738 334, 331, 328, 327, 326, 325, 324, 323, 322, 321,
739 320, 319, 317, 315, 313, 311, 310, 309, 308, 307,
740 306, 305, 304, 303, 302, 301, 299, 296, 295, 294,
741 293, 292, 290, 289, 288, 287, 285, 284, 283, 282,
742 281, 280, 279, 278, 277, 276, 275, 274, 273, 272,
743 269, 268, 266, 264, 263, 262, 261, 260, 259, 258,
744 257, 256, 255, 254, 253, 252, 249, 248, 247, 245,
745 243, 242, 241, 237, 236, 235, 234, 233, 232, 231,
746 230, 229, 228, 227, 226, 225, 224, 222, 221, 220,
747 219, 217, 216, 215, 214, 213, 212, 211, 210, 209,
748
749 198, 196, 195, 193, 192, 190, 188, 187, 185, 184,
750 183, 181, 180, 179, 177, 176, 175, 174, 173, 164,
751 163, 162, 161, 160, 159, 158, 153, 152, 148, 147,
752 146, 143, 142, 141, 140, 139, 138, 137, 136, 133,
753 131, 130, 129, 128, 127, 112, 111, 110, 109, 108,
754 107, 106, 105, 103, 101, 100, 99, 98, 97, 96,
755 95, 94, 93, 91, 89, 88, 87, 85, 84, 83,
756 82, 81, 80, 79, 78, 77, 68, 53, 48, 45,
757 43, 42, 39, 38, 35, 30, 29, 28, 27, 26,
758 25, 24, 23, 7, 382, 382, 382, 382, 382, 382,
759
760 382, 382, 382, 382, 382, 382, 382, 382, 382, 382,
761 382, 382, 382, 382, 382, 382, 382, 382, 382, 382,
762 382, 382, 382, 382, 382, 382, 382, 382, 382, 382,
763 382, 382, 382, 382, 382, 382, 382, 382, 382, 382,
764 382, 382, 382, 382, 382, 382, 382, 382, 382, 382,
765 382, 382, 382, 382, 382, 382, 382, 382, 382, 382,
766 382, 382, 382
767 } ;
768
769/* Table of booleans, true if rule could match eol. */
770static const flex_int32_t yy_rule_can_match_eol[97] =
771 { 0,
7721, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
773 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
774 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
775 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0,
776 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 1, 0, 0, 0, 0, 0, };
777
778static const flex_int16_t yy_rule_linenum[96] =
779 { 0,
780 91, 95, 96, 97, 98, 99, 100, 101, 102, 103,
781 104, 105, 106, 108, 109, 110, 111, 112, 113, 114,
782 115, 116, 117, 118, 119, 120, 121, 122, 123, 124,
783 125, 126, 127, 128, 129, 130, 131, 132, 133, 134,
784 136, 137, 138, 139, 140, 141, 142, 143, 144, 145,
785 146, 147, 148, 149, 150, 151, 152, 153, 154, 155,
786 156, 157, 158, 159, 160, 161, 162, 163, 165, 166,
787 167, 168, 169, 170, 171, 172, 175, 180, 184, 198,
788 203, 208, 213, 218, 223, 224, 225, 226, 231, 233,
789 234, 235, 240, 241, 244
790
791 } ;
792
793/* The intent behind this definition is that it'll catch
794 * any uses of REJECT which flex missed.
795 */
796#define REJECT reject_used_but_not_detected
797#define yymore() ((yy_more_flag) = 1)
798#define YY_MORE_ADJ (yy_more_len)
799#define YY_RESTORE_YY_MORE_OFFSET
800#line 1 "dreal/smt2/scanner.ll"
801#line 2 "dreal/smt2/scanner.ll"
802
803#ifdef __clang__
804#pragma clang diagnostic push
805#pragma clang diagnostic ignored "-Wdeprecated-register"
806#pragma clang diagnostic ignored "-Wnull-conversion"
807#pragma clang diagnostic ignored "-Wunneeded-internal-declaration"
808#endif
809
810/* ignore harmless bug in old versions of flex */
811#pragma GCC diagnostic push
812#pragma GCC diagnostic ignored "-Wsign-compare"
813#pragma GCC diagnostic ignored "-Wold-style-cast"
814
815#include <string>
816
817#include "dreal/smt2/scanner.h"
818
819/* import the parser's token type into a local typedef */
820typedef dreal::Smt2Parser::token token;
821typedef dreal::Smt2Parser::token_type token_type;
822
823/* By default yylex returns int, we use token_type. Unfortunately yyterminate
824 * by default returns 0, which is not of token_type. */
825#define yyterminate() return token::END
826
827/* This disables inclusion of unistd.h, which is not available under Visual C++
828 * on Win32. The C++ scanner uses STL streams instead. */
829#define YY_NO_UNISTD_H
830
831#line 831 "bazel-out/k8-opt/bin/dreal/smt2/scanner.ll.cc"
832/*** Flex Declarations and Options ***/
833/* enable c++ scanner class generation */
834/* change the name of the scanner class. results in "Smt2FlexLexer" */
835/* enable scanner to generate debug output. disable this for release
836 * versions. */
837/* no support for include files is planned */
838/* enables the use of start condition stacks */
839/* The following paragraph suffices to track locations accurately. Each time
840 * yylex is invoked, the begin position is moved onto the end position. */
841#line 56 "dreal/smt2/scanner.ll"
842/* handle locations */
843int smt2_yycolumn = 1;
844
845#define YY_USER_ACTION yylloc->begin.line = yylloc->end.line = yylineno; \
846yylloc->begin.column = smt2_yycolumn; yylloc->end.column = smt2_yycolumn+yyleng-1; \
847smt2_yycolumn += yyleng;
848#line 848 "bazel-out/k8-opt/bin/dreal/smt2/scanner.ll.cc"
849
850#line 850 "bazel-out/k8-opt/bin/dreal/smt2/scanner.ll.cc"
851
852#define INITIAL 0
853#define str 1
854#define quoted 2
855
856#ifndef YY_NO_UNISTD_H
857/* Special case for "unistd.h", since it is non-ANSI. We include it way
858 * down here because we want the user's section 1 to have been scanned first.
859 * The user has a chance to override it with an option.
860 */
861/* %if-c-only */
862/* %endif */
863/* %if-c++-only */
864#include <unistd.h>
865/* %endif */
866#endif
867
868#ifndef YY_EXTRA_TYPE
869#define YY_EXTRA_TYPE void *
870#endif
871
872/* %if-c-only Reentrant structure and macros (non-C++). */
873/* %if-reentrant */
874/* %if-c-only */
875/* %endif */
876/* %if-reentrant */
877/* %endif */
878/* %endif End reentrant structures and macros. */
879/* %if-bison-bridge */
880/* %endif */
881/* %not-for-header */
882/* %ok-for-header */
883
884/* %endif */
885
886#ifndef yytext_ptr
887static void yy_flex_strncpy ( char *, const char *, int );
888#endif
889
890#ifdef YY_NEED_STRLEN
891static int yy_flex_strlen ( const char * );
892#endif
893
894#ifndef YY_NO_INPUT
895/* %if-c-only Standard (non-C++) definition */
896/* %not-for-header */
897/* %ok-for-header */
898
899/* %endif */
900#endif
901
902/* %if-c-only */
903/* %endif */
904
905/* Amount of stuff to slurp up with each read. */
906#ifndef YY_READ_BUF_SIZE
907#ifdef __ia64__
908/* On IA-64, the buffer size is 16k, not 8k */
909#define YY_READ_BUF_SIZE 16384
910#else
911#define YY_READ_BUF_SIZE 8192
912#endif /* __ia64__ */
913#endif
914
915/* Copy whatever the last rule matched to the standard output. */
916#ifndef ECHO
917/* %if-c-only Standard (non-C++) definition */
918/* %endif */
919/* %if-c++-only C++ definition */
920#define ECHO LexerOutput( yytext, yyleng )
921/* %endif */
922#endif
923
924/* Gets input and stuffs it into "buf". number of characters read, or YY_NULL,
925 * is returned in "result".
926 */
927#ifndef YY_INPUT
928#define YY_INPUT(buf,result,max_size) \
929/* %% [5.0] fread()/read() definition of YY_INPUT goes here unless we're doing C++ \ */\
930\
931/* %if-c++-only C++ definition \ */\
932 if ( (int)(result = LexerInput( (char *) buf, max_size )) < 0 ) \
933 YY_FATAL_ERROR( "input in flex scanner failed" );
934/* %endif */
935
936#endif
937
938/* No semi-colon after return; correct usage is to write "yyterminate();" -
939 * we don't want an extra ';' after the "return" because that will cause
940 * some compilers to complain about unreachable statements.
941 */
942#ifndef yyterminate
943#define yyterminate() return YY_NULL
944#endif
945
946/* Number of entries by which start-condition stack grows. */
947#ifndef YY_START_STACK_INCR
948#define YY_START_STACK_INCR 25
949#endif
950
951/* Report a fatal error. */
952#ifndef YY_FATAL_ERROR
953/* %if-c-only */
954/* %endif */
955/* %if-c++-only */
956#define YY_FATAL_ERROR(msg) LexerError( msg )
957/* %endif */
958#endif
959
960/* %if-tables-serialization structures and prototypes */
961/* %not-for-header */
962/* %ok-for-header */
963
964/* %not-for-header */
965/* %tables-yydmap generated elements */
966/* %endif */
967/* end tables serialization structures and prototypes */
968
969/* %ok-for-header */
970
971/* Default declaration of generated scanner - a define so the user can
972 * easily add parameters.
973 */
974#ifndef YY_DECL
975#define YY_DECL_IS_OURS 1
976/* %if-c-only Standard (non-C++) definition */
977/* %endif */
978/* %if-c++-only C++ definition */
979#define YY_DECL int yyFlexLexer::yylex()
980/* %endif */
981#endif /* !YY_DECL */
982
983/* Code executed at the beginning of each rule, after yytext and yyleng
984 * have been set up.
985 */
986#ifndef YY_USER_ACTION
987#define YY_USER_ACTION
988#endif
989
990/* Code executed at the end of each rule. */
991#ifndef YY_BREAK
992#define YY_BREAK /*LINTED*/break;
993#endif
994
995/* %% [6.0] YY_RULE_SETUP definition goes here */
996#define YY_RULE_SETUP \
997 YY_USER_ACTION
998
999/* %not-for-header */
1000/** The main scanner function which does all the work.
1001 */
1002YY_DECL
1003{
1004 yy_state_type yy_current_state;
1005 char *yy_cp, *yy_bp;
1006 int yy_act;
1007
1008 if ( !(yy_init) )
1009 {
1010 (yy_init) = 1;
1011
1012#ifdef YY_USER_INIT
1013 YY_USER_INIT;
1014#endif
1015
1016 if ( ! (yy_start) )
1017 (yy_start) = 1; /* first start state */
1018
1019 if ( ! yyin )
1020/* %if-c-only */
1021/* %endif */
1022/* %if-c++-only */
1023 yyin.rdbuf(std::cin.rdbuf());
1024/* %endif */
1025
1026 if ( ! yyout )
1027/* %if-c-only */
1028/* %endif */
1029/* %if-c++-only */
1030 yyout.rdbuf(std::cout.rdbuf());
1031/* %endif */
1032
1033 if ( ! YY_CURRENT_BUFFER ) {
1034 yyensure_buffer_stack ();
1035 YY_CURRENT_BUFFER_LVALUE =
1036 yy_create_buffer( yyin, YY_BUF_SIZE );
1037 }
1038
1039 yy_load_buffer_state( );
1040 }
1041
1042 {
1043/* %% [7.0] user's declarations go here */
1044#line 81 "dreal/smt2/scanner.ll"
1045
1046
1047
1048#line 85 "dreal/smt2/scanner.ll"
1049 // reset location
1050 yylloc->step();
1051
1052
1053 /*** BEGIN - lexer rules ***/
1054
1055#line 1055 "bazel-out/k8-opt/bin/dreal/smt2/scanner.ll.cc"
1056
1057 while ( /*CONSTCOND*/1 ) /* loops until end-of-file is reached */
1058 {
1059/* %% [8.0] yymore()-related code goes here */
1060 (yy_more_len) = 0;
1061 if ( (yy_more_flag) )
1062 {
1063 (yy_more_len) = (int) ((yy_c_buf_p) - (yytext_ptr));
1064 (yy_more_flag) = 0;
1065 }
1066 yy_cp = (yy_c_buf_p);
1067
1068 /* Support of yytext. */
1069 *yy_cp = (yy_hold_char);
1070
1071 /* yy_bp points to the position in yy_ch_buf of the start of
1072 * the current run.
1073 */
1074 yy_bp = yy_cp;
1075
1076/* %% [9.0] code to set up and find next match goes here */
1077 yy_current_state = (yy_start);
1078yy_match:
1079 do
1080 {
1081 YY_CHAR yy_c = yy_ec[YY_SC_TO_UI(*yy_cp)] ;
1082 if ( yy_accept[yy_current_state] )
1083 {
1084 (yy_last_accepting_state) = yy_current_state;
1085 (yy_last_accepting_cpos) = yy_cp;
1086 }
1087 while ( yy_chk[yy_base[yy_current_state] + yy_c] != yy_current_state )
1088 {
1089 yy_current_state = (int) yy_def[yy_current_state];
1090 if ( yy_current_state >= 383 )
1091 yy_c = yy_meta[yy_c];
1092 }
1093 yy_current_state = yy_nxt[yy_base[yy_current_state] + yy_c];
1094 ++yy_cp;
1095 }
1096 while ( yy_base[yy_current_state] != 595 );
1097
1098yy_find_action:
1099/* %% [10.0] code to find the action number goes here */
1100 yy_act = yy_accept[yy_current_state];
1101 if ( yy_act == 0 )
1102 { /* have to back up */
1103 yy_cp = (yy_last_accepting_cpos);
1104 yy_current_state = (yy_last_accepting_state);
1105 yy_act = yy_accept[yy_current_state];
1106 }
1107
1108 YY_DO_BEFORE_ACTION;
1109
1110/* %% [11.0] code for yylineno update goes here */
1111
1112 if ( yy_act != YY_END_OF_BUFFER && yy_rule_can_match_eol[yy_act] )
1113 {
1114 int yyl;
1115 for ( yyl = (yy_more_len); yyl < yyleng; ++yyl )
1116 if ( yytext[yyl] == '\n' )
1117
1118 yylineno++;
1119;
1120 }
1121
1122do_action: /* This label is used only to access EOF actions. */
1123
1124/* %% [12.0] debug code goes here */
1125 if ( yy_flex_debug )
1126 {
1127 if ( yy_act == 0 )
1128 std::cerr << "--scanner backing up\n";
1129 else if ( yy_act < 96 )
1130 std::cerr << "--accepting rule at line " << yy_rule_linenum[yy_act] <<
1131 "(\"" << yytext << "\")\n";
1132 else if ( yy_act == 96 )
1133 std::cerr << "--accepting default rule (\"" << yytext << "\")\n";
1134 else if ( yy_act == 97 )
1135 std::cerr << "--(end of buffer or a NUL)\n";
1136 else
1137 std::cerr << "--EOF (start condition " << YY_START << ")\n";
1138 }
1139
1140 switch ( yy_act )
1141 { /* beginning of action switch */
1142/* %% [13.0] actions go here */
1143 case 0: /* must back up */
1144 /* undo the effects of YY_DO_BEFORE_ACTION */
1145 *yy_cp = (yy_hold_char);
1146 yy_cp = (yy_last_accepting_cpos);
1147 yy_current_state = (yy_last_accepting_state);
1148 goto yy_find_action;
1149
1150case 1:
1151/* rule 1 can match eol */
1152YY_RULE_SETUP
1153#line 91 "dreal/smt2/scanner.ll"
1154{
1155 smt2_yycolumn=1;
1156}
1157 YY_BREAK
1158case 2:
1159YY_RULE_SETUP
1160#line 95 "dreal/smt2/scanner.ll"
1161{ return Smt2Parser::token::TK_EXCLAMATION; }
1162 YY_BREAK
1163case 3:
1164YY_RULE_SETUP
1165#line 96 "dreal/smt2/scanner.ll"
1166{ return Smt2Parser::token::TK_BINARY; }
1167 YY_BREAK
1168case 4:
1169YY_RULE_SETUP
1170#line 97 "dreal/smt2/scanner.ll"
1171{ return Smt2Parser::token::TK_DECIMAL; }
1172 YY_BREAK
1173case 5:
1174YY_RULE_SETUP
1175#line 98 "dreal/smt2/scanner.ll"
1176{ return Smt2Parser::token::TK_HEXADECIMAL; }
1177 YY_BREAK
1178case 6:
1179YY_RULE_SETUP
1180#line 99 "dreal/smt2/scanner.ll"
1181{ return Smt2Parser::token::TK_NUMERAL; }
1182 YY_BREAK
1183case 7:
1184YY_RULE_SETUP
1185#line 100 "dreal/smt2/scanner.ll"
1186{ return Smt2Parser::token::TK_STRING; }
1187 YY_BREAK
1188case 8:
1189YY_RULE_SETUP
1190#line 101 "dreal/smt2/scanner.ll"
1191{ return Smt2Parser::token::TK_UNDERSCORE; }
1192 YY_BREAK
1193case 9:
1194YY_RULE_SETUP
1195#line 102 "dreal/smt2/scanner.ll"
1196{ return Smt2Parser::token::TK_AS; }
1197 YY_BREAK
1198case 10:
1199YY_RULE_SETUP
1200#line 103 "dreal/smt2/scanner.ll"
1201{ return Smt2Parser::token::TK_EXISTS; }
1202 YY_BREAK
1203case 11:
1204YY_RULE_SETUP
1205#line 104 "dreal/smt2/scanner.ll"
1206{ return Smt2Parser::token::TK_FORALL; }
1207 YY_BREAK
1208case 12:
1209YY_RULE_SETUP
1210#line 105 "dreal/smt2/scanner.ll"
1211{ return Smt2Parser::token::TK_LET; }
1212 YY_BREAK
1213case 13:
1214YY_RULE_SETUP
1215#line 106 "dreal/smt2/scanner.ll"
1216{ return Smt2Parser::token::TK_PAR; }
1217 YY_BREAK
1218case 14:
1219YY_RULE_SETUP
1220#line 108 "dreal/smt2/scanner.ll"
1221{ return Smt2Parser::token::TK_ASSERT; }
1222 YY_BREAK
1223case 15:
1224YY_RULE_SETUP
1225#line 109 "dreal/smt2/scanner.ll"
1226{ return Smt2Parser::token::TK_CHECK_SAT; }
1227 YY_BREAK
1228case 16:
1229YY_RULE_SETUP
1230#line 110 "dreal/smt2/scanner.ll"
1231{ return Smt2Parser::token::TK_CHECK_SAT_ASSUMING; }
1232 YY_BREAK
1233case 17:
1234YY_RULE_SETUP
1235#line 111 "dreal/smt2/scanner.ll"
1236{ return Smt2Parser::token::TK_DECLARE_CONST; }
1237 YY_BREAK
1238case 18:
1239YY_RULE_SETUP
1240#line 112 "dreal/smt2/scanner.ll"
1241{ return Smt2Parser::token::TK_DECLARE_FUN; }
1242 YY_BREAK
1243case 19:
1244YY_RULE_SETUP
1245#line 113 "dreal/smt2/scanner.ll"
1246{ return Smt2Parser::token::TK_DECLARE_SORT; }
1247 YY_BREAK
1248case 20:
1249YY_RULE_SETUP
1250#line 114 "dreal/smt2/scanner.ll"
1251{ return Smt2Parser::token::TK_DEFINE_FUN; }
1252 YY_BREAK
1253case 21:
1254YY_RULE_SETUP
1255#line 115 "dreal/smt2/scanner.ll"
1256{ return Smt2Parser::token::TK_DEFINE_FUN_REC; }
1257 YY_BREAK
1258case 22:
1259YY_RULE_SETUP
1260#line 116 "dreal/smt2/scanner.ll"
1261{ return Smt2Parser::token::TK_DEFINE_SORT; }
1262 YY_BREAK
1263case 23:
1264YY_RULE_SETUP
1265#line 117 "dreal/smt2/scanner.ll"
1266{ return Smt2Parser::token::TK_ECHO; }
1267 YY_BREAK
1268case 24:
1269YY_RULE_SETUP
1270#line 118 "dreal/smt2/scanner.ll"
1271{ return Smt2Parser::token::TK_EXIT; }
1272 YY_BREAK
1273case 25:
1274YY_RULE_SETUP
1275#line 119 "dreal/smt2/scanner.ll"
1276{ return Smt2Parser::token::TK_GET_ASSERTIONS; }
1277 YY_BREAK
1278case 26:
1279YY_RULE_SETUP
1280#line 120 "dreal/smt2/scanner.ll"
1281{ return Smt2Parser::token::TK_GET_ASSIGNMENT; }
1282 YY_BREAK
1283case 27:
1284YY_RULE_SETUP
1285#line 121 "dreal/smt2/scanner.ll"
1286{ return Smt2Parser::token::TK_GET_INFO; }
1287 YY_BREAK
1288case 28:
1289YY_RULE_SETUP
1290#line 122 "dreal/smt2/scanner.ll"
1291{ return Smt2Parser::token::TK_GET_MODEL; }
1292 YY_BREAK
1293case 29:
1294YY_RULE_SETUP
1295#line 123 "dreal/smt2/scanner.ll"
1296{ return Smt2Parser::token::TK_GET_OPTION; }
1297 YY_BREAK
1298case 30:
1299YY_RULE_SETUP
1300#line 124 "dreal/smt2/scanner.ll"
1301{ return Smt2Parser::token::TK_GET_PROOF; }
1302 YY_BREAK
1303case 31:
1304YY_RULE_SETUP
1305#line 125 "dreal/smt2/scanner.ll"
1306{ return Smt2Parser::token::TK_GET_UNSAT_ASSUMPTIONS; }
1307 YY_BREAK
1308case 32:
1309YY_RULE_SETUP
1310#line 126 "dreal/smt2/scanner.ll"
1311{ return Smt2Parser::token::TK_GET_UNSAT_CORE; }
1312 YY_BREAK
1313case 33:
1314YY_RULE_SETUP
1315#line 127 "dreal/smt2/scanner.ll"
1316{ return Smt2Parser::token::TK_GET_VALUE; }
1317 YY_BREAK
1318case 34:
1319YY_RULE_SETUP
1320#line 128 "dreal/smt2/scanner.ll"
1321{ return Smt2Parser::token::TK_POP; }
1322 YY_BREAK
1323case 35:
1324YY_RULE_SETUP
1325#line 129 "dreal/smt2/scanner.ll"
1326{ return Smt2Parser::token::TK_PUSH; }
1327 YY_BREAK
1328case 36:
1329YY_RULE_SETUP
1330#line 130 "dreal/smt2/scanner.ll"
1331{ return Smt2Parser::token::TK_RESET; }
1332 YY_BREAK
1333case 37:
1334YY_RULE_SETUP
1335#line 131 "dreal/smt2/scanner.ll"
1336{ return Smt2Parser::token::TK_RESET_ASSERTIONS; }
1337 YY_BREAK
1338case 38:
1339YY_RULE_SETUP
1340#line 132 "dreal/smt2/scanner.ll"
1341{ return Smt2Parser::token::TK_SET_INFO; }
1342 YY_BREAK
1343case 39:
1344YY_RULE_SETUP
1345#line 133 "dreal/smt2/scanner.ll"
1346{ return Smt2Parser::token::TK_SET_LOGIC; }
1347 YY_BREAK
1348case 40:
1349YY_RULE_SETUP
1350#line 134 "dreal/smt2/scanner.ll"
1351{ return Smt2Parser::token::TK_SET_OPTION; }
1352 YY_BREAK
1353case 41:
1354YY_RULE_SETUP
1355#line 136 "dreal/smt2/scanner.ll"
1356{ return Smt2Parser::token::TK_PLUS; }
1357 YY_BREAK
1358case 42:
1359YY_RULE_SETUP
1360#line 137 "dreal/smt2/scanner.ll"
1361{ return Smt2Parser::token::TK_MINUS; }
1362 YY_BREAK
1363case 43:
1364YY_RULE_SETUP
1365#line 138 "dreal/smt2/scanner.ll"
1366{ return Smt2Parser::token::TK_TIMES; }
1367 YY_BREAK
1368case 44:
1369YY_RULE_SETUP
1370#line 139 "dreal/smt2/scanner.ll"
1371{ return Smt2Parser::token::TK_DIV; }
1372 YY_BREAK
1373case 45:
1374YY_RULE_SETUP
1375#line 140 "dreal/smt2/scanner.ll"
1376{ return Smt2Parser::token::TK_EQ; }
1377 YY_BREAK
1378case 46:
1379YY_RULE_SETUP
1380#line 141 "dreal/smt2/scanner.ll"
1381{ return Smt2Parser::token::TK_LTE; }
1382 YY_BREAK
1383case 47:
1384YY_RULE_SETUP
1385#line 142 "dreal/smt2/scanner.ll"
1386{ return Smt2Parser::token::TK_GTE; }
1387 YY_BREAK
1388case 48:
1389YY_RULE_SETUP
1390#line 143 "dreal/smt2/scanner.ll"
1391{ return Smt2Parser::token::TK_LT; }
1392 YY_BREAK
1393case 49:
1394YY_RULE_SETUP
1395#line 144 "dreal/smt2/scanner.ll"
1396{ return Smt2Parser::token::TK_GT; }
1397 YY_BREAK
1398case 50:
1399YY_RULE_SETUP
1400#line 145 "dreal/smt2/scanner.ll"
1401{ return Smt2Parser::token::TK_EXP; }
1402 YY_BREAK
1403case 51:
1404YY_RULE_SETUP
1405#line 146 "dreal/smt2/scanner.ll"
1406{ return Smt2Parser::token::TK_LOG; }
1407 YY_BREAK
1408case 52:
1409YY_RULE_SETUP
1410#line 147 "dreal/smt2/scanner.ll"
1411{ return Smt2Parser::token::TK_ABS; }
1412 YY_BREAK
1413case 53:
1414YY_RULE_SETUP
1415#line 148 "dreal/smt2/scanner.ll"
1416{ return Smt2Parser::token::TK_SIN; }
1417 YY_BREAK
1418case 54:
1419YY_RULE_SETUP
1420#line 149 "dreal/smt2/scanner.ll"
1421{ return Smt2Parser::token::TK_COS; }
1422 YY_BREAK
1423case 55:
1424YY_RULE_SETUP
1425#line 150 "dreal/smt2/scanner.ll"
1426{ return Smt2Parser::token::TK_TAN; }
1427 YY_BREAK
1428case 56:
1429YY_RULE_SETUP
1430#line 151 "dreal/smt2/scanner.ll"
1431{ return Smt2Parser::token::TK_ASIN; }
1432 YY_BREAK
1433case 57:
1434YY_RULE_SETUP
1435#line 152 "dreal/smt2/scanner.ll"
1436{ return Smt2Parser::token::TK_ACOS; }
1437 YY_BREAK
1438case 58:
1439YY_RULE_SETUP
1440#line 153 "dreal/smt2/scanner.ll"
1441{ return Smt2Parser::token::TK_ATAN; }
1442 YY_BREAK
1443case 59:
1444YY_RULE_SETUP
1445#line 154 "dreal/smt2/scanner.ll"
1446{ return Smt2Parser::token::TK_ATAN2; }
1447 YY_BREAK
1448case 60:
1449YY_RULE_SETUP
1450#line 155 "dreal/smt2/scanner.ll"
1451{ return Smt2Parser::token::TK_SINH; }
1452 YY_BREAK
1453case 61:
1454YY_RULE_SETUP
1455#line 156 "dreal/smt2/scanner.ll"
1456{ return Smt2Parser::token::TK_COSH; }
1457 YY_BREAK
1458case 62:
1459YY_RULE_SETUP
1460#line 157 "dreal/smt2/scanner.ll"
1461{ return Smt2Parser::token::TK_TANH; }
1462 YY_BREAK
1463case 63:
1464YY_RULE_SETUP
1465#line 158 "dreal/smt2/scanner.ll"
1466{ return Smt2Parser::token::TK_MIN; }
1467 YY_BREAK
1468case 64:
1469YY_RULE_SETUP
1470#line 159 "dreal/smt2/scanner.ll"
1471{ return Smt2Parser::token::TK_MAX; }
1472 YY_BREAK
1473case 65:
1474YY_RULE_SETUP
1475#line 160 "dreal/smt2/scanner.ll"
1476{ return Smt2Parser::token::TK_MAXIMIZE; }
1477 YY_BREAK
1478case 66:
1479YY_RULE_SETUP
1480#line 161 "dreal/smt2/scanner.ll"
1481{ return Smt2Parser::token::TK_MINIMIZE; }
1482 YY_BREAK
1483case 67:
1484YY_RULE_SETUP
1485#line 162 "dreal/smt2/scanner.ll"
1486{ return Smt2Parser::token::TK_SQRT; }
1487 YY_BREAK
1488case 68:
1489YY_RULE_SETUP
1490#line 163 "dreal/smt2/scanner.ll"
1491{ return Smt2Parser::token::TK_POW; }
1492 YY_BREAK
1493case 69:
1494YY_RULE_SETUP
1495#line 165 "dreal/smt2/scanner.ll"
1496{ return Smt2Parser::token::TK_TRUE; }
1497 YY_BREAK
1498case 70:
1499YY_RULE_SETUP
1500#line 166 "dreal/smt2/scanner.ll"
1501{ return Smt2Parser::token::TK_FALSE; }
1502 YY_BREAK
1503case 71:
1504YY_RULE_SETUP
1505#line 167 "dreal/smt2/scanner.ll"
1506{ return Smt2Parser::token::TK_AND; }
1507 YY_BREAK
1508case 72:
1509YY_RULE_SETUP
1510#line 168 "dreal/smt2/scanner.ll"
1511{ return Smt2Parser::token::TK_OR; }
1512 YY_BREAK
1513case 73:
1514YY_RULE_SETUP
1515#line 169 "dreal/smt2/scanner.ll"
1516{ return Smt2Parser::token::TK_XOR; }
1517 YY_BREAK
1518case 74:
1519YY_RULE_SETUP
1520#line 170 "dreal/smt2/scanner.ll"
1521{ return Smt2Parser::token::TK_NOT; }
1522 YY_BREAK
1523case 75:
1524YY_RULE_SETUP
1525#line 171 "dreal/smt2/scanner.ll"
1526{ return Smt2Parser::token::TK_ITE; }
1527 YY_BREAK
1528case 76:
1529YY_RULE_SETUP
1530#line 172 "dreal/smt2/scanner.ll"
1531{ return Smt2Parser::token::TK_IMPLIES; }
1532 YY_BREAK
1533/* gobble up white-spaces */
1534case 77:
1535YY_RULE_SETUP
1536#line 175 "dreal/smt2/scanner.ll"
1537{
1538 yylloc->step();
1539}
1540 YY_BREAK
1541/* gobble up end-of-lines */
1542case 78:
1543/* rule 78 can match eol */
1544YY_RULE_SETUP
1545#line 180 "dreal/smt2/scanner.ll"
1546{
1547 smt2_yycolumn=1;
1548}
1549 YY_BREAK
1550case 79:
1551YY_RULE_SETUP
1552#line 184 "dreal/smt2/scanner.ll"
1553{
1554 try {
1555 static_assert(sizeof(std::int64_t) == sizeof(long),
1556 "sizeof(std::int64_t) != sizeof(long).");
1557 yylval->build<int64_t>(std::stol(yytext));
1558 return token::INT;
1559 } catch(std::out_of_range& e) {
1560 std::cerr << "At line " << yylloc->begin.line
1561 << " the following value would fall out of the range of the result type (long):\n"
1562 << yytext << "\n";
1563 throw e;
1564 }
1565}
1566 YY_BREAK
1567case 80:
1568YY_RULE_SETUP
1569#line 198 "dreal/smt2/scanner.ll"
1570{
1571 yylval->build<std::string>(std::string(yytext, yyleng));
1572 return token::DOUBLE;
1573}
1574 YY_BREAK
1575case 81:
1576YY_RULE_SETUP
1577#line 203 "dreal/smt2/scanner.ll"
1578{
1579 yylval->build<std::string>(std::string(yytext, yyleng));
1580 return token::DOUBLE;
1581}
1582 YY_BREAK
1583case 82:
1584YY_RULE_SETUP
1585#line 208 "dreal/smt2/scanner.ll"
1586{
1587 yylval->build<double>(std::stod(yytext));
1588 return token::HEXFLOAT;
1589}
1590 YY_BREAK
1591case 83:
1592YY_RULE_SETUP
1593#line 213 "dreal/smt2/scanner.ll"
1594{
1595 yylval->build<std::string>(std::string(yytext, yyleng));
1596 return token::SYMBOL;
1597}
1598 YY_BREAK
1599case 84:
1600YY_RULE_SETUP
1601#line 218 "dreal/smt2/scanner.ll"
1602{
1603 yylval->build<std::string>(std::string(yytext, yyleng));
1604 return token::KEYWORD;
1605}
1606 YY_BREAK
1607case 85:
1608YY_RULE_SETUP
1609#line 223 "dreal/smt2/scanner.ll"
1610{ BEGIN str; yymore(); }
1611 YY_BREAK
1612case 86:
1613YY_RULE_SETUP
1614#line 224 "dreal/smt2/scanner.ll"
1615{ yymore(); }
1616 YY_BREAK
1617case 87:
1618/* rule 87 can match eol */
1619YY_RULE_SETUP
1620#line 225 "dreal/smt2/scanner.ll"
1621{ yymore(); }
1622 YY_BREAK
1623case 88:
1624YY_RULE_SETUP
1625#line 226 "dreal/smt2/scanner.ll"
1626{
1627 BEGIN 0;
1628 yylval->build<std::string>(std::string(yytext, yyleng));
1629 return token::STRING;
1630}
1631 YY_BREAK
1632case 89:
1633YY_RULE_SETUP
1634#line 231 "dreal/smt2/scanner.ll"
1635{ yymore(); }
1636 YY_BREAK
1637case 90:
1638YY_RULE_SETUP
1639#line 233 "dreal/smt2/scanner.ll"
1640{ BEGIN quoted; yymore(); }
1641 YY_BREAK
1642case 91:
1643/* rule 91 can match eol */
1644YY_RULE_SETUP
1645#line 234 "dreal/smt2/scanner.ll"
1646{ yymore(); }
1647 YY_BREAK
1648case 92:
1649YY_RULE_SETUP
1650#line 235 "dreal/smt2/scanner.ll"
1651{
1652 BEGIN 0;
1653 yylval->build<std::string>(std::string(yytext, yyleng));
1654 return token::SYMBOL;
1655}
1656 YY_BREAK
1657case 93:
1658YY_RULE_SETUP
1659#line 240 "dreal/smt2/scanner.ll"
1660{ }
1661 YY_BREAK
1662case 94:
1663YY_RULE_SETUP
1664#line 241 "dreal/smt2/scanner.ll"
1665{ yymore(); }
1666 YY_BREAK
1667/* pass all other characters up to bison */
1668case 95:
1669YY_RULE_SETUP
1670#line 244 "dreal/smt2/scanner.ll"
1671{
1672 return static_cast<token_type>(*yytext);
1673}
1674 YY_BREAK
1675case 96:
1676YY_RULE_SETUP
1677#line 247 "dreal/smt2/scanner.ll"
1678ECHO;
1679 YY_BREAK
1680#line 1680 "bazel-out/k8-opt/bin/dreal/smt2/scanner.ll.cc"
1681case YY_STATE_EOF(INITIAL):
1682case YY_STATE_EOF(str):
1683case YY_STATE_EOF(quoted):
1684 yyterminate();
1685
1686 case YY_END_OF_BUFFER:
1687 {
1688 /* Amount of text matched not including the EOB char. */
1689 int yy_amount_of_matched_text = (int) (yy_cp - (yytext_ptr)) - 1;
1690
1691 /* Undo the effects of YY_DO_BEFORE_ACTION. */
1692 *yy_cp = (yy_hold_char);
1693 YY_RESTORE_YY_MORE_OFFSET
1694
1695 if ( YY_CURRENT_BUFFER_LVALUE->yy_buffer_status == YY_BUFFER_NEW )
1696 {
1697 /* We're scanning a new file or input source. It's
1698 * possible that this happened because the user
1699 * just pointed yyin at a new source and called
1700 * yylex(). If so, then we have to assure
1701 * consistency between YY_CURRENT_BUFFER and our
1702 * globals. Here is the right place to do so, because
1703 * this is the first action (other than possibly a
1704 * back-up) that will match for the new input source.
1705 */
1706 (yy_n_chars) = YY_CURRENT_BUFFER_LVALUE->yy_n_chars;
1707/* %if-c-only */
1708/* %endif */
1709/* %if-c++-only */
1710 YY_CURRENT_BUFFER_LVALUE->yy_input_file = yyin.rdbuf();
1711/* %endif */
1712 YY_CURRENT_BUFFER_LVALUE->yy_buffer_status = YY_BUFFER_NORMAL;
1713 }
1714
1715 /* Note that here we test for yy_c_buf_p "<=" to the position
1716 * of the first EOB in the buffer, since yy_c_buf_p will
1717 * already have been incremented past the NUL character
1718 * (since all states make transitions on EOB to the
1719 * end-of-buffer state). Contrast this with the test
1720 * in input().
1721 */
1722 if ( (yy_c_buf_p) <= &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars)] )
1723 { /* This was really a NUL. */
1724 yy_state_type yy_next_state;
1725
1726 (yy_c_buf_p) = (yytext_ptr) + yy_amount_of_matched_text;
1727
1728 yy_current_state = yy_get_previous_state( );
1729
1730 /* Okay, we're now positioned to make the NUL
1731 * transition. We couldn't have
1732 * yy_get_previous_state() go ahead and do it
1733 * for us because it doesn't know how to deal
1734 * with the possibility of jamming (and we don't
1735 * want to build jamming into it because then it
1736 * will run more slowly).
1737 */
1738
1739 yy_next_state = yy_try_NUL_trans( yy_current_state );
1740
1741 yy_bp = (yytext_ptr) + YY_MORE_ADJ;
1742
1743 if ( yy_next_state )
1744 {
1745 /* Consume the NUL. */
1746 yy_cp = ++(yy_c_buf_p);
1747 yy_current_state = yy_next_state;
1748 goto yy_match;
1749 }
1750
1751 else
1752 {
1753/* %% [14.0] code to do back-up for compressed tables and set up yy_cp goes here */
1754 yy_cp = (yy_c_buf_p);
1755 goto yy_find_action;
1756 }
1757 }
1758
1759 else switch ( yy_get_next_buffer( ) )
1760 {
1761 case EOB_ACT_END_OF_FILE:
1762 {
1763 (yy_did_buffer_switch_on_eof) = 0;
1764
1765 if ( yywrap( ) )
1766 {
1767 /* Note: because we've taken care in
1768 * yy_get_next_buffer() to have set up
1769 * yytext, we can now set up
1770 * yy_c_buf_p so that if some total
1771 * hoser (like flex itself) wants to
1772 * call the scanner after we return the
1773 * YY_NULL, it'll still work - another
1774 * YY_NULL will get returned.
1775 */
1776 (yy_c_buf_p) = (yytext_ptr) + YY_MORE_ADJ;
1777
1778 yy_act = YY_STATE_EOF(YY_START);
1779 goto do_action;
1780 }
1781
1782 else
1783 {
1784 if ( ! (yy_did_buffer_switch_on_eof) )
1785 YY_NEW_FILE;
1786 }
1787 break;
1788 }
1789
1790 case EOB_ACT_CONTINUE_SCAN:
1791 (yy_c_buf_p) =
1792 (yytext_ptr) + yy_amount_of_matched_text;
1793
1794 yy_current_state = yy_get_previous_state( );
1795
1796 yy_cp = (yy_c_buf_p);
1797 yy_bp = (yytext_ptr) + YY_MORE_ADJ;
1798 goto yy_match;
1799
1800 case EOB_ACT_LAST_MATCH:
1801 (yy_c_buf_p) =
1802 &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars)];
1803
1804 yy_current_state = yy_get_previous_state( );
1805
1806 yy_cp = (yy_c_buf_p);
1807 yy_bp = (yytext_ptr) + YY_MORE_ADJ;
1808 goto yy_find_action;
1809 }
1810 break;
1811 }
1812
1813 default:
1814 YY_FATAL_ERROR(
1815 "fatal flex scanner internal error--no action found" );
1816 } /* end of action switch */
1817 } /* end of scanning one token */
1818 } /* end of user's declarations */
1819} /* end of yylex */
1820/* %ok-for-header */
1821
1822/* %if-c++-only */
1823/* %not-for-header */
1824/* The contents of this function are C++ specific, so the () macro is not used.
1825 * This constructor simply maintains backward compatibility.
1826 * DEPRECATED
1827 */
1828yyFlexLexer::yyFlexLexer( std::istream* arg_yyin, std::ostream* arg_yyout ):
1829 yyin(arg_yyin ? arg_yyin->rdbuf() : std::cin.rdbuf()),
1830 yyout(arg_yyout ? arg_yyout->rdbuf() : std::cout.rdbuf())
1831{
1832 ctor_common();
1833}
1834
1835/* The contents of this function are C++ specific, so the () macro is not used.
1836 */
1837yyFlexLexer::yyFlexLexer( std::istream& arg_yyin, std::ostream& arg_yyout ):
1838 yyin(arg_yyin.rdbuf()),
1839 yyout(arg_yyout.rdbuf())
1840{
1841 ctor_common();
1842}
1843
1844/* The contents of this function are C++ specific, so the () macro is not used.
1845 */
1846void yyFlexLexer::ctor_common()
1847{
1848 yy_c_buf_p = 0;
1849 yy_init = 0;
1850 yy_start = 0;
1851 yy_flex_debug = 0;
1852 yylineno = 1; // this will only get updated if %option yylineno
1853
1854 yy_did_buffer_switch_on_eof = 0;
1855
1856 yy_looking_for_trail_begin = 0;
1857 yy_more_flag = 0;
1858 yy_more_len = 0;
1859 yy_more_offset = yy_prev_more_offset = 0;
1860
1861 yy_start_stack_ptr = yy_start_stack_depth = 0;
1862 yy_start_stack = NULL;
1863
1864 yy_buffer_stack = NULL;
1865 yy_buffer_stack_top = 0;
1866 yy_buffer_stack_max = 0;
1867
1868 yy_state_buf = 0;
1869
1870}
1871
1872/* The contents of this function are C++ specific, so the () macro is not used.
1873 */
1874yyFlexLexer::~yyFlexLexer()
1875{
1876 delete [] yy_state_buf;
1877 yyfree( yy_start_stack );
1878 yy_delete_buffer( YY_CURRENT_BUFFER );
1879 yyfree( yy_buffer_stack );
1880}
1881
1882/* The contents of this function are C++ specific, so the () macro is not used.
1883 */
1884void yyFlexLexer::switch_streams( std::istream& new_in, std::ostream& new_out )
1885{
1886 // was if( new_in )
1887 yy_delete_buffer( YY_CURRENT_BUFFER );
1888 yy_switch_to_buffer( yy_create_buffer( new_in, YY_BUF_SIZE ) );
1889
1890 // was if( new_out )
1891 yyout.rdbuf(new_out.rdbuf());
1892}
1893
1894/* The contents of this function are C++ specific, so the () macro is not used.
1895 */
1896void yyFlexLexer::switch_streams( std::istream* new_in, std::ostream* new_out )
1897{
1898 if( ! new_in ) {
1899 new_in = &yyin;
1900 }
1901
1902 if ( ! new_out ) {
1903 new_out = &yyout;
1904 }
1905
1906 switch_streams(*new_in, *new_out);
1907}
1908
1909#ifdef YY_INTERACTIVE
1910int yyFlexLexer::LexerInput( char* buf, int /* max_size */ )
1911#else
1912int yyFlexLexer::LexerInput( char* buf, int max_size )
1913#endif
1914{
1915 if ( yyin.eof() || yyin.fail() )
1916 return 0;
1917
1918#ifdef YY_INTERACTIVE
1919 yyin.get( buf[0] );
1920
1921 if ( yyin.eof() )
1922 return 0;
1923
1924 if ( yyin.bad() )
1925 return -1;
1926
1927 return 1;
1928
1929#else
1930 (void) yyin.read( buf, max_size );
1931
1932 if ( yyin.bad() )
1933 return -1;
1934 else
1935 return yyin.gcount();
1936#endif
1937}
1938
1939void yyFlexLexer::LexerOutput( const char* buf, int size )
1940{
1941 (void) yyout.write( buf, size );
1942}
1943/* %ok-for-header */
1944
1945/* %endif */
1946
1947/* yy_get_next_buffer - try to read in a new buffer
1948 *
1949 * Returns a code representing an action:
1950 * EOB_ACT_LAST_MATCH -
1951 * EOB_ACT_CONTINUE_SCAN - continue scanning from current position
1952 * EOB_ACT_END_OF_FILE - end of file
1953 */
1954/* %if-c-only */
1955/* %endif */
1956/* %if-c++-only */
1957int yyFlexLexer::yy_get_next_buffer()
1958/* %endif */
1959{
1960 char *dest = YY_CURRENT_BUFFER_LVALUE->yy_ch_buf;
1961 char *source = (yytext_ptr);
1962 int number_to_move, i;
1963 int ret_val;
1964
1965 if ( (yy_c_buf_p) > &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars) + 1] )
1966 YY_FATAL_ERROR(
1967 "fatal flex scanner internal error--end of buffer missed" );
1968
1969 if ( YY_CURRENT_BUFFER_LVALUE->yy_fill_buffer == 0 )
1970 { /* Don't try to fill the buffer, so this is an EOF. */
1971 if ( (yy_c_buf_p) - (yytext_ptr) - YY_MORE_ADJ == 1 )
1972 {
1973 /* We matched a single character, the EOB, so
1974 * treat this as a final EOF.
1975 */
1976 return EOB_ACT_END_OF_FILE;
1977 }
1978
1979 else
1980 {
1981 /* We matched some text prior to the EOB, first
1982 * process it.
1983 */
1984 return EOB_ACT_LAST_MATCH;
1985 }
1986 }
1987
1988 /* Try to read more data. */
1989
1990 /* First move last chars to start of buffer. */
1991 number_to_move = (int) ((yy_c_buf_p) - (yytext_ptr) - 1);
1992
1993 for ( i = 0; i < number_to_move; ++i )
1994 *(dest++) = *(source++);
1995
1996 if ( YY_CURRENT_BUFFER_LVALUE->yy_buffer_status == YY_BUFFER_EOF_PENDING )
1997 /* don't do the read, it's not guaranteed to return an EOF,
1998 * just force an EOF
1999 */
2000 YY_CURRENT_BUFFER_LVALUE->yy_n_chars = (yy_n_chars) = 0;
2001
2002 else
2003 {
2004 int num_to_read =
2005 YY_CURRENT_BUFFER_LVALUE->yy_buf_size - number_to_move - 1;
2006
2007 while ( num_to_read <= 0 )
2008 { /* Not enough room in the buffer - grow it. */
2009
2010 /* just a shorter name for the current buffer */
2011 YY_BUFFER_STATE b = YY_CURRENT_BUFFER_LVALUE;
2012
2013 int yy_c_buf_p_offset =
2014 (int) ((yy_c_buf_p) - b->yy_ch_buf);
2015
2016 if ( b->yy_is_our_buffer )
2017 {
2018 int new_size = b->yy_buf_size * 2;
2019
2020 if ( new_size <= 0 )
2021 b->yy_buf_size += b->yy_buf_size / 8;
2022 else
2023 b->yy_buf_size *= 2;
2024
2025 b->yy_ch_buf = (char *)
2026 /* Include room in for 2 EOB chars. */
2027 yyrealloc( (void *) b->yy_ch_buf,
2028 (yy_size_t) (b->yy_buf_size + 2) );
2029 }
2030 else
2031 /* Can't grow it, we don't own it. */
2032 b->yy_ch_buf = NULL;
2033
2034 if ( ! b->yy_ch_buf )
2035 YY_FATAL_ERROR(
2036 "fatal error - scanner input buffer overflow" );
2037
2038 (yy_c_buf_p) = &b->yy_ch_buf[yy_c_buf_p_offset];
2039
2040 num_to_read = YY_CURRENT_BUFFER_LVALUE->yy_buf_size -
2041 number_to_move - 1;
2042
2043 }
2044
2045 if ( num_to_read > YY_READ_BUF_SIZE )
2046 num_to_read = YY_READ_BUF_SIZE;
2047
2048 /* Read in more data. */
2049 YY_INPUT( (&YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[number_to_move]),
2050 (yy_n_chars), num_to_read );
2051
2052 YY_CURRENT_BUFFER_LVALUE->yy_n_chars = (yy_n_chars);
2053 }
2054
2055 if ( (yy_n_chars) == 0 )
2056 {
2057 if ( number_to_move == YY_MORE_ADJ )
2058 {
2059 ret_val = EOB_ACT_END_OF_FILE;
2060 yyrestart( yyin );
2061 }
2062
2063 else
2064 {
2065 ret_val = EOB_ACT_LAST_MATCH;
2066 YY_CURRENT_BUFFER_LVALUE->yy_buffer_status =
2067 YY_BUFFER_EOF_PENDING;
2068 }
2069 }
2070
2071 else
2072 ret_val = EOB_ACT_CONTINUE_SCAN;
2073
2074 if (((yy_n_chars) + number_to_move) > YY_CURRENT_BUFFER_LVALUE->yy_buf_size) {
2075 /* Extend the array by 50%, plus the number we really need. */
2076 int new_size = (yy_n_chars) + number_to_move + ((yy_n_chars) >> 1);
2077 YY_CURRENT_BUFFER_LVALUE->yy_ch_buf = (char *) yyrealloc(
2078 (void *) YY_CURRENT_BUFFER_LVALUE->yy_ch_buf, (yy_size_t) new_size );
2079 if ( ! YY_CURRENT_BUFFER_LVALUE->yy_ch_buf )
2080 YY_FATAL_ERROR( "out of dynamic memory in yy_get_next_buffer()" );
2081 /* "- 2" to take care of EOB's */
2082 YY_CURRENT_BUFFER_LVALUE->yy_buf_size = (int) (new_size - 2);
2083 }
2084
2085 (yy_n_chars) += number_to_move;
2086 YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars)] = YY_END_OF_BUFFER_CHAR;
2087 YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars) + 1] = YY_END_OF_BUFFER_CHAR;
2088
2089 (yytext_ptr) = &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[0];
2090
2091 return ret_val;
2092}
2093
2094/* yy_get_previous_state - get the state just before the EOB char was reached */
2095
2096/* %if-c-only */
2097/* %not-for-header */
2098/* %endif */
2099/* %if-c++-only */
2100 yy_state_type yyFlexLexer::yy_get_previous_state()
2101/* %endif */
2102{
2103 yy_state_type yy_current_state;
2104 char *yy_cp;
2105
2106/* %% [15.0] code to get the start state into yy_current_state goes here */
2107 yy_current_state = (yy_start);
2108
2109 for ( yy_cp = (yytext_ptr) + YY_MORE_ADJ; yy_cp < (yy_c_buf_p); ++yy_cp )
2110 {
2111/* %% [16.0] code to find the next state goes here */
2112 YY_CHAR yy_c = (*yy_cp ? yy_ec[YY_SC_TO_UI(*yy_cp)] : 1);
2113 if ( yy_accept[yy_current_state] )
2114 {
2115 (yy_last_accepting_state) = yy_current_state;
2116 (yy_last_accepting_cpos) = yy_cp;
2117 }
2118 while ( yy_chk[yy_base[yy_current_state] + yy_c] != yy_current_state )
2119 {
2120 yy_current_state = (int) yy_def[yy_current_state];
2121 if ( yy_current_state >= 383 )
2122 yy_c = yy_meta[yy_c];
2123 }
2124 yy_current_state = yy_nxt[yy_base[yy_current_state] + yy_c];
2125 }
2126
2127 return yy_current_state;
2128}
2129
2130/* yy_try_NUL_trans - try to make a transition on the NUL character
2131 *
2132 * synopsis
2133 * next_state = yy_try_NUL_trans( current_state );
2134 */
2135/* %if-c-only */
2136/* %endif */
2137/* %if-c++-only */
2138 yy_state_type yyFlexLexer::yy_try_NUL_trans( yy_state_type yy_current_state )
2139/* %endif */
2140{
2141 int yy_is_jam;
2142 /* %% [17.0] code to find the next state, and perhaps do backing up, goes here */
2143 char *yy_cp = (yy_c_buf_p);
2144
2145 YY_CHAR yy_c = 1;
2146 if ( yy_accept[yy_current_state] )
2147 {
2148 (yy_last_accepting_state) = yy_current_state;
2149 (yy_last_accepting_cpos) = yy_cp;
2150 }
2151 while ( yy_chk[yy_base[yy_current_state] + yy_c] != yy_current_state )
2152 {
2153 yy_current_state = (int) yy_def[yy_current_state];
2154 if ( yy_current_state >= 383 )
2155 yy_c = yy_meta[yy_c];
2156 }
2157 yy_current_state = yy_nxt[yy_base[yy_current_state] + yy_c];
2158 yy_is_jam = (yy_current_state == 382);
2159
2160 return yy_is_jam ? 0 : yy_current_state;
2161}
2162
2163#ifndef YY_NO_UNPUT
2164/* %if-c-only */
2165/* %endif */
2166/* %if-c++-only */
2167 void yyFlexLexer::yyunput( int c, char* yy_bp)
2168/* %endif */
2169{
2170 char *yy_cp;
2171
2172 yy_cp = (yy_c_buf_p);
2173
2174 /* undo effects of setting up yytext */
2175 *yy_cp = (yy_hold_char);
2176
2177 if ( yy_cp < YY_CURRENT_BUFFER_LVALUE->yy_ch_buf + 2 )
2178 { /* need to shift things up to make room */
2179 /* +2 for EOB chars. */
2180 int number_to_move = (yy_n_chars) + 2;
2181 char *dest = &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[
2182 YY_CURRENT_BUFFER_LVALUE->yy_buf_size + 2];
2183 char *source =
2184 &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[number_to_move];
2185
2186 while ( source > YY_CURRENT_BUFFER_LVALUE->yy_ch_buf )
2187 *--dest = *--source;
2188
2189 yy_cp += (int) (dest - source);
2190 yy_bp += (int) (dest - source);
2191 YY_CURRENT_BUFFER_LVALUE->yy_n_chars =
2192 (yy_n_chars) = (int) YY_CURRENT_BUFFER_LVALUE->yy_buf_size;
2193
2194 if ( yy_cp < YY_CURRENT_BUFFER_LVALUE->yy_ch_buf + 2 )
2195 YY_FATAL_ERROR( "flex scanner push-back overflow" );
2196 }
2197
2198 *--yy_cp = (char) c;
2199
2200/* %% [18.0] update yylineno here */
2201
2202 if ( c == '\n' ){
2203 --yylineno;
2204 }
2205
2206 (yytext_ptr) = yy_bp;
2207 (yy_hold_char) = *yy_cp;
2208 (yy_c_buf_p) = yy_cp;
2209}
2210/* %if-c-only */
2211/* %endif */
2212#endif
2213
2214/* %if-c-only */
2215/* %endif */
2216/* %if-c++-only */
2217 int yyFlexLexer::yyinput()
2218/* %endif */
2219{
2220 int c;
2221
2222 *(yy_c_buf_p) = (yy_hold_char);
2223
2224 if ( *(yy_c_buf_p) == YY_END_OF_BUFFER_CHAR )
2225 {
2226 /* yy_c_buf_p now points to the character we want to return.
2227 * If this occurs *before* the EOB characters, then it's a
2228 * valid NUL; if not, then we've hit the end of the buffer.
2229 */
2230 if ( (yy_c_buf_p) < &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars)] )
2231 /* This was really a NUL. */
2232 *(yy_c_buf_p) = '\0';
2233
2234 else
2235 { /* need more input */
2236 int offset = (int) ((yy_c_buf_p) - (yytext_ptr));
2237 ++(yy_c_buf_p);
2238
2239 switch ( yy_get_next_buffer( ) )
2240 {
2241 case EOB_ACT_LAST_MATCH:
2242 /* This happens because yy_g_n_b()
2243 * sees that we've accumulated a
2244 * token and flags that we need to
2245 * try matching the token before
2246 * proceeding. But for input(),
2247 * there's no matching to consider.
2248 * So convert the EOB_ACT_LAST_MATCH
2249 * to EOB_ACT_END_OF_FILE.
2250 */
2251
2252 /* Reset buffer status. */
2253 yyrestart( yyin );
2254
2255 /*FALLTHROUGH*/
2256
2257 case EOB_ACT_END_OF_FILE:
2258 {
2259 if ( yywrap( ) )
2260 return 0;
2261
2262 if ( ! (yy_did_buffer_switch_on_eof) )
2263 YY_NEW_FILE;
2264#ifdef __cplusplus
2265 return yyinput();
2266#else
2267 return input();
2268#endif
2269 }
2270
2271 case EOB_ACT_CONTINUE_SCAN:
2272 (yy_c_buf_p) = (yytext_ptr) + offset;
2273 break;
2274 }
2275 }
2276 }
2277
2278 c = *(unsigned char *) (yy_c_buf_p); /* cast for 8-bit char's */
2279 *(yy_c_buf_p) = '\0'; /* preserve yytext */
2280 (yy_hold_char) = *++(yy_c_buf_p);
2281
2282/* %% [19.0] update BOL and yylineno */
2283 if ( c == '\n' )
2284
2285 yylineno++;
2286;
2287
2288 return c;
2289}
2290/* %if-c-only */
2291/* %endif */
2292
2293/** Immediately switch to a different input stream.
2294 * @param input_file A readable stream.
2295 *
2296 * @note This function does not reset the start condition to @c INITIAL .
2297 */
2298/* %if-c-only */
2299/* %endif */
2300/* %if-c++-only */
2301 void yyFlexLexer::yyrestart( std::istream& input_file )
2302/* %endif */
2303{
2304
2305 if ( ! YY_CURRENT_BUFFER ){
2306 yyensure_buffer_stack ();
2307 YY_CURRENT_BUFFER_LVALUE =
2308 yy_create_buffer( yyin, YY_BUF_SIZE );
2309 }
2310
2311 yy_init_buffer( YY_CURRENT_BUFFER, input_file );
2312 yy_load_buffer_state( );
2313}
2314
2315/* %if-c++-only */
2316/** Delegate to the new version that takes an istream reference.
2317 * @param input_file A readable stream.
2318 *
2319 * @note This function does not reset the start condition to @c INITIAL .
2320 */
2321void yyFlexLexer::yyrestart( std::istream* input_file )
2322{
2323 if( ! input_file ) {
2324 input_file = &yyin;
2325 }
2326 yyrestart( *input_file );
2327}
2328/* %endif */
2329
2330/** Switch to a different input buffer.
2331 * @param new_buffer The new input buffer.
2332 *
2333 */
2334/* %if-c-only */
2335/* %endif */
2336/* %if-c++-only */
2337 void yyFlexLexer::yy_switch_to_buffer( YY_BUFFER_STATE new_buffer )
2338/* %endif */
2339{
2340
2341 /* TODO. We should be able to replace this entire function body
2342 * with
2343 * yypop_buffer_state();
2344 * yypush_buffer_state(new_buffer);
2345 */
2346 yyensure_buffer_stack ();
2347 if ( YY_CURRENT_BUFFER == new_buffer )
2348 return;
2349
2350 if ( YY_CURRENT_BUFFER )
2351 {
2352 /* Flush out information for old buffer. */
2353 *(yy_c_buf_p) = (yy_hold_char);
2354 YY_CURRENT_BUFFER_LVALUE->yy_buf_pos = (yy_c_buf_p);
2355 YY_CURRENT_BUFFER_LVALUE->yy_n_chars = (yy_n_chars);
2356 }
2357
2358 YY_CURRENT_BUFFER_LVALUE = new_buffer;
2359 yy_load_buffer_state( );
2360
2361 /* We don't actually know whether we did this switch during
2362 * EOF (yywrap()) processing, but the only time this flag
2363 * is looked at is after yywrap() is called, so it's safe
2364 * to go ahead and always set it.
2365 */
2366 (yy_did_buffer_switch_on_eof) = 1;
2367}
2368
2369/* %if-c-only */
2370/* %endif */
2371/* %if-c++-only */
2372 void yyFlexLexer::yy_load_buffer_state()
2373/* %endif */
2374{
2375 (yy_n_chars) = YY_CURRENT_BUFFER_LVALUE->yy_n_chars;
2376 (yytext_ptr) = (yy_c_buf_p) = YY_CURRENT_BUFFER_LVALUE->yy_buf_pos;
2377/* %if-c-only */
2378/* %endif */
2379/* %if-c++-only */
2380 yyin.rdbuf(YY_CURRENT_BUFFER_LVALUE->yy_input_file);
2381/* %endif */
2382 (yy_hold_char) = *(yy_c_buf_p);
2383}
2384
2385/** Allocate and initialize an input buffer state.
2386 * @param file A readable stream.
2387 * @param size The character buffer size in bytes. When in doubt, use @c YY_BUF_SIZE.
2388 *
2389 * @return the allocated buffer state.
2390 */
2391/* %if-c-only */
2392/* %endif */
2393/* %if-c++-only */
2394 YY_BUFFER_STATE yyFlexLexer::yy_create_buffer( std::istream& file, int size )
2395/* %endif */
2396{
2397 YY_BUFFER_STATE b;
2398
2399 b = (YY_BUFFER_STATE) yyalloc( sizeof( struct yy_buffer_state ) );
2400 if ( ! b )
2401 YY_FATAL_ERROR( "out of dynamic memory in yy_create_buffer()" );
2402
2403 b->yy_buf_size = size;
2404
2405 /* yy_ch_buf has to be 2 characters longer than the size given because
2406 * we need to put in 2 end-of-buffer characters.
2407 */
2408 b->yy_ch_buf = (char *) yyalloc( (yy_size_t) (b->yy_buf_size + 2) );
2409 if ( ! b->yy_ch_buf )
2410 YY_FATAL_ERROR( "out of dynamic memory in yy_create_buffer()" );
2411
2412 b->yy_is_our_buffer = 1;
2413
2414 yy_init_buffer( b, file );
2415
2416 return b;
2417}
2418
2419/* %if-c++-only */
2420/** Delegate creation of buffers to the new version that takes an istream reference.
2421 * @param file A readable stream.
2422 * @param size The character buffer size in bytes. When in doubt, use @c YY_BUF_SIZE.
2423 *
2424 * @return the allocated buffer state.
2425 */
2426 YY_BUFFER_STATE yyFlexLexer::yy_create_buffer( std::istream* file, int size )
2427{
2428 return yy_create_buffer( *file, size );
2429}
2430/* %endif */
2431
2432/** Destroy the buffer.
2433 * @param b a buffer created with yy_create_buffer()
2434 *
2435 */
2436/* %if-c-only */
2437/* %endif */
2438/* %if-c++-only */
2439 void yyFlexLexer::yy_delete_buffer( YY_BUFFER_STATE b )
2440/* %endif */
2441{
2442
2443 if ( ! b )
2444 return;
2445
2446 if ( b == YY_CURRENT_BUFFER ) /* Not sure if we should pop here. */
2447 YY_CURRENT_BUFFER_LVALUE = (YY_BUFFER_STATE) 0;
2448
2449 if ( b->yy_is_our_buffer )
2450 yyfree( (void *) b->yy_ch_buf );
2451
2452 yyfree( (void *) b );
2453}
2454
2455/* Initializes or reinitializes a buffer.
2456 * This function is sometimes called more than once on the same buffer,
2457 * such as during a yyrestart() or at EOF.
2458 */
2459/* %if-c-only */
2460/* %endif */
2461/* %if-c++-only */
2462 void yyFlexLexer::yy_init_buffer( YY_BUFFER_STATE b, std::istream& file )
2463/* %endif */
2464
2465{
2466 int oerrno = errno;
2467
2468 yy_flush_buffer( b );
2469
2470/* %if-c-only */
2471/* %endif */
2472/* %if-c++-only */
2473 b->yy_input_file = file.rdbuf();
2474/* %endif */
2475 b->yy_fill_buffer = 1;
2476
2477 /* If b is the current buffer, then yy_init_buffer was _probably_
2478 * called from yyrestart() or through yy_get_next_buffer.
2479 * In that case, we don't want to reset the lineno or column.
2480 */
2481 if (b != YY_CURRENT_BUFFER){
2482 b->yy_bs_lineno = 1;
2483 b->yy_bs_column = 0;
2484 }
2485
2486/* %if-c-only */
2487/* %endif */
2488/* %if-c++-only */
2489 b->yy_is_interactive = 0;
2490/* %endif */
2491 errno = oerrno;
2492}
2493
2494/** Discard all buffered characters. On the next scan, YY_INPUT will be called.
2495 * @param b the buffer state to be flushed, usually @c YY_CURRENT_BUFFER.
2496 *
2497 */
2498/* %if-c-only */
2499/* %endif */
2500/* %if-c++-only */
2501 void yyFlexLexer::yy_flush_buffer( YY_BUFFER_STATE b )
2502/* %endif */
2503{
2504 if ( ! b )
2505 return;
2506
2507 b->yy_n_chars = 0;
2508
2509 /* We always need two end-of-buffer characters. The first causes
2510 * a transition to the end-of-buffer state. The second causes
2511 * a jam in that state.
2512 */
2513 b->yy_ch_buf[0] = YY_END_OF_BUFFER_CHAR;
2514 b->yy_ch_buf[1] = YY_END_OF_BUFFER_CHAR;
2515
2516 b->yy_buf_pos = &b->yy_ch_buf[0];
2517
2518 b->yy_at_bol = 1;
2519 b->yy_buffer_status = YY_BUFFER_NEW;
2520
2521 if ( b == YY_CURRENT_BUFFER )
2522 yy_load_buffer_state( );
2523}
2524
2525/* %if-c-or-c++ */
2526/** Pushes the new state onto the stack. The new state becomes
2527 * the current state. This function will allocate the stack
2528 * if necessary.
2529 * @param new_buffer The new state.
2530 *
2531 */
2532/* %if-c-only */
2533/* %endif */
2534/* %if-c++-only */
2535void yyFlexLexer::yypush_buffer_state (YY_BUFFER_STATE new_buffer)
2536/* %endif */
2537{
2538 if (new_buffer == NULL)
2539 return;
2540
2541 yyensure_buffer_stack();
2542
2543 /* This block is copied from yy_switch_to_buffer. */
2544 if ( YY_CURRENT_BUFFER )
2545 {
2546 /* Flush out information for old buffer. */
2547 *(yy_c_buf_p) = (yy_hold_char);
2548 YY_CURRENT_BUFFER_LVALUE->yy_buf_pos = (yy_c_buf_p);
2549 YY_CURRENT_BUFFER_LVALUE->yy_n_chars = (yy_n_chars);
2550 }
2551
2552 /* Only push if top exists. Otherwise, replace top. */
2553 if (YY_CURRENT_BUFFER)
2554 (yy_buffer_stack_top)++;
2555 YY_CURRENT_BUFFER_LVALUE = new_buffer;
2556
2557 /* copied from yy_switch_to_buffer. */
2558 yy_load_buffer_state( );
2559 (yy_did_buffer_switch_on_eof) = 1;
2560}
2561/* %endif */
2562
2563/* %if-c-or-c++ */
2564/** Removes and deletes the top of the stack, if present.
2565 * The next element becomes the new top.
2566 *
2567 */
2568/* %if-c-only */
2569/* %endif */
2570/* %if-c++-only */
2571void yyFlexLexer::yypop_buffer_state (void)
2572/* %endif */
2573{
2574 if (!YY_CURRENT_BUFFER)
2575 return;
2576
2577 yy_delete_buffer(YY_CURRENT_BUFFER );
2578 YY_CURRENT_BUFFER_LVALUE = NULL;
2579 if ((yy_buffer_stack_top) > 0)
2580 --(yy_buffer_stack_top);
2581
2582 if (YY_CURRENT_BUFFER) {
2583 yy_load_buffer_state( );
2584 (yy_did_buffer_switch_on_eof) = 1;
2585 }
2586}
2587/* %endif */
2588
2589/* %if-c-or-c++ */
2590/* Allocates the stack if it does not exist.
2591 * Guarantees space for at least one push.
2592 */
2593/* %if-c-only */
2594/* %endif */
2595/* %if-c++-only */
2596void yyFlexLexer::yyensure_buffer_stack(void)
2597/* %endif */
2598{
2599 yy_size_t num_to_alloc;
2600
2601 if (!(yy_buffer_stack)) {
2602
2603 /* First allocation is just for 2 elements, since we don't know if this
2604 * scanner will even need a stack. We use 2 instead of 1 to avoid an
2605 * immediate realloc on the next call.
2606 */
2607 num_to_alloc = 1; /* After all that talk, this was set to 1 anyways... */
2608 (yy_buffer_stack) = (struct yy_buffer_state**)yyalloc
2609 (num_to_alloc * sizeof(struct yy_buffer_state*)
2610 );
2611 if ( ! (yy_buffer_stack) )
2612 YY_FATAL_ERROR( "out of dynamic memory in yyensure_buffer_stack()" );
2613
2614 memset((yy_buffer_stack), 0, num_to_alloc * sizeof(struct yy_buffer_state*));
2615
2616 (yy_buffer_stack_max) = num_to_alloc;
2617 (yy_buffer_stack_top) = 0;
2618 return;
2619 }
2620
2621 if ((yy_buffer_stack_top) >= ((yy_buffer_stack_max)) - 1){
2622
2623 /* Increase the buffer to prepare for a possible push. */
2624 yy_size_t grow_size = 8 /* arbitrary grow size */;
2625
2626 num_to_alloc = (yy_buffer_stack_max) + grow_size;
2627 (yy_buffer_stack) = (struct yy_buffer_state**)yyrealloc
2628 ((yy_buffer_stack),
2629 num_to_alloc * sizeof(struct yy_buffer_state*)
2630 );
2631 if ( ! (yy_buffer_stack) )
2632 YY_FATAL_ERROR( "out of dynamic memory in yyensure_buffer_stack()" );
2633
2634 /* zero only the new slots.*/
2635 memset((yy_buffer_stack) + (yy_buffer_stack_max), 0, grow_size * sizeof(struct yy_buffer_state*));
2636 (yy_buffer_stack_max) = num_to_alloc;
2637 }
2638}
2639/* %endif */
2640
2641/* %if-c-only */
2642/* %endif */
2643
2644/* %if-c-only */
2645/* %endif */
2646
2647/* %if-c-only */
2648/* %endif */
2649
2650/* %if-c-only */
2651/* %endif */
2652/* %if-c++-only */
2653 void yyFlexLexer::yy_push_state( int _new_state )
2654/* %endif */
2655{
2656 if ( (yy_start_stack_ptr) >= (yy_start_stack_depth) )
2657 {
2658 yy_size_t new_size;
2659
2660 (yy_start_stack_depth) += YY_START_STACK_INCR;
2661 new_size = (yy_size_t) (yy_start_stack_depth) * sizeof( int );
2662
2663 if ( ! (yy_start_stack) )
2664 (yy_start_stack) = (int *) yyalloc( new_size );
2665
2666 else
2667 (yy_start_stack) = (int *) yyrealloc(
2668 (void *) (yy_start_stack), new_size );
2669
2670 if ( ! (yy_start_stack) )
2671 YY_FATAL_ERROR( "out of memory expanding start-condition stack" );
2672 }
2673
2674 (yy_start_stack)[(yy_start_stack_ptr)++] = YY_START;
2675
2676 BEGIN(_new_state);
2677}
2678
2679/* %if-c-only */
2680/* %endif */
2681/* %if-c++-only */
2682 void yyFlexLexer::yy_pop_state()
2683/* %endif */
2684{
2685 if ( --(yy_start_stack_ptr) < 0 )
2686 YY_FATAL_ERROR( "start-condition stack underflow" );
2687
2688 BEGIN((yy_start_stack)[(yy_start_stack_ptr)]);
2689}
2690
2691/* %if-c-only */
2692/* %endif */
2693/* %if-c++-only */
2694 int yyFlexLexer::yy_top_state()
2695/* %endif */
2696{
2697 return (yy_start_stack)[(yy_start_stack_ptr) - 1];
2698}
2699
2700#ifndef YY_EXIT_FAILURE
2701#define YY_EXIT_FAILURE 2
2702#endif
2703
2704/* %if-c-only */
2705/* %endif */
2706/* %if-c++-only */
2707void yyFlexLexer::LexerError( const char* msg )
2708{
2709 std::cerr << msg << std::endl;
2710 exit( YY_EXIT_FAILURE );
2711}
2712/* %endif */
2713
2714/* Redefine yyless() so it works in section 3 code. */
2715
2716#undef yyless
2717#define yyless(n) \
2718 do \
2719 { \
2720 /* Undo effects of setting up yytext. */ \
2721 int yyless_macro_arg = (n); \
2722 YY_LESS_LINENO(yyless_macro_arg);\
2723 yytext[yyleng] = (yy_hold_char); \
2724 (yy_c_buf_p) = yytext + yyless_macro_arg; \
2725 (yy_hold_char) = *(yy_c_buf_p); \
2726 *(yy_c_buf_p) = '\0'; \
2727 yyleng = yyless_macro_arg; \
2728 } \
2729 while ( 0 )
2730
2731/* Accessor methods (get/set functions) to struct members. */
2732
2733/* %if-c-only */
2734/* %if-reentrant */
2735/* %endif */
2736/* %if-reentrant */
2737/* %endif */
2738/* %endif */
2739
2740/* %if-reentrant */
2741/* %if-bison-bridge */
2742/* %endif */
2743/* %endif if-c-only */
2744
2745/* %if-c-only */
2746/* %endif */
2747
2748/* %if-c-only SNIP! this currently causes conflicts with the c++ scanner */
2749/* %if-reentrant */
2750/* %endif */
2751/* %endif */
2752
2753/*
2754 * Internal utility routines.
2755 */
2756
2757#ifndef yytext_ptr
2758static void yy_flex_strncpy (char* s1, const char * s2, int n )
2759{
2760
2761 int i;
2762 for ( i = 0; i < n; ++i )
2763 s1[i] = s2[i];
2764}
2765#endif
2766
2767#ifdef YY_NEED_STRLEN
2768static int yy_flex_strlen (const char * s )
2769{
2770 int n;
2771 for ( n = 0; s[n]; ++n )
2772 ;
2773
2774 return n;
2775}
2776#endif
2777
2778void *yyalloc (yy_size_t size )
2779{
2780 return malloc(size);
2781}
2782
2783void *yyrealloc (void * ptr, yy_size_t size )
2784{
2785
2786 /* The cast to (char *) in the following accommodates both
2787 * implementations that use char* generic pointers, and those
2788 * that use void* generic pointers. It works with the latter
2789 * because both ANSI C and C++ allow castless assignment from
2790 * any pointer type to void*, and deal with argument conversions
2791 * as though doing an assignment.
2792 */
2793 return realloc(ptr, size);
2794}
2795
2796void yyfree (void * ptr )
2797{
2798 free( (char *) ptr ); /* see yyrealloc() for (char *) cast */
2799}
2800
2801/* %if-tables-serialization definitions */
2802/* %define-yytables The name for this specific scanner's tables. */
2803#define YYTABLES_NAME "yytables"
2804/* %endif */
2805
2806/* %ok-for-header */
2807
2808#line 247 "dreal/smt2/scanner.ll"
2809
2810
2811namespace dreal {
2812
2813Smt2Scanner::Smt2Scanner(std::istream* in,
2814 std::ostream* out)
2815 : Smt2FlexLexer(in, out) {}
2816
2817Smt2Scanner::~Smt2Scanner() {}
2818
2819void Smt2Scanner::set_debug(const bool b) {
2820 yy_flex_debug = b;
2821}
2822} // namespace dreal
2823
2824/* This implementation of Smt2FlexLexer::yylex() is required to fill the
2825 * vtable of the class Smt2FlexLexer. We define the scanner's main yylex
2826 * function via YY_DECL to reside in the Smt2Scanner class instead. */
2827
2828#ifdef yylex
2829#undef yylex
2830#endif
2831
2832int Smt2FlexLexer::yylex()
2833{
2834 std::cerr << "in Smt2lexLexer::yylex() !" << std::endl;
2835 return 0;
2836}
2837
2838/* When the scanner receives an end-of-file indication from YY_INPUT, it then
2839 * checks the yywrap() function. If yywrap() returns false (zero), then it is
2840 * assumed that the function has gone ahead and set up `yyin' to point to
2841 * another input file, and scanning continues. If it returns true (non-zero),
2842 * then the scanner terminates, returning 0 to its caller. */
2843
2844int Smt2FlexLexer::yywrap()
2845{
2846 return 1;
2847}
2848
2849#pragma GCC diagnostic pop
2850
2851#ifdef __clang__
2852#pragma clang diagnostic pop
2853#endif
2854
generated by cgit v1.2.3-54-g00ecf (git 2.45.0) at 2024-05-06 02:37:30 +0000