CBMC
fixedbv.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_FIXEDBV_H
11 #define CPROVER_UTIL_FIXEDBV_H
12 
13 #include "mp_arith.h"
14 #include "format_spec.h"
15 
16 class constant_exprt;
17 class fixedbv_typet;
18 
20 {
21 public:
22  std::size_t integer_bits, width;
23 
25  {
26  }
27 
28  fixedbv_spect(std::size_t _width, std::size_t _integer_bits):
29  integer_bits(_integer_bits), width(_width)
30  {
31  }
32 
33  explicit fixedbv_spect(const fixedbv_typet &type);
34 
35  std::size_t get_fraction_bits() const
36  {
37  return width-integer_bits;
38  }
39 };
40 
41 class fixedbvt
42 {
43 public:
45 
46  fixedbvt():v(0)
47  {
48  }
49 
50  explicit fixedbvt(const fixedbv_spect &_spec):spec(_spec), v(0)
51  {
52  }
53 
54  explicit fixedbvt(const constant_exprt &expr);
55 
56  void from_integer(const mp_integer &i);
57  mp_integer to_integer() const; // this rounds to zero
58  void from_expr(const constant_exprt &expr);
59  constant_exprt to_expr() const;
60  void round(const fixedbv_spect &dest_spec);
61 
62  std::string to_ansi_c_string() const
63  {
64  return format(format_spect());
65  }
66 
67  std::string format(const format_spect &format_spec) const;
68 
69  bool operator==(int i) const;
70 
71  bool is_zero() const
72  {
73  return v==0;
74  }
75 
76  static fixedbvt zero(const fixedbv_typet &type)
77  {
78  return fixedbvt(fixedbv_spect(type));
79  }
80 
81  void negate();
82 
83  fixedbvt &operator/=(const fixedbvt &other);
84  fixedbvt &operator*=(const fixedbvt &other);
85  fixedbvt &operator+=(const fixedbvt &other);
86  fixedbvt &operator-=(const fixedbvt &other);
87 
88  bool operator<(const fixedbvt &other) const { return v<other.v; }
89  bool operator<=(const fixedbvt &other) const { return v<=other.v; }
90  bool operator>(const fixedbvt &other) const { return v>other.v; }
91  bool operator>=(const fixedbvt &other) const { return v>=other.v; }
92  bool operator==(const fixedbvt &other) const { return v==other.v; }
93  bool operator!=(const fixedbvt &other) const { return v!=other.v; }
94 
95  const mp_integer &get_value() const { return v; }
96  void set_value(const mp_integer &_v) { v=_v; }
97 
98 protected:
99  // negative values stored as such
101 };
102 
103 #endif // CPROVER_UTIL_FIXEDBV_H
A constant literal expression.
Definition: std_expr.h:2990
std::size_t integer_bits
Definition: fixedbv.h:22
fixedbv_spect(std::size_t _width, std::size_t _integer_bits)
Definition: fixedbv.h:28
std::size_t width
Definition: fixedbv.h:22
fixedbv_spect()
Definition: fixedbv.h:24
std::size_t get_fraction_bits() const
Definition: fixedbv.h:35
Fixed-width bit-vector with signed fixed-point interpretation.
fixedbv_spect spec
Definition: fixedbv.h:44
bool operator>=(const fixedbvt &other) const
Definition: fixedbv.h:91
fixedbvt()
Definition: fixedbv.h:46
void from_integer(const mp_integer &i)
Definition: fixedbv.cpp:32
void from_expr(const constant_exprt &expr)
Definition: fixedbv.cpp:26
void negate()
Definition: fixedbv.cpp:90
bool operator<=(const fixedbvt &other) const
Definition: fixedbv.h:89
bool operator==(int i) const
Definition: fixedbv.cpp:129
fixedbvt & operator+=(const fixedbvt &other)
Definition: fixedbv.cpp:109
mp_integer to_integer() const
Definition: fixedbv.cpp:37
bool operator<(const fixedbvt &other) const
Definition: fixedbv.h:88
fixedbvt & operator*=(const fixedbvt &other)
Definition: fixedbv.cpp:95
void set_value(const mp_integer &_v)
Definition: fixedbv.h:96
void round(const fixedbv_spect &dest_spec)
Definition: fixedbv.cpp:52
static fixedbvt zero(const fixedbv_typet &type)
Definition: fixedbv.h:76
std::string format(const format_spect &format_spec) const
Definition: fixedbv.cpp:134
std::string to_ansi_c_string() const
Definition: fixedbv.h:62
fixedbvt & operator/=(const fixedbvt &other)
Definition: fixedbv.cpp:121
bool operator>(const fixedbvt &other) const
Definition: fixedbv.h:90
fixedbvt & operator-=(const fixedbvt &other)
Definition: fixedbv.cpp:115
fixedbvt(const fixedbv_spect &_spec)
Definition: fixedbv.h:50
bool is_zero() const
Definition: fixedbv.h:71
mp_integer v
Definition: fixedbv.h:100
bool operator!=(const fixedbvt &other) const
Definition: fixedbv.h:93
const mp_integer & get_value() const
Definition: fixedbv.h:95
constant_exprt to_expr() const
Definition: fixedbv.cpp:43
bool operator==(const fixedbvt &other) const
Definition: fixedbv.h:92
BigInt mp_integer
Definition: smt_terms.h:17