1 /********************* */
2 /*! \file floatingpoint.cpp
4 ** Top contributors (to current version):
5 ** Martin Brain, Tim King
6 ** Copyright (c) 2013 University of Oxford
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
9 ** in the top-level source directory) and their institutional affiliations.
10 ** All rights reserved. See the file COPYING in the top-level source
11 ** directory for licensing information.\endverbatim
13 ** \brief [[ Implementations of the utility functions for working with floating point theories. ]]
17 #include "util/floatingpoint.h"
18 #include "base/cvc4_assert.h"
19 #include "util/integer.h"
23 #ifdef CVC4_USE_SYMFPU
24 #include "symfpu/core/add.h"
25 #include "symfpu/core/classify.h"
26 #include "symfpu/core/compare.h"
27 #include "symfpu/core/convert.h"
28 #include "symfpu/core/divide.h"
29 #include "symfpu/core/fma.h"
30 #include "symfpu/core/ite.h"
31 #include "symfpu/core/multiply.h"
32 #include "symfpu/core/packing.h"
33 #include "symfpu/core/remainder.h"
34 #include "symfpu/core/sign.h"
35 #include "symfpu/core/sqrt.h"
36 #include "symfpu/utils/numberOfRoundingModes.h"
37 #include "symfpu/utils/properties.h"
40 #ifdef CVC4_USE_SYMFPU
43 #define CVC4_LIT_ITE_DFN(T) \
45 struct ite<::CVC4::symfpuLiteral::prop, T> \
47 static const T &iteOp(const ::CVC4::symfpuLiteral::prop &cond, \
51 return cond ? l : r; \
55 CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::rm
);
56 CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::prop
);
57 CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::sbv
);
58 CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::ubv
);
60 #undef CVC4_LIT_ITE_DFN
64 #ifndef CVC4_USE_SYMFPU
65 #define PRECONDITION(X) Assert((X))
70 FloatingPointSize::FloatingPointSize (unsigned _e
, unsigned _s
) : e(_e
), s(_s
)
72 PrettyCheckArgument(validExponentSize(_e
),_e
,"Invalid exponent size : %d",_e
);
73 PrettyCheckArgument(validSignificandSize(_s
),_s
,"Invalid significand size : %d",_s
);
76 FloatingPointSize::FloatingPointSize (const FloatingPointSize
&old
) : e(old
.e
), s(old
.s
)
78 PrettyCheckArgument(validExponentSize(e
),e
,"Invalid exponent size : %d",e
);
79 PrettyCheckArgument(validSignificandSize(s
),s
,"Invalid significand size : %d",s
);
82 namespace symfpuLiteral
{
84 // To simplify the property macros
87 template <bool isSigned
>
88 wrappedBitVector
<isSigned
> wrappedBitVector
<isSigned
>::one(const bwt
&w
)
90 return wrappedBitVector
<isSigned
>(w
, 1);
93 template <bool isSigned
>
94 wrappedBitVector
<isSigned
> wrappedBitVector
<isSigned
>::zero(const bwt
&w
)
96 return wrappedBitVector
<isSigned
>(w
, 0);
99 template <bool isSigned
>
100 wrappedBitVector
<isSigned
> wrappedBitVector
<isSigned
>::allOnes(const bwt
&w
)
102 return ~wrappedBitVector
<isSigned
>::zero(w
);
105 template <bool isSigned
>
106 prop wrappedBitVector
<isSigned
>::isAllOnes() const
108 return (*this == wrappedBitVector
<isSigned
>::allOnes(this->getWidth()));
110 template <bool isSigned
>
111 prop wrappedBitVector
<isSigned
>::isAllZeros() const
113 return (*this == wrappedBitVector
<isSigned
>::zero(this->getWidth()));
116 template <bool isSigned
>
117 wrappedBitVector
<isSigned
> wrappedBitVector
<isSigned
>::maxValue(const bwt
&w
)
121 BitVector
base(w
- 1, 0U);
122 return wrappedBitVector
<true>((~base
).zeroExtend(1));
126 return wrappedBitVector
<false>::allOnes(w
);
130 template <bool isSigned
>
131 wrappedBitVector
<isSigned
> wrappedBitVector
<isSigned
>::minValue(const bwt
&w
)
135 BitVector
base(w
, 1U);
136 BitVector
shiftAmount(w
, w
- 1);
137 BitVector
result(base
.leftShift(shiftAmount
));
138 return wrappedBitVector
<true>(result
);
142 return wrappedBitVector
<false>::zero(w
);
147 template <bool isSigned
>
148 wrappedBitVector
<isSigned
> wrappedBitVector
<isSigned
>::operator<<(
149 const wrappedBitVector
<isSigned
> &op
) const
151 return this->BitVector::leftShift(op
);
155 wrappedBitVector
<true> wrappedBitVector
<true>::operator>>(
156 const wrappedBitVector
<true> &op
) const
158 return this->BitVector::arithRightShift(op
);
162 wrappedBitVector
<false> wrappedBitVector
<false>::operator>>(
163 const wrappedBitVector
<false> &op
) const
165 return this->BitVector::logicalRightShift(op
);
168 template <bool isSigned
>
169 wrappedBitVector
<isSigned
> wrappedBitVector
<isSigned
>::operator|(
170 const wrappedBitVector
<isSigned
> &op
) const
172 return this->BitVector::operator|(op
);
175 template <bool isSigned
>
176 wrappedBitVector
<isSigned
> wrappedBitVector
<isSigned
>::operator&(
177 const wrappedBitVector
<isSigned
> &op
) const
179 return this->BitVector::operator&(op
);
182 template <bool isSigned
>
183 wrappedBitVector
<isSigned
> wrappedBitVector
<isSigned
>::operator+(
184 const wrappedBitVector
<isSigned
> &op
) const
186 return this->BitVector::operator+(op
);
189 template <bool isSigned
>
190 wrappedBitVector
<isSigned
> wrappedBitVector
<isSigned
>::operator-(
191 const wrappedBitVector
<isSigned
> &op
) const
193 return this->BitVector::operator-(op
);
196 template <bool isSigned
>
197 wrappedBitVector
<isSigned
> wrappedBitVector
<isSigned
>::operator*(
198 const wrappedBitVector
<isSigned
> &op
) const
200 return this->BitVector::operator*(op
);
204 wrappedBitVector
<false> wrappedBitVector
<false>::operator/(
205 const wrappedBitVector
<false> &op
) const
207 return this->BitVector::unsignedDivTotal(op
);
211 wrappedBitVector
<false> wrappedBitVector
<false>::operator%(
212 const wrappedBitVector
<false> &op
) const
214 return this->BitVector::unsignedRemTotal(op
);
217 template <bool isSigned
>
218 wrappedBitVector
<isSigned
> wrappedBitVector
<isSigned
>::operator-(void) const
220 return this->BitVector::operator-();
223 template <bool isSigned
>
224 wrappedBitVector
<isSigned
> wrappedBitVector
<isSigned
>::operator~(void)const
226 return this->BitVector::operator~();
229 template <bool isSigned
>
230 wrappedBitVector
<isSigned
> wrappedBitVector
<isSigned
>::increment() const
232 return *this + wrappedBitVector
<isSigned
>::one(this->getWidth());
235 template <bool isSigned
>
236 wrappedBitVector
<isSigned
> wrappedBitVector
<isSigned
>::decrement() const
238 return *this - wrappedBitVector
<isSigned
>::one(this->getWidth());
241 template <bool isSigned
>
242 wrappedBitVector
<isSigned
> wrappedBitVector
<isSigned
>::signExtendRightShift(
243 const wrappedBitVector
<isSigned
> &op
) const
245 return this->BitVector::arithRightShift(BitVector(this->getWidth(), op
));
248 /*** Modular opertaions ***/
249 // No overflow checking so these are the same as other operations
250 template <bool isSigned
>
251 wrappedBitVector
<isSigned
> wrappedBitVector
<isSigned
>::modularLeftShift(
252 const wrappedBitVector
<isSigned
> &op
) const
257 template <bool isSigned
>
258 wrappedBitVector
<isSigned
> wrappedBitVector
<isSigned
>::modularRightShift(
259 const wrappedBitVector
<isSigned
> &op
) const
264 template <bool isSigned
>
265 wrappedBitVector
<isSigned
> wrappedBitVector
<isSigned
>::modularIncrement() const
267 return this->increment();
270 template <bool isSigned
>
271 wrappedBitVector
<isSigned
> wrappedBitVector
<isSigned
>::modularDecrement() const
273 return this->decrement();
276 template <bool isSigned
>
277 wrappedBitVector
<isSigned
> wrappedBitVector
<isSigned
>::modularAdd(
278 const wrappedBitVector
<isSigned
> &op
) const
283 template <bool isSigned
>
284 wrappedBitVector
<isSigned
> wrappedBitVector
<isSigned
>::modularNegate() const
289 /*** Comparisons ***/
291 template <bool isSigned
>
292 prop wrappedBitVector
<isSigned
>::operator==(
293 const wrappedBitVector
<isSigned
> &op
) const
295 return this->BitVector::operator==(op
);
299 prop wrappedBitVector
<true>::operator<=(const wrappedBitVector
<true> &op
) const
301 return this->signedLessThanEq(op
);
305 prop wrappedBitVector
<true>::operator>=(const wrappedBitVector
<true> &op
) const
307 return !(this->signedLessThan(op
));
311 prop wrappedBitVector
<true>::operator<(const wrappedBitVector
<true> &op
) const
313 return this->signedLessThan(op
);
317 prop wrappedBitVector
<true>::operator>(const wrappedBitVector
<true> &op
) const
319 return !(this->signedLessThanEq(op
));
323 prop wrappedBitVector
<false>::operator<=(
324 const wrappedBitVector
<false> &op
) const
326 return this->unsignedLessThanEq(op
);
330 prop wrappedBitVector
<false>::operator>=(
331 const wrappedBitVector
<false> &op
) const
333 return !(this->unsignedLessThan(op
));
337 prop wrappedBitVector
<false>::operator<(const wrappedBitVector
<false> &op
) const
339 return this->unsignedLessThan(op
);
343 prop wrappedBitVector
<false>::operator>(const wrappedBitVector
<false> &op
) const
345 return !(this->unsignedLessThanEq(op
));
348 /*** Type conversion ***/
349 // CVC4 nodes make no distinction between signed and unsigned, thus ...
350 template <bool isSigned
>
351 wrappedBitVector
<true> wrappedBitVector
<isSigned
>::toSigned(void) const
353 return wrappedBitVector
<true>(*this);
356 template <bool isSigned
>
357 wrappedBitVector
<false> wrappedBitVector
<isSigned
>::toUnsigned(void) const
359 return wrappedBitVector
<false>(*this);
364 template <bool isSigned
>
365 wrappedBitVector
<isSigned
> wrappedBitVector
<isSigned
>::extend(
370 return this->BitVector::signExtend(extension
);
374 return this->BitVector::zeroExtend(extension
);
378 template <bool isSigned
>
379 wrappedBitVector
<isSigned
> wrappedBitVector
<isSigned
>::contract(
382 PRECONDITION(this->getWidth() > reduction
);
384 return this->extract((this->getWidth() - 1) - reduction
, 0);
387 template <bool isSigned
>
388 wrappedBitVector
<isSigned
> wrappedBitVector
<isSigned
>::resize(bwt newSize
) const
390 bwt width
= this->getWidth();
394 return this->extend(newSize
- width
);
396 else if (newSize
< width
)
398 return this->contract(width
- newSize
);
406 template <bool isSigned
>
407 wrappedBitVector
<isSigned
> wrappedBitVector
<isSigned
>::matchWidth(
408 const wrappedBitVector
<isSigned
> &op
) const
410 PRECONDITION(this->getWidth() <= op
.getWidth());
411 return this->extend(op
.getWidth() - this->getWidth());
414 template <bool isSigned
>
415 wrappedBitVector
<isSigned
> wrappedBitVector
<isSigned
>::append(
416 const wrappedBitVector
<isSigned
> &op
) const
418 return this->BitVector::concat(op
);
421 // Inclusive of end points, thus if the same, extracts just one bit
422 template <bool isSigned
>
423 wrappedBitVector
<isSigned
> wrappedBitVector
<isSigned
>::extract(bwt upper
,
426 PRECONDITION(upper
>= lower
);
427 return this->BitVector::extract(upper
, lower
);
430 // Explicit instantiation
431 template class wrappedBitVector
<true>;
432 template class wrappedBitVector
<false>;
434 rm
traits::RNE(void) { return ::CVC4::roundNearestTiesToEven
; };
435 rm
traits::RNA(void) { return ::CVC4::roundNearestTiesToAway
; };
436 rm
traits::RTP(void) { return ::CVC4::roundTowardPositive
; };
437 rm
traits::RTN(void) { return ::CVC4::roundTowardNegative
; };
438 rm
traits::RTZ(void) { return ::CVC4::roundTowardZero
; };
439 // This is a literal back-end so props are actually bools
440 // so these can be handled in the same way as the internal assertions above
442 void traits::precondition(const prop
&p
)
447 void traits::postcondition(const prop
&p
)
452 void traits::invariant(const prop
&p
)
459 #ifndef CVC4_USE_SYMFPU
460 void FloatingPointLiteral::unfinished(void) const
462 Unimplemented("Floating-point literals not yet implemented.");
466 FloatingPoint::FloatingPoint(unsigned e
, unsigned s
, const BitVector
&bv
)
468 #ifdef CVC4_USE_SYMFPU
469 fpl(symfpu::unpack
<symfpuLiteral::traits
>(symfpuLiteral::fpt(e
, s
), bv
)),
477 static FloatingPointLiteral
constructorHelperBitVector(
478 const FloatingPointSize
&ct
,
479 const RoundingMode
&rm
,
483 #ifdef CVC4_USE_SYMFPU
486 return FloatingPointLiteral(
487 symfpu::convertSBVToFloat
<symfpuLiteral::traits
>(
488 symfpuLiteral::fpt(ct
),
489 symfpuLiteral::rm(rm
),
490 symfpuLiteral::sbv(bv
)));
494 return FloatingPointLiteral(
495 symfpu::convertUBVToFloat
<symfpuLiteral::traits
>(
496 symfpuLiteral::fpt(ct
),
497 symfpuLiteral::rm(rm
),
498 symfpuLiteral::ubv(bv
)));
501 return FloatingPointLiteral(2, 2, 0.0);
503 Unreachable("Constructor helper broken");
506 FloatingPoint::FloatingPoint (const FloatingPointSize
&ct
, const RoundingMode
&rm
, const BitVector
&bv
, bool signedBV
) :
507 fpl(constructorHelperBitVector(ct
, rm
, bv
, signedBV
)),
511 static FloatingPointLiteral
constructorHelperRational (const FloatingPointSize
&ct
, const RoundingMode
&rm
, const Rational
&ri
) {
516 #ifdef CVC4_USE_SYMFPU
517 return FloatingPointLiteral::makeZero(
518 ct
, false); // In keeping with the SMT-LIB standard
520 return FloatingPointLiteral(2,2,0.0);
523 #ifdef CVC4_USE_SYMFPU
524 int negative
= (r
.sgn() < 0) ? 1 : 0;
528 // Compute the exponent
531 Rational
working(1,1);
535 } else if ( r
< working
) {
536 while (r
< working
) {
541 while (r
>= working
) {
549 Assert(working
<= r
);
550 Assert(r
< working
* two
);
552 // Work out the number of bits required to represent the exponent for a normal number
553 unsigned expBits
= 2; // No point starting with an invalid amount
555 Integer
doubleInt(2);
556 if (exp
.strictlyPositive()) {
557 Integer
representable(4); // 1 more than exactly representable with expBits
558 while (representable
<= exp
) {// hence <=
559 representable
*= doubleInt
;
562 } else if (exp
.strictlyNegative()) {
563 Integer
representable(-4); // Exactly representable with expBits + sign
564 // but -2^n and -(2^n - 1) are both subnormal
565 while ((representable
+ doubleInt
) > exp
) {
566 representable
*= doubleInt
;
570 ++expBits
; // To allow for sign
572 BitVector
exactExp(expBits
, exp
);
576 // Compute the significand.
577 unsigned sigBits
= ct
.significandWidth() + 2; // guard and sticky bits
578 BitVector
sig(sigBits
, 0U);
579 BitVector
one(sigBits
, 1U);
580 Rational
workingSig(0,1);
581 for (unsigned i
= 0; i
< sigBits
- 1; ++i
) {
582 Rational
mid(workingSig
+ working
);
589 sig
= sig
.leftShift(one
);
593 // Compute the sticky bit
594 Rational
remainder(r
- workingSig
);
595 Assert(Rational(0,1) <= remainder
);
597 if (!remainder
.isZero()) {
601 // Build an exact float
602 FloatingPointSize
exactFormat(expBits
, sigBits
);
604 // A small subtlety... if the format has expBits the unpacked format
605 // may have more to allow subnormals to be normalised.
607 #ifdef CVC4_USE_SYMFPU
609 FloatingPointLiteral::exponentWidth(exactFormat
) - expBits
;
611 FloatingPointLiteral
exactFloat(
612 negative
, exactExp
.signExtend(extension
), sig
);
615 FloatingPointLiteral
rounded(
616 symfpu::convertFloatToFloat(exactFormat
, ct
, rm
, exactFloat
));
619 Unreachable("no concrete implementation of FloatingPointLiteral");
622 Unreachable("Constructor helper broken");
625 FloatingPoint::FloatingPoint (const FloatingPointSize
&ct
, const RoundingMode
&rm
, const Rational
&r
) :
626 fpl(constructorHelperRational(ct
, rm
, r
)),
630 FloatingPoint
FloatingPoint::makeNaN (const FloatingPointSize
&t
) {
631 #ifdef CVC4_USE_SYMFPU
632 return FloatingPoint(
633 t
, symfpu::unpackedFloat
<symfpuLiteral::traits
>::makeNaN(t
));
635 return FloatingPoint(2, 2, BitVector(4U,0U));
639 FloatingPoint
FloatingPoint::makeInf (const FloatingPointSize
&t
, bool sign
) {
640 #ifdef CVC4_USE_SYMFPU
641 return FloatingPoint(
642 t
, symfpu::unpackedFloat
<symfpuLiteral::traits
>::makeInf(t
, sign
));
644 return FloatingPoint(2, 2, BitVector(4U,0U));
648 FloatingPoint
FloatingPoint::makeZero (const FloatingPointSize
&t
, bool sign
) {
649 #ifdef CVC4_USE_SYMFPU
650 return FloatingPoint(
651 t
, symfpu::unpackedFloat
<symfpuLiteral::traits
>::makeZero(t
, sign
));
653 return FloatingPoint(2, 2, BitVector(4U,0U));
658 /* Operations implemented using symfpu */
659 FloatingPoint
FloatingPoint::absolute (void) const {
660 #ifdef CVC4_USE_SYMFPU
661 return FloatingPoint(t
, symfpu::absolute
<symfpuLiteral::traits
>(t
, fpl
));
667 FloatingPoint
FloatingPoint::negate (void) const {
668 #ifdef CVC4_USE_SYMFPU
669 return FloatingPoint(t
, symfpu::negate
<symfpuLiteral::traits
>(t
, fpl
));
675 FloatingPoint
FloatingPoint::plus (const RoundingMode
&rm
, const FloatingPoint
&arg
) const {
676 #ifdef CVC4_USE_SYMFPU
677 Assert(this->t
== arg
.t
);
678 return FloatingPoint(
679 t
, symfpu::add
<symfpuLiteral::traits
>(t
, rm
, fpl
, arg
.fpl
, true));
685 FloatingPoint
FloatingPoint::sub (const RoundingMode
&rm
, const FloatingPoint
&arg
) const {
686 #ifdef CVC4_USE_SYMFPU
687 Assert(this->t
== arg
.t
);
688 return FloatingPoint(
689 t
, symfpu::add
<symfpuLiteral::traits
>(t
, rm
, fpl
, arg
.fpl
, false));
695 FloatingPoint
FloatingPoint::mult (const RoundingMode
&rm
, const FloatingPoint
&arg
) const {
696 #ifdef CVC4_USE_SYMFPU
697 Assert(this->t
== arg
.t
);
698 return FloatingPoint(
699 t
, symfpu::multiply
<symfpuLiteral::traits
>(t
, rm
, fpl
, arg
.fpl
));
705 FloatingPoint
FloatingPoint::fma (const RoundingMode
&rm
, const FloatingPoint
&arg1
, const FloatingPoint
&arg2
) const {
706 #ifdef CVC4_USE_SYMFPU
707 Assert(this->t
== arg1
.t
);
708 Assert(this->t
== arg2
.t
);
709 return FloatingPoint(
710 t
, symfpu::fma
<symfpuLiteral::traits
>(t
, rm
, fpl
, arg1
.fpl
, arg2
.fpl
));
716 FloatingPoint
FloatingPoint::div (const RoundingMode
&rm
, const FloatingPoint
&arg
) const {
717 #ifdef CVC4_USE_SYMFPU
718 Assert(this->t
== arg
.t
);
719 return FloatingPoint(
720 t
, symfpu::divide
<symfpuLiteral::traits
>(t
, rm
, fpl
, arg
.fpl
));
726 FloatingPoint
FloatingPoint::sqrt (const RoundingMode
&rm
) const {
727 #ifdef CVC4_USE_SYMFPU
728 return FloatingPoint(t
, symfpu::sqrt
<symfpuLiteral::traits
>(t
, rm
, fpl
));
734 FloatingPoint
FloatingPoint::rti (const RoundingMode
&rm
) const {
735 #ifdef CVC4_USE_SYMFPU
736 return FloatingPoint(
737 t
, symfpu::roundToIntegral
<symfpuLiteral::traits
>(t
, rm
, fpl
));
743 FloatingPoint
FloatingPoint::rem (const FloatingPoint
&arg
) const {
744 #ifdef CVC4_USE_SYMFPU
745 Assert(this->t
== arg
.t
);
746 return FloatingPoint(
747 t
, symfpu::remainder
<symfpuLiteral::traits
>(t
, fpl
, arg
.fpl
));
753 FloatingPoint
FloatingPoint::maxTotal (const FloatingPoint
&arg
, bool zeroCaseLeft
) const {
754 #ifdef CVC4_USE_SYMFPU
755 Assert(this->t
== arg
.t
);
756 return FloatingPoint(
757 t
, symfpu::max
<symfpuLiteral::traits
>(t
, fpl
, arg
.fpl
, zeroCaseLeft
));
763 FloatingPoint
FloatingPoint::minTotal (const FloatingPoint
&arg
, bool zeroCaseLeft
) const {
764 #ifdef CVC4_USE_SYMFPU
765 Assert(this->t
== arg
.t
);
766 return FloatingPoint(
767 t
, symfpu::min
<symfpuLiteral::traits
>(t
, fpl
, arg
.fpl
, zeroCaseLeft
));
773 FloatingPoint::PartialFloatingPoint
FloatingPoint::max (const FloatingPoint
&arg
) const {
774 FloatingPoint
tmp(maxTotal(arg
, true));
775 return PartialFloatingPoint(tmp
, tmp
== maxTotal(arg
, false));
778 FloatingPoint::PartialFloatingPoint
FloatingPoint::min (const FloatingPoint
&arg
) const {
779 FloatingPoint
tmp(minTotal(arg
, true));
780 return PartialFloatingPoint(tmp
, tmp
== minTotal(arg
, false));
783 bool FloatingPoint::operator ==(const FloatingPoint
& fp
) const {
784 #ifdef CVC4_USE_SYMFPU
786 && symfpu::smtlibEqual
<symfpuLiteral::traits
>(t
, fpl
, fp
.fpl
));
788 return ( (t
== fp
.t
) );
792 bool FloatingPoint::operator <= (const FloatingPoint
&arg
) const {
793 #ifdef CVC4_USE_SYMFPU
794 Assert(this->t
== arg
.t
);
795 return symfpu::lessThanOrEqual
<symfpuLiteral::traits
>(t
, fpl
, arg
.fpl
);
801 bool FloatingPoint::operator < (const FloatingPoint
&arg
) const {
802 #ifdef CVC4_USE_SYMFPU
803 Assert(this->t
== arg
.t
);
804 return symfpu::lessThan
<symfpuLiteral::traits
>(t
, fpl
, arg
.fpl
);
810 bool FloatingPoint::isNormal (void) const {
811 #ifdef CVC4_USE_SYMFPU
812 return symfpu::isNormal
<symfpuLiteral::traits
>(t
, fpl
);
818 bool FloatingPoint::isSubnormal (void) const {
819 #ifdef CVC4_USE_SYMFPU
820 return symfpu::isSubnormal
<symfpuLiteral::traits
>(t
, fpl
);
826 bool FloatingPoint::isZero (void) const {
827 #ifdef CVC4_USE_SYMFPU
828 return symfpu::isZero
<symfpuLiteral::traits
>(t
, fpl
);
834 bool FloatingPoint::isInfinite (void) const {
835 #ifdef CVC4_USE_SYMFPU
836 return symfpu::isInfinite
<symfpuLiteral::traits
>(t
, fpl
);
842 bool FloatingPoint::isNaN (void) const {
843 #ifdef CVC4_USE_SYMFPU
844 return symfpu::isNaN
<symfpuLiteral::traits
>(t
, fpl
);
850 bool FloatingPoint::isNegative (void) const {
851 #ifdef CVC4_USE_SYMFPU
852 return symfpu::isNegative
<symfpuLiteral::traits
>(t
, fpl
);
858 bool FloatingPoint::isPositive (void) const {
859 #ifdef CVC4_USE_SYMFPU
860 return symfpu::isPositive
<symfpuLiteral::traits
>(t
, fpl
);
866 FloatingPoint
FloatingPoint::convert (const FloatingPointSize
&target
, const RoundingMode
&rm
) const {
867 #ifdef CVC4_USE_SYMFPU
868 return FloatingPoint(
870 symfpu::convertFloatToFloat
<symfpuLiteral::traits
>(t
, target
, rm
, fpl
));
876 BitVector
FloatingPoint::convertToBVTotal (BitVectorSize width
, const RoundingMode
&rm
, bool signedBV
, BitVector undefinedCase
) const {
877 #ifdef CVC4_USE_SYMFPU
879 return symfpu::convertFloatToSBV
<symfpuLiteral::traits
>(
880 t
, rm
, fpl
, width
, undefinedCase
);
882 return symfpu::convertFloatToUBV
<symfpuLiteral::traits
>(
883 t
, rm
, fpl
, width
, undefinedCase
);
885 return undefinedCase
;
889 Rational
FloatingPoint::convertToRationalTotal (Rational undefinedCase
) const {
890 PartialRational
p(convertToRational());
892 return p
.second
? p
.first
: undefinedCase
;
895 FloatingPoint::PartialBitVector
FloatingPoint::convertToBV (BitVectorSize width
, const RoundingMode
&rm
, bool signedBV
) const {
896 BitVector
tmp(convertToBVTotal (width
, rm
, signedBV
, BitVector(width
, 0U)));
897 BitVector
confirm(convertToBVTotal (width
, rm
, signedBV
, BitVector(width
, 1U)));
899 return PartialBitVector(tmp
, tmp
== confirm
);
902 FloatingPoint::PartialRational
FloatingPoint::convertToRational (void) const {
903 if (this->isNaN() || this->isInfinite()) {
904 return PartialRational(Rational(0U, 1U), false);
906 if (this->isZero()) {
907 return PartialRational(Rational(0U, 1U), true);
910 #ifdef CVC4_USE_SYMFPU
911 Integer
sign((this->fpl
.getSign()) ? -1 : 1);
913 this->fpl
.getExponent().toSignedInteger()
914 - (Integer(t
.significand()
915 - 1))); // -1 as forcibly normalised into the [1,2) range
916 Integer
significand(this->fpl
.getSignificand().toInteger());
920 Integer
significand(0);
922 Integer
signedSignificand(sign
* significand
);
924 // Only have pow(uint32_t) so we should check this.
925 Assert(this->t
.significand() <= 32);
927 if (!(exp
.strictlyNegative())) {
928 Integer
r(signedSignificand
.multiplyByPow2(exp
.toUnsignedInt()));
929 return PartialRational(Rational(r
), true);
932 Integer
q(one
.multiplyByPow2((-exp
).toUnsignedInt()));
933 Rational
r(signedSignificand
, q
);
934 return PartialRational(r
, true);
938 Unreachable("Convert float literal to real broken.");
941 BitVector
FloatingPoint::pack (void) const {
942 #ifdef CVC4_USE_SYMFPU
943 BitVector
bv(symfpu::pack
<symfpuLiteral::traits
>(this->t
, this->fpl
));
952 }/* CVC4 namespace */