construct_value_expr_from_smt.cpp File Reference

#include <util/arith_tools.h>
#include <util/bitvector_types.h>
#include <util/pointer_expr.h>
#include <util/std_expr.h>
#include <util/std_types.h>
#include <util/type.h>
#include <solvers/smt2_incremental/construct_value_expr_from_smt.h>
#include <solvers/smt2_incremental/smt_terms.h>

Include dependency graph for construct_value_expr_from_smt.cpp:

Go to the source code of this file.

Classes
class	value_expr_from_smt_factoryt

Functions
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 on value_term and a type of type_to_construct. More...

Function Documentation

construct_value_expr_from_smt()

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 on value_term and a type of type_to_construct.

Parameters

value_term	This must be a "simple" term encoding a value. It must not be a term requiring any kind of further evaluation to get a value, such as would be the case for identifiers or function applications.
type_to_construct	The type which the constructed expr returned is expected to have. This type must be compatible with the sort of value_term.

Note

The type is required separately in order to carry out this conversion, because the smt value term does not contain all the required information. For example an 8 bit, bit vector with a value of 255 could be used to construct an unsigned char with the value 255 or alternatively a signed char with the value -1. So these alternatives are disambiguated using the type.

Definition at line 115 of file construct_value_expr_from_smt.cpp.