CBMC
Public Member Functions | Public Attributes | List of all members
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 Attributes

const smt_termt & from_term
 
const typet & from_type
 
const bitvector_typet & to_type
 
std::optional< smt_termt > result
 

Detailed Description

Definition at line 202 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 210 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 &  )
inlineoverride

Definition at line 234 of file convert_expr_to_smt.cpp.

◆ visit() [2/3]

void sort_based_cast_to_bit_vector_convertert::visit ( const smt_bit_vector_sortt &  )
inlineoverride

Definition at line 224 of file convert_expr_to_smt.cpp.

◆ visit() [3/3]

void sort_based_cast_to_bit_vector_convertert::visit ( const smt_bool_sortt &  )
inlineoverride

Definition at line 218 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 205 of file convert_expr_to_smt.cpp.

◆ from_type

const typet& sort_based_cast_to_bit_vector_convertert::from_type

Definition at line 206 of file convert_expr_to_smt.cpp.

◆ result

std::optional<smt_termt> sort_based_cast_to_bit_vector_convertert::result

Definition at line 208 of file convert_expr_to_smt.cpp.

◆ to_type

const bitvector_typet& sort_based_cast_to_bit_vector_convertert::to_type

Definition at line 207 of file convert_expr_to_smt.cpp.

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