cbmc/construct__value__expr__from__smt_8h_source.html

// Author: Diffblue Ltd.


#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_CONSTRUCT_VALUE_EXPR_FROM_SMT_H

#define CPROVER_SOLVERS_SMT2_INCREMENTAL_CONSTRUCT_VALUE_EXPR_FROM_SMT_H


#include <util/expr.h>


class smt_termt;

class typet;


exprt construct_value_expr_from_smt(

  const smt_termt &value_term,

  const typet &type_to_construct,

  const namespacet &ns);


#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_CONSTRUCT_VALUE_EXPR_FROM_SMT_H

ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562

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:91

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

expr.h