1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Martin Brain, Aina Niemetz |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* SymFPU glue code for floating-point values. |
14 |
|
*/ |
15 |
|
|
16 |
|
#if CVC5_USE_SYMFPU |
17 |
|
|
18 |
|
#include "util/floatingpoint_literal_symfpu_traits.h" |
19 |
|
|
20 |
|
#include "base/check.h" |
21 |
|
|
22 |
|
namespace cvc5 { |
23 |
|
namespace symfpuLiteral { |
24 |
|
|
25 |
|
template <bool isSigned> |
26 |
274537 |
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::one( |
27 |
|
const Cvc5BitWidth& w) |
28 |
|
{ |
29 |
274537 |
return wrappedBitVector<isSigned>(w, 1); |
30 |
|
} |
31 |
|
|
32 |
|
template <bool isSigned> |
33 |
150192 |
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::zero( |
34 |
|
const Cvc5BitWidth& w) |
35 |
|
{ |
36 |
150192 |
return wrappedBitVector<isSigned>(w, 0); |
37 |
|
} |
38 |
|
|
39 |
|
template <bool isSigned> |
40 |
18225 |
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::allOnes( |
41 |
|
const Cvc5BitWidth& w) |
42 |
|
{ |
43 |
18225 |
return ~wrappedBitVector<isSigned>::zero(w); |
44 |
|
} |
45 |
|
|
46 |
|
template <bool isSigned> |
47 |
10322 |
Cvc5Prop wrappedBitVector<isSigned>::isAllOnes() const |
48 |
|
{ |
49 |
10322 |
return (*this == wrappedBitVector<isSigned>::allOnes(getWidth())); |
50 |
|
} |
51 |
|
template <bool isSigned> |
52 |
48756 |
Cvc5Prop wrappedBitVector<isSigned>::isAllZeros() const |
53 |
|
{ |
54 |
48756 |
return (*this == wrappedBitVector<isSigned>::zero(getWidth())); |
55 |
|
} |
56 |
|
|
57 |
|
template <bool isSigned> |
58 |
9 |
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::maxValue( |
59 |
|
const Cvc5BitWidth& w) |
60 |
|
{ |
61 |
|
if (isSigned) |
62 |
|
{ |
63 |
18 |
BitVector base(w - 1, 0U); |
64 |
9 |
return wrappedBitVector<true>((~base).zeroExtend(1)); |
65 |
|
} |
66 |
|
else |
67 |
|
{ |
68 |
|
return wrappedBitVector<false>::allOnes(w); |
69 |
|
} |
70 |
|
} |
71 |
|
|
72 |
|
template <bool isSigned> |
73 |
21 |
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::minValue( |
74 |
|
const Cvc5BitWidth& w) |
75 |
|
{ |
76 |
|
if (isSigned) |
77 |
|
{ |
78 |
42 |
BitVector base(w, 1U); |
79 |
42 |
BitVector shiftAmount(w, w - 1); |
80 |
42 |
BitVector result(base.leftShift(shiftAmount)); |
81 |
21 |
return wrappedBitVector<true>(result); |
82 |
|
} |
83 |
|
else |
84 |
|
{ |
85 |
|
return wrappedBitVector<false>::zero(w); |
86 |
|
} |
87 |
|
} |
88 |
|
|
89 |
|
/*** Operators ***/ |
90 |
|
template <bool isSigned> |
91 |
207700 |
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator<<( |
92 |
|
const wrappedBitVector<isSigned>& op) const |
93 |
|
{ |
94 |
207700 |
return BitVector::leftShift(op); |
95 |
|
} |
96 |
|
|
97 |
|
template <> |
98 |
|
wrappedBitVector<true> wrappedBitVector<true>::operator>>( |
99 |
|
const wrappedBitVector<true>& op) const |
100 |
|
{ |
101 |
|
return BitVector::arithRightShift(op); |
102 |
|
} |
103 |
|
|
104 |
|
template <> |
105 |
4747 |
wrappedBitVector<false> wrappedBitVector<false>::operator>>( |
106 |
|
const wrappedBitVector<false>& op) const |
107 |
|
{ |
108 |
4747 |
return BitVector::logicalRightShift(op); |
109 |
|
} |
110 |
|
|
111 |
|
template <bool isSigned> |
112 |
4496 |
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator|( |
113 |
|
const wrappedBitVector<isSigned>& op) const |
114 |
|
{ |
115 |
4496 |
return BitVector::operator|(op); |
116 |
|
} |
117 |
|
|
118 |
|
template <bool isSigned> |
119 |
44140 |
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator&( |
120 |
|
const wrappedBitVector<isSigned>& op) const |
121 |
|
{ |
122 |
44140 |
return BitVector::operator&(op); |
123 |
|
} |
124 |
|
|
125 |
|
template <bool isSigned> |
126 |
10834 |
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator+( |
127 |
|
const wrappedBitVector<isSigned>& op) const |
128 |
|
{ |
129 |
10834 |
return BitVector::operator+(op); |
130 |
|
} |
131 |
|
|
132 |
|
template <bool isSigned> |
133 |
258651 |
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator-( |
134 |
|
const wrappedBitVector<isSigned>& op) const |
135 |
|
{ |
136 |
258651 |
return BitVector::operator-(op); |
137 |
|
} |
138 |
|
|
139 |
|
template <bool isSigned> |
140 |
456 |
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator*( |
141 |
|
const wrappedBitVector<isSigned>& op) const |
142 |
|
{ |
143 |
456 |
return BitVector::operator*(op); |
144 |
|
} |
145 |
|
|
146 |
|
template <> |
147 |
189 |
wrappedBitVector<false> wrappedBitVector<false>::operator/( |
148 |
|
const wrappedBitVector<false>& op) const |
149 |
|
{ |
150 |
189 |
return BitVector::unsignedDivTotal(op); |
151 |
|
} |
152 |
|
|
153 |
|
template <> |
154 |
189 |
wrappedBitVector<false> wrappedBitVector<false>::operator%( |
155 |
|
const wrappedBitVector<false>& op) const |
156 |
|
{ |
157 |
189 |
return BitVector::unsignedRemTotal(op); |
158 |
|
} |
159 |
|
|
160 |
|
template <bool isSigned> |
161 |
107141 |
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator-(void) const |
162 |
|
{ |
163 |
107141 |
return BitVector::operator-(); |
164 |
|
} |
165 |
|
|
166 |
|
template <bool isSigned> |
167 |
21717 |
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator~(void) const |
168 |
|
{ |
169 |
21717 |
return BitVector::operator~(); |
170 |
|
} |
171 |
|
|
172 |
|
template <bool isSigned> |
173 |
140 |
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::increment() const |
174 |
|
{ |
175 |
140 |
return *this + wrappedBitVector<isSigned>::one(getWidth()); |
176 |
|
} |
177 |
|
|
178 |
|
template <bool isSigned> |
179 |
21189 |
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::decrement() const |
180 |
|
{ |
181 |
21189 |
return *this - wrappedBitVector<isSigned>::one(getWidth()); |
182 |
|
} |
183 |
|
|
184 |
|
template <bool isSigned> |
185 |
1511 |
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::signExtendRightShift( |
186 |
|
const wrappedBitVector<isSigned>& op) const |
187 |
|
{ |
188 |
1511 |
return BitVector::arithRightShift(BitVector(getWidth(), op)); |
189 |
|
} |
190 |
|
|
191 |
|
/*** Modular opertaions ***/ |
192 |
|
// No overflow checking so these are the same as other operations |
193 |
|
template <bool isSigned> |
194 |
24859 |
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularLeftShift( |
195 |
|
const wrappedBitVector<isSigned>& op) const |
196 |
|
{ |
197 |
24859 |
return *this << op; |
198 |
|
} |
199 |
|
|
200 |
|
template <bool isSigned> |
201 |
550 |
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularRightShift( |
202 |
|
const wrappedBitVector<isSigned>& op) const |
203 |
|
{ |
204 |
550 |
return *this >> op; |
205 |
|
} |
206 |
|
|
207 |
|
template <bool isSigned> |
208 |
|
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularIncrement() const |
209 |
|
{ |
210 |
|
return increment(); |
211 |
|
} |
212 |
|
|
213 |
|
template <bool isSigned> |
214 |
19181 |
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularDecrement() const |
215 |
|
{ |
216 |
19181 |
return decrement(); |
217 |
|
} |
218 |
|
|
219 |
|
template <bool isSigned> |
220 |
4741 |
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularAdd( |
221 |
|
const wrappedBitVector<isSigned>& op) const |
222 |
|
{ |
223 |
4741 |
return *this + op; |
224 |
|
} |
225 |
|
|
226 |
|
template <bool isSigned> |
227 |
4609 |
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularNegate() const |
228 |
|
{ |
229 |
4609 |
return -(*this); |
230 |
|
} |
231 |
|
|
232 |
|
/*** Comparisons ***/ |
233 |
|
|
234 |
|
template <bool isSigned> |
235 |
102263 |
Cvc5Prop wrappedBitVector<isSigned>::operator==( |
236 |
|
const wrappedBitVector<isSigned>& op) const |
237 |
|
{ |
238 |
102263 |
return BitVector::operator==(op); |
239 |
|
} |
240 |
|
|
241 |
|
template <> |
242 |
152351 |
Cvc5Prop wrappedBitVector<true>::operator<=( |
243 |
|
const wrappedBitVector<true>& op) const |
244 |
|
{ |
245 |
152351 |
return signedLessThanEq(op); |
246 |
|
} |
247 |
|
|
248 |
|
template <> |
249 |
1074 |
Cvc5Prop wrappedBitVector<true>::operator>=( |
250 |
|
const wrappedBitVector<true>& op) const |
251 |
|
{ |
252 |
1074 |
return !(signedLessThan(op)); |
253 |
|
} |
254 |
|
|
255 |
|
template <> |
256 |
5245 |
Cvc5Prop wrappedBitVector<true>::operator<( |
257 |
|
const wrappedBitVector<true>& op) const |
258 |
|
{ |
259 |
5245 |
return signedLessThan(op); |
260 |
|
} |
261 |
|
|
262 |
|
template <> |
263 |
5013 |
Cvc5Prop wrappedBitVector<true>::operator>( |
264 |
|
const wrappedBitVector<true>& op) const |
265 |
|
{ |
266 |
5013 |
return !(signedLessThanEq(op)); |
267 |
|
} |
268 |
|
|
269 |
|
template <> |
270 |
380 |
Cvc5Prop wrappedBitVector<false>::operator<=( |
271 |
|
const wrappedBitVector<false>& op) const |
272 |
|
{ |
273 |
380 |
return unsignedLessThanEq(op); |
274 |
|
} |
275 |
|
|
276 |
|
template <> |
277 |
4710 |
Cvc5Prop wrappedBitVector<false>::operator>=( |
278 |
|
const wrappedBitVector<false>& op) const |
279 |
|
{ |
280 |
4710 |
return !(unsignedLessThan(op)); |
281 |
|
} |
282 |
|
|
283 |
|
template <> |
284 |
1125 |
Cvc5Prop wrappedBitVector<false>::operator<( |
285 |
|
const wrappedBitVector<false>& op) const |
286 |
|
{ |
287 |
1125 |
return unsignedLessThan(op); |
288 |
|
} |
289 |
|
|
290 |
|
template <> |
291 |
20 |
Cvc5Prop wrappedBitVector<false>::operator>( |
292 |
|
const wrappedBitVector<false>& op) const |
293 |
|
{ |
294 |
20 |
return !(unsignedLessThanEq(op)); |
295 |
|
} |
296 |
|
|
297 |
|
/*** Type conversion ***/ |
298 |
|
|
299 |
|
// Node makes no distinction between signed and unsigned, thus ... |
300 |
|
template <bool isSigned> |
301 |
1367 |
wrappedBitVector<true> wrappedBitVector<isSigned>::toSigned(void) const |
302 |
|
{ |
303 |
1367 |
return wrappedBitVector<true>(*this); |
304 |
|
} |
305 |
|
|
306 |
|
template <bool isSigned> |
307 |
26125 |
wrappedBitVector<false> wrappedBitVector<isSigned>::toUnsigned(void) const |
308 |
|
{ |
309 |
26125 |
return wrappedBitVector<false>(*this); |
310 |
|
} |
311 |
|
|
312 |
|
/*** Bit hacks ***/ |
313 |
|
|
314 |
|
template <bool isSigned> |
315 |
65567 |
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::extend( |
316 |
|
Cvc5BitWidth extension) const |
317 |
|
{ |
318 |
|
if (isSigned) |
319 |
|
{ |
320 |
15511 |
return BitVector::signExtend(extension); |
321 |
|
} |
322 |
|
else |
323 |
|
{ |
324 |
50056 |
return BitVector::zeroExtend(extension); |
325 |
|
} |
326 |
|
} |
327 |
|
|
328 |
|
template <bool isSigned> |
329 |
1484 |
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::contract( |
330 |
|
Cvc5BitWidth reduction) const |
331 |
|
{ |
332 |
1484 |
Assert(getWidth() > reduction); |
333 |
|
|
334 |
1484 |
return extract((getWidth() - 1) - reduction, 0); |
335 |
|
} |
336 |
|
|
337 |
|
template <bool isSigned> |
338 |
20773 |
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::resize( |
339 |
|
Cvc5BitWidth newSize) const |
340 |
|
{ |
341 |
20773 |
Cvc5BitWidth width = getWidth(); |
342 |
|
|
343 |
20773 |
if (newSize > width) |
344 |
|
{ |
345 |
20773 |
return extend(newSize - width); |
346 |
|
} |
347 |
|
else if (newSize < width) |
348 |
|
{ |
349 |
|
return contract(width - newSize); |
350 |
|
} |
351 |
|
else |
352 |
|
{ |
353 |
|
return *this; |
354 |
|
} |
355 |
|
} |
356 |
|
|
357 |
|
template <bool isSigned> |
358 |
27622 |
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::matchWidth( |
359 |
|
const wrappedBitVector<isSigned>& op) const |
360 |
|
{ |
361 |
27622 |
Assert(getWidth() <= op.getWidth()); |
362 |
27622 |
return extend(op.getWidth() - getWidth()); |
363 |
|
} |
364 |
|
|
365 |
|
template <bool isSigned> |
366 |
15858 |
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::append( |
367 |
|
const wrappedBitVector<isSigned>& op) const |
368 |
|
{ |
369 |
15858 |
return BitVector::concat(op); |
370 |
|
} |
371 |
|
|
372 |
|
// Inclusive of end points, thus if the same, extracts just one bit |
373 |
|
template <bool isSigned> |
374 |
48399 |
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::extract( |
375 |
|
Cvc5BitWidth upper, Cvc5BitWidth lower) const |
376 |
|
{ |
377 |
48399 |
Assert(upper >= lower); |
378 |
48399 |
return BitVector::extract(upper, lower); |
379 |
|
} |
380 |
|
|
381 |
|
// Explicit instantiation |
382 |
|
template class wrappedBitVector<true>; |
383 |
|
template class wrappedBitVector<false>; |
384 |
|
|
385 |
3140 |
traits::rm traits::RNE(void) { return ::cvc5::ROUND_NEAREST_TIES_TO_EVEN; }; |
386 |
1951 |
traits::rm traits::RNA(void) { return ::cvc5::ROUND_NEAREST_TIES_TO_AWAY; }; |
387 |
1714 |
traits::rm traits::RTP(void) { return ::cvc5::ROUND_TOWARD_POSITIVE; }; |
388 |
2751 |
traits::rm traits::RTN(void) { return ::cvc5::ROUND_TOWARD_NEGATIVE; }; |
389 |
1490 |
traits::rm traits::RTZ(void) { return ::cvc5::ROUND_TOWARD_ZERO; }; |
390 |
|
// This is a literal back-end so props are actually bools |
391 |
|
// so these can be handled in the same way as the internal assertions above |
392 |
|
|
393 |
53960 |
void traits::precondition(const traits::prop& p) |
394 |
|
{ |
395 |
53960 |
Assert(p); |
396 |
53960 |
return; |
397 |
|
} |
398 |
11485 |
void traits::postcondition(const traits::prop& p) |
399 |
|
{ |
400 |
11485 |
Assert(p); |
401 |
11485 |
return; |
402 |
|
} |
403 |
53399 |
void traits::invariant(const traits::prop& p) |
404 |
|
{ |
405 |
53399 |
Assert(p); |
406 |
53399 |
return; |
407 |
|
} |
408 |
|
} // namespace symfpuLiteral |
409 |
28194 |
} // namespace cvc5 |
410 |
|
#endif |