cprover
|
Public Member Functions | |
smt2_solvert (std::istream &_in, decision_proceduret &_solver) | |
![]() | |
smt2_parsert (std::istream &_in) | |
void | parse () |
smt2_tokenizert::smt2_errort | error (const std::string &message) |
smt2_tokenizert::smt2_errort | error () |
void | skip_to_end_of_list () |
This skips tokens until all bracketed expressions are closed. More... | |
Protected Types | |
enum | { NOT_SOLVED, SAT, UNSAT } |
![]() | |
using | renaming_mapt = std::map< irep_idt, irep_idt > |
using | renaming_counterst = std::map< irep_idt, unsigned > |
Protected Attributes | |
decision_proceduret & | solver |
std::set< irep_idt > | constants_done |
enum smt2_solvert:: { ... } | status |
![]() | |
smt2_tokenizert | smt2_tokenizer |
std::size_t | parenthesis_level |
renaming_mapt | renaming_map |
renaming_counterst | renaming_counters |
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 25 of file smt2_solver.cpp.
|
protected |
Enumerator | |
---|---|
NOT_SOLVED | |
SAT | |
UNSAT |
Definition at line 43 of file smt2_solver.cpp.
|
inline |
Definition at line 28 of file smt2_solver.cpp.
|
protected |
Definition at line 51 of file smt2_solver.cpp.
|
protected |
Definition at line 76 of file smt2_solver.cpp.
|
protected |
Definition at line 122 of file smt2_solver.cpp.
|
protected |
Definition at line 41 of file smt2_solver.cpp.
|
protected |
Definition at line 35 of file smt2_solver.cpp.
enum { ... } smt2_solvert::status |