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 /* 20 * Tables for parsing the SMT-LIB 2.0 language 21 */ 22 23 #ifndef __SMT2_PARSE_TABLES_H 24 #define __SMT2_PARSE_TABLES_H 25 26 #include <stdint.h> 27 28 /* 29 * States 30 */ 31 typedef enum state_s { 32 c0, c1, c3, c4, c5, c6, c6a, c8, c9, c9a, c9b, 33 c10, c10a, c10b, c11, c11a, c11b, c11d, c11f, c12, c12b, 34 c13, c14, c15, c16, c16a, c16b, c16c, c16d, 35 a0, a1, v0, 36 s0, s1, s2, s3, s4, s5, s6, s7, s8, s10, 37 t0, t1, t2, t2a, t2b, t2d, t2e, 38 t3, t3a, t3b, t3d, t3e, 39 t4a, t4b, t4c, t4d, t4e, t4g, 40 t5, t5a, t5b, t5c, t5d, 41 t6, t6a, t6b, t6c, t6d, t6e, t6g, t6h, t6i, t6j, 42 t7, t7a, t7b, t8a, 43 r0, 44 } state_t; 45 46 47 /* 48 * Action codes 49 */ 50 typedef enum actions { 51 // commands 52 next_goto_c1, 53 empty_command_return, 54 55 assert_next_push_r0_goto_t0, 56 check_sat_next_goto_r0, 57 check_sat_assuming_next_goto_c16, 58 declare_sort_next_goto_c8, 59 declare_const_next_goto_c14, 60 declare_fun_next_goto_c10, 61 define_sort_next_goto_c9, 62 define_const_next_goto_c15, 63 define_fun_next_goto_c11, 64 echo_next_goto_c13, 65 exit_next_goto_r0, 66 get_assertions_next_goto_r0, 67 get_assignment_next_goto_r0, 68 get_info_next_goto_c4, 69 get_model_next_goto_r0, 70 get_option_next_goto_c4, 71 get_proof_next_goto_r0, 72 get_unsat_assumptions_next_goto_r0, 73 get_unsat_core_next_goto_r0, 74 get_value_next_goto_c12, 75 pop_next_goto_c3, 76 push_next_goto_c3, 77 set_logic_next_goto_c5, 78 set_info_next_goto_c6, 79 set_option_next_goto_c6, 80 reset_next_goto_r0, 81 reset_assertions_next_goto_r0, 82 83 // arguments to the commands 84 numeral_next_goto_r0, 85 keyword_next_goto_r0, 86 symbol_next_goto_r0, 87 keyword_next_goto_c6a, 88 next_return, 89 push_r0_goto_a0, 90 symbol_next_goto_c3, 91 symbol_next_goto_c9a, 92 next_goto_c9b, 93 next_push_r0_goto_s0, 94 symbol_next_goto_c9b, 95 symbol_next_goto_c10a, 96 next_goto_c10b, 97 push_c10b_goto_s0, 98 symbol_next_goto_c11a, 99 next_goto_c11b, 100 next_push_r0_push_t0_goto_s0, 101 next_goto_c11d, 102 symbol_next_push_c11f_goto_s0, 103 eval_next_goto_c11b, 104 next_push_c12b_goto_t0, 105 next_goto_r0, 106 push_c12b_goto_t0, 107 string_next_goto_r0, 108 symbol_next_push_r0_goto_s0, 109 symbol_next_push_r0_push_t0_goto_s0, 110 next_goto_c16a, 111 symbol_next_goto_c16a, 112 next_goto_c16b, 113 not_next_goto_c16c, 114 symbol_next_goto_c16d, 115 116 // attribute values + s-expressions 117 numeral_next_return, 118 decimal_next_return, 119 hexadecimal_next_return, 120 binary_next_return, 121 string_next_return, 122 symbol_next_return, 123 next_goto_a1, 124 push_a1_goto_v0, 125 keyword_next_return, 126 127 // sorts 128 sort_symbol_next_return, 129 next_goto_s1, 130 next_goto_s2, 131 next_goto_s5, 132 symbol_next_push_s10_goto_s0, 133 symbol_next_goto_s3, 134 numeral_next_goto_s4, 135 next_goto_s6, 136 symbol_next_goto_s7, 137 numeral_next_goto_s8, 138 next_push_s10_goto_s0, 139 push_s10_goto_s0, 140 141 // terms 142 term_symbol_next_return, 143 next_goto_t1, 144 next_goto_t2, // (let 145 forall_next_goto_t3, // (forall 146 exists_next_goto_t3, // (exists 147 next_push_t4a_goto_t0, // (! 148 next_goto_t5, // (as 149 next_goto_t6, // (( 150 next_goto_t7, // (_ 151 152 // simple function application (<symbol> <term> ... <term>) 153 symbol_next_push_t8a_goto_t0, 154 155 // (let ... 156 next_goto_t2a, 157 next_goto_t2b, 158 symbol_next_push_t2d_goto_t0, 159 next_goto_t2e, 160 next_push_r0_goto_t0, 161 162 // (exists ... and (forall ... 163 next_goto_t3a, 164 next_goto_t3b, 165 symbol_next_push_t3d_goto_s0, 166 next_goto_t3e, 167 168 // (! <term> ... 169 check_keyword_then_branch, 170 push_t4c_goto_a0, 171 symbol_next_goto_t4c, 172 next_push_t4g_goto_t0, 173 next_goto_t4c, 174 push_t4g_goto_t0, 175 176 // (as ... 177 next_goto_t5a, 178 asymbol_next_push_r0_goto_s0, 179 next_goto_t5b, 180 symbol_next_goto_t5c, 181 numeral_next_goto_t5d, 182 183 // (( ... 184 next_goto_t6a, 185 next_goto_t6h, 186 187 // ((as ... 188 next_goto_t6b, 189 symbol_next_push_t6g_goto_s0, 190 next_goto_t6c, 191 symbol_next_goto_t6d, 192 numeral_next_goto_t6e, 193 next_push_t6g_goto_s0, 194 next_push_t8a_goto_t0, 195 196 // ((_ ... 197 symbol_next_goto_t6i, 198 numeral_next_goto_t6j, 199 200 // (_ ... 201 symbol_next_goto_t7a, 202 numeral_next_goto_t7b, 203 204 // after <term> in a function application 205 push_t8a_goto_t0, 206 207 // errors 208 error_lp_expected, 209 error_string_expected, 210 error_symbol_expected, 211 error_numeral_expected, 212 error_keyword_expected, 213 error_rp_expected, 214 error_underscore_expected, 215 error_command_expected, 216 error_literal_expected, 217 error_not_expected, 218 error, 219 } smt2_action_t; 220 221 /* 222 * Tables generated by table_builder 223 * see utils/table_builder.c 224 */ 225 226 // Table sizes 227 #define NSTATES 80 228 #define BSIZE 298 229 230 // Default values for each state 231 static const uint8_t default_value[NSTATES] = { 232 error_lp_expected, 233 error_command_expected, 234 error_numeral_expected, 235 error_keyword_expected, 236 error_symbol_expected, 237 error_keyword_expected, 238 push_r0_goto_a0, 239 error_symbol_expected, 240 error_symbol_expected, 241 error_lp_expected, 242 error, 243 error_symbol_expected, 244 error_lp_expected, 245 push_c10b_goto_s0, 246 error_symbol_expected, 247 error_lp_expected, 248 error, 249 error_symbol_expected, 250 error_rp_expected, 251 error_lp_expected, 252 push_c12b_goto_t0, 253 error, 254 error_symbol_expected, 255 error_symbol_expected, 256 error_lp_expected, 257 error_literal_expected, 258 error_not_expected, 259 error_symbol_expected, 260 error_rp_expected, 261 error, 262 push_a1_goto_v0, 263 error, 264 error, 265 error, 266 error_symbol_expected, 267 error_numeral_expected, 268 error, 269 error_underscore_expected, 270 error_symbol_expected, 271 error_numeral_expected, 272 error, 273 push_s10_goto_s0, 274 error, 275 error, 276 error_lp_expected, 277 error_lp_expected, 278 error_symbol_expected, 279 error_rp_expected, 280 error, 281 error_lp_expected, 282 error_lp_expected, 283 error_symbol_expected, 284 error_rp_expected, 285 error, 286 error_keyword_expected, 287 push_t4c_goto_a0, 288 error, 289 error_symbol_expected, 290 error_lp_expected, 291 push_t4g_goto_t0, 292 error, 293 error_underscore_expected, 294 error_symbol_expected, 295 error_numeral_expected, 296 error, 297 error, 298 error, 299 error_underscore_expected, 300 error_symbol_expected, 301 error_numeral_expected, 302 error, 303 error_rp_expected, 304 error_symbol_expected, 305 error_numeral_expected, 306 error, 307 error_symbol_expected, 308 error_numeral_expected, 309 error, 310 push_t8a_goto_t0, 311 error_rp_expected, 312 }; 313 314 // Base values for each state 315 static const uint8_t base[NSTATES] = { 316 0, 0, 0, 0, 40, 1, 0, 0, 42, 4, 317 52, 46, 5, 5, 48, 7, 12, 50, 13, 15, 318 15, 10, 10, 54, 20, 65, 44, 59, 63, 97, 319 68, 107, 120, 126, 114, 68, 88, 64, 116, 81, 320 92, 89, 170, 193, 99, 108, 122, 108, 118, 121, 321 133, 150, 135, 138, 130, 144, 180, 189, 147, 147, 322 195, 148, 212, 161, 164, 154, 218, 167, 224, 180, 323 183, 186, 236, 185, 188, 242, 189, 214, 193, 198, 324 }; 325 326 // Check table 327 static const uint8_t check[BSIZE] = { 328 0, 6, 0, 2, 9, 12, 13, 15, 7, 7, 329 3, 5, 16, 16, 18, 19, 20, 21, 22, 22, 330 24, 1, 1, 1, 1, 1, 1, 1, 1, 1, 331 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 332 1, 1, 1, 1, 1, 1, 1, 1, 4, 4, 333 8, 8, 26, 10, 11, 11, 14, 14, 17, 17, 334 10, 10, 23, 23, 28, 25, 25, 27, 27, 30, 335 4, 35, 8, 25, 25, 4, 11, 8, 14, 37, 336 17, 11, 10, 14, 39, 17, 4, 10, 8, 36, 337 41, 36, 11, 40, 14, 40, 17, 29, 10, 44, 338 29, 29, 29, 29, 29, 29, 29, 31, 45, 47, 339 31, 31, 31, 31, 31, 31, 31, 31, 48, 48, 340 32, 49, 34, 34, 38, 38, 33, 29, 32, 32, 341 46, 46, 29, 50, 33, 33, 52, 31, 53, 53, 342 54, 33, 31, 29, 34, 55, 38, 58, 59, 34, 343 32, 38, 46, 31, 55, 32, 33, 46, 51, 51, 344 34, 33, 38, 61, 63, 64, 32, 64, 46, 65, 345 42, 65, 33, 42, 42, 42, 42, 42, 42, 42, 346 51, 56, 67, 69, 70, 51, 70, 71, 73, 74, 347 56, 74, 76, 43, 78, 60, 51, 57, 57, 79, 348 42, 43, 43, 60, 60, 42, 80, 80, 43, 43, 349 43, 43, 43, 43, 80, 77, 42, 77, 66, 57, 350 62, 62, 80, 43, 57, 60, 66, 66, 43, 80, 351 60, 80, 68, 68, 80, 57, 80, 80, 80, 43, 352 80, 60, 62, 80, 72, 72, 80, 62, 66, 80, 353 75, 75, 80, 66, 68, 80, 80, 80, 62, 68, 354 80, 80, 80, 80, 66, 80, 72, 80, 80, 80, 355 68, 72, 75, 80, 80, 80, 80, 75, 80, 80, 356 80, 80, 72, 80, 80, 80, 80, 80, 75, 80, 357 80, 80, 80, 80, 80, 80, 80, 80, 358 }; 359 360 // Value table 361 static const uint8_t value[BSIZE] = { 362 next_goto_c1, 363 next_return, 364 empty_command_return, 365 numeral_next_goto_r0, 366 next_goto_c9b, 367 next_goto_c10b, 368 next_push_r0_goto_s0, 369 next_goto_c11b, 370 symbol_next_goto_c3, 371 symbol_next_goto_c3, 372 keyword_next_goto_r0, 373 keyword_next_goto_c6a, 374 next_goto_c11d, 375 next_push_r0_push_t0_goto_s0, 376 eval_next_goto_c11b, 377 next_push_c12b_goto_t0, 378 next_goto_r0, 379 string_next_goto_r0, 380 symbol_next_push_r0_goto_s0, 381 symbol_next_push_r0_goto_s0, 382 next_goto_c16a, 383 assert_next_push_r0_goto_t0, 384 check_sat_next_goto_r0, 385 check_sat_assuming_next_goto_c16, 386 declare_sort_next_goto_c8, 387 declare_const_next_goto_c14, 388 declare_fun_next_goto_c10, 389 define_sort_next_goto_c9, 390 define_const_next_goto_c15, 391 define_fun_next_goto_c11, 392 echo_next_goto_c13, 393 exit_next_goto_r0, 394 get_assertions_next_goto_r0, 395 get_assignment_next_goto_r0, 396 get_info_next_goto_c4, 397 get_model_next_goto_r0, 398 get_option_next_goto_c4, 399 get_proof_next_goto_r0, 400 get_unsat_assumptions_next_goto_r0, 401 get_unsat_core_next_goto_r0, 402 get_value_next_goto_c12, 403 pop_next_goto_c3, 404 push_next_goto_c3, 405 set_logic_next_goto_c5, 406 set_info_next_goto_c6, 407 set_option_next_goto_c6, 408 reset_next_goto_r0, 409 reset_assertions_next_goto_r0, 410 symbol_next_goto_r0, 411 symbol_next_goto_r0, 412 symbol_next_goto_c9a, 413 symbol_next_goto_c9a, 414 not_next_goto_c16c, 415 next_push_r0_goto_s0, 416 symbol_next_goto_c10a, 417 symbol_next_goto_c10a, 418 symbol_next_goto_c11a, 419 symbol_next_goto_c11a, 420 symbol_next_push_c11f_goto_s0, 421 symbol_next_push_c11f_goto_s0, 422 symbol_next_goto_c9b, 423 symbol_next_goto_c9b, 424 symbol_next_push_r0_push_t0_goto_s0, 425 symbol_next_push_r0_push_t0_goto_s0, 426 next_goto_c16a, 427 next_goto_c16b, 428 next_goto_r0, 429 symbol_next_goto_c16d, 430 symbol_next_goto_c16d, 431 next_return, 432 symbol_next_goto_r0, 433 numeral_next_goto_s4, 434 symbol_next_goto_c9a, 435 symbol_next_goto_c16a, 436 symbol_next_goto_c16a, 437 symbol_next_goto_r0, 438 symbol_next_goto_c10a, 439 symbol_next_goto_c9a, 440 symbol_next_goto_c11a, 441 next_goto_s6, 442 symbol_next_push_c11f_goto_s0, 443 symbol_next_goto_c10a, 444 symbol_next_goto_c9b, 445 symbol_next_goto_c11a, 446 numeral_next_goto_s8, 447 symbol_next_push_c11f_goto_s0, 448 symbol_next_goto_r0, 449 symbol_next_goto_c9b, 450 symbol_next_goto_c9a, 451 next_return, 452 next_return, 453 numeral_next_goto_s4, 454 symbol_next_goto_c10a, 455 next_push_s10_goto_s0, 456 symbol_next_goto_c11a, 457 numeral_next_goto_s8, 458 symbol_next_push_c11f_goto_s0, 459 next_goto_a1, 460 symbol_next_goto_c9b, 461 next_goto_t2a, 462 numeral_next_return, 463 decimal_next_return, 464 hexadecimal_next_return, 465 binary_next_return, 466 string_next_return, 467 symbol_next_return, 468 symbol_next_return, 469 next_goto_a1, 470 next_goto_t2b, 471 next_goto_t2e, 472 numeral_next_return, 473 decimal_next_return, 474 hexadecimal_next_return, 475 binary_next_return, 476 string_next_return, 477 symbol_next_return, 478 symbol_next_return, 479 keyword_next_return, 480 next_goto_t2b, 481 next_push_r0_goto_t0, 482 next_goto_s1, 483 next_goto_t3a, 484 symbol_next_goto_s3, 485 symbol_next_goto_s3, 486 symbol_next_goto_s7, 487 symbol_next_goto_s7, 488 next_goto_s5, 489 symbol_next_return, 490 sort_symbol_next_return, 491 sort_symbol_next_return, 492 symbol_next_push_t2d_goto_t0, 493 symbol_next_push_t2d_goto_t0, 494 symbol_next_return, 495 next_goto_t3b, 496 symbol_next_push_s10_goto_s0, 497 symbol_next_push_s10_goto_s0, 498 next_goto_t3e, 499 symbol_next_return, 500 next_goto_t3b, 501 next_push_r0_goto_t0, 502 check_keyword_then_branch, 503 next_goto_s2, 504 symbol_next_return, 505 symbol_next_return, 506 symbol_next_goto_s3, 507 next_return, 508 symbol_next_goto_s7, 509 next_push_t4g_goto_t0, 510 next_goto_t4c, 511 symbol_next_goto_s3, 512 sort_symbol_next_return, 513 symbol_next_goto_s7, 514 symbol_next_push_t2d_goto_t0, 515 symbol_next_return, 516 check_keyword_then_branch, 517 sort_symbol_next_return, 518 symbol_next_push_s10_goto_s0, 519 symbol_next_push_t2d_goto_t0, 520 symbol_next_push_t3d_goto_s0, 521 symbol_next_push_t3d_goto_s0, 522 symbol_next_goto_s3, 523 symbol_next_push_s10_goto_s0, 524 symbol_next_goto_s7, 525 next_goto_t5b, 526 numeral_next_goto_t5d, 527 next_push_r0_goto_s0, 528 sort_symbol_next_return, 529 numeral_next_goto_t5d, 530 symbol_next_push_t2d_goto_t0, 531 next_goto_t6h, 532 next_goto_t1, 533 next_goto_t6a, 534 symbol_next_push_s10_goto_s0, 535 numeral_next_return, 536 decimal_next_return, 537 hexadecimal_next_return, 538 binary_next_return, 539 string_next_return, 540 term_symbol_next_return, 541 term_symbol_next_return, 542 symbol_next_push_t3d_goto_s0, 543 next_return, 544 next_goto_t6c, 545 numeral_next_goto_t6e, 546 next_push_t6g_goto_s0, 547 symbol_next_push_t3d_goto_s0, 548 numeral_next_goto_t6e, 549 next_push_t8a_goto_t0, 550 numeral_next_goto_t6j, 551 next_push_t8a_goto_t0, 552 check_keyword_then_branch, 553 numeral_next_goto_t6j, 554 numeral_next_goto_t7b, 555 next_goto_t6, 556 next_return, 557 next_goto_t5a, 558 symbol_next_push_t3d_goto_s0, 559 symbol_next_goto_t4c, 560 symbol_next_goto_t4c, 561 next_return, 562 term_symbol_next_return, 563 symbol_next_push_t8a_goto_t0, 564 symbol_next_push_t8a_goto_t0, 565 asymbol_next_push_r0_goto_s0, 566 asymbol_next_push_r0_goto_s0, 567 term_symbol_next_return, 568 error, 569 error, 570 next_goto_t7, 571 next_push_t4a_goto_t0, 572 next_goto_t5, 573 next_goto_t2, 574 exists_next_goto_t3, 575 forall_next_goto_t3, 576 error, 577 next_return, 578 term_symbol_next_return, 579 numeral_next_goto_t7b, 580 next_goto_t6b, 581 symbol_next_goto_t4c, 582 symbol_next_goto_t5c, 583 symbol_next_goto_t5c, 584 error, 585 symbol_next_push_t8a_goto_t0, 586 symbol_next_goto_t4c, 587 asymbol_next_push_r0_goto_s0, 588 symbol_next_push_t6g_goto_s0, 589 symbol_next_push_t6g_goto_s0, 590 symbol_next_push_t8a_goto_t0, 591 error, 592 asymbol_next_push_r0_goto_s0, 593 error, 594 symbol_next_goto_t6d, 595 symbol_next_goto_t6d, 596 error, 597 symbol_next_goto_t4c, 598 error, 599 error, 600 error, 601 symbol_next_push_t8a_goto_t0, 602 error, 603 asymbol_next_push_r0_goto_s0, 604 symbol_next_goto_t5c, 605 error, 606 symbol_next_goto_t6i, 607 symbol_next_goto_t6i, 608 error, 609 symbol_next_goto_t5c, 610 symbol_next_push_t6g_goto_s0, 611 error, 612 symbol_next_goto_t7a, 613 symbol_next_goto_t7a, 614 error, 615 symbol_next_push_t6g_goto_s0, 616 symbol_next_goto_t6d, 617 error, 618 error, 619 error, 620 symbol_next_goto_t5c, 621 symbol_next_goto_t6d, 622 error, 623 error, 624 error, 625 error, 626 symbol_next_push_t6g_goto_s0, 627 error, 628 symbol_next_goto_t6i, 629 error, 630 error, 631 error, 632 symbol_next_goto_t6d, 633 symbol_next_goto_t6i, 634 symbol_next_goto_t7a, 635 error, 636 error, 637 error, 638 error, 639 symbol_next_goto_t7a, 640 error, 641 error, 642 error, 643 error, 644 symbol_next_goto_t6i, 645 error, 646 error, 647 error, 648 error, 649 error, 650 symbol_next_goto_t7a, 651 error, 652 error, 653 error, 654 error, 655 error, 656 error, 657 error, 658 error, 659 error, 660 }; 661 662 663 664 #endif /* __SMT2_PARSE_TABLES_H */ 665