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 * Parser for the SMT-LIB 2.0 language
21 */
22
23 #include <setjmp.h>
24 #include <inttypes.h>
25
26 #include "frontend/smt2/smt2_commands.h"
27 #include "frontend/smt2/smt2_lexer.h"
28 #include "frontend/smt2/smt2_parse_tables.h"
29 #include "frontend/smt2/smt2_parser.h"
30 #include "frontend/smt2/smt2_term_stack.h"
31
32 /*
33 * Short cuts to save typing
34 */
tkval(lexer_t * lex)35 static inline char *tkval(lexer_t *lex) {
36 return current_token_value(lex);
37 }
38
tklen(lexer_t * lex)39 static inline uint32_t tklen(lexer_t *lex) {
40 return current_token_length(lex);
41 }
42
43
44 /*
45 * Marker for the bottom of the state stack
46 */
47 enum {
48 done = NSTATES,
49 };
50
51
52 /*
53 * Read action from the tables in smt2_parse_tables.h
54 */
get_action(state_t s,smt2_token_t tk)55 static smt2_action_t get_action(state_t s, smt2_token_t tk) {
56 int32_t i;
57
58 i = base[s] + tk;
59 if (check[i] == s) {
60 return value[i];
61 } else {
62 return default_value[s];
63 }
64 }
65
66
67 /*
68 * Special case: check whether the token is equal to "not"
69 * The lexer returns a code of SMT2_TK_SYMBOL in this case.
70 * - tk = character string
71 * - len = number of characters in the token
72 */
token_is_not(const char * tk,uint32_t len)73 static bool token_is_not(const char *tk, uint32_t len) {
74 return smt2_string_to_symbol(tk, len) == SMT2_SYM_NOT;
75 }
76
77
78 /*
79 * Main parsing procedure
80 * - start = initial state
81 * return -1 on error, 0 otherwise
82 */
smt2_parse(parser_t * parser,state_t start)83 static int32_t smt2_parse(parser_t *parser, state_t start) {
84 smt2_token_t token;
85 smt2_keyword_t kw;
86 parser_state_t state;
87 parser_stack_t *stack;
88 lexer_t *lex;
89 tstack_t *tstack;
90 int exception;
91 loc_t loc;
92 loc_t saved_loc; // used to store location of (as ...
93 bool keep_tokens;
94 etk_queue_t *token_queue;
95
96 stack = &parser->pstack;
97 lex = parser->lex;
98 tstack = parser->tstack;
99
100 assert(parser_stack_is_empty(stack));
101 assert(tstack_is_empty(tstack));
102
103
104 /*
105 * keep_tokens: when true, all tokens received from the lexer are
106 * pushed into the SMT2 global token queue. This enables SMT2
107 * commands to print SMT2 expressions as they appear in the input.
108 */
109 keep_tokens = false;
110 token_queue = NULL;
111
112 // To catch exceptions in term-stack operations
113 exception = setjmp(tstack->env);
114 if (exception == 0) {
115 parser_push_state(stack, done);
116 state = start;
117
118 loop:
119 // jump here for actions that consume the current token
120 token = next_smt2_token(lex);
121 loc.line = current_token_line(lex);
122 loc.column = current_token_column(lex);
123 if (keep_tokens) {
124 assert(token_queue != NULL);
125 push_smt2_token(token_queue, token, tkval(lex), tklen(lex));
126 }
127
128 skip_token:
129 // jump here for actions that don't consume the token
130 switch (get_action(state, token)) {
131 case next_goto_c1:
132 state = c1;
133 goto loop;
134
135 case empty_command_return:
136 tstack_push_op(tstack, SMT2_SILENT_EXIT, &loc);
137 tstack_eval(tstack);
138 state = parser_pop_state(stack);
139 assert(state == done);
140 goto the_end;
141
142 case check_sat_next_goto_r0:
143 tstack_push_op(tstack, SMT2_CHECK_SAT, &loc);
144 state = r0;
145 goto loop;
146
147 case check_sat_assuming_next_goto_c16:
148 tstack_push_op(tstack, SMT2_CHECK_SAT_ASSUMING, &loc);
149 state = c16;
150 goto loop;
151
152 case get_assertions_next_goto_r0:
153 tstack_push_op(tstack, SMT2_GET_ASSERTIONS, &loc);
154 state = r0;
155 goto loop;
156
157 case get_proof_next_goto_r0:
158 tstack_push_op(tstack, SMT2_GET_PROOF, &loc);
159 state = r0;
160 goto loop;
161
162 case get_unsat_assumptions_next_goto_r0:
163 tstack_push_op(tstack, SMT2_GET_UNSAT_ASSUMPTIONS, &loc);
164 state = r0;
165 goto loop;
166
167 case get_unsat_core_next_goto_r0:
168 tstack_push_op(tstack, SMT2_GET_UNSAT_CORE, &loc);
169 state = r0;
170 goto loop;
171
172 case get_assignment_next_goto_r0:
173 tstack_push_op(tstack, SMT2_GET_ASSIGNMENT, &loc);
174 state = r0;
175 goto loop;
176
177 case exit_next_goto_r0:
178 tstack_push_op(tstack, SMT2_EXIT, &loc);
179 state = r0;
180 goto loop;
181
182 case push_next_goto_c3:
183 tstack_push_op(tstack, SMT2_PUSH, &loc);
184 state = c3;
185 goto loop;
186
187 case pop_next_goto_c3:
188 tstack_push_op(tstack, SMT2_POP, &loc);
189 state = c3;
190 goto loop;
191
192 case get_option_next_goto_c4:
193 tstack_push_op(tstack, SMT2_GET_OPTION, &loc);
194 state = c4;
195 goto loop;
196
197 case get_info_next_goto_c4:
198 tstack_push_op(tstack, SMT2_GET_INFO, &loc);
199 state = c4;
200 goto loop;
201
202 case set_logic_next_goto_c5:
203 tstack_push_op(tstack, SMT2_SET_LOGIC, &loc);
204 state = c5;
205 goto loop;
206
207 case set_option_next_goto_c6:
208 tstack_push_op(tstack, SMT2_SET_OPTION, &loc);
209 state = c6;
210 goto loop;
211
212 case set_info_next_goto_c6:
213 tstack_push_op(tstack, SMT2_SET_INFO, &loc);
214 state = c6;
215 goto loop;
216
217 case assert_next_push_r0_goto_t0:
218 tstack_push_op(tstack, SMT2_ASSERT, &loc);
219 parser_push_state(stack, r0);
220 state = t0;
221 goto loop;
222
223 case declare_sort_next_goto_c8:
224 tstack_push_op(tstack, SMT2_DECLARE_SORT, &loc);
225 state = c8;
226 goto loop;
227
228 case define_sort_next_goto_c9:
229 tstack_push_op(tstack, SMT2_DEFINE_SORT, &loc);
230 state = c9;
231 goto loop;
232
233 case declare_const_next_goto_c14:
234 tstack_push_op(tstack, SMT2_DECLARE_FUN, &loc);
235 state = c14;
236 goto loop;
237
238 case declare_fun_next_goto_c10:
239 tstack_push_op(tstack, SMT2_DECLARE_FUN, &loc);
240 state = c10;
241 goto loop;
242
243 case define_const_next_goto_c15:
244 tstack_push_op(tstack, SMT2_DEFINE_FUN, &loc);
245 state = c15;
246 goto loop;
247
248 case define_fun_next_goto_c11:
249 tstack_push_op(tstack, SMT2_DEFINE_FUN, &loc);
250 state = c11;
251 goto loop;
252
253 case get_value_next_goto_c12:
254 /*
255 * Activate the keep_tokens hack here
256 * We push the two tokens '(' 'get-value' into the token_queue
257 */
258 keep_tokens = true;
259 token_queue = smt2_token_queue();
260 push_smt2_token(token_queue, SMT2_TK_LP, NULL, 0);
261 push_smt2_token(token_queue, token, tkval(lex), tklen(lex));
262 // now proceed as normal: push the command
263 tstack_push_op(tstack, SMT2_GET_VALUE, &loc);
264 state = c12;
265 goto loop;
266
267 case get_model_next_goto_r0:
268 tstack_push_op(tstack, SMT2_GET_MODEL, &loc);
269 state = r0;
270 goto loop;
271
272 case echo_next_goto_c13:
273 tstack_push_op(tstack, SMT2_ECHO, &loc);
274 state = c13;
275 goto loop;
276
277 case reset_assertions_next_goto_r0:
278 tstack_push_op(tstack, SMT2_RESET_ASSERTIONS, &loc);
279 state = r0;
280 goto loop;
281
282 case reset_next_goto_r0:
283 tstack_push_op(tstack, SMT2_RESET_ALL, &loc);
284 state = r0;
285 goto loop;
286
287 case numeral_next_goto_r0:
288 tstack_push_rational(tstack, tkval(lex), &loc);
289 state = r0;
290 goto loop;
291
292 case keyword_next_goto_r0:
293 case symbol_next_goto_r0:
294 tstack_push_symbol(tstack, tkval(lex), tklen(lex), &loc);
295 state = r0;
296 goto loop;
297
298 case keyword_next_goto_c6a:
299 tstack_push_symbol(tstack, tkval(lex), tklen(lex), &loc);
300 state = c6a;
301 goto loop;
302
303 case next_return:
304 // eval current command
305 assert(! parser_stack_is_empty(stack));
306 tstack_eval(tstack);
307 state = parser_pop_state(stack);
308 if (state == done) {
309 goto the_end;
310 }
311 goto loop;
312
313 case push_r0_goto_a0:
314 parser_push_state(stack, r0);
315 state = a0;
316 goto skip_token;
317
318 case symbol_next_goto_c3:
319 // in (declare-sort <symbol> ..)
320 // tstack_push_free_type_or_macro_name(tstack, tkval(lex), tklen(lex), &loc);
321 tstack_push_free_sort_name(tstack, tkval(lex), tklen(lex), &loc);
322 state = c3;
323 goto loop;
324
325 case symbol_next_goto_c9a:
326 // in (define-sort <symbol> ...)
327 // tstack_push_free_type_or_macro_name(tstack, tkval(lex), tklen(lex), &loc);
328 tstack_push_free_sort_name(tstack, tkval(lex), tklen(lex), &loc);
329 state = c9a;
330 goto loop;
331
332 case next_goto_c9b:
333 state = c9b;
334 goto loop;
335
336 case next_push_r0_goto_s0:
337 parser_push_state(stack, r0);
338 state = s0;
339 goto loop;
340
341 case symbol_next_goto_c9b:
342 // in (define-sort .. (... <symbol> ...) ...)
343 // type variable
344 tstack_push_op(tstack, DECLARE_TYPE_VAR, &loc);
345 tstack_push_symbol(tstack, tkval(lex), tklen(lex), &loc);
346 tstack_eval(tstack); // eval DECLARE_TYPE_VAR
347 state = c9b;
348 goto loop;
349
350 case symbol_next_goto_c10a:
351 // in (declare-fun <symbol> ...)
352 // tstack_push_free_termname(tstack, tkval(lex), tklen(lex), &loc);
353 tstack_push_free_fun_name(tstack, tkval(lex), tklen(lex), &loc);
354 state = c10a;
355 goto loop;
356
357 case next_goto_c10b:
358 state = c10b;
359 goto loop;
360
361 case push_c10b_goto_s0:
362 parser_push_state(stack, c10b);
363 state = s0;
364 goto skip_token;
365
366 case symbol_next_goto_c11a:
367 // in (define-fun <symbol> ...)
368 // tstack_push_free_termname(tstack, tkval(lex), tklen(lex), &loc);
369 tstack_push_free_fun_name(tstack, tkval(lex), tklen(lex), &loc);
370 state = c11a;
371 goto loop;
372
373 case next_goto_c11b:
374 state = c11b;
375 goto loop;
376
377 case next_push_r0_push_t0_goto_s0:
378 parser_push_state(stack, r0);
379 parser_push_state(stack, t0);
380 state = s0;
381 goto loop;
382
383 case next_goto_c11d:
384 state = c11d;
385 goto loop;
386
387 case symbol_next_push_c11f_goto_s0:
388 // in (define-fun ... ( .. (<symbol> <sort> ) ... ) ...)
389 // variable of the given <sort>
390 tstack_push_op(tstack, DECLARE_VAR, &loc);
391 tstack_push_symbol(tstack, tkval(lex), tklen(lex), &loc);
392 parser_push_state(stack, c11f);
393 state = s0;
394 goto loop;
395
396 case eval_next_goto_c11b:
397 // evaluate the DECLARE_VAR
398 tstack_eval(tstack);
399 state = c11b;
400 goto loop;
401
402 case next_push_c12b_goto_t0:
403 parser_push_state(stack, c12b);
404 state = t0;
405 goto loop;
406
407 case next_goto_r0:
408 state = r0;
409 goto loop;
410
411 case push_c12b_goto_t0:
412 parser_push_state(stack, c12b);
413 state = t0;
414 goto skip_token;
415
416 case string_next_goto_r0:
417 // string argument to echo
418 tstack_push_string(tstack, tkval(lex), tklen(lex), &loc);
419 state = r0;
420 goto loop;
421
422 case symbol_next_push_r0_goto_s0:
423 // <symbol> in (declare-const <symbol> <sort> )
424 tstack_push_free_fun_name(tstack, tkval(lex), tklen(lex), &loc);
425 parser_push_state(stack, r0);
426 state = s0;
427 goto loop;
428
429 case symbol_next_push_r0_push_t0_goto_s0:
430 // <symbol> in (define-const <symbol> <sort> <term> )
431 tstack_push_free_fun_name(tstack, tkval(lex), tklen(lex), &loc);
432 parser_push_state(stack, r0);
433 parser_push_state(stack, t0);
434 state = s0;
435 goto loop;
436
437 case next_goto_c16a:
438 state = c16a;
439 goto loop;
440
441 case symbol_next_goto_c16a:
442 // <symbol> in a positive literal list in check-sat-assuming
443 tstack_push_symbol(tstack, tkval(lex), tklen(lex), &loc);
444 state = c16a;
445 goto loop;
446
447 case next_goto_c16b:
448 state = c16b;
449 goto loop;
450
451 case not_next_goto_c16c:
452 if (! token_is_not(tkval(lex), tklen(lex))) {
453 // syntax error.
454 smt2_syntax_error(lex, -3); // NOT expected
455 goto cleanup;
456 }
457 state = c16c;
458 goto loop;
459
460 case symbol_next_goto_c16d:
461 // <symbol> is a negated literal in check-sat-assuming
462 tstack_push_not_symbol(tstack, tkval(lex), tklen(lex), &loc);
463 state = c16d;
464 goto loop;
465
466 case numeral_next_return:
467 tstack_push_rational(tstack, tkval(lex), &loc);
468 state = parser_pop_state(stack);
469 if (state == done) {
470 goto the_end;
471 }
472 goto loop;
473
474 case decimal_next_return:
475 tstack_push_float(tstack, tkval(lex), &loc);
476 state = parser_pop_state(stack);
477 if (state == done) {
478 goto the_end;
479 }
480 goto loop;
481
482 case hexadecimal_next_return:
483 // skip the prefix '#x'
484 assert(tklen(lex) > 2);
485 tstack_push_bvhex(tstack, tkval(lex) + 2, tklen(lex) - 2, &loc);
486 state = parser_pop_state(stack);
487 if (state == done) {
488 goto the_end;
489 }
490 goto loop;
491
492 case binary_next_return:
493 // skip the prefix '#b'
494 assert(tklen(lex) > 2);
495 tstack_push_bvbin(tstack, tkval(lex) + 2, tklen(lex) - 2, &loc);
496 state = parser_pop_state(stack);
497 if (state == done) {
498 goto the_end;
499 }
500 goto loop;
501
502 case string_next_return:
503 tstack_push_string(tstack, tkval(lex), tklen(lex), &loc);
504 state = parser_pop_state(stack);
505 if (state == done) {
506 goto the_end;
507 }
508 goto loop;
509
510 case symbol_next_return:
511 // in attribute value
512 tstack_push_symbol(tstack, tkval(lex), tklen(lex), &loc);
513 state = parser_pop_state(stack);
514 if (state == done) {
515 goto the_end;
516 }
517 goto loop;
518
519 case next_goto_a1:
520 // start of s-expression as attribute value
521 tstack_push_op(tstack, SMT2_MAKE_ATTR_LIST, &loc);
522 state = a1;
523 goto loop;
524
525 case push_a1_goto_v0:
526 parser_push_state(stack, a1);
527 state = v0;
528 goto skip_token;
529
530 case keyword_next_return:
531 // in attribute value
532 tstack_push_symbol(tstack, tkval(lex), tklen(lex), &loc);
533 state = parser_pop_state(stack);
534 if (state == done) {
535 goto the_end;
536 }
537 goto loop;
538
539 case sort_symbol_next_return:
540 // sort name
541 tstack_push_sort_name(tstack, tkval(lex), tklen(lex), &loc);
542 state = parser_pop_state(stack);
543 if (state == done) {
544 goto the_end;
545 }
546 goto loop;
547
548 case next_goto_s1:
549 state = s1;
550 goto loop;
551
552 case next_goto_s2:
553 state = s2;
554 goto loop;
555
556 case next_goto_s5:
557 state = s5;
558 goto loop;
559
560 case symbol_next_push_s10_goto_s0:
561 // sort constructor in ( <symbol> <sort> ... <sort> )
562 tstack_push_sort_constructor(tstack, tkval(lex), tklen(lex), &loc);
563 parser_push_state(stack, s10);
564 state = s0;
565 goto loop;
566
567 case symbol_next_goto_s3:
568 // indexed sort in (_ <symbol> <idx> .. <idx> )
569 tstack_push_idx_sort(tstack, tkval(lex), tklen(lex), &loc);
570 state = s3;
571 goto loop;
572
573 case numeral_next_goto_s4:
574 // index in indexed sort
575 tstack_push_rational(tstack, tkval(lex), &loc);
576 state = s4;
577 goto loop;
578
579 case next_goto_s6:
580 state = s6;
581 goto loop;
582
583 case symbol_next_goto_s7:
584 // indexed sort constructor
585 // in ((_ <symbol> <idx> ... <idx>) <sort> ... <sort>)
586 tstack_push_idx_sort_constructor(tstack, tkval(lex), tklen(lex), &loc);
587 state = s7;
588 goto loop;
589
590 case numeral_next_goto_s8:
591 // <idx> in indexed sort constructor
592 tstack_push_rational(tstack, tkval(lex), &loc);
593 state = s8;
594 goto loop;
595
596 case next_push_s10_goto_s0:
597 parser_push_state(stack, s10);
598 state = s0;
599 goto loop;
600
601 case push_s10_goto_s0:
602 parser_push_state(stack, s10);
603 state = s0;
604 goto skip_token;
605
606 case term_symbol_next_return:
607 // term name
608 tstack_push_term_name(tstack, tkval(lex), tklen(lex), &loc);
609 state = parser_pop_state(stack);
610 if (state == done) {
611 goto the_end;
612 }
613 goto loop;
614
615 case next_goto_t1:
616 state = t1;
617 goto loop;
618
619 case next_goto_t2:
620 // (let
621 tstack_push_op(tstack, LET, &loc);
622 state = t2;
623 goto loop;
624
625 case forall_next_goto_t3:
626 // (forall
627 tstack_push_op(tstack, MK_FORALL, &loc);
628 state = t3;
629 goto loop;
630
631 case exists_next_goto_t3:
632 // (exists
633 tstack_push_op(tstack, MK_EXISTS, &loc);
634 state = t3;
635 goto loop;
636
637 case next_push_t4a_goto_t0:
638 // (!
639 tstack_push_op(tstack, SMT2_ADD_ATTRIBUTES, &loc);
640 parser_push_state(stack, t4a);
641 state = t0;
642 goto loop;
643
644 case next_goto_t5:
645 // (as
646 saved_loc = loc;
647 state = t5;
648 goto loop;
649
650 case next_goto_t6:
651 // ((
652 state = t6;
653 goto loop;
654
655 case next_goto_t7:
656 // (_
657 state = t7;
658 goto loop;
659
660 case symbol_next_push_t8a_goto_t0:
661 // function name in (<symbol> <term> .... <term>)
662 tstack_push_smt2_op(tstack, tkval(lex), tklen(lex), &loc);
663 parser_push_state(stack, t8a);
664 state = t0;
665 goto loop;
666
667 case next_goto_t2a:
668 state = t2a;
669 goto loop;
670
671 case next_goto_t2b:
672 state = t2b;
673 goto loop;
674
675 case symbol_next_push_t2d_goto_t0:
676 // in (let (.. (<symbol> <term>) ...) ...)
677 tstack_push_op(tstack, BIND, &loc);
678 tstack_push_symbol(tstack, tkval(lex), tklen(lex), &loc);
679 parser_push_state(stack, t2d);
680 state = t0;
681 goto loop;
682
683 case next_goto_t2e:
684 tstack_eval(tstack); // eval the BIND
685 state = t2e;
686 goto loop;
687
688 case next_push_r0_goto_t0:
689 parser_push_state(stack, r0);
690 state = t0;
691 goto loop;
692
693 case next_goto_t3a:
694 state = t3a;
695 goto loop;
696
697 case next_goto_t3b:
698 state = t3b;
699 goto loop;
700
701 case symbol_next_push_t3d_goto_s0:
702 // in (exists/forall (.. (<symbol <sort>) ...) ...)
703 tstack_push_op(tstack, DECLARE_VAR, &loc);
704 tstack_push_symbol(tstack, tkval(lex), tklen(lex), &loc);
705 parser_push_state(stack, t3d);
706 state = s0;
707 goto loop;
708
709 case next_goto_t3e:
710 tstack_eval(tstack); // eval DECLARE_VAR
711 state = t3e;
712 goto loop;
713
714 case check_keyword_then_branch:
715 // in (! <term> .. <keyword> <attribute-value> ...)
716 // We push the keyword in all cases as tstack's add_attributes requires a keyword.
717 // We ignore anything other than :named or :pattern
718 kw = smt2_string_to_keyword(tkval(lex), tklen(lex));
719 tstack_push_symbol(tstack, tkval(lex), tklen(lex), &loc);
720 if (kw == SMT2_KW_NAMED) {
721 state = t4d;
722 } else if (kw == SMT2_KW_PATTERN) {
723 state = t4e;
724 } else {
725 state = t4b;
726 }
727 goto loop;
728
729 case push_t4c_goto_a0:
730 parser_push_state(stack, t4c);
731 state = a0;
732 goto skip_token;
733
734 case symbol_next_goto_t4c:
735 // <symbol> as :named attribute
736 // in (! <term> ... :named <symbol> ...)
737 tstack_push_symbol(tstack, tkval(lex), tklen(lex), &loc);
738 state = t4c;
739 goto loop;
740
741 case next_push_t4g_goto_t0:
742 parser_push_state(stack, t4g);
743 state = t0;
744 goto loop;
745
746 case next_goto_t4c:
747 state = t4c;
748 goto loop;
749
750 case push_t4g_goto_t0:
751 parser_push_state(stack, t4g);
752 state = t0;
753 goto skip_token;
754
755 case next_goto_t5a:
756 state = t5a;
757 goto loop;
758
759 case asymbol_next_push_r0_goto_s0:
760 // in (as <symbol> <sort> )
761 tstack_push_op(tstack, SMT2_SORTED_TERM, &saved_loc);
762 tstack_push_qual_term_name(tstack, tkval(lex), tklen(lex), &loc);
763 parser_push_state(stack, r0);
764 state = s0;
765 goto loop;
766
767 case next_goto_t5b:
768 state = t5b;
769 goto loop;
770
771 case symbol_next_goto_t5c:
772 // in (as (_ <symbol> ...) <sort> )
773 tstack_push_op(tstack, SMT2_SORTED_INDEXED_TERM, &saved_loc);
774 tstack_push_qual_idx_term_name(tstack, tkval(lex), tklen(lex), &loc);
775 state = t5c;
776 goto loop;
777
778 case numeral_next_goto_t5d:
779 // push number
780 tstack_push_rational(tstack, tkval(lex), &loc);
781 state = t5d;
782 goto loop;
783
784 case next_goto_t6a:
785 // ((as
786 saved_loc = loc;
787 state = t6a;
788 goto loop;
789
790 case next_goto_t6h:
791 state = t6h;
792 goto loop;
793
794 case next_goto_t6b:
795 state = t6b;
796 goto loop;
797
798 case symbol_next_push_t6g_goto_s0:
799 // in ((as <symbol> <sort>) <arg> ... <arg>)
800 tstack_push_op(tstack, SMT2_SORTED_APPLY, &saved_loc);
801 tstack_push_qual_smt2_op(tstack, tkval(lex), tklen(lex), &loc);
802 parser_push_state(stack, t6g);
803 state = s0;
804 goto loop;
805
806 case next_goto_t6c:
807 state = t6c;
808 goto loop;
809
810 case symbol_next_goto_t6d:
811 // in ((as (_ <symbol> ...) <sort> ) <arg> ... <arg> )
812 tstack_push_op(tstack, SMT2_SORTED_INDEXED_APPLY, &saved_loc);
813 tstack_push_qual_smt2_idx_op(tstack, tkval(lex), tklen(lex), &loc);
814 state = t6d;
815 goto loop;
816
817 case numeral_next_goto_t6e:
818 tstack_push_rational(tstack, tkval(lex), &loc);
819 state = t6e;
820 goto loop;
821
822 case next_push_t6g_goto_s0:
823 parser_push_state(stack, t6g);
824 state = s0;
825 goto loop;
826
827 case next_push_t8a_goto_t0:
828 parser_push_state(stack, t8a);
829 state = t0;
830 goto loop;
831
832 case symbol_next_goto_t6i:
833 // in ((_ <symbol> ,,, ) <arg> ... <arg> )
834 tstack_push_smt2_idx_op(tstack, tkval(lex), tklen(lex), &loc);
835 state = t6i;
836 goto loop;
837
838 case numeral_next_goto_t6j:
839 tstack_push_rational(tstack, tkval(lex), &loc);
840 state = t6j;
841 goto loop;
842
843 case symbol_next_goto_t7a:
844 // in (_ <symbol> <idx> ... <idx> )
845 tstack_push_idx_term(tstack, tkval(lex), tklen(lex), &loc);
846 state = t7a;
847 goto loop;
848
849 case numeral_next_goto_t7b:
850 tstack_push_rational(tstack, tkval(lex), &loc);
851 state = t7b;
852 goto loop;
853
854 case push_t8a_goto_t0:
855 parser_push_state(stack, t8a);
856 state = t0;
857 goto skip_token;
858
859 case error_lp_expected:
860 smt2_syntax_error(lex, SMT2_TK_LP);
861 goto cleanup;
862
863 case error_string_expected:
864 smt2_syntax_error(lex, SMT2_TK_STRING);
865 goto cleanup;
866
867 case error_symbol_expected:
868 smt2_syntax_error(lex, SMT2_TK_SYMBOL);
869 goto cleanup;
870
871 case error_numeral_expected:
872 smt2_syntax_error(lex, SMT2_TK_NUMERAL);
873 goto cleanup;
874
875 case error_keyword_expected:
876 smt2_syntax_error(lex, SMT2_TK_KEYWORD);
877 goto cleanup;
878
879 case error_rp_expected:
880 smt2_syntax_error(lex, SMT2_TK_RP);
881 goto cleanup;
882
883 case error_underscore_expected:
884 smt2_syntax_error(lex, SMT2_TK_UNDERSCORE);
885 goto cleanup;
886
887 case error_command_expected:
888 smt2_syntax_error(lex, SMT2_COMMAND_EXPECTED);
889 goto cleanup;
890
891 case error_literal_expected:
892 smt2_syntax_error(lex, SMT2_LITERAL_EXPECTED);
893 goto cleanup;
894
895 case error_not_expected:
896 smt2_syntax_error(lex, SMT2_NOT_EXPECTED);
897 goto cleanup;
898
899 case error:
900 smt2_syntax_error(lex, -1);
901 goto cleanup;
902 }
903
904 } else {
905 // exception from term_stack
906 smt2_tstack_error(tstack, exception);
907 goto cleanup;
908 }
909
910 cleanup:
911 tstack_reset(tstack);
912 parser_stack_reset(stack);
913 if (keep_tokens) {
914 reset_etk_queue(token_queue);
915 }
916 return -1;
917
918 the_end:
919 if (keep_tokens) {
920 reset_etk_queue(token_queue);
921 }
922 return 0;
923 }
924
925
parse_smt2_command(parser_t * parser)926 int32_t parse_smt2_command(parser_t *parser) {
927 return smt2_parse(parser, c0);
928 }
929
930