cprover
Loading...
Searching...
No Matches
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
12#include <sstream>
13#include <string>
14
16{
17public:
18 explicit smt2_tokenizert(std::istream &_in) : peeked(false), token(NONE)
19 {
20 in=&_in;
21 line_no=1;
22 }
23
25 {
26 public:
27 smt2_errort(const std::string &_message, unsigned _line_no)
29 {
31 }
32
33 explicit smt2_errort(unsigned _line_no) : line_no(_line_no)
34 {
35 }
36
37 std::string what() const
38 {
39 return message.str();
40 }
41
42 unsigned get_line_no() const
43 {
44 return line_no;
45 }
46
47 std::ostringstream &message_ostream()
48 {
49 return message;
50 }
51
52 protected:
53 std::ostringstream message;
54 unsigned line_no;
55 };
56
57 using tokent = enum {
58 NONE,
61 NUMERAL,
62 SYMBOL,
63 KEYWORD,
64 OPEN,
65 CLOSE
66 };
67
69
71 {
72 if(peeked)
73 return token;
74 else
75 {
77 peeked=true;
78 return token;
79 }
80 }
81
82 const std::string &get_buffer() const
83 {
84 return buffer;
85 }
86
88 {
89 return quoted_symbol;
90 }
91
93 smt2_errort error(const std::string &message) const
94 {
95 return smt2_errort(message, line_no);
96 }
97
100 {
101 return smt2_errort(line_no);
102 }
103
104protected:
105 std::istream *in;
106 unsigned line_no;
107 std::string buffer;
108 bool quoted_symbol = false;
109 bool peeked;
111
115
116private:
123
126};
127
129template <typename T>
131operator<<(smt2_tokenizert::smt2_errort &&e, const T &message)
132{
133 e.message_ostream() << message;
134 return std::move(e);
135}
136
138
139#endif // CPROVER_SOLVERS_SMT2_SMT2_PARSER_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
smt2_errort(const std::string &_message, unsigned _line_no)
std::ostringstream & message_ostream()
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_tokenizert(std::istream &_in)
std::istream * in
smt2_errort error() const
generate an error exception
tokent get_simple_symbol()
enum { NONE, END_OF_FILE, STRING_LITERAL, NUMERAL, SYMBOL, KEYWORD, OPEN, CLOSE } tokent
const std::string & get_buffer() const
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
@ NONE
Do not apply loop contracts.
smt2_tokenizert::smt2_errort operator<<(smt2_tokenizert::smt2_errort &&e, const T &message)
add to the diagnostic information in the given smt2_tokenizer exception
bool is_smt2_simple_symbol_character(char)