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, const namespacet &ns)
 This function is complete the external interface to this class. More...
 

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 typet & type_to_construct
 
const namespacet & ns
 
std::optional< exprt > result
 

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()

static 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)
inlineoverrideprivate

Definition at line 42 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 28 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 114 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 108 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 101 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 36 of file construct_value_expr_from_smt.cpp.

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: