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))
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
The type of an expression.
Definition: type.h:20
BigInt mp_integer
Definition: mp_arith.h:19
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
void mp_min(mp_integer &a, const mp_integer &b)
A constant literal expression.
Definition: std_expr.h:3685
mp_integer address_bits(const mp_integer &size)
ceil(log2(size))
void mp_max(mp_integer &a, const mp_integer &b)
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
Base class for all expressions.
Definition: expr.h:46
constant_exprt from_integer(const mp_integer &int_value, const typet &type)