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/exception_utils.h>
13 #include <util/parser.h>
14 
15 #include <sstream>
16 #include <string>
17 
19 {
20 public:
21  explicit smt2_tokenizert(std::istream &_in) : peeked(false), token(NONE)
22  {
23  in=&_in;
24  line_no=1;
25  }
26 
28  {
29  public:
30  smt2_errort(const std::string &_message, unsigned _line_no)
31  : line_no(_line_no)
32  {
33  message << _message;
34  }
35 
36  explicit smt2_errort(unsigned _line_no) : line_no(_line_no)
37  {
38  }
39 
40  std::string what() const override
41  {
42  return message.str();
43  }
44 
45  unsigned get_line_no() const
46  {
47  return line_no;
48  }
49 
50  std::ostringstream &message_ostream()
51  {
52  return message;
53  }
54 
55  protected:
56  std::ostringstream message;
57  unsigned line_no;
58  };
59 
60 protected:
61  std::string buffer;
62  bool quoted_symbol = false;
63  bool peeked;
64  using tokent = enum {
65  NONE,
66  END_OF_FILE,
68  NUMERAL,
69  SYMBOL,
70  KEYWORD,
71  OPEN,
72  CLOSE
73  };
75 
76  virtual tokent next_token();
77 
79  {
80  if(peeked)
81  return token;
82  else
83  {
85  peeked=true;
86  return token;
87  }
88  }
89 
92  void skip_to_end_of_list();
93 
95  smt2_errort error(const std::string &message)
96  {
97  return smt2_errort(message, line_no);
98  }
99 
102  {
103  return smt2_errort(line_no);
104  }
105 
106 private:
113  static bool is_simple_symbol_character(char);
114 
116  void get_token_from_stream();
117 };
118 
120 template <typename T>
123 {
124  e.message_ostream() << message;
125  return std::move(e);
126 }
127 
128 #endif // CPROVER_SOLVERS_SMT2_SMT2_PARSER_H
void skip_to_end_of_list()
skip any tokens until all parentheses are closed or the end of file is reached
unsigned get_line_no() const
void get_token_from_stream()
read a token from the input stream and store it in 'token'
std::istream * in
Definition: parser.h:26
tokent get_decimal_numeral()
smt2_tokenizert::smt2_errort operator<<(smt2_tokenizert::smt2_errort &&e, const T &message)
add to the diagnostic information in the given smt2_tokenizer exception
smt2_errort error(const std::string &message)
generate an error exception, pre-filled with a message
std::string what() const override
A human readable description of what went wrong.
Definition: parser.h:23
tokent get_bin_numeral()
smt2_tokenizert(std::istream &_in)
smt2_errort(unsigned _line_no)
tokent get_hex_numeral()
Parser utilities.
tokent get_string_literal()
Base class for exceptions thrown in the cprover project.
static bool is_simple_symbol_character(char)
std::ostringstream & message_ostream()
enum { NONE, END_OF_FILE, STRING_LITERAL, NUMERAL, SYMBOL, KEYWORD, OPEN, CLOSE } tokent
#define STRING_LITERAL
tokent get_quoted_symbol()
unsigned line_no
Definition: parser.h:136
smt2_errort(const std::string &_message, unsigned _line_no)
std::string buffer
#define CLOSE
Definition: xml_y.tab.cpp:155
smt2_errort error()
generate an error exception
std::ostringstream message
tokent get_simple_symbol()
virtual tokent next_token()