cprover
Loading...
Searching...
No Matches
sort_based_cast_to_bit_vector_convertert Struct Referencefinal
+ Inheritance diagram for sort_based_cast_to_bit_vector_convertert:
+ Collaboration diagram for sort_based_cast_to_bit_vector_convertert:

Public Member Functions

 sort_based_cast_to_bit_vector_convertert (const smt_termt &from_term, const typet &from_type, const bitvector_typet &to_type)
 
void visit (const smt_bool_sortt &) override
 
void visit (const smt_bit_vector_sortt &) override
 
void visit (const smt_array_sortt &) override
 
- Public Member Functions inherited from smt_sort_const_downcast_visitort

Public Attributes

const smt_termtfrom_term
 
const typetfrom_type
 
const bitvector_typetto_type
 
std::optional< smt_termtresult
 

Detailed Description

Definition at line 203 of file convert_expr_to_smt.cpp.

Constructor & Destructor Documentation

◆ sort_based_cast_to_bit_vector_convertert()

sort_based_cast_to_bit_vector_convertert::sort_based_cast_to_bit_vector_convertert ( const smt_termt & from_term,
const typet & from_type,
const bitvector_typet & to_type )
inline

Definition at line 211 of file convert_expr_to_smt.cpp.

Member Function Documentation

◆ visit() [1/3]

void sort_based_cast_to_bit_vector_convertert::visit ( const smt_array_sortt & )
inlineoverridevirtual

Implements smt_sort_const_downcast_visitort.

Definition at line 235 of file convert_expr_to_smt.cpp.

◆ visit() [2/3]

void sort_based_cast_to_bit_vector_convertert::visit ( const smt_bit_vector_sortt & )
inlineoverridevirtual

Implements smt_sort_const_downcast_visitort.

Definition at line 225 of file convert_expr_to_smt.cpp.

◆ visit() [3/3]

void sort_based_cast_to_bit_vector_convertert::visit ( const smt_bool_sortt & )
inlineoverridevirtual

Implements smt_sort_const_downcast_visitort.

Definition at line 219 of file convert_expr_to_smt.cpp.

Member Data Documentation

◆ from_term

const smt_termt& sort_based_cast_to_bit_vector_convertert::from_term

Definition at line 206 of file convert_expr_to_smt.cpp.

◆ from_type

const typet& sort_based_cast_to_bit_vector_convertert::from_type

Definition at line 207 of file convert_expr_to_smt.cpp.

◆ result

std::optional<smt_termt> sort_based_cast_to_bit_vector_convertert::result

Definition at line 209 of file convert_expr_to_smt.cpp.

◆ to_type

const bitvector_typet& sort_based_cast_to_bit_vector_convertert::to_type

Definition at line 208 of file convert_expr_to_smt.cpp.


The documentation for this struct was generated from the following file: