cprover
|
#include <smt2_parser.h>
Classes | |
struct | idt |
Public Types | |
using | id_mapt = std::map< irep_idt, idt > |
Public Member Functions | |
smt2_parsert (std::istream &_in) | |
bool | parse () override |
![]() | |
smt2_tokenizert (std::istream &_in) | |
operator bool () | |
![]() | |
virtual void | clear () |
parsert () | |
virtual | ~parsert () |
bool | read (char &ch) |
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) |
Public Attributes | |
id_mapt | id_map |
![]() | |
std::istream * | in |
std::string | this_line |
std::string | last_line |
std::vector< exprt > | stack |
Protected Types | |
using | renaming_mapt = std::map< irep_idt, irep_idt > |
using | renaming_counterst = std::map< irep_idt, unsigned > |
![]() | |
using | tokent = enum { NONE, END_OF_FILE, ERROR, STRING_LITERAL, NUMERAL, SYMBOL, OPEN, CLOSE } |
Protected Attributes | |
bool | exit |
renaming_mapt | renaming_map |
renaming_counterst | renaming_counters |
![]() | |
std::string | buffer |
bool | ok |
bool | peeked |
tokent | token |
![]() | |
source_locationt | source_location |
unsigned | line_no |
unsigned | previous_line_no |
unsigned | column |
Additional Inherited Members |
Definition at line 18 of file smt2_parser.h.
using smt2_parsert::id_mapt = std::map<irep_idt, idt> |
Definition at line 43 of file smt2_parser.h.
|
protected |
Definition at line 55 of file smt2_parser.h.
|
protected |
Definition at line 53 of file smt2_parser.h.
|
inlineexplicit |
Definition at line 21 of file smt2_parser.h.
|
protected |
Definition at line 414 of file smt2_parser.cpp.
References messaget::eom(), and smt2_tokenizert::error().
Referenced by function_application().
|
protected |
Definition at line 381 of file smt2_parser.cpp.
References messaget::eom(), and smt2_tokenizert::error().
Referenced by function_application().
|
protected |
Apply typecast to signedbv to expressions in vector.
Definition at line 316 of file smt2_parser.cpp.
References messaget::eom(), smt2_tokenizert::error(), messaget::result(), and to_unsignedbv_type().
Referenced by function_application().
Apply typecast to unsignedbv to given expression.
Definition at line 339 of file smt2_parser.cpp.
References messaget::eom(), smt2_tokenizert::error(), irept::id(), to_signedbv_type(), and exprt::type().
Referenced by function_application().
|
protectedvirtual |
Reimplemented in smt2_solvert.
Definition at line 1099 of file smt2_parser.cpp.
References smt2_tokenizert::buffer, messaget::eom(), smt2_tokenizert::error(), exit, expression(), function_signature_declaration(), function_signature_definition(), id_map, ignore_command(), smt2_tokenizert::next_token(), and sort().
Referenced by smt2_solvert::command(), and command_sequence().
|
protected |
Definition at line 13 of file smt2_parser.cpp.
References smt2_tokenizert::buffer, CLOSE, command(), messaget::eom(), smt2_tokenizert::error(), exit, smt2_tokenizert::next_token(), and smt2_tokenizert::token.
Referenced by parse().
|
protected |
Definition at line 864 of file smt2_parser.cpp.
References smt2_tokenizert::buffer, CHECK_RETURN, messaget::eom(), smt2_tokenizert::error(), from_integer(), function_application(), id_map, smt2_tokenizert::next_token(), rename_id(), and string2integer().
Referenced by smt2_solvert::command(), command(), function_application(), let_expression(), operands(), and quantifier_expression().
|
protected |
Definition at line 433 of file smt2_parser.cpp.
References function_application_exprt::arguments(), binary(), binary_predicate(), smt2_tokenizert::buffer, cast_bv_to_signed(), cast_bv_to_unsigned(), CLOSE, mathematical_function_typet::codomain(), messaget::eom(), smt2_tokenizert::error(), expression(), from_integer(), function_application_exprt::function(), bitvector_typet::get_width(), has_prefix(), id_map, let_expression(), multi_ary(), smt2_tokenizert::next_token(), operands(), smt2_tokenizert::peek(), quantifier_expression(), rename_id(), string2integer(), to_mathematical_function_type(), to_unsignedbv_type(), exprt::type(), and unary().
Referenced by expression().
|
protected |
Definition at line 282 of file smt2_parser.cpp.
References messaget::eom(), smt2_tokenizert::error(), id_map, and messaget::result().
|
protected |
Definition at line 1051 of file smt2_parser.cpp.
References CLOSE, messaget::eom(), smt2_tokenizert::error(), smt2_tokenizert::next_token(), smt2_tokenizert::peek(), sort(), and mathematical_function_typet::variablet::type().
Referenced by command().
|
protected |
Definition at line 997 of file smt2_parser.cpp.
References smt2_tokenizert::buffer, CLOSE, messaget::eom(), smt2_tokenizert::error(), id_map, smt2_tokenizert::next_token(), smt2_tokenizert::peek(), mathematical_function_typet::variablet::set_identifier(), sort(), and mathematical_function_typet::variablet::type().
Referenced by command().
Definition at line 94 of file smt2_parser.cpp.
References id2string(), id_map, renaming_counters, renaming_map, and to_string().
Referenced by let_expression().
|
protected |
Definition at line 53 of file smt2_parser.cpp.
References CLOSE, messaget::eom(), smt2_tokenizert::error(), smt2_tokenizert::next_token(), and smt2_tokenizert::peek().
Referenced by command().
|
protected |
Definition at line 124 of file smt2_parser.cpp.
References smt2_tokenizert::buffer, CLOSE, messaget::eom(), smt2_tokenizert::error(), expression(), get_fresh_id(), id_map, smt2_tokenizert::next_token(), smt2_tokenizert::peek(), renaming_map, messaget::result(), irept::swap(), let_exprt::symbol(), exprt::type(), let_exprt::value(), and let_exprt::where().
Referenced by function_application().
|
protected |
Definition at line 354 of file smt2_parser.cpp.
References messaget::eom(), smt2_tokenizert::error(), and messaget::result().
Referenced by function_application().
|
protected |
Definition at line 82 of file smt2_parser.cpp.
References CLOSE, expression(), smt2_tokenizert::next_token(), smt2_tokenizert::peek(), and messaget::result().
Referenced by function_application().
|
inlineoverridevirtual |
Implements parsert.
Definition at line 27 of file smt2_parser.h.
References command_sequence(), and smt2_tokenizert::ok.
Referenced by solver().
Definition at line 209 of file smt2_parser.cpp.
References smt2_tokenizert::buffer, CLOSE, messaget::eom(), smt2_tokenizert::error(), expression(), id_map, smt2_tokenizert::next_token(), exprt::op0(), exprt::op1(), smt2_tokenizert::peek(), messaget::result(), sort(), and irept::swap().
Referenced by function_application().
Definition at line 114 of file smt2_parser.cpp.
References renaming_map.
Referenced by expression(), and function_application().
|
protected |
Definition at line 927 of file smt2_parser.cpp.
References smt2_tokenizert::buffer, CLOSE, messaget::eom(), smt2_tokenizert::error(), and smt2_tokenizert::next_token().
Referenced by smt2_solvert::command(), command(), function_signature_declaration(), function_signature_definition(), and quantifier_expression().
|
protected |
Definition at line 403 of file smt2_parser.cpp.
References messaget::eom(), and smt2_tokenizert::error().
Referenced by function_application().
|
protected |
Definition at line 47 of file smt2_parser.h.
Referenced by smt2_solvert::command(), command(), and command_sequence().
id_mapt smt2_parsert::id_map |
Definition at line 44 of file smt2_parser.h.
Referenced by command(), smt2_solvert::define_constants(), smt2_solvert::expand_function_applications(), expression(), function_application(), function_signature_definition(), get_fresh_id(), let_expression(), and quantifier_expression().
|
protected |
Definition at line 56 of file smt2_parser.h.
Referenced by get_fresh_id().
|
protected |
Definition at line 54 of file smt2_parser.h.
Referenced by get_fresh_id(), let_expression(), and rename_id().