cprover
|
Public Member Functions | |
smt2_solvert (std::istream &_in, decision_proceduret &_solver) | |
![]() | |
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) |
Protected Attributes | |
decision_proceduret & | solver |
std::set< irep_idt > | constants_done |
![]() | |
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 | |
![]() | |
using | id_mapt = std::map< irep_idt, idt > |
![]() | |
id_mapt | id_map |
![]() | |
std::istream * | in |
std::string | this_line |
std::string | last_line |
std::vector< exprt > | stack |
![]() | |
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 } |
Definition at line 23 of file smt2_solver.cpp.
|
inline |
Definition at line 26 of file smt2_solver.cpp.
|
overrideprotectedvirtual |
Reimplemented from smt2_parsert.
Definition at line 123 of file smt2_solver.cpp.
References smt2_parsert::command(), decision_proceduret::D_ERROR, decision_proceduret::D_SATISFIABLE, decision_proceduret::D_UNSATISFIABLE, define_constants(), smt2_tokenizert::error(), smt2_parsert::exit, expand_function_applications(), smt2_parsert::expression(), irept::is_not_nil(), irept::pretty(), decision_proceduret::set_to_true(), simplify_expr(), solver, and smt2_parsert::sort().
|
protected |
Definition at line 44 of file smt2_solver.cpp.
References constants_done, expand_function_applications(), symbol_exprt::get_identifier(), irept::id(), smt2_parsert::id_map, exprt::operands(), decision_proceduret::set_to_true(), solver, and to_symbol_expr().
Referenced by command().
|
protected |
Definition at line 77 of file smt2_solver.cpp.
References DATA_INVARIANT, irept::id(), smt2_parsert::id_map, exprt::operands(), to_function_application_expr(), and to_mathematical_function_type().
Referenced by command(), and define_constants().
|
protected |
Definition at line 41 of file smt2_solver.cpp.
Referenced by define_constants().
|
protected |
Definition at line 35 of file smt2_solver.cpp.
Referenced by command(), and define_constants().