diff options
Diffstat (limited to 'lib/SMT/smtlib_lexer.cpp')
| -rw-r--r-- | lib/SMT/smtlib_lexer.cpp | 2378 |
1 files changed, 2378 insertions, 0 deletions
diff --git a/lib/SMT/smtlib_lexer.cpp b/lib/SMT/smtlib_lexer.cpp new file mode 100644 index 00000000..c25e7f9a --- /dev/null +++ b/lib/SMT/smtlib_lexer.cpp @@ -0,0 +1,2378 @@ +#line 2 "smtlib_lexer.cpp" + +#line 4 "smtlib_lexer.cpp" + +#define YY_INT_ALIGNED short int + +/* A lexical scanner generated by flex */ + +#define yy_create_buffer smtlib_create_buffer +#define yy_delete_buffer smtlib_delete_buffer +#define yy_flex_debug smtlib_flex_debug +#define yy_init_buffer smtlib_init_buffer +#define yy_flush_buffer smtlib_flush_buffer +#define yy_load_buffer_state smtlib_load_buffer_state +#define yy_switch_to_buffer smtlib_switch_to_buffer +#define yyin smtlibin +#define yyleng smtlibleng +#define yylex smtliblex +#define yylineno smtliblineno +#define yyout smtlibout +#define yyrestart smtlibrestart +#define yytext smtlibtext +#define yywrap smtlibwrap +#define yyalloc smtliballoc +#define yyrealloc smtlibrealloc +#define yyfree smtlibfree + +#define FLEX_SCANNER +#define YY_FLEX_MAJOR_VERSION 2 +#define YY_FLEX_MINOR_VERSION 5 +#define YY_FLEX_SUBMINOR_VERSION 35 +#if YY_FLEX_SUBMINOR_VERSION > 0 +#define FLEX_BETA +#endif + +/* First, we deal with platform-specific or compiler-specific issues. */ + +/* begin standard C headers. */ +#include <stdio.h> +#include <string.h> +#include <errno.h> +#include <stdlib.h> + +/* end standard C headers. */ + +/* flex integer type definitions */ + +#ifndef FLEXINT_H +#define FLEXINT_H + +/* C99 systems have <inttypes.h>. 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 <inttypes.h> +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 + +#endif /* ! C99 */ + +#endif /* ! FLEXINT_H */ + +#ifdef __cplusplus + +/* The "const" storage-class-modifier is valid. */ +#define YY_USE_CONST + +#else /* ! __cplusplus */ + +/* C99 requires __STDC__ to be defined as 1. */ +#if defined (__STDC__) + +#define YY_USE_CONST + +#endif /* defined (__STDC__) */ +#endif /* ! __cplusplus */ + +#ifdef YY_USE_CONST +#define yyconst const +#else +#define yyconst +#endif + +/* Returned upon end-of-file. */ +#define YY_NULL 0 + +/* Promotes a possibly negative, possibly signed char to an unsigned + * integer for use as an array index. If the signed char is negative, + * we want to instead treat it as an 8-bit unsigned char, hence the + * double cast. + */ +#define YY_SC_TO_UI(c) ((unsigned int) (unsigned char) c) + +/* 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 (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 (((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 smtlibrestart(smtlibin ) + +#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 + +extern int smtlibleng; + +extern FILE *smtlibin, *smtlibout; + +#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 smtliblex. + * One obvious solution it to make yy_act a global. I tried that, and saw + * a 5% performance hit in a non-smtliblineno 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 < smtlibleng; ++yyl )\ + if ( smtlibtext[yyl] == '\n' )\ + --smtliblineno;\ + }while(0) + +/* Return all but the first "n" matched characters back to the input stream. */ +#define yyless(n) \ + do \ + { \ + /* Undo effects of setting up smtlibtext. */ \ + int yyless_macro_arg = (n); \ + YY_LESS_LINENO(yyless_macro_arg);\ + *yy_cp = (yy_hold_char); \ + YY_RESTORE_YY_MORE_OFFSET \ + (yy_c_buf_p) = yy_cp = yy_bp + yyless_macro_arg - YY_MORE_ADJ; \ + YY_DO_BEFORE_ACTION; /* set up smtlibtext again */ \ + } \ + while ( 0 ) + +#define unput(c) yyunput( c, (yytext_ptr) ) + +#ifndef YY_TYPEDEF_YY_SIZE_T +#define YY_TYPEDEF_YY_SIZE_T +typedef size_t yy_size_t; +#endif + +#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. + */ + yy_size_t 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 smtlibrestart()), so that the user can continue scanning by + * just pointing smtlibin at a new input file. + */ +#define YY_BUFFER_EOF_PENDING 2 + + }; +#endif /* !YY_STRUCT_YY_BUFFER_STATE */ + +/* Stack of input buffers. */ +static size_t yy_buffer_stack_top = 0; /**< index of top of stack. */ +static size_t yy_buffer_stack_max = 0; /**< capacity of stack. */ +static YY_BUFFER_STATE * yy_buffer_stack = 0; /**< Stack as an array. */ + +/* 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 ( (yy_buffer_stack) \ + ? (yy_buffer_stack)[(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 (yy_buffer_stack)[(yy_buffer_stack_top)] + +/* yy_hold_char holds the character lost when smtlibtext is formed. */ +static char yy_hold_char; +static int yy_n_chars; /* number of characters read into yy_ch_buf */ +int smtlibleng; + +/* Points to current character in buffer. */ +static char *yy_c_buf_p = (char *) 0; +static int yy_init = 0; /* whether we need to initialize */ +static int yy_start = 0; /* start state number */ + +/* Flag which is used to allow smtlibwrap()'s to do buffer switches + * instead of setting up a fresh smtlibin. A bit of a hack ... + */ +static int yy_did_buffer_switch_on_eof; + +void smtlibrestart (FILE *input_file ); +void smtlib_switch_to_buffer (YY_BUFFER_STATE new_buffer ); +YY_BUFFER_STATE smtlib_create_buffer (FILE *file,int size ); +void smtlib_delete_buffer (YY_BUFFER_STATE b ); +void smtlib_flush_buffer (YY_BUFFER_STATE b ); +void smtlibpush_buffer_state (YY_BUFFER_STATE new_buffer ); +void smtlibpop_buffer_state (void ); + +static void smtlibensure_buffer_stack (void ); +static void smtlib_load_buffer_state (void ); +static void smtlib_init_buffer (YY_BUFFER_STATE b,FILE *file ); + +#define YY_FLUSH_BUFFER smtlib_flush_buffer(YY_CURRENT_BUFFER ) + +YY_BUFFER_STATE smtlib_scan_buffer (char *base,yy_size_t size ); +YY_BUFFER_STATE smtlib_scan_string (yyconst char *yy_str ); +YY_BUFFER_STATE smtlib_scan_bytes (yyconst char *bytes,int len ); + +void *smtliballoc (yy_size_t ); +void *smtlibrealloc (void *,yy_size_t ); +void smtlibfree (void * ); + +#define yy_new_buffer smtlib_create_buffer + +#define yy_set_interactive(is_interactive) \ + { \ + if ( ! YY_CURRENT_BUFFER ){ \ + smtlibensure_buffer_stack (); \ + YY_CURRENT_BUFFER_LVALUE = \ + smtlib_create_buffer(smtlibin,YY_BUF_SIZE ); \ + } \ + YY_CURRENT_BUFFER_LVALUE->yy_is_interactive = is_interactive; \ + } + +#define yy_set_bol(at_bol) \ + { \ + if ( ! YY_CURRENT_BUFFER ){\ + smtlibensure_buffer_stack (); \ + YY_CURRENT_BUFFER_LVALUE = \ + smtlib_create_buffer(smtlibin,YY_BUF_SIZE ); \ + } \ + YY_CURRENT_BUFFER_LVALUE->yy_at_bol = at_bol; \ + } + +#define YY_AT_BOL() (YY_CURRENT_BUFFER_LVALUE->yy_at_bol) + +/* Begin user sect3 */ + +#define smtlibwrap(n) 1 +#define YY_SKIP_YYWRAP + +typedef unsigned char YY_CHAR; + +FILE *smtlibin = (FILE *) 0, *smtlibout = (FILE *) 0; + +typedef int yy_state_type; + +extern int smtliblineno; + +int smtliblineno = 1; + +extern char *smtlibtext; +#define yytext_ptr smtlibtext + +static yy_state_type yy_get_previous_state (void ); +static yy_state_type yy_try_NUL_trans (yy_state_type current_state ); +static int yy_get_next_buffer (void ); +static void yy_fatal_error (yyconst char msg[] ); + +/* Done after the current pattern has been matched and before the + * corresponding action - sets up smtlibtext. + */ +#define YY_DO_BEFORE_ACTION \ + (yytext_ptr) = yy_bp; \ + smtlibleng = (size_t) (yy_cp - yy_bp); \ + (yy_hold_char) = *yy_cp; \ + *yy_cp = '\0'; \ + (yy_c_buf_p) = yy_cp; + +#define YY_NUM_RULES 67 +#define YY_END_OF_BUFFER 68 +/* 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 yyconst flex_int16_t yy_accept[240] = + { 0, + 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, + 68, 66, 2, 1, 8, 64, 62, 60, 61, 4, + 55, 5, 63, 65, 56, 57, 65, 65, 65, 65, + 65, 65, 65, 65, 65, 65, 65, 65, 65, 65, + 65, 14, 59, 7, 6, 11, 67, 10, 11, 18, + 17, 18, 16, 55, 58, 13, 64, 0, 4, 0, + 65, 65, 65, 65, 65, 65, 65, 65, 65, 65, + 65, 65, 65, 65, 65, 65, 65, 65, 65, 65, + 26, 65, 65, 65, 65, 65, 65, 65, 9, 15, + 0, 3, 0, 25, 65, 65, 65, 65, 65, 65, + + 65, 65, 65, 65, 65, 65, 65, 28, 65, 21, + 65, 31, 65, 22, 65, 42, 65, 65, 65, 65, + 65, 27, 0, 12, 65, 65, 65, 65, 65, 65, + 65, 65, 65, 65, 32, 65, 65, 36, 65, 65, + 65, 65, 65, 65, 65, 65, 19, 65, 65, 0, + 0, 65, 65, 65, 65, 65, 65, 65, 65, 65, + 20, 65, 65, 65, 65, 65, 41, 33, 37, 35, + 65, 65, 43, 0, 65, 40, 65, 65, 65, 65, + 29, 65, 65, 65, 65, 30, 65, 65, 65, 65, + 47, 65, 0, 65, 65, 65, 65, 65, 65, 65, + + 65, 65, 46, 65, 23, 65, 44, 54, 65, 65, + 65, 65, 53, 65, 65, 65, 65, 65, 52, 65, + 48, 65, 65, 65, 50, 65, 65, 65, 45, 65, + 39, 38, 51, 49, 65, 34, 65, 24, 0 + } ; + +static yyconst flex_int32_t yy_ec[256] = + { 0, + 1, 1, 1, 1, 1, 1, 1, 1, 2, 3, + 1, 2, 2, 1, 1, 1, 1, 1, 1, 1, + 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, + 1, 2, 1, 4, 5, 6, 5, 5, 7, 8, + 9, 5, 5, 1, 5, 10, 5, 11, 11, 11, + 11, 11, 11, 11, 11, 11, 11, 12, 13, 5, + 5, 5, 14, 5, 15, 15, 15, 15, 15, 15, + 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, + 15, 15, 15, 15, 15, 15, 15, 15, 15, 15, + 16, 17, 18, 1, 19, 1, 20, 21, 22, 23, + + 24, 25, 26, 27, 28, 15, 29, 30, 31, 32, + 33, 34, 15, 35, 36, 37, 38, 39, 40, 41, + 15, 15, 42, 5, 43, 5, 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 yyconst flex_int32_t yy_meta[44] = + { 0, + 1, 1, 2, 1, 1, 1, 3, 1, 1, 3, + 3, 1, 1, 1, 3, 1, 1, 1, 3, 3, + 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, + 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, + 3, 1, 1 + } ; + +static yyconst flex_int16_t yy_base[245] = + { 0, + 0, 0, 261, 260, 41, 43, 45, 46, 49, 52, + 262, 265, 265, 265, 265, 256, 265, 265, 265, 40, + 226, 265, 265, 0, 265, 265, 33, 235, 219, 31, + 216, 37, 41, 53, 223, 220, 219, 48, 218, 220, + 218, 265, 265, 265, 265, 265, 265, 265, 0, 265, + 265, 37, 265, 216, 265, 265, 244, 237, 72, 227, + 0, 223, 209, 216, 211, 220, 216, 204, 56, 209, + 214, 202, 204, 71, 201, 210, 201, 195, 205, 193, + 0, 205, 191, 192, 206, 187, 68, 189, 265, 265, + 203, 211, 184, 0, 182, 186, 196, 198, 188, 178, + + 178, 52, 177, 175, 78, 175, 173, 0, 179, 0, + 182, 0, 179, 182, 182, 0, 167, 166, 178, 169, + 180, 0, 162, 161, 166, 165, 168, 172, 161, 164, + 154, 158, 169, 164, 0, 157, 148, 0, 158, 156, + 145, 160, 145, 144, 143, 140, 0, 144, 139, 138, + 150, 139, 136, 140, 137, 141, 136, 131, 130, 74, + 0, 135, 134, 139, 138, 141, 0, 0, 0, 0, + 124, 119, 0, 123, 120, 0, 136, 124, 117, 131, + 0, 124, 113, 115, 116, 0, 128, 115, 110, 119, + 0, 112, 111, 114, 106, 109, 111, 101, 104, 104, + + 111, 99, 0, 114, 0, 108, 0, 265, 98, 101, + 109, 95, 0, 95, 90, 102, 87, 99, 0, 89, + 0, 75, 74, 69, 0, 67, 66, 71, 0, 77, + 0, 0, 0, 0, 35, 0, 30, 0, 265, 110, + 113, 116, 49, 119 + } ; + +static yyconst flex_int16_t yy_def[245] = + { 0, + 239, 1, 240, 240, 241, 241, 242, 242, 1, 1, + 239, 239, 239, 239, 239, 239, 239, 239, 239, 239, + 239, 239, 239, 243, 239, 239, 243, 243, 243, 243, + 243, 243, 243, 243, 243, 243, 243, 243, 243, 243, + 243, 239, 239, 239, 239, 239, 239, 239, 244, 239, + 239, 239, 239, 239, 239, 239, 239, 239, 239, 239, + 243, 243, 243, 243, 243, 243, 243, 243, 243, 243, + 243, 243, 243, 243, 243, 243, 243, 243, 243, 243, + 243, 243, 243, 243, 243, 243, 243, 243, 239, 239, + 239, 239, 239, 243, 243, 243, 243, 243, 243, 243, + + 243, 243, 243, 243, 243, 243, 243, 243, 243, 243, + 243, 243, 243, 243, 243, 243, 243, 243, 243, 243, + 243, 243, 239, 239, 243, 243, 243, 243, 243, 243, + 243, 243, 243, 243, 243, 243, 243, 243, 243, 243, + 243, 243, 243, 243, 243, 243, 243, 243, 243, 239, + 239, 243, 243, 243, 243, 243, 243, 243, 243, 243, + 243, 243, 243, 243, 243, 243, 243, 243, 243, 243, + 243, 243, 243, 239, 243, 243, 243, 243, 243, 243, + 243, 243, 243, 243, 243, 243, 243, 243, 243, 243, + 243, 243, 239, 243, 243, 243, 243, 243, 243, 243, + + 243, 243, 243, 243, 243, 243, 243, 239, 243, 243, + 243, 243, 243, 243, 243, 243, 243, 243, 243, 243, + 243, 243, 243, 243, 243, 243, 243, 243, 243, 243, + 243, 243, 243, 243, 243, 243, 243, 243, 0, 239, + 239, 239, 239, 239 + } ; + +static yyconst flex_int16_t yy_nxt[309] = + { 0, + 12, 13, 14, 15, 16, 17, 12, 18, 19, 12, + 20, 21, 22, 23, 24, 25, 12, 26, 12, 27, + 28, 29, 30, 31, 32, 24, 24, 33, 24, 34, + 24, 35, 36, 37, 24, 38, 39, 40, 24, 24, + 41, 42, 43, 47, 48, 47, 48, 51, 51, 58, + 59, 61, 12, 238, 67, 12, 70, 49, 68, 49, + 54, 52, 52, 54, 62, 74, 71, 83, 63, 72, + 237, 75, 77, 64, 73, 132, 78, 76, 90, 90, + 84, 58, 59, 101, 85, 79, 133, 53, 53, 107, + 55, 56, 102, 55, 56, 108, 120, 136, 183, 236, + + 235, 234, 233, 121, 232, 231, 230, 184, 137, 185, + 44, 44, 44, 46, 46, 46, 50, 50, 50, 89, + 229, 89, 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, 182, 181, 180, 179, 178, + 177, 176, 175, 174, 151, 173, 172, 171, 170, 169, + 168, 167, 166, 165, 164, 163, 162, 161, 160, 159, + 158, 157, 156, 155, 154, 153, 152, 151, 150, 149, + + 148, 147, 146, 145, 144, 143, 142, 141, 140, 139, + 138, 135, 134, 131, 130, 129, 128, 127, 126, 125, + 124, 92, 123, 122, 119, 118, 117, 116, 115, 114, + 113, 112, 111, 110, 109, 106, 105, 104, 103, 100, + 99, 98, 97, 96, 95, 94, 93, 92, 57, 91, + 88, 87, 86, 82, 81, 80, 69, 66, 65, 60, + 57, 239, 45, 45, 11, 239, 239, 239, 239, 239, + 239, 239, 239, 239, 239, 239, 239, 239, 239, 239, + 239, 239, 239, 239, 239, 239, 239, 239, 239, 239, + 239, 239, 239, 239, 239, 239, 239, 239, 239, 239, + + 239, 239, 239, 239, 239, 239, 239, 239 + } ; + +static yyconst flex_int16_t yy_chk[309] = + { 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, 5, 5, 6, 6, 7, 8, 20, + 20, 243, 9, 237, 30, 10, 32, 5, 30, 6, + 9, 7, 8, 10, 27, 33, 32, 38, 27, 32, + 235, 33, 34, 27, 32, 102, 34, 33, 52, 52, + 38, 59, 59, 69, 38, 34, 102, 7, 8, 74, + 9, 9, 69, 10, 10, 74, 87, 105, 160, 230, + + 228, 227, 226, 87, 224, 223, 222, 160, 105, 160, + 240, 240, 240, 241, 241, 241, 242, 242, 242, 244, + 220, 244, 218, 217, 216, 215, 214, 212, 211, 210, + 209, 206, 204, 202, 201, 200, 199, 198, 197, 196, + 195, 194, 193, 192, 190, 189, 188, 187, 185, 184, + 183, 182, 180, 179, 178, 177, 175, 174, 172, 171, + 166, 165, 164, 163, 162, 159, 158, 157, 156, 155, + 154, 153, 152, 151, 150, 149, 148, 146, 145, 144, + 143, 142, 141, 140, 139, 137, 136, 134, 133, 132, + 131, 130, 129, 128, 127, 126, 125, 124, 123, 121, + + 120, 119, 118, 117, 115, 114, 113, 111, 109, 107, + 106, 104, 103, 101, 100, 99, 98, 97, 96, 95, + 93, 92, 91, 88, 86, 85, 84, 83, 82, 80, + 79, 78, 77, 76, 75, 73, 72, 71, 70, 68, + 67, 66, 65, 64, 63, 62, 60, 58, 57, 54, + 41, 40, 39, 37, 36, 35, 31, 29, 28, 21, + 16, 11, 4, 3, 239, 239, 239, 239, 239, 239, + 239, 239, 239, 239, 239, 239, 239, 239, 239, 239, + 239, 239, 239, 239, 239, 239, 239, 239, 239, 239, + 239, 239, 239, 239, 239, 239, 239, 239, 239, 239, + + 239, 239, 239, 239, 239, 239, 239, 239 + } ; + +/* Table of booleans, true if rule could match eol. */ +static yyconst flex_int32_t yy_rule_can_match_eol[68] = + { 0, +1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 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, }; + +static yy_state_type yy_last_accepting_state; +static char *yy_last_accepting_cpos; + +extern int smtlib_flex_debug; +int smtlib_flex_debug = 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 +char *smtlibtext; +#line 1 "smtlib.lex" +#line 2 "smtlib.lex" +/*****************************************************************************/ +/*! + * \file smtlib.lex + * + * Author: Clark Barrett + * + * Created: 2005 + * + * <hr> + * + * License to use, copy, modify, sell and/or distribute this software + * and its documentation for any purpose is hereby granted without + * royalty, subject to the terms and conditions defined in the \ref + * LICENSE file provided with this distribution. + * + * <hr> + * + */ +/*****************************************************************************/ + +#include <iostream> +#include "parser_temp.h" +#include "smtlib_parser.h" + +namespace CVC3 { + extern ParserTemp* parserTemp; +} + +extern int smtlib_inputLine; +extern char *smtlibtext; + +extern int smtliberror (const char *msg); + +static int smtlibinput(std::istream& is, char* buf, int size) { + int res; + if(is) { + // If interactive, read line by line; otherwise read as much as we + // can gobble + if(CVC3::parserTemp->interactive) { + // Print the current prompt + std::cout << CVC3::parserTemp->getPrompt() << std::flush; + // Set the prompt to "middle of the command" one + CVC3::parserTemp->setPrompt2(); + // Read the line + is.getline(buf, size-1); + } else // Set the terminator char to 0 + is.getline(buf, size-1, 0); + // If failbit is set, but eof is not, it means the line simply + // didn't fit; so we clear the state and keep on reading. + bool partialStr = is.fail() && !is.eof(); + if(partialStr) + is.clear(); + + for(res = 0; res<size && buf[res] != 0; res++) ; + if(res == size) smtliberror("Lexer bug: overfilled the buffer"); + if(!partialStr) { // Insert \n into the buffer + buf[res++] = '\n'; + buf[res] = '\0'; + } + } else { + res = YY_NULL; + } + return res; +} + +// Redefine the input buffer function to read from an istream +#define YY_INPUT(buf,result,max_size) \ + result = smtlibinput(*CVC3::parserTemp->is, buf, max_size); + +int smtlib_bufSize() { return YY_BUF_SIZE; } +YY_BUFFER_STATE smtlib_buf_state() { return YY_CURRENT_BUFFER; } + +/* some wrappers for methods that need to refer to a struct. + These are used by CVC3::Parser. */ +void *smtlib_createBuffer(int sz) { + return (void *)smtlib_create_buffer(NULL, sz); +} +void smtlib_deleteBuffer(void *buf_state) { + smtlib_delete_buffer((struct yy_buffer_state *)buf_state); +} +void smtlib_switchToBuffer(void *buf_state) { + smtlib_switch_to_buffer((struct yy_buffer_state *)buf_state); +} +void *smtlib_bufState() { + return (void *)smtlib_buf_state(); +} + +void smtlib_setInteractive(bool is_interactive) { + yy_set_interactive(is_interactive); +} + +// File-static (local to this file) variables and functions +static std::string _string_lit; + + static char escapeChar(char c) { + switch(c) { + case 'n': return '\n'; + case 't': return '\t'; + default: return c; + } + } + +// for now, we don't have subranges. +// +// ".." { return DOTDOT_TOK; } +/*OPCHAR (['!#?\_$&\|\\@])*/ + + + + + +#line 761 "smtlib_lexer.cpp" + +#define INITIAL 0 +#define COMMENT 1 +#define STRING_LITERAL 2 +#define USER_VALUE 3 +#define PAT_MODE 4 + +#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 <unistd.h> +#endif + +#ifndef YY_EXTRA_TYPE +#define YY_EXTRA_TYPE void * +#endif + +static int yy_init_globals (void ); + +/* Accessor methods to globals. + These are made visible to non-reentrant scanners for convenience. */ + +int smtliblex_destroy (void ); + +int smtlibget_debug (void ); + +void smtlibset_debug (int debug_flag ); + +YY_EXTRA_TYPE smtlibget_extra (void ); + +void smtlibset_extra (YY_EXTRA_TYPE user_defined ); + +FILE *smtlibget_in (void ); + +void smtlibset_in (FILE * in_str ); + +FILE *smtlibget_out (void ); + +void smtlibset_out (FILE * out_str ); + +int smtlibget_leng (void ); + +char *smtlibget_text (void ); + +int smtlibget_lineno (void ); + +void smtlibset_lineno (int line_number ); + +/* Macros after this point can all be overridden by user definitions in + * section 1. + */ + +#ifndef YY_SKIP_YYWRAP +#ifdef __cplusplus +extern "C" int smtlibwrap (void ); +#else +extern int smtlibwrap (void ); +#endif +#endif + +#ifndef yytext_ptr +static void yy_flex_strncpy (char *,yyconst char *,int ); +#endif + +#ifdef YY_NEED_STRLEN +static int yy_flex_strlen (yyconst char * ); +#endif + +#ifndef YY_NO_INPUT + +#ifdef __cplusplus +static int yyinput (void ); +#else +static int input (void ); +#endif + +#endif + +/* 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( smtlibtext, smtlibleng, 1, smtlibout )) {} } 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 = '*'; \ + size_t n; \ + for ( n = 0; n < max_size && \ + (c = getc( smtlibin )) != EOF && c != '\n'; ++n ) \ + buf[n] = (char) c; \ + if ( c == '\n' ) \ + buf[n++] = (char) c; \ + if ( c == EOF && ferror( smtlibin ) ) \ + YY_FATAL_ERROR( "input in flex scanner failed" ); \ + result = n; \ + } \ + else \ + { \ + errno=0; \ + while ( (result = fread(buf, 1, max_size, smtlibin))==0 && ferror(smtlibin)) \ + { \ + if( errno != EINTR) \ + { \ + YY_FATAL_ERROR( "input in flex scanner failed" ); \ + break; \ + } \ + errno=0; \ + clearerr(smtlibin); \ + } \ + }\ +\ + +#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 ) +#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 smtliblex (void); + +#define YY_DECL int smtliblex (void) +#endif /* !YY_DECL */ + +/* Code executed at the beginning of each rule, after smtlibtext and smtlibleng + * 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 break; +#endif + +#define YY_RULE_SETUP \ + YY_USER_ACTION + +/** The main scanner function which does all the work. + */ +YY_DECL +{ + register yy_state_type yy_current_state; + register char *yy_cp, *yy_bp; + register int yy_act; + +#line 126 "smtlib.lex" + + +#line 953 "smtlib_lexer.cpp" + + if ( !(yy_init) ) + { + (yy_init) = 1; + +#ifdef YY_USER_INIT + YY_USER_INIT; +#endif + + if ( ! (yy_start) ) + (yy_start) = 1; /* first start state */ + + if ( ! smtlibin ) + smtlibin = stdin; + + if ( ! smtlibout ) + smtlibout = stdout; + + if ( ! YY_CURRENT_BUFFER ) { + smtlibensure_buffer_stack (); + YY_CURRENT_BUFFER_LVALUE = + smtlib_create_buffer(smtlibin,YY_BUF_SIZE ); + } + + smtlib_load_buffer_state( ); + } + + while ( 1 ) /* loops until end-of-file is reached */ + { + yy_cp = (yy_c_buf_p); + + /* Support of smtlibtext. */ + *yy_cp = (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 = (yy_start); +yy_match: + do + { + register YY_CHAR yy_c = yy_ec[YY_SC_TO_UI(*yy_cp)]; + if ( yy_accept[yy_current_state] ) + { + (yy_last_accepting_state) = yy_current_state; + (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 >= 240 ) + yy_c = yy_meta[(unsigned int) yy_c]; + } + yy_current_state = yy_nxt[yy_base[yy_current_state] + (unsigned int) yy_c]; + ++yy_cp; + } + while ( yy_base[yy_current_state] != 265 ); + +yy_find_action: + yy_act = yy_accept[yy_current_state]; + if ( yy_act == 0 ) + { /* have to back up */ + yy_cp = (yy_last_accepting_cpos); + yy_current_state = (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 < smtlibleng; ++yyl ) + if ( smtlibtext[yyl] == '\n' ) + + smtliblineno++; +; + } + +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 = (yy_hold_char); + yy_cp = (yy_last_accepting_cpos); + yy_current_state = (yy_last_accepting_state); + goto yy_find_action; + +case 1: +/* rule 1 can match eol */ +YY_RULE_SETUP +#line 128 "smtlib.lex" +{ CVC3::parserTemp->lineNum++; } + YY_BREAK +case 2: +YY_RULE_SETUP +#line 129 "smtlib.lex" +{ /* skip whitespace */ } + YY_BREAK +case 3: +YY_RULE_SETUP +#line 131 "smtlib.lex" +{ smtliblval.str = new std::string(smtlibtext); return NUMERAL_TOK; } + YY_BREAK +case 4: +YY_RULE_SETUP +#line 132 "smtlib.lex" +{ smtliblval.str = new std::string(smtlibtext); return NUMERAL_TOK; + } + YY_BREAK +case 5: +YY_RULE_SETUP +#line 135 "smtlib.lex" +{ BEGIN COMMENT; } + YY_BREAK +case 6: +/* rule 6 can match eol */ +YY_RULE_SETUP +#line 136 "smtlib.lex" +{ BEGIN INITIAL; /* return to normal mode */ + CVC3::parserTemp->lineNum++; } + YY_BREAK +case 7: +YY_RULE_SETUP +#line 138 "smtlib.lex" +{ /* stay in comment mode */ } + YY_BREAK +case 8: +YY_RULE_SETUP +#line 140 "smtlib.lex" +{ BEGIN STRING_LITERAL; + _string_lit.erase(_string_lit.begin(), + _string_lit.end()); } + YY_BREAK +case 9: +YY_RULE_SETUP +#line 143 "smtlib.lex" +{ /* escape characters (like \n or \") */ + _string_lit.insert(_string_lit.end(), + escapeChar(smtlibtext[1])); } + YY_BREAK +case 10: +YY_RULE_SETUP +#line 146 "smtlib.lex" +{ BEGIN INITIAL; /* return to normal mode */ + smtliblval.str = new std::string(_string_lit); + return STRING_TOK; } + YY_BREAK +case 11: +YY_RULE_SETUP +#line 149 "smtlib.lex" +{ _string_lit.insert(_string_lit.end(),*smtlibtext); } + YY_BREAK +case 12: +YY_RULE_SETUP +#line 151 "smtlib.lex" +{ BEGIN PAT_MODE; + return PAT_TOK;} + YY_BREAK +case 13: +YY_RULE_SETUP +#line 153 "smtlib.lex" +{ BEGIN INITIAL; + return RCURBRACK_TOK; } + YY_BREAK +case 14: +YY_RULE_SETUP +#line 155 "smtlib.lex" +{ BEGIN USER_VALUE; + _string_lit.erase(_string_lit.begin(), + _string_lit.end()); } + YY_BREAK +case 15: +YY_RULE_SETUP +#line 158 "smtlib.lex" +{ /* escape characters */ + _string_lit.insert(_string_lit.end(),smtlibtext[1]); } + YY_BREAK +case 16: +YY_RULE_SETUP +#line 161 "smtlib.lex" +{ BEGIN INITIAL; /* return to normal mode */ + smtliblval.str = new std::string(_string_lit); + return USER_VAL_TOK; } + YY_BREAK +case 17: +/* rule 17 can match eol */ +YY_RULE_SETUP +#line 165 "smtlib.lex" +{ _string_lit.insert(_string_lit.end(),'\n'); + CVC3::parserTemp->lineNum++; } + YY_BREAK +case 18: +YY_RULE_SETUP +#line 167 "smtlib.lex" +{ _string_lit.insert(_string_lit.end(),*smtlibtext); } + YY_BREAK +case 19: +YY_RULE_SETUP +#line 169 "smtlib.lex" +{ return TRUE_TOK; } + YY_BREAK +case 20: +YY_RULE_SETUP +#line 170 "smtlib.lex" +{ return FALSE_TOK; } + YY_BREAK +case 21: +YY_RULE_SETUP +#line 171 "smtlib.lex" +{ return ITE_TOK; } + YY_BREAK +case 22: +YY_RULE_SETUP +#line 172 "smtlib.lex" +{ return NOT_TOK; } + YY_BREAK +case 23: +YY_RULE_SETUP +#line 173 "smtlib.lex" +{ return IMPLIES_TOK; } + YY_BREAK +case 24: +YY_RULE_SETUP +#line 174 "smtlib.lex" +{ return IF_THEN_ELSE_TOK; } + YY_BREAK +case 25: +YY_RULE_SETUP +#line 175 "smtlib.lex" +{ return AND_TOK; } + YY_BREAK +case 26: +YY_RULE_SETUP +#line 176 "smtlib.lex" +{ return OR_TOK; } + YY_BREAK +case 27: +YY_RULE_SETUP +#line 177 "smtlib.lex" +{ return XOR_TOK; } + YY_BREAK +case 28: +YY_RULE_SETUP +#line 178 "smtlib.lex" +{ return IFF_TOK; } + YY_BREAK +case 29: +YY_RULE_SETUP +#line 179 "smtlib.lex" +{ return EXISTS_TOK; } + YY_BREAK +case 30: +YY_RULE_SETUP +#line 180 "smtlib.lex" +{ return FORALL_TOK; } + YY_BREAK +case 31: +YY_RULE_SETUP +#line 181 "smtlib.lex" +{ return LET_TOK; } + YY_BREAK +case 32: +YY_RULE_SETUP +#line 182 "smtlib.lex" +{ return FLET_TOK; } + YY_BREAK +case 33: +YY_RULE_SETUP +#line 183 "smtlib.lex" +{ return NOTES_TOK; } + YY_BREAK +case 34: +YY_RULE_SETUP +#line 184 "smtlib.lex" +{ return CVC_COMMAND_TOK; } + YY_BREAK +case 35: +YY_RULE_SETUP +#line 185 "smtlib.lex" +{ return SORTS_TOK; } + YY_BREAK +case 36: +YY_RULE_SETUP +#line 186 "smtlib.lex" +{ return FUNS_TOK; } + YY_BREAK +case 37: +YY_RULE_SETUP +#line 187 "smtlib.lex" +{ return PREDS_TOK; } + YY_BREAK +case 38: +YY_RULE_SETUP +#line 188 "smtlib.lex" +{ return EXTENSIONS_TOK; } + YY_BREAK +case 39: +YY_RULE_SETUP +#line 189 "smtlib.lex" +{ return DEFINITION_TOK; } + YY_BREAK +case 40: +YY_RULE_SETUP +#line 190 "smtlib.lex" +{ return AXIOMS_TOK; } + YY_BREAK +case 41: +YY_RULE_SETUP +#line 191 "smtlib.lex" +{ return LOGIC_TOK; } + YY_BREAK +case 42: +YY_RULE_SETUP +#line 192 "smtlib.lex" +{ return SAT_TOK; } + YY_BREAK +case 43: +YY_RULE_SETUP +#line 193 "smtlib.lex" +{ return UNSAT_TOK; } + YY_BREAK +case 44: +YY_RULE_SETUP +#line 194 "smtlib.lex" +{ return UNKNOWN_TOK; } + YY_BREAK +case 45: +YY_RULE_SETUP +#line 195 "smtlib.lex" +{ return ASSUMPTION_TOK; } + YY_BREAK +case 46: +YY_RULE_SETUP +#line 196 "smtlib.lex" +{ return FORMULA_TOK; } + YY_BREAK +case 47: +YY_RULE_SETUP +#line 197 "smtlib.lex" +{ return STATUS_TOK; } + YY_BREAK +case 48: +YY_RULE_SETUP +#line 198 "smtlib.lex" +{ return BENCHMARK_TOK; } + YY_BREAK +case 49: +YY_RULE_SETUP +#line 199 "smtlib.lex" +{ return EXTRASORTS_TOK; } + YY_BREAK +case 50: +YY_RULE_SETUP +#line 200 "smtlib.lex" +{ return EXTRAFUNS_TOK; } + YY_BREAK +case 51: +YY_RULE_SETUP +#line 201 "smtlib.lex" +{ return EXTRAPREDS_TOK; } + YY_BREAK +case 52: +YY_RULE_SETUP +#line 202 "smtlib.lex" +{ return LANGUAGE_TOK; } + YY_BREAK +case 53: +YY_RULE_SETUP +#line 203 "smtlib.lex" +{ return DISTINCT_TOK; } + YY_BREAK +case 54: +YY_RULE_SETUP +#line 204 "smtlib.lex" +{ return PAT_TOK; } + YY_BREAK +case 55: +YY_RULE_SETUP +#line 205 "smtlib.lex" +{ return COLON_TOK; } + YY_BREAK +case 56: +YY_RULE_SETUP +#line 206 "smtlib.lex" +{ return LBRACKET_TOK; } + YY_BREAK +case 57: +YY_RULE_SETUP +#line 207 "smtlib.lex" +{ return RBRACKET_TOK; } + YY_BREAK +case 58: +YY_RULE_SETUP +#line 208 "smtlib.lex" +{ return LCURBRACK_TOK;} + YY_BREAK +case 59: +YY_RULE_SETUP +#line 209 "smtlib.lex" +{ return RCURBRACK_TOK;} + YY_BREAK +case 60: +YY_RULE_SETUP +#line 210 "smtlib.lex" +{ return LPAREN_TOK; } + YY_BREAK +case 61: +YY_RULE_SETUP +#line 211 "smtlib.lex" +{ return RPAREN_TOK; } + YY_BREAK +case 62: +YY_RULE_SETUP +#line 212 "smtlib.lex" +{ return DOLLAR_TOK; } + YY_BREAK +case 63: +YY_RULE_SETUP +#line 213 "smtlib.lex" +{ return QUESTION_TOK; } + YY_BREAK +case 64: +YY_RULE_SETUP +#line 215 "smtlib.lex" +{ smtliblval.str = new std::string(smtlibtext); return AR_SYMB; } + YY_BREAK +case 65: +YY_RULE_SETUP +#line 216 "smtlib.lex" +{smtliblval.str = new std::string(smtlibtext); return SYM_TOK; } + YY_BREAK +case YY_STATE_EOF(INITIAL): +case YY_STATE_EOF(COMMENT): +case YY_STATE_EOF(STRING_LITERAL): +case YY_STATE_EOF(USER_VALUE): +case YY_STATE_EOF(PAT_MODE): +#line 218 "smtlib.lex" +{ return EOF_TOK; } + YY_BREAK +case 66: +YY_RULE_SETUP +#line 220 "smtlib.lex" +{ smtliberror("Illegal input character."); } + YY_BREAK +case 67: +YY_RULE_SETUP +#line 221 "smtlib.lex" +ECHO; + YY_BREAK +#line 1408 "smtlib_lexer.cpp" + + case YY_END_OF_BUFFER: + { + /* Amount of text matched not including the EOB char. */ + int yy_amount_of_matched_text = (int) (yy_cp - (yytext_ptr)) - 1; + + /* Undo the effects of YY_DO_BEFORE_ACTION. */ + *yy_cp = (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 smtlibin at a new source and called + * smtliblex(). 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. + */ + (yy_n_chars) = YY_CURRENT_BUFFER_LVALUE->yy_n_chars; + YY_CURRENT_BUFFER_LVALUE->yy_input_file = smtlibin; + 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 ( (yy_c_buf_p) <= &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars)] ) + { /* This was really a NUL. */ + yy_state_type yy_next_state; + + (yy_c_buf_p) = (yytext_ptr) + yy_amount_of_matched_text; + + yy_current_state = yy_get_previous_state( ); + + /* 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 ); + + yy_bp = (yytext_ptr) + YY_MORE_ADJ; + + if ( yy_next_state ) + { + /* Consume the NUL. */ + yy_cp = ++(yy_c_buf_p); + yy_current_state = yy_next_state; + goto yy_match; + } + + else + { + yy_cp = (yy_c_buf_p); + goto yy_find_action; + } + } + + else switch ( yy_get_next_buffer( ) ) + { + case EOB_ACT_END_OF_FILE: + { + (yy_did_buffer_switch_on_eof) = 0; + + if ( smtlibwrap( ) ) + { + /* Note: because we've taken care in + * yy_get_next_buffer() to have set up + * smtlibtext, 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. + */ + (yy_c_buf_p) = (yytext_ptr) + YY_MORE_ADJ; + + yy_act = YY_STATE_EOF(YY_START); + goto do_action; + } + + else + { + if ( ! (yy_did_buffer_switch_on_eof) ) + YY_NEW_FILE; + } + break; + } + + case EOB_ACT_CONTINUE_SCAN: + (yy_c_buf_p) = + (yytext_ptr) + yy_amount_of_matched_text; + + yy_current_state = yy_get_previous_state( ); + + yy_cp = (yy_c_buf_p); + yy_bp = (yytext_ptr) + YY_MORE_ADJ; + goto yy_match; + + case EOB_ACT_LAST_MATCH: + (yy_c_buf_p) = + &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars)]; + + yy_current_state = yy_get_previous_state( ); + + yy_cp = (yy_c_buf_p); + yy_bp = (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 smtliblex */ + +/* 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 (void) +{ + register char *dest = YY_CURRENT_BUFFER_LVALUE->yy_ch_buf; + register char *source = (yytext_ptr); + register int number_to_move, i; + int ret_val; + + if ( (yy_c_buf_p) > &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(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 ( (yy_c_buf_p) - (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) ((yy_c_buf_p) - (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 = (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; + + int yy_c_buf_p_offset = + (int) ((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. */ + smtlibrealloc((void *) b->yy_ch_buf,b->yy_buf_size + 2 ); + } + else + /* Can't grow it, we don't own it. */ + b->yy_ch_buf = 0; + + if ( ! b->yy_ch_buf ) + YY_FATAL_ERROR( + "fatal error - scanner input buffer overflow" ); + + (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]), + (yy_n_chars), (size_t) num_to_read ); + + YY_CURRENT_BUFFER_LVALUE->yy_n_chars = (yy_n_chars); + } + + if ( (yy_n_chars) == 0 ) + { + if ( number_to_move == YY_MORE_ADJ ) + { + ret_val = EOB_ACT_END_OF_FILE; + smtlibrestart(smtlibin ); + } + + 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 ((yy_size_t) ((yy_n_chars) + number_to_move) > YY_CURRENT_BUFFER_LVALUE->yy_buf_size) { + /* Extend the array by 50%, plus the number we really need. */ + yy_size_t new_size = (yy_n_chars) + number_to_move + ((yy_n_chars) >> 1); + YY_CURRENT_BUFFER_LVALUE->yy_ch_buf = (char *) smtlibrealloc((void *) YY_CURRENT_BUFFER_LVALUE->yy_ch_buf,new_size ); + if ( ! YY_CURRENT_BUFFER_LVALUE->yy_ch_buf ) + YY_FATAL_ERROR( "out of dynamic memory in yy_get_next_buffer()" ); + } + + (yy_n_chars) += number_to_move; + YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars)] = YY_END_OF_BUFFER_CHAR; + YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars) + 1] = YY_END_OF_BUFFER_CHAR; + + (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 (void) +{ + register yy_state_type yy_current_state; + register char *yy_cp; + + yy_current_state = (yy_start); + + for ( yy_cp = (yytext_ptr) + YY_MORE_ADJ; yy_cp < (yy_c_buf_p); ++yy_cp ) + { + register YY_CHAR yy_c = (*yy_cp ? yy_ec[YY_SC_TO_UI(*yy_cp)] : 1); + if ( yy_accept[yy_current_state] ) + { + (yy_last_accepting_state) = yy_current_state; + (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 >= 240 ) + yy_c = yy_meta[(unsigned int) yy_c]; + } + yy_current_state = yy_nxt[yy_base[yy_current_state] + (unsigned int) 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 ) +{ + register int yy_is_jam; + register char *yy_cp = (yy_c_buf_p); + + register YY_CHAR yy_c = 1; + if ( yy_accept[yy_current_state] ) + { + (yy_last_accepting_state) = yy_current_state; + (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 >= 240 ) + yy_c = yy_meta[(unsigned int) yy_c]; + } + yy_current_state = yy_nxt[yy_base[yy_current_state] + (unsigned int) yy_c]; + yy_is_jam = (yy_current_state == 239); + + return yy_is_jam ? 0 : yy_current_state; +} + +#ifndef YY_NO_INPUT +#ifdef __cplusplus + static int yyinput (void) +#else + static int input (void) +#endif + +{ + int c; + + *(yy_c_buf_p) = (yy_hold_char); + + if ( *(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 ( (yy_c_buf_p) < &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars)] ) + /* This was really a NUL. */ + *(yy_c_buf_p) = '\0'; + + else + { /* need more input */ + int offset = (yy_c_buf_p) - (yytext_ptr); + ++(yy_c_buf_p); + + switch ( yy_get_next_buffer( ) ) + { + 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. */ + smtlibrestart(smtlibin ); + + /*FALLTHROUGH*/ + + case EOB_ACT_END_OF_FILE: + { + if ( smtlibwrap( ) ) + return EOF; + + if ( ! (yy_did_buffer_switch_on_eof) ) + YY_NEW_FILE; +#ifdef __cplusplus + return yyinput(); +#else + return input(); +#endif + } + + case EOB_ACT_CONTINUE_SCAN: + (yy_c_buf_p) = (yytext_ptr) + offset; + break; + } + } + } + + c = *(unsigned char *) (yy_c_buf_p); /* cast for 8-bit char's */ + *(yy_c_buf_p) = '\0'; /* preserve smtlibtext */ + (yy_hold_char) = *++(yy_c_buf_p); + + if ( c == '\n' ) + + smtliblineno++; +; + + return c; +} +#endif /* ifndef YY_NO_INPUT */ + +/** Immediately switch to a different input stream. + * @param input_file A readable stream. + * + * @note This function does not reset the start condition to @c INITIAL . + */ + void smtlibrestart (FILE * input_file ) +{ + + if ( ! YY_CURRENT_BUFFER ){ + smtlibensure_buffer_stack (); + YY_CURRENT_BUFFER_LVALUE = + smtlib_create_buffer(smtlibin,YY_BUF_SIZE ); + } + + smtlib_init_buffer(YY_CURRENT_BUFFER,input_file ); + smtlib_load_buffer_state( ); +} + +/** Switch to a different input buffer. + * @param new_buffer The new input buffer. + * + */ + void smtlib_switch_to_buffer (YY_BUFFER_STATE new_buffer ) +{ + + /* TODO. We should be able to replace this entire function body + * with + * smtlibpop_buffer_state(); + * smtlibpush_buffer_state(new_buffer); + */ + smtlibensure_buffer_stack (); + if ( YY_CURRENT_BUFFER == new_buffer ) + return; + + if ( YY_CURRENT_BUFFER ) + { + /* Flush out information for old buffer. */ + *(yy_c_buf_p) = (yy_hold_char); + YY_CURRENT_BUFFER_LVALUE->yy_buf_pos = (yy_c_buf_p); + YY_CURRENT_BUFFER_LVALUE->yy_n_chars = (yy_n_chars); + } + + YY_CURRENT_BUFFER_LVALUE = new_buffer; + smtlib_load_buffer_state( ); + + /* We don't actually know whether we did this switch during + * EOF (smtlibwrap()) processing, but the only time this flag + * is looked at is after smtlibwrap() is called, so it's safe + * to go ahead and always set it. + */ + (yy_did_buffer_switch_on_eof) = 1; +} + +static void smtlib_load_buffer_state (void) +{ + (yy_n_chars) = YY_CURRENT_BUFFER_LVALUE->yy_n_chars; + (yytext_ptr) = (yy_c_buf_p) = YY_CURRENT_BUFFER_LVALUE->yy_buf_pos; + smtlibin = YY_CURRENT_BUFFER_LVALUE->yy_input_file; + (yy_hold_char) = *(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. + * + * @return the allocated buffer state. + */ + YY_BUFFER_STATE smtlib_create_buffer (FILE * file, int size ) +{ + YY_BUFFER_STATE b; + + b = (YY_BUFFER_STATE) smtliballoc(sizeof( struct yy_buffer_state ) ); + if ( ! b ) + YY_FATAL_ERROR( "out of dynamic memory in smtlib_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 *) smtliballoc(b->yy_buf_size + 2 ); + if ( ! b->yy_ch_buf ) + YY_FATAL_ERROR( "out of dynamic memory in smtlib_create_buffer()" ); + + b->yy_is_our_buffer = 1; + + smtlib_init_buffer(b,file ); + + return b; +} + +/** Destroy the buffer. + * @param b a buffer created with smtlib_create_buffer() + * + */ + void smtlib_delete_buffer (YY_BUFFER_STATE b ) +{ + + 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 ) + smtlibfree((void *) b->yy_ch_buf ); + + smtlibfree((void *) b ); +} + +#ifndef __cplusplus +extern int isatty (int ); +#endif /* __cplusplus */ + +/* Initializes or reinitializes a buffer. + * This function is sometimes called more than once on the same buffer, + * such as during a smtlibrestart() or at EOF. + */ + static void smtlib_init_buffer (YY_BUFFER_STATE b, FILE * file ) + +{ + int oerrno = errno; + + smtlib_flush_buffer(b ); + + b->yy_input_file = file; + b->yy_fill_buffer = 1; + + /* If b is the current buffer, then smtlib_init_buffer was _probably_ + * called from smtlibrestart() 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. + * + */ + void smtlib_flush_buffer (YY_BUFFER_STATE b ) +{ + 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 ) + smtlib_load_buffer_state( ); +} + +/** 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. + * + */ +void smtlibpush_buffer_state (YY_BUFFER_STATE new_buffer ) +{ + if (new_buffer == NULL) + return; + + smtlibensure_buffer_stack(); + + /* This block is copied from smtlib_switch_to_buffer. */ + if ( YY_CURRENT_BUFFER ) + { + /* Flush out information for old buffer. */ + *(yy_c_buf_p) = (yy_hold_char); + YY_CURRENT_BUFFER_LVALUE->yy_buf_pos = (yy_c_buf_p); + YY_CURRENT_BUFFER_LVALUE->yy_n_chars = (yy_n_chars); + } + + /* Only push if top exists. Otherwise, replace top. */ + if (YY_CURRENT_BUFFER) + (yy_buffer_stack_top)++; + YY_CURRENT_BUFFER_LVALUE = new_buffer; + + /* copied from smtlib_switch_to_buffer. */ + smtlib_load_buffer_state( ); + (yy_did_buffer_switch_on_eof) = 1; +} + +/** Removes and deletes the top of the stack, if present. + * The next element becomes the new top. + * + */ +void smtlibpop_buffer_state (void) +{ + if (!YY_CURRENT_BUFFER) + return; + + smtlib_delete_buffer(YY_CURRENT_BUFFER ); + YY_CURRENT_BUFFER_LVALUE = NULL; + if ((yy_buffer_stack_top) > 0) + --(yy_buffer_stack_top); + + if (YY_CURRENT_BUFFER) { + smtlib_load_buffer_state( ); + (yy_did_buffer_switch_on_eof) = 1; + } +} + +/* Allocates the stack if it does not exist. + * Guarantees space for at least one push. + */ +static void smtlibensure_buffer_stack (void) +{ + int num_to_alloc; + + if (!(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; + (yy_buffer_stack) = (struct yy_buffer_state**)smtliballoc + (num_to_alloc * sizeof(struct yy_buffer_state*) + ); + if ( ! (yy_buffer_stack) ) + YY_FATAL_ERROR( "out of dynamic memory in smtlibensure_buffer_stack()" ); + + memset((yy_buffer_stack), 0, num_to_alloc * sizeof(struct yy_buffer_state*)); + + (yy_buffer_stack_max) = num_to_alloc; + (yy_buffer_stack_top) = 0; + return; + } + + if ((yy_buffer_stack_top) >= ((yy_buffer_stack_max)) - 1){ + + /* Increase the buffer to prepare for a possible push. */ + int grow_size = 8 /* arbitrary grow size */; + + num_to_alloc = (yy_buffer_stack_max) + grow_size; + (yy_buffer_stack) = (struct yy_buffer_state**)smtlibrealloc + ((yy_buffer_stack), + num_to_alloc * sizeof(struct yy_buffer_state*) + ); + if ( ! (yy_buffer_stack) ) + YY_FATAL_ERROR( "out of dynamic memory in smtlibensure_buffer_stack()" ); + + /* zero only the new slots.*/ + memset((yy_buffer_stack) + (yy_buffer_stack_max), 0, grow_size * sizeof(struct yy_buffer_state*)); + (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 + * + * @return the newly allocated buffer state object. + */ +YY_BUFFER_STATE smtlib_scan_buffer (char * base, yy_size_t size ) +{ + 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 0; + + b = (YY_BUFFER_STATE) smtliballoc(sizeof( struct yy_buffer_state ) ); + if ( ! b ) + YY_FATAL_ERROR( "out of dynamic memory in smtlib_scan_buffer()" ); + + b->yy_buf_size = 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 = 0; + 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; + + smtlib_switch_to_buffer(b ); + + return b; +} + +/** Setup the input buffer state to scan a string. The next call to smtliblex() will + * scan from a @e copy of @a str. + * @param yystr a NUL-terminated string to scan + * + * @return the newly allocated buffer state object. + * @note If you want to scan bytes that may contain NUL values, then use + * smtlib_scan_bytes() instead. + */ +YY_BUFFER_STATE smtlib_scan_string (yyconst char * yystr ) +{ + + return smtlib_scan_bytes(yystr,strlen(yystr) ); +} + +/** Setup the input buffer state to scan the given bytes. The next call to smtliblex() 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. + * + * @return the newly allocated buffer state object. + */ +YY_BUFFER_STATE smtlib_scan_bytes (yyconst char * yybytes, int _yybytes_len ) +{ + YY_BUFFER_STATE b; + char *buf; + yy_size_t n; + int i; + + /* Get memory for full buffer, including space for trailing EOB's. */ + n = _yybytes_len + 2; + buf = (char *) smtliballoc(n ); + if ( ! buf ) + YY_FATAL_ERROR( "out of dynamic memory in smtlib_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 = smtlib_scan_buffer(buf,n ); + if ( ! b ) + YY_FATAL_ERROR( "bad buffer in smtlib_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; +} + +#ifndef YY_EXIT_FAILURE +#define YY_EXIT_FAILURE 2 +#endif + +static void yy_fatal_error (yyconst char* msg ) +{ + (void) 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 smtlibtext. */ \ + int yyless_macro_arg = (n); \ + YY_LESS_LINENO(yyless_macro_arg);\ + smtlibtext[smtlibleng] = (yy_hold_char); \ + (yy_c_buf_p) = smtlibtext + yyless_macro_arg; \ + (yy_hold_char) = *(yy_c_buf_p); \ + *(yy_c_buf_p) = '\0'; \ + smtlibleng = yyless_macro_arg; \ + } \ + while ( 0 ) + +/* Accessor methods (get/set functions) to struct members. */ + +/** Get the current line number. + * + */ +int smtlibget_lineno (void) +{ + + return smtliblineno; +} + +/** Get the input stream. + * + */ +FILE *smtlibget_in (void) +{ + return smtlibin; +} + +/** Get the output stream. + * + */ +FILE *smtlibget_out (void) +{ + return smtlibout; +} + +/** Get the length of the current token. + * + */ +int smtlibget_leng (void) +{ + return smtlibleng; +} + +/** Get the current token. + * + */ + +char *smtlibget_text (void) +{ + return smtlibtext; +} + +/** Set the current line number. + * @param line_number + * + */ +void smtlibset_lineno (int line_number ) +{ + + smtliblineno = line_number; +} + +/** Set the input stream. This does not discard the current + * input buffer. + * @param in_str A readable stream. + * + * @see smtlib_switch_to_buffer + */ +void smtlibset_in (FILE * in_str ) +{ + smtlibin = in_str ; +} + +void smtlibset_out (FILE * out_str ) +{ + smtlibout = out_str ; +} + +int smtlibget_debug (void) +{ + return smtlib_flex_debug; +} + +void smtlibset_debug (int bdebug ) +{ + smtlib_flex_debug = bdebug ; +} + +static int yy_init_globals (void) +{ + /* Initialization is the same as for the non-reentrant scanner. + * This function is called from smtliblex_destroy(), so don't allocate here. + */ + + /* We do not touch smtliblineno unless the option is enabled. */ + smtliblineno = 1; + + (yy_buffer_stack) = 0; + (yy_buffer_stack_top) = 0; + (yy_buffer_stack_max) = 0; + (yy_c_buf_p) = (char *) 0; + (yy_init) = 0; + (yy_start) = 0; + +/* Defined in main.c */ +#ifdef YY_STDINIT + smtlibin = stdin; + smtlibout = stdout; +#else + smtlibin = (FILE *) 0; + smtlibout = (FILE *) 0; +#endif + + /* For future reference: Set errno on error, since we are called by + * smtliblex_init() + */ + return 0; +} + +/* smtliblex_destroy is for both reentrant and non-reentrant scanners. */ +int smtliblex_destroy (void) +{ + + /* Pop the buffer stack, destroying each element. */ + while(YY_CURRENT_BUFFER){ + smtlib_delete_buffer(YY_CURRENT_BUFFER ); + YY_CURRENT_BUFFER_LVALUE = NULL; + smtlibpop_buffer_state(); + } + + /* Destroy the stack itself. */ + smtlibfree((yy_buffer_stack) ); + (yy_buffer_stack) = NULL; + + /* Reset the globals. This is important in a non-reentrant scanner so the next time + * smtliblex() is called, initialization will occur. */ + yy_init_globals( ); + + return 0; +} + +/* + * Internal utility routines. + */ + +#ifndef yytext_ptr +static void yy_flex_strncpy (char* s1, yyconst char * s2, int n ) +{ + register int i; + for ( i = 0; i < n; ++i ) + s1[i] = s2[i]; +} +#endif + +#ifdef YY_NEED_STRLEN +static int yy_flex_strlen (yyconst char * s ) +{ + register int n; + for ( n = 0; s[n]; ++n ) + ; + + return n; +} +#endif + +void *smtliballoc (yy_size_t size ) +{ + return (void *) malloc( size ); +} + +void *smtlibrealloc (void * ptr, yy_size_t size ) +{ + /* 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 (void *) realloc( (char *) ptr, size ); +} + +void smtlibfree (void * ptr ) +{ + free( (char *) ptr ); /* see smtlibrealloc() for (char *) cast */ +} + +#define YYTABLES_NAME "yytables" + +#line 221 "smtlib.lex" + + + + |