cprover
smt2_tokenizer.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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
13
14#include <sstream>
15#include <string>
16
18{
19public:
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) const
96 {
97 return smt2_errort(message, line_no);
98 }
99
102 {
103 return smt2_errort(line_no);
104 }
105
106protected:
107 std::istream *in;
108 unsigned line_no;
109 std::string buffer;
110 bool quoted_symbol = false;
111 bool peeked;
113
117
118private:
125 static bool is_simple_symbol_character(char);
126
129};
130
132template <typename T>
134operator<<(smt2_tokenizert::smt2_errort &&e, const T &message)
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
std::ostringstream & message_ostream()
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()
enum { NONE, END_OF_FILE, STRING_LITERAL, NUMERAL, SYMBOL, KEYWORD, OPEN, CLOSE } tokent
smt2_tokenizert(std::istream &_in)
std::istream * in
smt2_errort error() const
generate an error exception
tokent get_bin_numeral()
tokent get_simple_symbol()
tokent get_quoted_symbol()
const std::string & get_buffer() const
static bool is_simple_symbol_character(char)
smt2_errort error(const std::string &message) const
generate an error exception, pre-filled with a message
bool token_is_quoted_symbol() const
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