cprover
|
#include <smt2_tokenizer.h>
Public Member Functions | |
smt2_tokenizert (std::istream &_in) | |
operator bool () | |
![]() | |
virtual void | clear () |
parsert () | |
virtual | ~parsert () |
bool | read (char &ch) |
virtual bool | parse ()=0 |
bool | eof () |
void | parse_error (const std::string &message, const std::string &before) |
void | inc_line_no () |
void | set_line_no (unsigned _line_no) |
void | set_file (const irep_idt &file) |
irep_idt | get_file () const |
unsigned | get_line_no () const |
unsigned | get_column () const |
void | set_column (unsigned _column) |
void | set_source_location (exprt &e) |
void | set_function (const irep_idt &function) |
void | advance_column (unsigned token_width) |
Protected Types | |
using | tokent = enum { NONE, END_OF_FILE, ERROR, STRING_LITERAL, NUMERAL, SYMBOL, OPEN, CLOSE } |
Protected Member Functions | |
tokent | next_token () |
tokent | peek () |
mstreamt & | error () |
Protected Attributes | |
std::string | buffer |
bool | ok |
bool | peeked |
tokent | token |
![]() | |
source_locationt | source_location |
unsigned | line_no |
unsigned | previous_line_no |
unsigned | column |
Private Member Functions | |
tokent | get_decimal_numeral () |
tokent | get_hex_numeral () |
tokent | get_bin_numeral () |
tokent | get_simple_symbol () |
tokent | get_quoted_symbol () |
tokent | get_string_literal () |
Static Private Member Functions | |
static bool | is_simple_symbol_character (char) |
Additional Inherited Members | |
![]() | |
std::istream * | in |
std::string | this_line |
std::string | last_line |
std::vector< exprt > | stack |
Definition at line 16 of file smt2_tokenizer.h.
|
protected |
Definition at line 35 of file smt2_tokenizer.h.
|
inlineexplicit |
Definition at line 19 of file smt2_tokenizer.h.
References parsert::in, and parsert::line_no.
|
inlineprotected |
Definition at line 52 of file smt2_tokenizer.h.
References messaget::error(), parsert::line_no, ok, source_locationt::set_line(), and messaget::mstreamt::source_location.
Referenced by smt2_parsert::binary(), smt2_parsert::binary_predicate(), smt2_parsert::cast_bv_to_signed(), smt2_parsert::cast_bv_to_unsigned(), smt2_solvert::command(), smt2_parsert::command(), smt2_parsert::command_sequence(), smt2_parsert::expression(), smt2_parsert::function_application(), smt2_parsert::function_signature_declaration(), smt2_parsert::function_signature_definition(), get_quoted_symbol(), get_string_literal(), smt2_parsert::ignore_command(), smt2_parsert::let_expression(), smt2_parsert::multi_ary(), next_token(), smt2irept::parse(), smt2_parsert::quantifier_expression(), smt2_parsert::sort(), and smt2_parsert::unary().
|
private |
Definition at line 82 of file smt2_tokenizer.cpp.
References buffer, and parsert::in.
Referenced by next_token().
|
private |
Definition at line 55 of file smt2_tokenizer.cpp.
References buffer, and parsert::in.
Referenced by next_token().
|
private |
Definition at line 111 of file smt2_tokenizer.cpp.
References buffer, and parsert::in.
Referenced by next_token().
|
private |
Definition at line 140 of file smt2_tokenizer.cpp.
References buffer, messaget::eom(), error(), parsert::in, and parsert::line_no.
Referenced by next_token().
|
private |
Definition at line 26 of file smt2_tokenizer.cpp.
References buffer, parsert::in, and is_simple_symbol_character().
Referenced by next_token().
|
private |
Definition at line 166 of file smt2_tokenizer.cpp.
References buffer, messaget::eom(), error(), parsert::in, and STRING_LITERAL.
Referenced by next_token().
|
staticprivate |
Definition at line 13 of file smt2_tokenizer.cpp.
Referenced by get_simple_symbol(), and next_token().
|
protected |
Definition at line 198 of file smt2_tokenizer.cpp.
References CLOSE, messaget::eom(), error(), get_bin_numeral(), get_decimal_numeral(), get_hex_numeral(), get_quoted_symbol(), get_simple_symbol(), get_string_literal(), parsert::in, is_simple_symbol_character(), parsert::line_no, peeked, and token.
Referenced by smt2_parsert::command(), smt2_parsert::command_sequence(), smt2_parsert::expression(), smt2_parsert::function_application(), smt2_parsert::function_signature_declaration(), smt2_parsert::function_signature_definition(), smt2_parsert::ignore_command(), smt2_parsert::let_expression(), smt2_parsert::operands(), smt2irept::parse(), peek(), smt2_parsert::quantifier_expression(), and smt2_parsert::sort().
|
inline |
Definition at line 26 of file smt2_tokenizer.h.
References ok.
|
inlineprotected |
Definition at line 40 of file smt2_tokenizer.h.
References next_token(), peeked, and token.
Referenced by smt2_parsert::function_application(), smt2_parsert::function_signature_declaration(), smt2_parsert::function_signature_definition(), smt2_parsert::ignore_command(), smt2_parsert::let_expression(), smt2_parsert::operands(), and smt2_parsert::quantifier_expression().
|
protected |
Definition at line 32 of file smt2_tokenizer.h.
Referenced by smt2_parsert::command(), smt2_parsert::command_sequence(), smt2_parsert::expression(), smt2_parsert::function_application(), smt2_parsert::function_signature_definition(), get_bin_numeral(), get_decimal_numeral(), get_hex_numeral(), get_quoted_symbol(), get_simple_symbol(), get_string_literal(), smt2_parsert::let_expression(), smt2irept::parse(), smt2_parsert::quantifier_expression(), and smt2_parsert::sort().
|
protected |
Definition at line 33 of file smt2_tokenizer.h.
Referenced by error(), operator bool(), and smt2_parsert::parse().
|
protected |
Definition at line 33 of file smt2_tokenizer.h.
Referenced by next_token(), and peek().
|
protected |
Definition at line 36 of file smt2_tokenizer.h.
Referenced by smt2_parsert::command_sequence(), next_token(), and peek().