cprover
smt2_parser.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "smt2_parser.h"
10 
11 #include <istream>
12 #include <ostream>
13 
15 {
16  // any non-empty sequence of letters, digits and the characters
17  // ~ ! @ $ % ^ & * _ - + = < > . ? /
18  // that does not start with a digit and is not a reserved word.
19 
20  return isalnum(ch) ||
21  ch=='~' || ch=='!' || ch=='@' || ch=='$' || ch=='%' ||
22  ch=='^' || ch=='&' || ch=='*' || ch=='_' || ch=='-' ||
23  ch=='+' || ch=='=' || ch=='<' || ch=='>' || ch=='.' ||
24  ch=='?' || ch=='/';
25 }
26 
28 {
29  // any non-empty sequence of letters, digits and the characters
30  // ~ ! @ $ % ^ & * _ - + = < > . ? /
31  // that does not start with a digit and is not a reserved word.
32 
33  buffer.clear();
34 
35  char ch;
36  while(in.get(ch))
37  {
39  {
40  buffer+=ch;
41  }
42  else
43  {
44  in.unget(); // put back
45  return;
46  }
47  }
48 
49  // eof -- this is ok here
50 }
51 
53 {
54  // we accept any sequence of digits and dots
55 
56  buffer.clear();
57 
58  char ch;
59  while(in.get(ch))
60  {
61  if(isdigit(ch) || ch=='.')
62  {
63  buffer+=ch;
64  }
65  else
66  {
67  in.unget(); // put back
68  return;
69  }
70  }
71 
72  // eof -- this is ok here
73 }
74 
76 {
77  // we accept any sequence of '0' or '1'
78 
79  buffer.clear();
80  buffer+='#';
81  buffer+='b';
82 
83  char ch;
84  while(in.get(ch))
85  {
86  if(ch=='0' || ch=='1')
87  {
88  buffer+=ch;
89  }
90  else
91  {
92  in.unget(); // put back
93  return;
94  }
95  }
96 
97  // eof -- this is ok here
98 }
99 
101 {
102  // we accept any sequence of '0'-'9', 'a'-'f', 'A'-'F'
103 
104  buffer.clear();
105  buffer+='#';
106  buffer+='x';
107 
108  char ch;
109  while(in.get(ch))
110  {
111  if(isxdigit(ch))
112  {
113  buffer+=ch;
114  }
115  else
116  {
117  in.unget(); // put back
118  return;
119  }
120  }
121 
122  // eof -- this is ok here
123 }
124 
126 {
127  // any sequence of printable ASCII characters (including space,
128  // tab, and line-breaking characters) except for the backslash
129  // character \, that starts and ends with | and does not otherwise
130  // contain |
131 
132  buffer.clear();
133 
134  char ch;
135  while(in.get(ch))
136  {
137  if(ch=='|')
138  return; // done
139  buffer+=ch;
140  }
141 
142  // Hmpf. Eof before end of quoted string. This is an error.
143 }
144 
146 {
147  buffer.clear();
148 
149  char ch;
150  while(in.get(ch))
151  {
152  if(ch=='"')
153  {
154  // quotes may be escaped by repeating
155  if(in.get(ch))
156  {
157  if(ch=='"')
158  {
159  }
160  else
161  {
162  in.unget();
163  return; // done
164  }
165  }
166  else
167  return; // done
168  }
169  buffer+=ch;
170  }
171 
172  // Hmpf. Eof before end of string literal. This is an error.
173  error("EOF within string literal");
174 }
175 
177 {
178  char ch;
179  unsigned open_parentheses=0;
180 
181  while(in.get(ch))
182  {
183  switch(ch)
184  {
185  case ' ':
186  case '\n':
187  case '\r':
188  case '\t':
189  case static_cast<char>(160): // non-breaking space
190  // skip any whitespace
191  break;
192 
193  case ';': // comment
194  // skip until newline
195  while(in.get(ch) && ch!='\n')
196  {
197  // ignore
198  }
199  break;
200 
201  case '(':
202  // produce sub-expression
203  open_parentheses++;
204  open_expression();
205  break;
206 
207  case ')':
208  // done with sub-expression
209  if(open_parentheses==0) // unexpected ')'. This is an error.
210  {
211  error("unexpected closing parenthesis");
212  return;
213  }
214 
215  open_parentheses--;
216 
218 
219  if(open_parentheses==0)
220  return; // done
221 
222  break;
223 
224  case '|': // quoted symbol
226  symbol();
227  if(open_parentheses==0)
228  return; // done
229  break;
230 
231  case '"': // string literal
233  string_literal();
234  if(open_parentheses==0)
235  return; // done
236  break;
237 
238  case ':': // keyword
240  keyword();
241  if(open_parentheses==0)
242  return; // done
243  break;
244 
245  case '#':
246  if(in.get(ch))
247  {
248  if(ch=='b')
249  {
250  get_bin_numeral();
251  numeral();
252  }
253  else if(ch=='x')
254  {
255  get_hex_numeral();
256  numeral();
257  }
258  else
259  {
260  error("unexpected numeral token");
261  return;
262  }
263 
264  if(open_parentheses==0)
265  return; // done
266  }
267  else
268  {
269  error("unexpected EOF in numeral token");
270  return;
271  }
272  break;
273 
274  default: // likely a simple symbol or a numeral
275  if(isdigit(ch))
276  {
277  in.unget();
279  numeral();
280  if(open_parentheses==0)
281  return; // done
282  }
283  else if(is_simple_symbol_character(ch))
284  {
285  in.unget();
287  symbol();
288  if(open_parentheses==0)
289  return; // done
290  }
291  else
292  {
293  // illegal character, error
294  error("unexpected character");
295  return;
296  }
297  }
298  }
299 
300  if(open_parentheses==0)
301  {
302  // Hmpf, eof before we got anything. Blank file!
303  }
304  else
305  {
306  // Eof before end of expression. Error!
307  error("EOF before end of expression");
308  }
309 }
virtual void symbol()=0
virtual void keyword()=0
virtual void numeral()=0
std::istream & in
Definition: smt2_parser.h:26
void get_decimal_numeral()
Definition: smt2_parser.cpp:52
std::string buffer
Definition: smt2_parser.h:27
void get_simple_symbol()
Definition: smt2_parser.cpp:27
virtual void open_expression()=0
void get_quoted_symbol()
void get_string_literal()
virtual void error(const std::string &)=0
void get_hex_numeral()
void operator()()
void get_bin_numeral()
Definition: smt2_parser.cpp:75
virtual void close_expression()=0
bool is_simple_symbol_character(char ch)
Definition: smt2_parser.cpp:14
virtual void string_literal()=0