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 * Lexer for Yices language with support for EF-solver
21 * - separators are ( ) : and spaces
22 *
23 * - strings are delimited by " with escaped char \n, \t, etc. allowed
24 *
25 * - two kinds of numeric literals are recognized
26 * TK_NUM_RATIONAL: <optional_sign><digits>/<digits>
27 * or <optional_sign><digits>
28 * TK_NUM_FLOAT:
29 * <optional_sign> <digits> . <digits>
30 * <optional_sign> <digits> <exp> <optional_sign> <digits>
31 * <optional_sign> <digits> . <digits> <exp> <optional_sign> <digits>
32 *
33 * (the two formats recognized by string-to-rational conversions in rational.c)
34 *
35 * - bit-vector literals are written 0b<binary digits> (cf. bv_constants.c)
36 * or 0x<hexa digits>
37 *
38 * - comments start with ; and extend to the end of the line
39 *
40 * 2013/12/12: added ef-solve token
41 * 2014/03: added export-to-dimancs and show-implicants
42 */
43
44 #ifndef __YICES_LEXER_H
45 #define __YICES_LEXER_H
46
47 #include "parser_utils/lexer.h"
48
49
50 /*
51 * Tokens
52 */
53 enum yices_token {
54 // commands
55 TK_DEFINE_TYPE, TK_DEFINE, TK_ASSERT, TK_CHECK, TK_CHECK_ASSUMING,
56 TK_PUSH, TK_POP, TK_RESET, TK_DUMP_CONTEXT, TK_EXIT,
57 TK_ECHO, TK_INCLUDE, TK_SHOW_MODEL, TK_EVAL, TK_SET_PARAM,
58 TK_SHOW_PARAM, TK_SHOW_PARAMS, TK_SHOW_STATS, TK_RESET_STATS,
59 TK_SET_TIMEOUT, TK_SHOW_TIMEOUT, TK_HELP, TK_EF_SOLVE,
60 TK_EXPORT_TO_DIMACS, TK_SHOW_IMPLICANT,
61 TK_SHOW_UNSAT_CORE, TK_SHOW_UNSAT_ASSUMPTIONS,
62 TK_SHOW_REDUCED_MODEL,
63
64 // term constructors
65 TK_UPDATE, TK_FORALL, TK_EXISTS, TK_LAMBDA, TK_LET,
66
67 // separators and end-of-stream
68 TK_LP, TK_RP, TK_COLON_COLON, TK_EOS,
69
70 // literals
71 TK_STRING, TK_NUM_RATIONAL, TK_NUM_FLOAT, TK_BV_CONSTANT, TK_HEX_CONSTANT,
72
73 // any symbol that's not a keyword
74 TK_SYMBOL,
75
76 // type keywords
77 TK_BOOL, TK_INT, TK_REAL, TK_BITVECTOR, TK_SCALAR, TK_TUPLE, TK_ARROW,
78
79 // term keywords
80 TK_TRUE, TK_FALSE, TK_IF, TK_ITE, TK_EQ, TK_DISEQ, TK_DISTINCT,
81 TK_OR, TK_AND, TK_NOT, TK_XOR, TK_IFF, TK_IMPLIES, TK_MK_TUPLE,
82 TK_SELECT, TK_UPDATE_TUPLE,
83
84 // arithmetic keywords
85 TK_ADD, TK_SUB, TK_MUL, TK_DIV, TK_POW, TK_LT, TK_LE, TK_GT, TK_GE,
86
87 // bitvector keywords
88 TK_MK_BV, TK_BV_ADD, TK_BV_SUB, TK_BV_MUL, TK_BV_NEG, TK_BV_POW,
89 TK_BV_NOT, TK_BV_AND, TK_BV_OR, TK_BV_XOR, TK_BV_NAND, TK_BV_NOR, TK_BV_XNOR,
90
91 TK_BV_SHIFT_LEFT0, TK_BV_SHIFT_LEFT1, TK_BV_SHIFT_RIGHT0,
92 TK_BV_SHIFT_RIGHT1, TK_BV_ASHIFT_RIGHT, TK_BV_ROTATE_LEFT, TK_BV_ROTATE_RIGHT,
93 TK_BV_EXTRACT, TK_BV_CONCAT, TK_BV_REPEAT,
94 TK_BV_SIGN_EXTEND, TK_BV_ZERO_EXTEND,
95 TK_BV_GE, TK_BV_GT, TK_BV_LE, TK_BV_LT,
96 TK_BV_SGE, TK_BV_SGT, TK_BV_SLE, TK_BV_SLT,
97
98 // more bitvector operators
99 TK_BV_SHL, TK_BV_LSHR, TK_BV_ASHR,
100 TK_BV_DIV, TK_BV_REM, TK_BV_SDIV, TK_BV_SREM, TK_BV_SMOD,
101 TK_BV_REDOR, TK_BV_REDAND, TK_BV_COMP,
102
103 // conversions between bitvectors and Booleans
104 TK_BOOL_TO_BV, TK_BIT,
105
106 // more arithmetic functions (inherited from SMT-LIB2 Ints theory)
107 TK_FLOOR, TK_CEIL, TK_ABS, TK_IDIV, TK_MOD, TK_DIVIDES, TK_IS_INT,
108
109 // unrecognized tokens or other errors
110 TK_OPEN_STRING, TK_EMPTY_BVCONST, TK_EMPTY_HEXCONST,
111 TK_INVALID_NUM, TK_ZERO_DIVISOR, TK_ERROR,
112 };
113
114 #define NUM_YICES_TOKENS (TK_ERROR+1)
115
116 typedef enum yices_token yices_token_t;
117
118
119 /*
120 * Lexer initialization:
121 * - for file_lexer, return code 0 means OK, negative code means error
122 * (can't open the file).
123 */
124 extern int32_t init_yices_file_lexer(lexer_t *lex, char *filename);
125
126 extern void init_yices_stream_lexer(lexer_t *lex, FILE *f, char *name);
127
init_yices_stdin_lexer(lexer_t * lex)128 static inline void init_yices_stdin_lexer(lexer_t *lex) {
129 init_yices_stream_lexer(lex, stdin, "stdin");
130 }
131
132 extern void init_yices_string_lexer(lexer_t *lex, char *data, char *name);
133
134
135
136 /*
137 * Conversion from a token type to a string.
138 * The internal table is initialized by one of the
139 * init_yices_lexer functions. This function should not be
140 * called before the init function.
141 */
142 extern char *yices_token_to_string(yices_token_t tk);
143
144
145 /*
146 * Read next token and return its type tk
147 * - set lex->token to tk
148 * - set lex->tk_pos, etc.
149 * - if token is TK_STRING, TK_NUM_RATIONAL, TK_NUM_FLOAT,
150 * TK_BV_CONSTANT, TK_SYMBOL, or TK_ERROR,
151 * the token value is set in lex->buffer.
152 */
153 extern yices_token_t next_yices_token(lexer_t *lex);
154
155
156
157
158 #endif /* __YICE_LEXER_H */
159