cprover
|
#include <smt2_parser.h>
Classes | |
struct | idt |
struct | named_termt |
struct | signature_with_parameter_idst |
Public Types | |
using | id_mapt = std::map< irep_idt, idt > |
using | named_termst = std::map< irep_idt, named_termt > |
Public Member Functions | |
smt2_parsert (std::istream &_in) | |
bool | parse () override |
void | skip_to_end_of_list () |
This skips tokens until all bracketed expressions are closed. More... | |
![]() | |
smt2_tokenizert (std::istream &_in) | |
![]() | |
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 |
named_termst | named_terms |
bool | exit |
![]() | |
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, STRING_LITERAL, NUMERAL, SYMBOL, KEYWORD, OPEN, CLOSE } |
Protected Attributes | |
std::size_t | parenthesis_level |
renaming_mapt | renaming_map |
renaming_counterst | renaming_counters |
![]() | |
std::string | buffer |
bool | quoted_symbol = false |
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.
using smt2_parsert::named_termst = std::map<irep_idt, named_termt> |
Definition at line 52 of file smt2_parser.h.
|
protected |
Definition at line 72 of file smt2_parser.h.
|
protected |
Definition at line 70 of file smt2_parser.h.
|
inlineexplicit |
Definition at line 21 of file smt2_parser.h.
|
protected |
Definition at line 379 of file smt2_parser.cpp.
|
protected |
Definition at line 355 of file smt2_parser.cpp.
|
protected |
Apply typecast to signedbv to expressions in vector.
Definition at line 299 of file smt2_parser.cpp.
Apply typecast to unsignedbv to given expression.
Definition at line 322 of file smt2_parser.cpp.
|
protectedvirtual |
Reimplemented in smt2_solvert.
Definition at line 1164 of file smt2_parser.cpp.
|
protected |
Definition at line 38 of file smt2_parser.cpp.
|
protected |
Definition at line 912 of file smt2_parser.cpp.
|
protected |
Definition at line 448 of file smt2_parser.cpp.
|
protected |
Definition at line 276 of file smt2_parser.cpp.
|
protected |
Definition at line 419 of file smt2_parser.cpp.
|
protected |
Definition at line 390 of file smt2_parser.cpp.
|
protected |
Definition at line 1130 of file smt2_parser.cpp.
|
protected |
Definition at line 1087 of file smt2_parser.cpp.
Definition at line 119 of file smt2_parser.cpp.
|
protected |
Definition at line 78 of file smt2_parser.cpp.
|
protected |
Definition at line 149 of file smt2_parser.cpp.
|
protected |
Definition at line 334 of file smt2_parser.cpp.
|
overrideprotectedvirtual |
Reimplemented from smt2_tokenizert.
Definition at line 19 of file smt2_parser.cpp.
|
protected |
Definition at line 107 of file smt2_parser.cpp.
|
inlineoverridevirtual |
Implements parsert.
Definition at line 26 of file smt2_parser.h.
Definition at line 218 of file smt2_parser.cpp.
Definition at line 139 of file smt2_parser.cpp.
void smt2_parsert::skip_to_end_of_list | ( | ) |
This skips tokens until all bracketed expressions are closed.
Definition at line 31 of file smt2_parser.cpp.
|
protected |
Definition at line 1003 of file smt2_parser.cpp.
|
protected |
Definition at line 371 of file smt2_parser.cpp.
bool smt2_parsert::exit |
Definition at line 55 of file smt2_parser.h.
id_mapt smt2_parsert::id_map |
Definition at line 44 of file smt2_parser.h.
named_termst smt2_parsert::named_terms |
Definition at line 53 of file smt2_parser.h.
|
protected |
Definition at line 62 of file smt2_parser.h.
|
protected |
Definition at line 73 of file smt2_parser.h.
|
protected |
Definition at line 71 of file smt2_parser.h.