CBMC
construct_value_expr_from_smt.h
Go to the documentation of this file.
1 // Author: Diffblue Ltd.
2 
3 #ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_CONSTRUCT_VALUE_EXPR_FROM_SMT_H
4 #define CPROVER_SOLVERS_SMT2_INCREMENTAL_CONSTRUCT_VALUE_EXPR_FROM_SMT_H
5 
6 #include <util/expr.h>
7 
8 class smt_termt;
9 class typet;
10 
30 exprt construct_value_expr_from_smt(
31  const smt_termt &value_term,
32  const typet &type_to_construct,
33  const namespacet &ns);
34 
35 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_CONSTRUCT_VALUE_EXPR_FROM_SMT_H
exprt
Base class for all expressions.
Definition: expr.h:56
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
smt_termt
Definition: smt_terms.h:21
typet
The type of an expression, extends irept.
Definition: type.h:29
construct_value_expr_from_smt
exprt construct_value_expr_from_smt(const smt_termt &value_term, const typet &type_to_construct, const namespacet &ns)
Given a value_term and a type_to_construct, this function constructs a value exprt with a value based...
Definition: construct_value_expr_from_smt.cpp:136