CBMC
|
Public Member Functions | |
smt2_solvert (std::istream &_in, stack_decision_proceduret &_solver) | |
![]() | |
smt2_parsert (std::istream &_in) | |
void | parse () |
smt2_tokenizert::smt2_errort | error (const std::string &message) const |
smt2_tokenizert::smt2_errort | error () const |
void | skip_to_end_of_list () |
This skips tokens until all bracketed expressions are closed. | |
Protected Types | |
enum | { NOT_SOLVED , SAT , UNSAT } |
Protected Attributes | |
stack_decision_proceduret & | solver |
std::set< irep_idt > | constants_done |
enum smt2_solvert:: { ... } | status |
![]() | |
smt2_tokenizert | smt2_tokenizer |
std::size_t | parenthesis_level |
std::unordered_map< std::string, std::function< exprt()> > | expressions |
std::unordered_map< std::string, std::function< typet()> > | sorts |
std::unordered_map< std::string, std::function< void()> > | commands |
Additional Inherited Members | |
![]() | |
using | id_mapt = std::map< irep_idt, idt > |
using | named_termst = std::map< irep_idt, named_termt > |
![]() | |
id_mapt | id_map |
named_termst | named_terms |
bool | exit |
Definition at line 23 of file smt2_solver.cpp.
Enumerator | |
---|---|
NOT_SOLVED | |
SAT | |
UNSAT |
Definition at line 41 of file smt2_solver.cpp.
|
inline |
Definition at line 26 of file smt2_solver.cpp.
|
protected |
Definition at line 49 of file smt2_solver.cpp.
Definition at line 74 of file smt2_solver.cpp.
|
protected |
Definition at line 119 of file smt2_solver.cpp.
|
protected |
Definition at line 39 of file smt2_solver.cpp.
|
protected |
Definition at line 33 of file smt2_solver.cpp.
enum { ... } smt2_solvert::status |