From 1f3bc8188e9061885ad7a3477eb629399bcb938a Mon Sep 17 00:00:00 2001 From: Martin Blicha Date: Tue, 5 Mar 2024 19:43:51 +0100 Subject: [PATCH] Parser: Remove generated files These files should be generated locally at the user and should not be commited to the repository. --- src/parsers/smt2new/smt2newlexer.cc | 3166 -------------------------- src/parsers/smt2new/smt2newparser.cc | 2887 ----------------------- src/parsers/smt2new/smt2newparser.hh | 160 -- 3 files changed, 6213 deletions(-) delete mode 100644 src/parsers/smt2new/smt2newlexer.cc delete mode 100644 src/parsers/smt2new/smt2newparser.cc delete mode 100644 src/parsers/smt2new/smt2newparser.hh diff --git a/src/parsers/smt2new/smt2newlexer.cc b/src/parsers/smt2new/smt2newlexer.cc deleted file mode 100644 index c3dc11387..000000000 --- a/src/parsers/smt2new/smt2newlexer.cc +++ /dev/null @@ -1,3166 +0,0 @@ -#line 1 "smt2new/smt2newlexer.cc" - -#line 3 "smt2new/smt2newlexer.cc" - -#define YY_INT_ALIGNED short int - -/* A lexical scanner generated by flex */ - -#define FLEX_SCANNER -#define YY_FLEX_MAJOR_VERSION 2 -#define YY_FLEX_MINOR_VERSION 6 -#define YY_FLEX_SUBMINOR_VERSION 4 -#if YY_FLEX_SUBMINOR_VERSION > 0 -#define FLEX_BETA -#endif - -#ifdef yy_create_buffer -#define smt2new_create_buffer_ALREADY_DEFINED -#else -#define yy_create_buffer smt2new_create_buffer -#endif - -#ifdef yy_delete_buffer -#define smt2new_delete_buffer_ALREADY_DEFINED -#else -#define yy_delete_buffer smt2new_delete_buffer -#endif - -#ifdef yy_scan_buffer -#define smt2new_scan_buffer_ALREADY_DEFINED -#else -#define yy_scan_buffer smt2new_scan_buffer -#endif - -#ifdef yy_scan_string -#define smt2new_scan_string_ALREADY_DEFINED -#else -#define yy_scan_string smt2new_scan_string -#endif - -#ifdef yy_scan_bytes -#define smt2new_scan_bytes_ALREADY_DEFINED -#else -#define yy_scan_bytes smt2new_scan_bytes -#endif - -#ifdef yy_init_buffer -#define smt2new_init_buffer_ALREADY_DEFINED -#else -#define yy_init_buffer smt2new_init_buffer -#endif - -#ifdef yy_flush_buffer -#define smt2new_flush_buffer_ALREADY_DEFINED -#else -#define yy_flush_buffer smt2new_flush_buffer -#endif - -#ifdef yy_load_buffer_state -#define smt2new_load_buffer_state_ALREADY_DEFINED -#else -#define yy_load_buffer_state smt2new_load_buffer_state -#endif - -#ifdef yy_switch_to_buffer -#define smt2new_switch_to_buffer_ALREADY_DEFINED -#else -#define yy_switch_to_buffer smt2new_switch_to_buffer -#endif - -#ifdef yypush_buffer_state -#define smt2newpush_buffer_state_ALREADY_DEFINED -#else -#define yypush_buffer_state smt2newpush_buffer_state -#endif - -#ifdef yypop_buffer_state -#define smt2newpop_buffer_state_ALREADY_DEFINED -#else -#define yypop_buffer_state smt2newpop_buffer_state -#endif - -#ifdef yyensure_buffer_stack -#define smt2newensure_buffer_stack_ALREADY_DEFINED -#else -#define yyensure_buffer_stack smt2newensure_buffer_stack -#endif - -#ifdef yylex -#define smt2newlex_ALREADY_DEFINED -#else -#define yylex smt2newlex -#endif - -#ifdef yyrestart -#define smt2newrestart_ALREADY_DEFINED -#else -#define yyrestart smt2newrestart -#endif - -#ifdef yylex_init -#define smt2newlex_init_ALREADY_DEFINED -#else -#define yylex_init smt2newlex_init -#endif - -#ifdef yylex_init_extra -#define smt2newlex_init_extra_ALREADY_DEFINED -#else -#define yylex_init_extra smt2newlex_init_extra -#endif - -#ifdef yylex_destroy -#define smt2newlex_destroy_ALREADY_DEFINED -#else -#define yylex_destroy smt2newlex_destroy -#endif - -#ifdef yyget_debug -#define smt2newget_debug_ALREADY_DEFINED -#else -#define yyget_debug smt2newget_debug -#endif - -#ifdef yyset_debug -#define smt2newset_debug_ALREADY_DEFINED -#else -#define yyset_debug smt2newset_debug -#endif - -#ifdef yyget_extra -#define smt2newget_extra_ALREADY_DEFINED -#else -#define yyget_extra smt2newget_extra -#endif - -#ifdef yyset_extra -#define smt2newset_extra_ALREADY_DEFINED -#else -#define yyset_extra smt2newset_extra -#endif - -#ifdef yyget_in -#define smt2newget_in_ALREADY_DEFINED -#else -#define yyget_in smt2newget_in -#endif - -#ifdef yyset_in -#define smt2newset_in_ALREADY_DEFINED -#else -#define yyset_in smt2newset_in -#endif - -#ifdef yyget_out -#define smt2newget_out_ALREADY_DEFINED -#else -#define yyget_out smt2newget_out -#endif - -#ifdef yyset_out -#define smt2newset_out_ALREADY_DEFINED -#else -#define yyset_out smt2newset_out -#endif - -#ifdef yyget_leng -#define smt2newget_leng_ALREADY_DEFINED -#else -#define yyget_leng smt2newget_leng -#endif - -#ifdef yyget_text -#define smt2newget_text_ALREADY_DEFINED -#else -#define yyget_text smt2newget_text -#endif - -#ifdef yyget_lineno -#define smt2newget_lineno_ALREADY_DEFINED -#else -#define yyget_lineno smt2newget_lineno -#endif - -#ifdef yyset_lineno -#define smt2newset_lineno_ALREADY_DEFINED -#else -#define yyset_lineno smt2newset_lineno -#endif - -#ifdef yyget_column -#define smt2newget_column_ALREADY_DEFINED -#else -#define yyget_column smt2newget_column -#endif - -#ifdef yyset_column -#define smt2newset_column_ALREADY_DEFINED -#else -#define yyset_column smt2newset_column -#endif - -#ifdef yywrap -#define smt2newwrap_ALREADY_DEFINED -#else -#define yywrap smt2newwrap -#endif - -#ifdef yyget_lval -#define smt2newget_lval_ALREADY_DEFINED -#else -#define yyget_lval smt2newget_lval -#endif - -#ifdef yyset_lval -#define smt2newset_lval_ALREADY_DEFINED -#else -#define yyset_lval smt2newset_lval -#endif - -#ifdef yyget_lloc -#define smt2newget_lloc_ALREADY_DEFINED -#else -#define yyget_lloc smt2newget_lloc -#endif - -#ifdef yyset_lloc -#define smt2newset_lloc_ALREADY_DEFINED -#else -#define yyset_lloc smt2newset_lloc -#endif - -#ifdef yyalloc -#define smt2newalloc_ALREADY_DEFINED -#else -#define yyalloc smt2newalloc -#endif - -#ifdef yyrealloc -#define smt2newrealloc_ALREADY_DEFINED -#else -#define yyrealloc smt2newrealloc -#endif - -#ifdef yyfree -#define smt2newfree_ALREADY_DEFINED -#else -#define yyfree smt2newfree -#endif - -/* First, we deal with platform-specific or compiler-specific issues. */ - -/* begin standard C headers. */ -#include -#include -#include -#include - -/* end standard C headers. */ - -/* flex integer type definitions */ - -#ifndef FLEXINT_H -#define FLEXINT_H - -/* C99 systems have . Non-C99 systems may or may not. */ - -#if defined (__STDC_VERSION__) && __STDC_VERSION__ >= 199901L - -/* C99 says to define __STDC_LIMIT_MACROS before including stdint.h, - * if you want the limit (max/min) macros for int types. - */ -#ifndef __STDC_LIMIT_MACROS -#define __STDC_LIMIT_MACROS 1 -#endif - -#include -typedef int8_t flex_int8_t; -typedef uint8_t flex_uint8_t; -typedef int16_t flex_int16_t; -typedef uint16_t flex_uint16_t; -typedef int32_t flex_int32_t; -typedef uint32_t flex_uint32_t; -#else -typedef signed char flex_int8_t; -typedef short int flex_int16_t; -typedef int flex_int32_t; -typedef unsigned char flex_uint8_t; -typedef unsigned short int flex_uint16_t; -typedef unsigned int flex_uint32_t; - -/* Limits of integral types. */ -#ifndef INT8_MIN -#define INT8_MIN (-128) -#endif -#ifndef INT16_MIN -#define INT16_MIN (-32767-1) -#endif -#ifndef INT32_MIN -#define INT32_MIN (-2147483647-1) -#endif -#ifndef INT8_MAX -#define INT8_MAX (127) -#endif -#ifndef INT16_MAX -#define INT16_MAX (32767) -#endif -#ifndef INT32_MAX -#define INT32_MAX (2147483647) -#endif -#ifndef UINT8_MAX -#define UINT8_MAX (255U) -#endif -#ifndef UINT16_MAX -#define UINT16_MAX (65535U) -#endif -#ifndef UINT32_MAX -#define UINT32_MAX (4294967295U) -#endif - -#ifndef SIZE_MAX -#define SIZE_MAX (~(size_t)0) -#endif - -#endif /* ! C99 */ - -#endif /* ! FLEXINT_H */ - -/* begin standard C++ headers. */ - -/* TODO: this is always defined, so inline it */ -#define yyconst const - -#if defined(__GNUC__) && __GNUC__ >= 3 -#define yynoreturn __attribute__((__noreturn__)) -#else -#define yynoreturn -#endif - -/* Returned upon end-of-file. */ -#define YY_NULL 0 - -/* Promotes a possibly negative, possibly signed char to an - * integer in range [0..255] for use as an array index. - */ -#define YY_SC_TO_UI(c) ((YY_CHAR) (c)) - -/* An opaque pointer. */ -#ifndef YY_TYPEDEF_YY_SCANNER_T -#define YY_TYPEDEF_YY_SCANNER_T -typedef void* yyscan_t; -#endif - -/* For convenience, these vars (plus the bison vars far below) - are macros in the reentrant scanner. */ -#define yyin yyg->yyin_r -#define yyout yyg->yyout_r -#define yyextra yyg->yyextra_r -#define yyleng yyg->yyleng_r -#define yytext yyg->yytext_r -#define yylineno (YY_CURRENT_BUFFER_LVALUE->yy_bs_lineno) -#define yycolumn (YY_CURRENT_BUFFER_LVALUE->yy_bs_column) -#define yy_flex_debug yyg->yy_flex_debug_r - -/* Enter a start condition. This macro really ought to take a parameter, - * but we do it the disgusting crufty way forced on us by the ()-less - * definition of BEGIN. - */ -#define BEGIN yyg->yy_start = 1 + 2 * -/* Translate the current start state into a value that can be later handed - * to BEGIN to return to the state. The YYSTATE alias is for lex - * compatibility. - */ -#define YY_START ((yyg->yy_start - 1) / 2) -#define YYSTATE YY_START -/* Action number for EOF rule of a given start state. */ -#define YY_STATE_EOF(state) (YY_END_OF_BUFFER + state + 1) -/* Special action meaning "start processing a new file". */ -#define YY_NEW_FILE yyrestart( yyin , yyscanner ) -#define YY_END_OF_BUFFER_CHAR 0 - -/* Size of default input buffer. */ -#ifndef YY_BUF_SIZE -#ifdef __ia64__ -/* On IA-64, the buffer size is 16k, not 8k. - * Moreover, YY_BUF_SIZE is 2*YY_READ_BUF_SIZE in the general case. - * Ditto for the __ia64__ case accordingly. - */ -#define YY_BUF_SIZE 32768 -#else -#define YY_BUF_SIZE 16384 -#endif /* __ia64__ */ -#endif - -/* The state buf must be large enough to hold one state per character in the main buffer. - */ -#define YY_STATE_BUF_SIZE ((YY_BUF_SIZE + 2) * sizeof(yy_state_type)) - -#ifndef YY_TYPEDEF_YY_BUFFER_STATE -#define YY_TYPEDEF_YY_BUFFER_STATE -typedef struct yy_buffer_state *YY_BUFFER_STATE; -#endif - -#ifndef YY_TYPEDEF_YY_SIZE_T -#define YY_TYPEDEF_YY_SIZE_T -typedef size_t yy_size_t; -#endif - -#define EOB_ACT_CONTINUE_SCAN 0 -#define EOB_ACT_END_OF_FILE 1 -#define EOB_ACT_LAST_MATCH 2 - - /* Note: We specifically omit the test for yy_rule_can_match_eol because it requires - * access to the local variable yy_act. Since yyless() is a macro, it would break - * existing scanners that call yyless() from OUTSIDE yylex. - * One obvious solution it to make yy_act a global. I tried that, and saw - * a 5% performance hit in a non-yylineno scanner, because yy_act is - * normally declared as a register variable-- so it is not worth it. - */ - #define YY_LESS_LINENO(n) \ - do { \ - int yyl;\ - for ( yyl = n; yyl < yyleng; ++yyl )\ - if ( yytext[yyl] == '\n' )\ - --yylineno;\ - }while(0) - #define YY_LINENO_REWIND_TO(dst) \ - do {\ - const char *p;\ - for ( p = yy_cp-1; p >= (dst); --p)\ - if ( *p == '\n' )\ - --yylineno;\ - }while(0) - -/* Return all but the first "n" matched characters back to the input stream. */ -#define yyless(n) \ - do \ - { \ - /* Undo effects of setting up yytext. */ \ - int yyless_macro_arg = (n); \ - YY_LESS_LINENO(yyless_macro_arg);\ - *yy_cp = yyg->yy_hold_char; \ - YY_RESTORE_YY_MORE_OFFSET \ - yyg->yy_c_buf_p = yy_cp = yy_bp + yyless_macro_arg - YY_MORE_ADJ; \ - YY_DO_BEFORE_ACTION; /* set up yytext again */ \ - } \ - while ( 0 ) -#define unput(c) yyunput( c, yyg->yytext_ptr , yyscanner ) - -#ifndef YY_STRUCT_YY_BUFFER_STATE -#define YY_STRUCT_YY_BUFFER_STATE -struct yy_buffer_state - { - FILE *yy_input_file; - - char *yy_ch_buf; /* input buffer */ - char *yy_buf_pos; /* current position in input buffer */ - - /* Size of input buffer in bytes, not including room for EOB - * characters. - */ - int yy_buf_size; - - /* Number of characters read into yy_ch_buf, not including EOB - * characters. - */ - int yy_n_chars; - - /* Whether we "own" the buffer - i.e., we know we created it, - * and can realloc() it to grow it, and should free() it to - * delete it. - */ - int yy_is_our_buffer; - - /* Whether this is an "interactive" input source; if so, and - * if we're using stdio for input, then we want to use getc() - * instead of fread(), to make sure we stop fetching input after - * each newline. - */ - int yy_is_interactive; - - /* Whether we're considered to be at the beginning of a line. - * If so, '^' rules will be active on the next match, otherwise - * not. - */ - int yy_at_bol; - - int yy_bs_lineno; /**< The line count. */ - int yy_bs_column; /**< The column count. */ - - /* Whether to try to fill the input buffer when we reach the - * end of it. - */ - int yy_fill_buffer; - - int yy_buffer_status; - -#define YY_BUFFER_NEW 0 -#define YY_BUFFER_NORMAL 1 - /* When an EOF's been seen but there's still some text to process - * then we mark the buffer as YY_EOF_PENDING, to indicate that we - * shouldn't try reading from the input source any more. We might - * still have a bunch of tokens to match, though, because of - * possible backing-up. - * - * When we actually see the EOF, we change the status to "new" - * (via yyrestart()), so that the user can continue scanning by - * just pointing yyin at a new input file. - */ -#define YY_BUFFER_EOF_PENDING 2 - - }; -#endif /* !YY_STRUCT_YY_BUFFER_STATE */ - -/* We provide macros for accessing buffer states in case in the - * future we want to put the buffer states in a more general - * "scanner state". - * - * Returns the top of the stack, or NULL. - */ -#define YY_CURRENT_BUFFER ( yyg->yy_buffer_stack \ - ? yyg->yy_buffer_stack[yyg->yy_buffer_stack_top] \ - : NULL) -/* Same as previous macro, but useful when we know that the buffer stack is not - * NULL or when we need an lvalue. For internal use only. - */ -#define YY_CURRENT_BUFFER_LVALUE yyg->yy_buffer_stack[yyg->yy_buffer_stack_top] - -void yyrestart ( FILE *input_file , yyscan_t yyscanner ); -void yy_switch_to_buffer ( YY_BUFFER_STATE new_buffer , yyscan_t yyscanner ); -YY_BUFFER_STATE yy_create_buffer ( FILE *file, int size , yyscan_t yyscanner ); -void yy_delete_buffer ( YY_BUFFER_STATE b , yyscan_t yyscanner ); -void yy_flush_buffer ( YY_BUFFER_STATE b , yyscan_t yyscanner ); -void yypush_buffer_state ( YY_BUFFER_STATE new_buffer , yyscan_t yyscanner ); -void yypop_buffer_state ( yyscan_t yyscanner ); - -static void yyensure_buffer_stack ( yyscan_t yyscanner ); -static void yy_load_buffer_state ( yyscan_t yyscanner ); -static void yy_init_buffer ( YY_BUFFER_STATE b, FILE *file , yyscan_t yyscanner ); -#define YY_FLUSH_BUFFER yy_flush_buffer( YY_CURRENT_BUFFER , yyscanner) - -YY_BUFFER_STATE yy_scan_buffer ( char *base, yy_size_t size , yyscan_t yyscanner ); -YY_BUFFER_STATE yy_scan_string ( const char *yy_str , yyscan_t yyscanner ); -YY_BUFFER_STATE yy_scan_bytes ( const char *bytes, int len , yyscan_t yyscanner ); - -void *yyalloc ( yy_size_t , yyscan_t yyscanner ); -void *yyrealloc ( void *, yy_size_t , yyscan_t yyscanner ); -void yyfree ( void * , yyscan_t yyscanner ); - -#define yy_new_buffer yy_create_buffer -#define yy_set_interactive(is_interactive) \ - { \ - if ( ! YY_CURRENT_BUFFER ){ \ - yyensure_buffer_stack (yyscanner); \ - YY_CURRENT_BUFFER_LVALUE = \ - yy_create_buffer( yyin, YY_BUF_SIZE , yyscanner); \ - } \ - YY_CURRENT_BUFFER_LVALUE->yy_is_interactive = is_interactive; \ - } -#define yy_set_bol(at_bol) \ - { \ - if ( ! YY_CURRENT_BUFFER ){\ - yyensure_buffer_stack (yyscanner); \ - YY_CURRENT_BUFFER_LVALUE = \ - yy_create_buffer( yyin, YY_BUF_SIZE , yyscanner); \ - } \ - YY_CURRENT_BUFFER_LVALUE->yy_at_bol = at_bol; \ - } -#define YY_AT_BOL() (YY_CURRENT_BUFFER_LVALUE->yy_at_bol) - -/* Begin user sect3 */ - -#define smt2newwrap(yyscanner) (/*CONSTCOND*/1) -#define YY_SKIP_YYWRAP -typedef flex_uint8_t YY_CHAR; - -typedef int yy_state_type; - -#define yytext_ptr yytext_r - -static yy_state_type yy_get_previous_state ( yyscan_t yyscanner ); -static yy_state_type yy_try_NUL_trans ( yy_state_type current_state , yyscan_t yyscanner); -static int yy_get_next_buffer ( yyscan_t yyscanner ); -static void yynoreturn yy_fatal_error ( const char* msg , yyscan_t yyscanner ); - -/* Done after the current pattern has been matched and before the - * corresponding action - sets up yytext. - */ -#define YY_DO_BEFORE_ACTION \ - yyg->yytext_ptr = yy_bp; \ - yyleng = (int) (yy_cp - yy_bp); \ - yyg->yy_hold_char = *yy_cp; \ - *yy_cp = '\0'; \ - yyg->yy_c_buf_p = yy_cp; -#define YY_NUM_RULES 91 -#define YY_END_OF_BUFFER 92 -/* This struct is not used in this scanner, - but its presence is necessary. */ -struct yy_trans_info - { - flex_int32_t yy_verify; - flex_int32_t yy_nxt; - }; -static const flex_int16_t yy_accept[559] = - { 0, - 0, 0, 0, 0, 0, 0, 92, 90, 2, 2, - 3, 75, 90, 72, 74, 72, 68, 68, 90, 1, - 72, 72, 72, 4, 72, 72, 72, 72, 72, 72, - 72, 72, 72, 72, 72, 72, 83, 81, 77, 78, - 76, 82, 91, 87, 85, 86, 84, 89, 88, 2, - 72, 0, 0, 72, 68, 0, 0, 0, 68, 73, - 73, 73, 73, 73, 73, 73, 73, 73, 73, 73, - 73, 73, 1, 72, 72, 72, 5, 72, 72, 72, - 72, 72, 72, 72, 72, 72, 72, 72, 72, 72, - 72, 79, 80, 71, 70, 72, 72, 68, 69, 69, - - 68, 73, 73, 73, 73, 73, 73, 73, 73, 73, - 73, 73, 73, 73, 73, 73, 73, 73, 73, 73, - 72, 72, 72, 72, 72, 72, 72, 72, 72, 72, - 9, 11, 28, 72, 72, 72, 72, 72, 72, 69, - 69, 68, 68, 73, 73, 73, 73, 73, 73, 73, - 73, 73, 73, 73, 73, 73, 73, 73, 73, 73, - 73, 73, 73, 73, 73, 72, 72, 72, 72, 72, - 72, 72, 72, 20, 72, 72, 29, 72, 72, 72, - 72, 72, 68, 73, 73, 73, 73, 73, 73, 73, - 40, 73, 73, 61, 73, 73, 73, 73, 73, 73, - - 73, 73, 73, 73, 73, 73, 72, 72, 72, 72, - 72, 72, 72, 72, 72, 72, 72, 72, 72, 72, - 72, 72, 72, 72, 72, 72, 72, 72, 73, 73, - 73, 73, 73, 73, 73, 73, 73, 73, 62, 45, - 73, 73, 73, 73, 73, 39, 73, 73, 73, 73, - 73, 72, 72, 12, 13, 72, 72, 72, 7, 8, - 72, 72, 72, 72, 72, 72, 72, 72, 72, 72, - 72, 34, 72, 73, 73, 73, 73, 73, 73, 73, - 73, 73, 73, 73, 73, 73, 73, 73, 73, 65, - 73, 44, 73, 73, 6, 10, 72, 72, 72, 72, - - 72, 72, 72, 72, 72, 72, 72, 72, 72, 72, - 72, 72, 72, 73, 63, 73, 73, 73, 73, 73, - 73, 73, 73, 73, 73, 73, 73, 73, 73, 73, - 73, 64, 72, 72, 72, 72, 72, 72, 23, 72, - 72, 72, 72, 72, 72, 31, 72, 72, 37, 72, - 72, 73, 73, 73, 73, 73, 73, 73, 73, 47, - 73, 73, 73, 73, 73, 73, 46, 73, 14, 72, - 72, 72, 72, 72, 72, 72, 72, 72, 25, 72, - 27, 72, 30, 72, 72, 72, 73, 73, 73, 73, - 73, 73, 73, 73, 73, 73, 73, 73, 73, 73, - - 73, 73, 73, 59, 72, 72, 72, 19, 72, 72, - 72, 72, 24, 72, 36, 32, 38, 72, 73, 43, - 73, 73, 73, 48, 73, 73, 73, 73, 73, 73, - 73, 73, 73, 73, 73, 72, 16, 72, 18, 72, - 72, 72, 72, 35, 73, 73, 73, 73, 73, 73, - 73, 73, 73, 73, 73, 58, 73, 73, 73, 72, - 15, 72, 72, 72, 72, 73, 73, 73, 73, 73, - 73, 73, 73, 73, 73, 73, 73, 73, 73, 17, - 72, 72, 72, 72, 73, 73, 73, 73, 73, 73, - 49, 73, 73, 73, 73, 73, 73, 73, 21, 22, - - 72, 26, 67, 73, 60, 73, 73, 73, 73, 54, - 52, 73, 66, 73, 73, 72, 73, 73, 73, 73, - 73, 73, 73, 73, 33, 73, 73, 42, 51, 73, - 73, 73, 73, 73, 73, 73, 73, 73, 41, 73, - 50, 73, 73, 73, 73, 55, 53, 73, 73, 73, - 73, 73, 73, 56, 73, 73, 57, 0 - } ; - -static const YY_CHAR yy_ec[256] = - { 0, - 1, 1, 1, 1, 1, 1, 1, 1, 2, 3, - 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, - 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, - 1, 4, 5, 6, 7, 8, 8, 8, 9, 10, - 10, 8, 8, 1, 11, 12, 13, 14, 15, 16, - 16, 16, 16, 16, 16, 16, 16, 17, 18, 8, - 8, 8, 8, 8, 19, 20, 21, 22, 23, 20, - 24, 8, 25, 8, 8, 26, 27, 28, 8, 8, - 8, 29, 30, 31, 32, 8, 8, 8, 8, 8, - 1, 33, 1, 8, 34, 1, 35, 36, 37, 38, - - 39, 40, 41, 42, 43, 8, 44, 45, 46, 47, - 48, 49, 8, 50, 51, 52, 53, 54, 55, 56, - 57, 8, 1, 58, 1, 8, 1, 1, 1, 1, - 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, - 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, - 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, - 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, - 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, - 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, - 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, - - 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, - 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, - 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, - 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, - 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, - 1, 1, 1, 1, 1 - } ; - -static const YY_CHAR yy_meta[59] = - { 0, - 1, 1, 2, 1, 3, 1, 1, 3, 4, 1, - 3, 3, 3, 5, 5, 5, 1, 1, 5, 5, - 5, 5, 5, 3, 3, 3, 3, 3, 3, 3, - 3, 3, 1, 3, 5, 5, 5, 5, 5, 5, - 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, - 3, 3, 3, 3, 3, 3, 3, 1 - } ; - -static const flex_int16_t yy_base[565] = - { 0, - 0, 0, 57, 62, 67, 70, 666, 667, 73, 76, - 0, 667, 26, 0, 667, 69, 77, 92, 94, 0, - 642, 632, 632, 0, 611, 619, 621, 603, 610, 618, - 617, 46, 616, 58, 612, 603, 667, 667, 667, 667, - 667, 667, 80, 667, 667, 667, 667, 667, 667, 107, - 0, 73, 0, 100, 105, 108, 135, 111, 140, 0, - 85, 59, 86, 599, 604, 615, 122, 599, 96, 110, - 606, 124, 0, 626, 619, 616, 593, 604, 124, 599, - 591, 588, 587, 588, 588, 585, 600, 582, 587, 593, - 588, 667, 667, 151, 0, 153, 156, 161, 164, 167, - - 170, 585, 577, 588, 592, 576, 138, 578, 572, 576, - 576, 569, 145, 573, 154, 569, 583, 578, 571, 565, - 589, 590, 587, 572, 573, 564, 565, 140, 572, 595, - 0, 0, 0, 563, 566, 592, 553, 553, 548, 182, - 185, 188, 191, 588, 556, 554, 555, 547, 559, 554, - 541, 552, 549, 550, 549, 540, 548, 547, 533, 530, - 530, 529, 532, 526, 158, 551, 548, 548, 525, 530, - 538, 525, 519, 0, 525, 173, 0, 558, 167, 523, - 517, 527, 203, 514, 516, 516, 515, 511, 513, 512, - 547, 507, 503, 517, 503, 501, 499, 503, 502, 504, - - 497, 494, 496, 506, 496, 500, 523, 522, 516, 487, - 527, 487, 497, 484, 489, 482, 485, 482, 480, 482, - 493, 476, 479, 477, 475, 480, 465, 510, 468, 469, - 475, 469, 505, 477, 463, 475, 477, 476, 0, 0, - 499, 472, 462, 460, 471, 494, 453, 460, 451, 450, - 452, 473, 472, 0, 0, 446, 457, 484, 0, 0, - 443, 171, 441, 444, 440, 445, 437, 448, 446, 434, - 445, 0, 173, 449, 432, 430, 430, 444, 468, 435, - 438, 439, 434, 423, 434, 461, 460, 420, 431, 0, - 429, 0, 424, 419, 0, 0, 430, 453, 174, 189, - - 415, 423, 418, 412, 424, 405, 422, 408, 412, 411, - 396, 399, 399, 398, 0, 406, 396, 408, 408, 397, - 393, 391, 403, 388, 429, 388, 385, 426, 397, 384, - 382, 0, 381, 193, 379, 383, 380, 388, 0, 378, - 379, 386, 373, 385, 371, 0, 385, 373, 0, 373, - 384, 375, 369, 373, 373, 375, 366, 375, 368, 0, - 373, 185, 370, 361, 359, 355, 0, 348, 0, 356, - 350, 354, 354, 350, 347, 351, 348, 349, 0, 384, - 0, 355, 0, 346, 341, 339, 339, 342, 351, 352, - 346, 334, 334, 329, 345, 330, 332, 329, 331, 338, - - 332, 322, 337, 0, 326, 325, 321, 0, 318, 326, - 322, 319, 0, 329, 0, 0, 0, 326, 312, 0, - 352, 308, 318, 0, 317, 320, 319, 306, 318, 307, - 303, 315, 305, 299, 300, 298, 0, 296, 0, 299, - 307, 300, 296, 0, 300, 294, 298, 293, 290, 327, - 286, 293, 296, 286, 298, 0, 284, 282, 287, 277, - 0, 281, 280, 291, 275, 287, 270, 274, 278, 268, - 273, 267, 276, 271, 275, 262, 258, 259, 262, 0, - 259, 257, 261, 268, 255, 253, 254, 251, 259, 253, - 0, 253, 248, 247, 286, 249, 243, 242, 0, 0, - - 241, 0, 0, 243, 0, 248, 242, 251, 242, 0, - 0, 250, 0, 275, 242, 233, 230, 234, 234, 241, - 240, 230, 240, 228, 0, 223, 227, 0, 0, 226, - 222, 229, 223, 258, 217, 215, 227, 227, 0, 222, - 0, 192, 191, 194, 198, 0, 0, 192, 202, 197, - 188, 184, 113, 0, 101, 51, 0, 667, 244, 249, - 252, 255, 260, 62 - } ; - -static const flex_int16_t yy_def[565] = - { 0, - 558, 1, 559, 559, 560, 560, 558, 558, 558, 558, - 561, 558, 558, 561, 558, 561, 558, 558, 562, 563, - 561, 561, 561, 561, 561, 561, 561, 561, 561, 561, - 561, 561, 561, 561, 561, 561, 558, 558, 558, 558, - 558, 558, 558, 558, 558, 558, 558, 558, 558, 558, - 561, 558, 564, 561, 561, 558, 558, 558, 558, 562, - 562, 562, 562, 562, 562, 562, 562, 562, 562, 562, - 562, 562, 563, 561, 561, 561, 561, 561, 561, 561, - 561, 561, 561, 561, 561, 561, 561, 561, 561, 561, - 561, 558, 558, 558, 564, 561, 561, 561, 558, 558, - - 558, 562, 562, 562, 562, 562, 562, 562, 562, 562, - 562, 562, 562, 562, 562, 562, 562, 562, 562, 562, - 561, 561, 561, 561, 561, 561, 561, 561, 561, 561, - 561, 561, 561, 561, 561, 561, 561, 561, 561, 561, - 561, 561, 558, 562, 562, 562, 562, 562, 562, 562, - 562, 562, 562, 562, 562, 562, 562, 562, 562, 562, - 562, 562, 562, 562, 562, 561, 561, 561, 561, 561, - 561, 561, 561, 561, 561, 561, 561, 561, 561, 561, - 561, 561, 561, 562, 562, 562, 562, 562, 562, 562, - 562, 562, 562, 562, 562, 562, 562, 562, 562, 562, - - 562, 562, 562, 562, 562, 562, 561, 561, 561, 561, - 561, 561, 561, 561, 561, 561, 561, 561, 561, 561, - 561, 561, 561, 561, 561, 561, 561, 561, 562, 562, - 562, 562, 562, 562, 562, 562, 562, 562, 562, 562, - 562, 562, 562, 562, 562, 562, 562, 562, 562, 562, - 562, 561, 561, 561, 561, 561, 561, 561, 561, 561, - 561, 561, 561, 561, 561, 561, 561, 561, 561, 561, - 561, 561, 561, 562, 562, 562, 562, 562, 562, 562, - 562, 562, 562, 562, 562, 562, 562, 562, 562, 562, - 562, 562, 562, 562, 561, 561, 561, 561, 561, 561, - - 561, 561, 561, 561, 561, 561, 561, 561, 561, 561, - 561, 561, 561, 562, 562, 562, 562, 562, 562, 562, - 562, 562, 562, 562, 562, 562, 562, 562, 562, 562, - 562, 562, 561, 561, 561, 561, 561, 561, 561, 561, - 561, 561, 561, 561, 561, 561, 561, 561, 561, 561, - 561, 562, 562, 562, 562, 562, 562, 562, 562, 562, - 562, 562, 562, 562, 562, 562, 562, 562, 561, 561, - 561, 561, 561, 561, 561, 561, 561, 561, 561, 561, - 561, 561, 561, 561, 561, 561, 562, 562, 562, 562, - 562, 562, 562, 562, 562, 562, 562, 562, 562, 562, - - 562, 562, 562, 562, 561, 561, 561, 561, 561, 561, - 561, 561, 561, 561, 561, 561, 561, 561, 562, 562, - 562, 562, 562, 562, 562, 562, 562, 562, 562, 562, - 562, 562, 562, 562, 562, 561, 561, 561, 561, 561, - 561, 561, 561, 561, 562, 562, 562, 562, 562, 562, - 562, 562, 562, 562, 562, 562, 562, 562, 562, 561, - 561, 561, 561, 561, 561, 562, 562, 562, 562, 562, - 562, 562, 562, 562, 562, 562, 562, 562, 562, 561, - 561, 561, 561, 561, 562, 562, 562, 562, 562, 562, - 562, 562, 562, 562, 562, 562, 562, 562, 561, 561, - - 561, 561, 562, 562, 562, 562, 562, 562, 562, 562, - 562, 562, 562, 562, 562, 561, 562, 562, 562, 562, - 562, 562, 562, 562, 561, 562, 562, 562, 562, 562, - 562, 562, 562, 562, 562, 562, 562, 562, 562, 562, - 562, 562, 562, 562, 562, 562, 562, 562, 562, 562, - 562, 562, 562, 562, 562, 562, 562, 0, 558, 558, - 558, 558, 558, 558 - } ; - -static const flex_int16_t yy_nxt[726] = - { 0, - 8, 9, 10, 9, 11, 12, 13, 14, 14, 15, - 16, 14, 14, 17, 18, 18, 19, 20, 14, 14, - 14, 21, 14, 14, 14, 14, 14, 22, 14, 23, - 14, 14, 8, 24, 25, 14, 26, 27, 28, 29, - 30, 14, 14, 14, 31, 14, 14, 14, 32, 33, - 34, 35, 14, 14, 36, 14, 14, 37, 39, 40, - 41, 52, 42, 39, 40, 41, 95, 42, 45, 46, - 47, 45, 46, 47, 50, 50, 50, 50, 50, 50, - 84, 53, 54, 55, 55, 92, 94, 94, 56, 43, - 57, 57, 57, 85, 43, 557, 88, 104, 86, 48, - - 89, 105, 48, 56, 58, 59, 59, 59, 50, 50, - 50, 96, 93, 54, 54, 54, 96, 97, 98, 98, - 98, 99, 100, 100, 49, 101, 101, 49, 61, 102, - 114, 62, 63, 64, 115, 106, 65, 103, 66, 556, - 67, 107, 68, 69, 70, 71, 56, 72, 57, 57, - 57, 56, 58, 59, 59, 59, 111, 116, 119, 555, - 126, 117, 120, 127, 94, 94, 140, 141, 141, 112, - 142, 142, 96, 97, 98, 98, 98, 99, 100, 100, - 100, 100, 100, 143, 143, 143, 149, 156, 159, 150, - 173, 174, 157, 205, 160, 140, 141, 141, 141, 141, - - 141, 183, 183, 183, 143, 143, 143, 216, 206, 223, - 301, 224, 312, 335, 225, 217, 183, 183, 183, 396, - 218, 219, 302, 313, 336, 220, 221, 337, 554, 370, - 397, 338, 371, 398, 553, 552, 551, 399, 550, 549, - 548, 547, 546, 372, 38, 38, 38, 38, 38, 44, - 44, 44, 44, 44, 51, 51, 51, 60, 545, 60, - 73, 544, 73, 73, 73, 543, 542, 541, 540, 539, - 538, 537, 536, 535, 534, 533, 532, 531, 530, 529, - 528, 527, 526, 525, 524, 523, 522, 521, 520, 519, - 518, 517, 516, 515, 514, 513, 512, 511, 510, 509, - - 508, 507, 506, 505, 504, 503, 502, 501, 500, 499, - 498, 497, 496, 495, 494, 493, 492, 491, 490, 489, - 488, 487, 486, 485, 484, 483, 482, 481, 480, 479, - 478, 477, 476, 475, 474, 473, 472, 471, 470, 469, - 468, 467, 466, 465, 464, 463, 462, 461, 460, 459, - 458, 457, 456, 455, 454, 453, 452, 451, 450, 449, - 448, 447, 446, 445, 444, 443, 442, 441, 440, 439, - 438, 437, 436, 435, 434, 433, 432, 431, 430, 429, - 428, 427, 426, 425, 424, 423, 422, 421, 420, 419, - 418, 417, 416, 415, 414, 413, 412, 411, 410, 409, - - 408, 407, 406, 405, 404, 403, 402, 401, 400, 395, - 394, 393, 392, 391, 390, 389, 388, 387, 386, 385, - 384, 383, 382, 381, 380, 379, 378, 377, 376, 375, - 374, 373, 369, 368, 367, 366, 365, 364, 363, 362, - 361, 360, 359, 358, 357, 356, 355, 354, 353, 352, - 351, 350, 349, 348, 347, 346, 345, 344, 343, 342, - 341, 340, 339, 334, 333, 332, 331, 330, 329, 328, - 327, 326, 325, 324, 323, 322, 321, 320, 319, 318, - 317, 316, 315, 314, 311, 310, 309, 308, 307, 306, - 305, 304, 303, 300, 299, 298, 297, 296, 295, 294, - - 293, 292, 291, 290, 289, 288, 287, 286, 285, 284, - 283, 282, 281, 280, 279, 278, 277, 276, 275, 274, - 273, 272, 271, 270, 269, 268, 267, 266, 265, 264, - 263, 262, 261, 260, 259, 258, 257, 256, 255, 254, - 253, 252, 251, 250, 249, 248, 247, 246, 245, 244, - 243, 242, 241, 240, 239, 238, 237, 236, 235, 234, - 233, 232, 231, 230, 229, 228, 227, 226, 222, 215, - 214, 213, 212, 211, 210, 209, 208, 207, 204, 203, - 202, 201, 200, 199, 198, 197, 196, 195, 194, 193, - 192, 191, 190, 189, 188, 187, 186, 185, 184, 182, - - 181, 180, 179, 178, 177, 176, 175, 172, 171, 170, - 169, 168, 167, 166, 165, 164, 163, 162, 161, 158, - 155, 154, 153, 152, 151, 148, 147, 146, 145, 144, - 139, 138, 137, 136, 135, 134, 133, 132, 131, 130, - 129, 128, 125, 124, 123, 122, 121, 118, 113, 110, - 109, 108, 91, 90, 87, 83, 82, 81, 80, 79, - 78, 77, 76, 75, 74, 558, 7, 558, 558, 558, - 558, 558, 558, 558, 558, 558, 558, 558, 558, 558, - 558, 558, 558, 558, 558, 558, 558, 558, 558, 558, - 558, 558, 558, 558, 558, 558, 558, 558, 558, 558, - - 558, 558, 558, 558, 558, 558, 558, 558, 558, 558, - 558, 558, 558, 558, 558, 558, 558, 558, 558, 558, - 558, 558, 558, 558, 558 - } ; - -static const flex_int16_t yy_chk[726] = - { 0, - 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, - 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, - 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, - 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, - 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, - 1, 1, 1, 1, 1, 1, 1, 1, 3, 3, - 3, 13, 3, 4, 4, 4, 564, 4, 5, 5, - 5, 6, 6, 6, 9, 9, 9, 10, 10, 10, - 32, 13, 16, 16, 16, 43, 52, 52, 17, 3, - 17, 17, 17, 32, 4, 556, 34, 62, 32, 5, - - 34, 62, 6, 18, 18, 18, 18, 18, 50, 50, - 50, 54, 43, 54, 54, 54, 55, 55, 55, 55, - 55, 56, 56, 56, 5, 58, 58, 6, 19, 61, - 69, 19, 19, 19, 69, 63, 19, 61, 19, 555, - 19, 63, 19, 19, 19, 19, 57, 19, 57, 57, - 57, 59, 59, 59, 59, 59, 67, 70, 72, 553, - 79, 70, 72, 79, 94, 94, 96, 96, 96, 67, - 97, 97, 98, 98, 98, 98, 98, 99, 99, 99, - 100, 100, 100, 101, 101, 101, 107, 113, 115, 107, - 128, 128, 113, 165, 115, 140, 140, 140, 141, 141, - - 141, 142, 142, 142, 143, 143, 143, 176, 165, 179, - 262, 179, 273, 299, 179, 176, 183, 183, 183, 362, - 176, 176, 262, 273, 299, 176, 176, 300, 552, 334, - 362, 300, 334, 362, 551, 550, 549, 362, 548, 545, - 544, 543, 542, 334, 559, 559, 559, 559, 559, 560, - 560, 560, 560, 560, 561, 561, 561, 562, 540, 562, - 563, 538, 563, 563, 563, 537, 536, 535, 534, 533, - 532, 531, 530, 527, 526, 524, 523, 522, 521, 520, - 519, 518, 517, 516, 515, 514, 512, 509, 508, 507, - 506, 504, 501, 498, 497, 496, 495, 494, 493, 492, - - 490, 489, 488, 487, 486, 485, 484, 483, 482, 481, - 479, 478, 477, 476, 475, 474, 473, 472, 471, 470, - 469, 468, 467, 466, 465, 464, 463, 462, 460, 459, - 458, 457, 455, 454, 453, 452, 451, 450, 449, 448, - 447, 446, 445, 443, 442, 441, 440, 438, 436, 435, - 434, 433, 432, 431, 430, 429, 428, 427, 426, 425, - 423, 422, 421, 419, 418, 414, 412, 411, 410, 409, - 407, 406, 405, 403, 402, 401, 400, 399, 398, 397, - 396, 395, 394, 393, 392, 391, 390, 389, 388, 387, - 386, 385, 384, 382, 380, 378, 377, 376, 375, 374, - - 373, 372, 371, 370, 368, 366, 365, 364, 363, 361, - 359, 358, 357, 356, 355, 354, 353, 352, 351, 350, - 348, 347, 345, 344, 343, 342, 341, 340, 338, 337, - 336, 335, 333, 331, 330, 329, 328, 327, 326, 325, - 324, 323, 322, 321, 320, 319, 318, 317, 316, 314, - 313, 312, 311, 310, 309, 308, 307, 306, 305, 304, - 303, 302, 301, 298, 297, 294, 293, 291, 289, 288, - 287, 286, 285, 284, 283, 282, 281, 280, 279, 278, - 277, 276, 275, 274, 271, 270, 269, 268, 267, 266, - 265, 264, 263, 261, 258, 257, 256, 253, 252, 251, - - 250, 249, 248, 247, 246, 245, 244, 243, 242, 241, - 238, 237, 236, 235, 234, 233, 232, 231, 230, 229, - 228, 227, 226, 225, 224, 223, 222, 221, 220, 219, - 218, 217, 216, 215, 214, 213, 212, 211, 210, 209, - 208, 207, 206, 205, 204, 203, 202, 201, 200, 199, - 198, 197, 196, 195, 194, 193, 192, 191, 190, 189, - 188, 187, 186, 185, 184, 182, 181, 180, 178, 175, - 173, 172, 171, 170, 169, 168, 167, 166, 164, 163, - 162, 161, 160, 159, 158, 157, 156, 155, 154, 153, - 152, 151, 150, 149, 148, 147, 146, 145, 144, 139, - - 138, 137, 136, 135, 134, 130, 129, 127, 126, 125, - 124, 123, 122, 121, 120, 119, 118, 117, 116, 114, - 112, 111, 110, 109, 108, 106, 105, 104, 103, 102, - 91, 90, 89, 88, 87, 86, 85, 84, 83, 82, - 81, 80, 78, 77, 76, 75, 74, 71, 68, 66, - 65, 64, 36, 35, 33, 31, 30, 29, 28, 27, - 26, 25, 23, 22, 21, 7, 558, 558, 558, 558, - 558, 558, 558, 558, 558, 558, 558, 558, 558, 558, - 558, 558, 558, 558, 558, 558, 558, 558, 558, 558, - 558, 558, 558, 558, 558, 558, 558, 558, 558, 558, - - 558, 558, 558, 558, 558, 558, 558, 558, 558, 558, - 558, 558, 558, 558, 558, 558, 558, 558, 558, 558, - 558, 558, 558, 558, 558 - } ; - -/* Table of booleans, true if rule could match eol. */ -static const flex_int32_t yy_rule_can_match_eol[92] = - { 0, -0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, - 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, - 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, - 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, - 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, }; - -/* The intent behind this definition is that it'll catch - * any uses of REJECT which flex missed. - */ -#define REJECT reject_used_but_not_detected -#define yymore() yymore_used_but_not_detected -#define YY_MORE_ADJ 0 -#define YY_RESTORE_YY_MORE_OFFSET -#line 1 "smt2new/smt2newlexer.ll" -/********************************************************************* -Author: Antti Hyvarinen - -OpenSMT2 -- Copyright (C) 2012 - 2014 Antti Hyvarinen - -Permission is hereby granted, free of charge, to any person obtaining a -copy of this software and associated documentation files (the -"Software"), to deal in the Software without restriction, including -without limitation the rights to use, copy, modify, merge, publish, -distribute, sublicense, and/or sell copies of the Software, and to -permit persons to whom the Software is furnished to do so, subject to -the following conditions: - -The above copyright notice and this permission notice shall be included -in all copies or substantial portions of the Software. - -THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS -OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF -MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND -NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE -LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION -OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION -WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. -*********************************************************************/ -#line 36 "smt2new/smt2newlexer.ll" - -#include -#include -#include -#include - -#include "smt2tokens.h" -#include "smt2newcontext.h" -#include "smt2newparser.hh" - -#define YY_EXTRA_TYPE Smt2newContext* -#define YY_USER_ACTION yyget_lloc(yyscanner)->first_line = yyget_lineno(yyscanner); -#line 1065 "smt2new/smt2newlexer.cc" - -#line 1067 "smt2new/smt2newlexer.cc" - -#define INITIAL 0 -#define STR 1 -#define PSYM 2 - -#ifndef YY_NO_UNISTD_H -/* Special case for "unistd.h", since it is non-ANSI. We include it way - * down here because we want the user's section 1 to have been scanned first. - * The user has a chance to override it with an option. - */ -#include -#endif - -#ifndef YY_EXTRA_TYPE -#define YY_EXTRA_TYPE void * -#endif - -/* Holds the entire state of the reentrant scanner. */ -struct yyguts_t - { - - /* User-defined. Not touched by flex. */ - YY_EXTRA_TYPE yyextra_r; - - /* The rest are the same as the globals declared in the non-reentrant scanner. */ - FILE *yyin_r, *yyout_r; - size_t yy_buffer_stack_top; /**< index of top of stack. */ - size_t yy_buffer_stack_max; /**< capacity of stack. */ - YY_BUFFER_STATE * yy_buffer_stack; /**< Stack as an array. */ - char yy_hold_char; - int yy_n_chars; - int yyleng_r; - char *yy_c_buf_p; - int yy_init; - int yy_start; - int yy_did_buffer_switch_on_eof; - int yy_start_stack_ptr; - int yy_start_stack_depth; - int *yy_start_stack; - yy_state_type yy_last_accepting_state; - char* yy_last_accepting_cpos; - - int yylineno_r; - int yy_flex_debug_r; - - char *yytext_r; - int yy_more_flag; - int yy_more_len; - - YYSTYPE * yylval_r; - - YYLTYPE * yylloc_r; - - }; /* end struct yyguts_t */ - -static int yy_init_globals ( yyscan_t yyscanner ); - - /* This must go here because YYSTYPE and YYLTYPE are included - * from bison output in section 1.*/ - # define yylval yyg->yylval_r - - # define yylloc yyg->yylloc_r - -int yylex_init (yyscan_t* scanner); - -int yylex_init_extra ( YY_EXTRA_TYPE user_defined, yyscan_t* scanner); - -/* Accessor methods to globals. - These are made visible to non-reentrant scanners for convenience. */ - -int yylex_destroy ( yyscan_t yyscanner ); - -int yyget_debug ( yyscan_t yyscanner ); - -void yyset_debug ( int debug_flag , yyscan_t yyscanner ); - -YY_EXTRA_TYPE yyget_extra ( yyscan_t yyscanner ); - -void yyset_extra ( YY_EXTRA_TYPE user_defined , yyscan_t yyscanner ); - -FILE *yyget_in ( yyscan_t yyscanner ); - -void yyset_in ( FILE * _in_str , yyscan_t yyscanner ); - -FILE *yyget_out ( yyscan_t yyscanner ); - -void yyset_out ( FILE * _out_str , yyscan_t yyscanner ); - - int yyget_leng ( yyscan_t yyscanner ); - -char *yyget_text ( yyscan_t yyscanner ); - -int yyget_lineno ( yyscan_t yyscanner ); - -void yyset_lineno ( int _line_number , yyscan_t yyscanner ); - -int yyget_column ( yyscan_t yyscanner ); - -void yyset_column ( int _column_no , yyscan_t yyscanner ); - -YYSTYPE * yyget_lval ( yyscan_t yyscanner ); - -void yyset_lval ( YYSTYPE * yylval_param , yyscan_t yyscanner ); - - YYLTYPE *yyget_lloc ( yyscan_t yyscanner ); - - void yyset_lloc ( YYLTYPE * yylloc_param , yyscan_t yyscanner ); - -/* Macros after this point can all be overridden by user definitions in - * section 1. - */ - -#ifndef YY_SKIP_YYWRAP -#ifdef __cplusplus -extern "C" int yywrap ( yyscan_t yyscanner ); -#else -extern int yywrap ( yyscan_t yyscanner ); -#endif -#endif - -#ifndef YY_NO_UNPUT - - static void yyunput ( int c, char *buf_ptr , yyscan_t yyscanner); - -#endif - -#ifndef yytext_ptr -static void yy_flex_strncpy ( char *, const char *, int , yyscan_t yyscanner); -#endif - -#ifdef YY_NEED_STRLEN -static int yy_flex_strlen ( const char * , yyscan_t yyscanner); -#endif - -#ifndef YY_NO_INPUT -#ifdef __cplusplus -static int yyinput ( yyscan_t yyscanner ); -#else -static int input ( yyscan_t yyscanner ); -#endif - -#endif - - static void yy_push_state ( int _new_state , yyscan_t yyscanner); - - static void yy_pop_state ( yyscan_t yyscanner ); - - static int yy_top_state ( yyscan_t yyscanner ); - -/* Amount of stuff to slurp up with each read. */ -#ifndef YY_READ_BUF_SIZE -#ifdef __ia64__ -/* On IA-64, the buffer size is 16k, not 8k */ -#define YY_READ_BUF_SIZE 16384 -#else -#define YY_READ_BUF_SIZE 8192 -#endif /* __ia64__ */ -#endif - -/* Copy whatever the last rule matched to the standard output. */ -#ifndef ECHO -/* This used to be an fputs(), but since the string might contain NUL's, - * we now use fwrite(). - */ -#define ECHO do { if (fwrite( yytext, (size_t) yyleng, 1, yyout )) {} } while (0) -#endif - -/* Gets input and stuffs it into "buf". number of characters read, or YY_NULL, - * is returned in "result". - */ -#ifndef YY_INPUT -#define YY_INPUT(buf,result,max_size) \ - if ( YY_CURRENT_BUFFER_LVALUE->yy_is_interactive ) \ - { \ - int c = '*'; \ - int n; \ - for ( n = 0; n < max_size && \ - (c = getc( yyin )) != EOF && c != '\n'; ++n ) \ - buf[n] = (char) c; \ - if ( c == '\n' ) \ - buf[n++] = (char) c; \ - if ( c == EOF && ferror( yyin ) ) \ - YY_FATAL_ERROR( "input in flex scanner failed" ); \ - result = n; \ - } \ - else \ - { \ - errno=0; \ - while ( (result = (int) fread(buf, 1, (yy_size_t) max_size, yyin)) == 0 && ferror(yyin)) \ - { \ - if( errno != EINTR) \ - { \ - YY_FATAL_ERROR( "input in flex scanner failed" ); \ - break; \ - } \ - errno=0; \ - clearerr(yyin); \ - } \ - }\ -\ - -#endif - -/* No semi-colon after return; correct usage is to write "yyterminate();" - - * we don't want an extra ';' after the "return" because that will cause - * some compilers to complain about unreachable statements. - */ -#ifndef yyterminate -#define yyterminate() return YY_NULL -#endif - -/* Number of entries by which start-condition stack grows. */ -#ifndef YY_START_STACK_INCR -#define YY_START_STACK_INCR 25 -#endif - -/* Report a fatal error. */ -#ifndef YY_FATAL_ERROR -#define YY_FATAL_ERROR(msg) yy_fatal_error( msg , yyscanner) -#endif - -/* end tables serialization structures and prototypes */ - -/* Default declaration of generated scanner - a define so the user can - * easily add parameters. - */ -#ifndef YY_DECL -#define YY_DECL_IS_OURS 1 - -extern int yylex \ - (YYSTYPE * yylval_param, YYLTYPE * yylloc_param , yyscan_t yyscanner); - -#define YY_DECL int yylex \ - (YYSTYPE * yylval_param, YYLTYPE * yylloc_param , yyscan_t yyscanner) -#endif /* !YY_DECL */ - -/* Code executed at the beginning of each rule, after yytext and yyleng - * have been set up. - */ -#ifndef YY_USER_ACTION -#define YY_USER_ACTION -#endif - -/* Code executed at the end of each rule. */ -#ifndef YY_BREAK -#define YY_BREAK /*LINTED*/break; -#endif - -#define YY_RULE_SETUP \ - YY_USER_ACTION - -/** The main scanner function which does all the work. - */ -YY_DECL -{ - yy_state_type yy_current_state; - char *yy_cp, *yy_bp; - int yy_act; - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; - - yylval = yylval_param; - - yylloc = yylloc_param; - - if ( !yyg->yy_init ) - { - yyg->yy_init = 1; - -#ifdef YY_USER_INIT - YY_USER_INIT; -#endif - - if ( ! yyg->yy_start ) - yyg->yy_start = 1; /* first start state */ - - if ( ! yyin ) - yyin = stdin; - - if ( ! yyout ) - yyout = stdout; - - if ( ! YY_CURRENT_BUFFER ) { - yyensure_buffer_stack (yyscanner); - YY_CURRENT_BUFFER_LVALUE = - yy_create_buffer( yyin, YY_BUF_SIZE , yyscanner); - } - - yy_load_buffer_state( yyscanner ); - } - - { -#line 53 "smt2new/smt2newlexer.ll" - - -#line 1362 "smt2new/smt2newlexer.cc" - - while ( /*CONSTCOND*/1 ) /* loops until end-of-file is reached */ - { - yy_cp = yyg->yy_c_buf_p; - - /* Support of yytext. */ - *yy_cp = yyg->yy_hold_char; - - /* yy_bp points to the position in yy_ch_buf of the start of - * the current run. - */ - yy_bp = yy_cp; - - yy_current_state = yyg->yy_start; -yy_match: - do - { - YY_CHAR yy_c = yy_ec[YY_SC_TO_UI(*yy_cp)] ; - if ( yy_accept[yy_current_state] ) - { - yyg->yy_last_accepting_state = yy_current_state; - yyg->yy_last_accepting_cpos = yy_cp; - } - while ( yy_chk[yy_base[yy_current_state] + yy_c] != yy_current_state ) - { - yy_current_state = (int) yy_def[yy_current_state]; - if ( yy_current_state >= 559 ) - yy_c = yy_meta[yy_c]; - } - yy_current_state = yy_nxt[yy_base[yy_current_state] + yy_c]; - ++yy_cp; - } - while ( yy_base[yy_current_state] != 667 ); - -yy_find_action: - yy_act = yy_accept[yy_current_state]; - if ( yy_act == 0 ) - { /* have to back up */ - yy_cp = yyg->yy_last_accepting_cpos; - yy_current_state = yyg->yy_last_accepting_state; - yy_act = yy_accept[yy_current_state]; - } - - YY_DO_BEFORE_ACTION; - - if ( yy_act != YY_END_OF_BUFFER && yy_rule_can_match_eol[yy_act] ) - { - int yyl; - for ( yyl = 0; yyl < yyleng; ++yyl ) - if ( yytext[yyl] == '\n' ) - - do{ yylineno++; - yycolumn=0; - }while(0) -; - } - -do_action: /* This label is used only to access EOF actions. */ - - switch ( yy_act ) - { /* beginning of action switch */ - case 0: /* must back up */ - /* undo the effects of YY_DO_BEFORE_ACTION */ - *yy_cp = yyg->yy_hold_char; - yy_cp = yyg->yy_last_accepting_cpos; - yy_current_state = yyg->yy_last_accepting_state; - goto yy_find_action; - -case 1: -YY_RULE_SETUP -#line 55 "smt2new/smt2newlexer.ll" -// Eat comments - YY_BREAK -case 2: -/* rule 2 can match eol */ -YY_RULE_SETUP -#line 56 "smt2new/smt2newlexer.ll" -// Eat spaces - YY_BREAK -case 3: -YY_RULE_SETUP -#line 58 "smt2new/smt2newlexer.ll" -{ return *yyget_text(yyscanner); } - YY_BREAK -case 4: -YY_RULE_SETUP -#line 59 "smt2new/smt2newlexer.ll" -{ return *yyget_text(yyscanner); } - YY_BREAK -case 5: -YY_RULE_SETUP -#line 60 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->tok = { t_as }; return TK_AS; } - YY_BREAK -case 6: -YY_RULE_SETUP -#line 62 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->tok = { t_DECIMAL }; return TK_DECIMAL; } - YY_BREAK -case 7: -YY_RULE_SETUP -#line 63 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->tok = { t_exists }; return TK_EXISTS; } - YY_BREAK -case 8: -YY_RULE_SETUP -#line 64 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->tok = { t_forall }; return TK_FORALL; } - YY_BREAK -case 9: -YY_RULE_SETUP -#line 65 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->tok = { t_let }; return TK_LET; } - YY_BREAK -case 10: -YY_RULE_SETUP -#line 66 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->tok = { t_NUMERAL }; return TK_NUMERAL; } - YY_BREAK -case 11: -YY_RULE_SETUP -#line 67 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->tok = { t_par }; return TK_PAR; } - YY_BREAK -case 12: -YY_RULE_SETUP -#line 68 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->tok = { t_STRING}; return TK_STRING; } - YY_BREAK -case 13: -YY_RULE_SETUP -#line 70 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->tok = { t_assert }; return TK_ASSERT; } - YY_BREAK -case 14: -YY_RULE_SETUP -#line 71 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->tok = { t_checksat }; return TK_CHECKSAT; } - YY_BREAK -case 15: -YY_RULE_SETUP -#line 72 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->tok = { t_declaresort }; return TK_DECLARESORT; } - YY_BREAK -case 16: -YY_RULE_SETUP -#line 73 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->tok = { t_declarefun }; return TK_DECLAREFUN; } - YY_BREAK -case 17: -YY_RULE_SETUP -#line 74 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->tok = { t_declareconst} ; return TK_DECLARECONST; } - YY_BREAK -case 18: -YY_RULE_SETUP -#line 75 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->tok = { t_definesort }; return TK_DEFINESORT; } - YY_BREAK -case 19: -YY_RULE_SETUP -#line 76 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->tok = { t_definefun }; return TK_DEFINEFUN; } - YY_BREAK -case 20: -YY_RULE_SETUP -#line 77 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->tok = { t_exit }; return TK_EXIT; } - YY_BREAK -case 21: -YY_RULE_SETUP -#line 78 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->tok = { t_getassertions }; return TK_GETASSERTIONS; } - YY_BREAK -case 22: -YY_RULE_SETUP -#line 79 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->tok = { t_getassignment }; return TK_GETASSIGNMENT; } - YY_BREAK -case 23: -YY_RULE_SETUP -#line 80 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->tok = { t_getinfo }; return TK_GETINFO; } - YY_BREAK -case 24: -YY_RULE_SETUP -#line 81 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->tok = { t_getoption }; return TK_GETOPTION; } - YY_BREAK -case 25: -YY_RULE_SETUP -#line 82 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->tok = { t_getproof }; return TK_GETPROOF; } - YY_BREAK -case 26: -YY_RULE_SETUP -#line 83 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->tok = { t_getunsatcore }; return TK_GETUNSATCORE; } - YY_BREAK -case 27: -YY_RULE_SETUP -#line 84 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->tok = { t_getvalue }; return TK_GETVALUE; } - YY_BREAK -case 28: -YY_RULE_SETUP -#line 85 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->tok = { t_pop }; return TK_POP; } - YY_BREAK -case 29: -YY_RULE_SETUP -#line 86 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->tok = { t_push }; return TK_PUSH; } - YY_BREAK -case 30: -YY_RULE_SETUP -#line 87 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->tok = { t_setlogic }; return TK_SETLOGIC; } - YY_BREAK -case 31: -YY_RULE_SETUP -#line 88 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->tok = { t_setinfo }; return TK_SETINFO; } - YY_BREAK -case 32: -YY_RULE_SETUP -#line 89 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->tok = { t_setoption }; return TK_SETOPTION; } - YY_BREAK -case 33: -YY_RULE_SETUP -#line 90 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->tok = { t_getinterpolants }; return TK_GETITPS; } - YY_BREAK -case 34: -YY_RULE_SETUP -#line 91 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->tok = { t_theory }; return TK_THEORY; } - YY_BREAK -case 35: -YY_RULE_SETUP -#line 92 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->tok = { t_writestate }; return TK_WRSTATE; } - YY_BREAK -case 36: -YY_RULE_SETUP -#line 93 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->tok = { t_readstate }; return TK_RDSTATE; } - YY_BREAK -case 37: -YY_RULE_SETUP -#line 94 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->tok = { t_simplify }; return TK_SIMPLIFY; } - YY_BREAK -case 38: -YY_RULE_SETUP -#line 95 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->tok = { t_writefuns }; return TK_WRFUNS; } - YY_BREAK -case 39: -YY_RULE_SETUP -#line 97 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_SORTS; } - YY_BREAK -case 40: -YY_RULE_SETUP -#line 98 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_FUNS; } - YY_BREAK -case 41: -YY_RULE_SETUP -#line 99 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_SORTSDESCRIPTION; } - YY_BREAK -case 42: -YY_RULE_SETUP -#line 100 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_FUNSDESCRIPTION; } - YY_BREAK -case 43: -YY_RULE_SETUP -#line 101 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_DEFINITION; } - YY_BREAK -case 44: -YY_RULE_SETUP -#line 102 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_VALUES; } - YY_BREAK -case 45: -YY_RULE_SETUP -#line 103 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_NOTES; } - YY_BREAK -case 46: -YY_RULE_SETUP -#line 104 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_THEORIES; } - YY_BREAK -case 47: -YY_RULE_SETUP -#line 105 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_LANGUAGE; } - YY_BREAK -case 48: -YY_RULE_SETUP -#line 106 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_EXTENSIONS; } - YY_BREAK -case 49: -YY_RULE_SETUP -#line 107 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_PRINTSUCCESS; } - YY_BREAK -case 50: -YY_RULE_SETUP -#line 108 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_EXPANDDEFINITIONS; } - YY_BREAK -case 51: -YY_RULE_SETUP -#line 109 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_INTERACTIVEMODE; } - YY_BREAK -case 52: -YY_RULE_SETUP -#line 110 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_PRODUCEPROOFS; } - YY_BREAK -case 53: -YY_RULE_SETUP -#line 111 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_PRODUCEUNSATCORES; } - YY_BREAK -case 54: -YY_RULE_SETUP -#line 112 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_PRODUCEMODELS; } - YY_BREAK -case 55: -YY_RULE_SETUP -#line 113 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_PRODUCEASSIGNMENTS; } - YY_BREAK -case 56: -YY_RULE_SETUP -#line 114 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_REGULAROUTPUTCHANNEL; } - YY_BREAK -case 57: -YY_RULE_SETUP -#line 115 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_DIAGNOSTICOUTPUTCHANNEL; } - YY_BREAK -case 58: -YY_RULE_SETUP -#line 116 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_RANDOMSEED; } - YY_BREAK -case 59: -YY_RULE_SETUP -#line 117 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_VERBOSITY; } - YY_BREAK -case 60: -YY_RULE_SETUP -#line 118 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_ERRORBEHAVIOR; } - YY_BREAK -case 61: -YY_RULE_SETUP -#line 119 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_NAME; } - YY_BREAK -case 62: -YY_RULE_SETUP -#line 120 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_NAMED; } - YY_BREAK -case 63: -YY_RULE_SETUP -#line 121 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_AUTHORS; } - YY_BREAK -case 64: -YY_RULE_SETUP -#line 122 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_VERSION; } - YY_BREAK -case 65: -YY_RULE_SETUP -#line 123 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_STATUS; } - YY_BREAK -case 66: -YY_RULE_SETUP -#line 124 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_REASONUNKNOWN; } - YY_BREAK -case 67: -YY_RULE_SETUP -#line 125 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return KW_ALLSTATISTICS; } - YY_BREAK -case 68: -YY_RULE_SETUP -#line 128 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return TK_NUM; } - YY_BREAK -case 69: -YY_RULE_SETUP -#line 129 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return TK_DEC; } - YY_BREAK -case 70: -YY_RULE_SETUP -#line 130 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return TK_HEX; } - YY_BREAK -case 71: -YY_RULE_SETUP -#line 131 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return TK_BIN; } - YY_BREAK -case 72: -YY_RULE_SETUP -#line 133 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return TK_SYM; } - YY_BREAK -case 73: -YY_RULE_SETUP -#line 134 "smt2new/smt2newlexer.ll" -{ yyget_lval(yyscanner)->str = strdup( yyget_text(yyscanner) ); return TK_KEY; } - YY_BREAK -case 74: -YY_RULE_SETUP -#line 136 "smt2new/smt2newlexer.ll" -{ return *yyget_text(yyscanner); } - YY_BREAK -case 75: -YY_RULE_SETUP -#line 138 "smt2new/smt2newlexer.ll" -{ yy_push_state(STR, yyscanner); } - YY_BREAK - -case 76: -YY_RULE_SETUP -#line 141 "smt2new/smt2newlexer.ll" -{ yyextra->insertBuf(' '); } - YY_BREAK -case 77: -YY_RULE_SETUP -#line 142 "smt2new/smt2newlexer.ll" -{ yyextra->insertBuf('\t'); } - YY_BREAK -case 78: -/* rule 78 can match eol */ -YY_RULE_SETUP -#line 143 "smt2new/smt2newlexer.ll" -{ yyextra->insertBuf('\n'); } - YY_BREAK -case 79: -YY_RULE_SETUP -#line 144 "smt2new/smt2newlexer.ll" -{ yyextra->insertBuf('"'); } - YY_BREAK -case 80: -YY_RULE_SETUP -#line 145 "smt2new/smt2newlexer.ll" -{ yyextra->insertBuf('\\'); } - YY_BREAK -case 81: -YY_RULE_SETUP -#line 146 "smt2new/smt2newlexer.ll" -{ yyextra->insertBuf(yyget_text(yyscanner)[0]); } - YY_BREAK -case 82: -YY_RULE_SETUP -#line 147 "smt2new/smt2newlexer.ll" -{ yylval->str = strdup(yyextra->getBuf()); yyextra->clearBuf(); - yy_pop_state(yyscanner); return TK_STR; } - YY_BREAK - -case 83: -YY_RULE_SETUP -#line 151 "smt2new/smt2newlexer.ll" -{ yy_push_state(PSYM, yyscanner); } - YY_BREAK - -case 84: -YY_RULE_SETUP -#line 154 "smt2new/smt2newlexer.ll" -{ yyextra->insertBuf(' '); } - YY_BREAK -case 85: -YY_RULE_SETUP -#line 155 "smt2new/smt2newlexer.ll" -{ yyextra->insertBuf('\t'); } - YY_BREAK -case 86: -/* rule 86 can match eol */ -YY_RULE_SETUP -#line 156 "smt2new/smt2newlexer.ll" -{ yyextra->insertBuf('\n'); } - YY_BREAK -case 87: -YY_RULE_SETUP -#line 157 "smt2new/smt2newlexer.ll" -{ yyextra->insertBuf(yyget_text(yyscanner)[0]); } - YY_BREAK -case 88: -YY_RULE_SETUP -#line 158 "smt2new/smt2newlexer.ll" -{ yylval->str = strdup(yyextra->getBuf()); yyextra->clearBuf(); - yy_pop_state(yyscanner); return TK_SYM; } - YY_BREAK -case 89: -YY_RULE_SETUP -#line 160 "smt2new/smt2newlexer.ll" -{ printf("Syntax error at line %d near %s, \\ not allowed inside | ... |\n", yyget_lineno(yyscanner), yyget_text(yyscanner)); exit(1); } - YY_BREAK - -case 90: -YY_RULE_SETUP -#line 163 "smt2new/smt2newlexer.ll" -{ printf( "Syntax error at line %d near %s\n", yyget_lineno(yyscanner), yyget_text(yyscanner) ); exit( 1 ); } - YY_BREAK -case 91: -YY_RULE_SETUP -#line 165 "smt2new/smt2newlexer.ll" -ECHO; - YY_BREAK -#line 1895 "smt2new/smt2newlexer.cc" -case YY_STATE_EOF(INITIAL): -case YY_STATE_EOF(STR): -case YY_STATE_EOF(PSYM): - yyterminate(); - - case YY_END_OF_BUFFER: - { - /* Amount of text matched not including the EOB char. */ - int yy_amount_of_matched_text = (int) (yy_cp - yyg->yytext_ptr) - 1; - - /* Undo the effects of YY_DO_BEFORE_ACTION. */ - *yy_cp = yyg->yy_hold_char; - YY_RESTORE_YY_MORE_OFFSET - - if ( YY_CURRENT_BUFFER_LVALUE->yy_buffer_status == YY_BUFFER_NEW ) - { - /* We're scanning a new file or input source. It's - * possible that this happened because the user - * just pointed yyin at a new source and called - * yylex(). If so, then we have to assure - * consistency between YY_CURRENT_BUFFER and our - * globals. Here is the right place to do so, because - * this is the first action (other than possibly a - * back-up) that will match for the new input source. - */ - yyg->yy_n_chars = YY_CURRENT_BUFFER_LVALUE->yy_n_chars; - YY_CURRENT_BUFFER_LVALUE->yy_input_file = yyin; - YY_CURRENT_BUFFER_LVALUE->yy_buffer_status = YY_BUFFER_NORMAL; - } - - /* Note that here we test for yy_c_buf_p "<=" to the position - * of the first EOB in the buffer, since yy_c_buf_p will - * already have been incremented past the NUL character - * (since all states make transitions on EOB to the - * end-of-buffer state). Contrast this with the test - * in input(). - */ - if ( yyg->yy_c_buf_p <= &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[yyg->yy_n_chars] ) - { /* This was really a NUL. */ - yy_state_type yy_next_state; - - yyg->yy_c_buf_p = yyg->yytext_ptr + yy_amount_of_matched_text; - - yy_current_state = yy_get_previous_state( yyscanner ); - - /* Okay, we're now positioned to make the NUL - * transition. We couldn't have - * yy_get_previous_state() go ahead and do it - * for us because it doesn't know how to deal - * with the possibility of jamming (and we don't - * want to build jamming into it because then it - * will run more slowly). - */ - - yy_next_state = yy_try_NUL_trans( yy_current_state , yyscanner); - - yy_bp = yyg->yytext_ptr + YY_MORE_ADJ; - - if ( yy_next_state ) - { - /* Consume the NUL. */ - yy_cp = ++yyg->yy_c_buf_p; - yy_current_state = yy_next_state; - goto yy_match; - } - - else - { - yy_cp = yyg->yy_c_buf_p; - goto yy_find_action; - } - } - - else switch ( yy_get_next_buffer( yyscanner ) ) - { - case EOB_ACT_END_OF_FILE: - { - yyg->yy_did_buffer_switch_on_eof = 0; - - if ( yywrap( yyscanner ) ) - { - /* Note: because we've taken care in - * yy_get_next_buffer() to have set up - * yytext, we can now set up - * yy_c_buf_p so that if some total - * hoser (like flex itself) wants to - * call the scanner after we return the - * YY_NULL, it'll still work - another - * YY_NULL will get returned. - */ - yyg->yy_c_buf_p = yyg->yytext_ptr + YY_MORE_ADJ; - - yy_act = YY_STATE_EOF(YY_START); - goto do_action; - } - - else - { - if ( ! yyg->yy_did_buffer_switch_on_eof ) - YY_NEW_FILE; - } - break; - } - - case EOB_ACT_CONTINUE_SCAN: - yyg->yy_c_buf_p = - yyg->yytext_ptr + yy_amount_of_matched_text; - - yy_current_state = yy_get_previous_state( yyscanner ); - - yy_cp = yyg->yy_c_buf_p; - yy_bp = yyg->yytext_ptr + YY_MORE_ADJ; - goto yy_match; - - case EOB_ACT_LAST_MATCH: - yyg->yy_c_buf_p = - &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[yyg->yy_n_chars]; - - yy_current_state = yy_get_previous_state( yyscanner ); - - yy_cp = yyg->yy_c_buf_p; - yy_bp = yyg->yytext_ptr + YY_MORE_ADJ; - goto yy_find_action; - } - break; - } - - default: - YY_FATAL_ERROR( - "fatal flex scanner internal error--no action found" ); - } /* end of action switch */ - } /* end of scanning one token */ - } /* end of user's declarations */ -} /* end of yylex */ - -/* yy_get_next_buffer - try to read in a new buffer - * - * Returns a code representing an action: - * EOB_ACT_LAST_MATCH - - * EOB_ACT_CONTINUE_SCAN - continue scanning from current position - * EOB_ACT_END_OF_FILE - end of file - */ -static int yy_get_next_buffer (yyscan_t yyscanner) -{ - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; - char *dest = YY_CURRENT_BUFFER_LVALUE->yy_ch_buf; - char *source = yyg->yytext_ptr; - int number_to_move, i; - int ret_val; - - if ( yyg->yy_c_buf_p > &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[yyg->yy_n_chars + 1] ) - YY_FATAL_ERROR( - "fatal flex scanner internal error--end of buffer missed" ); - - if ( YY_CURRENT_BUFFER_LVALUE->yy_fill_buffer == 0 ) - { /* Don't try to fill the buffer, so this is an EOF. */ - if ( yyg->yy_c_buf_p - yyg->yytext_ptr - YY_MORE_ADJ == 1 ) - { - /* We matched a single character, the EOB, so - * treat this as a final EOF. - */ - return EOB_ACT_END_OF_FILE; - } - - else - { - /* We matched some text prior to the EOB, first - * process it. - */ - return EOB_ACT_LAST_MATCH; - } - } - - /* Try to read more data. */ - - /* First move last chars to start of buffer. */ - number_to_move = (int) (yyg->yy_c_buf_p - yyg->yytext_ptr - 1); - - for ( i = 0; i < number_to_move; ++i ) - *(dest++) = *(source++); - - if ( YY_CURRENT_BUFFER_LVALUE->yy_buffer_status == YY_BUFFER_EOF_PENDING ) - /* don't do the read, it's not guaranteed to return an EOF, - * just force an EOF - */ - YY_CURRENT_BUFFER_LVALUE->yy_n_chars = yyg->yy_n_chars = 0; - - else - { - int num_to_read = - YY_CURRENT_BUFFER_LVALUE->yy_buf_size - number_to_move - 1; - - while ( num_to_read <= 0 ) - { /* Not enough room in the buffer - grow it. */ - - /* just a shorter name for the current buffer */ - YY_BUFFER_STATE b = YY_CURRENT_BUFFER_LVALUE; - - int yy_c_buf_p_offset = - (int) (yyg->yy_c_buf_p - b->yy_ch_buf); - - if ( b->yy_is_our_buffer ) - { - int new_size = b->yy_buf_size * 2; - - if ( new_size <= 0 ) - b->yy_buf_size += b->yy_buf_size / 8; - else - b->yy_buf_size *= 2; - - b->yy_ch_buf = (char *) - /* Include room in for 2 EOB chars. */ - yyrealloc( (void *) b->yy_ch_buf, - (yy_size_t) (b->yy_buf_size + 2) , yyscanner ); - } - else - /* Can't grow it, we don't own it. */ - b->yy_ch_buf = NULL; - - if ( ! b->yy_ch_buf ) - YY_FATAL_ERROR( - "fatal error - scanner input buffer overflow" ); - - yyg->yy_c_buf_p = &b->yy_ch_buf[yy_c_buf_p_offset]; - - num_to_read = YY_CURRENT_BUFFER_LVALUE->yy_buf_size - - number_to_move - 1; - - } - - if ( num_to_read > YY_READ_BUF_SIZE ) - num_to_read = YY_READ_BUF_SIZE; - - /* Read in more data. */ - YY_INPUT( (&YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[number_to_move]), - yyg->yy_n_chars, num_to_read ); - - YY_CURRENT_BUFFER_LVALUE->yy_n_chars = yyg->yy_n_chars; - } - - if ( yyg->yy_n_chars == 0 ) - { - if ( number_to_move == YY_MORE_ADJ ) - { - ret_val = EOB_ACT_END_OF_FILE; - yyrestart( yyin , yyscanner); - } - - else - { - ret_val = EOB_ACT_LAST_MATCH; - YY_CURRENT_BUFFER_LVALUE->yy_buffer_status = - YY_BUFFER_EOF_PENDING; - } - } - - else - ret_val = EOB_ACT_CONTINUE_SCAN; - - if ((yyg->yy_n_chars + number_to_move) > YY_CURRENT_BUFFER_LVALUE->yy_buf_size) { - /* Extend the array by 50%, plus the number we really need. */ - int new_size = yyg->yy_n_chars + number_to_move + (yyg->yy_n_chars >> 1); - YY_CURRENT_BUFFER_LVALUE->yy_ch_buf = (char *) yyrealloc( - (void *) YY_CURRENT_BUFFER_LVALUE->yy_ch_buf, (yy_size_t) new_size , yyscanner ); - if ( ! YY_CURRENT_BUFFER_LVALUE->yy_ch_buf ) - YY_FATAL_ERROR( "out of dynamic memory in yy_get_next_buffer()" ); - /* "- 2" to take care of EOB's */ - YY_CURRENT_BUFFER_LVALUE->yy_buf_size = (int) (new_size - 2); - } - - yyg->yy_n_chars += number_to_move; - YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[yyg->yy_n_chars] = YY_END_OF_BUFFER_CHAR; - YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[yyg->yy_n_chars + 1] = YY_END_OF_BUFFER_CHAR; - - yyg->yytext_ptr = &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[0]; - - return ret_val; -} - -/* yy_get_previous_state - get the state just before the EOB char was reached */ - - static yy_state_type yy_get_previous_state (yyscan_t yyscanner) -{ - yy_state_type yy_current_state; - char *yy_cp; - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; - - yy_current_state = yyg->yy_start; - - for ( yy_cp = yyg->yytext_ptr + YY_MORE_ADJ; yy_cp < yyg->yy_c_buf_p; ++yy_cp ) - { - YY_CHAR yy_c = (*yy_cp ? yy_ec[YY_SC_TO_UI(*yy_cp)] : 1); - if ( yy_accept[yy_current_state] ) - { - yyg->yy_last_accepting_state = yy_current_state; - yyg->yy_last_accepting_cpos = yy_cp; - } - while ( yy_chk[yy_base[yy_current_state] + yy_c] != yy_current_state ) - { - yy_current_state = (int) yy_def[yy_current_state]; - if ( yy_current_state >= 559 ) - yy_c = yy_meta[yy_c]; - } - yy_current_state = yy_nxt[yy_base[yy_current_state] + yy_c]; - } - - return yy_current_state; -} - -/* yy_try_NUL_trans - try to make a transition on the NUL character - * - * synopsis - * next_state = yy_try_NUL_trans( current_state ); - */ - static yy_state_type yy_try_NUL_trans (yy_state_type yy_current_state , yyscan_t yyscanner) -{ - int yy_is_jam; - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; /* This var may be unused depending upon options. */ - char *yy_cp = yyg->yy_c_buf_p; - - YY_CHAR yy_c = 1; - if ( yy_accept[yy_current_state] ) - { - yyg->yy_last_accepting_state = yy_current_state; - yyg->yy_last_accepting_cpos = yy_cp; - } - while ( yy_chk[yy_base[yy_current_state] + yy_c] != yy_current_state ) - { - yy_current_state = (int) yy_def[yy_current_state]; - if ( yy_current_state >= 559 ) - yy_c = yy_meta[yy_c]; - } - yy_current_state = yy_nxt[yy_base[yy_current_state] + yy_c]; - yy_is_jam = (yy_current_state == 558); - - (void)yyg; - return yy_is_jam ? 0 : yy_current_state; -} - -#ifndef YY_NO_UNPUT - - static void yyunput (int c, char * yy_bp , yyscan_t yyscanner) -{ - char *yy_cp; - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; - - yy_cp = yyg->yy_c_buf_p; - - /* undo effects of setting up yytext */ - *yy_cp = yyg->yy_hold_char; - - if ( yy_cp < YY_CURRENT_BUFFER_LVALUE->yy_ch_buf + 2 ) - { /* need to shift things up to make room */ - /* +2 for EOB chars. */ - int number_to_move = yyg->yy_n_chars + 2; - char *dest = &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[ - YY_CURRENT_BUFFER_LVALUE->yy_buf_size + 2]; - char *source = - &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[number_to_move]; - - while ( source > YY_CURRENT_BUFFER_LVALUE->yy_ch_buf ) - *--dest = *--source; - - yy_cp += (int) (dest - source); - yy_bp += (int) (dest - source); - YY_CURRENT_BUFFER_LVALUE->yy_n_chars = - yyg->yy_n_chars = (int) YY_CURRENT_BUFFER_LVALUE->yy_buf_size; - - if ( yy_cp < YY_CURRENT_BUFFER_LVALUE->yy_ch_buf + 2 ) - YY_FATAL_ERROR( "flex scanner push-back overflow" ); - } - - *--yy_cp = (char) c; - - if ( c == '\n' ){ - --yylineno; - } - - yyg->yytext_ptr = yy_bp; - yyg->yy_hold_char = *yy_cp; - yyg->yy_c_buf_p = yy_cp; -} - -#endif - -#ifndef YY_NO_INPUT -#ifdef __cplusplus - static int yyinput (yyscan_t yyscanner) -#else - static int input (yyscan_t yyscanner) -#endif - -{ - int c; - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; - - *yyg->yy_c_buf_p = yyg->yy_hold_char; - - if ( *yyg->yy_c_buf_p == YY_END_OF_BUFFER_CHAR ) - { - /* yy_c_buf_p now points to the character we want to return. - * If this occurs *before* the EOB characters, then it's a - * valid NUL; if not, then we've hit the end of the buffer. - */ - if ( yyg->yy_c_buf_p < &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[yyg->yy_n_chars] ) - /* This was really a NUL. */ - *yyg->yy_c_buf_p = '\0'; - - else - { /* need more input */ - int offset = (int) (yyg->yy_c_buf_p - yyg->yytext_ptr); - ++yyg->yy_c_buf_p; - - switch ( yy_get_next_buffer( yyscanner ) ) - { - case EOB_ACT_LAST_MATCH: - /* This happens because yy_g_n_b() - * sees that we've accumulated a - * token and flags that we need to - * try matching the token before - * proceeding. But for input(), - * there's no matching to consider. - * So convert the EOB_ACT_LAST_MATCH - * to EOB_ACT_END_OF_FILE. - */ - - /* Reset buffer status. */ - yyrestart( yyin , yyscanner); - - /*FALLTHROUGH*/ - - case EOB_ACT_END_OF_FILE: - { - if ( yywrap( yyscanner ) ) - return 0; - - if ( ! yyg->yy_did_buffer_switch_on_eof ) - YY_NEW_FILE; -#ifdef __cplusplus - return yyinput(yyscanner); -#else - return input(yyscanner); -#endif - } - - case EOB_ACT_CONTINUE_SCAN: - yyg->yy_c_buf_p = yyg->yytext_ptr + offset; - break; - } - } - } - - c = *(unsigned char *) yyg->yy_c_buf_p; /* cast for 8-bit char's */ - *yyg->yy_c_buf_p = '\0'; /* preserve yytext */ - yyg->yy_hold_char = *++yyg->yy_c_buf_p; - - if ( c == '\n' ) - - do{ yylineno++; - yycolumn=0; - }while(0) -; - - return c; -} -#endif /* ifndef YY_NO_INPUT */ - -/** Immediately switch to a different input stream. - * @param input_file A readable stream. - * @param yyscanner The scanner object. - * @note This function does not reset the start condition to @c INITIAL . - */ - void yyrestart (FILE * input_file , yyscan_t yyscanner) -{ - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; - - if ( ! YY_CURRENT_BUFFER ){ - yyensure_buffer_stack (yyscanner); - YY_CURRENT_BUFFER_LVALUE = - yy_create_buffer( yyin, YY_BUF_SIZE , yyscanner); - } - - yy_init_buffer( YY_CURRENT_BUFFER, input_file , yyscanner); - yy_load_buffer_state( yyscanner ); -} - -/** Switch to a different input buffer. - * @param new_buffer The new input buffer. - * @param yyscanner The scanner object. - */ - void yy_switch_to_buffer (YY_BUFFER_STATE new_buffer , yyscan_t yyscanner) -{ - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; - - /* TODO. We should be able to replace this entire function body - * with - * yypop_buffer_state(); - * yypush_buffer_state(new_buffer); - */ - yyensure_buffer_stack (yyscanner); - if ( YY_CURRENT_BUFFER == new_buffer ) - return; - - if ( YY_CURRENT_BUFFER ) - { - /* Flush out information for old buffer. */ - *yyg->yy_c_buf_p = yyg->yy_hold_char; - YY_CURRENT_BUFFER_LVALUE->yy_buf_pos = yyg->yy_c_buf_p; - YY_CURRENT_BUFFER_LVALUE->yy_n_chars = yyg->yy_n_chars; - } - - YY_CURRENT_BUFFER_LVALUE = new_buffer; - yy_load_buffer_state( yyscanner ); - - /* We don't actually know whether we did this switch during - * EOF (yywrap()) processing, but the only time this flag - * is looked at is after yywrap() is called, so it's safe - * to go ahead and always set it. - */ - yyg->yy_did_buffer_switch_on_eof = 1; -} - -static void yy_load_buffer_state (yyscan_t yyscanner) -{ - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; - yyg->yy_n_chars = YY_CURRENT_BUFFER_LVALUE->yy_n_chars; - yyg->yytext_ptr = yyg->yy_c_buf_p = YY_CURRENT_BUFFER_LVALUE->yy_buf_pos; - yyin = YY_CURRENT_BUFFER_LVALUE->yy_input_file; - yyg->yy_hold_char = *yyg->yy_c_buf_p; -} - -/** Allocate and initialize an input buffer state. - * @param file A readable stream. - * @param size The character buffer size in bytes. When in doubt, use @c YY_BUF_SIZE. - * @param yyscanner The scanner object. - * @return the allocated buffer state. - */ - YY_BUFFER_STATE yy_create_buffer (FILE * file, int size , yyscan_t yyscanner) -{ - YY_BUFFER_STATE b; - - b = (YY_BUFFER_STATE) yyalloc( sizeof( struct yy_buffer_state ) , yyscanner ); - if ( ! b ) - YY_FATAL_ERROR( "out of dynamic memory in yy_create_buffer()" ); - - b->yy_buf_size = size; - - /* yy_ch_buf has to be 2 characters longer than the size given because - * we need to put in 2 end-of-buffer characters. - */ - b->yy_ch_buf = (char *) yyalloc( (yy_size_t) (b->yy_buf_size + 2) , yyscanner ); - if ( ! b->yy_ch_buf ) - YY_FATAL_ERROR( "out of dynamic memory in yy_create_buffer()" ); - - b->yy_is_our_buffer = 1; - - yy_init_buffer( b, file , yyscanner); - - return b; -} - -/** Destroy the buffer. - * @param b a buffer created with yy_create_buffer() - * @param yyscanner The scanner object. - */ - void yy_delete_buffer (YY_BUFFER_STATE b , yyscan_t yyscanner) -{ - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; - - if ( ! b ) - return; - - if ( b == YY_CURRENT_BUFFER ) /* Not sure if we should pop here. */ - YY_CURRENT_BUFFER_LVALUE = (YY_BUFFER_STATE) 0; - - if ( b->yy_is_our_buffer ) - yyfree( (void *) b->yy_ch_buf , yyscanner ); - - yyfree( (void *) b , yyscanner ); -} - -/* Initializes or reinitializes a buffer. - * This function is sometimes called more than once on the same buffer, - * such as during a yyrestart() or at EOF. - */ - static void yy_init_buffer (YY_BUFFER_STATE b, FILE * file , yyscan_t yyscanner) - -{ - int oerrno = errno; - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; - - yy_flush_buffer( b , yyscanner); - - b->yy_input_file = file; - b->yy_fill_buffer = 1; - - /* If b is the current buffer, then yy_init_buffer was _probably_ - * called from yyrestart() or through yy_get_next_buffer. - * In that case, we don't want to reset the lineno or column. - */ - if (b != YY_CURRENT_BUFFER){ - b->yy_bs_lineno = 1; - b->yy_bs_column = 0; - } - - b->yy_is_interactive = file ? (isatty( fileno(file) ) > 0) : 0; - - errno = oerrno; -} - -/** Discard all buffered characters. On the next scan, YY_INPUT will be called. - * @param b the buffer state to be flushed, usually @c YY_CURRENT_BUFFER. - * @param yyscanner The scanner object. - */ - void yy_flush_buffer (YY_BUFFER_STATE b , yyscan_t yyscanner) -{ - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; - if ( ! b ) - return; - - b->yy_n_chars = 0; - - /* We always need two end-of-buffer characters. The first causes - * a transition to the end-of-buffer state. The second causes - * a jam in that state. - */ - b->yy_ch_buf[0] = YY_END_OF_BUFFER_CHAR; - b->yy_ch_buf[1] = YY_END_OF_BUFFER_CHAR; - - b->yy_buf_pos = &b->yy_ch_buf[0]; - - b->yy_at_bol = 1; - b->yy_buffer_status = YY_BUFFER_NEW; - - if ( b == YY_CURRENT_BUFFER ) - yy_load_buffer_state( yyscanner ); -} - -/** Pushes the new state onto the stack. The new state becomes - * the current state. This function will allocate the stack - * if necessary. - * @param new_buffer The new state. - * @param yyscanner The scanner object. - */ -void yypush_buffer_state (YY_BUFFER_STATE new_buffer , yyscan_t yyscanner) -{ - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; - if (new_buffer == NULL) - return; - - yyensure_buffer_stack(yyscanner); - - /* This block is copied from yy_switch_to_buffer. */ - if ( YY_CURRENT_BUFFER ) - { - /* Flush out information for old buffer. */ - *yyg->yy_c_buf_p = yyg->yy_hold_char; - YY_CURRENT_BUFFER_LVALUE->yy_buf_pos = yyg->yy_c_buf_p; - YY_CURRENT_BUFFER_LVALUE->yy_n_chars = yyg->yy_n_chars; - } - - /* Only push if top exists. Otherwise, replace top. */ - if (YY_CURRENT_BUFFER) - yyg->yy_buffer_stack_top++; - YY_CURRENT_BUFFER_LVALUE = new_buffer; - - /* copied from yy_switch_to_buffer. */ - yy_load_buffer_state( yyscanner ); - yyg->yy_did_buffer_switch_on_eof = 1; -} - -/** Removes and deletes the top of the stack, if present. - * The next element becomes the new top. - * @param yyscanner The scanner object. - */ -void yypop_buffer_state (yyscan_t yyscanner) -{ - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; - if (!YY_CURRENT_BUFFER) - return; - - yy_delete_buffer(YY_CURRENT_BUFFER , yyscanner); - YY_CURRENT_BUFFER_LVALUE = NULL; - if (yyg->yy_buffer_stack_top > 0) - --yyg->yy_buffer_stack_top; - - if (YY_CURRENT_BUFFER) { - yy_load_buffer_state( yyscanner ); - yyg->yy_did_buffer_switch_on_eof = 1; - } -} - -/* Allocates the stack if it does not exist. - * Guarantees space for at least one push. - */ -static void yyensure_buffer_stack (yyscan_t yyscanner) -{ - yy_size_t num_to_alloc; - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; - - if (!yyg->yy_buffer_stack) { - - /* First allocation is just for 2 elements, since we don't know if this - * scanner will even need a stack. We use 2 instead of 1 to avoid an - * immediate realloc on the next call. - */ - num_to_alloc = 1; /* After all that talk, this was set to 1 anyways... */ - yyg->yy_buffer_stack = (struct yy_buffer_state**)yyalloc - (num_to_alloc * sizeof(struct yy_buffer_state*) - , yyscanner); - if ( ! yyg->yy_buffer_stack ) - YY_FATAL_ERROR( "out of dynamic memory in yyensure_buffer_stack()" ); - - memset(yyg->yy_buffer_stack, 0, num_to_alloc * sizeof(struct yy_buffer_state*)); - - yyg->yy_buffer_stack_max = num_to_alloc; - yyg->yy_buffer_stack_top = 0; - return; - } - - if (yyg->yy_buffer_stack_top >= (yyg->yy_buffer_stack_max) - 1){ - - /* Increase the buffer to prepare for a possible push. */ - yy_size_t grow_size = 8 /* arbitrary grow size */; - - num_to_alloc = yyg->yy_buffer_stack_max + grow_size; - yyg->yy_buffer_stack = (struct yy_buffer_state**)yyrealloc - (yyg->yy_buffer_stack, - num_to_alloc * sizeof(struct yy_buffer_state*) - , yyscanner); - if ( ! yyg->yy_buffer_stack ) - YY_FATAL_ERROR( "out of dynamic memory in yyensure_buffer_stack()" ); - - /* zero only the new slots.*/ - memset(yyg->yy_buffer_stack + yyg->yy_buffer_stack_max, 0, grow_size * sizeof(struct yy_buffer_state*)); - yyg->yy_buffer_stack_max = num_to_alloc; - } -} - -/** Setup the input buffer state to scan directly from a user-specified character buffer. - * @param base the character buffer - * @param size the size in bytes of the character buffer - * @param yyscanner The scanner object. - * @return the newly allocated buffer state object. - */ -YY_BUFFER_STATE yy_scan_buffer (char * base, yy_size_t size , yyscan_t yyscanner) -{ - YY_BUFFER_STATE b; - - if ( size < 2 || - base[size-2] != YY_END_OF_BUFFER_CHAR || - base[size-1] != YY_END_OF_BUFFER_CHAR ) - /* They forgot to leave room for the EOB's. */ - return NULL; - - b = (YY_BUFFER_STATE) yyalloc( sizeof( struct yy_buffer_state ) , yyscanner ); - if ( ! b ) - YY_FATAL_ERROR( "out of dynamic memory in yy_scan_buffer()" ); - - b->yy_buf_size = (int) (size - 2); /* "- 2" to take care of EOB's */ - b->yy_buf_pos = b->yy_ch_buf = base; - b->yy_is_our_buffer = 0; - b->yy_input_file = NULL; - b->yy_n_chars = b->yy_buf_size; - b->yy_is_interactive = 0; - b->yy_at_bol = 1; - b->yy_fill_buffer = 0; - b->yy_buffer_status = YY_BUFFER_NEW; - - yy_switch_to_buffer( b , yyscanner ); - - return b; -} - -/** Setup the input buffer state to scan a string. The next call to yylex() will - * scan from a @e copy of @a str. - * @param yystr a NUL-terminated string to scan - * @param yyscanner The scanner object. - * @return the newly allocated buffer state object. - * @note If you want to scan bytes that may contain NUL values, then use - * yy_scan_bytes() instead. - */ -YY_BUFFER_STATE yy_scan_string (const char * yystr , yyscan_t yyscanner) -{ - - return yy_scan_bytes( yystr, (int) strlen(yystr) , yyscanner); -} - -/** Setup the input buffer state to scan the given bytes. The next call to yylex() will - * scan from a @e copy of @a bytes. - * @param yybytes the byte buffer to scan - * @param _yybytes_len the number of bytes in the buffer pointed to by @a bytes. - * @param yyscanner The scanner object. - * @return the newly allocated buffer state object. - */ -YY_BUFFER_STATE yy_scan_bytes (const char * yybytes, int _yybytes_len , yyscan_t yyscanner) -{ - YY_BUFFER_STATE b; - char *buf; - yy_size_t n; - int i; - - /* Get memory for full buffer, including space for trailing EOB's. */ - n = (yy_size_t) (_yybytes_len + 2); - buf = (char *) yyalloc( n , yyscanner ); - if ( ! buf ) - YY_FATAL_ERROR( "out of dynamic memory in yy_scan_bytes()" ); - - for ( i = 0; i < _yybytes_len; ++i ) - buf[i] = yybytes[i]; - - buf[_yybytes_len] = buf[_yybytes_len+1] = YY_END_OF_BUFFER_CHAR; - - b = yy_scan_buffer( buf, n , yyscanner); - if ( ! b ) - YY_FATAL_ERROR( "bad buffer in yy_scan_bytes()" ); - - /* It's okay to grow etc. this buffer, and we should throw it - * away when we're done. - */ - b->yy_is_our_buffer = 1; - - return b; -} - - static void yy_push_state (int _new_state , yyscan_t yyscanner) -{ - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; - if ( yyg->yy_start_stack_ptr >= yyg->yy_start_stack_depth ) - { - yy_size_t new_size; - - yyg->yy_start_stack_depth += YY_START_STACK_INCR; - new_size = (yy_size_t) yyg->yy_start_stack_depth * sizeof( int ); - - if ( ! yyg->yy_start_stack ) - yyg->yy_start_stack = (int *) yyalloc( new_size , yyscanner ); - - else - yyg->yy_start_stack = (int *) yyrealloc( - (void *) yyg->yy_start_stack, new_size , yyscanner ); - - if ( ! yyg->yy_start_stack ) - YY_FATAL_ERROR( "out of memory expanding start-condition stack" ); - } - - yyg->yy_start_stack[yyg->yy_start_stack_ptr++] = YY_START; - - BEGIN(_new_state); -} - - static void yy_pop_state (yyscan_t yyscanner) -{ - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; - if ( --yyg->yy_start_stack_ptr < 0 ) - YY_FATAL_ERROR( "start-condition stack underflow" ); - - BEGIN(yyg->yy_start_stack[yyg->yy_start_stack_ptr]); -} - - static int yy_top_state (yyscan_t yyscanner) -{ - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; - return yyg->yy_start_stack[yyg->yy_start_stack_ptr - 1]; -} - -#ifndef YY_EXIT_FAILURE -#define YY_EXIT_FAILURE 2 -#endif - -static void yynoreturn yy_fatal_error (const char* msg , yyscan_t yyscanner) -{ - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; - (void)yyg; - fprintf( stderr, "%s\n", msg ); - exit( YY_EXIT_FAILURE ); -} - -/* Redefine yyless() so it works in section 3 code. */ - -#undef yyless -#define yyless(n) \ - do \ - { \ - /* Undo effects of setting up yytext. */ \ - int yyless_macro_arg = (n); \ - YY_LESS_LINENO(yyless_macro_arg);\ - yytext[yyleng] = yyg->yy_hold_char; \ - yyg->yy_c_buf_p = yytext + yyless_macro_arg; \ - yyg->yy_hold_char = *yyg->yy_c_buf_p; \ - *yyg->yy_c_buf_p = '\0'; \ - yyleng = yyless_macro_arg; \ - } \ - while ( 0 ) - -/* Accessor methods (get/set functions) to struct members. */ - -/** Get the user-defined data for this scanner. - * @param yyscanner The scanner object. - */ -YY_EXTRA_TYPE yyget_extra (yyscan_t yyscanner) -{ - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; - return yyextra; -} - -/** Get the current line number. - * @param yyscanner The scanner object. - */ -int yyget_lineno (yyscan_t yyscanner) -{ - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; - - if (! YY_CURRENT_BUFFER) - return 0; - - return yylineno; -} - -/** Get the current column number. - * @param yyscanner The scanner object. - */ -int yyget_column (yyscan_t yyscanner) -{ - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; - - if (! YY_CURRENT_BUFFER) - return 0; - - return yycolumn; -} - -/** Get the input stream. - * @param yyscanner The scanner object. - */ -FILE *yyget_in (yyscan_t yyscanner) -{ - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; - return yyin; -} - -/** Get the output stream. - * @param yyscanner The scanner object. - */ -FILE *yyget_out (yyscan_t yyscanner) -{ - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; - return yyout; -} - -/** Get the length of the current token. - * @param yyscanner The scanner object. - */ -int yyget_leng (yyscan_t yyscanner) -{ - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; - return yyleng; -} - -/** Get the current token. - * @param yyscanner The scanner object. - */ - -char *yyget_text (yyscan_t yyscanner) -{ - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; - return yytext; -} - -/** Set the user-defined data. This data is never touched by the scanner. - * @param user_defined The data to be associated with this scanner. - * @param yyscanner The scanner object. - */ -void yyset_extra (YY_EXTRA_TYPE user_defined , yyscan_t yyscanner) -{ - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; - yyextra = user_defined ; -} - -/** Set the current line number. - * @param _line_number line number - * @param yyscanner The scanner object. - */ -void yyset_lineno (int _line_number , yyscan_t yyscanner) -{ - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; - - /* lineno is only valid if an input buffer exists. */ - if (! YY_CURRENT_BUFFER ) - YY_FATAL_ERROR( "yyset_lineno called with no buffer" ); - - yylineno = _line_number; -} - -/** Set the current column. - * @param _column_no column number - * @param yyscanner The scanner object. - */ -void yyset_column (int _column_no , yyscan_t yyscanner) -{ - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; - - /* column is only valid if an input buffer exists. */ - if (! YY_CURRENT_BUFFER ) - YY_FATAL_ERROR( "yyset_column called with no buffer" ); - - yycolumn = _column_no; -} - -/** Set the input stream. This does not discard the current - * input buffer. - * @param _in_str A readable stream. - * @param yyscanner The scanner object. - * @see yy_switch_to_buffer - */ -void yyset_in (FILE * _in_str , yyscan_t yyscanner) -{ - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; - yyin = _in_str ; -} - -void yyset_out (FILE * _out_str , yyscan_t yyscanner) -{ - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; - yyout = _out_str ; -} - -int yyget_debug (yyscan_t yyscanner) -{ - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; - return yy_flex_debug; -} - -void yyset_debug (int _bdebug , yyscan_t yyscanner) -{ - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; - yy_flex_debug = _bdebug ; -} - -/* Accessor methods for yylval and yylloc */ - -YYSTYPE * yyget_lval (yyscan_t yyscanner) -{ - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; - return yylval; -} - -void yyset_lval (YYSTYPE * yylval_param , yyscan_t yyscanner) -{ - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; - yylval = yylval_param; -} - -YYLTYPE *yyget_lloc (yyscan_t yyscanner) -{ - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; - return yylloc; -} - -void yyset_lloc (YYLTYPE * yylloc_param , yyscan_t yyscanner) -{ - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; - yylloc = yylloc_param; -} - -/* User-visible API */ - -/* yylex_init is special because it creates the scanner itself, so it is - * the ONLY reentrant function that doesn't take the scanner as the last argument. - * That's why we explicitly handle the declaration, instead of using our macros. - */ -int yylex_init(yyscan_t* ptr_yy_globals) -{ - if (ptr_yy_globals == NULL){ - errno = EINVAL; - return 1; - } - - *ptr_yy_globals = (yyscan_t) yyalloc ( sizeof( struct yyguts_t ), NULL ); - - if (*ptr_yy_globals == NULL){ - errno = ENOMEM; - return 1; - } - - /* By setting to 0xAA, we expose bugs in yy_init_globals. Leave at 0x00 for releases. */ - memset(*ptr_yy_globals,0x00,sizeof(struct yyguts_t)); - - return yy_init_globals ( *ptr_yy_globals ); -} - -/* yylex_init_extra has the same functionality as yylex_init, but follows the - * convention of taking the scanner as the last argument. Note however, that - * this is a *pointer* to a scanner, as it will be allocated by this call (and - * is the reason, too, why this function also must handle its own declaration). - * The user defined value in the first argument will be available to yyalloc in - * the yyextra field. - */ -int yylex_init_extra( YY_EXTRA_TYPE yy_user_defined, yyscan_t* ptr_yy_globals ) -{ - struct yyguts_t dummy_yyguts; - - yyset_extra (yy_user_defined, &dummy_yyguts); - - if (ptr_yy_globals == NULL){ - errno = EINVAL; - return 1; - } - - *ptr_yy_globals = (yyscan_t) yyalloc ( sizeof( struct yyguts_t ), &dummy_yyguts ); - - if (*ptr_yy_globals == NULL){ - errno = ENOMEM; - return 1; - } - - /* By setting to 0xAA, we expose bugs in - yy_init_globals. Leave at 0x00 for releases. */ - memset(*ptr_yy_globals,0x00,sizeof(struct yyguts_t)); - - yyset_extra (yy_user_defined, *ptr_yy_globals); - - return yy_init_globals ( *ptr_yy_globals ); -} - -static int yy_init_globals (yyscan_t yyscanner) -{ - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; - /* Initialization is the same as for the non-reentrant scanner. - * This function is called from yylex_destroy(), so don't allocate here. - */ - - yyg->yy_buffer_stack = NULL; - yyg->yy_buffer_stack_top = 0; - yyg->yy_buffer_stack_max = 0; - yyg->yy_c_buf_p = NULL; - yyg->yy_init = 0; - yyg->yy_start = 0; - - yyg->yy_start_stack_ptr = 0; - yyg->yy_start_stack_depth = 0; - yyg->yy_start_stack = NULL; - -/* Defined in main.c */ -#ifdef YY_STDINIT - yyin = stdin; - yyout = stdout; -#else - yyin = NULL; - yyout = NULL; -#endif - - /* For future reference: Set errno on error, since we are called by - * yylex_init() - */ - return 0; -} - -/* yylex_destroy is for both reentrant and non-reentrant scanners. */ -int yylex_destroy (yyscan_t yyscanner) -{ - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; - - /* Pop the buffer stack, destroying each element. */ - while(YY_CURRENT_BUFFER){ - yy_delete_buffer( YY_CURRENT_BUFFER , yyscanner ); - YY_CURRENT_BUFFER_LVALUE = NULL; - yypop_buffer_state(yyscanner); - } - - /* Destroy the stack itself. */ - yyfree(yyg->yy_buffer_stack , yyscanner); - yyg->yy_buffer_stack = NULL; - - /* Destroy the start condition stack. */ - yyfree( yyg->yy_start_stack , yyscanner ); - yyg->yy_start_stack = NULL; - - /* Reset the globals. This is important in a non-reentrant scanner so the next time - * yylex() is called, initialization will occur. */ - yy_init_globals( yyscanner); - - /* Destroy the main struct (reentrant only). */ - yyfree ( yyscanner , yyscanner ); - yyscanner = NULL; - return 0; -} - -/* - * Internal utility routines. - */ - -#ifndef yytext_ptr -static void yy_flex_strncpy (char* s1, const char * s2, int n , yyscan_t yyscanner) -{ - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; - (void)yyg; - - int i; - for ( i = 0; i < n; ++i ) - s1[i] = s2[i]; -} -#endif - -#ifdef YY_NEED_STRLEN -static int yy_flex_strlen (const char * s , yyscan_t yyscanner) -{ - int n; - for ( n = 0; s[n]; ++n ) - ; - - return n; -} -#endif - -void *yyalloc (yy_size_t size , yyscan_t yyscanner) -{ - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; - (void)yyg; - return malloc(size); -} - -void *yyrealloc (void * ptr, yy_size_t size , yyscan_t yyscanner) -{ - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; - (void)yyg; - - /* The cast to (char *) in the following accommodates both - * implementations that use char* generic pointers, and those - * that use void* generic pointers. It works with the latter - * because both ANSI C and C++ allow castless assignment from - * any pointer type to void*, and deal with argument conversions - * as though doing an assignment. - */ - return realloc(ptr, size); -} - -void yyfree (void * ptr , yyscan_t yyscanner) -{ - struct yyguts_t * yyg = (struct yyguts_t*)yyscanner; - (void)yyg; - free( (char *) ptr ); /* see yyrealloc() for (char *) cast */ -} - -#define YYTABLES_NAME "yytables" - -#line 165 "smt2new/smt2newlexer.ll" - - -int Smt2newContext::init_scanner() -{ - if (is != NULL) { - yylex_init_extra(this, &scanner); - yyset_in(is, scanner); - } - else if (ib != NULL) { - yylex_init(&scanner); - yylex_init_extra(this, &scanner); - yy_scan_string(ib, scanner); - } - else - return -1; - return 0; -} - -void Smt2newContext::destroy_scanner() -{ - yylex_destroy(scanner); -} - - diff --git a/src/parsers/smt2new/smt2newparser.cc b/src/parsers/smt2new/smt2newparser.cc deleted file mode 100644 index 6a3c8730f..000000000 --- a/src/parsers/smt2new/smt2newparser.cc +++ /dev/null @@ -1,2887 +0,0 @@ -/* A Bison parser, made by GNU Bison 3.0.4. */ - -/* Bison implementation for Yacc-like parsers in C - - Copyright (C) 1984, 1989-1990, 2000-2015 Free Software Foundation, Inc. - - This program is free software: you can redistribute it and/or modify - it under the terms of the GNU General Public License as published by - the Free Software Foundation, either version 3 of the License, or - (at your option) any later version. - - This program is distributed in the hope that it will be useful, - but WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - GNU General Public License for more details. - - You should have received a copy of the GNU General Public License - along with this program. If not, see . */ - -/* As a special exception, you may create a larger work that contains - part or all of the Bison parser skeleton and distribute that work - under terms of your choice, so long as that work isn't itself a - parser generator using the skeleton or a modified version thereof - as a parser skeleton. Alternatively, if you modify or redistribute - the parser skeleton itself, you may (at your option) remove this - special exception, which will cause the skeleton and the resulting - Bison output files to be licensed under the GNU General Public - License without this special exception. - - This special exception was added by the Free Software Foundation in - version 2.2 of Bison. */ - -/* C LALR(1) parser skeleton written by Richard Stallman, by - simplifying the original so-called "semantic" parser. */ - -/* All symbols defined below should begin with yy or YY, to avoid - infringing on user name space. This should be done even for local - variables, as they might otherwise be expanded by user macros. - There are some unavoidable exceptions within include files to - define necessary library symbols; they are noted "INFRINGES ON - USER NAME SPACE" below. */ - -/* Identify Bison output. */ -#define YYBISON 1 - -/* Bison version. */ -#define YYBISON_VERSION "3.0.4" - -/* Skeleton name. */ -#define YYSKELETON_NAME "yacc.c" - -/* Pure parsers. */ -#define YYPURE 1 - -/* Push parsers. */ -#define YYPUSH 0 - -/* Pull parsers. */ -#define YYPULL 1 - - -/* Substitute the variable and function names. */ -#define yyparse smt2newparse -#define yylex smt2newlex -#define yyerror smt2newerror -#define yydebug smt2newdebug -#define yynerrs smt2newnerrs - - -/* Copy the first part of user declarations. */ -#line 35 "smt2new/smt2newparser.yy" /* yacc.c:339 */ - -#include -#include -#include -#include -#include -#include -#include - -#include "smt2newcontext.h" -#include "smt2newparser.hh" -#include "smt2tokens.h" - -int smt2newlex(YYSTYPE* lvalp, YYLTYPE* llocp, void* scanner); - -void smt2newerror( YYLTYPE* locp, Smt2newContext* context, const char * s ) -{ - if (context->interactive) - printf("At interactive input: %s\n", s); - else - printf( "At line %d: %s\n", locp->first_line, s ); -// exit( 1 ); -} - -#define scanner context->scanner - -/* Overallocation to prevent stack overflow */ -#define YYMAXDEPTH 1024 * 1024 - -#line 102 "smt2new/smt2newparser.cc" /* yacc.c:339 */ - -# ifndef YY_NULLPTR -# if defined __cplusplus && 201103L <= __cplusplus -# define YY_NULLPTR nullptr -# else -# define YY_NULLPTR 0 -# endif -# endif - -/* Enabling verbose error messages. */ -#ifdef YYERROR_VERBOSE -# undef YYERROR_VERBOSE -# define YYERROR_VERBOSE 1 -#else -# define YYERROR_VERBOSE 1 -#endif - -/* In a future release of Bison, this section will be replaced - by #include "smt2newparser.hh". */ -#ifndef YY_SMT2NEW_SMT2NEW_SMT2NEWPARSER_HH_INCLUDED -# define YY_SMT2NEW_SMT2NEW_SMT2NEWPARSER_HH_INCLUDED -/* Debug traces. */ -#ifndef YYDEBUG -# define YYDEBUG 0 -#endif -#if YYDEBUG -extern int smt2newdebug; -#endif - -/* Token type. */ -#ifndef YYTOKENTYPE -# define YYTOKENTYPE - enum yytokentype - { - TK_AS = 258, - TK_DECIMAL = 259, - TK_EXISTS = 260, - TK_FORALL = 261, - TK_LET = 262, - TK_NUMERAL = 263, - TK_PAR = 264, - TK_STRING = 265, - TK_ASSERT = 266, - TK_CHECKSAT = 267, - TK_DECLARESORT = 268, - TK_DECLAREFUN = 269, - TK_DECLARECONST = 270, - TK_DEFINESORT = 271, - TK_DEFINEFUN = 272, - TK_EXIT = 273, - TK_GETASSERTIONS = 274, - TK_GETASSIGNMENT = 275, - TK_GETINFO = 276, - TK_GETOPTION = 277, - TK_GETPROOF = 278, - TK_GETUNSATCORE = 279, - TK_GETVALUE = 280, - TK_POP = 281, - TK_PUSH = 282, - TK_SETLOGIC = 283, - TK_SETINFO = 284, - TK_SETOPTION = 285, - TK_THEORY = 286, - TK_GETITPS = 287, - TK_WRSTATE = 288, - TK_RDSTATE = 289, - TK_SIMPLIFY = 290, - TK_WRFUNS = 291, - TK_NUM = 292, - TK_SYM = 293, - TK_KEY = 294, - TK_STR = 295, - TK_DEC = 296, - TK_HEX = 297, - TK_BIN = 298, - KW_SORTS = 299, - KW_FUNS = 300, - KW_SORTSDESCRIPTION = 301, - KW_FUNSDESCRIPTION = 302, - KW_DEFINITION = 303, - KW_NOTES = 304, - KW_THEORIES = 305, - KW_LANGUAGE = 306, - KW_EXTENSIONS = 307, - KW_VALUES = 308, - KW_PRINTSUCCESS = 309, - KW_EXPANDDEFINITIONS = 310, - KW_INTERACTIVEMODE = 311, - KW_PRODUCEPROOFS = 312, - KW_PRODUCEUNSATCORES = 313, - KW_PRODUCEMODELS = 314, - KW_PRODUCEASSIGNMENTS = 315, - KW_REGULAROUTPUTCHANNEL = 316, - KW_DIAGNOSTICOUTPUTCHANNEL = 317, - KW_RANDOMSEED = 318, - KW_VERBOSITY = 319, - KW_ERRORBEHAVIOR = 320, - KW_NAME = 321, - KW_NAMED = 322, - KW_AUTHORS = 323, - KW_VERSION = 324, - KW_STATUS = 325, - KW_REASONUNKNOWN = 326, - KW_ALLSTATISTICS = 327 - }; -#endif - -/* Value type. */ -#if ! defined YYSTYPE && ! defined YYSTYPE_IS_DECLARED - -union YYSTYPE -{ -#line 66 "smt2new/smt2newparser.yy" /* yacc.c:355 */ - - char * str; - std::vector< std::string > * str_list; - ASTNode * snode; - std::list< ASTNode * > * snode_list; - smt2token tok; - -#line 223 "smt2new/smt2newparser.cc" /* yacc.c:355 */ -}; - -typedef union YYSTYPE YYSTYPE; -# define YYSTYPE_IS_TRIVIAL 1 -# define YYSTYPE_IS_DECLARED 1 -#endif - -/* Location type. */ -#if ! defined YYLTYPE && ! defined YYLTYPE_IS_DECLARED -typedef struct YYLTYPE YYLTYPE; -struct YYLTYPE -{ - int first_line; - int first_column; - int last_line; - int last_column; -}; -# define YYLTYPE_IS_DECLARED 1 -# define YYLTYPE_IS_TRIVIAL 1 -#endif - - - -int smt2newparse (Smt2newContext* context); - -#endif /* !YY_SMT2NEW_SMT2NEW_SMT2NEWPARSER_HH_INCLUDED */ - -/* Copy the second part of user declarations. */ - -#line 253 "smt2new/smt2newparser.cc" /* yacc.c:358 */ - -#ifdef short -# undef short -#endif - -#ifdef YYTYPE_UINT8 -typedef YYTYPE_UINT8 yytype_uint8; -#else -typedef unsigned char yytype_uint8; -#endif - -#ifdef YYTYPE_INT8 -typedef YYTYPE_INT8 yytype_int8; -#else -typedef signed char yytype_int8; -#endif - -#ifdef YYTYPE_UINT16 -typedef YYTYPE_UINT16 yytype_uint16; -#else -typedef unsigned short int yytype_uint16; -#endif - -#ifdef YYTYPE_INT16 -typedef YYTYPE_INT16 yytype_int16; -#else -typedef short int yytype_int16; -#endif - -#ifndef YYSIZE_T -# ifdef __SIZE_TYPE__ -# define YYSIZE_T __SIZE_TYPE__ -# elif defined size_t -# define YYSIZE_T size_t -# elif ! defined YYSIZE_T -# include /* INFRINGES ON USER NAME SPACE */ -# define YYSIZE_T size_t -# else -# define YYSIZE_T unsigned int -# endif -#endif - -#define YYSIZE_MAXIMUM ((YYSIZE_T) -1) - -#ifndef YY_ -# if defined YYENABLE_NLS && YYENABLE_NLS -# if ENABLE_NLS -# include /* INFRINGES ON USER NAME SPACE */ -# define YY_(Msgid) dgettext ("bison-runtime", Msgid) -# endif -# endif -# ifndef YY_ -# define YY_(Msgid) Msgid -# endif -#endif - -#ifndef YY_ATTRIBUTE -# if (defined __GNUC__ \ - && (2 < __GNUC__ || (__GNUC__ == 2 && 96 <= __GNUC_MINOR__))) \ - || defined __SUNPRO_C && 0x5110 <= __SUNPRO_C -# define YY_ATTRIBUTE(Spec) __attribute__(Spec) -# else -# define YY_ATTRIBUTE(Spec) /* empty */ -# endif -#endif - -#ifndef YY_ATTRIBUTE_PURE -# define YY_ATTRIBUTE_PURE YY_ATTRIBUTE ((__pure__)) -#endif - -#ifndef YY_ATTRIBUTE_UNUSED -# define YY_ATTRIBUTE_UNUSED YY_ATTRIBUTE ((__unused__)) -#endif - -#if !defined _Noreturn \ - && (!defined __STDC_VERSION__ || __STDC_VERSION__ < 201112) -# if defined _MSC_VER && 1200 <= _MSC_VER -# define _Noreturn __declspec (noreturn) -# else -# define _Noreturn YY_ATTRIBUTE ((__noreturn__)) -# endif -#endif - -/* Suppress unused-variable warnings by "using" E. */ -#if ! defined lint || defined __GNUC__ -# define YYUSE(E) ((void) (E)) -#else -# define YYUSE(E) /* empty */ -#endif - -#if defined __GNUC__ && 407 <= __GNUC__ * 100 + __GNUC_MINOR__ -/* Suppress an incorrect diagnostic about yylval being uninitialized. */ -# define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN \ - _Pragma ("GCC diagnostic push") \ - _Pragma ("GCC diagnostic ignored \"-Wuninitialized\"")\ - _Pragma ("GCC diagnostic ignored \"-Wmaybe-uninitialized\"") -# define YY_IGNORE_MAYBE_UNINITIALIZED_END \ - _Pragma ("GCC diagnostic pop") -#else -# define YY_INITIAL_VALUE(Value) Value -#endif -#ifndef YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN -# define YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN -# define YY_IGNORE_MAYBE_UNINITIALIZED_END -#endif -#ifndef YY_INITIAL_VALUE -# define YY_INITIAL_VALUE(Value) /* Nothing. */ -#endif - - -#if ! defined yyoverflow || YYERROR_VERBOSE - -/* The parser invokes alloca or malloc; define the necessary symbols. */ - -# ifdef YYSTACK_USE_ALLOCA -# if YYSTACK_USE_ALLOCA -# ifdef __GNUC__ -# define YYSTACK_ALLOC __builtin_alloca -# elif defined __BUILTIN_VA_ARG_INCR -# include /* INFRINGES ON USER NAME SPACE */ -# elif defined _AIX -# define YYSTACK_ALLOC __alloca -# elif defined _MSC_VER -# include /* INFRINGES ON USER NAME SPACE */ -# define alloca _alloca -# else -# define YYSTACK_ALLOC alloca -# if ! defined _ALLOCA_H && ! defined EXIT_SUCCESS -# include /* INFRINGES ON USER NAME SPACE */ - /* Use EXIT_SUCCESS as a witness for stdlib.h. */ -# ifndef EXIT_SUCCESS -# define EXIT_SUCCESS 0 -# endif -# endif -# endif -# endif -# endif - -# ifdef YYSTACK_ALLOC - /* Pacify GCC's 'empty if-body' warning. */ -# define YYSTACK_FREE(Ptr) do { /* empty */; } while (0) -# ifndef YYSTACK_ALLOC_MAXIMUM - /* The OS might guarantee only one guard page at the bottom of the stack, - and a page size can be as small as 4096 bytes. So we cannot safely - invoke alloca (N) if N exceeds 4096. Use a slightly smaller number - to allow for a few compiler-allocated temporary stack slots. */ -# define YYSTACK_ALLOC_MAXIMUM 4032 /* reasonable circa 2006 */ -# endif -# else -# define YYSTACK_ALLOC YYMALLOC -# define YYSTACK_FREE YYFREE -# ifndef YYSTACK_ALLOC_MAXIMUM -# define YYSTACK_ALLOC_MAXIMUM YYSIZE_MAXIMUM -# endif -# if (defined __cplusplus && ! defined EXIT_SUCCESS \ - && ! ((defined YYMALLOC || defined malloc) \ - && (defined YYFREE || defined free))) -# include /* INFRINGES ON USER NAME SPACE */ -# ifndef EXIT_SUCCESS -# define EXIT_SUCCESS 0 -# endif -# endif -# ifndef YYMALLOC -# define YYMALLOC malloc -# if ! defined malloc && ! defined EXIT_SUCCESS -void *malloc (YYSIZE_T); /* INFRINGES ON USER NAME SPACE */ -# endif -# endif -# ifndef YYFREE -# define YYFREE free -# if ! defined free && ! defined EXIT_SUCCESS -void free (void *); /* INFRINGES ON USER NAME SPACE */ -# endif -# endif -# endif -#endif /* ! defined yyoverflow || YYERROR_VERBOSE */ - - -#if (! defined yyoverflow \ - && (! defined __cplusplus \ - || (defined YYLTYPE_IS_TRIVIAL && YYLTYPE_IS_TRIVIAL \ - && defined YYSTYPE_IS_TRIVIAL && YYSTYPE_IS_TRIVIAL))) - -/* A type that is properly aligned for any stack member. */ -union yyalloc -{ - yytype_int16 yyss_alloc; - YYSTYPE yyvs_alloc; - YYLTYPE yyls_alloc; -}; - -/* The size of the maximum gap between one aligned stack and the next. */ -# define YYSTACK_GAP_MAXIMUM (sizeof (union yyalloc) - 1) - -/* The size of an array large to enough to hold all stacks, each with - N elements. */ -# define YYSTACK_BYTES(N) \ - ((N) * (sizeof (yytype_int16) + sizeof (YYSTYPE) + sizeof (YYLTYPE)) \ - + 2 * YYSTACK_GAP_MAXIMUM) - -# define YYCOPY_NEEDED 1 - -/* Relocate STACK from its old location to the new one. The - local variables YYSIZE and YYSTACKSIZE give the old and new number of - elements in the stack, and YYPTR gives the new location of the - stack. Advance YYPTR to a properly aligned location for the next - stack. */ -# define YYSTACK_RELOCATE(Stack_alloc, Stack) \ - do \ - { \ - YYSIZE_T yynewbytes; \ - YYCOPY (&yyptr->Stack_alloc, Stack, yysize); \ - Stack = &yyptr->Stack_alloc; \ - yynewbytes = yystacksize * sizeof (*Stack) + YYSTACK_GAP_MAXIMUM; \ - yyptr += yynewbytes / sizeof (*yyptr); \ - } \ - while (0) - -#endif - -#if defined YYCOPY_NEEDED && YYCOPY_NEEDED -/* Copy COUNT objects from SRC to DST. The source and destination do - not overlap. */ -# ifndef YYCOPY -# if defined __GNUC__ && 1 < __GNUC__ -# define YYCOPY(Dst, Src, Count) \ - __builtin_memcpy (Dst, Src, (Count) * sizeof (*(Src))) -# else -# define YYCOPY(Dst, Src, Count) \ - do \ - { \ - YYSIZE_T yyi; \ - for (yyi = 0; yyi < (Count); yyi++) \ - (Dst)[yyi] = (Src)[yyi]; \ - } \ - while (0) -# endif -# endif -#endif /* !YYCOPY_NEEDED */ - -/* YYFINAL -- State number of the termination state. */ -#define YYFINAL 3 -/* YYLAST -- Last index in YYTABLE. */ -#define YYLAST 378 - -/* YYNTOKENS -- Number of terminals. */ -#define YYNTOKENS 77 -/* YYNNTS -- Number of nonterminals. */ -#define YYNNTS 27 -/* YYNRULES -- Number of rules. */ -#define YYNRULES 129 -/* YYNSTATES -- Number of states. */ -#define YYNSTATES 246 - -/* YYTRANSLATE[YYX] -- Symbol number corresponding to YYX as returned - by yylex, with out-of-bounds checking. */ -#define YYUNDEFTOK 2 -#define YYMAXUTOK 327 - -#define YYTRANSLATE(YYX) \ - ((unsigned int) (YYX) <= YYMAXUTOK ? yytranslate[YYX] : YYUNDEFTOK) - -/* YYTRANSLATE[TOKEN-NUM] -- Symbol number corresponding to TOKEN-NUM - as returned by yylex, without out-of-bounds checking. */ -static const yytype_uint8 yytranslate[] = -{ - 0, 2, 2, 2, 2, 2, 2, 2, 2, 2, - 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, - 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, - 2, 2, 2, 76, 2, 2, 2, 2, 2, 2, - 73, 74, 2, 2, 2, 2, 2, 2, 2, 2, - 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, - 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, - 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, - 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, - 2, 2, 2, 2, 2, 75, 2, 2, 2, 2, - 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, - 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, - 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, - 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, - 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, - 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, - 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, - 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, - 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, - 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, - 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, - 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, - 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, - 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, - 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, - 2, 2, 2, 2, 2, 2, 1, 2, 3, 4, - 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, - 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, - 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, - 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, - 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, - 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, - 65, 66, 67, 68, 69, 70, 71, 72 -}; - -#if YYDEBUG - /* YYRLINE[YYN] -- Source line where rule number YYN was defined. */ -static const yytype_uint16 yyrline[] = -{ - 0, 97, 97, 101, 102, 106, 112, 118, 124, 131, - 144, 156, 168, 181, 187, 193, 199, 203, 207, 211, - 215, 221, 227, 233, 237, 243, 247, 253, 259, 265, - 269, 274, 275, 279, 281, 283, 285, 289, 291, 295, - 302, 304, 308, 310, 318, 321, 324, 330, 334, 338, - 346, 349, 357, 359, 361, 363, 365, 369, 371, 375, - 377, 381, 383, 393, 394, 398, 403, 404, 408, 412, - 413, 417, 419, 421, 428, 438, 448, 458, 535, 536, - 693, 706, 712, 718, 724, 730, 736, 742, 748, 754, - 760, 766, 772, 780, 782, 784, 786, 788, 790, 792, - 794, 796, 798, 800, 802, 804, 806, 808, 810, 812, - 814, 816, 818, 820, 822, 824, 826, 828, 830, 832, - 834, 836, 840, 842, 844, 846, 848, 850, 852, 854 -}; -#endif - -#if YYDEBUG || YYERROR_VERBOSE || 1 -/* YYTNAME[SYMBOL-NUM] -- String name of the symbol SYMBOL-NUM. - First, the terminals, then, starting at YYNTOKENS, nonterminals. */ -static const char *const yytname[] = -{ - "$end", "error", "$undefined", "TK_AS", "TK_DECIMAL", "TK_EXISTS", - "TK_FORALL", "TK_LET", "TK_NUMERAL", "TK_PAR", "TK_STRING", "TK_ASSERT", - "TK_CHECKSAT", "TK_DECLARESORT", "TK_DECLAREFUN", "TK_DECLARECONST", - "TK_DEFINESORT", "TK_DEFINEFUN", "TK_EXIT", "TK_GETASSERTIONS", - "TK_GETASSIGNMENT", "TK_GETINFO", "TK_GETOPTION", "TK_GETPROOF", - "TK_GETUNSATCORE", "TK_GETVALUE", "TK_POP", "TK_PUSH", "TK_SETLOGIC", - "TK_SETINFO", "TK_SETOPTION", "TK_THEORY", "TK_GETITPS", "TK_WRSTATE", - "TK_RDSTATE", "TK_SIMPLIFY", "TK_WRFUNS", "TK_NUM", "TK_SYM", "TK_KEY", - "TK_STR", "TK_DEC", "TK_HEX", "TK_BIN", "KW_SORTS", "KW_FUNS", - "KW_SORTSDESCRIPTION", "KW_FUNSDESCRIPTION", "KW_DEFINITION", "KW_NOTES", - "KW_THEORIES", "KW_LANGUAGE", "KW_EXTENSIONS", "KW_VALUES", - "KW_PRINTSUCCESS", "KW_EXPANDDEFINITIONS", "KW_INTERACTIVEMODE", - "KW_PRODUCEPROOFS", "KW_PRODUCEUNSATCORES", "KW_PRODUCEMODELS", - "KW_PRODUCEASSIGNMENTS", "KW_REGULAROUTPUTCHANNEL", - "KW_DIAGNOSTICOUTPUTCHANNEL", "KW_RANDOMSEED", "KW_VERBOSITY", - "KW_ERRORBEHAVIOR", "KW_NAME", "KW_NAMED", "KW_AUTHORS", "KW_VERSION", - "KW_STATUS", "KW_REASONUNKNOWN", "KW_ALLSTATISTICS", "'('", "')'", "'_'", - "'!'", "$accept", "script", "command_list", "command", "attribute_list", - "attribute", "attribute_value", "identifier", "sort", "sort_list", - "s_expr", "s_expr_list", "spec_const", "const_val", "numeral_list", - "qual_identifier", "var_binding_list", "var_binding", "sorted_var_list", - "sorted_var", "term_list", "term", "symbol_list", "b_value", "option", - "predef_key", "info_flag", YY_NULLPTR -}; -#endif - -# ifdef YYPRINT -/* YYTOKNUM[NUM] -- (External) token number corresponding to the - (internal) symbol number NUM (which must be that of a token). */ -static const yytype_uint16 yytoknum[] = -{ - 0, 256, 257, 258, 259, 260, 261, 262, 263, 264, - 265, 266, 267, 268, 269, 270, 271, 272, 273, 274, - 275, 276, 277, 278, 279, 280, 281, 282, 283, 284, - 285, 286, 287, 288, 289, 290, 291, 292, 293, 294, - 295, 296, 297, 298, 299, 300, 301, 302, 303, 304, - 305, 306, 307, 308, 309, 310, 311, 312, 313, 314, - 315, 316, 317, 318, 319, 320, 321, 322, 323, 324, - 325, 326, 327, 40, 41, 95, 33 -}; -# endif - -#define YYPACT_NINF -161 - -#define yypact_value_is_default(Yystate) \ - (!!((Yystate) == (-161))) - -#define YYTABLE_NINF -1 - -#define yytable_value_is_error(Yytable_value) \ - 0 - - /* YYPACT[STATE-NUM] -- Index in YYTABLE of the portion describing - STATE-NUM. */ -static const yytype_int16 yypact[] = -{ - -161, 10, -58, -161, 342, -161, -1, -10, 27, 29, - 112, 32, 33, 3, 5, 11, 104, 212, 12, 13, - 1, 43, 47, 50, 246, 280, 17, 54, 65, 36, - 73, -161, -161, -161, -161, -161, -161, 0, -161, -161, - -161, 44, -161, 82, 49, -161, -161, 53, 61, 62, - -161, -161, -161, -161, -161, -161, -161, -161, -161, -161, - -161, 57, 63, -161, -161, -161, -161, -161, -161, -161, - -161, -161, -161, -161, -161, -161, -161, -161, -161, -161, - -161, -161, -161, -161, -161, -161, -161, -161, -161, -161, - -161, -161, 64, -161, -161, -1, 67, 68, 70, 87, - 71, 87, 98, 98, 98, 98, 98, 98, 98, 111, - 116, 120, 121, -161, 85, -161, 93, 97, -161, 103, - -22, 105, 106, 107, 6, 143, -1, -1, -161, 108, - -161, 109, -161, -161, -161, -161, -161, -161, -161, -161, - -161, -161, -161, -161, -161, -161, -161, -161, -161, -161, - -161, -161, -161, -161, -161, -161, -161, -161, -161, -161, - -161, -161, -161, 110, -14, 113, 113, 114, 147, 246, - -161, -161, -11, -14, -24, -48, 66, -20, -27, -161, - 115, 150, -161, -161, 152, -161, -161, -25, -161, 74, - -14, -161, 118, -161, -14, -14, -161, 119, -161, -161, - -161, -161, -161, -161, -161, -14, -161, -14, -45, -42, - -1, -30, -161, -161, 178, -161, 122, -161, 123, -1, - -161, 59, -161, 124, -1, -1, 125, -1, -161, -161, - -161, -161, -161, 126, -161, -5, -161, 127, 128, -161, - 129, -161, -161, -161, -161, -161 -}; - - /* YYDEFACT[STATE-NUM] -- Default reduction number in state STATE-NUM. - Performed when YYTABLE does not specify something else to do. Zero - means the default is an error. */ -static const yytype_uint8 yydefact[] = -{ - 3, 0, 2, 1, 0, 4, 0, 0, 0, 0, - 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, - 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, - 0, 52, 40, 56, 53, 54, 55, 0, 61, 71, - 72, 0, 16, 0, 0, 57, 58, 0, 0, 0, - 30, 17, 25, 129, 122, 123, 124, 125, 126, 127, - 128, 0, 0, 93, 94, 95, 96, 97, 99, 100, - 101, 102, 98, 103, 104, 105, 106, 107, 108, 109, - 110, 111, 112, 113, 114, 115, 116, 117, 118, 119, - 120, 121, 0, 18, 23, 0, 0, 0, 0, 33, - 0, 35, 103, 104, 105, 106, 107, 108, 109, 110, - 111, 112, 113, 92, 0, 19, 0, 0, 29, 0, - 0, 0, 0, 0, 0, 0, 0, 0, 15, 0, - 45, 0, 78, 66, 28, 26, 27, 69, 14, 13, - 5, 38, 50, 34, 37, 7, 36, 80, 81, 82, - 83, 84, 85, 86, 87, 88, 89, 90, 91, 6, - 20, 21, 22, 0, 0, 0, 0, 0, 0, 0, - 69, 8, 0, 0, 0, 0, 0, 0, 0, 42, - 0, 0, 66, 66, 0, 63, 60, 0, 31, 0, - 0, 44, 0, 79, 0, 0, 67, 0, 70, 47, - 48, 50, 39, 51, 46, 0, 62, 0, 0, 0, - 0, 0, 59, 41, 0, 73, 0, 11, 0, 0, - 24, 0, 45, 0, 0, 0, 0, 0, 64, 77, - 32, 10, 9, 0, 49, 0, 68, 0, 0, 65, - 0, 12, 43, 76, 75, 74 -}; - - /* YYPGOTO[NTERM-NUM]. */ -static const yytype_int16 yypgoto[] = -{ - -161, -161, -161, -161, -161, -23, 94, -112, -160, -28, - -161, 4, -9, -161, -161, 169, -161, -4, -127, -108, - 38, -6, -161, 58, -161, 192, -161 -}; - - /* YYDEFGOTO[NTERM-NUM]. */ -static const yytype_int16 yydefgoto[] = -{ - -1, 1, 2, 5, 214, 100, 143, 38, 191, 172, - 203, 177, 39, 47, 187, 40, 211, 185, 175, 196, - 176, 198, 174, 148, 114, 101, 61 -}; - - /* YYTABLE[YYPACT[STATE-NUM]] -- What to do in state STATE-NUM. If - positive, shift that token. If negative, reduce the rule whose - number is the opposite. If YYTABLE_NINF, syntax error. */ -static const yytype_uint8 yytable[] = -{ - 41, 46, 113, 120, 180, 121, 122, 123, 164, 120, - 3, 32, 212, 192, 193, 4, 32, 31, 199, 200, - 33, 34, 35, 36, 32, 181, 195, 32, 181, 224, - 216, 181, 225, 32, 218, 219, 31, 32, 32, 33, - 34, 35, 36, 184, 227, 222, 163, 223, 125, 213, - 194, 163, 179, 201, 202, 208, 209, 182, 183, 178, - 179, 179, 178, 190, 42, 43, 205, 44, 178, 242, - 48, 49, 37, 124, 95, 125, 126, 50, 179, 51, - 96, 125, 179, 179, 97, 52, 93, 94, 98, 137, - 144, 115, 144, 179, 116, 179, 31, 199, 200, 33, - 34, 35, 36, 31, 32, 117, 33, 34, 35, 36, - 118, 31, 32, 119, 33, 34, 35, 36, 128, 129, - 169, 170, 130, 179, 31, 141, 131, 33, 34, 35, - 36, 134, 201, 234, 132, 133, 147, 135, 136, 37, - 197, 138, 139, 53, 140, 145, 188, 37, 215, 31, - 45, 155, 33, 34, 35, 36, 156, 157, 158, 159, - 142, 149, 150, 151, 152, 153, 154, 160, 204, 54, - 55, 161, 56, 57, 58, 59, 60, 162, 165, 166, - 167, 168, 171, 173, 186, 125, 181, 184, 207, 206, - 210, 230, 217, 220, 235, 146, 231, 232, 236, 239, - 241, 243, 244, 245, 226, 221, 127, 228, 189, 92, - 0, 0, 204, 233, 0, 0, 0, 99, 237, 238, - 0, 240, 63, 64, 65, 66, 67, 68, 69, 70, - 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, - 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, - 91, 62, 229, 0, 0, 0, 63, 64, 65, 66, - 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, - 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, - 87, 88, 89, 90, 91, 99, 0, 0, 0, 0, - 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, - 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, - 83, 84, 85, 86, 87, 88, 89, 90, 91, 99, - 0, 0, 0, 0, 63, 64, 65, 66, 67, 68, - 69, 70, 71, 72, 102, 103, 104, 105, 106, 107, - 108, 109, 110, 111, 112, 84, 85, 86, 87, 88, - 89, 90, 91, 6, 7, 8, 9, 10, 11, 12, - 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, - 23, 24, 25, 0, 26, 27, 28, 29, 30 -}; - -static const yytype_int16 yycheck[] = -{ - 6, 10, 25, 3, 164, 5, 6, 7, 120, 3, - 0, 38, 37, 173, 38, 73, 38, 37, 38, 39, - 40, 41, 42, 43, 38, 73, 74, 38, 73, 74, - 190, 73, 74, 38, 194, 195, 37, 38, 38, 40, - 41, 42, 43, 73, 74, 205, 73, 207, 75, 74, - 74, 73, 164, 73, 74, 182, 183, 165, 166, 73, - 172, 173, 73, 74, 74, 38, 178, 38, 73, 74, - 38, 38, 73, 73, 73, 75, 76, 74, 190, 74, - 37, 75, 194, 195, 37, 74, 74, 74, 38, 95, - 99, 74, 101, 205, 40, 207, 37, 38, 39, 40, - 41, 42, 43, 37, 38, 40, 40, 41, 42, 43, - 74, 37, 38, 40, 40, 41, 42, 43, 74, 37, - 126, 127, 73, 235, 37, 38, 73, 40, 41, 42, - 43, 74, 73, 74, 73, 73, 38, 74, 74, 73, - 74, 74, 74, 39, 74, 74, 169, 73, 74, 37, - 38, 40, 40, 41, 42, 43, 40, 37, 37, 74, - 73, 103, 104, 105, 106, 107, 108, 74, 177, 65, - 66, 74, 68, 69, 70, 71, 72, 74, 73, 73, - 73, 38, 74, 74, 37, 75, 73, 73, 38, 74, - 38, 214, 74, 74, 222, 101, 74, 74, 74, 74, - 74, 74, 74, 74, 210, 201, 37, 211, 170, 17, - -1, -1, 221, 219, -1, -1, -1, 39, 224, 225, - -1, 227, 44, 45, 46, 47, 48, 49, 50, 51, - 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, - 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, - 72, 39, 74, -1, -1, -1, 44, 45, 46, 47, - 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, - 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, - 68, 69, 70, 71, 72, 39, -1, -1, -1, -1, - 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, - 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, - 64, 65, 66, 67, 68, 69, 70, 71, 72, 39, - -1, -1, -1, -1, 44, 45, 46, 47, 48, 49, - 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, - 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, - 70, 71, 72, 11, 12, 13, 14, 15, 16, 17, - 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, - 28, 29, 30, -1, 32, 33, 34, 35, 36 -}; - - /* YYSTOS[STATE-NUM] -- The (internal number of the) accessing - symbol of state STATE-NUM. */ -static const yytype_uint8 yystos[] = -{ - 0, 78, 79, 0, 73, 80, 11, 12, 13, 14, - 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, - 25, 26, 27, 28, 29, 30, 32, 33, 34, 35, - 36, 37, 38, 40, 41, 42, 43, 73, 84, 89, - 92, 98, 74, 38, 38, 38, 89, 90, 38, 38, - 74, 74, 74, 39, 65, 66, 68, 69, 70, 71, - 72, 103, 39, 44, 45, 46, 47, 48, 49, 50, - 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, - 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, - 71, 72, 102, 74, 74, 73, 37, 37, 38, 39, - 82, 102, 54, 55, 56, 57, 58, 59, 60, 61, - 62, 63, 64, 82, 101, 74, 40, 40, 74, 40, - 3, 5, 6, 7, 73, 75, 76, 92, 74, 37, - 73, 73, 73, 73, 74, 74, 74, 98, 74, 74, - 74, 38, 73, 83, 89, 74, 83, 38, 100, 100, - 100, 100, 100, 100, 100, 40, 40, 37, 37, 74, - 74, 74, 74, 73, 84, 73, 73, 73, 38, 98, - 98, 74, 86, 74, 99, 95, 97, 88, 73, 84, - 85, 73, 96, 96, 73, 94, 37, 91, 82, 97, - 74, 85, 85, 38, 74, 74, 96, 74, 98, 38, - 39, 73, 74, 87, 89, 84, 74, 38, 95, 95, - 38, 93, 37, 74, 81, 74, 85, 74, 85, 85, - 74, 88, 85, 85, 74, 74, 98, 74, 94, 74, - 82, 74, 74, 98, 74, 86, 74, 98, 98, 74, - 98, 74, 74, 74, 74, 74 -}; - - /* YYR1[YYN] -- Symbol number of symbol that rule YYN derives. */ -static const yytype_uint8 yyr1[] = -{ - 0, 77, 78, 79, 79, 80, 80, 80, 80, 80, - 80, 80, 80, 80, 80, 80, 80, 80, 80, 80, - 80, 80, 80, 80, 80, 80, 80, 80, 80, 80, - 80, 81, 81, 82, 82, 82, 82, 83, 83, 83, - 84, 84, 85, 85, 86, 86, 87, 87, 87, 87, - 88, 88, 89, 89, 89, 89, 89, 90, 90, 91, - 91, 92, 92, 93, 93, 94, 95, 95, 96, 97, - 97, 98, 98, 98, 98, 98, 98, 98, 99, 99, - 100, 101, 101, 101, 101, 101, 101, 101, 101, 101, - 101, 101, 101, 102, 102, 102, 102, 102, 102, 102, - 102, 102, 102, 102, 102, 102, 102, 102, 102, 102, - 102, 102, 102, 102, 102, 102, 102, 102, 102, 102, - 102, 102, 103, 103, 103, 103, 103, 103, 103, 103 -}; - - /* YYR2[YYN] -- Number of symbols on the right hand side of rule YYN. */ -static const yytype_uint8 yyr2[] = -{ - 0, 2, 1, 0, 2, 4, 4, 4, 5, 8, - 8, 7, 9, 4, 4, 4, 3, 3, 3, 3, - 4, 4, 4, 3, 7, 3, 4, 4, 4, 3, - 3, 0, 2, 1, 2, 1, 2, 1, 1, 3, - 1, 5, 1, 5, 2, 0, 1, 1, 1, 3, - 0, 2, 1, 1, 1, 1, 1, 1, 1, 2, - 1, 1, 5, 0, 2, 4, 0, 2, 4, 0, - 2, 1, 1, 5, 8, 8, 8, 6, 0, 2, - 1, 2, 2, 2, 2, 2, 2, 2, 2, 2, - 2, 2, 1, 1, 1, 1, 1, 1, 1, 1, - 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, - 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, - 1, 1, 1, 1, 1, 1, 1, 1, 1, 1 -}; - - -#define yyerrok (yyerrstatus = 0) -#define yyclearin (yychar = YYEMPTY) -#define YYEMPTY (-2) -#define YYEOF 0 - -#define YYACCEPT goto yyacceptlab -#define YYABORT goto yyabortlab -#define YYERROR goto yyerrorlab - - -#define YYRECOVERING() (!!yyerrstatus) - -#define YYBACKUP(Token, Value) \ -do \ - if (yychar == YYEMPTY) \ - { \ - yychar = (Token); \ - yylval = (Value); \ - YYPOPSTACK (yylen); \ - yystate = *yyssp; \ - goto yybackup; \ - } \ - else \ - { \ - yyerror (&yylloc, context, YY_("syntax error: cannot back up")); \ - YYERROR; \ - } \ -while (0) - -/* Error token number */ -#define YYTERROR 1 -#define YYERRCODE 256 - - -/* YYLLOC_DEFAULT -- Set CURRENT to span from RHS[1] to RHS[N]. - If N is 0, then set CURRENT to the empty location which ends - the previous symbol: RHS[0] (always defined). */ - -#ifndef YYLLOC_DEFAULT -# define YYLLOC_DEFAULT(Current, Rhs, N) \ - do \ - if (N) \ - { \ - (Current).first_line = YYRHSLOC (Rhs, 1).first_line; \ - (Current).first_column = YYRHSLOC (Rhs, 1).first_column; \ - (Current).last_line = YYRHSLOC (Rhs, N).last_line; \ - (Current).last_column = YYRHSLOC (Rhs, N).last_column; \ - } \ - else \ - { \ - (Current).first_line = (Current).last_line = \ - YYRHSLOC (Rhs, 0).last_line; \ - (Current).first_column = (Current).last_column = \ - YYRHSLOC (Rhs, 0).last_column; \ - } \ - while (0) -#endif - -#define YYRHSLOC(Rhs, K) ((Rhs)[K]) - - -/* Enable debugging if requested. */ -#if YYDEBUG - -# ifndef YYFPRINTF -# include /* INFRINGES ON USER NAME SPACE */ -# define YYFPRINTF fprintf -# endif - -# define YYDPRINTF(Args) \ -do { \ - if (yydebug) \ - YYFPRINTF Args; \ -} while (0) - - -/* YY_LOCATION_PRINT -- Print the location on the stream. - This macro was not mandated originally: define only if we know - we won't break user code: when these are the locations we know. */ - -#ifndef YY_LOCATION_PRINT -# if defined YYLTYPE_IS_TRIVIAL && YYLTYPE_IS_TRIVIAL - -/* Print *YYLOCP on YYO. Private, do not rely on its existence. */ - -YY_ATTRIBUTE_UNUSED -static unsigned -yy_location_print_ (FILE *yyo, YYLTYPE const * const yylocp) -{ - unsigned res = 0; - int end_col = 0 != yylocp->last_column ? yylocp->last_column - 1 : 0; - if (0 <= yylocp->first_line) - { - res += YYFPRINTF (yyo, "%d", yylocp->first_line); - if (0 <= yylocp->first_column) - res += YYFPRINTF (yyo, ".%d", yylocp->first_column); - } - if (0 <= yylocp->last_line) - { - if (yylocp->first_line < yylocp->last_line) - { - res += YYFPRINTF (yyo, "-%d", yylocp->last_line); - if (0 <= end_col) - res += YYFPRINTF (yyo, ".%d", end_col); - } - else if (0 <= end_col && yylocp->first_column < end_col) - res += YYFPRINTF (yyo, "-%d", end_col); - } - return res; - } - -# define YY_LOCATION_PRINT(File, Loc) \ - yy_location_print_ (File, &(Loc)) - -# else -# define YY_LOCATION_PRINT(File, Loc) ((void) 0) -# endif -#endif - - -# define YY_SYMBOL_PRINT(Title, Type, Value, Location) \ -do { \ - if (yydebug) \ - { \ - YYFPRINTF (stderr, "%s ", Title); \ - yy_symbol_print (stderr, \ - Type, Value, Location, context); \ - YYFPRINTF (stderr, "\n"); \ - } \ -} while (0) - - -/*----------------------------------------. -| Print this symbol's value on YYOUTPUT. | -`----------------------------------------*/ - -static void -yy_symbol_value_print (FILE *yyoutput, int yytype, YYSTYPE const * const yyvaluep, YYLTYPE const * const yylocationp, Smt2newContext* context) -{ - FILE *yyo = yyoutput; - YYUSE (yyo); - YYUSE (yylocationp); - YYUSE (context); - if (!yyvaluep) - return; -# ifdef YYPRINT - if (yytype < YYNTOKENS) - YYPRINT (yyoutput, yytoknum[yytype], *yyvaluep); -# endif - YYUSE (yytype); -} - - -/*--------------------------------. -| Print this symbol on YYOUTPUT. | -`--------------------------------*/ - -static void -yy_symbol_print (FILE *yyoutput, int yytype, YYSTYPE const * const yyvaluep, YYLTYPE const * const yylocationp, Smt2newContext* context) -{ - YYFPRINTF (yyoutput, "%s %s (", - yytype < YYNTOKENS ? "token" : "nterm", yytname[yytype]); - - YY_LOCATION_PRINT (yyoutput, *yylocationp); - YYFPRINTF (yyoutput, ": "); - yy_symbol_value_print (yyoutput, yytype, yyvaluep, yylocationp, context); - YYFPRINTF (yyoutput, ")"); -} - -/*------------------------------------------------------------------. -| yy_stack_print -- Print the state stack from its BOTTOM up to its | -| TOP (included). | -`------------------------------------------------------------------*/ - -static void -yy_stack_print (yytype_int16 *yybottom, yytype_int16 *yytop) -{ - YYFPRINTF (stderr, "Stack now"); - for (; yybottom <= yytop; yybottom++) - { - int yybot = *yybottom; - YYFPRINTF (stderr, " %d", yybot); - } - YYFPRINTF (stderr, "\n"); -} - -# define YY_STACK_PRINT(Bottom, Top) \ -do { \ - if (yydebug) \ - yy_stack_print ((Bottom), (Top)); \ -} while (0) - - -/*------------------------------------------------. -| Report that the YYRULE is going to be reduced. | -`------------------------------------------------*/ - -static void -yy_reduce_print (yytype_int16 *yyssp, YYSTYPE *yyvsp, YYLTYPE *yylsp, int yyrule, Smt2newContext* context) -{ - unsigned long int yylno = yyrline[yyrule]; - int yynrhs = yyr2[yyrule]; - int yyi; - YYFPRINTF (stderr, "Reducing stack by rule %d (line %lu):\n", - yyrule - 1, yylno); - /* The symbols being reduced. */ - for (yyi = 0; yyi < yynrhs; yyi++) - { - YYFPRINTF (stderr, " $%d = ", yyi + 1); - yy_symbol_print (stderr, - yystos[yyssp[yyi + 1 - yynrhs]], - &(yyvsp[(yyi + 1) - (yynrhs)]) - , &(yylsp[(yyi + 1) - (yynrhs)]) , context); - YYFPRINTF (stderr, "\n"); - } -} - -# define YY_REDUCE_PRINT(Rule) \ -do { \ - if (yydebug) \ - yy_reduce_print (yyssp, yyvsp, yylsp, Rule, context); \ -} while (0) - -/* Nonzero means print parse trace. It is left uninitialized so that - multiple parsers can coexist. */ -int yydebug; -#else /* !YYDEBUG */ -# define YYDPRINTF(Args) -# define YY_SYMBOL_PRINT(Title, Type, Value, Location) -# define YY_STACK_PRINT(Bottom, Top) -# define YY_REDUCE_PRINT(Rule) -#endif /* !YYDEBUG */ - - -/* YYINITDEPTH -- initial size of the parser's stacks. */ -#ifndef YYINITDEPTH -# define YYINITDEPTH 200 -#endif - -/* YYMAXDEPTH -- maximum size the stacks can grow to (effective only - if the built-in stack extension method is used). - - Do not make this value too large; the results are undefined if - YYSTACK_ALLOC_MAXIMUM < YYSTACK_BYTES (YYMAXDEPTH) - evaluated with infinite-precision integer arithmetic. */ - -#ifndef YYMAXDEPTH -# define YYMAXDEPTH 10000 -#endif - - -#if YYERROR_VERBOSE - -# ifndef yystrlen -# if defined __GLIBC__ && defined _STRING_H -# define yystrlen strlen -# else -/* Return the length of YYSTR. */ -static YYSIZE_T -yystrlen (const char *yystr) -{ - YYSIZE_T yylen; - for (yylen = 0; yystr[yylen]; yylen++) - continue; - return yylen; -} -# endif -# endif - -# ifndef yystpcpy -# if defined __GLIBC__ && defined _STRING_H && defined _GNU_SOURCE -# define yystpcpy stpcpy -# else -/* Copy YYSRC to YYDEST, returning the address of the terminating '\0' in - YYDEST. */ -static char * -yystpcpy (char *yydest, const char *yysrc) -{ - char *yyd = yydest; - const char *yys = yysrc; - - while ((*yyd++ = *yys++) != '\0') - continue; - - return yyd - 1; -} -# endif -# endif - -# ifndef yytnamerr -/* Copy to YYRES the contents of YYSTR after stripping away unnecessary - quotes and backslashes, so that it's suitable for yyerror. The - heuristic is that double-quoting is unnecessary unless the string - contains an apostrophe, a comma, or backslash (other than - backslash-backslash). YYSTR is taken from yytname. If YYRES is - null, do not copy; instead, return the length of what the result - would have been. */ -static YYSIZE_T -yytnamerr (char *yyres, const char *yystr) -{ - if (*yystr == '"') - { - YYSIZE_T yyn = 0; - char const *yyp = yystr; - - for (;;) - switch (*++yyp) - { - case '\'': - case ',': - goto do_not_strip_quotes; - - case '\\': - if (*++yyp != '\\') - goto do_not_strip_quotes; - /* Fall through. */ - default: - if (yyres) - yyres[yyn] = *yyp; - yyn++; - break; - - case '"': - if (yyres) - yyres[yyn] = '\0'; - return yyn; - } - do_not_strip_quotes: ; - } - - if (! yyres) - return yystrlen (yystr); - - return yystpcpy (yyres, yystr) - yyres; -} -# endif - -/* Copy into *YYMSG, which is of size *YYMSG_ALLOC, an error message - about the unexpected token YYTOKEN for the state stack whose top is - YYSSP. - - Return 0 if *YYMSG was successfully written. Return 1 if *YYMSG is - not large enough to hold the message. In that case, also set - *YYMSG_ALLOC to the required number of bytes. Return 2 if the - required number of bytes is too large to store. */ -static int -yysyntax_error (YYSIZE_T *yymsg_alloc, char **yymsg, - yytype_int16 *yyssp, int yytoken) -{ - YYSIZE_T yysize0 = yytnamerr (YY_NULLPTR, yytname[yytoken]); - YYSIZE_T yysize = yysize0; - enum { YYERROR_VERBOSE_ARGS_MAXIMUM = 5 }; - /* Internationalized format string. */ - const char *yyformat = YY_NULLPTR; - /* Arguments of yyformat. */ - char const *yyarg[YYERROR_VERBOSE_ARGS_MAXIMUM]; - /* Number of reported tokens (one for the "unexpected", one per - "expected"). */ - int yycount = 0; - - /* There are many possibilities here to consider: - - If this state is a consistent state with a default action, then - the only way this function was invoked is if the default action - is an error action. In that case, don't check for expected - tokens because there are none. - - The only way there can be no lookahead present (in yychar) is if - this state is a consistent state with a default action. Thus, - detecting the absence of a lookahead is sufficient to determine - that there is no unexpected or expected token to report. In that - case, just report a simple "syntax error". - - Don't assume there isn't a lookahead just because this state is a - consistent state with a default action. There might have been a - previous inconsistent state, consistent state with a non-default - action, or user semantic action that manipulated yychar. - - Of course, the expected token list depends on states to have - correct lookahead information, and it depends on the parser not - to perform extra reductions after fetching a lookahead from the - scanner and before detecting a syntax error. Thus, state merging - (from LALR or IELR) and default reductions corrupt the expected - token list. However, the list is correct for canonical LR with - one exception: it will still contain any token that will not be - accepted due to an error action in a later state. - */ - if (yytoken != YYEMPTY) - { - int yyn = yypact[*yyssp]; - yyarg[yycount++] = yytname[yytoken]; - if (!yypact_value_is_default (yyn)) - { - /* Start YYX at -YYN if negative to avoid negative indexes in - YYCHECK. In other words, skip the first -YYN actions for - this state because they are default actions. */ - int yyxbegin = yyn < 0 ? -yyn : 0; - /* Stay within bounds of both yycheck and yytname. */ - int yychecklim = YYLAST - yyn + 1; - int yyxend = yychecklim < YYNTOKENS ? yychecklim : YYNTOKENS; - int yyx; - - for (yyx = yyxbegin; yyx < yyxend; ++yyx) - if (yycheck[yyx + yyn] == yyx && yyx != YYTERROR - && !yytable_value_is_error (yytable[yyx + yyn])) - { - if (yycount == YYERROR_VERBOSE_ARGS_MAXIMUM) - { - yycount = 1; - yysize = yysize0; - break; - } - yyarg[yycount++] = yytname[yyx]; - { - YYSIZE_T yysize1 = yysize + yytnamerr (YY_NULLPTR, yytname[yyx]); - if (! (yysize <= yysize1 - && yysize1 <= YYSTACK_ALLOC_MAXIMUM)) - return 2; - yysize = yysize1; - } - } - } - } - - switch (yycount) - { -# define YYCASE_(N, S) \ - case N: \ - yyformat = S; \ - break - YYCASE_(0, YY_("syntax error")); - YYCASE_(1, YY_("syntax error, unexpected %s")); - YYCASE_(2, YY_("syntax error, unexpected %s, expecting %s")); - YYCASE_(3, YY_("syntax error, unexpected %s, expecting %s or %s")); - YYCASE_(4, YY_("syntax error, unexpected %s, expecting %s or %s or %s")); - YYCASE_(5, YY_("syntax error, unexpected %s, expecting %s or %s or %s or %s")); -# undef YYCASE_ - } - - { - YYSIZE_T yysize1 = yysize + yystrlen (yyformat); - if (! (yysize <= yysize1 && yysize1 <= YYSTACK_ALLOC_MAXIMUM)) - return 2; - yysize = yysize1; - } - - if (*yymsg_alloc < yysize) - { - *yymsg_alloc = 2 * yysize; - if (! (yysize <= *yymsg_alloc - && *yymsg_alloc <= YYSTACK_ALLOC_MAXIMUM)) - *yymsg_alloc = YYSTACK_ALLOC_MAXIMUM; - return 1; - } - - /* Avoid sprintf, as that infringes on the user's name space. - Don't have undefined behavior even if the translation - produced a string with the wrong number of "%s"s. */ - { - char *yyp = *yymsg; - int yyi = 0; - while ((*yyp = *yyformat) != '\0') - if (*yyp == '%' && yyformat[1] == 's' && yyi < yycount) - { - yyp += yytnamerr (yyp, yyarg[yyi++]); - yyformat += 2; - } - else - { - yyp++; - yyformat++; - } - } - return 0; -} -#endif /* YYERROR_VERBOSE */ - -/*-----------------------------------------------. -| Release the memory associated to this symbol. | -`-----------------------------------------------*/ - -static void -yydestruct (const char *yymsg, int yytype, YYSTYPE *yyvaluep, YYLTYPE *yylocationp, Smt2newContext* context) -{ - YYUSE (yyvaluep); - YYUSE (yylocationp); - YYUSE (context); - if (!yymsg) - yymsg = "Deleting"; - YY_SYMBOL_PRINT (yymsg, yytype, yyvaluep, yylocationp); - - YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN - YYUSE (yytype); - YY_IGNORE_MAYBE_UNINITIALIZED_END -} - - - - -/*----------. -| yyparse. | -`----------*/ - -int -yyparse (Smt2newContext* context) -{ -/* The lookahead symbol. */ -int yychar; - - -/* The semantic value of the lookahead symbol. */ -/* Default value used for initialization, for pacifying older GCCs - or non-GCC compilers. */ -YY_INITIAL_VALUE (static YYSTYPE yyval_default;) -YYSTYPE yylval YY_INITIAL_VALUE (= yyval_default); - -/* Location data for the lookahead symbol. */ -static YYLTYPE yyloc_default -# if defined YYLTYPE_IS_TRIVIAL && YYLTYPE_IS_TRIVIAL - = { 1, 1, 1, 1 } -# endif -; -YYLTYPE yylloc = yyloc_default; - - /* Number of syntax errors so far. */ - int yynerrs; - - int yystate; - /* Number of tokens to shift before error messages enabled. */ - int yyerrstatus; - - /* The stacks and their tools: - 'yyss': related to states. - 'yyvs': related to semantic values. - 'yyls': related to locations. - - Refer to the stacks through separate pointers, to allow yyoverflow - to reallocate them elsewhere. */ - - /* The state stack. */ - yytype_int16 yyssa[YYINITDEPTH]; - yytype_int16 *yyss; - yytype_int16 *yyssp; - - /* The semantic value stack. */ - YYSTYPE yyvsa[YYINITDEPTH]; - YYSTYPE *yyvs; - YYSTYPE *yyvsp; - - /* The location stack. */ - YYLTYPE yylsa[YYINITDEPTH]; - YYLTYPE *yyls; - YYLTYPE *yylsp; - - /* The locations where the error started and ended. */ - YYLTYPE yyerror_range[3]; - - YYSIZE_T yystacksize; - - int yyn; - int yyresult; - /* Lookahead token as an internal (translated) token number. */ - int yytoken = 0; - /* The variables used to return semantic value and location from the - action routines. */ - YYSTYPE yyval; - YYLTYPE yyloc; - -#if YYERROR_VERBOSE - /* Buffer for error messages, and its allocated size. */ - char yymsgbuf[128]; - char *yymsg = yymsgbuf; - YYSIZE_T yymsg_alloc = sizeof yymsgbuf; -#endif - -#define YYPOPSTACK(N) (yyvsp -= (N), yyssp -= (N), yylsp -= (N)) - - /* The number of symbols on the RHS of the reduced rule. - Keep to zero when no symbol should be popped. */ - int yylen = 0; - - yyssp = yyss = yyssa; - yyvsp = yyvs = yyvsa; - yylsp = yyls = yylsa; - yystacksize = YYINITDEPTH; - - YYDPRINTF ((stderr, "Starting parse\n")); - - yystate = 0; - yyerrstatus = 0; - yynerrs = 0; - yychar = YYEMPTY; /* Cause a token to be read. */ - yylsp[0] = yylloc; - goto yysetstate; - -/*------------------------------------------------------------. -| yynewstate -- Push a new state, which is found in yystate. | -`------------------------------------------------------------*/ - yynewstate: - /* In all cases, when you get here, the value and location stacks - have just been pushed. So pushing a state here evens the stacks. */ - yyssp++; - - yysetstate: - *yyssp = yystate; - - if (yyss + yystacksize - 1 <= yyssp) - { - /* Get the current used size of the three stacks, in elements. */ - YYSIZE_T yysize = yyssp - yyss + 1; - -#ifdef yyoverflow - { - /* Give user a chance to reallocate the stack. Use copies of - these so that the &'s don't force the real ones into - memory. */ - YYSTYPE *yyvs1 = yyvs; - yytype_int16 *yyss1 = yyss; - YYLTYPE *yyls1 = yyls; - - /* Each stack pointer address is followed by the size of the - data in use in that stack, in bytes. This used to be a - conditional around just the two extra args, but that might - be undefined if yyoverflow is a macro. */ - yyoverflow (YY_("memory exhausted"), - &yyss1, yysize * sizeof (*yyssp), - &yyvs1, yysize * sizeof (*yyvsp), - &yyls1, yysize * sizeof (*yylsp), - &yystacksize); - - yyls = yyls1; - yyss = yyss1; - yyvs = yyvs1; - } -#else /* no yyoverflow */ -# ifndef YYSTACK_RELOCATE - goto yyexhaustedlab; -# else - /* Extend the stack our own way. */ - if (YYMAXDEPTH <= yystacksize) - goto yyexhaustedlab; - yystacksize *= 2; - if (YYMAXDEPTH < yystacksize) - yystacksize = YYMAXDEPTH; - - { - yytype_int16 *yyss1 = yyss; - union yyalloc *yyptr = - (union yyalloc *) YYSTACK_ALLOC (YYSTACK_BYTES (yystacksize)); - if (! yyptr) - goto yyexhaustedlab; - YYSTACK_RELOCATE (yyss_alloc, yyss); - YYSTACK_RELOCATE (yyvs_alloc, yyvs); - YYSTACK_RELOCATE (yyls_alloc, yyls); -# undef YYSTACK_RELOCATE - if (yyss1 != yyssa) - YYSTACK_FREE (yyss1); - } -# endif -#endif /* no yyoverflow */ - - yyssp = yyss + yysize - 1; - yyvsp = yyvs + yysize - 1; - yylsp = yyls + yysize - 1; - - YYDPRINTF ((stderr, "Stack size increased to %lu\n", - (unsigned long int) yystacksize)); - - if (yyss + yystacksize - 1 <= yyssp) - YYABORT; - } - - YYDPRINTF ((stderr, "Entering state %d\n", yystate)); - - if (yystate == YYFINAL) - YYACCEPT; - - goto yybackup; - -/*-----------. -| yybackup. | -`-----------*/ -yybackup: - - /* Do appropriate processing given the current state. Read a - lookahead token if we need one and don't already have one. */ - - /* First try to decide what to do without reference to lookahead token. */ - yyn = yypact[yystate]; - if (yypact_value_is_default (yyn)) - goto yydefault; - - /* Not known => get a lookahead token if don't already have one. */ - - /* YYCHAR is either YYEMPTY or YYEOF or a valid lookahead symbol. */ - if (yychar == YYEMPTY) - { - YYDPRINTF ((stderr, "Reading a token: ")); - yychar = yylex (&yylval, &yylloc, scanner); - } - - if (yychar <= YYEOF) - { - yychar = yytoken = YYEOF; - YYDPRINTF ((stderr, "Now at end of input.\n")); - } - else - { - yytoken = YYTRANSLATE (yychar); - YY_SYMBOL_PRINT ("Next token is", yytoken, &yylval, &yylloc); - } - - /* If the proper action on seeing token YYTOKEN is to reduce or to - detect an error, take that action. */ - yyn += yytoken; - if (yyn < 0 || YYLAST < yyn || yycheck[yyn] != yytoken) - goto yydefault; - yyn = yytable[yyn]; - if (yyn <= 0) - { - if (yytable_value_is_error (yyn)) - goto yyerrlab; - yyn = -yyn; - goto yyreduce; - } - - /* Count tokens shifted since error; after three, turn off error - status. */ - if (yyerrstatus) - yyerrstatus--; - - /* Shift the lookahead token. */ - YY_SYMBOL_PRINT ("Shifting", yytoken, &yylval, &yylloc); - - /* Discard the shifted token. */ - yychar = YYEMPTY; - - yystate = yyn; - YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN - *++yyvsp = yylval; - YY_IGNORE_MAYBE_UNINITIALIZED_END - *++yylsp = yylloc; - goto yynewstate; - - -/*-----------------------------------------------------------. -| yydefault -- do the default action for the current state. | -`-----------------------------------------------------------*/ -yydefault: - yyn = yydefact[yystate]; - if (yyn == 0) - goto yyerrlab; - goto yyreduce; - - -/*-----------------------------. -| yyreduce -- Do a reduction. | -`-----------------------------*/ -yyreduce: - /* yyn is the number of a rule to reduce with. */ - yylen = yyr2[yyn]; - - /* If YYLEN is nonzero, implement the default value of the action: - '$$ = $1'. - - Otherwise, the following line sets YYVAL to garbage. - This behavior is undocumented and Bison - users should not rely upon it. Assigning to YYVAL - unconditionally makes the parser a bit smaller, and it avoids a - GCC warning that YYVAL may be used uninitialized. */ - yyval = yyvsp[1-yylen]; - - /* Default location. */ - YYLLOC_DEFAULT (yyloc, (yylsp - yylen), yylen); - YY_REDUCE_PRINT (yyn); - switch (yyn) - { - case 2: -#line 97 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { ASTNode *n = new ASTNode(CMDL_T, strdup("main-script")); n->children = (yyvsp[0].snode_list); context->insertRoot(n); } -#line 1642 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 3: -#line 101 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.snode_list) = new std::list(); } -#line 1648 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 4: -#line 103 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (*(yyvsp[-1].snode_list)).push_back((yyvsp[0].snode)); (yyval.snode_list) = (yyvsp[-1].snode_list); } -#line 1654 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 5: -#line 107 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(CMD_T, (yyvsp[-2].tok)); - (yyval.snode)->children = new std::list(); - (yyval.snode)->children->push_back(new ASTNode(SYM_T, (yyvsp[-1].str))); - } -#line 1664 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 6: -#line 113 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(CMD_T, (yyvsp[-2].tok)); - (yyval.snode)->children = new std::list(); - (yyval.snode)->children->push_back((yyvsp[-1].snode)); - } -#line 1674 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 7: -#line 119 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(CMD_T, (yyvsp[-2].tok)); - (yyval.snode)->children = new std::list(); - (yyval.snode)->children->push_back((yyvsp[-1].snode)); - } -#line 1684 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 8: -#line 125 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(CMD_T, (yyvsp[-3].tok)); - (yyval.snode)->children = new std::list(); - (yyval.snode)->children->push_back(new ASTNode(SYM_T, (yyvsp[-2].str))); - (yyval.snode)->children->push_back(new ASTNode(NUM_T, (yyvsp[-1].str))); - } -#line 1695 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 9: -#line 132 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(CMD_T, (yyvsp[-6].tok)); - (yyval.snode)->children = new std::list(); - (yyval.snode)->children->push_back(new ASTNode(SYM_T, (yyvsp[-5].str))); - - ASTNode* syml = new ASTNode(SYML_T, NULL); - syml->children = (yyvsp[-3].snode_list); - (yyval.snode)->children->push_back(syml); - - (yyval.snode)->children->push_back((yyvsp[-1].snode)); - } -#line 1711 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 10: -#line 145 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(CMD_T, (yyvsp[-6].tok)); - (yyval.snode)->children = new std::list(); - (yyval.snode)->children->push_back(new ASTNode(SYM_T, (yyvsp[-5].str))); - - ASTNode* sortl = new ASTNode(SORTL_T, NULL); - sortl->children = (yyvsp[-3].snode_list); - (yyval.snode)->children->push_back(sortl); - - (yyval.snode)->children->push_back((yyvsp[-1].snode)); - } -#line 1727 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 11: -#line 157 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(CMD_T, (yyvsp[-5].tok)); - (yyval.snode)->children = new std::list(); - (yyval.snode)->children->push_back((yyvsp[-4].snode)); - - ASTNode* sortl = new ASTNode(SORTL_T, NULL); - sortl->children = new std::list(); - (yyval.snode)->children->push_back(sortl); - - (yyval.snode)->children->push_back((yyvsp[-1].snode)); - } -#line 1743 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 12: -#line 169 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(CMD_T, (yyvsp[-7].tok)); - (yyval.snode)->children = new std::list(); - (yyval.snode)->children->push_back(new ASTNode(SYM_T, (yyvsp[-6].str))); - - ASTNode* svl = new ASTNode(SVL_T, NULL); - svl->children = (yyvsp[-4].snode_list); - (yyval.snode)->children->push_back(svl); - - (yyval.snode)->children->push_back((yyvsp[-2].snode)); - (yyval.snode)->children->push_back((yyvsp[-1].snode)); - } -#line 1760 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 13: -#line 182 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(CMD_T, (yyvsp[-2].tok)); - (yyval.snode)->children = new std::list(); - (yyval.snode)->children->push_back(new ASTNode(NUM_T, (yyvsp[-1].str))); - } -#line 1770 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 14: -#line 188 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(CMD_T, (yyvsp[-2].tok)); - (yyval.snode)->children = new std::list(); - (yyval.snode)->children->push_back(new ASTNode(NUM_T, (yyvsp[-1].str))); - } -#line 1780 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 15: -#line 194 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(CMD_T, (yyvsp[-2].tok)); - (yyval.snode)->children = new std::list(); - (yyval.snode)->children->push_back((yyvsp[-1].snode)); - } -#line 1790 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 16: -#line 200 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(CMD_T, (yyvsp[-1].tok)); - } -#line 1798 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 17: -#line 204 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(CMD_T, (yyvsp[-1].tok)); - } -#line 1806 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 18: -#line 208 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(CMD_T, (yyvsp[-1].tok)); - } -#line 1814 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 19: -#line 212 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(CMD_T, (yyvsp[-1].tok)); - } -#line 1822 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 20: -#line 216 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(CMD_T, (yyvsp[-2].tok)); - (yyval.snode)->children = new std::list(); - (yyval.snode)->children->push_back(new ASTNode(UATTR_T, (yyvsp[-1].str))); - } -#line 1832 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 21: -#line 222 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(CMD_T, (yyvsp[-2].tok)); - (yyval.snode)->children = new std::list(); - (yyval.snode)->children->push_back(new ASTNode(UATTR_T, (yyvsp[-1].str))); - } -#line 1842 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 22: -#line 228 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(CMD_T, (yyvsp[-2].tok)); - (yyval.snode)->children = new std::list(); - (yyval.snode)->children->push_back(new ASTNode(UATTR_T, (yyvsp[-1].str))); - } -#line 1852 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 23: -#line 234 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(CMD_T, (yyvsp[-1].tok)); - } -#line 1860 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 24: -#line 238 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(CMD_T, (yyvsp[-5].tok)); - (yyval.snode)->children = (yyvsp[-2].snode_list); - (yyval.snode)->children->push_front((yyvsp[-3].snode)); - } -#line 1870 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 25: -#line 244 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(CMD_T, (yyvsp[-1].tok)); - } -#line 1878 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 26: -#line 248 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(CMD_T, (yyvsp[-2].tok)); - (yyval.snode)->children = new std::list(); - (yyval.snode)->children->push_back(new ASTNode(UATTR_T, (yyvsp[-1].str))); - } -#line 1888 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 27: -#line 254 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(CMD_T, (yyvsp[-2].tok)); - (yyval.snode)->children = new std::list(); - (yyval.snode)->children->push_back(new ASTNode(PATTR_T, (yyvsp[-1].str))); - } -#line 1898 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 28: -#line 260 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(CMD_T, (yyvsp[-2].tok)); - (yyval.snode)->children = new std::list(); - (yyval.snode)->children->push_back((yyvsp[-1].snode)); - } -#line 1908 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 29: -#line 266 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(CMD_T, (yyvsp[-1].tok)); - } -#line 1916 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 30: -#line 270 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.snode) = new ASTNode(CMD_T, (yyvsp[-1].tok)); } -#line 1922 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 31: -#line 274 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.snode_list) = new std::list(); } -#line 1928 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 32: -#line 276 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyvsp[-1].snode_list)->push_back((yyvsp[0].snode)); (yyval.snode_list) = (yyvsp[-1].snode_list); } -#line 1934 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 33: -#line 280 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.snode) = new ASTNode(UATTR_T, (yyvsp[0].str)); } -#line 1940 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 34: -#line 282 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.snode) = new ASTNode(UATTR_T, (yyvsp[-1].str)); (yyval.snode)->children = new std::list(); (yyval.snode)->children->push_back((yyvsp[0].snode)); } -#line 1946 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 35: -#line 284 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.snode) = new ASTNode(PATTR_T, (yyvsp[0].str)); } -#line 1952 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 36: -#line 286 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.snode) = new ASTNode(PATTR_T, (yyvsp[-1].str)); (yyval.snode)->children = new std::list(); (yyval.snode)->children->push_back((yyvsp[0].snode)); } -#line 1958 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 37: -#line 290 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.snode) = new ASTNode(SPECC_T, NULL); (yyval.snode)->children = new std::list(); (yyval.snode)->children->push_back((yyvsp[0].snode)); } -#line 1964 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 38: -#line 292 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(SYM_T, (yyvsp[0].str)); - } -#line 1972 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 39: -#line 296 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(SEXPRL_T, NULL); - (yyval.snode)->children = (yyvsp[-1].snode_list); - } -#line 1981 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 40: -#line 303 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.snode) = new ASTNode(SYM_T, (yyvsp[0].str)); } -#line 1987 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 41: -#line 305 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.snode) = new ASTNode(SYM_T, (yyvsp[-2].str)); (yyval.snode)->children = (yyvsp[-1].snode_list); } -#line 1993 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 42: -#line 309 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.snode) = new ASTNode(ID_T, NULL); (yyval.snode)->children = new std::list(); (yyval.snode)->children->push_back((yyvsp[0].snode)); } -#line 1999 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 43: -#line 311 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(LID_T, NULL); - (yyval.snode)->children = (yyvsp[-1].snode_list); - (yyval.snode)->children->push_front((yyvsp[-2].snode)); - } -#line 2009 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 44: -#line 319 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyvsp[-1].snode_list)->push_back((yyvsp[0].snode)); (yyval.snode_list) = (yyvsp[-1].snode_list); } -#line 2015 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 45: -#line 321 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.snode_list) = new std::list(); } -#line 2021 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 46: -#line 325 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(SPECC_T, NULL); - (yyval.snode)->children = new std::list(); - (yyval.snode)->children->push_back((yyvsp[0].snode)); - } -#line 2031 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 47: -#line 331 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(SYM_T, (yyvsp[0].str)); - } -#line 2039 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 48: -#line 335 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(UATTR_T, (yyvsp[0].str)); - } -#line 2047 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 49: -#line 339 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(SEXPRL_T, NULL); - (yyval.snode)->children = (yyvsp[-1].snode_list); - } -#line 2056 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 50: -#line 346 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode_list) = new std::list(); - } -#line 2064 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 51: -#line 350 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyvsp[-1].snode_list)->push_back((yyvsp[0].snode)); - (yyval.snode_list) = (yyvsp[-1].snode_list); - } -#line 2073 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 52: -#line 358 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.snode) = new ASTNode(NUM_T, (yyvsp[0].str)); } -#line 2079 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 53: -#line 360 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.snode) = new ASTNode(DEC_T, (yyvsp[0].str)); } -#line 2085 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 54: -#line 362 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.snode) = new ASTNode(HEX_T, (yyvsp[0].str)); } -#line 2091 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 55: -#line 364 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.snode) = new ASTNode(BIN_T, (yyvsp[0].str)); } -#line 2097 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 56: -#line 366 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.snode) = new ASTNode(STR_T, (yyvsp[0].str)); } -#line 2103 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 57: -#line 370 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.snode) = new ASTNode(SYM_T, (yyvsp[0].str)); } -#line 2109 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 58: -#line 372 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.snode) = (yyvsp[0].snode); } -#line 2115 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 59: -#line 376 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyvsp[-1].snode_list)->push_back(new ASTNode(NUM_T, (yyvsp[0].str))); (yyval.snode_list) = (yyvsp[-1].snode_list); } -#line 2121 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 60: -#line 378 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.snode_list) = new std::list(); (yyval.snode_list)->push_back(new ASTNode(NUM_T, (yyvsp[0].str))); } -#line 2127 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 61: -#line 382 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.snode) = (yyvsp[0].snode); } -#line 2133 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 62: -#line 384 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(AS_T, NULL); - (yyval.snode)->children = new std::list(); - (yyval.snode)->children->push_back((yyvsp[-2].snode)); - (yyval.snode)->children->push_back((yyvsp[-1].snode)); - } -#line 2144 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 63: -#line 393 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.snode_list) = new std::list(); } -#line 2150 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 64: -#line 395 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyvsp[-1].snode_list)->push_back((yyvsp[0].snode)); (yyval.snode_list) = (yyvsp[-1].snode_list); } -#line 2156 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 65: -#line 399 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.snode) = new ASTNode(VARB_T, (yyvsp[-2].str)); (yyval.snode)->children = new std::list(); (yyval.snode)->children->push_back((yyvsp[-1].snode)); } -#line 2162 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 66: -#line 403 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.snode_list) = new std::list(); } -#line 2168 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 67: -#line 405 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyvsp[-1].snode_list)->push_back((yyvsp[0].snode)); (yyval.snode_list) = (yyvsp[-1].snode_list); } -#line 2174 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 68: -#line 409 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.snode) = new ASTNode(SV_T, (yyvsp[-2].str)); (yyval.snode)->children = new std::list(); (yyval.snode)->children->push_back((yyvsp[-1].snode)); } -#line 2180 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 69: -#line 412 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.snode_list) = new std::list(); } -#line 2186 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 70: -#line 414 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyvsp[-1].snode_list)->push_back((yyvsp[0].snode)); (yyval.snode_list) = (yyvsp[-1].snode_list); } -#line 2192 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 71: -#line 418 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.snode) = new ASTNode(TERM_T, NULL); (yyval.snode)->children = new std::list(); (yyval.snode)->children->push_back((yyvsp[0].snode)); } -#line 2198 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 72: -#line 420 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.snode) = new ASTNode(QID_T, NULL); (yyval.snode)->children = new std::list(); (yyval.snode)->children->push_back((yyvsp[0].snode)); } -#line 2204 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 73: -#line 422 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(LQID_T, NULL); - (yyval.snode)->children = (yyvsp[-1].snode_list); - (yyval.snode)->children->push_front((yyvsp[-2].snode)); - (yyval.snode)->children->push_front((yyvsp[-3].snode)); - } -#line 2215 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 74: -#line 429 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(LET_T, NULL); - (yyval.snode)->children = new std::list(); - (yyvsp[-3].snode_list)->push_front((yyvsp[-4].snode)); - ASTNode* vbl = new ASTNode(VARBL_T, NULL); - vbl->children = (yyvsp[-3].snode_list); - (yyval.snode)->children->push_back(vbl); - (yyval.snode)->children->push_back((yyvsp[-1].snode)); - } -#line 2229 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 75: -#line 439 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(FORALL_T, NULL); - (yyval.snode)->children = new std::list(); - (yyvsp[-3].snode_list)->push_front((yyvsp[-4].snode)); - ASTNode* svl = new ASTNode(SVL_T, NULL); - svl->children = (yyvsp[-3].snode_list); - (yyval.snode)->children->push_back(svl); - (yyval.snode)->children->push_back((yyvsp[-1].snode)); - } -#line 2243 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 76: -#line 449 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(EXISTS_T, NULL); - (yyval.snode)->children = new std::list(); - (yyvsp[-3].snode_list)->push_front((yyvsp[-4].snode)); - ASTNode* svl = new ASTNode(SVL_T, NULL); - svl->children = (yyvsp[-3].snode_list); - (yyval.snode)->children->push_back(svl); - (yyval.snode)->children->push_back((yyvsp[-1].snode)); - } -#line 2257 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 77: -#line 459 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(BANG_T, NULL); - (yyval.snode)->children = new std::list(); - (yyval.snode)->children->push_front((yyvsp[-3].snode)); - ASTNode *atrs = new ASTNode(GATTRL_T, NULL); - (yyvsp[-1].snode_list)->push_front((yyvsp[-2].snode)); - atrs->children = (yyvsp[-1].snode_list); - (yyval.snode)->children->push_back(atrs); - } -#line 2271 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 78: -#line 535 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.snode_list) = new std::list(); } -#line 2277 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 79: -#line 537 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyvsp[-1].snode_list)->push_back(new ASTNode(SYM_T, (yyvsp[0].str))); (yyval.snode_list) = (yyvsp[-1].snode_list); } -#line 2283 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 80: -#line 694 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - if (strcmp((yyvsp[0].str), "true") == 0) - (yyval.snode) = new ASTNode(BOOL_T, strdup("true")); - else if (strcmp((yyvsp[0].str), "false") == 0) - (yyval.snode) = new ASTNode(BOOL_T, strdup("false")); - else { - printf("Syntax error: expecting either 'true' or 'false', got '%s'\n", (yyvsp[0].str)); - YYERROR; - } - } -#line 2298 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 81: -#line 707 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(OPTION_T, (yyvsp[-1].str)); - (yyval.snode)->children = new std::list(); - (yyval.snode)->children->push_back((yyvsp[0].snode)); - } -#line 2308 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 82: -#line 713 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(OPTION_T, (yyvsp[-1].str)); - (yyval.snode)->children = new std::list(); - (yyval.snode)->children->push_back((yyvsp[0].snode)); - } -#line 2318 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 83: -#line 719 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(OPTION_T, (yyvsp[-1].str)); - (yyval.snode)->children = new std::list(); - (yyval.snode)->children->push_back((yyvsp[0].snode)); - } -#line 2328 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 84: -#line 725 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(OPTION_T, (yyvsp[-1].str)); - (yyval.snode)->children = new std::list(); - (yyval.snode)->children->push_back((yyvsp[0].snode)); - } -#line 2338 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 85: -#line 731 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(OPTION_T, (yyvsp[-1].str)); - (yyval.snode)->children = new std::list(); - (yyval.snode)->children->push_back((yyvsp[0].snode)); - } -#line 2348 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 86: -#line 737 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(OPTION_T, (yyvsp[-1].str)); - (yyval.snode)->children = new std::list(); - (yyval.snode)->children->push_back((yyvsp[0].snode)); - } -#line 2358 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 87: -#line 743 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(OPTION_T, (yyvsp[-1].str)); - (yyval.snode)->children = new std::list(); - (yyval.snode)->children->push_back((yyvsp[0].snode)); - } -#line 2368 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 88: -#line 749 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(OPTION_T, (yyvsp[-1].str)); - (yyval.snode)->children = new std::list(); - (yyval.snode)->children->push_back(new ASTNode(STR_T, (yyvsp[0].str))); - } -#line 2378 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 89: -#line 755 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(OPTION_T, (yyvsp[-1].str)); - (yyval.snode)->children = new std::list(); - (yyval.snode)->children->push_back(new ASTNode(STR_T, (yyvsp[0].str))); - } -#line 2388 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 90: -#line 761 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(OPTION_T, (yyvsp[-1].str)); - (yyval.snode)->children = new std::list(); - (yyval.snode)->children->push_back(new ASTNode(NUM_T, (yyvsp[0].str))); - } -#line 2398 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 91: -#line 767 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(OPTION_T, (yyvsp[-1].str)); - (yyval.snode)->children = new std::list(); - (yyval.snode)->children->push_back(new ASTNode(NUM_T, (yyvsp[0].str))); - } -#line 2408 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 92: -#line 773 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(OPTION_T, NULL); - (yyval.snode)->children = new std::list(); - (yyval.snode)->children->push_back((yyvsp[0].snode)); - } -#line 2418 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 93: -#line 781 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.str) = (yyvsp[0].str); } -#line 2424 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 94: -#line 783 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.str) = (yyvsp[0].str); } -#line 2430 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 95: -#line 785 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.str) = (yyvsp[0].str); } -#line 2436 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 96: -#line 787 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.str) = (yyvsp[0].str); } -#line 2442 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 97: -#line 789 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.str) = (yyvsp[0].str); } -#line 2448 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 98: -#line 791 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.str) = (yyvsp[0].str); } -#line 2454 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 99: -#line 793 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.str) = (yyvsp[0].str); } -#line 2460 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 100: -#line 795 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.str) = (yyvsp[0].str); } -#line 2466 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 101: -#line 797 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.str) = (yyvsp[0].str); } -#line 2472 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 102: -#line 799 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.str) = (yyvsp[0].str); } -#line 2478 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 103: -#line 801 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.str) = (yyvsp[0].str); } -#line 2484 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 104: -#line 803 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.str) = (yyvsp[0].str); } -#line 2490 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 105: -#line 805 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.str) = (yyvsp[0].str); } -#line 2496 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 106: -#line 807 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.str) = (yyvsp[0].str); } -#line 2502 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 107: -#line 809 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.str) = (yyvsp[0].str); } -#line 2508 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 108: -#line 811 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.str) = (yyvsp[0].str); } -#line 2514 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 109: -#line 813 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.str) = (yyvsp[0].str); } -#line 2520 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 110: -#line 815 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.str) = (yyvsp[0].str); } -#line 2526 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 111: -#line 817 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.str) = (yyvsp[0].str); } -#line 2532 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 112: -#line 819 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.str) = (yyvsp[0].str); } -#line 2538 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 113: -#line 821 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.str) = (yyvsp[0].str); } -#line 2544 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 114: -#line 823 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.str) = (yyvsp[0].str); } -#line 2550 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 115: -#line 825 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.str) = (yyvsp[0].str); } -#line 2556 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 116: -#line 827 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.str) = (yyvsp[0].str); } -#line 2562 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 117: -#line 829 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.str) = (yyvsp[0].str); } -#line 2568 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 118: -#line 831 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.str) = (yyvsp[0].str); } -#line 2574 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 119: -#line 833 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.str) = (yyvsp[0].str); } -#line 2580 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 120: -#line 835 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.str) = (yyvsp[0].str); } -#line 2586 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 121: -#line 837 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.str) = (yyvsp[0].str); } -#line 2592 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 122: -#line 841 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.snode) = new ASTNode(INFO_T, (yyvsp[0].str)); } -#line 2598 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 123: -#line 843 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.snode) = new ASTNode(INFO_T, (yyvsp[0].str)); } -#line 2604 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 124: -#line 845 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.snode) = new ASTNode(INFO_T, (yyvsp[0].str)); } -#line 2610 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 125: -#line 847 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.snode) = new ASTNode(INFO_T, (yyvsp[0].str)); } -#line 2616 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 126: -#line 849 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.snode) = new ASTNode(INFO_T, (yyvsp[0].str)); } -#line 2622 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 127: -#line 851 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.snode) = new ASTNode(INFO_T, (yyvsp[0].str)); } -#line 2628 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 128: -#line 853 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { (yyval.snode) = new ASTNode(INFO_T, (yyvsp[0].str)); } -#line 2634 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - case 129: -#line 855 "smt2new/smt2newparser.yy" /* yacc.c:1646 */ - { - (yyval.snode) = new ASTNode(INFO_T, NULL); - (yyval.snode)->children = new std::list(); - (yyval.snode)->children->push_back(new ASTNode(GATTR_T, (yyvsp[0].str))); - } -#line 2644 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - break; - - -#line 2648 "smt2new/smt2newparser.cc" /* yacc.c:1646 */ - default: break; - } - /* User semantic actions sometimes alter yychar, and that requires - that yytoken be updated with the new translation. We take the - approach of translating immediately before every use of yytoken. - One alternative is translating here after every semantic action, - but that translation would be missed if the semantic action invokes - YYABORT, YYACCEPT, or YYERROR immediately after altering yychar or - if it invokes YYBACKUP. In the case of YYABORT or YYACCEPT, an - incorrect destructor might then be invoked immediately. In the - case of YYERROR or YYBACKUP, subsequent parser actions might lead - to an incorrect destructor call or verbose syntax error message - before the lookahead is translated. */ - YY_SYMBOL_PRINT ("-> $$ =", yyr1[yyn], &yyval, &yyloc); - - YYPOPSTACK (yylen); - yylen = 0; - YY_STACK_PRINT (yyss, yyssp); - - *++yyvsp = yyval; - *++yylsp = yyloc; - - /* Now 'shift' the result of the reduction. Determine what state - that goes to, based on the state we popped back to and the rule - number reduced by. */ - - yyn = yyr1[yyn]; - - yystate = yypgoto[yyn - YYNTOKENS] + *yyssp; - if (0 <= yystate && yystate <= YYLAST && yycheck[yystate] == *yyssp) - yystate = yytable[yystate]; - else - yystate = yydefgoto[yyn - YYNTOKENS]; - - goto yynewstate; - - -/*--------------------------------------. -| yyerrlab -- here on detecting error. | -`--------------------------------------*/ -yyerrlab: - /* Make sure we have latest lookahead translation. See comments at - user semantic actions for why this is necessary. */ - yytoken = yychar == YYEMPTY ? YYEMPTY : YYTRANSLATE (yychar); - - /* If not already recovering from an error, report this error. */ - if (!yyerrstatus) - { - ++yynerrs; -#if ! YYERROR_VERBOSE - yyerror (&yylloc, context, YY_("syntax error")); -#else -# define YYSYNTAX_ERROR yysyntax_error (&yymsg_alloc, &yymsg, \ - yyssp, yytoken) - { - char const *yymsgp = YY_("syntax error"); - int yysyntax_error_status; - yysyntax_error_status = YYSYNTAX_ERROR; - if (yysyntax_error_status == 0) - yymsgp = yymsg; - else if (yysyntax_error_status == 1) - { - if (yymsg != yymsgbuf) - YYSTACK_FREE (yymsg); - yymsg = (char *) YYSTACK_ALLOC (yymsg_alloc); - if (!yymsg) - { - yymsg = yymsgbuf; - yymsg_alloc = sizeof yymsgbuf; - yysyntax_error_status = 2; - } - else - { - yysyntax_error_status = YYSYNTAX_ERROR; - yymsgp = yymsg; - } - } - yyerror (&yylloc, context, yymsgp); - if (yysyntax_error_status == 2) - goto yyexhaustedlab; - } -# undef YYSYNTAX_ERROR -#endif - } - - yyerror_range[1] = yylloc; - - if (yyerrstatus == 3) - { - /* If just tried and failed to reuse lookahead token after an - error, discard it. */ - - if (yychar <= YYEOF) - { - /* Return failure if at end of input. */ - if (yychar == YYEOF) - YYABORT; - } - else - { - yydestruct ("Error: discarding", - yytoken, &yylval, &yylloc, context); - yychar = YYEMPTY; - } - } - - /* Else will try to reuse lookahead token after shifting the error - token. */ - goto yyerrlab1; - - -/*---------------------------------------------------. -| yyerrorlab -- error raised explicitly by YYERROR. | -`---------------------------------------------------*/ -yyerrorlab: - - /* Pacify compilers like GCC when the user code never invokes - YYERROR and the label yyerrorlab therefore never appears in user - code. */ - if (/*CONSTCOND*/ 0) - goto yyerrorlab; - - yyerror_range[1] = yylsp[1-yylen]; - /* Do not reclaim the symbols of the rule whose action triggered - this YYERROR. */ - YYPOPSTACK (yylen); - yylen = 0; - YY_STACK_PRINT (yyss, yyssp); - yystate = *yyssp; - goto yyerrlab1; - - -/*-------------------------------------------------------------. -| yyerrlab1 -- common code for both syntax error and YYERROR. | -`-------------------------------------------------------------*/ -yyerrlab1: - yyerrstatus = 3; /* Each real token shifted decrements this. */ - - for (;;) - { - yyn = yypact[yystate]; - if (!yypact_value_is_default (yyn)) - { - yyn += YYTERROR; - if (0 <= yyn && yyn <= YYLAST && yycheck[yyn] == YYTERROR) - { - yyn = yytable[yyn]; - if (0 < yyn) - break; - } - } - - /* Pop the current state because it cannot handle the error token. */ - if (yyssp == yyss) - YYABORT; - - yyerror_range[1] = *yylsp; - yydestruct ("Error: popping", - yystos[yystate], yyvsp, yylsp, context); - YYPOPSTACK (1); - yystate = *yyssp; - YY_STACK_PRINT (yyss, yyssp); - } - - YY_IGNORE_MAYBE_UNINITIALIZED_BEGIN - *++yyvsp = yylval; - YY_IGNORE_MAYBE_UNINITIALIZED_END - - yyerror_range[2] = yylloc; - /* Using YYLLOC is tempting, but would change the location of - the lookahead. YYLOC is available though. */ - YYLLOC_DEFAULT (yyloc, yyerror_range, 2); - *++yylsp = yyloc; - - /* Shift the error token. */ - YY_SYMBOL_PRINT ("Shifting", yystos[yyn], yyvsp, yylsp); - - yystate = yyn; - goto yynewstate; - - -/*-------------------------------------. -| yyacceptlab -- YYACCEPT comes here. | -`-------------------------------------*/ -yyacceptlab: - yyresult = 0; - goto yyreturn; - -/*-----------------------------------. -| yyabortlab -- YYABORT comes here. | -`-----------------------------------*/ -yyabortlab: - yyresult = 1; - goto yyreturn; - -#if !defined yyoverflow || YYERROR_VERBOSE -/*-------------------------------------------------. -| yyexhaustedlab -- memory exhaustion comes here. | -`-------------------------------------------------*/ -yyexhaustedlab: - yyerror (&yylloc, context, YY_("memory exhausted")); - yyresult = 2; - /* Fall through. */ -#endif - -yyreturn: - if (yychar != YYEMPTY) - { - /* Make sure we have latest lookahead translation. See comments at - user semantic actions for why this is necessary. */ - yytoken = YYTRANSLATE (yychar); - yydestruct ("Cleanup: discarding lookahead", - yytoken, &yylval, &yylloc, context); - } - /* Do not reclaim the symbols of the rule whose action triggered - this YYABORT or YYACCEPT. */ - YYPOPSTACK (yylen); - YY_STACK_PRINT (yyss, yyssp); - while (yyssp != yyss) - { - yydestruct ("Cleanup: popping", - yystos[*yyssp], yyvsp, yylsp, context); - YYPOPSTACK (1); - } -#ifndef yyoverflow - if (yyss != yyssa) - YYSTACK_FREE (yyss); -#endif -#if YYERROR_VERBOSE - if (yymsg != yymsgbuf) - YYSTACK_FREE (yymsg); -#endif - return yyresult; -} -#line 862 "smt2new/smt2newparser.yy" /* yacc.c:1906 */ - - -//======================================================================================= -// Auxiliary Routines - diff --git a/src/parsers/smt2new/smt2newparser.hh b/src/parsers/smt2new/smt2newparser.hh deleted file mode 100644 index 9cbb1ec9c..000000000 --- a/src/parsers/smt2new/smt2newparser.hh +++ /dev/null @@ -1,160 +0,0 @@ -/* A Bison parser, made by GNU Bison 3.0.4. */ - -/* Bison interface for Yacc-like parsers in C - - Copyright (C) 1984, 1989-1990, 2000-2015 Free Software Foundation, Inc. - - This program is free software: you can redistribute it and/or modify - it under the terms of the GNU General Public License as published by - the Free Software Foundation, either version 3 of the License, or - (at your option) any later version. - - This program is distributed in the hope that it will be useful, - but WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - GNU General Public License for more details. - - You should have received a copy of the GNU General Public License - along with this program. If not, see . */ - -/* As a special exception, you may create a larger work that contains - part or all of the Bison parser skeleton and distribute that work - under terms of your choice, so long as that work isn't itself a - parser generator using the skeleton or a modified version thereof - as a parser skeleton. Alternatively, if you modify or redistribute - the parser skeleton itself, you may (at your option) remove this - special exception, which will cause the skeleton and the resulting - Bison output files to be licensed under the GNU General Public - License without this special exception. - - This special exception was added by the Free Software Foundation in - version 2.2 of Bison. */ - -#ifndef YY_SMT2NEW_SMT2NEW_SMT2NEWPARSER_HH_INCLUDED -# define YY_SMT2NEW_SMT2NEW_SMT2NEWPARSER_HH_INCLUDED -/* Debug traces. */ -#ifndef YYDEBUG -# define YYDEBUG 0 -#endif -#if YYDEBUG -extern int smt2newdebug; -#endif - -/* Token type. */ -#ifndef YYTOKENTYPE -# define YYTOKENTYPE - enum yytokentype - { - TK_AS = 258, - TK_DECIMAL = 259, - TK_EXISTS = 260, - TK_FORALL = 261, - TK_LET = 262, - TK_NUMERAL = 263, - TK_PAR = 264, - TK_STRING = 265, - TK_ASSERT = 266, - TK_CHECKSAT = 267, - TK_DECLARESORT = 268, - TK_DECLAREFUN = 269, - TK_DECLARECONST = 270, - TK_DEFINESORT = 271, - TK_DEFINEFUN = 272, - TK_EXIT = 273, - TK_GETASSERTIONS = 274, - TK_GETASSIGNMENT = 275, - TK_GETINFO = 276, - TK_GETOPTION = 277, - TK_GETPROOF = 278, - TK_GETUNSATCORE = 279, - TK_GETVALUE = 280, - TK_POP = 281, - TK_PUSH = 282, - TK_SETLOGIC = 283, - TK_SETINFO = 284, - TK_SETOPTION = 285, - TK_THEORY = 286, - TK_GETITPS = 287, - TK_WRSTATE = 288, - TK_RDSTATE = 289, - TK_SIMPLIFY = 290, - TK_WRFUNS = 291, - TK_NUM = 292, - TK_SYM = 293, - TK_KEY = 294, - TK_STR = 295, - TK_DEC = 296, - TK_HEX = 297, - TK_BIN = 298, - KW_SORTS = 299, - KW_FUNS = 300, - KW_SORTSDESCRIPTION = 301, - KW_FUNSDESCRIPTION = 302, - KW_DEFINITION = 303, - KW_NOTES = 304, - KW_THEORIES = 305, - KW_LANGUAGE = 306, - KW_EXTENSIONS = 307, - KW_VALUES = 308, - KW_PRINTSUCCESS = 309, - KW_EXPANDDEFINITIONS = 310, - KW_INTERACTIVEMODE = 311, - KW_PRODUCEPROOFS = 312, - KW_PRODUCEUNSATCORES = 313, - KW_PRODUCEMODELS = 314, - KW_PRODUCEASSIGNMENTS = 315, - KW_REGULAROUTPUTCHANNEL = 316, - KW_DIAGNOSTICOUTPUTCHANNEL = 317, - KW_RANDOMSEED = 318, - KW_VERBOSITY = 319, - KW_ERRORBEHAVIOR = 320, - KW_NAME = 321, - KW_NAMED = 322, - KW_AUTHORS = 323, - KW_VERSION = 324, - KW_STATUS = 325, - KW_REASONUNKNOWN = 326, - KW_ALLSTATISTICS = 327 - }; -#endif - -/* Value type. */ -#if ! defined YYSTYPE && ! defined YYSTYPE_IS_DECLARED - -union YYSTYPE -{ -#line 66 "smt2new/smt2newparser.yy" /* yacc.c:1909 */ - - char * str; - std::vector< std::string > * str_list; - ASTNode * snode; - std::list< ASTNode * > * snode_list; - smt2token tok; - -#line 135 "smt2new/smt2newparser.hh" /* yacc.c:1909 */ -}; - -typedef union YYSTYPE YYSTYPE; -# define YYSTYPE_IS_TRIVIAL 1 -# define YYSTYPE_IS_DECLARED 1 -#endif - -/* Location type. */ -#if ! defined YYLTYPE && ! defined YYLTYPE_IS_DECLARED -typedef struct YYLTYPE YYLTYPE; -struct YYLTYPE -{ - int first_line; - int first_column; - int last_line; - int last_column; -}; -# define YYLTYPE_IS_DECLARED 1 -# define YYLTYPE_IS_TRIVIAL 1 -#endif - - - -int smt2newparse (Smt2newContext* context); - -#endif /* !YY_SMT2NEW_SMT2NEW_SMT2NEWPARSER_HH_INCLUDED */