cprover
arith_tools.cpp File Reference
#include "arith_tools.h"
#include "fixedbv.h"
#include "ieee_float.h"
#include "invariant.h"
#include "std_types.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. 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...
 
static char nibble2hex (unsigned char nibble)
 turn a value 0...15 into '0'-'9', 'A'-'Z' 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 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 More...
 
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 More...
 
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. More...
 
mp_integer bvrep2integer (const irep_idt &src, 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 src,
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.

◆ 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 349 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 366 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.

◆ nibble2hex()

static char nibble2hex ( unsigned char  nibble)
static

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

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