cprover
arith_tools.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module:
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
9
10
#ifndef CPROVER_UTIL_ARITH_TOOLS_H
11
#define CPROVER_UTIL_ARITH_TOOLS_H
12
13
#include "
mp_arith.h
"
14
15
class
exprt
;
16
class
constant_exprt
;
17
class
typet
;
18
19
// this one will go away
20
// returns 'true' on error
21
bool
to_integer
(
const
exprt
&expr,
mp_integer
&int_value);
22
23
// returns 'true' on error
24
bool
to_integer
(
const
constant_exprt
&expr,
mp_integer
&int_value);
25
26
// returns 'true' on error
27
bool
to_unsigned_integer
(
const
constant_exprt
&expr,
unsigned
&uint_value);
28
29
// assert(false) in case of unsupported type
30
constant_exprt
from_integer
(
const
mp_integer
&int_value,
const
typet
&type);
31
32
// ceil(log2(size))
33
mp_integer
address_bits
(
const
mp_integer
&size);
34
35
mp_integer
power
(
const
mp_integer
&base,
const
mp_integer
&exponent);
36
37
void
mp_min
(
mp_integer
&a,
const
mp_integer
&b);
38
void
mp_max
(
mp_integer
&a,
const
mp_integer
&b);
39
40
#endif // CPROVER_UTIL_ARITH_TOOLS_H
typet
The type of an expression.
Definition:
type.h:20
mp_integer
BigInt mp_integer
Definition:
mp_arith.h:19
to_unsigned_integer
bool to_unsigned_integer(const constant_exprt &expr, unsigned &uint_value)
convert a positive integer expression to an unsigned int
Definition:
arith_tools.cpp:95
mp_min
void mp_min(mp_integer &a, const mp_integer &b)
Definition:
arith_tools.cpp:273
constant_exprt
A constant literal expression.
Definition:
std_expr.h:3685
address_bits
mp_integer address_bits(const mp_integer &size)
ceil(log2(size))
Definition:
arith_tools.cpp:210
mp_max
void mp_max(mp_integer &a, const mp_integer &b)
Definition:
arith_tools.cpp:279
power
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
Definition:
arith_tools.cpp:222
to_integer
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition:
arith_tools.cpp:18
mp_arith.h
exprt
Base class for all expressions.
Definition:
expr.h:46
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition:
arith_tools.cpp:109
util
arith_tools.h
Generated by
1.8.14