cprover
bv_arithmetic.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_BV_ARITHMETIC_H
11 #define CPROVER_UTIL_BV_ARITHMETIC_H
12 
13 #include <iosfwd>
14 
15 #include "mp_arith.h"
16 #include "format_spec.h"
17 
18 class constant_exprt;
19 class exprt;
20 class typet;
21 
22 class bv_spect
23 {
24 public:
25  std::size_t width;
26  bool is_signed;
27 
28  explicit bv_spect(const typet &type)
29  {
30  from_type(type);
31  }
32 
33  void from_type(const typet &type);
34 
35  bv_spect():width(0), is_signed(false)
36  {
37  }
38 
39  mp_integer max_value() const;
40  mp_integer min_value() const;
41 
42  typet to_type() const;
43 
44  bool operator==(const bv_spect &other) const
45  {
46  return width==other.width && is_signed==other.is_signed;
47  }
48 };
49 
51 {
52 public:
54 
55  explicit bv_arithmetict(const bv_spect &_spec):
56  spec(_spec), value(0)
57  {
58  }
59 
61  {
62  }
63 
64  explicit bv_arithmetict(const constant_exprt &expr)
65  {
66  from_expr(expr);
67  }
68 
69  void negate();
70 
71  void make_zero()
72  {
73  value=0;
74  }
75 
76  bool is_zero() const { return value==0; }
77 
78  // performs conversion to bit-vector format
79  void from_integer(const mp_integer &i);
80 
81  // performs conversion from ieee floating point format
82  void change_spec(const bv_spect &dest_spec);
83  mp_integer to_integer() const { return value; }
84 
85  void print(std::ostream &out) const;
86 
87  std::string to_ansi_c_string() const
88  {
89  return format(format_spect());
90  }
91 
92  std::string format(const format_spect &format_spec) const;
93 
94  // expressions
95  constant_exprt to_expr() const;
96  void from_expr(const constant_exprt &expr);
97 
103 
104  bool operator<(const bv_arithmetict &other);
105  bool operator<=(const bv_arithmetict &other);
106  bool operator>(const bv_arithmetict &other);
107  bool operator>=(const bv_arithmetict &other);
108  bool operator==(const bv_arithmetict &other);
109  bool operator!=(const bv_arithmetict &other);
110  bool operator==(int i);
111 
112  std::ostream &operator<<(std::ostream &out)
113  {
114  return out << to_ansi_c_string();
115  }
116 
117  // turn into natural number representation
118  void unpack(const mp_integer &i) { value=i; adjust(); }
119  mp_integer pack() const;
120 
121 protected:
122  // we store negative numbers as such
124 
125  // puts the value back into its range
126  void adjust();
127 };
128 
129 #endif // CPROVER_UTIL_BV_ARITHMETIC_H
bv_arithmetict(const bv_spect &_spec)
Definition: bv_arithmetic.h:55
mp_integer to_integer() const
Definition: bv_arithmetic.h:83
bool operator==(const bv_arithmetict &other)
bool operator>=(const bv_arithmetict &other)
mp_integer value
bool operator<(const bv_arithmetict &other)
void change_spec(const bv_spect &dest_spec)
void unpack(const mp_integer &i)
constant_exprt to_expr() const
void from_integer(const mp_integer &i)
bv_arithmetict & operator*=(const bv_arithmetict &other)
bool operator<=(const bv_arithmetict &other)
void print(std::ostream &out) const
std::string format(const format_spect &format_spec) const
bool is_zero() const
Definition: bv_arithmetic.h:76
bv_arithmetict & operator+=(const bv_arithmetict &other)
bool operator!=(const bv_arithmetict &other)
void from_expr(const constant_exprt &expr)
bv_arithmetict(const constant_exprt &expr)
Definition: bv_arithmetic.h:64
bv_arithmetict & operator%=(const bv_arithmetict &other)
bv_arithmetict & operator-=(const bv_arithmetict &other)
std::ostream & operator<<(std::ostream &out)
std::string to_ansi_c_string() const
Definition: bv_arithmetic.h:87
bv_arithmetict & operator/=(const bv_arithmetict &other)
bool operator>(const bv_arithmetict &other)
mp_integer pack() const
std::size_t width
Definition: bv_arithmetic.h:25
bv_spect(const typet &type)
Definition: bv_arithmetic.h:28
bool operator==(const bv_spect &other) const
Definition: bv_arithmetic.h:44
bool is_signed
Definition: bv_arithmetic.h:26
void from_type(const typet &type)
mp_integer min_value() const
typet to_type() const
mp_integer max_value() const
A constant literal expression.
Definition: std_expr.h:2668
Base class for all expressions.
Definition: expr.h:54
The type of an expression, extends irept.
Definition: type.h:28
BigInt mp_integer
Definition: mp_arith.h:19