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