CBMC
Public Member Functions | Protected Types | Protected Member Functions | Protected Attributes | List of all members
smt2_solvert Class Reference
+ Inheritance diagram for smt2_solvert:
+ Collaboration diagram for smt2_solvert:

Public Member Functions

 smt2_solvert (std::istream &_in, stack_decision_proceduret &_solver)
 
- Public Member Functions inherited from smt2_parsert
 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. More...
 

Protected Types

enum  { NOT_SOLVED , SAT , UNSAT }
 

Protected Member Functions

void setup_commands ()
 
void define_constants ()
 
void expand_function_applications (exprt &)
 
- Protected Member Functions inherited from smt2_parsert
smt2_tokenizert::tokent next_token ()
 
void add_unique_id (irep_idt, exprt)
 
void setup_expressions ()
 
exprt expression ()
 
exprt function_application ()
 
exprt function_application_ieee_float_op (const irep_idt &, const exprt::operandst &)
 
exprt function_application_ieee_float_eq (const exprt::operandst &)
 
exprt function_application_fp (const exprt::operandst &)
 
exprt::operandst operands ()
 
typet function_signature_declaration ()
 
signature_with_parameter_idst function_signature_definition ()
 
void check_matching_operand_types (const exprt::operandst &) const
 
exprt multi_ary (irep_idt, const exprt::operandst &)
 
exprt binary_predicate (irep_idt, const exprt::operandst &)
 
exprt binary (irep_idt, const exprt::operandst &)
 
exprt unary (irep_idt, const exprt::operandst &)
 
exprt bv_division (const exprt::operandst &, bool is_signed)
 
exprt bv_mod (const exprt::operandst &, bool is_signed)
 
std::pair< binding_exprt::variablest, exprt > binding (irep_idt)
 
exprt lambda_expression ()
 
exprt let_expression ()
 
exprt quantifier_expression (irep_idt)
 
exprt function_application (const symbol_exprt &function, const exprt::operandst &op)
 
exprt::operandst cast_bv_to_signed (const exprt::operandst &)
 Apply typecast to signedbv to expressions in vector. More...
 
exprt cast_bv_to_unsigned (const exprt &)
 Apply typecast to unsignedbv to given expression. More...
 
typet sort ()
 
typet function_sort ()
 
void setup_sorts ()
 
void command_sequence ()
 
void command (const std::string &)
 
void ignore_command ()
 
void setup_commands ()
 

Protected Attributes

stack_decision_proceduret & solver
 
std::set< irep_idt > constants_done
 
enum smt2_solvert:: { ... }  status
 
- Protected Attributes inherited from smt2_parsert
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

- Public Types inherited from smt2_parsert
using id_mapt = std::map< irep_idt, idt >
 
using named_termst = std::map< irep_idt, named_termt >
 
- Public Attributes inherited from smt2_parsert
id_mapt id_map
 
named_termst named_terms
 
bool exit
 

Detailed Description

Definition at line 23 of file smt2_solver.cpp.

Member Enumeration Documentation

◆ anonymous enum

anonymous enum
protected
Enumerator
NOT_SOLVED 
SAT 
UNSAT 

Definition at line 41 of file smt2_solver.cpp.

Constructor & Destructor Documentation

◆ smt2_solvert()

smt2_solvert::smt2_solvert ( std::istream &  _in,
stack_decision_proceduret &  _solver 
)
inline

Definition at line 26 of file smt2_solver.cpp.

Member Function Documentation

◆ define_constants()

void smt2_solvert::define_constants ( )
protected

Definition at line 49 of file smt2_solver.cpp.

◆ expand_function_applications()

void smt2_solvert::expand_function_applications ( exprt &  expr)
protected

Definition at line 74 of file smt2_solver.cpp.

◆ setup_commands()

void smt2_solvert::setup_commands ( )
protected

Definition at line 119 of file smt2_solver.cpp.

Member Data Documentation

◆ constants_done

std::set<irep_idt> smt2_solvert::constants_done
protected

Definition at line 39 of file smt2_solver.cpp.

◆ solver

stack_decision_proceduret& smt2_solvert::solver
protected

Definition at line 33 of file smt2_solver.cpp.

◆ 

enum { ... } smt2_solvert::status
The documentation for this class was generated from the following file: