cprover
smt2_tokenizer.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_SOLVERS_SMT2_SMT2_TOKENIZER_H
10 #define CPROVER_SOLVERS_SMT2_SMT2_TOKENIZER_H
11 
12 #include <util/parser.h>
13 
14 #include <string>
15 
17 {
18 public:
19  explicit smt2_tokenizert(std::istream &_in):
20  ok(true), peeked(false), token(NONE)
21  {
22  in=&_in;
23  line_no=1;
24  }
25 
26  operator bool()
27  {
28  return ok;
29  }
30 
31 protected:
32  std::string buffer;
33  bool ok, peeked;
34  using tokent=enum { NONE, END_OF_FILE, ERROR, STRING_LITERAL,
35  NUMERAL, SYMBOL, OPEN, CLOSE };
37 
39 
41  {
42  if(peeked)
43  return token;
44  else
45  {
46  next_token();
47  peeked=true;
48  return token;
49  }
50  }
51 
53  {
54  ok=false;
56  return messaget::error();
57  }
58 
59 private:
66  static bool is_simple_symbol_character(char);
67 };
68 
69 #endif // CPROVER_SOLVERS_SMT2_SMT2_PARSER_H
std::istream * in
Definition: parser.h:26
tokent get_decimal_numeral()
Definition: parser.h:23
tokent get_bin_numeral()
smt2_tokenizert(std::istream &_in)
tokent get_hex_numeral()
Parser utilities.
enum { NONE, END_OF_FILE, ERROR, STRING_LITERAL, NUMERAL, SYMBOL, OPEN, CLOSE } tokent
source_locationt source_location
Definition: message.h:214
tokent get_string_literal()
mstreamt & error() const
Definition: message.h:302
void set_line(const irep_idt &line)
static bool is_simple_symbol_character(char)
#define STRING_LITERAL
tokent get_quoted_symbol()
unsigned line_no
Definition: parser.h:136
std::string buffer
#define CLOSE
Definition: xml_y.tab.cpp:147
mstreamt & error()
tokent get_simple_symbol()