cprover
Loading...
Searching...
No Matches
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
8class smt_termt;
9class typet;
10
28 const smt_termt &value_term,
29 const typet &type_to_construct);
30
31#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_CONSTRUCT_VALUE_EXPR_FROM_SMT_H
Base class for all expressions.
Definition expr.h:54
The type of an expression, extends irept.
Definition type.h:29
exprt construct_value_expr_from_smt(const smt_termt &value_term, const typet &type_to_construct)
Given a value_term and a type_to_construct, this function constructs a value exprt with a value based...