CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
mp_arith.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9
10#ifndef CPROVER_UTIL_MP_ARITH_H
11#define CPROVER_UTIL_MP_ARITH_H
12
13#include <iosfwd>
14#include <string>
15
16#include "big-int/bigint.hh"
17
18// NOLINTNEXTLINE(readability/identifiers)
20
21std::ostream &operator<<(std::ostream &, const mp_integer &);
27
29 const mp_integer &, const mp_integer &, std::size_t true_size);
30
32 const mp_integer &, const mp_integer &, std::size_t true_size);
33
35 const mp_integer &, const mp_integer &, std::size_t true_size);
36
38 const mp_integer &, const mp_integer &, std::size_t true_size);
39
41 const mp_integer &, const mp_integer &, std::size_t true_size);
42
44 const mp_integer &, const mp_integer &, std::size_t true_size);
45
46const std::string integer2string(const mp_integer &, unsigned base=10);
47const mp_integer string2integer(const std::string &, unsigned base=10);
48const std::string integer2binary(const mp_integer &, std::size_t width);
49const mp_integer binary2integer(const std::string &, bool is_signed);
50
51#endif // CPROVER_UTIL_MP_ARITH_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
const mp_integer binary2integer(const std::string &, bool is_signed)
convert binary string representation to mp_integer
Definition mp_arith.cpp:117
BigInt mp_integer
Definition mp_arith.h:19
const mp_integer string2integer(const std::string &, unsigned base=10)
Definition mp_arith.cpp:54
mp_integer logic_left_shift(const mp_integer &, const mp_integer &, std::size_t true_size)
logic left shift bitwise operations only make sense on native objects, hence the largest object size ...
Definition mp_arith.cpp:291
mp_integer bitwise_or(const mp_integer &, const mp_integer &)
bitwise 'or' of two nonnegative integers
Definition mp_arith.cpp:215
mp_integer bitwise_and(const mp_integer &, const mp_integer &)
bitwise 'and' of two nonnegative integers
Definition mp_arith.cpp:227
const std::string integer2binary(const mp_integer &, std::size_t width)
Definition mp_arith.cpp:64
mp_integer arith_right_shift(const mp_integer &, const mp_integer &, std::size_t true_size)
arithmetic right shift (loads sign on MSB) bitwise operations only make sense on native objects,...
Definition mp_arith.cpp:272
const std::string integer2string(const mp_integer &, unsigned base=10)
Definition mp_arith.cpp:103
std::ostream & operator<<(std::ostream &, const mp_integer &)
Definition mp_arith.cpp:45
mp_integer logic_right_shift(const mp_integer &, const mp_integer &, std::size_t true_size)
logic right shift (loads 0 on MSB) bitwise operations only make sense on native objects,...
Definition mp_arith.cpp:317
mp_integer operator>>(const mp_integer &, const mp_integer &)
Definition mp_arith.cpp:22
mp_integer rotate_left(const mp_integer &, const mp_integer &, std::size_t true_size)
rotate left (LSB=MSB) bitwise operations only make sense on native objects, hence the largest object ...
Definition mp_arith.cpp:353
mp_integer arith_left_shift(const mp_integer &, const mp_integer &, std::size_t true_size)
arithmetic left shift bitwise operations only make sense on native objects, hence the largest object ...
Definition mp_arith.cpp:253
mp_integer bitwise_xor(const mp_integer &, const mp_integer &)
bitwise 'xor' of two nonnegative integers
Definition mp_arith.cpp:239
mp_integer rotate_right(const mp_integer &, const mp_integer &, std::size_t true_size)
rotates right (MSB=LSB) bitwise operations only make sense on native objects, hence the largest objec...
Definition mp_arith.cpp:333
BigInt mp_integer
Definition smt_terms.h:17
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition util.cpp:45