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
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:74
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
smt2_tokenizert::tokent
enum { NONE, END_OF_FILE, STRING_LITERAL, NUMERAL, SYMBOL, KEYWORD, OPEN, CLOSE } tokent
Definition: smt2_tokenizer.h:73
smt2_tokenizert::peek
tokent peek()
Definition: smt2_tokenizer.h:78
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:36
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:30
smt2_tokenizert::peeked
bool peeked
Definition: smt2_tokenizer.h:63
smt2_tokenizert::error
smt2_errort error()
generate an error exception
Definition: smt2_tokenizer.h:101
parsert::in
std::istream * in
Definition: parser.h:26
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:21
CLOSE
#define CLOSE
Definition: xml_y.tab.cpp:155
parsert::line_no
unsigned line_no
Definition: parser.h:136
smt2_tokenizert::smt2_errort::message
std::ostringstream message
Definition: smt2_tokenizer.h:56
STRING_LITERAL
#define STRING_LITERAL
Definition: ansi_c_lex.yy.cpp:4406
parsert
Definition: parser.h:23
smt2_tokenizert::smt2_errort::get_line_no
unsigned get_line_no() const
Definition: smt2_tokenizer.h:45
smt2_tokenizert::buffer
std::string buffer
Definition: smt2_tokenizer.h:61
smt2_tokenizert::smt2_errort::line_no
unsigned line_no
Definition: smt2_tokenizer.h:57
smt2_tokenizert::get_hex_numeral
tokent get_hex_numeral()
Definition: smt2_tokenizer.cpp:115
parser.h
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:50
smt2_tokenizert::get_decimal_numeral
tokent get_decimal_numeral()
Definition: smt2_tokenizer.cpp:59
smt2_tokenizert::next_token
virtual tokent next_token()
Definition: smt2_tokenizer.cpp:203
smt2_tokenizert::quoted_symbol
bool quoted_symbol
Definition: smt2_tokenizer.h:62
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:122
smt2_tokenizert::smt2_errort::what
std::string what() const override
A human readable description of what went wrong.
Definition: smt2_tokenizer.h:40
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:24
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