cprover
Loading...
Searching...
No Matches
arith_tools.cpp File Reference
#include "arith_tools.h"
#include "c_types.h"
#include "expr_util.h"
#include "fixedbv.h"
#include "ieee_float.h"
#include "invariant.h"
#include "std_expr.h"
#include <algorithm>
Include dependency graph for arith_tools.cpp:

Go to the source code of this file.

Functions

bool to_integer (const constant_exprt &expr, mp_integer &int_value)
 Convert a constant expression expr to an arbitrary-precision integer.
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.
static char nibble2hex (unsigned char nibble)
 turn a value 0...15 into '0'-'9', 'A'-'Z'
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 bvrep_bitwise_op (const irep_idt &a, const irep_idt &b, const std::size_t width, const std::function< bool(bool, bool)> f)
 perform a binary bit-wise operation, given as a functor, on a bit-vector representation
irep_idt bvrep_bitwise_op (const irep_idt &a, const std::size_t width, const std::function< bool(bool)> f)
 perform a unary bit-wise operation, given as a functor, on a bit-vector representation
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.
mp_integer bvrep2integer (const irep_idt &src, 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 185 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 410 of file arith_tools.cpp.

◆ bvrep_bitwise_op() [1/2]

irep_idt bvrep_bitwise_op ( const irep_idt & a,
const irep_idt & b,
const std::size_t width,
const std::function< bool(bool, bool)> f )

perform a binary bit-wise operation, given as a functor, on a bit-vector representation

Parameters
athe representation of the first bit vector
bthe representation of the second bit vector
widththe width of the bit-vector
fthe functor
Returns
new bitvector representation

Definition at line 358 of file arith_tools.cpp.

◆ bvrep_bitwise_op() [2/2]

irep_idt bvrep_bitwise_op ( const irep_idt & a,
const std::size_t width,
const std::function< bool(bool)> f )

perform a unary bit-wise operation, given as a functor, on a bit-vector representation

Parameters
athe bit-vector representation
widththe width of the bit-vector
fthe functor
Returns
new bitvector representation

Definition at line 375 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 270 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 388 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 314 of file arith_tools.cpp.

◆ mp_max()

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

Definition at line 260 of file arith_tools.cpp.

◆ mp_min()

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

Definition at line 254 of file arith_tools.cpp.

◆ nibble2hex()

char nibble2hex ( unsigned char nibble)
static

turn a value 0...15 into '0'-'9', 'A'-'Z'

Definition at line 299 of file arith_tools.cpp.

◆ 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 203 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 20 of file arith_tools.cpp.