arith_tools.h File Reference

#include "invariant.h"
#include "mp_arith.h"
#include "std_expr.h"
#include <limits>

Include dependency graph for arith_tools.h:

Go to the source code of this file.

Classes
struct	numeric_castt< Target, typename >
	Numerical cast provides a unified way of converting from one numerical type to another. More...
struct	numeric_castt< mp_integer >
	Convert expression to mp_integer. More...
struct	numeric_castt< T, typename std::enable_if< std::is_integral< T >::value >::type >
	Convert mp_integer or expr to any integral type. More...

Functions
bool	to_integer (const constant_exprt &expr, mp_integer &int_value)
	Convert a constant expression expr to an arbitrary-precision integer. More...
template<typename Target >
std::optional< Target >	numeric_cast (const exprt &arg)
	Converts an expression to any integral type. More...
template<typename Target >
Target	numeric_cast_v (const mp_integer &arg)
	Convert an mp_integer to integral type Target An invariant will fail if the conversion is not possible. More...
template<typename Target >
Target	numeric_cast_v (const constant_exprt &arg)
	Convert an expression to integral type Target An invariant will fail if the conversion is not possible. More...
constant_exprt	from_integer (const mp_integer &int_value, const typet &type)
std::size_t	address_bits (const mp_integer &size)
	ceil(log2(size)) More...
mp_integer	power (const mp_integer &base, const mp_integer &exponent)
	A multi-precision implementation of the power operator. More...
void	mp_min (mp_integer &a, const mp_integer &b)
void	mp_max (mp_integer &a, const mp_integer &b)
bool	get_bvrep_bit (const irep_idt &src, std::size_t width, std::size_t bit_index)
	Get a bit with given index from bit-vector representation. More...
irep_idt	make_bvrep (const std::size_t width, const std::function< bool(std::size_t)> f)
	construct a bit-vector representation from a functor More...
irep_idt	integer2bvrep (const mp_integer &, std::size_t width)
	convert an integer to bit-vector representation with given width This uses two's complement for negative numbers. More...
mp_integer	bvrep2integer (const irep_idt &, std::size_t width, bool is_signed)
	convert a bit-vector representation (possibly signed) to integer More...

Function Documentation

address_bits()

std::size_t address_bits

(

const mp_integer &

size

)

ceil(log2(size))

Definition at line 183 of file arith_tools.cpp.

bvrep2integer()

mp_integer bvrep2integer	(	const irep_idt &	src,
		std::size_t	width,
		bool	is_signed
	)

convert a bit-vector representation (possibly signed) to integer

Definition at line 408 of file arith_tools.cpp.

from_integer()

constant_exprt from_integer	(	const mp_integer &	int_value,
		const typet &	type
	)

Definition at line 99 of file arith_tools.cpp.

get_bvrep_bit()

bool get_bvrep_bit	(	const irep_idt &	src,
		std::size_t	width,
		std::size_t	bit_index
	)

Get a bit with given index from bit-vector representation.

Parameters

src	the bitvector representation
width	the number of bits in the bitvector
bit_index	index (0 is the least significant)

Definition at line 268 of file arith_tools.cpp.

integer2bvrep()

irep_idt integer2bvrep	(	const mp_integer &	src,
		std::size_t	width
	)

convert an integer to bit-vector representation with given width This uses two's complement for negative numbers.

If the value is out of range, it is 'wrapped around'.

Definition at line 386 of file arith_tools.cpp.

make_bvrep()

irep_idt make_bvrep	(	const std::size_t	width,
		const std::function< bool(std::size_t)>	f
	)

construct a bit-vector representation from a functor

Parameters

width	the width of the bit-vector
f	the functor – the parameter is the bit index

Returns

new bitvector representation

Definition at line 312 of file arith_tools.cpp.

mp_max()

void mp_max	(	mp_integer &	a,
		const mp_integer &	b
	)

Definition at line 258 of file arith_tools.cpp.

mp_min()

void mp_min	(	mp_integer &	a,
		const mp_integer &	b
	)

Definition at line 252 of file arith_tools.cpp.

numeric_cast()

template<typename Target >

std::optional<Target> numeric_cast

(

const exprt &

arg

)

Converts an expression to any integral type.

Template Parameters

Target

type to convert to

Parameters

arg	expression to convert

Returns

optional integer of type Target if conversion is possible, empty optional otherwise.

Definition at line 124 of file arith_tools.h.

numeric_cast_v() [1/2]

template<typename Target >

Target numeric_cast_v

(

const constant_exprt &

arg

)

Convert an expression to integral type Target An invariant will fail if the conversion is not possible.

Template Parameters

Target

type to convert to

Parameters

arg	constant expression

Returns

value of type Target

Definition at line 148 of file arith_tools.h.

numeric_cast_v() [2/2]

template<typename Target >

Target numeric_cast_v

(

const mp_integer &

arg

)

Convert an mp_integer to integral type Target An invariant will fail if the conversion is not possible.

Template Parameters

Target

type to convert to

Parameters

arg	mp_integer

Returns

value of type Target

Definition at line 135 of file arith_tools.h.

power()

mp_integer power	(	const mp_integer &	base,
		const mp_integer &	exponent
	)

A multi-precision implementation of the power operator.

parameters: Two mp_integers, base and exponent

Returns

One mp_integer with the value base^{exponent}

Definition at line 201 of file arith_tools.cpp.

to_integer()

bool to_integer	(	const constant_exprt &	expr,
		mp_integer &	int_value
	)

Convert a constant expression expr to an arbitrary-precision integer.

Parameters

	expr	Source expression
[out]	int_value	Integer value (only modified if conversion succeeds)

Returns

False if, and only if, the conversion was successful.

Definition at line 20 of file arith_tools.cpp.