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
smt2_tokenizert::get_quoted_symbol
tokent get_quoted_symbol()
Definition: smt2_tokenizer.cpp:144
exception_utils.h
smt2_tokenizert::token
tokent token
Definition: smt2_tokenizer.h:112
smt2_tokenizert::skip_to_end_of_list
void skip_to_end_of_list()
skip any tokens until all parentheses are closed or the end of file is reached
complexity_violationt::NONE
@ NONE
smt2_tokenizert::tokent
enum { NONE, END_OF_FILE, STRING_LITERAL, NUMERAL, SYMBOL, KEYWORD, OPEN, CLOSE } tokent
Definition: smt2_tokenizer.h:68
smt2_tokenizert::peek
tokent peek()
Definition: smt2_tokenizer.h:72
smt2_tokenizert::get_string_literal
tokent get_string_literal()
Definition: smt2_tokenizer.cpp:172
smt2_tokenizert::smt2_errort::smt2_errort
smt2_errort(unsigned _line_no)
Definition: smt2_tokenizer.h:35
smt2_tokenizert::error
smt2_errort error(const std::string &message)
generate an error exception, pre-filled with a message
Definition: smt2_tokenizer.h:95
smt2_tokenizert
Definition: smt2_tokenizer.h:18
smt2_tokenizert::smt2_errort::smt2_errort
smt2_errort(const std::string &_message, unsigned _line_no)
Definition: smt2_tokenizer.h:29
message
static const char * message(const static_verifier_resultt::statust &status)
Makes a status message string from a status.
Definition: static_verifier.cpp:74
smt2_tokenizert::in
std::istream * in
Definition: smt2_tokenizer.h:107
smt2_tokenizert::peeked
bool peeked
Definition: smt2_tokenizer.h:111
smt2_tokenizert::error
smt2_errort error()
generate an error exception
Definition: smt2_tokenizer.h:101
smt2_tokenizert::get_bin_numeral
tokent get_bin_numeral()
Definition: smt2_tokenizer.cpp:86
smt2_tokenizert::smt2_tokenizert
smt2_tokenizert(std::istream &_in)
Definition: smt2_tokenizer.h:20
smt2_tokenizert::smt2_errort::message
std::ostringstream message
Definition: smt2_tokenizer.h:55
smt2_tokenizert::smt2_errort::get_line_no
unsigned get_line_no() const
Definition: smt2_tokenizer.h:44
smt2_tokenizert::line_no
unsigned line_no
Definition: smt2_tokenizer.h:108
smt2_tokenizert::buffer
std::string buffer
Definition: smt2_tokenizer.h:109
smt2_tokenizert::smt2_errort::line_no
unsigned line_no
Definition: smt2_tokenizer.h:56
smt2_tokenizert::get_hex_numeral
tokent get_hex_numeral()
Definition: smt2_tokenizer.cpp:115
smt2_tokenizert::smt2_errort
Definition: smt2_tokenizer.h:27
smt2_tokenizert::get_simple_symbol
tokent get_simple_symbol()
Definition: smt2_tokenizer.cpp:26
smt2_tokenizert::smt2_errort::message_ostream
std::ostringstream & message_ostream()
Definition: smt2_tokenizer.h:49
smt2_tokenizert::token_is_quoted_symbol
bool token_is_quoted_symbol() const
Definition: smt2_tokenizer.h:89
smt2_tokenizert::get_decimal_numeral
tokent get_decimal_numeral()
Definition: smt2_tokenizer.cpp:59
smt2_tokenizert::next_token
tokent next_token()
Definition: smt2_tokenizer.cpp:203
smt2_tokenizert::quoted_symbol
bool quoted_symbol
Definition: smt2_tokenizer.h:110
operator<<
smt2_tokenizert::smt2_errort operator<<(smt2_tokenizert::smt2_errort &&e, const T &message)
add to the diagnostic information in the given smt2_tokenizer exception
Definition: smt2_tokenizer.h:134
smt2_tokenizert::smt2_errort::what
std::string what() const override
A human readable description of what went wrong.
Definition: smt2_tokenizer.h:39
smt2_tokenizert::get_buffer
const std::string & get_buffer() const
Definition: smt2_tokenizer.h:84
smt2_tokenizert::is_simple_symbol_character
static bool is_simple_symbol_character(char)
Definition: smt2_tokenizer.cpp:13
cprover_exception_baset
Base class for exceptions thrown in the cprover project.
Definition: exception_utils.h:25
smt2_tokenizert::get_token_from_stream
void get_token_from_stream()
read a token from the input stream and store it in 'token'
Definition: smt2_tokenizer.cpp:213