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 Yices language.
21 */
22
23 #include <stdio.h>
24 #include <setjmp.h>
25 #include <inttypes.h>
26
27 #include "api/yices_globals.h"
28 #include "frontend/yices/yices_lexer.h"
29 #include "frontend/yices/yices_parse_tables.h"
30 #include "frontend/yices/yices_parser.h"
31 #include "frontend/yices/yices_tstack_ops.h"
32 #include "parser_utils/term_stack_error.h"
33
34 //IAM: FIXME:
35 extern error_report_t *yices_error_report(void);
36
37 /*
38 * Short cuts to save typing
39 */
tkval(lexer_t * lex)40 static inline char *tkval(lexer_t *lex) {
41 return current_token_value(lex);
42 }
43
tklen(lexer_t * lex)44 static inline uint32_t tklen(lexer_t *lex) {
45 return current_token_length(lex);
46 }
47
48
49 /*
50 * Name of the current input file (NULL if stdin)
51 */
reader_name(lexer_t * lex)52 static inline const char *reader_name(lexer_t *lex) {
53 return lex->reader.name;
54 }
55
56
57 /*
58 * Store error code and location data for a syntax error
59 * - lex = lexer
60 * - expected_token = what was expected
61 */
export_syntax_error(lexer_t * lex,int32_t expected_token)62 static void export_syntax_error(lexer_t *lex, int32_t expected_token) {
63 error_report_t *error;
64 reader_t *rd;
65 yices_token_t tk;
66
67 error = yices_error_report(); //IAM: __yices_globals.error;
68 rd = &lex->reader;
69 tk = current_token(lex);
70 switch (tk) {
71 case TK_OPEN_STRING:
72 error->code = INVALID_TOKEN;
73 error->line = rd->line;
74 error->column = rd->column;
75 break;
76
77 case TK_EMPTY_BVCONST:
78 error->code = INVALID_BVBIN_FORMAT;
79 error->line = lex->tk_line;
80 error->column = lex->tk_column;
81 break;
82
83 case TK_EMPTY_HEXCONST:
84 error->code = INVALID_BVHEX_FORMAT;
85 error->line = lex->tk_line;
86 error->column = lex->tk_column;
87 break;
88
89 case TK_INVALID_NUM:
90 error->code = INVALID_TOKEN; // invalid rational or float
91 error->line = lex->tk_line;
92 error->column = lex->tk_column;
93 break;
94
95 case TK_ZERO_DIVISOR:
96 error->code = DIVISION_BY_ZERO;
97 error->line = lex->tk_line;
98 error->column = lex->tk_column;
99 break;
100
101 case TK_ERROR:
102 error->code = INVALID_TOKEN;
103 error->line = lex->tk_line;
104 error->column = lex->tk_column;
105 break;
106
107 default:
108 error->code = SYNTAX_ERROR;
109 error->line = lex->tk_line;
110 error->column = lex->tk_column;
111 break;
112 }
113 }
114
115
116 /*
117 * Table for conversion of tstack error codes to yices error codes
118 * (NO_ERROR means a bug)
119 */
120 static error_code_t const tstack_error2yices_error[NUM_TSTACK_ERRORS] = {
121 NO_ERROR, // TSTACK_NO_ERROR
122 NO_ERROR, // TSTACK_INTERNAL_ERROR
123 NO_ERROR, // TSTACK_OP_NOT_IMPLEMENTED
124 UNDEFINED_TERM_NAME, // TSTACK_UNDEF_TERM
125 UNDEFINED_TYPE_NAME, // TSTACK_UNDEF_TYPE
126 INVALID_RATIONAL_FORMAT, // TSTACK_RATIONAL_FORMAT
127 INVALID_FLOAT_FORMAT, // TSTACK_FLOAT_FORMAT
128 INVALID_BVBIN_FORMAT, // TSTACK_BVBIN_FORMAT
129 INVALID_BVHEX_FORMAT, // TSTACK_BVHEX_FORMAT
130 REDEFINED_TYPE_NAME, // TSTACK_TYPENAME_REDEF
131 REDEFINED_TERM_NAME, // TSTACK_TERMNAME_REDEF
132 DUPLICATE_NAME_IN_SCALAR, // TSTACK_DUPLICATE_SCALAR_NAME
133 DUPLICATE_VAR_NAME, // TSTACK_DUPLICATE_VAR_NAME
134 NO_ERROR, // TSTACK_INVALID_OP
135 WRONG_NUMBER_OF_ARGUMENTS, // TSTACK_INVALID_FRAME
136 INTEGER_OVERFLOW, // TSTACK_INTEGER_OVERFLOW
137 NONNEG_INT_REQUIRED, // TSTACK_NEGATIVE_EXPONENT
138 INTEGER_REQUIRED, // TSTACK_NOT_AN_INTEGER
139 SYMBOL_REQUIRED, // TSTACK_NOT_A_SYMBOL
140 RATIONAL_REQUIRED, // TSTACK_NOT_A_RATIONAL
141 TYPE_REQUIRED, // TSTACK_NOT_A_TYPE
142 ARITH_ERROR, // TSTACK_ARITH_ERROR
143 DIVISION_BY_ZERO, // TSTACK_DIVIDE_BY_ZERO
144 NON_CONSTANT_DIVISOR, // TSTACK_NON_CONSTANT_DIVISOR
145 NEGATIVE_BVSIZE, // TSTACK_NEGATIVE_BVSIZE
146 INCOMPATIBLE_BVSIZES, // TSTACK_INCOMPATIBLE_BVSIZES
147 INVALID_BVCONSTANT, // TSTACK_INVALID_BVCONSTANT
148 BVARITH_ERROR, // TSTACK_BVARITH_ERROR
149 BVARITH_ERROR, // TSTACK_BVLOGIC_ERROR
150 TYPE_MISMATCH_IN_DEF, // TSTACK_TYPE_ERROR_IN_DEFTERM
151 NO_ERROR, // TSTACK_STRINGS_ARE_NOT_TERMS
152 NO_ERROR, // TSTACK_YICES_ERROR
153 };
154
155
156 /*
157 * Store code and location data for an exception raised by tstack
158 */
export_tstack_error(tstack_t * tstack,tstack_error_t exception)159 static void export_tstack_error(tstack_t *tstack, tstack_error_t exception) {
160 error_report_t *error;
161
162 error = yices_error_report(); //IAM: __yices_globals.error;
163 error->line = tstack->error_loc.line;
164 error->column = tstack->error_loc.column;
165 if (exception != TSTACK_YICES_ERROR) {
166 error->code = tstack_error2yices_error[exception];
167 if (error->code == NO_ERROR) {
168 report_bug("Internal error");
169 }
170 }
171 }
172
173
174 /*
175 * Syntax error:
176 * - lex = the lexer
177 * - err = error file or NULL
178 * - expected_token = what was expected or -1
179 */
syntax_error(lexer_t * lex,FILE * err,int32_t expected_token)180 static void syntax_error(lexer_t *lex, FILE *err, int32_t expected_token) {
181 yices_token_t tk;
182 reader_t *rd;
183
184 if (err == NULL) {
185 export_syntax_error(lex, expected_token);
186 return;
187 }
188
189 tk = current_token(lex);
190 rd = &lex->reader;
191
192 if (rd->name != NULL) {
193 fprintf(err, "%s: ", rd->name);
194 }
195
196 switch (tk) {
197 case TK_OPEN_STRING:
198 fprintf(err, "missing string terminator \" (line %"PRId32", column %"PRId32")\n",
199 rd->line, rd->column);
200 break;
201
202 case TK_EMPTY_BVCONST:
203 fprintf(err, "invalid binary constant %s (line %"PRId32", column %"PRId32")\n",
204 tkval(lex), lex->tk_line, lex->tk_column);
205 break;
206
207 case TK_EMPTY_HEXCONST:
208 fprintf(err, "invalid hexadecimal constant %s (line %"PRId32", column %"PRId32")\n",
209 tkval(lex), lex->tk_line, lex->tk_column);
210 break;
211
212 case TK_INVALID_NUM:
213 fprintf(err, "invalid number %s (line %"PRId32", column %"PRId32")\n",
214 tkval(lex), lex->tk_line, lex->tk_column);
215 break;
216
217 case TK_ZERO_DIVISOR:
218 fprintf(err, "zero divisor in constant %s (line %"PRId32", column %"PRId32")\n",
219 tkval(lex), lex->tk_line, lex->tk_column);
220 break;
221
222 case TK_ERROR:
223 fprintf(err, "invalid token %s (line %"PRId32", column %"PRId32")\n",
224 tkval(lex), lex->tk_line, lex->tk_column);
225 break;
226
227 default:
228 // try to avoid confusion: don't want to print 'error not expected'
229 if (expected_token == TK_NOT) {
230 fprintf(err, "syntax error (line %"PRId32", column %"PRId32"): expected 'not'\n",
231 lex->tk_line, lex->tk_column);
232 } else if (expected_token != -1) {
233 assert(0 <= expected_token && expected_token < NUM_YICES_TOKENS);
234 fprintf(err, "syntax error (line %"PRId32", column %"PRId32"): %s expected\n",
235 lex->tk_line, lex->tk_column, yices_token_to_string(expected_token));
236 } else {
237 fprintf(err, "syntax error (line %"PRId32", column %"PRId32")\n",
238 lex->tk_line, lex->tk_column);
239 }
240 break;
241 }
242 }
243
244 // when we get (<symbol> ... ) and <symbol> is not a known command
syntax_error_bad_command(lexer_t * lex,FILE * err)245 static void syntax_error_bad_command(lexer_t *lex, FILE *err) {
246 reader_t *rd;
247
248 if (err == NULL) {
249 export_syntax_error(lex, -1);
250 return;
251 }
252
253 rd = &lex->reader;
254 if (rd->name != NULL) {
255 fprintf(err, "%s: ", rd->name);
256 }
257 fprintf(err, "syntax error: (line %"PRId32", column %"PRId32"): %s is not a command\n",
258 lex->tk_line, lex->tk_column, tkval(lex));
259 }
260
261
262 /*
263 * Marker for bottom of the state stack.
264 */
265 enum {
266 done = NSTATES,
267 };
268
269
270 /*
271 * Read action from the tables in yices_parse_tables.h
272 */
get_action(state_t s,token_t tk)273 static action_t get_action(state_t s, token_t tk) {
274 int32_t i;
275
276 i = base[s] + tk;
277 if (check[i] == s) {
278 return value[i];
279 } else {
280 return default_value[s];
281 }
282 }
283
284
285 /*
286 * Main parsing procedure
287 * - start = initial state
288 * - err = error output file or NULL
289 * return -1 if there's an error, 0 otherwise
290 */
yices_parse(parser_t * parser,state_t start,FILE * err)291 static int32_t yices_parse(parser_t *parser, state_t start, FILE *err) {
292 token_t token;
293 parser_state_t state;
294 parser_stack_t *stack;
295 lexer_t *lex;
296 tstack_t *tstack;
297 int exception;
298 loc_t loc;
299
300 stack = &parser->pstack;
301 lex = parser->lex;
302 tstack = parser->tstack;
303
304 assert(parser_stack_is_empty(stack));
305 assert(tstack_is_empty(tstack) ||
306 tstack->top_op == BUILD_TYPE ||
307 tstack->top_op == BUILD_TERM);
308
309 // prepare to catch exceptions in term stack operations
310 exception = setjmp(tstack->env);
311 if (exception == 0) {
312
313 parser_push_state(stack, done);
314 state = start;
315
316 loop:
317 // jump here for actions that consume the current token
318 token = next_yices_token(lex);
319 loc.line = current_token_line(lex);
320 loc.column = current_token_column(lex);
321
322 // jump here for actions that don't consume the token
323 skip_token:
324 switch (get_action(state, token)) {
325 case next_goto_c1:
326 state = c1;
327 goto loop;
328
329 case empty_command:
330 tstack_push_op(tstack, EXIT_CMD, &loc);
331 tstack_eval(tstack);
332 state = parser_pop_state(stack);
333 assert (state == done);
334 goto the_end;
335
336 case exit_next_goto_r0:
337 tstack_push_op(tstack, EXIT_CMD, &loc);
338 state = r0;
339 goto loop;
340
341 case check_next_goto_r0:
342 tstack_push_op(tstack, CHECK_CMD, &loc);
343 state = r0;
344 goto loop;
345
346 case check_assuming_next_goto_c16:
347 tstack_push_op(tstack, CHECK_ASSUMING_CMD, &loc);
348 state = c16;
349 goto loop;
350
351 case push_next_goto_r0:
352 tstack_push_op(tstack, PUSH_CMD, &loc);
353 state = r0;
354 goto loop;
355
356 case pop_next_goto_r0:
357 tstack_push_op(tstack, POP_CMD, &loc);
358 state = r0;
359 goto loop;
360
361 case reset_next_goto_r0:
362 tstack_push_op(tstack, RESET_CMD, &loc);
363 state = r0;
364 goto loop;
365
366 case dump_context_next_goto_r0:
367 tstack_push_op(tstack, DUMP_CMD, &loc);
368 state = r0;
369 goto loop;
370
371 case echo_next_goto_c3:
372 tstack_push_op(tstack, ECHO_CMD, &loc);
373 state = c3;
374 goto loop;
375
376 case include_next_goto_c3:
377 tstack_push_op(tstack, INCLUDE_CMD, &loc);
378 state = c3;
379 goto loop;
380
381 case assert_next_push_c20_goto_e0:
382 tstack_push_op(tstack, ASSERT_CMD, &loc);
383 parser_push_state(stack, c20);
384 state = e0;
385 goto loop;
386
387 case deftype_next_goto_c2:
388 tstack_push_op(tstack, DEF_YICES_TYPE, &loc);
389 state = c2;
390 goto loop;
391
392 case defterm_next_goto_c6:
393 tstack_push_op(tstack, DEF_YICES_TERM, &loc);
394 state = c6;
395 goto loop;
396
397 case showmodel_next_goto_r0:
398 tstack_push_op(tstack, SHOWMODEL_CMD, &loc);
399 state = r0;
400 goto loop;
401
402 case eval_next_push_r0_goto_e0:
403 tstack_push_op(tstack, EVAL_CMD, &loc);
404 parser_push_state(stack, r0);
405 state = e0;
406 goto loop;
407
408 case setparam_next_goto_c11:
409 tstack_push_op(tstack, SET_PARAM_CMD, &loc);
410 state = c11;
411 goto loop;
412
413 case showparam_next_goto_c13:
414 tstack_push_op(tstack, SHOW_PARAM_CMD, &loc);
415 state = c13;
416 goto loop;
417
418 case showparams_next_goto_r0:
419 tstack_push_op(tstack, SHOW_PARAMS_CMD, &loc);
420 state = r0;
421 goto loop;
422
423 case showstats_next_goto_r0:
424 tstack_push_op(tstack, SHOW_STATS_CMD, &loc);
425 state = r0;
426 goto loop;
427
428 case resetstats_next_goto_r0:
429 tstack_push_op(tstack, RESET_STATS_CMD, &loc);
430 state = r0;
431 goto loop;
432
433 case showtimeout_next_goto_r0:
434 tstack_push_op(tstack, SHOW_TIMEOUT_CMD, &loc);
435 state = r0;
436 goto loop;
437
438 case settimeout_next_goto_c14:
439 tstack_push_op(tstack, SET_TIMEOUT_CMD, &loc);
440 state = c14;
441 goto loop;
442
443 case help_next_goto_c15:
444 tstack_push_op(tstack, HELP_CMD, &loc);
445 state = c15;
446 goto loop;
447
448 case efsolve_next_goto_r0:
449 tstack_push_op(tstack, EFSOLVE_CMD, &loc);
450 state = r0;
451 goto loop;
452
453 case export_next_goto_c3:
454 tstack_push_op(tstack, EXPORT_CMD, &loc);
455 state = c3;
456 goto loop;
457
458 case implicant_next_goto_r0:
459 tstack_push_op(tstack, SHOW_IMPLICANT_CMD, &loc);
460 state = r0;
461 goto loop;
462
463 case unsat_core_next_goto_r0:
464 tstack_push_op(tstack, SHOW_UNSAT_CORE_CMD, &loc);
465 state = r0;
466 goto loop;
467
468 case unsat_assumptions_next_goto_r0:
469 tstack_push_op(tstack, SHOW_UNSAT_ASSUMPTIONS_CMD, &loc);
470 state = r0;
471 goto loop;
472
473 case reduced_model_next_goto_r0:
474 tstack_push_op(tstack, SHOW_REDUCED_MODEL_CMD, &loc);
475 state = r0;
476 goto loop;
477
478 case typename_next_goto_c10:
479 // token must be a free typename (TK_SYMBOL)
480 tstack_push_free_typename(tstack, tkval(lex), tklen(lex), &loc);
481 state = c10;
482 goto loop;
483
484 case string_next_goto_r0:
485 tstack_push_string(tstack, tkval(lex), tklen(lex), &loc);
486 state = r0;
487 goto loop;
488
489 case termname_next_goto_c7:
490 // token must be a free termname (TK_SYMBOL)
491 tstack_push_free_termname(tstack, tkval(lex), tklen(lex), &loc);
492 state = c7;
493 goto loop;
494
495 case next_push_c9_goto_t0:
496 parser_push_state(stack, c9);
497 state = t0;
498 goto loop;
499
500 case symbol_next_goto_c12:
501 // symbol in (set-param <symbol> value)
502 tstack_push_symbol(tstack, tkval(lex), tklen(lex), &loc);
503 state = c12;
504 goto loop;
505
506 case true_next_goto_r0:
507 tstack_push_true(tstack, &loc);
508 state = r0;
509 goto loop;
510
511 case false_next_goto_r0:
512 tstack_push_false(tstack, &loc);
513 state = r0;
514 goto loop;
515
516 case float_next_goto_r0:
517 tstack_push_float(tstack, tkval(lex), &loc);
518 state = r0;
519 goto loop;
520
521 case symbol_next_goto_r0:
522 // symbol in (show-param <symbol>) or (help <symbol>)
523 // or (set-param ... <symbol>)
524 tstack_push_symbol(tstack, tkval(lex), tklen(lex), &loc);
525 state = r0;
526 goto loop;
527
528 case ret:
529 assert(! parser_stack_is_empty(stack));
530 // eval current operation
531 tstack_eval(tstack);
532 state = parser_pop_state(stack);
533 if (state == done) {
534 goto the_end;
535 }
536 goto loop;
537
538 case push_r0_goto_e0:
539 parser_push_state(stack, r0);
540 state = e0;
541 goto skip_token;
542
543 case push_r0_goto_td0:
544 parser_push_state(stack, r0);
545 state = td0;
546 goto skip_token;
547
548 case symbol_next_goto_c16:
549 // positive assumption in check-assuming
550 tstack_push_symbol(tstack, tkval(lex), tklen(lex), &loc);
551 state = c16;
552 goto loop;
553
554 case next_goto_c17:
555 state = c17;
556 goto loop;
557
558 case not_next_goto_c18:
559 state = c18;
560 goto loop;
561
562 case symbol_next_goto_c19:
563 // negative assumption in check-assuming
564 tstack_push_not_symbol(tstack, tkval(lex), tklen(lex), &loc);
565 state = c19;
566 goto loop;
567
568 case next_goto_c16:
569 state = c16;
570 goto loop;
571
572 case int_return:
573 tstack_push_int_type(tstack, &loc);
574 assert(! parser_stack_is_empty(stack));
575 state = parser_pop_state(stack);
576 if (state == done) {
577 goto the_end;
578 }
579 goto loop;
580
581 case real_return:
582 tstack_push_real_type(tstack, &loc);
583 assert(! parser_stack_is_empty(stack));
584 state = parser_pop_state(stack);
585 if (state == done) {
586 goto the_end;
587 }
588 goto loop;
589
590 case bool_return:
591 tstack_push_bool_type(tstack, &loc);
592 assert(! parser_stack_is_empty(stack));
593 state = parser_pop_state(stack);
594 if (state == done) {
595 goto the_end;
596 }
597 goto loop;
598
599 case typesymbol_return:
600 // TK_SYMBOL bound to a type
601 tstack_push_type_by_name(tstack, tkval(lex), &loc);
602 assert(! parser_stack_is_empty(stack));
603 state = parser_pop_state(stack);
604 if (state == done) {
605 goto the_end;
606 }
607 goto loop;
608
609 case next_goto_td1:
610 state = td1;
611 goto loop;
612
613 case scalar_next_goto_td2:
614 tstack_push_op(tstack, MK_SCALAR_TYPE, &loc);
615 state = td2;
616 goto loop;
617
618 case bitvector_next_goto_t4:
619 tstack_push_op(tstack, MK_BV_TYPE, &loc);
620 state = t4;
621 goto loop;
622
623 case tuple_next_push_t6_goto_t0:
624 tstack_push_op(tstack, MK_TUPLE_TYPE, &loc);
625 parser_push_state(stack, t6);
626 state = t0;
627 goto loop;
628
629 case arrow_next_push_t6_push_t0_goto_t0:
630 tstack_push_op(tstack, MK_FUN_TYPE, &loc);
631 parser_push_state(stack, t6);
632 parser_push_state(stack, t0);
633 state = t0;
634 goto loop;
635
636 case termname_next_goto_td3:
637 // free termane in scalar definition
638 tstack_push_free_termname(tstack, tkval(lex), tklen(lex), &loc);
639 state = td3;
640 goto loop;
641
642 case next_goto_t1:
643 state = t1;
644 goto loop;
645
646 case rational_next_goto_r0:
647 tstack_push_rational(tstack, tkval(lex), &loc);
648 state = r0;
649 goto loop;
650
651 case push_t6_goto_t0:
652 parser_push_state(stack, t6);
653 state = t0;
654 goto skip_token;
655
656 case true_return:
657 tstack_push_true(tstack, &loc);
658 assert(! parser_stack_is_empty(stack));
659 state = parser_pop_state(stack);
660 if (state == done) {
661 goto the_end;
662 }
663 goto loop;
664
665 case false_return:
666 tstack_push_false(tstack, &loc);
667 assert(! parser_stack_is_empty(stack));
668 state = parser_pop_state(stack);
669 if (state == done) {
670 goto the_end;
671 }
672 goto loop;
673
674 case rational_return:
675 tstack_push_rational(tstack, tkval(lex), &loc);
676 assert(! parser_stack_is_empty(stack));
677 state = parser_pop_state(stack);
678 if (state == done) {
679 goto the_end;
680 }
681 goto loop;
682
683 case float_return:
684 tstack_push_float(tstack, tkval(lex), &loc);
685 assert(! parser_stack_is_empty(stack));
686 state = parser_pop_state(stack);
687 if (state == done) {
688 goto the_end;
689 }
690 goto loop;
691
692 case bvbin_return:
693 // skip prefix 0b
694 assert(tklen(lex) > 2);
695 tstack_push_bvbin(tstack, tkval(lex) + 2, tklen(lex) - 2, &loc);
696 state = parser_pop_state(stack);
697 if (state == done) {
698 goto the_end;
699 }
700 goto loop;
701
702 case bvhex_return:
703 // skip prefix 0x
704 assert(tklen(lex) > 2);
705 tstack_push_bvhex(tstack, tkval(lex) + 2, tklen(lex) - 2, &loc);
706 state = parser_pop_state(stack);
707 if (state == done) {
708 goto the_end;
709 }
710 goto loop;
711
712 case termsymbol_return:
713 // TK_SYMBOL bound to a term
714 tstack_push_term_by_name(tstack, tkval(lex), &loc);
715 assert(! parser_stack_is_empty(stack));
716 state = parser_pop_state(stack);
717 if (state == done) {
718 goto the_end;
719 }
720 goto loop;
721
722 case next_goto_e1:
723 state = e1;
724 goto loop;
725
726 // all function keywords
727 case if_next_push_e3_goto_e0:
728 tstack_push_op(tstack, MK_ITE, &loc);
729 parser_push_state(stack, e3);
730 state = e0;
731 goto loop;
732
733 case eq_next_push_e3_goto_e0:
734 tstack_push_op(tstack, MK_EQ, &loc);
735 parser_push_state(stack, e3);
736 state = e0;
737 goto loop;
738
739 case diseq_next_push_e3_goto_e0:
740 tstack_push_op(tstack, MK_DISEQ, &loc);
741 parser_push_state(stack, e3);
742 state = e0;
743 goto loop;
744
745 case distinct_next_push_e3_goto_e0:
746 tstack_push_op(tstack, MK_DISTINCT, &loc);
747 parser_push_state(stack, e3);
748 state = e0;
749 goto loop;
750
751 case or_next_push_e3_goto_e0:
752 tstack_push_op(tstack, MK_OR, &loc);
753 parser_push_state(stack, e3);
754 state = e0;
755 goto loop;
756
757 case and_next_push_e3_goto_e0:
758 tstack_push_op(tstack, MK_AND, &loc);
759 parser_push_state(stack, e3);
760 state = e0;
761 goto loop;
762
763 case not_next_push_e3_goto_e0:
764 tstack_push_op(tstack, MK_NOT, &loc);
765 parser_push_state(stack, e3);
766 state = e0;
767 goto loop;
768
769 case xor_next_push_e3_goto_e0:
770 tstack_push_op(tstack, MK_XOR, &loc);
771 parser_push_state(stack, e3);
772 state = e0;
773 goto loop;
774
775 case iff_next_push_e3_goto_e0:
776 tstack_push_op(tstack, MK_IFF, &loc);
777 parser_push_state(stack, e3);
778 state = e0;
779 goto loop;
780
781 case implies_next_push_e3_goto_e0:
782 tstack_push_op(tstack, MK_IMPLIES, &loc);
783 parser_push_state(stack, e3);
784 state = e0;
785 goto loop;
786
787 case mk_tuple_next_push_e3_goto_e0:
788 tstack_push_op(tstack, MK_TUPLE, &loc);
789 parser_push_state(stack, e3);
790 state = e0;
791 goto loop;
792
793 case select_next_push_e3_goto_e0:
794 tstack_push_op(tstack, MK_SELECT, &loc);
795 parser_push_state(stack, e3);
796 state = e0;
797 goto loop;
798
799 case update_tuple_next_push_e3_goto_e0:
800 tstack_push_op(tstack, MK_TUPLE_UPDATE, &loc);
801 parser_push_state(stack, e3);
802 state = e0;
803 goto loop;
804
805 case add_next_push_e3_goto_e0:
806 tstack_push_op(tstack, MK_ADD, &loc);
807 parser_push_state(stack, e3);
808 state = e0;
809 goto loop;
810
811 case sub_next_push_e3_goto_e0:
812 tstack_push_op(tstack, MK_SUB, &loc);
813 parser_push_state(stack, e3);
814 state = e0;
815 goto loop;
816
817 case mul_next_push_e3_goto_e0:
818 tstack_push_op(tstack, MK_MUL, &loc);
819 parser_push_state(stack, e3);
820 state = e0;
821 goto loop;
822
823 case div_next_push_e3_goto_e0:
824 tstack_push_op(tstack, MK_DIVISION, &loc);
825 parser_push_state(stack, e3);
826 state = e0;
827 goto loop;
828
829 case pow_next_push_e3_goto_e0:
830 tstack_push_op(tstack, MK_POW, &loc);
831 parser_push_state(stack, e3);
832 state = e0;
833 goto loop;
834
835 case lt_next_push_e3_goto_e0:
836 tstack_push_op(tstack, MK_LT, &loc);
837 parser_push_state(stack, e3);
838 state = e0;
839 goto loop;
840
841 case le_next_push_e3_goto_e0:
842 tstack_push_op(tstack, MK_LE, &loc);
843 parser_push_state(stack, e3);
844 state = e0;
845 goto loop;
846
847 case gt_next_push_e3_goto_e0:
848 tstack_push_op(tstack, MK_GT, &loc);
849 parser_push_state(stack, e3);
850 state = e0;
851 goto loop;
852
853 case ge_next_push_e3_goto_e0:
854 tstack_push_op(tstack, MK_GE, &loc);
855 parser_push_state(stack, e3);
856 state = e0;
857 goto loop;
858
859 case mk_bv_next_push_e3_goto_e0:
860 tstack_push_op(tstack, MK_BV_CONST, &loc);
861 parser_push_state(stack, e3);
862 state = e0;
863 goto loop;
864
865 case bv_add_next_push_e3_goto_e0:
866 tstack_push_op(tstack, MK_BV_ADD, &loc);
867 parser_push_state(stack, e3);
868 state = e0;
869 goto loop;
870
871 case bv_sub_next_push_e3_goto_e0:
872 tstack_push_op(tstack, MK_BV_SUB, &loc);
873 parser_push_state(stack, e3);
874 state = e0;
875 goto loop;
876
877 case bv_mul_next_push_e3_goto_e0:
878 tstack_push_op(tstack, MK_BV_MUL, &loc);
879 parser_push_state(stack, e3);
880 state = e0;
881 goto loop;
882
883 case bv_neg_next_push_e3_goto_e0:
884 tstack_push_op(tstack, MK_BV_NEG, &loc);
885 parser_push_state(stack, e3);
886 state = e0;
887 goto loop;
888
889 case bv_pow_next_push_e3_goto_e0:
890 tstack_push_op(tstack, MK_BV_POW, &loc);
891 parser_push_state(stack, e3);
892 state = e0;
893 goto loop;
894
895 case bv_not_next_push_e3_goto_e0:
896 tstack_push_op(tstack, MK_BV_NOT, &loc);
897 parser_push_state(stack, e3);
898 state = e0;
899 goto loop;
900
901 case bv_and_next_push_e3_goto_e0:
902 tstack_push_op(tstack, MK_BV_AND, &loc);
903 parser_push_state(stack, e3);
904 state = e0;
905 goto loop;
906
907 case bv_or_next_push_e3_goto_e0:
908 tstack_push_op(tstack, MK_BV_OR, &loc);
909 parser_push_state(stack, e3);
910 state = e0;
911 goto loop;
912
913 case bv_xor_next_push_e3_goto_e0:
914 tstack_push_op(tstack, MK_BV_XOR, &loc);
915 parser_push_state(stack, e3);
916 state = e0;
917 goto loop;
918
919 case bv_nand_next_push_e3_goto_e0:
920 tstack_push_op(tstack, MK_BV_NAND, &loc);
921 parser_push_state(stack, e3);
922 state = e0;
923 goto loop;
924
925 case bv_nor_next_push_e3_goto_e0:
926 tstack_push_op(tstack, MK_BV_NOR, &loc);
927 parser_push_state(stack, e3);
928 state = e0;
929 goto loop;
930
931 case bv_xnor_next_push_e3_goto_e0:
932 tstack_push_op(tstack, MK_BV_XNOR, &loc);
933 parser_push_state(stack, e3);
934 state = e0;
935 goto loop;
936
937 case bv_shift_left0_next_push_e3_goto_e0:
938 tstack_push_op(tstack, MK_BV_SHIFT_LEFT0, &loc);
939 parser_push_state(stack, e3);
940 state = e0;
941 goto loop;
942
943 case bv_shift_left1_next_push_e3_goto_e0:
944 tstack_push_op(tstack, MK_BV_SHIFT_LEFT1, &loc);
945 parser_push_state(stack, e3);
946 state = e0;
947 goto loop;
948
949 case bv_shift_right0_next_push_e3_goto_e0:
950 tstack_push_op(tstack, MK_BV_SHIFT_RIGHT0, &loc);
951 parser_push_state(stack, e3);
952 state = e0;
953 goto loop;
954
955 case bv_shift_right1_next_push_e3_goto_e0:
956 tstack_push_op(tstack, MK_BV_SHIFT_RIGHT1, &loc);
957 parser_push_state(stack, e3);
958 state = e0;
959 goto loop;
960
961 case bv_ashift_right_next_push_e3_goto_e0:
962 tstack_push_op(tstack, MK_BV_ASHIFT_RIGHT, &loc);
963 parser_push_state(stack, e3);
964 state = e0;
965 goto loop;
966
967 case bv_rotate_left_next_push_e3_goto_e0:
968 tstack_push_op(tstack, MK_BV_ROTATE_LEFT, &loc);
969 parser_push_state(stack, e3);
970 state = e0;
971 goto loop;
972
973 case bv_rotate_right_next_push_e3_goto_e0:
974 tstack_push_op(tstack, MK_BV_ROTATE_RIGHT, &loc);
975 parser_push_state(stack, e3);
976 state = e0;
977 goto loop;
978
979 case bv_extract_next_push_e3_goto_e0:
980 tstack_push_op(tstack, MK_BV_EXTRACT, &loc);
981 parser_push_state(stack, e3);
982 state = e0;
983 goto loop;
984
985 case bv_concat_next_push_e3_goto_e0:
986 tstack_push_op(tstack, MK_BV_CONCAT, &loc);
987 parser_push_state(stack, e3);
988 state = e0;
989 goto loop;
990
991 case bv_repeat_next_push_e3_goto_e0:
992 tstack_push_op(tstack, MK_BV_REPEAT, &loc);
993 parser_push_state(stack, e3);
994 state = e0;
995 goto loop;
996
997 case bv_sign_extend_next_push_e3_goto_e0:
998 tstack_push_op(tstack, MK_BV_SIGN_EXTEND, &loc);
999 parser_push_state(stack, e3);
1000 state = e0;
1001 goto loop;
1002
1003 case bv_zero_extend_next_push_e3_goto_e0:
1004 tstack_push_op(tstack, MK_BV_ZERO_EXTEND, &loc);
1005 parser_push_state(stack, e3);
1006 state = e0;
1007 goto loop;
1008
1009 case bv_ge_next_push_e3_goto_e0:
1010 tstack_push_op(tstack, MK_BV_GE, &loc);
1011 parser_push_state(stack, e3);
1012 state = e0;
1013 goto loop;
1014
1015 case bv_gt_next_push_e3_goto_e0:
1016 tstack_push_op(tstack, MK_BV_GT, &loc);
1017 parser_push_state(stack, e3);
1018 state = e0;
1019 goto loop;
1020
1021 case bv_le_next_push_e3_goto_e0:
1022 tstack_push_op(tstack, MK_BV_LE, &loc);
1023 parser_push_state(stack, e3);
1024 state = e0;
1025 goto loop;
1026
1027 case bv_lt_next_push_e3_goto_e0:
1028 tstack_push_op(tstack, MK_BV_LT, &loc);
1029 parser_push_state(stack, e3);
1030 state = e0;
1031 goto loop;
1032
1033 case bv_sge_next_push_e3_goto_e0:
1034 tstack_push_op(tstack, MK_BV_SGE, &loc);
1035 parser_push_state(stack, e3);
1036 state = e0;
1037 goto loop;
1038
1039 case bv_sgt_next_push_e3_goto_e0:
1040 tstack_push_op(tstack, MK_BV_SGT, &loc);
1041 parser_push_state(stack, e3);
1042 state = e0;
1043 goto loop;
1044
1045 case bv_sle_next_push_e3_goto_e0:
1046 tstack_push_op(tstack, MK_BV_SLE, &loc);
1047 parser_push_state(stack, e3);
1048 state = e0;
1049 goto loop;
1050
1051 case bv_slt_next_push_e3_goto_e0:
1052 tstack_push_op(tstack, MK_BV_SLT, &loc);
1053 parser_push_state(stack, e3);
1054 state = e0;
1055 goto loop;
1056
1057 case bv_shl_next_push_e3_goto_e0:
1058 tstack_push_op(tstack, MK_BV_SHL, &loc);
1059 parser_push_state(stack, e3);
1060 state = e0;
1061 goto loop;
1062
1063 case bv_lshr_next_push_e3_goto_e0:
1064 tstack_push_op(tstack, MK_BV_LSHR, &loc);
1065 parser_push_state(stack, e3);
1066 state = e0;
1067 goto loop;
1068
1069 case bv_ashr_next_push_e3_goto_e0:
1070 tstack_push_op(tstack, MK_BV_ASHR, &loc);
1071 parser_push_state(stack, e3);
1072 state = e0;
1073 goto loop;
1074
1075 case bv_div_next_push_e3_goto_e0:
1076 tstack_push_op(tstack, MK_BV_DIV, &loc);
1077 parser_push_state(stack, e3);
1078 state = e0;
1079 goto loop;
1080
1081 case bv_rem_next_push_e3_goto_e0:
1082 tstack_push_op(tstack, MK_BV_REM, &loc);
1083 parser_push_state(stack, e3);
1084 state = e0;
1085 goto loop;
1086
1087 case bv_sdiv_next_push_e3_goto_e0:
1088 tstack_push_op(tstack, MK_BV_SDIV, &loc);
1089 parser_push_state(stack, e3);
1090 state = e0;
1091 goto loop;
1092
1093 case bv_srem_next_push_e3_goto_e0:
1094 tstack_push_op(tstack, MK_BV_SREM, &loc);
1095 parser_push_state(stack, e3);
1096 state = e0;
1097 goto loop;
1098
1099 case bv_smod_next_push_e3_goto_e0:
1100 tstack_push_op(tstack, MK_BV_SMOD, &loc);
1101 parser_push_state(stack, e3);
1102 state = e0;
1103 goto loop;
1104
1105 case bv_redor_next_push_e3_goto_e0:
1106 tstack_push_op(tstack, MK_BV_REDOR, &loc);
1107 parser_push_state(stack, e3);
1108 state = e0;
1109 goto loop;
1110
1111 case bv_redand_next_push_e3_goto_e0:
1112 tstack_push_op(tstack, MK_BV_REDAND, &loc);
1113 parser_push_state(stack, e3);
1114 state = e0;
1115 goto loop;
1116
1117 case bv_comp_next_push_e3_goto_e0:
1118 tstack_push_op(tstack, MK_BV_COMP, &loc);
1119 parser_push_state(stack, e3);
1120 state = e0;
1121 goto loop;
1122
1123 case bool_to_bv_next_push_e3_goto_e0:
1124 tstack_push_op(tstack, MK_BOOL_TO_BV, &loc);
1125 parser_push_state(stack, e3);
1126 state = e0;
1127 goto loop;
1128
1129 case bit_next_push_e3_goto_e0:
1130 tstack_push_op(tstack, MK_BIT, &loc);
1131 parser_push_state(stack, e3);
1132 state = e0;
1133 goto loop;
1134
1135 case floor_next_push_e3_goto_e0:
1136 tstack_push_op(tstack, MK_FLOOR, &loc);
1137 parser_push_state(stack, e3);
1138 state = e0;
1139 goto loop;
1140
1141 case ceil_next_push_e3_goto_e0:
1142 tstack_push_op(tstack, MK_CEIL, &loc);
1143 parser_push_state(stack, e3);
1144 state = e0;
1145 goto loop;
1146
1147 case abs_next_push_e3_goto_e0:
1148 tstack_push_op(tstack, MK_ABS, &loc);
1149 parser_push_state(stack, e3);
1150 state = e0;
1151 goto loop;
1152
1153 case idiv_next_push_e3_goto_e0:
1154 tstack_push_op(tstack, MK_IDIV, &loc);
1155 parser_push_state(stack, e3);
1156 state = e0;
1157 goto loop;
1158
1159 case mod_next_push_e3_goto_e0:
1160 tstack_push_op(tstack, MK_MOD, &loc);
1161 parser_push_state(stack, e3);
1162 state = e0;
1163 goto loop;
1164
1165 case divides_next_push_e3_goto_e0:
1166 tstack_push_op(tstack, MK_DIVIDES, &loc);
1167 parser_push_state(stack, e3);
1168 state = e0;
1169 goto loop;
1170
1171 case is_int_next_push_e3_goto_e0:
1172 tstack_push_op(tstack, MK_IS_INT, &loc);
1173 parser_push_state(stack, e3);
1174 state = e0;
1175 goto loop;
1176
1177 case update_next_push_e5_goto_e0:
1178 tstack_push_op(tstack, MK_UPDATE, &loc);
1179 parser_push_state(stack, e5);
1180 state = e0;
1181 goto loop;
1182
1183 case forall_next_goto_e10:
1184 tstack_push_op(tstack, MK_FORALL, &loc);
1185 state = e10;
1186 goto loop;
1187
1188 case exists_next_goto_e10:
1189 tstack_push_op(tstack, MK_EXISTS, &loc);
1190 state = e10;
1191 goto loop;
1192
1193 case lambda_next_goto_e10:
1194 tstack_push_op(tstack, MK_LAMBDA, &loc);
1195 state = e10;
1196 goto loop;
1197
1198 case let_next_goto_e15:
1199 tstack_push_op(tstack, LET, &loc);
1200 state = e15;
1201 goto loop;
1202
1203 case push_e3_push_e0_goto_e0:
1204 // uninterpreted function
1205 tstack_push_op(tstack, MK_APPLY, &loc);
1206 parser_push_state(stack, e3);
1207 parser_push_state(stack, e0);
1208 state = e0;
1209 goto skip_token;
1210
1211 case push_e3_goto_e0:
1212 parser_push_state(stack, e3);
1213 state = e0;
1214 goto skip_token;
1215
1216 case next_push_e7_goto_e0:
1217 parser_push_state(stack, e7);
1218 state = e0;
1219 goto loop;
1220
1221 case next_push_r0_goto_e0:
1222 parser_push_state(stack, r0);
1223 state = e0;
1224 goto loop;
1225
1226 case push_e7_goto_e0:
1227 parser_push_state(stack, e7);
1228 state = e0;
1229 goto skip_token;
1230
1231 case next_goto_e11:
1232 state = e11;
1233 goto loop;
1234
1235 case e11_varname_next_goto_e12:
1236 // first var decl in quantifiers
1237 tstack_push_op(tstack, DECLARE_VAR, &loc);
1238 tstack_push_symbol(tstack, tkval(lex), tklen(lex), &loc);
1239 state = e12;
1240 goto loop;
1241
1242 case next_push_e14_goto_t0:
1243 parser_push_state(stack, e14);
1244 state = t0;
1245 goto loop;
1246
1247 case e14_varname_next_goto_e12:
1248 // var decl in quantifier except the first one
1249 tstack_eval(tstack); // eval previous binding
1250 // prepare for next var decl
1251 tstack_push_op(tstack, DECLARE_VAR, &loc);
1252 tstack_push_symbol(tstack, tkval(lex), tklen(lex), &loc);
1253 state = e12;
1254 goto loop;
1255
1256 case e14_next_push_r0_goto_e0:
1257 // end of var decls
1258 tstack_eval(tstack); // eval last binding
1259 parser_push_state(stack, r0);
1260 state = e0;
1261 goto loop;
1262
1263 case next_goto_e16:
1264 state = e16;
1265 goto loop;
1266
1267 case next_goto_e17:
1268 state = e17;
1269 goto loop;
1270
1271 case termname_next_push_e19_goto_e0:
1272 // name in binding
1273 tstack_push_op(tstack, BIND, &loc);
1274 tstack_push_symbol(tstack, tkval(lex), tklen(lex), &loc);
1275 parser_push_state(stack, e19);
1276 state = e0;
1277 goto loop;
1278
1279 case next_goto_e20:
1280 // end of let binding: evaluate the binding
1281 tstack_eval(tstack);
1282 state = e20;
1283 goto loop;
1284
1285 case error_lpar_expected:
1286 syntax_error(lex, err, TK_LP);
1287 goto cleanup;
1288
1289 case error_symbol_expected:
1290 syntax_error(lex, err, TK_SYMBOL);
1291 goto cleanup;
1292
1293 case error_string_expected:
1294 syntax_error(lex, err, TK_STRING);
1295 goto cleanup;
1296
1297 case error_colon_colon_expected:
1298 syntax_error(lex, err, TK_COLON_COLON);
1299 goto cleanup;
1300
1301 case error_rational_expected:
1302 syntax_error(lex, err, TK_NUM_RATIONAL);
1303 goto cleanup;
1304
1305 case error_rpar_expected:
1306 syntax_error(lex, err, TK_RP);
1307 goto cleanup;
1308
1309 case error_not_expected:
1310 // this means that we got a token other than 'not'.
1311 syntax_error(lex, err, TK_NOT);
1312 goto cleanup;
1313
1314 case error_not_a_command:
1315 syntax_error_bad_command(lex, err);
1316 goto cleanup;
1317
1318 case error:
1319 syntax_error(lex, err, -1);
1320 goto cleanup;
1321 }
1322
1323 } else {
1324 // exception raised by term_stack
1325 if (err == NULL) {
1326 export_tstack_error(tstack, exception);
1327 } else {
1328 term_stack_error(err, reader_name(lex), tstack, exception);
1329 }
1330 goto cleanup;
1331 }
1332
1333 cleanup:
1334 tstack_reset(tstack);
1335 parser_stack_reset(stack);
1336 return -1;
1337
1338 the_end:
1339 return 0;
1340 }
1341
1342
1343 /*
1344 * Top-level calls:
1345 */
parse_yices_command(parser_t * parser,FILE * err)1346 extern int32_t parse_yices_command(parser_t *parser, FILE *err) {
1347 return yices_parse(parser, c0, err);
1348 }
1349
parse_yices_term(parser_t * parser,FILE * err)1350 extern term_t parse_yices_term(parser_t *parser, FILE *err) {
1351 loc_t loc;
1352
1353 loc.line = 0;
1354 loc.column = 0;
1355 tstack_push_op(parser->tstack, BUILD_TERM, &loc);
1356 if (yices_parse(parser, e0, err) < 0) {
1357 return NULL_TERM;
1358 }
1359
1360 /*
1361 * Unless there's a bug somewhere. eval cannot generate an exception here.
1362 * (cf. eval_build_term in term_stack.c)
1363 */
1364 assert(parser->tstack->top_op == BUILD_TERM);
1365 tstack_eval(parser->tstack);
1366
1367 assert(parser_stack_is_empty(&parser->pstack) &&
1368 tstack_is_empty(parser->tstack));
1369
1370 return tstack_get_term(parser->tstack);
1371 }
1372
1373
parse_yices_type(parser_t * parser,FILE * err)1374 type_t parse_yices_type(parser_t *parser, FILE *err) {
1375 loc_t loc;
1376
1377 loc.line = 0;
1378 loc.column = 0;
1379 tstack_push_op(parser->tstack, BUILD_TYPE, &loc);
1380 if (yices_parse(parser, td0, err) < 0) {
1381 return NULL_TYPE;
1382 }
1383
1384 /*
1385 * Unless there's a bug somewhere. eval cannot generate an exception here.
1386 * (cf. eval_build_type in term_stack.c)
1387 */
1388 assert(parser->tstack->top_op == BUILD_TYPE);
1389 tstack_eval(parser->tstack);
1390
1391 assert(parser_stack_is_empty(&parser->pstack) &&
1392 tstack_is_empty(parser->tstack));
1393
1394 return tstack_get_type(parser->tstack);
1395 }
1396
1397
1398