cprover
Loading...
Searching...
No Matches
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.

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, exprtbinding (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.
exprt cast_bv_to_unsigned (const exprt &)
 Apply typecast to unsignedbv to given expression.
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_proceduretsolver
std::set< irep_idtconstants_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: