CBMC
Static Public Member Functions | Private Member Functions | Private Attributes | List of all members
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)
 This function is complete the external interface to this class. More...
 

Private Member Functions

 value_expr_from_smt_factoryt (const typet &type_to_construct)
 
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 typet & type_to_construct
 
optionalt< exprt > result
 

Detailed Description

Definition at line 13 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)
inlineexplicitprivate

Definition at line 19 of file construct_value_expr_from_smt.cpp.

Member Function Documentation

◆ make()

static exprt value_expr_from_smt_factoryt::make ( const smt_termt &  value_term,
const typet &  type_to_construct 
)
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 106 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)
inlineoverrideprivate

Definition at line 38 of file construct_value_expr_from_smt.cpp.

◆ visit() [2/6]

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

Definition at line 24 of file construct_value_expr_from_smt.cpp.

◆ visit() [3/6]

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

Definition at line 96 of file construct_value_expr_from_smt.cpp.

◆ visit() [4/6]

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

Definition at line 90 of file construct_value_expr_from_smt.cpp.

◆ visit() [5/6]

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

Definition at line 83 of file construct_value_expr_from_smt.cpp.

◆ visit() [6/6]

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

Definition at line 32 of file construct_value_expr_from_smt.cpp.

Member Data Documentation

◆ result

optionalt<exprt> value_expr_from_smt_factoryt::result
private

Definition at line 17 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 16 of file construct_value_expr_from_smt.cpp.

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