cprover
mp_arith.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 "mp_arith.h"
10 
11 #include <cstdlib>
12 #include <cctype>
13 #include <cassert>
14 
15 #include <sstream>
16 #include <ostream>
17 #include <limits>
18 
19 #include "arith_tools.h"
20 
22 {
23  mp_integer power=::power(2, b);
24 
25  if(a>=0)
26  return a/power;
27  else
28  {
29  // arithmetic shift right isn't division for negative numbers!
30  // http://en.wikipedia.org/wiki/Arithmetic_shift
31 
32  if((a%power)==0)
33  return a/power;
34  else
35  return a/power-1;
36  }
37 }
38 
40 {
41  return a*power(2, b);
42 }
43 
44 std::ostream &operator<<(std::ostream &out, const mp_integer &n)
45 {
46  out << integer2string(n);
47  return out;
48 }
49 
53 const mp_integer string2integer(const std::string &n, unsigned base)
54 {
55  for(unsigned i=0; i<n.size(); i++)
56  if(!(isalnum(n[i]) || (n[i]=='-' && i==0)))
57  return 0;
58 
59  return mp_integer(n.c_str(), base);
60 }
61 
63 const std::string integer2binary(const mp_integer &n, std::size_t width)
64 {
65  mp_integer a(n);
66 
67  if(width==0)
68  return "";
69 
70  bool neg=a.is_negative();
71 
72  if(neg)
73  {
74  a.negate();
75  a=a-1;
76  }
77 
78  std::size_t len = a.digits(2) + 2;
79  char *buffer=new char[len];
80  char *s = a.as_string(buffer, len, 2);
81 
82  std::string result(s);
83 
84  delete[] buffer;
85 
86  if(result.size()<width)
87  {
88  std::string fill;
89  fill.resize(width-result.size(), '0');
90  result=fill+result;
91  }
92  else if(result.size()>width)
93  result=result.substr(result.size()-width, width);
94 
95  if(neg)
96  {
97  for(std::size_t i=0; i<result.size(); i++)
98  result[i]=(result[i]=='0')?'1':'0';
99  }
100 
101  return result;
102 }
103 
104 const std::string integer2string(const mp_integer &n, unsigned base)
105 {
106  unsigned len = n.digits(base) + 2;
107  char *buffer=new char[len];
108  char *s = n.as_string(buffer, len, base);
109 
110  std::string result(s);
111 
112  delete[] buffer;
113 
114  return result;
115 }
116 
120 const mp_integer binary2integer(const std::string &n, bool is_signed)
121 {
122  if(n.empty())
123  return 0;
124 
125  if(n.size()<=(sizeof(unsigned long)*8))
126  {
127  // this is a tuned implementation for short integers
128 
129  unsigned long mask=1;
130  mask=mask << (n.size()-1);
131  mp_integer top_bit=(n[0]=='1') ? mask : 0;
132  if(is_signed)
133  top_bit.negate();
134  mask>>=1;
135  unsigned long other_bits=0;
136 
137  for(std::string::const_iterator it=++n.begin();
138  it!=n.end();
139  ++it)
140  {
141  if(*it=='1')
142  other_bits+=mask;
143  else if(*it!='0')
144  return 0;
145 
146  mask>>=1;
147  }
148 
149  return top_bit+other_bits;
150  }
151 
152  #if 0
153 
154  mp_integer mask=1;
155  mask=mask << (n.size()-1);
156  mp_integer result=(n[0]=='1') ? mask : 0;
157  if(is_signed)
158  result.negate();
159  mask=mask>>1;
160 
161  for(std::string::const_iterator it=++n.begin();
162  it!=n.end();
163  ++it)
164  {
165  if(*it=='1')
166  result+=mask;
167 
168  mask=mask>>1;
169  }
170 
171  return result;
172 
173  #else
174  if(n.find_first_not_of("01")!=std::string::npos)
175  return 0;
176 
177  if(is_signed && n[0]=='1')
178  {
179  mp_integer result(n.c_str()+1, 2);
180  result-=mp_integer(1)<<(n.size()-1);
181  return result;
182  }
183  else
184  return BigInt(n.c_str(), 2);
185 
186  #endif
187 }
188 
189 mp_integer::ullong_t integer2ulong(const mp_integer &n)
190 {
191  assert(n.is_ulong());
192  return n.to_ulong();
193 }
194 
195 std::size_t integer2size_t(const mp_integer &n)
196 {
197  assert(n>=0);
198  mp_integer::ullong_t ull=integer2ulong(n);
199  assert(ull <= std::numeric_limits<std::size_t>::max());
200  return (std::size_t)ull;
201 }
202 
203 unsigned integer2unsigned(const mp_integer &n)
204 {
205  assert(n>=0);
206  mp_integer::ullong_t ull=integer2ulong(n);
207  assert(ull <= std::numeric_limits<unsigned>::max());
208  return (unsigned)ull;
209 }
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition: util.cpp:45
BigInt mp_integer
Definition: mp_arith.h:19
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:53
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:104
mp_integer::ullong_t integer2ulong(const mp_integer &n)
Definition: mp_arith.cpp:189
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
Definition: mp_arith.cpp:120
mp_integer operator<<(const mp_integer &a, const mp_integer &b)
Definition: mp_arith.cpp:39
mp_integer operator>>(const mp_integer &a, const mp_integer &b)
Definition: mp_arith.cpp:21
unsigned integer2unsigned(const mp_integer &n)
Definition: mp_arith.cpp:203
const std::string integer2binary(const mp_integer &n, std::size_t width)
Definition: mp_arith.cpp:63
literalt neg(literalt a)
Definition: literal.h:192
std::size_t integer2size_t(const mp_integer &n)
Definition: mp_arith.cpp:195
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.