cprover
fixedbv.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "fixedbv.h"
10 
11 #include "arith_tools.h"
12 #include "bitvector_types.h"
13 #include "std_expr.h"
14 #include "std_types.h"
15 
17 {
19  width=type.get_width();
20 }
21 
23 {
24  from_expr(expr);
25 }
26 
28 {
30  v = bvrep2integer(expr.get_value(), spec.width, true);
31 }
32 
34 {
35  v=i*power(2, spec.get_fraction_bits());
36 }
37 
39 {
40  // this rounds to zero, i.e., we just divide
41  return v/power(2, spec.get_fraction_bits());
42 }
43 
45 {
46  fixedbv_typet type;
47  type.set_width(spec.width);
49  PRECONDITION(spec.width != 0);
50  return constant_exprt(integer2bvrep(v, spec.width), type);
51 }
52 
53 void fixedbvt::round(const fixedbv_spect &dest_spec)
54 {
55  std::size_t old_fraction_bits=spec.width-spec.integer_bits;
56  std::size_t new_fraction_bits=dest_spec.width-dest_spec.integer_bits;
57 
58  mp_integer result;
59 
60  if(new_fraction_bits>old_fraction_bits)
61  result=v*power(2, new_fraction_bits-old_fraction_bits);
62  else if(new_fraction_bits<old_fraction_bits)
63  {
64  // may need to round
65  mp_integer p=power(2, old_fraction_bits-new_fraction_bits);
66  mp_integer div=v/p;
67  mp_integer rem=v%p;
68  if(rem<0)
69  rem=-rem;
70 
71  if(rem*2>=p)
72  {
73  if(v<0)
74  --div;
75  else
76  ++div;
77  }
78 
79  result=div;
80  }
81  else // new_faction_bits==old_fraction_vits
82  {
83  // no change!
84  result=v;
85  }
86 
87  v=result;
88  spec=dest_spec;
89 }
90 
92 {
93  v=-v;
94 }
95 
97 {
98  v*=o.v;
99 
100  fixedbv_spect old_spec=spec;
101 
102  spec.width+=o.spec.width;
104 
105  round(old_spec);
106 
107  return *this;
108 }
109 
111 {
112  v += o.v;
113  return *this;
114 }
115 
117 {
118  v -= o.v;
119  return *this;
120 }
121 
123 {
124  v*=power(2, o.spec.get_fraction_bits());
125  v/=o.v;
126 
127  return *this;
128 }
129 
130 bool fixedbvt::operator==(int i) const
131 {
132  return v==power(2, spec.get_fraction_bits())*i;
133 }
134 
135 std::string fixedbvt::format(
136  const format_spect &format_spec) const
137 {
138  std::string dest;
139  std::size_t fraction_bits=spec.get_fraction_bits();
140 
141  mp_integer int_value=v;
142  mp_integer factor=power(2, fraction_bits);
143 
144  if(int_value.is_negative())
145  {
146  dest+='-';
147  int_value.negate();
148  }
149 
150  std::string base_10_string=
151  integer2string(int_value*power(10, fraction_bits)/factor);
152 
153  while(base_10_string.size()<=fraction_bits)
154  base_10_string="0"+base_10_string;
155 
156  std::string integer_part=
157  std::string(base_10_string, 0, base_10_string.size()-fraction_bits);
158 
159  std::string fraction_part=
160  std::string(base_10_string, base_10_string.size()-fraction_bits);
161 
162  dest+=integer_part;
163 
164  // strip trailing zeros
165  while(!fraction_part.empty() &&
166  fraction_part[fraction_part.size()-1]=='0')
167  fraction_part.resize(fraction_part.size()-1);
168 
169  if(!fraction_part.empty())
170  dest+="."+fraction_part;
171 
172  while(dest.size()<format_spec.min_width)
173  dest=" "+dest;
174 
175  return dest;
176 }
fixedbvt::from_integer
void from_integer(const mp_integer &i)
Definition: fixedbv.cpp:33
fixedbvt::operator/=
fixedbvt & operator/=(const fixedbvt &other)
Definition: fixedbv.cpp:122
fixedbv_typet::set_integer_bits
void set_integer_bits(std::size_t b)
Definition: bitvector_types.h:274
arith_tools.h
format_spect
Definition: format_spec.h:16
fixedbvt::negate
void negate()
Definition: fixedbv.cpp:91
fixedbvt::to_integer
mp_integer to_integer() const
Definition: fixedbv.cpp:38
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
fixedbv_spect::get_fraction_bits
std::size_t get_fraction_bits() const
Definition: fixedbv.h:35
fixedbv.h
fixedbv_spect::integer_bits
std::size_t integer_bits
Definition: fixedbv.h:22
fixedbvt::operator+=
fixedbvt & operator+=(const fixedbvt &other)
Definition: fixedbv.cpp:110
fixedbvt::fixedbvt
fixedbvt()
Definition: fixedbv.h:46
fixedbvt::operator-=
fixedbvt & operator-=(const fixedbvt &other)
Definition: fixedbv.cpp:116
fixedbvt::to_expr
constant_exprt to_expr() const
Definition: fixedbv.cpp:44
to_fixedbv_type
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a typet to a fixedbv_typet.
Definition: bitvector_types.h:305
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
integer2bvrep
irep_idt integer2bvrep(const mp_integer &src, std::size_t width)
convert an integer to bit-vector representation with given width This uses two's complement for negat...
Definition: arith_tools.cpp:380
fixedbv_spect::fixedbv_spect
fixedbv_spect()
Definition: fixedbv.h:24
format_spect::min_width
unsigned min_width
Definition: format_spec.h:18
fixedbvt::operator*=
fixedbvt & operator*=(const fixedbvt &other)
Definition: fixedbv.cpp:96
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
bitvector_types.h
Pre-defined bitvector types.
std_types.h
Pre-defined types.
fixedbv_spect::width
std::size_t width
Definition: fixedbv.h:22
fixedbvt::v
mp_integer v
Definition: fixedbv.h:100
bitvector_typet::set_width
void set_width(std::size_t width)
Definition: std_types.h:842
fixedbv_spect
Definition: fixedbv.h:20
fixedbv_typet
Fixed-width bit-vector with signed fixed-point interpretation.
Definition: bitvector_types.h:261
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:837
bvrep2integer
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
Definition: arith_tools.cpp:402
fixedbvt::operator==
bool operator==(int i) const
Definition: fixedbv.cpp:130
fixedbvt::from_expr
void from_expr(const constant_exprt &expr)
Definition: fixedbv.cpp:27
fixedbv_typet::get_integer_bits
std::size_t get_integer_bits() const
Definition: bitvector_types.cpp:19
fixedbvt::round
void round(const fixedbv_spect &dest_spec)
Definition: fixedbv.cpp:53
power
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
Definition: arith_tools.cpp:195
fixedbvt::spec
fixedbv_spect spec
Definition: fixedbv.h:44
fixedbvt
Definition: fixedbv.h:42
constant_exprt
A constant literal expression.
Definition: std_expr.h:2667
std_expr.h
API to expression classes.
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:2675
fixedbvt::format
std::string format(const format_spect &format_spec) const
Definition: fixedbv.cpp:135
integer2string
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106