cprover
arith_tools.h File Reference
#include "invariant.h"
#include "mp_arith.h"
#include "optional.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 >
optionalt< 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 176 of file arith_tools.cpp.

◆ bvrep2integer()

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

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

Definition at line 401 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
srcthe bitvector representation
widththe number of bits in the bitvector
bit_indexindex (0 is the least significant)

Definition at line 261 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 379 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
widththe width of the bit-vector
fthe functor – the parameter is the bit index
Returns
new bitvector representation

Definition at line 305 of file arith_tools.cpp.

◆ mp_max()

void mp_max ( mp_integer a,
const mp_integer b 
)

Definition at line 251 of file arith_tools.cpp.

◆ mp_min()

void mp_min ( mp_integer a,
const mp_integer b 
)

Definition at line 245 of file arith_tools.cpp.

◆ numeric_cast()

template<typename Target >
optionalt<Target> numeric_cast ( const exprt arg)

Converts an expression to any integral type.

Template Parameters
Targettype to convert to
Parameters
argexpression to convert
Returns
optional integer of type Target if conversion is possible, empty optional otherwise.

Definition at line 125 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
Targettype to convert to
Parameters
argconstant expression
Returns
value of type Target

Definition at line 149 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
Targettype to convert to
Parameters
argmp_integer
Returns
value of type Target

Definition at line 136 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 194 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
exprSource expression
[out]int_valueInteger value (only modified if conversion succeeds)
Returns
False if, and only if, the conversion was successful.

Definition at line 19 of file arith_tools.cpp.