CBMC
Public Member Functions | Public Attributes | List of all members
sort_based_literal_convertert Struct Reference
+ Inheritance diagram for sort_based_literal_convertert:
+ Collaboration diagram for sort_based_literal_convertert:

Public Member Functions

 sort_based_literal_convertert (const constant_exprt &input)
 
void visit (const smt_bool_sortt &) override
 
void visit (const smt_bit_vector_sortt &bit_vector_sort) override
 
void visit (const smt_array_sortt &array_sort) override
 

Public Attributes

const constant_exprt & member_input
 
optionalt< smt_termt > result
 

Detailed Description

Definition at line 295 of file convert_expr_to_smt.cpp.

Constructor & Destructor Documentation

◆ sort_based_literal_convertert()

sort_based_literal_convertert::sort_based_literal_convertert ( const constant_exprt &  input)
inlineexplicit

Definition at line 300 of file convert_expr_to_smt.cpp.

Member Function Documentation

◆ visit() [1/3]

void sort_based_literal_convertert::visit ( const smt_array_sortt &  array_sort)
inlineoverride

Definition at line 319 of file convert_expr_to_smt.cpp.

◆ visit() [2/3]

void sort_based_literal_convertert::visit ( const smt_bit_vector_sortt &  bit_vector_sort)
inlineoverride

Definition at line 310 of file convert_expr_to_smt.cpp.

◆ visit() [3/3]

void sort_based_literal_convertert::visit ( const smt_bool_sortt &  )
inlineoverride

Definition at line 305 of file convert_expr_to_smt.cpp.

Member Data Documentation

◆ member_input

const constant_exprt& sort_based_literal_convertert::member_input

Definition at line 297 of file convert_expr_to_smt.cpp.

◆ result

optionalt<smt_termt> sort_based_literal_convertert::result

Definition at line 298 of file convert_expr_to_smt.cpp.

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