1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
|
%{
/*****************************************************************************/
/*!
* \file smtlib.lex
*
* Author: Clark Barrett
*
* Created: 2005
*
* <hr>
*
* License to use, copy, modify, sell and/or distribute this software
* and its documentation for any purpose is hereby granted without
* royalty, subject to the terms and conditions defined in the \ref
* LICENSE file provided with this distribution.
*
* <hr>
*
*/
/*****************************************************************************/
#include <iostream>
#include "parser_temp.h"
//#include "expr_manager.h" /* for the benefit of parsesmtlib_defs.h */
#include "parsesmtlib_defs.h"
//#include "debug.h"
namespace CVC3 {
extern ParserTemp* parserTemp;
}
extern int smtlib_inputLine;
extern char *smtlibtext;
extern int smtliberror (const char *msg);
static int smtlibinput(std::istream& is, char* buf, int size) {
int res;
if(is) {
// If interactive, read line by line; otherwise read as much as we
// can gobble
if(CVC3::parserTemp->interactive) {
// Print the current prompt
std::cout << CVC3::parserTemp->getPrompt() << std::flush;
// Set the prompt to "middle of the command" one
CVC3::parserTemp->setPrompt2();
// Read the line
is.getline(buf, size-1);
} else // Set the terminator char to 0
is.getline(buf, size-1, 0);
// If failbit is set, but eof is not, it means the line simply
// didn't fit; so we clear the state and keep on reading.
bool partialStr = is.fail() && !is.eof();
if(partialStr)
is.clear();
for(res = 0; res<size && buf[res] != 0; res++) ;
if(res == size) smtliberror("Lexer bug: overfilled the buffer");
if(!partialStr) { // Insert \n into the buffer
buf[res++] = '\n';
buf[res] = '\0';
}
} else {
res = YY_NULL;
}
return res;
}
// Redefine the input buffer function to read from an istream
#define YY_INPUT(buf,result,max_size) \
result = smtlibinput(*CVC3::parserTemp->is, buf, max_size);
int smtlib_bufSize() { return YY_BUF_SIZE; }
YY_BUFFER_STATE smtlib_buf_state() { return YY_CURRENT_BUFFER; }
/* some wrappers for methods that need to refer to a struct.
These are used by CVC3::Parser. */
void *smtlib_createBuffer(int sz) {
return (void *)smtlib_create_buffer(NULL, sz);
}
void smtlib_deleteBuffer(void *buf_state) {
smtlib_delete_buffer((struct yy_buffer_state *)buf_state);
}
void smtlib_switchToBuffer(void *buf_state) {
smtlib_switch_to_buffer((struct yy_buffer_state *)buf_state);
}
void *smtlib_bufState() {
return (void *)smtlib_buf_state();
}
void smtlib_setInteractive(bool is_interactive) {
yy_set_interactive(is_interactive);
}
// File-static (local to this file) variables and functions
static std::string _string_lit;
static char escapeChar(char c) {
switch(c) {
case 'n': return '\n';
case 't': return '\t';
default: return c;
}
}
// for now, we don't have subranges.
//
// ".." { return DOTDOT_TOK; }
/*OPCHAR (['!#?\_$&\|\\@])*/
%}
%option noyywrap
%option nounput
%option noreject
%option noyymore
%option yylineno
%x COMMENT
%x STRING_LITERAL
%x USER_VALUE
%s PAT_MODE
LETTER ([a-zA-Z])
DIGIT ([0-9])
OPCHAR (['\.\_])
IDCHAR ({LETTER}|{DIGIT}|{OPCHAR})
%%
[\n] { CVC3::parserTemp->lineNum++; }
[ \t\r\f] { /* skip whitespace */ }
{DIGIT}+"\."{DIGIT}+ { smtliblval.str = new std::string(smtlibtext); return NUMERAL_TOK; }
{DIGIT}+ { smtliblval.str = new std::string(smtlibtext); return NUMERAL_TOK;
}
";" { BEGIN COMMENT; }
<COMMENT>"\n" { BEGIN INITIAL; /* return to normal mode */
CVC3::parserTemp->lineNum++; }
<COMMENT>. { /* stay in comment mode */ }
<INITIAL>"\"" { BEGIN STRING_LITERAL;
_string_lit.erase(_string_lit.begin(),
_string_lit.end()); }
<STRING_LITERAL>"\\". { /* escape characters (like \n or \") */
_string_lit.insert(_string_lit.end(),
escapeChar(smtlibtext[1])); }
<STRING_LITERAL>"\"" { BEGIN INITIAL; /* return to normal mode */
smtliblval.str = new std::string(_string_lit);
return STRING_TOK; }
<STRING_LITERAL>. { _string_lit.insert(_string_lit.end(),*smtlibtext); }
<INITIAL>":pat" { BEGIN PAT_MODE;
return PAT_TOK;}
<PAT_MODE>"}" { BEGIN INITIAL;
return RCURBRACK_TOK; }
<INITIAL>"{" { BEGIN USER_VALUE;
_string_lit.erase(_string_lit.begin(),
_string_lit.end()); }
<USER_VALUE>"\\"[{}] { /* escape characters */
_string_lit.insert(_string_lit.end(),smtlibtext[1]); }
<USER_VALUE>"}" { BEGIN INITIAL; /* return to normal mode */
smtliblval.str = new std::string(_string_lit);
return USER_VAL_TOK; }
<USER_VALUE>"\n" { _string_lit.insert(_string_lit.end(),'\n');
CVC3::parserTemp->lineNum++; }
<USER_VALUE>. { _string_lit.insert(_string_lit.end(),*smtlibtext); }
"true" { return TRUE_TOK; }
"false" { return FALSE_TOK; }
"ite" { return ITE_TOK; }
"not" { return NOT_TOK; }
"implies" { return IMPLIES_TOK; }
"if_then_else" { return IF_THEN_ELSE_TOK; }
"and" { return AND_TOK; }
"or" { return OR_TOK; }
"xor" { return XOR_TOK; }
"iff" { return IFF_TOK; }
"exists" { return EXISTS_TOK; }
"forall" { return FORALL_TOK; }
"let" { return LET_TOK; }
"flet" { return FLET_TOK; }
"notes" { return NOTES_TOK; }
"cvc_command" { return CVC_COMMAND_TOK; }
"sorts" { return SORTS_TOK; }
"funs" { return FUNS_TOK; }
"preds" { return PREDS_TOK; }
"extensions" { return EXTENSIONS_TOK; }
"definition" { return DEFINITION_TOK; }
"axioms" { return AXIOMS_TOK; }
"logic" { return LOGIC_TOK; }
"sat" { return SAT_TOK; }
"unsat" { return UNSAT_TOK; }
"unknown" { return UNKNOWN_TOK; }
"assumption" { return ASSUMPTION_TOK; }
"formula" { return FORMULA_TOK; }
"status" { return STATUS_TOK; }
"benchmark" { return BENCHMARK_TOK; }
"extrasorts" { return EXTRASORTS_TOK; }
"extrafuns" { return EXTRAFUNS_TOK; }
"extrapreds" { return EXTRAPREDS_TOK; }
"language" { return LANGUAGE_TOK; }
"distinct" { return DISTINCT_TOK; }
":pattern" { return PAT_TOK; }
":" { return COLON_TOK; }
"\[" { return LBRACKET_TOK; }
"\]" { return RBRACKET_TOK; }
"{" { return LCURBRACK_TOK;}
"}" { return RCURBRACK_TOK;}
"(" { return LPAREN_TOK; }
")" { return RPAREN_TOK; }
"$" { return DOLLAR_TOK; }
"?" { return QUESTION_TOK; }
[=<>&@#+\-*/%|~]+ { smtliblval.str = new std::string(smtlibtext); return AR_SYMB; }
({LETTER})({IDCHAR})* {smtliblval.str = new std::string(smtlibtext); return SYM_TOK; }
<<EOF>> { return EOF_TOK; }
. { smtliberror("Illegal input character."); }
%%
|
