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 exprt;
19 class typet;
20 
21 class bv_spect
22 {
23 public:
24  std::size_t width;
25  bool is_signed;
26 
27  explicit bv_spect(const typet &type)
28  {
29  from_type(type);
30  }
31 
32  void from_type(const typet &type);
33 
34  bv_spect():width(0), is_signed(false)
35  {
36  }
37 
38  mp_integer max_value() const;
39  mp_integer min_value() const;
40 
41  typet to_type() const;
42 
43  bool operator==(const bv_spect &other) const
44  {
45  return width==other.width && is_signed==other.is_signed;
46  }
47 };
48 
50 {
51 public:
53 
54  explicit bv_arithmetict(const bv_spect &_spec):
55  spec(_spec), value(0)
56  {
57  }
58 
59  bv_arithmetict():value(0)
60  {
61  }
62 
63  explicit bv_arithmetict(const exprt &expr)
64  {
65  from_expr(expr);
66  }
67 
68  void negate();
69 
70  void make_zero()
71  {
72  value=0;
73  }
74 
75  bool is_zero() const { return value==0; }
76 
77  // performs conversion to bit-vector format
78  void from_integer(const mp_integer &i);
79 
80  // performs conversion from ieee floating point format
81  void change_spec(const bv_spect &dest_spec);
82  mp_integer to_integer() const { return value; }
83 
84  void print(std::ostream &out) const;
85 
86  std::string to_ansi_c_string() const
87  {
88  return format(format_spect());
89  }
90 
91  std::string format(const format_spect &format_spec) const;
92 
93  // expressions
94  exprt to_expr() const;
95  void from_expr(const exprt &expr);
96 
97  bv_arithmetict &operator/=(const bv_arithmetict &other);
98  bv_arithmetict &operator*=(const bv_arithmetict &other);
99  bv_arithmetict &operator+=(const bv_arithmetict &other);
101  bv_arithmetict &operator%=(const bv_arithmetict &other);
102 
103  bool operator<(const bv_arithmetict &other);
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==(int i);
110 
111  std::ostream &operator<<(std::ostream &out)
112  {
113  return out << to_ansi_c_string();
114  }
115 
116  // turn into natural number representation
117  void unpack(const mp_integer &i) { value=i; adjust(); }
118  mp_integer pack() const;
119 
120 protected:
121  // we store negative numbers as such
123 
124  // puts the value back into its range
125  void adjust();
126 };
127 
128 #endif // CPROVER_UTIL_BV_ARITHMETIC_H
The type of an expression.
Definition: type.h:20
bool operator==(const bv_spect &other) const
Definition: bv_arithmetic.h:43
BigInt mp_integer
Definition: mp_arith.h:19
exprt to_expr(const namespacet &ns, const irep_idt &identifier, const std::string &src)
guardt & operator-=(guardt &g1, const guardt &g2)
Definition: guard.cpp:93
void from_type(const typet &type)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
bool operator!=(const interval_templatet< T > &a, const interval_templatet< T > &b)
tvt operator>(const interval_templatet< T > &a, const interval_templatet< T > &b)
std::string to_ansi_c_string() const
Definition: bv_arithmetic.h:86
bv_spect(const typet &type)
Definition: bv_arithmetic.h:27
bool is_signed
Definition: bv_arithmetic.h:25
tvt operator<=(const interval_templatet< T > &a, const interval_templatet< T > &b)
typet to_type() const
std::size_t width
Definition: bv_arithmetic.h:24
mp_integer max_value() const
mp_integer value
mp_integer to_integer() const
Definition: bv_arithmetic.h:82
mp_integer min_value() const
std::ostream & operator<<(std::ostream &out)
Base class for all expressions.
Definition: expr.h:46
bv_arithmetict(const exprt &expr)
Definition: bv_arithmetic.h:63
bool is_zero() const
Definition: bv_arithmetic.h:75
bv_arithmetict(const bv_spect &_spec)
Definition: bv_arithmetic.h:54
tvt operator>=(const interval_templatet< T > &a, const interval_templatet< T > &b)
tvt operator<(const interval_templatet< T > &a, const interval_templatet< T > &b)
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
void unpack(const mp_integer &i)