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 
14 #include <sstream>
15 #include <string>
16 
18 {
19 public:
20  explicit smt2_tokenizert(std::istream &_in) : peeked(false), token(NONE)
21  {
22  in=&_in;
23  line_no=1;
24  }
25 
27  {
28  public:
29  smt2_errort(const std::string &_message, unsigned _line_no)
30  : line_no(_line_no)
31  {
32  message << _message;
33  }
34 
35  explicit smt2_errort(unsigned _line_no) : line_no(_line_no)
36  {
37  }
38 
39  std::string what() const override
40  {
41  return message.str();
42  }
43 
44  unsigned get_line_no() const
45  {
46  return line_no;
47  }
48 
49  std::ostringstream &message_ostream()
50  {
51  return message;
52  }
53 
54  protected:
55  std::ostringstream message;
56  unsigned line_no;
57  };
58 
59  using tokent = enum {
60  NONE,
61  END_OF_FILE,
62  STRING_LITERAL,
63  NUMERAL,
64  SYMBOL,
65  KEYWORD,
66  OPEN,
67  CLOSE
68  };
69 
71 
73  {
74  if(peeked)
75  return token;
76  else
77  {
79  peeked=true;
80  return token;
81  }
82  }
83 
84  const std::string &get_buffer() const
85  {
86  return buffer;
87  }
88 
90  {
91  return quoted_symbol;
92  }
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 protected:
107  std::istream *in;
108  unsigned line_no;
109  std::string buffer;
110  bool quoted_symbol = false;
111  bool peeked;
113 
117 
118 private:
125  static bool is_simple_symbol_character(char);
126 
128  void get_token_from_stream();
129 };
130 
132 template <typename T>
135 {
136  e.message_ostream() << message;
137  return std::move(e);
138 }
139 
140 #endif // CPROVER_SOLVERS_SMT2_SMT2_PARSER_H
Base class for exceptions thrown in the cprover project.
std::string what() const override
A human readable description of what went wrong.
smt2_errort(const std::string &_message, unsigned _line_no)
std::ostringstream & message_ostream()
std::ostringstream message
unsigned get_line_no() const
smt2_errort(unsigned _line_no)
void get_token_from_stream()
read a token from the input stream and store it in 'token'
tokent get_string_literal()
tokent get_decimal_numeral()
smt2_errort error(const std::string &message)
generate an error exception, pre-filled with a message
enum { NONE, END_OF_FILE, STRING_LITERAL, NUMERAL, SYMBOL, KEYWORD, OPEN, CLOSE } tokent
const std::string & get_buffer() const
smt2_tokenizert(std::istream &_in)
std::istream * in
tokent get_bin_numeral()
tokent get_simple_symbol()
tokent get_quoted_symbol()
static bool is_simple_symbol_character(char)
bool token_is_quoted_symbol() const
smt2_errort error()
generate an error exception
std::string buffer
void skip_to_end_of_list()
skip any tokens until all parentheses are closed or the end of file is reached
tokent get_hex_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
static const char * message(const statust &status)
Makes a status message string from a status.