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
std::optional< smt_termt >	result

Detailed Description

Definition at line 298 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 303 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 322 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 313 of file convert_expr_to_smt.cpp.

visit() [3/3]

void sort_based_literal_convertert::visit ( const smt_bool_sortt &  )

inlineoverride

Definition at line 308 of file convert_expr_to_smt.cpp.

Member Data Documentation

member_input

const constant_exprt& sort_based_literal_convertert::member_input

Definition at line 300 of file convert_expr_to_smt.cpp.

result

std::optional<smt_termt> sort_based_literal_convertert::result

Definition at line 301 of file convert_expr_to_smt.cpp.

---

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

• /home/runner/work/cbmc/cbmc/src/solvers/smt2_incremental/convert_expr_to_smt.cpp