diff options
Diffstat (limited to 'Solvers/dreal4/bazel-bin/dreal/smt2/scanner.ll.cc')
-rwxr-xr-x | Solvers/dreal4/bazel-bin/dreal/smt2/scanner.ll.cc | 2854 |
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> | ||
86 | typedef int8_t flex_int8_t; | ||
87 | typedef uint8_t flex_uint8_t; | ||
88 | typedef int16_t flex_int16_t; | ||
89 | typedef uint16_t flex_uint16_t; | ||
90 | typedef int32_t flex_int32_t; | ||
91 | typedef uint32_t flex_uint32_t; | ||
92 | #else | ||
93 | typedef signed char flex_int8_t; | ||
94 | typedef short int flex_int16_t; | ||
95 | typedef int flex_int32_t; | ||
96 | typedef unsigned char flex_uint8_t; | ||
97 | typedef unsigned short int flex_uint16_t; | ||
98 | typedef 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 | ||
213 | typedef struct yy_buffer_state *YY_BUFFER_STATE; | ||
214 | #endif | ||
215 | |||
216 | #ifndef YY_TYPEDEF_YY_SIZE_T | ||
217 | #define YY_TYPEDEF_YY_SIZE_T | ||
218 | typedef size_t yy_size_t; | ||
219 | #endif | ||
220 | |||
221 | /* %if-not-reentrant */ | ||
222 | extern 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 | ||
273 | struct 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 | |||
371 | void *yyalloc ( yy_size_t ); | ||
372 | void *yyrealloc ( void *, yy_size_t ); | ||
373 | void 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 | ||
400 | typedef 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. */ | ||
429 | struct yy_trans_info | ||
430 | { | ||
431 | flex_int32_t yy_verify; | ||
432 | flex_int32_t yy_nxt; | ||
433 | }; | ||
434 | static 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 | |||
480 | static 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 | |||
512 | static 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 | |||
523 | static 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 | |||
569 | static 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 | |||
615 | static 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 | |||
692 | static 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. */ | ||
770 | static const flex_int32_t yy_rule_can_match_eol[97] = | ||
771 | { 0, | ||
772 | 1, 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 | |||
778 | static 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 */ | ||
820 | typedef dreal::Smt2Parser::token token; | ||
821 | typedef 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 */ | ||
843 | int smt2_yycolumn = 1; | ||
844 | |||
845 | #define YY_USER_ACTION yylloc->begin.line = yylloc->end.line = yylineno; \ | ||
846 | yylloc->begin.column = smt2_yycolumn; yylloc->end.column = smt2_yycolumn+yyleng-1; \ | ||
847 | smt2_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 | ||
887 | static void yy_flex_strncpy ( char *, const char *, int ); | ||
888 | #endif | ||
889 | |||
890 | #ifdef YY_NEED_STRLEN | ||
891 | static 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 | */ | ||
1002 | YY_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); | ||
1078 | yy_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 | |||
1098 | yy_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 | |||
1122 | do_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 | |||
1150 | case 1: | ||
1151 | /* rule 1 can match eol */ | ||
1152 | YY_RULE_SETUP | ||
1153 | #line 91 "dreal/smt2/scanner.ll" | ||
1154 | { | ||
1155 | smt2_yycolumn=1; | ||
1156 | } | ||
1157 | YY_BREAK | ||
1158 | case 2: | ||
1159 | YY_RULE_SETUP | ||
1160 | #line 95 "dreal/smt2/scanner.ll" | ||
1161 | { return Smt2Parser::token::TK_EXCLAMATION; } | ||
1162 | YY_BREAK | ||
1163 | case 3: | ||
1164 | YY_RULE_SETUP | ||
1165 | #line 96 "dreal/smt2/scanner.ll" | ||
1166 | { return Smt2Parser::token::TK_BINARY; } | ||
1167 | YY_BREAK | ||
1168 | case 4: | ||
1169 | YY_RULE_SETUP | ||
1170 | #line 97 "dreal/smt2/scanner.ll" | ||
1171 | { return Smt2Parser::token::TK_DECIMAL; } | ||
1172 | YY_BREAK | ||
1173 | case 5: | ||
1174 | YY_RULE_SETUP | ||
1175 | #line 98 "dreal/smt2/scanner.ll" | ||
1176 | { return Smt2Parser::token::TK_HEXADECIMAL; } | ||
1177 | YY_BREAK | ||
1178 | case 6: | ||
1179 | YY_RULE_SETUP | ||
1180 | #line 99 "dreal/smt2/scanner.ll" | ||
1181 | { return Smt2Parser::token::TK_NUMERAL; } | ||
1182 | YY_BREAK | ||
1183 | case 7: | ||
1184 | YY_RULE_SETUP | ||
1185 | #line 100 "dreal/smt2/scanner.ll" | ||
1186 | { return Smt2Parser::token::TK_STRING; } | ||
1187 | YY_BREAK | ||
1188 | case 8: | ||
1189 | YY_RULE_SETUP | ||
1190 | #line 101 "dreal/smt2/scanner.ll" | ||
1191 | { return Smt2Parser::token::TK_UNDERSCORE; } | ||
1192 | YY_BREAK | ||
1193 | case 9: | ||
1194 | YY_RULE_SETUP | ||
1195 | #line 102 "dreal/smt2/scanner.ll" | ||
1196 | { return Smt2Parser::token::TK_AS; } | ||
1197 | YY_BREAK | ||
1198 | case 10: | ||
1199 | YY_RULE_SETUP | ||
1200 | #line 103 "dreal/smt2/scanner.ll" | ||
1201 | { return Smt2Parser::token::TK_EXISTS; } | ||
1202 | YY_BREAK | ||
1203 | case 11: | ||
1204 | YY_RULE_SETUP | ||
1205 | #line 104 "dreal/smt2/scanner.ll" | ||
1206 | { return Smt2Parser::token::TK_FORALL; } | ||
1207 | YY_BREAK | ||
1208 | case 12: | ||
1209 | YY_RULE_SETUP | ||
1210 | #line 105 "dreal/smt2/scanner.ll" | ||
1211 | { return Smt2Parser::token::TK_LET; } | ||
1212 | YY_BREAK | ||
1213 | case 13: | ||
1214 | YY_RULE_SETUP | ||
1215 | #line 106 "dreal/smt2/scanner.ll" | ||
1216 | { return Smt2Parser::token::TK_PAR; } | ||
1217 | YY_BREAK | ||
1218 | case 14: | ||
1219 | YY_RULE_SETUP | ||
1220 | #line 108 "dreal/smt2/scanner.ll" | ||
1221 | { return Smt2Parser::token::TK_ASSERT; } | ||
1222 | YY_BREAK | ||
1223 | case 15: | ||
1224 | YY_RULE_SETUP | ||
1225 | #line 109 "dreal/smt2/scanner.ll" | ||
1226 | { return Smt2Parser::token::TK_CHECK_SAT; } | ||
1227 | YY_BREAK | ||
1228 | case 16: | ||
1229 | YY_RULE_SETUP | ||
1230 | #line 110 "dreal/smt2/scanner.ll" | ||
1231 | { return Smt2Parser::token::TK_CHECK_SAT_ASSUMING; } | ||
1232 | YY_BREAK | ||
1233 | case 17: | ||
1234 | YY_RULE_SETUP | ||
1235 | #line 111 "dreal/smt2/scanner.ll" | ||
1236 | { return Smt2Parser::token::TK_DECLARE_CONST; } | ||
1237 | YY_BREAK | ||
1238 | case 18: | ||
1239 | YY_RULE_SETUP | ||
1240 | #line 112 "dreal/smt2/scanner.ll" | ||
1241 | { return Smt2Parser::token::TK_DECLARE_FUN; } | ||
1242 | YY_BREAK | ||
1243 | case 19: | ||
1244 | YY_RULE_SETUP | ||
1245 | #line 113 "dreal/smt2/scanner.ll" | ||
1246 | { return Smt2Parser::token::TK_DECLARE_SORT; } | ||
1247 | YY_BREAK | ||
1248 | case 20: | ||
1249 | YY_RULE_SETUP | ||
1250 | #line 114 "dreal/smt2/scanner.ll" | ||
1251 | { return Smt2Parser::token::TK_DEFINE_FUN; } | ||
1252 | YY_BREAK | ||
1253 | case 21: | ||
1254 | YY_RULE_SETUP | ||
1255 | #line 115 "dreal/smt2/scanner.ll" | ||
1256 | { return Smt2Parser::token::TK_DEFINE_FUN_REC; } | ||
1257 | YY_BREAK | ||
1258 | case 22: | ||
1259 | YY_RULE_SETUP | ||
1260 | #line 116 "dreal/smt2/scanner.ll" | ||
1261 | { return Smt2Parser::token::TK_DEFINE_SORT; } | ||
1262 | YY_BREAK | ||
1263 | case 23: | ||
1264 | YY_RULE_SETUP | ||
1265 | #line 117 "dreal/smt2/scanner.ll" | ||
1266 | { return Smt2Parser::token::TK_ECHO; } | ||
1267 | YY_BREAK | ||
1268 | case 24: | ||
1269 | YY_RULE_SETUP | ||
1270 | #line 118 "dreal/smt2/scanner.ll" | ||
1271 | { return Smt2Parser::token::TK_EXIT; } | ||
1272 | YY_BREAK | ||
1273 | case 25: | ||
1274 | YY_RULE_SETUP | ||
1275 | #line 119 "dreal/smt2/scanner.ll" | ||
1276 | { return Smt2Parser::token::TK_GET_ASSERTIONS; } | ||
1277 | YY_BREAK | ||
1278 | case 26: | ||
1279 | YY_RULE_SETUP | ||
1280 | #line 120 "dreal/smt2/scanner.ll" | ||
1281 | { return Smt2Parser::token::TK_GET_ASSIGNMENT; } | ||
1282 | YY_BREAK | ||
1283 | case 27: | ||
1284 | YY_RULE_SETUP | ||
1285 | #line 121 "dreal/smt2/scanner.ll" | ||
1286 | { return Smt2Parser::token::TK_GET_INFO; } | ||
1287 | YY_BREAK | ||
1288 | case 28: | ||
1289 | YY_RULE_SETUP | ||
1290 | #line 122 "dreal/smt2/scanner.ll" | ||
1291 | { return Smt2Parser::token::TK_GET_MODEL; } | ||
1292 | YY_BREAK | ||
1293 | case 29: | ||
1294 | YY_RULE_SETUP | ||
1295 | #line 123 "dreal/smt2/scanner.ll" | ||
1296 | { return Smt2Parser::token::TK_GET_OPTION; } | ||
1297 | YY_BREAK | ||
1298 | case 30: | ||
1299 | YY_RULE_SETUP | ||
1300 | #line 124 "dreal/smt2/scanner.ll" | ||
1301 | { return Smt2Parser::token::TK_GET_PROOF; } | ||
1302 | YY_BREAK | ||
1303 | case 31: | ||
1304 | YY_RULE_SETUP | ||
1305 | #line 125 "dreal/smt2/scanner.ll" | ||
1306 | { return Smt2Parser::token::TK_GET_UNSAT_ASSUMPTIONS; } | ||
1307 | YY_BREAK | ||
1308 | case 32: | ||
1309 | YY_RULE_SETUP | ||
1310 | #line 126 "dreal/smt2/scanner.ll" | ||
1311 | { return Smt2Parser::token::TK_GET_UNSAT_CORE; } | ||
1312 | YY_BREAK | ||
1313 | case 33: | ||
1314 | YY_RULE_SETUP | ||
1315 | #line 127 "dreal/smt2/scanner.ll" | ||
1316 | { return Smt2Parser::token::TK_GET_VALUE; } | ||
1317 | YY_BREAK | ||
1318 | case 34: | ||
1319 | YY_RULE_SETUP | ||
1320 | #line 128 "dreal/smt2/scanner.ll" | ||
1321 | { return Smt2Parser::token::TK_POP; } | ||
1322 | YY_BREAK | ||
1323 | case 35: | ||
1324 | YY_RULE_SETUP | ||
1325 | #line 129 "dreal/smt2/scanner.ll" | ||
1326 | { return Smt2Parser::token::TK_PUSH; } | ||
1327 | YY_BREAK | ||
1328 | case 36: | ||
1329 | YY_RULE_SETUP | ||
1330 | #line 130 "dreal/smt2/scanner.ll" | ||
1331 | { return Smt2Parser::token::TK_RESET; } | ||
1332 | YY_BREAK | ||
1333 | case 37: | ||
1334 | YY_RULE_SETUP | ||
1335 | #line 131 "dreal/smt2/scanner.ll" | ||
1336 | { return Smt2Parser::token::TK_RESET_ASSERTIONS; } | ||
1337 | YY_BREAK | ||
1338 | case 38: | ||
1339 | YY_RULE_SETUP | ||
1340 | #line 132 "dreal/smt2/scanner.ll" | ||
1341 | { return Smt2Parser::token::TK_SET_INFO; } | ||
1342 | YY_BREAK | ||
1343 | case 39: | ||
1344 | YY_RULE_SETUP | ||
1345 | #line 133 "dreal/smt2/scanner.ll" | ||
1346 | { return Smt2Parser::token::TK_SET_LOGIC; } | ||
1347 | YY_BREAK | ||
1348 | case 40: | ||
1349 | YY_RULE_SETUP | ||
1350 | #line 134 "dreal/smt2/scanner.ll" | ||
1351 | { return Smt2Parser::token::TK_SET_OPTION; } | ||
1352 | YY_BREAK | ||
1353 | case 41: | ||
1354 | YY_RULE_SETUP | ||
1355 | #line 136 "dreal/smt2/scanner.ll" | ||
1356 | { return Smt2Parser::token::TK_PLUS; } | ||
1357 | YY_BREAK | ||
1358 | case 42: | ||
1359 | YY_RULE_SETUP | ||
1360 | #line 137 "dreal/smt2/scanner.ll" | ||
1361 | { return Smt2Parser::token::TK_MINUS; } | ||
1362 | YY_BREAK | ||
1363 | case 43: | ||
1364 | YY_RULE_SETUP | ||
1365 | #line 138 "dreal/smt2/scanner.ll" | ||
1366 | { return Smt2Parser::token::TK_TIMES; } | ||
1367 | YY_BREAK | ||
1368 | case 44: | ||
1369 | YY_RULE_SETUP | ||
1370 | #line 139 "dreal/smt2/scanner.ll" | ||
1371 | { return Smt2Parser::token::TK_DIV; } | ||
1372 | YY_BREAK | ||
1373 | case 45: | ||
1374 | YY_RULE_SETUP | ||
1375 | #line 140 "dreal/smt2/scanner.ll" | ||
1376 | { return Smt2Parser::token::TK_EQ; } | ||
1377 | YY_BREAK | ||
1378 | case 46: | ||
1379 | YY_RULE_SETUP | ||
1380 | #line 141 "dreal/smt2/scanner.ll" | ||
1381 | { return Smt2Parser::token::TK_LTE; } | ||
1382 | YY_BREAK | ||
1383 | case 47: | ||
1384 | YY_RULE_SETUP | ||
1385 | #line 142 "dreal/smt2/scanner.ll" | ||
1386 | { return Smt2Parser::token::TK_GTE; } | ||
1387 | YY_BREAK | ||
1388 | case 48: | ||
1389 | YY_RULE_SETUP | ||
1390 | #line 143 "dreal/smt2/scanner.ll" | ||
1391 | { return Smt2Parser::token::TK_LT; } | ||
1392 | YY_BREAK | ||
1393 | case 49: | ||
1394 | YY_RULE_SETUP | ||
1395 | #line 144 "dreal/smt2/scanner.ll" | ||
1396 | { return Smt2Parser::token::TK_GT; } | ||
1397 | YY_BREAK | ||
1398 | case 50: | ||
1399 | YY_RULE_SETUP | ||
1400 | #line 145 "dreal/smt2/scanner.ll" | ||
1401 | { return Smt2Parser::token::TK_EXP; } | ||
1402 | YY_BREAK | ||
1403 | case 51: | ||
1404 | YY_RULE_SETUP | ||
1405 | #line 146 "dreal/smt2/scanner.ll" | ||
1406 | { return Smt2Parser::token::TK_LOG; } | ||
1407 | YY_BREAK | ||
1408 | case 52: | ||
1409 | YY_RULE_SETUP | ||
1410 | #line 147 "dreal/smt2/scanner.ll" | ||
1411 | { return Smt2Parser::token::TK_ABS; } | ||
1412 | YY_BREAK | ||
1413 | case 53: | ||
1414 | YY_RULE_SETUP | ||
1415 | #line 148 "dreal/smt2/scanner.ll" | ||
1416 | { return Smt2Parser::token::TK_SIN; } | ||
1417 | YY_BREAK | ||
1418 | case 54: | ||
1419 | YY_RULE_SETUP | ||
1420 | #line 149 "dreal/smt2/scanner.ll" | ||
1421 | { return Smt2Parser::token::TK_COS; } | ||
1422 | YY_BREAK | ||
1423 | case 55: | ||
1424 | YY_RULE_SETUP | ||
1425 | #line 150 "dreal/smt2/scanner.ll" | ||
1426 | { return Smt2Parser::token::TK_TAN; } | ||
1427 | YY_BREAK | ||
1428 | case 56: | ||
1429 | YY_RULE_SETUP | ||
1430 | #line 151 "dreal/smt2/scanner.ll" | ||
1431 | { return Smt2Parser::token::TK_ASIN; } | ||
1432 | YY_BREAK | ||
1433 | case 57: | ||
1434 | YY_RULE_SETUP | ||
1435 | #line 152 "dreal/smt2/scanner.ll" | ||
1436 | { return Smt2Parser::token::TK_ACOS; } | ||
1437 | YY_BREAK | ||
1438 | case 58: | ||
1439 | YY_RULE_SETUP | ||
1440 | #line 153 "dreal/smt2/scanner.ll" | ||
1441 | { return Smt2Parser::token::TK_ATAN; } | ||
1442 | YY_BREAK | ||
1443 | case 59: | ||
1444 | YY_RULE_SETUP | ||
1445 | #line 154 "dreal/smt2/scanner.ll" | ||
1446 | { return Smt2Parser::token::TK_ATAN2; } | ||
1447 | YY_BREAK | ||
1448 | case 60: | ||
1449 | YY_RULE_SETUP | ||
1450 | #line 155 "dreal/smt2/scanner.ll" | ||
1451 | { return Smt2Parser::token::TK_SINH; } | ||
1452 | YY_BREAK | ||
1453 | case 61: | ||
1454 | YY_RULE_SETUP | ||
1455 | #line 156 "dreal/smt2/scanner.ll" | ||
1456 | { return Smt2Parser::token::TK_COSH; } | ||
1457 | YY_BREAK | ||
1458 | case 62: | ||
1459 | YY_RULE_SETUP | ||
1460 | #line 157 "dreal/smt2/scanner.ll" | ||
1461 | { return Smt2Parser::token::TK_TANH; } | ||
1462 | YY_BREAK | ||
1463 | case 63: | ||
1464 | YY_RULE_SETUP | ||
1465 | #line 158 "dreal/smt2/scanner.ll" | ||
1466 | { return Smt2Parser::token::TK_MIN; } | ||
1467 | YY_BREAK | ||
1468 | case 64: | ||
1469 | YY_RULE_SETUP | ||
1470 | #line 159 "dreal/smt2/scanner.ll" | ||
1471 | { return Smt2Parser::token::TK_MAX; } | ||
1472 | YY_BREAK | ||
1473 | case 65: | ||
1474 | YY_RULE_SETUP | ||
1475 | #line 160 "dreal/smt2/scanner.ll" | ||
1476 | { return Smt2Parser::token::TK_MAXIMIZE; } | ||
1477 | YY_BREAK | ||
1478 | case 66: | ||
1479 | YY_RULE_SETUP | ||
1480 | #line 161 "dreal/smt2/scanner.ll" | ||
1481 | { return Smt2Parser::token::TK_MINIMIZE; } | ||
1482 | YY_BREAK | ||
1483 | case 67: | ||
1484 | YY_RULE_SETUP | ||
1485 | #line 162 "dreal/smt2/scanner.ll" | ||
1486 | { return Smt2Parser::token::TK_SQRT; } | ||
1487 | YY_BREAK | ||
1488 | case 68: | ||
1489 | YY_RULE_SETUP | ||
1490 | #line 163 "dreal/smt2/scanner.ll" | ||
1491 | { return Smt2Parser::token::TK_POW; } | ||
1492 | YY_BREAK | ||
1493 | case 69: | ||
1494 | YY_RULE_SETUP | ||
1495 | #line 165 "dreal/smt2/scanner.ll" | ||
1496 | { return Smt2Parser::token::TK_TRUE; } | ||
1497 | YY_BREAK | ||
1498 | case 70: | ||
1499 | YY_RULE_SETUP | ||
1500 | #line 166 "dreal/smt2/scanner.ll" | ||
1501 | { return Smt2Parser::token::TK_FALSE; } | ||
1502 | YY_BREAK | ||
1503 | case 71: | ||
1504 | YY_RULE_SETUP | ||
1505 | #line 167 "dreal/smt2/scanner.ll" | ||
1506 | { return Smt2Parser::token::TK_AND; } | ||
1507 | YY_BREAK | ||
1508 | case 72: | ||
1509 | YY_RULE_SETUP | ||
1510 | #line 168 "dreal/smt2/scanner.ll" | ||
1511 | { return Smt2Parser::token::TK_OR; } | ||
1512 | YY_BREAK | ||
1513 | case 73: | ||
1514 | YY_RULE_SETUP | ||
1515 | #line 169 "dreal/smt2/scanner.ll" | ||
1516 | { return Smt2Parser::token::TK_XOR; } | ||
1517 | YY_BREAK | ||
1518 | case 74: | ||
1519 | YY_RULE_SETUP | ||
1520 | #line 170 "dreal/smt2/scanner.ll" | ||
1521 | { return Smt2Parser::token::TK_NOT; } | ||
1522 | YY_BREAK | ||
1523 | case 75: | ||
1524 | YY_RULE_SETUP | ||
1525 | #line 171 "dreal/smt2/scanner.ll" | ||
1526 | { return Smt2Parser::token::TK_ITE; } | ||
1527 | YY_BREAK | ||
1528 | case 76: | ||
1529 | YY_RULE_SETUP | ||
1530 | #line 172 "dreal/smt2/scanner.ll" | ||
1531 | { return Smt2Parser::token::TK_IMPLIES; } | ||
1532 | YY_BREAK | ||
1533 | /* gobble up white-spaces */ | ||
1534 | case 77: | ||
1535 | YY_RULE_SETUP | ||
1536 | #line 175 "dreal/smt2/scanner.ll" | ||
1537 | { | ||
1538 | yylloc->step(); | ||
1539 | } | ||
1540 | YY_BREAK | ||
1541 | /* gobble up end-of-lines */ | ||
1542 | case 78: | ||
1543 | /* rule 78 can match eol */ | ||
1544 | YY_RULE_SETUP | ||
1545 | #line 180 "dreal/smt2/scanner.ll" | ||
1546 | { | ||
1547 | smt2_yycolumn=1; | ||
1548 | } | ||
1549 | YY_BREAK | ||
1550 | case 79: | ||
1551 | YY_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 | ||
1567 | case 80: | ||
1568 | YY_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 | ||
1575 | case 81: | ||
1576 | YY_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 | ||
1583 | case 82: | ||
1584 | YY_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 | ||
1591 | case 83: | ||
1592 | YY_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 | ||
1599 | case 84: | ||
1600 | YY_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 | ||
1607 | case 85: | ||
1608 | YY_RULE_SETUP | ||
1609 | #line 223 "dreal/smt2/scanner.ll" | ||
1610 | { BEGIN str; yymore(); } | ||
1611 | YY_BREAK | ||
1612 | case 86: | ||
1613 | YY_RULE_SETUP | ||
1614 | #line 224 "dreal/smt2/scanner.ll" | ||
1615 | { yymore(); } | ||
1616 | YY_BREAK | ||
1617 | case 87: | ||
1618 | /* rule 87 can match eol */ | ||
1619 | YY_RULE_SETUP | ||
1620 | #line 225 "dreal/smt2/scanner.ll" | ||
1621 | { yymore(); } | ||
1622 | YY_BREAK | ||
1623 | case 88: | ||
1624 | YY_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 | ||
1632 | case 89: | ||
1633 | YY_RULE_SETUP | ||
1634 | #line 231 "dreal/smt2/scanner.ll" | ||
1635 | { yymore(); } | ||
1636 | YY_BREAK | ||
1637 | case 90: | ||
1638 | YY_RULE_SETUP | ||
1639 | #line 233 "dreal/smt2/scanner.ll" | ||
1640 | { BEGIN quoted; yymore(); } | ||
1641 | YY_BREAK | ||
1642 | case 91: | ||
1643 | /* rule 91 can match eol */ | ||
1644 | YY_RULE_SETUP | ||
1645 | #line 234 "dreal/smt2/scanner.ll" | ||
1646 | { yymore(); } | ||
1647 | YY_BREAK | ||
1648 | case 92: | ||
1649 | YY_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 | ||
1657 | case 93: | ||
1658 | YY_RULE_SETUP | ||
1659 | #line 240 "dreal/smt2/scanner.ll" | ||
1660 | { } | ||
1661 | YY_BREAK | ||
1662 | case 94: | ||
1663 | YY_RULE_SETUP | ||
1664 | #line 241 "dreal/smt2/scanner.ll" | ||
1665 | { yymore(); } | ||
1666 | YY_BREAK | ||
1667 | /* pass all other characters up to bison */ | ||
1668 | case 95: | ||
1669 | YY_RULE_SETUP | ||
1670 | #line 244 "dreal/smt2/scanner.ll" | ||
1671 | { | ||
1672 | return static_cast<token_type>(*yytext); | ||
1673 | } | ||
1674 | YY_BREAK | ||
1675 | case 96: | ||
1676 | YY_RULE_SETUP | ||
1677 | #line 247 "dreal/smt2/scanner.ll" | ||
1678 | ECHO; | ||
1679 | YY_BREAK | ||
1680 | #line 1680 "bazel-out/k8-opt/bin/dreal/smt2/scanner.ll.cc" | ||
1681 | case YY_STATE_EOF(INITIAL): | ||
1682 | case YY_STATE_EOF(str): | ||
1683 | case 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 | */ | ||
1828 | yyFlexLexer::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 | */ | ||
1837 | yyFlexLexer::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 | */ | ||
1846 | void 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 | */ | ||
1874 | yyFlexLexer::~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 | */ | ||
1884 | void 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 | */ | ||
1896 | void 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 | ||
1910 | int yyFlexLexer::LexerInput( char* buf, int /* max_size */ ) | ||
1911 | #else | ||
1912 | int 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 | |||
1939 | void 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 */ | ||
1957 | int 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 | */ | ||
2321 | void 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 */ | ||
2535 | void 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 */ | ||
2571 | void 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 */ | ||
2596 | void 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 */ | ||
2707 | void 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 | ||
2758 | static 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 | ||
2768 | static 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 | |||
2778 | void *yyalloc (yy_size_t size ) | ||
2779 | { | ||
2780 | return malloc(size); | ||
2781 | } | ||
2782 | |||
2783 | void *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 | |||
2796 | void 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 | |||
2811 | namespace dreal { | ||
2812 | |||
2813 | Smt2Scanner::Smt2Scanner(std::istream* in, | ||
2814 | std::ostream* out) | ||
2815 | : Smt2FlexLexer(in, out) {} | ||
2816 | |||
2817 | Smt2Scanner::~Smt2Scanner() {} | ||
2818 | |||
2819 | void 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 | |||
2832 | int 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 | |||
2844 | int 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 | |||