cprover
Loading...
Searching...
No Matches
value_expr_from_smt_factoryt Class Reference
Inheritance diagram for value_expr_from_smt_factoryt:
Collaboration diagram for value_expr_from_smt_factoryt:

Static Public Member Functions

static exprt make (const smt_termt &value_term, const typet &type_to_construct, const namespacet &ns)
 This function is complete the external interface to this class.

Private Member Functions

 value_expr_from_smt_factoryt (const typet &type_to_construct, const namespacet &ns)
void visit (const smt_bool_literal_termt &bool_literal) override
void visit (const smt_identifier_termt &identifier_term) override
void visit (const smt_bit_vector_constant_termt &bit_vector_constant) override
void visit (const smt_function_application_termt &function_application) override
void visit (const smt_forall_termt &forall) override
void visit (const smt_exists_termt &exists) override

Private Attributes

const typettype_to_construct
const namespacetns
std::optional< exprtresult

Detailed Description

Definition at line 14 of file construct_value_expr_from_smt.cpp.

Constructor & Destructor Documentation

◆ value_expr_from_smt_factoryt()

value_expr_from_smt_factoryt::value_expr_from_smt_factoryt ( const typet & type_to_construct,
const namespacet & ns )
inlineexplicitprivate

Definition at line 21 of file construct_value_expr_from_smt.cpp.

Member Function Documentation

◆ make()

exprt value_expr_from_smt_factoryt::make ( const smt_termt & value_term,
const typet & type_to_construct,
const namespacet & ns )
inlinestatic

This function is complete the external interface to this class.

All construction of this class and construction of expressions should be carried out via this function.

Definition at line 124 of file construct_value_expr_from_smt.cpp.

◆ visit() [1/6]

void value_expr_from_smt_factoryt::visit ( const smt_bit_vector_constant_termt & bit_vector_constant)
inlineoverrideprivatevirtual

◆ visit() [2/6]

void value_expr_from_smt_factoryt::visit ( const smt_bool_literal_termt & bool_literal)
inlineoverrideprivatevirtual

◆ visit() [3/6]

void value_expr_from_smt_factoryt::visit ( const smt_exists_termt & exists)
inlineoverrideprivatevirtual

◆ visit() [4/6]

void value_expr_from_smt_factoryt::visit ( const smt_forall_termt & forall)
inlineoverrideprivatevirtual

◆ visit() [5/6]

void value_expr_from_smt_factoryt::visit ( const smt_function_application_termt & function_application)
inlineoverrideprivatevirtual

◆ visit() [6/6]

void value_expr_from_smt_factoryt::visit ( const smt_identifier_termt & identifier_term)
inlineoverrideprivatevirtual

Member Data Documentation

◆ ns

const namespacet& value_expr_from_smt_factoryt::ns
private

Definition at line 18 of file construct_value_expr_from_smt.cpp.

◆ result

std::optional<exprt> value_expr_from_smt_factoryt::result
private

Definition at line 19 of file construct_value_expr_from_smt.cpp.

◆ type_to_construct

const typet& value_expr_from_smt_factoryt::type_to_construct
private

Definition at line 17 of file construct_value_expr_from_smt.cpp.


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