10#ifndef CPROVER_UTIL_ARITH_TOOLS_H
11#define CPROVER_UTIL_ARITH_TOOLS_H
30template <
typename Target,
typename =
void>
64 template <
typename U = T,
65 typename std::enable_if<std::is_signed<U>::value,
int>::type = 0>
72 template <
typename U = T,
73 typename std::enable_if<!std::is_signed<U>::value,
int>::type = 0>
76 return mpi.to_ulong();
84 std::numeric_limits<T>::max() <=
85 std::numeric_limits<
decltype(get_val(
mpi))>::max() &&
86 std::numeric_limits<T>::min() >=
87 std::numeric_limits<
decltype(get_val(
mpi))>::min(),
88 "Numeric cast only works for types smaller than long long");
91 mpi <= std::numeric_limits<T>::max() &&
92 mpi >= std::numeric_limits<T>::min())
94 return static_cast<T
>(get_val(
mpi));
123template <
typename Target>
134template <
typename Target>
138 INVARIANT(
maybe,
"mp_integer should be convertible to target integral type");
147template <
typename Target>
153 "expression should be convertible to target integral type",
175make_bvrep(
const std::size_t width,
const std::function<
bool(std::size_t)> f);
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
A constant literal expression.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
bool is_constant() const
Return whether the expression is a constant.
The type of an expression, extends irept.
#define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Same as invariant, with one or more diagnostics attached Diagnostics can be of any type that has a sp...
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
API to expression classes.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
static auto get_val(const mp_integer &mpi) -> decltype(mpi.to_long())
std::optional< T > operator()(const exprt &expr) const
std::optional< T > operator()(const constant_exprt &expr) const
std::optional< T > operator()(const mp_integer &mpi) const
static auto get_val(const mp_integer &mpi) -> decltype(mpi.to_ulong())
std::optional< mp_integer > operator()(const constant_exprt &expr) const
std::optional< mp_integer > operator()(const exprt &expr) const
Numerical cast provides a unified way of converting from one numerical type to another.
bool is_signed(const typet &t)
Convenience function – is the type signed?