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 #include <stdio.h>
20 #include <stdlib.h>
21 #include <inttypes.h>
22
23 #include "frontend/yices/yices_lexer.h"
24
25 static lexer_t lexer;
26
print_token(token_t tk)27 static void print_token(token_t tk) {
28 printf("---> Token %s\n", yices_token_to_string(tk));
29 printf(" pos = %"PRIu64", line = %"PRIu32", column = %"PRIu32"\n",
30 lexer.tk_pos, lexer.tk_line, lexer.tk_column);
31 if (tk != TK_LP && tk != TK_RP && tk != TK_EOS && tk != TK_COLON_COLON && tk != TK_ERROR) {
32 printf(" value: %s\n", current_token_value(&lexer));
33 printf(" length: %"PRIu32"\n", current_token_length(&lexer));
34 }
35 }
36
main(int argc,char * argv[])37 int main(int argc, char *argv[]) {
38 char *filename;
39 token_t tk;
40
41 if (argc <= 1) {
42 init_yices_stdin_lexer(&lexer);
43 } else {
44 filename = argv[1];
45 if (init_yices_file_lexer(&lexer, filename) < 0) {
46 perror(filename);
47 exit(2);
48 }
49 }
50
51 do {
52 tk = next_yices_token(&lexer);
53 if (tk >= TK_OPEN_STRING) {
54 printf("****** ERROR ******\n");
55 }
56 print_token(tk);
57 } while (tk != TK_EOS);
58
59 close_lexer(&lexer);
60
61 return 0;
62 }
63