1 /* 2 * This file is part of the Yices SMT Solver. 3 * Copyright (C) 2017 SRI International. 4 * 5 * Yices is free software: you can redistribute it and/or modify 6 * it under the terms of the GNU General Public License as published by 7 * the Free Software Foundation, either version 3 of the License, or 8 * (at your option) any later version. 9 * 10 * Yices is distributed in the hope that it will be useful, 11 * but WITHOUT ANY WARRANTY; without even the implied warranty of 12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 13 * GNU General Public License for more details. 14 * 15 * You should have received a copy of the GNU General Public License 16 * along with Yices. If not, see <http://www.gnu.org/licenses/>. 17 */ 18 19 // get token type 20 #include "frontend/yices/yices_lexer.h" 21 22 typedef enum state_s { 23 r0, 24 c0, c1, c2, c3, c6, c7, c9, c10, c11, c12, c13, 25 c14, c15, c16, c17, c18, c19, c20, 26 td0, td1, td2, td3, 27 t0, t1, t4, t6, 28 e0, e1, e3, e5, e7, e10, e11, e12, e14, e15, e16, e17, e19, e20, 29 } state_t; 30 31 typedef struct { 32 state_t source; 33 token_t token; 34 char *value; 35 } triple_t; 36 37 #define DEFAULT_TOKEN -1 38 39 /* 40 * Action codes 41 */ 42 enum actions { 43 next_goto_c1, 44 empty_command, 45 exit_next_goto_r0, 46 check_next_goto_r0, 47 check_assuming_next_goto_c16, 48 push_next_goto_r0, 49 pop_next_goto_r0, 50 reset_next_goto_r0, 51 dump_context_next_goto_r0, 52 echo_next_goto_c3, 53 include_next_goto_c3, 54 assert_next_push_c20_goto_e0, 55 deftype_next_goto_c2, 56 defterm_next_goto_c6, 57 showmodel_next_goto_r0, 58 eval_next_push_r0_goto_e0, 59 setparam_next_goto_c11, 60 showparam_next_goto_c13, 61 showparams_next_goto_r0, 62 showstats_next_goto_r0, 63 resetstats_next_goto_r0, 64 showtimeout_next_goto_r0, 65 settimeout_next_goto_c14, 66 help_next_goto_c15, 67 efsolve_next_goto_r0, // New command: (ef-solve) 68 export_next_goto_c3, // New command: (export-to-dimacs filename) 69 implicant_next_goto_r0, // New command: (show-implicant) 70 unsat_core_next_goto_r0, // (show-unsat-core) 71 unsat_assumptions_next_goto_r0, // (show-unsat-assumptions) 72 reduced_model_next_goto_r0, // (show-reduced-model) 73 74 typename_next_goto_c10, // token must be a free typename (TK_SYMBOL) 75 string_next_goto_r0, // string argument to echo, include, help, export 76 termname_next_goto_c7, // token must be a free termname (TK_SYMBOL) 77 next_push_c9_goto_t0, 78 symbol_next_goto_c12, // in (set-param <symbol> ...) 79 true_next_goto_r0, // in (set-param ... true) 80 false_next_goto_r0, // in (set-param ... false) 81 float_next_goto_r0, // in (set-param ... <float>) 82 symbol_next_goto_r0, // in (show-param <symbol>) or (help <symbol>) or (set-param ... <symbol>) 83 ret, // return 84 push_r0_goto_e0, 85 push_r0_goto_td0, 86 87 symbol_next_goto_c16, // positive assumption 88 next_goto_c17, 89 not_next_goto_c18, 90 symbol_next_goto_c19, // negated assumption 91 next_goto_c16, 92 93 int_return, 94 real_return, 95 bool_return, 96 typesymbol_return, // TK_SYMBOL bound to a type 97 next_goto_td1, 98 scalar_next_goto_td2, 99 bitvector_next_goto_t4, 100 tuple_next_push_t6_goto_t0, 101 arrow_next_push_t6_push_t0_goto_t0, 102 termname_next_goto_td3, // free termane in scalar definition 103 104 next_goto_t1, 105 rational_next_goto_r0, 106 push_t6_goto_t0, 107 108 true_return, 109 false_return, 110 rational_return, 111 float_return, 112 bvbin_return, 113 bvhex_return, 114 termsymbol_return, // TK_SYMBOL bound to a term 115 next_goto_e1, 116 117 // all function keywords 118 if_next_push_e3_goto_e0, 119 eq_next_push_e3_goto_e0, 120 diseq_next_push_e3_goto_e0, 121 distinct_next_push_e3_goto_e0, 122 or_next_push_e3_goto_e0, 123 and_next_push_e3_goto_e0, 124 not_next_push_e3_goto_e0, 125 xor_next_push_e3_goto_e0, 126 iff_next_push_e3_goto_e0, 127 implies_next_push_e3_goto_e0, 128 mk_tuple_next_push_e3_goto_e0, 129 select_next_push_e3_goto_e0, 130 update_tuple_next_push_e3_goto_e0, 131 add_next_push_e3_goto_e0, 132 sub_next_push_e3_goto_e0, 133 mul_next_push_e3_goto_e0, 134 div_next_push_e3_goto_e0, 135 pow_next_push_e3_goto_e0, 136 lt_next_push_e3_goto_e0, 137 le_next_push_e3_goto_e0, 138 gt_next_push_e3_goto_e0, 139 ge_next_push_e3_goto_e0, 140 mk_bv_next_push_e3_goto_e0, 141 bv_add_next_push_e3_goto_e0, 142 bv_sub_next_push_e3_goto_e0, 143 bv_mul_next_push_e3_goto_e0, 144 bv_neg_next_push_e3_goto_e0, 145 bv_pow_next_push_e3_goto_e0, 146 bv_not_next_push_e3_goto_e0, 147 bv_and_next_push_e3_goto_e0, 148 bv_or_next_push_e3_goto_e0, 149 bv_xor_next_push_e3_goto_e0, 150 bv_nand_next_push_e3_goto_e0, 151 bv_nor_next_push_e3_goto_e0, 152 bv_xnor_next_push_e3_goto_e0, 153 bv_shift_left0_next_push_e3_goto_e0, 154 bv_shift_left1_next_push_e3_goto_e0, 155 bv_shift_right0_next_push_e3_goto_e0, 156 bv_shift_right1_next_push_e3_goto_e0, 157 bv_ashift_right_next_push_e3_goto_e0, 158 bv_rotate_left_next_push_e3_goto_e0, 159 bv_rotate_right_next_push_e3_goto_e0, 160 bv_extract_next_push_e3_goto_e0, 161 bv_concat_next_push_e3_goto_e0, 162 bv_repeat_next_push_e3_goto_e0, 163 bv_sign_extend_next_push_e3_goto_e0, 164 bv_zero_extend_next_push_e3_goto_e0, 165 bv_ge_next_push_e3_goto_e0, 166 bv_gt_next_push_e3_goto_e0, 167 bv_le_next_push_e3_goto_e0, 168 bv_lt_next_push_e3_goto_e0, 169 bv_sge_next_push_e3_goto_e0, 170 bv_sgt_next_push_e3_goto_e0, 171 bv_sle_next_push_e3_goto_e0, 172 bv_slt_next_push_e3_goto_e0, 173 bv_shl_next_push_e3_goto_e0, 174 bv_lshr_next_push_e3_goto_e0, 175 bv_ashr_next_push_e3_goto_e0, 176 bv_div_next_push_e3_goto_e0, 177 bv_rem_next_push_e3_goto_e0, 178 bv_sdiv_next_push_e3_goto_e0, 179 bv_srem_next_push_e3_goto_e0, 180 bv_smod_next_push_e3_goto_e0, 181 bv_redor_next_push_e3_goto_e0, 182 bv_redand_next_push_e3_goto_e0, 183 bv_comp_next_push_e3_goto_e0, 184 bool_to_bv_next_push_e3_goto_e0, 185 bit_next_push_e3_goto_e0, 186 floor_next_push_e3_goto_e0, 187 ceil_next_push_e3_goto_e0, 188 abs_next_push_e3_goto_e0, 189 idiv_next_push_e3_goto_e0, 190 mod_next_push_e3_goto_e0, 191 divides_next_push_e3_goto_e0, 192 is_int_next_push_e3_goto_e0, 193 194 update_next_push_e5_goto_e0, 195 forall_next_goto_e10, 196 exists_next_goto_e10, 197 lambda_next_goto_e10, 198 let_next_goto_e15, 199 push_e3_push_e0_goto_e0, 200 201 push_e3_goto_e0, 202 next_push_e7_goto_e0, 203 next_push_r0_goto_e0, 204 push_e7_goto_e0, 205 next_goto_e11, 206 e11_varname_next_goto_e12, // first var decl in quantifiers 207 next_push_e14_goto_t0, 208 e14_varname_next_goto_e12, // var decl in quantifier except the first one 209 e14_next_push_r0_goto_e0, // end of var decls 210 211 next_goto_e16, 212 next_goto_e17, 213 termname_next_push_e19_goto_e0, // name in binding 214 next_goto_e20, 215 216 error_lpar_expected, 217 error_symbol_expected, 218 error_string_expected, 219 error_colon_colon_expected, 220 error_rational_expected, 221 error_rpar_expected, 222 error_not_expected, 223 error_not_a_command, 224 error, 225 }; 226 227 static triple_t triples[] = { 228 { c0, TK_LP, "next_goto_c1" }, 229 { c0, TK_EOS, "empty_command" }, 230 { c0, DEFAULT_TOKEN, "error_lpar_expected" }, 231 232 { c1, TK_EXIT, "exit_next_goto_r0" }, 233 { c1, TK_CHECK, "check_next_goto_r0" }, 234 { c1, TK_CHECK_ASSUMING, "check_assuming_next_goto_c16" }, 235 { c1, TK_PUSH, "push_next_goto_r0" }, 236 { c1, TK_POP, "pop_next_goto_r0" }, 237 { c1, TK_RESET, "reset_next_goto_r0" }, 238 { c1, TK_DUMP_CONTEXT, "dump_context_next_goto_r0" }, 239 { c1, TK_ECHO, "echo_next_goto_c3" }, 240 { c1, TK_INCLUDE, "include_next_goto_c3" }, 241 { c1, TK_ASSERT, "assert_next_push_c20_goto_e0" }, 242 { c1, TK_DEFINE_TYPE, "deftype_next_goto_c2" }, 243 { c1, TK_DEFINE, "defterm_next_goto_c6" }, 244 { c1, TK_SHOW_MODEL, "showmodel_next_goto_r0" }, 245 { c1, TK_EVAL, "eval_next_push_r0_goto_e0" }, 246 { c1, TK_SET_PARAM, "setparam_next_goto_c11" }, 247 { c1, TK_SHOW_PARAM, "showparam_next_goto_c13" }, 248 { c1, TK_SHOW_PARAMS, "showparams_next_goto_r0" }, 249 { c1, TK_SHOW_STATS, "showstats_next_goto_r0" }, 250 { c1, TK_SHOW_TIMEOUT, "showtimeout_next_goto_r0" }, 251 { c1, TK_RESET_STATS, "resetstats_next_goto_r0" }, 252 { c1, TK_SET_TIMEOUT, "settimeout_next_goto_c14" }, 253 { c1, TK_HELP, "help_next_goto_c15" }, 254 { c1, TK_EF_SOLVE, "efsolve_next_goto_r0" }, 255 { c1, TK_EXPORT_TO_DIMACS, "export_next_goto_c3" }, 256 { c1, TK_SHOW_IMPLICANT, "implicant_next_goto_r0" }, 257 { c1, TK_SHOW_UNSAT_CORE, "unsat_core_next_goto_r0" }, 258 { c1, TK_SHOW_UNSAT_ASSUMPTIONS, "unsat_assumptions_next_goto_r0" }, 259 { c1, TK_SHOW_REDUCED_MODEL, "reduced_model_next_goto_r0" }, 260 { c1, TK_SYMBOL, "error_not_a_command" }, 261 262 { c2, TK_SYMBOL, "typename_next_goto_c10" }, 263 { c2, DEFAULT_TOKEN, "error_symbol_expected" }, 264 265 { c3, TK_STRING, "string_next_goto_r0" }, 266 { c3, DEFAULT_TOKEN, "error_string_expected" }, 267 268 { c6, TK_SYMBOL, "termname_next_goto_c7" }, 269 { c6, DEFAULT_TOKEN, "error_symbol_expected" }, 270 271 { c7, TK_COLON_COLON, "next_push_c9_goto_t0" }, 272 { c7, DEFAULT_TOKEN, "error_colon_colon_expected" }, 273 274 { c9, TK_RP, "ret" }, 275 { c9, DEFAULT_TOKEN, "push_r0_goto_e0" }, 276 277 { c10, TK_RP, "ret" }, 278 { c10, DEFAULT_TOKEN, "push_r0_goto_td0" }, 279 280 { c11, TK_SYMBOL, "symbol_next_goto_c12" }, 281 { c11, DEFAULT_TOKEN, "error_symbol_expected" }, 282 283 { c12, TK_TRUE, "true_next_goto_r0" }, 284 { c12, TK_FALSE, "false_next_goto_r0" }, 285 { c12, TK_NUM_RATIONAL, "rational_next_goto_r0" }, 286 { c12, TK_NUM_FLOAT, "float_next_goto_r0" }, 287 { c12, TK_SYMBOL, "symbol_next_goto_r0" }, 288 289 { c13, TK_SYMBOL, "symbol_next_goto_r0" }, 290 291 { c14, TK_NUM_RATIONAL, "rational_next_goto_r0" }, 292 293 // c15: parameters to (help ...): treat all keywords as symbols here 294 { c15, TK_DEFINE_TYPE, "symbol_next_goto_r0" }, 295 { c15, TK_DEFINE, "symbol_next_goto_r0" }, 296 { c15, TK_ASSERT, "symbol_next_goto_r0" }, 297 { c15, TK_CHECK, "symbol_next_goto_r0" }, 298 { c15, TK_CHECK_ASSUMING, "symbol_next_goto_r0" }, 299 { c15, TK_PUSH, "symbol_next_goto_r0" }, 300 { c15, TK_POP, "symbol_next_goto_r0" }, 301 { c15, TK_RESET, "symbol_next_goto_r0" }, 302 { c15, TK_DUMP_CONTEXT, "symbol_next_goto_r0" }, 303 { c15, TK_EXIT, "symbol_next_goto_r0" }, 304 { c15, TK_ECHO, "symbol_next_goto_r0" }, 305 { c15, TK_INCLUDE, "symbol_next_goto_r0" }, 306 { c15, TK_SHOW_MODEL, "symbol_next_goto_r0" }, 307 { c15, TK_EVAL, "symbol_next_goto_r0" }, 308 { c15, TK_SET_PARAM, "symbol_next_goto_r0" }, 309 { c15, TK_SHOW_PARAM, "symbol_next_goto_r0" }, 310 { c15, TK_SHOW_PARAMS, "symbol_next_goto_r0" }, 311 { c15, TK_SHOW_STATS, "symbol_next_goto_r0" }, 312 { c15, TK_RESET_STATS, "symbol_next_goto_r0" }, 313 { c15, TK_SET_TIMEOUT, "symbol_next_goto_r0" }, 314 { c15, TK_SHOW_TIMEOUT, "symbol_next_goto_r0" }, 315 { c15, TK_HELP, "symbol_next_goto_r0" }, 316 { c15, TK_EF_SOLVE, "symbol_next_goto_r0" }, 317 { c15, TK_EXPORT_TO_DIMACS, "symbol_next_goto_r0" }, 318 { c15, TK_SHOW_IMPLICANT, "symbol_next_goto_r0" }, 319 { c15, TK_SHOW_UNSAT_CORE, "symbol_next_goto_r0" }, 320 { c15, TK_SHOW_UNSAT_ASSUMPTIONS, "symbol_next_goto_r0" }, 321 { c15, TK_SHOW_REDUCED_MODEL, "symbol_next_goto_r0" }, 322 { c15, TK_UPDATE, "symbol_next_goto_r0" }, 323 { c15, TK_FORALL, "symbol_next_goto_r0" }, 324 { c15, TK_EXISTS, "symbol_next_goto_r0" }, 325 { c15, TK_LAMBDA, "symbol_next_goto_r0" }, 326 { c15, TK_LET, "symbol_next_goto_r0" }, 327 { c15, TK_BOOL, "symbol_next_goto_r0" }, 328 { c15, TK_INT, "symbol_next_goto_r0" }, 329 { c15, TK_REAL, "symbol_next_goto_r0" }, 330 { c15, TK_BITVECTOR, "symbol_next_goto_r0" }, 331 { c15, TK_SCALAR, "symbol_next_goto_r0" }, 332 { c15, TK_TUPLE, "symbol_next_goto_r0" }, 333 { c15, TK_ARROW, "symbol_next_goto_r0" }, 334 { c15, TK_TRUE, "symbol_next_goto_r0" }, 335 { c15, TK_FALSE, "symbol_next_goto_r0" }, 336 { c15, TK_IF, "symbol_next_goto_r0" }, 337 { c15, TK_ITE, "symbol_next_goto_r0" }, 338 { c15, TK_EQ, "symbol_next_goto_r0" }, 339 { c15, TK_DISEQ, "symbol_next_goto_r0" }, 340 { c15, TK_DISTINCT, "symbol_next_goto_r0" }, 341 { c15, TK_OR, "symbol_next_goto_r0" }, 342 { c15, TK_AND, "symbol_next_goto_r0" }, 343 { c15, TK_NOT, "symbol_next_goto_r0" }, 344 { c15, TK_XOR, "symbol_next_goto_r0" }, 345 { c15, TK_IFF, "symbol_next_goto_r0" }, 346 { c15, TK_IMPLIES, "symbol_next_goto_r0" }, 347 { c15, TK_MK_TUPLE, "symbol_next_goto_r0" }, 348 { c15, TK_SELECT, "symbol_next_goto_r0" }, 349 { c15, TK_UPDATE_TUPLE, "symbol_next_goto_r0" }, 350 { c15, TK_ADD, "symbol_next_goto_r0" }, 351 { c15, TK_SUB, "symbol_next_goto_r0" }, 352 { c15, TK_MUL, "symbol_next_goto_r0" }, 353 { c15, TK_DIV, "symbol_next_goto_r0" }, 354 { c15, TK_POW, "symbol_next_goto_r0" }, 355 { c15, TK_LT, "symbol_next_goto_r0" }, 356 { c15, TK_LE, "symbol_next_goto_r0" }, 357 { c15, TK_GT, "symbol_next_goto_r0" }, 358 { c15, TK_GE, "symbol_next_goto_r0" }, 359 { c15, TK_MK_BV, "symbol_next_goto_r0" }, 360 { c15, TK_BV_ADD, "symbol_next_goto_r0" }, 361 { c15, TK_BV_SUB, "symbol_next_goto_r0" }, 362 { c15, TK_BV_MUL, "symbol_next_goto_r0" }, 363 { c15, TK_BV_NEG, "symbol_next_goto_r0" }, 364 { c15, TK_BV_POW, "symbol_next_goto_r0" }, 365 { c15, TK_BV_NOT, "symbol_next_goto_r0" }, 366 { c15, TK_BV_AND, "symbol_next_goto_r0" }, 367 { c15, TK_BV_OR, "symbol_next_goto_r0" }, 368 { c15, TK_BV_XOR, "symbol_next_goto_r0" }, 369 { c15, TK_BV_NAND, "symbol_next_goto_r0" }, 370 { c15, TK_BV_NOR, "symbol_next_goto_r0" }, 371 { c15, TK_BV_XNOR, "symbol_next_goto_r0" }, 372 { c15, TK_BV_SHIFT_LEFT0, "symbol_next_goto_r0" }, 373 { c15, TK_BV_SHIFT_LEFT1, "symbol_next_goto_r0" }, 374 { c15, TK_BV_SHIFT_RIGHT0, "symbol_next_goto_r0" }, 375 { c15, TK_BV_SHIFT_RIGHT1, "symbol_next_goto_r0" }, 376 { c15, TK_BV_ASHIFT_RIGHT, "symbol_next_goto_r0" }, 377 { c15, TK_BV_ROTATE_LEFT, "symbol_next_goto_r0" }, 378 { c15, TK_BV_ROTATE_RIGHT, "symbol_next_goto_r0" }, 379 { c15, TK_BV_EXTRACT, "symbol_next_goto_r0" }, 380 { c15, TK_BV_CONCAT, "symbol_next_goto_r0" }, 381 { c15, TK_BV_REPEAT, "symbol_next_goto_r0" }, 382 { c15, TK_BV_SIGN_EXTEND, "symbol_next_goto_r0" }, 383 { c15, TK_BV_ZERO_EXTEND, "symbol_next_goto_r0" }, 384 { c15, TK_BV_GE, "symbol_next_goto_r0" }, 385 { c15, TK_BV_GT, "symbol_next_goto_r0" }, 386 { c15, TK_BV_LE, "symbol_next_goto_r0" }, 387 { c15, TK_BV_LT, "symbol_next_goto_r0" }, 388 { c15, TK_BV_SGE, "symbol_next_goto_r0" }, 389 { c15, TK_BV_SGT, "symbol_next_goto_r0" }, 390 { c15, TK_BV_SLE, "symbol_next_goto_r0" }, 391 { c15, TK_BV_SLT, "symbol_next_goto_r0" }, 392 { c15, TK_BV_SHL, "symbol_next_goto_r0" }, 393 { c15, TK_BV_LSHR, "symbol_next_goto_r0" }, 394 { c15, TK_BV_ASHR, "symbol_next_goto_r0" }, 395 { c15, TK_BV_DIV, "symbol_next_goto_r0" }, 396 { c15, TK_BV_REM, "symbol_next_goto_r0" }, 397 { c15, TK_BV_SDIV, "symbol_next_goto_r0" }, 398 { c15, TK_BV_SREM, "symbol_next_goto_r0" }, 399 { c15, TK_BV_SMOD, "symbol_next_goto_r0" }, 400 { c15, TK_BV_REDOR, "symbol_next_goto_r0" }, 401 { c15, TK_BV_REDAND, "symbol_next_goto_r0" }, 402 { c15, TK_BV_COMP, "symbol_next_goto_r0" }, 403 { c15, TK_BOOL_TO_BV, "symbol_next_goto_r0" }, 404 { c15, TK_BIT, "symbol_next_goto_r0" }, 405 { c15, TK_FLOOR, "symbol_next_goto_r0" }, 406 { c15, TK_CEIL, "symbol_next_goto_r0" }, 407 { c15, TK_ABS, "symbol_next_goto_r0" }, 408 { c15, TK_IDIV, "symbol_next_goto_r0" }, 409 { c15, TK_MOD, "symbol_next_goto_r0" }, 410 { c15, TK_DIVIDES, "symbol_next_goto_r0" }, 411 { c15, TK_IS_INT, "symbol_next_goto_r0" }, 412 { c15, TK_SYMBOL, "symbol_next_goto_r0" }, 413 { c15, TK_STRING, "string_next_goto_r0" }, 414 { c15, TK_RP, "ret" }, 415 416 // list of assumptions 417 { c16, TK_RP, "ret" }, 418 { c16, TK_SYMBOL, "symbol_next_goto_c16" }, 419 { c16, TK_LP, "next_goto_c17" }, 420 421 { c17, TK_NOT, "not_next_goto_c18" }, 422 { c17, DEFAULT_TOKEN, "error_not_expected" }, 423 424 { c18, TK_SYMBOL, "symbol_next_goto_c19" }, 425 { c18, DEFAULT_TOKEN, "error_symbol_expected" }, 426 427 { c19, TK_RP, "next_goto_c16" }, 428 { c19, DEFAULT_TOKEN, "error_rpar_expected" }, 429 430 { c20, TK_RP, "ret" }, 431 { c20, TK_SYMBOL, "symbol_next_goto_r0" }, 432 433 { td0, TK_INT, "int_return" }, 434 { td0, TK_REAL, "real_return" }, 435 { td0, TK_BOOL, "bool_return" }, 436 { td0, TK_SYMBOL, "typesymbol_return" }, 437 { td0, TK_LP, "next_goto_td1" }, 438 439 { td1, TK_SCALAR, "scalar_next_goto_td2" }, 440 { td1, TK_BITVECTOR, "bitvector_next_goto_t4" }, 441 { td1, TK_TUPLE, "tuple_next_push_t6_goto_t0" }, 442 { td1, TK_ARROW, "arrow_next_push_t6_push_t0_goto_t0" }, 443 444 { td2, TK_SYMBOL, "termname_next_goto_td3" }, 445 { td2, DEFAULT_TOKEN, "error_symbol_expected" }, 446 447 { td3, TK_RP, "ret" }, 448 { td3, TK_SYMBOL, "termname_next_goto_td3" }, 449 450 { t0, TK_INT, "int_return" }, 451 { t0, TK_REAL, "real_return" }, 452 { t0, TK_BOOL, "bool_return" }, 453 { t0, TK_SYMBOL, "typesymbol_return" }, 454 { t0, TK_LP, "next_goto_t1" }, 455 456 { t1, TK_BITVECTOR, "bitvector_next_goto_t4" }, 457 { t1, TK_TUPLE, "tuple_next_push_t6_goto_t0" }, 458 { t1, TK_ARROW, "arrow_next_push_t6_push_t0_goto_t0" }, 459 460 { t4, TK_NUM_RATIONAL, "rational_next_goto_r0" }, 461 { t4, DEFAULT_TOKEN, "error_rational_expected" }, 462 463 { t6, TK_RP, "ret" }, 464 { t6, DEFAULT_TOKEN, "push_t6_goto_t0" }, 465 466 { e0, TK_TRUE, "true_return" }, 467 { e0, TK_FALSE, "false_return" }, 468 { e0, TK_NUM_RATIONAL, "rational_return" }, 469 { e0, TK_NUM_FLOAT, "float_return" }, 470 { e0, TK_BV_CONSTANT, "bvbin_return" }, 471 { e0, TK_HEX_CONSTANT, "bvhex_return" }, 472 { e0, TK_SYMBOL, "termsymbol_return" }, 473 { e0, TK_LP, "next_goto_e1" }, 474 475 { e1, TK_IF, "if_next_push_e3_goto_e0" }, 476 { e1, TK_ITE, "if_next_push_e3_goto_e0" }, 477 { e1, TK_EQ, "eq_next_push_e3_goto_e0" }, 478 { e1, TK_DISEQ, "diseq_next_push_e3_goto_e0" }, 479 { e1, TK_DISTINCT, "distinct_next_push_e3_goto_e0" }, 480 { e1, TK_OR, "or_next_push_e3_goto_e0" }, 481 { e1, TK_AND, "and_next_push_e3_goto_e0" }, 482 { e1, TK_NOT, "not_next_push_e3_goto_e0" }, 483 { e1, TK_XOR, "xor_next_push_e3_goto_e0" }, 484 { e1, TK_IFF, "iff_next_push_e3_goto_e0" }, 485 { e1, TK_IMPLIES, "implies_next_push_e3_goto_e0" }, 486 { e1, TK_MK_TUPLE, "mk_tuple_next_push_e3_goto_e0" }, 487 { e1, TK_SELECT, "select_next_push_e3_goto_e0" }, 488 { e1, TK_UPDATE_TUPLE, "update_tuple_next_push_e3_goto_e0" }, 489 { e1, TK_ADD, "add_next_push_e3_goto_e0" }, 490 { e1, TK_SUB, "sub_next_push_e3_goto_e0" }, 491 { e1, TK_MUL, "mul_next_push_e3_goto_e0" }, 492 { e1, TK_DIV, "div_next_push_e3_goto_e0" }, 493 { e1, TK_POW, "pow_next_push_e3_goto_e0" }, 494 { e1, TK_LT, "lt_next_push_e3_goto_e0" }, 495 { e1, TK_LE, "le_next_push_e3_goto_e0" }, 496 { e1, TK_GT, "gt_next_push_e3_goto_e0" }, 497 { e1, TK_GE, "ge_next_push_e3_goto_e0" }, 498 { e1, TK_MK_BV, "mk_bv_next_push_e3_goto_e0" }, 499 { e1, TK_BV_ADD, "bv_add_next_push_e3_goto_e0" }, 500 { e1, TK_BV_SUB, "bv_sub_next_push_e3_goto_e0" }, 501 { e1, TK_BV_MUL, "bv_mul_next_push_e3_goto_e0" }, 502 { e1, TK_BV_NEG, "bv_neg_next_push_e3_goto_e0" }, 503 { e1, TK_BV_POW, "bv_pow_next_push_e3_goto_e0" }, 504 { e1, TK_BV_NOT, "bv_not_next_push_e3_goto_e0" }, 505 { e1, TK_BV_AND, "bv_and_next_push_e3_goto_e0" }, 506 { e1, TK_BV_OR, "bv_or_next_push_e3_goto_e0" }, 507 { e1, TK_BV_XOR, "bv_xor_next_push_e3_goto_e0" }, 508 { e1, TK_BV_NAND, "bv_nand_next_push_e3_goto_e0" }, 509 { e1, TK_BV_NOR, "bv_nor_next_push_e3_goto_e0" }, 510 { e1, TK_BV_XNOR, "bv_xnor_next_push_e3_goto_e0" }, 511 { e1, TK_BV_SHIFT_LEFT0, "bv_shift_left0_next_push_e3_goto_e0" }, 512 { e1, TK_BV_SHIFT_LEFT1, "bv_shift_left1_next_push_e3_goto_e0" }, 513 { e1, TK_BV_SHIFT_RIGHT0, "bv_shift_right0_next_push_e3_goto_e0" }, 514 { e1, TK_BV_SHIFT_RIGHT1, "bv_shift_right1_next_push_e3_goto_e0" }, 515 { e1, TK_BV_ASHIFT_RIGHT, "bv_ashift_right_next_push_e3_goto_e0" }, 516 { e1, TK_BV_ROTATE_LEFT, "bv_rotate_left_next_push_e3_goto_e0" }, 517 { e1, TK_BV_ROTATE_RIGHT, "bv_rotate_right_next_push_e3_goto_e0" }, 518 { e1, TK_BV_EXTRACT, "bv_extract_next_push_e3_goto_e0" }, 519 { e1, TK_BV_CONCAT, "bv_concat_next_push_e3_goto_e0" }, 520 { e1, TK_BV_REPEAT, "bv_repeat_next_push_e3_goto_e0" }, 521 { e1, TK_BV_SIGN_EXTEND, "bv_sign_extend_next_push_e3_goto_e0" }, 522 { e1, TK_BV_ZERO_EXTEND, "bv_zero_extend_next_push_e3_goto_e0" }, 523 { e1, TK_BV_GE, "bv_ge_next_push_e3_goto_e0" }, 524 { e1, TK_BV_GT, "bv_gt_next_push_e3_goto_e0" }, 525 { e1, TK_BV_LE, "bv_le_next_push_e3_goto_e0" }, 526 { e1, TK_BV_LT, "bv_lt_next_push_e3_goto_e0" }, 527 { e1, TK_BV_SGE, "bv_sge_next_push_e3_goto_e0" }, 528 { e1, TK_BV_SGT, "bv_sgt_next_push_e3_goto_e0" }, 529 { e1, TK_BV_SLE, "bv_sle_next_push_e3_goto_e0" }, 530 { e1, TK_BV_SLT, "bv_slt_next_push_e3_goto_e0" }, 531 { e1, TK_BV_SHL, "bv_shl_next_push_e3_goto_e0" }, 532 { e1, TK_BV_LSHR, "bv_lshr_next_push_e3_goto_e0" }, 533 { e1, TK_BV_ASHR, "bv_ashr_next_push_e3_goto_e0" }, 534 { e1, TK_BV_DIV, "bv_div_next_push_e3_goto_e0" }, 535 { e1, TK_BV_REM, "bv_rem_next_push_e3_goto_e0" }, 536 { e1, TK_BV_SDIV, "bv_sdiv_next_push_e3_goto_e0" }, 537 { e1, TK_BV_SREM, "bv_srem_next_push_e3_goto_e0" }, 538 { e1, TK_BV_SMOD, "bv_smod_next_push_e3_goto_e0" }, 539 { e1, TK_BV_REDOR, "bv_redor_next_push_e3_goto_e0" }, 540 { e1, TK_BV_REDAND, "bv_redand_next_push_e3_goto_e0" }, 541 { e1, TK_BV_COMP, "bv_comp_next_push_e3_goto_e0" }, 542 { e1, TK_BOOL_TO_BV, "bool_to_bv_next_push_e3_goto_e0" }, 543 { e1, TK_BIT, "bit_next_push_e3_goto_e0" }, 544 { e1, TK_FLOOR, "floor_next_push_e3_goto_e0" }, 545 { e1, TK_CEIL, "ceil_next_push_e3_goto_e0" }, 546 { e1, TK_ABS, "abs_next_push_e3_goto_e0" }, 547 { e1, TK_IDIV, "idiv_next_push_e3_goto_e0" }, 548 { e1, TK_MOD, "mod_next_push_e3_goto_e0" }, 549 { e1, TK_DIVIDES, "divides_next_push_e3_goto_e0" }, 550 { e1, TK_IS_INT, "is_int_next_push_e3_goto_e0" }, 551 552 { e1, TK_UPDATE, "update_next_push_e5_goto_e0" }, 553 { e1, TK_FORALL, "forall_next_goto_e10" }, 554 { e1, TK_EXISTS, "exists_next_goto_e10" }, 555 { e1, TK_LAMBDA, "lambda_next_goto_e10" }, 556 { e1, TK_LET, "let_next_goto_e15" }, 557 { e1, DEFAULT_TOKEN, "push_e3_push_e0_goto_e0" }, 558 559 { e3, TK_RP, "ret" }, 560 { e3, DEFAULT_TOKEN, "push_e3_goto_e0" }, 561 562 { e5, TK_LP, "next_push_e7_goto_e0" }, 563 { e5, DEFAULT_TOKEN, "error_lpar_expected" }, 564 565 { e7, TK_RP, "next_push_r0_goto_e0" }, 566 { e7, DEFAULT_TOKEN, "push_e7_goto_e0" }, 567 568 { e10, TK_LP, "next_goto_e11" }, 569 { e10, DEFAULT_TOKEN, "error_lpar_expected" }, 570 571 { e11, TK_SYMBOL, "e11_varname_next_goto_e12" }, 572 { e11, DEFAULT_TOKEN, "error_symbol_expected" }, 573 574 { e12, TK_COLON_COLON, "next_push_e14_goto_t0" }, 575 { e12, DEFAULT_TOKEN, "error_colon_colon_expected" }, 576 577 { e14, TK_RP, "e14_next_push_r0_goto_e0" }, 578 { e14, TK_SYMBOL, "e14_varname_next_goto_e12" }, 579 580 { e15, TK_LP, "next_goto_e16" }, 581 { e15, DEFAULT_TOKEN, "error_lpar_expected" }, 582 583 { e16, TK_LP, "next_goto_e17" }, 584 { e16, DEFAULT_TOKEN, "error_lpar_expected" }, 585 586 { e17, TK_SYMBOL, "termname_next_push_e19_goto_e0" }, 587 { e17, DEFAULT_TOKEN, "error_symbol_expected" }, 588 589 { e19, TK_RP, "next_goto_e20" }, 590 { e19, DEFAULT_TOKEN, "error_rpar_expected" }, 591 592 { e20, TK_LP, "next_goto_e17" }, 593 { e20, TK_RP, "next_push_r0_goto_e0" }, 594 595 { r0, TK_RP, "ret" }, 596 { r0, DEFAULT_TOKEN, "error_rpar_expected" }, 597 598 { -1, -1, NULL }, 599 }; 600 601 #define NSTATES (e20+1) 602 #define NTOKENS (TK_ERROR+1) 603 #define DEFAULT_VALUE "error" 604