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

Include dependency graph for arith_tools.h:

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.

template<typename Target >
std::optional< Target >	numeric_cast (const exprt &arg)
	Converts an expression to any integral type.

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<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.

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

std::size_t	address_bits (const mp_integer &size)
	ceil(log2(size))

mp_integer	power (const mp_integer &base, const mp_integer &exponent)
	A multi-precision implementation of the power operator.

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.

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

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.

mp_integer	bvrep2integer (const irep_idt &, std::size_t width, bool is_signed)
	convert a bit-vector representation (possibly signed) to integer

Function Documentation

◆ address_bits()

std::size_t address_bits ( const mp_integer & size )

ceil(log2(size))

Definition at line 189 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 414 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 274 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 392 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 318 of file arith_tools.cpp.

◆ mp_max()

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

Definition at line 264 of file arith_tools.cpp.

◆ mp_min()

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

Definition at line 258 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 207 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.

Classes

Functions

Function Documentation

◆ address_bits()

◆ bvrep2integer()

◆ from_integer()

◆ get_bvrep_bit()

◆ integer2bvrep()

◆ make_bvrep()

◆ mp_max()

◆ mp_min()

◆ numeric_cast()

◆ numeric_cast_v() [1/2]

◆ numeric_cast_v() [2/2]

◆ power()

◆ to_integer()