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 "std_types.h"
12 #include "std_expr.h"
13 #include "arith_tools.h"
14 
16 {
18  width=type.get_width();
19 }
20 
22 {
23  from_expr(expr);
24 }
25 
27 {
29  v=binary2integer(id2string(expr.get_value()), true);
30 }
31 
33 {
34  v=i*power(2, spec.get_fraction_bits());
35 }
36 
38 {
39  // this rounds to zero, i.e., we just divide
40  return v/power(2, spec.get_fraction_bits());
41 }
42 
44 {
45  fixedbv_typet type;
46  type.set_width(spec.width);
48  constant_exprt expr(type);
49  assert(spec.width!=0);
51  return expr;
52 }
53 
54 void fixedbvt::round(const fixedbv_spect &dest_spec)
55 {
56  std::size_t old_fraction_bits=spec.width-spec.integer_bits;
57  std::size_t new_fraction_bits=dest_spec.width-dest_spec.integer_bits;
58 
59  mp_integer result;
60 
61  if(new_fraction_bits>old_fraction_bits)
62  result=v*power(2, new_fraction_bits-old_fraction_bits);
63  else if(new_fraction_bits<old_fraction_bits)
64  {
65  // may need to round
66  mp_integer p=power(2, old_fraction_bits-new_fraction_bits);
67  mp_integer div=v/p;
68  mp_integer rem=v%p;
69  if(rem<0)
70  rem=-rem;
71 
72  if(rem*2>=p)
73  {
74  if(v<0)
75  --div;
76  else
77  ++div;
78  }
79 
80  result=div;
81  }
82  else // new_faction_bits==old_fraction_vits
83  {
84  // no change!
85  result=v;
86  }
87 
88  v=result;
89  spec=dest_spec;
90 }
91 
93 {
94  v=-v;
95 }
96 
98 {
99  v*=o.v;
100 
101  fixedbv_spect old_spec=spec;
102 
103  spec.width+=o.spec.width;
105 
106  round(old_spec);
107 
108  return *this;
109 }
110 
112 {
113  v*=power(2, o.spec.get_fraction_bits());
114  v/=o.v;
115 
116  return *this;
117 }
118 
119 bool fixedbvt::operator==(int i) const
120 {
121  return v==power(2, spec.get_fraction_bits())*i;
122 }
123 
124 std::string fixedbvt::format(
125  const format_spect &format_spec) const
126 {
127  std::string dest;
128  std::size_t fraction_bits=spec.get_fraction_bits();
129 
130  mp_integer int_value=v;
131  mp_integer factor=power(2, fraction_bits);
132 
133  if(int_value.is_negative())
134  {
135  dest+='-';
136  int_value.negate();
137  }
138 
139  std::string base_10_string=
140  integer2string(int_value*power(10, fraction_bits)/factor);
141 
142  while(base_10_string.size()<=fraction_bits)
143  base_10_string="0"+base_10_string;
144 
145  std::string integer_part=
146  std::string(base_10_string, 0, base_10_string.size()-fraction_bits);
147 
148  std::string fraction_part=
149  std::string(base_10_string, base_10_string.size()-fraction_bits);
150 
151  dest+=integer_part;
152 
153  // strip trailing zeros
154  while(!fraction_part.empty() &&
155  fraction_part[fraction_part.size()-1]=='0')
156  fraction_part.resize(fraction_part.size()-1);
157 
158  if(!fraction_part.empty())
159  dest+="."+fraction_part;
160 
161  while(dest.size()<format_spec.min_width)
162  dest=" "+dest;
163 
164  return dest;
165 }
std::size_t get_fraction_bits() const
Definition: fixedbv.h:35
BigInt mp_integer
Definition: mp_arith.h:22
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
fixedbvt & operator*=(const fixedbvt &other)
Definition: fixedbv.cpp:97
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106
std::size_t get_integer_bits() const
Definition: std_types.cpp:15
const irep_idt & get_value() const
Definition: std_expr.h:4439
void from_expr(const constant_exprt &expr)
Definition: fixedbv.cpp:26
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
Definition: mp_arith.cpp:120
typet & type()
Definition: expr.h:56
A constant literal expression.
Definition: std_expr.h:4422
bool operator==(int i) const
Definition: fixedbv.cpp:119
void round(const fixedbv_spect &dest_spec)
Definition: fixedbv.cpp:54
void set_value(const irep_idt &value)
Definition: std_expr.h:4444
fixedbv_spect spec
Definition: fixedbv.h:44
void from_integer(const mp_integer &i)
Definition: fixedbv.cpp:32
fixedbvt & operator/=(const fixedbvt &other)
Definition: fixedbv.cpp:111
void set_integer_bits(std::size_t b)
Definition: std_types.h:1327
API to expression classes.
std::string format(const format_spect &format_spec) const
Definition: fixedbv.cpp:124
std::size_t integer_bits
Definition: fixedbv.h:22
constant_exprt to_expr() const
Definition: fixedbv.cpp:43
Fixed-width bit-vector with signed fixed-point interpretation.
Definition: std_types.h:1313
std::size_t get_width() const
Definition: std_types.h:1138
mp_integer to_integer() const
Definition: fixedbv.cpp:37
unsigned min_width
Definition: format_spec.h:18
API to type classes.
const fixedbv_typet & to_fixedbv_type(const typet &type)
Cast a generic typet to a fixedbv_typet.
Definition: std_types.h:1343
std::size_t width
Definition: fixedbv.h:22
const std::string integer2binary(const mp_integer &n, std::size_t width)
Definition: mp_arith.cpp:67
void negate()
Definition: fixedbv.cpp:92
fixedbv_spect()
Definition: fixedbv.h:24
mp_integer v
Definition: fixedbv.h:100
fixedbvt()
Definition: fixedbv.h:46
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
void set_width(std::size_t width)
Definition: std_types.h:1143