From 83a502c54b59e6d654ed2a068c5f29f5e22ff660 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 17 Nov 2020 17:54:19 -0800 Subject: [PATCH] FloatingPoint: Use uint32_t instead of unsigned. (#5459) --- src/util/floatingpoint.cpp | 25 ++++++++-------- src/util/floatingpoint.h.in | 60 ++++++++++++++++++------------------- 2 files changed, 43 insertions(+), 42 deletions(-) diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp index 6e8f8369a..cfb0120fb 100644 --- a/src/util/floatingpoint.cpp +++ b/src/util/floatingpoint.cpp @@ -70,7 +70,7 @@ CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::ubv); namespace CVC4 { -FloatingPointSize::FloatingPointSize(unsigned exp_size, unsigned sig_size) +FloatingPointSize::FloatingPointSize(uint32_t exp_size, uint32_t sig_size) : d_exp_size(exp_size), d_sig_size(sig_size) { PrettyCheckArgument(validExponentSize(exp_size), @@ -492,8 +492,8 @@ void FloatingPointLiteral::unfinished(void) const } #endif -FloatingPoint::FloatingPoint(unsigned d_exp_size, - unsigned d_sig_size, +FloatingPoint::FloatingPoint(uint32_t d_exp_size, + uint32_t d_sig_size, const BitVector& bv) : d_fp_size(d_exp_size, d_sig_size), #ifdef CVC4_USE_SYMFPU @@ -568,7 +568,7 @@ static FloatingPointLiteral constructorHelperRational( #endif } else { #ifdef CVC4_USE_SYMFPU - int negative = (r.sgn() < 0) ? 1 : 0; + uint32_t negative = (r.sgn() < 0) ? 1 : 0; #endif r = r.abs(); @@ -597,7 +597,7 @@ static FloatingPointLiteral constructorHelperRational( Assert(r < working * two); // Work out the number of bits required to represent the exponent for a normal number - unsigned expBits = 2; // No point starting with an invalid amount + uint32_t expBits = 2; // No point starting with an invalid amount Integer doubleInt(2); if (exp.strictlyPositive()) { @@ -619,12 +619,13 @@ static FloatingPointLiteral constructorHelperRational( BitVector exactExp(expBits, exp); // Compute the significand. - unsigned sigBits = size.significandWidth() + 2; // guard and sticky bits + uint32_t sigBits = size.significandWidth() + 2; // guard and sticky bits BitVector sig(sigBits, 0U); BitVector one(sigBits, 1U); Rational workingSig(0,1); - for (unsigned i = 0; i < sigBits - 1; ++i) { - Rational mid(workingSig + working); + for (uint32_t i = 0; i < sigBits - 1; ++i) + { + Rational mid(workingSig + working); if (mid <= r) { sig = sig | one; @@ -650,7 +651,7 @@ static FloatingPointLiteral constructorHelperRational( // may have more to allow subnormals to be normalised. // Thus... #ifdef CVC4_USE_SYMFPU - unsigned extension = + uint32_t extension = FloatingPointLiteral::exponentWidth(exactFormat) - expBits; FloatingPointLiteral exactFloat( @@ -1113,16 +1114,16 @@ std::string FloatingPoint::toString(bool printAsIndexed) const std::string str; // retrive BV value BitVector bv(pack()); - unsigned largestSignificandBit = + uint32_t largestSignificandBit = d_fp_size.significandWidth() - 2; // -1 for -inclusive, -1 for hidden - unsigned largestExponentBit = + uint32_t largestExponentBit = (d_fp_size.exponentWidth() - 1) + (largestSignificandBit + 1); BitVector v[3]; v[0] = bv.extract(largestExponentBit + 1, largestExponentBit + 1); v[1] = bv.extract(largestExponentBit, largestSignificandBit + 1); v[2] = bv.extract(largestSignificandBit, 0); str.append("(fp "); - for (unsigned i = 0; i < 3; ++i) + for (uint32_t i = 0; i < 3; ++i) { if (printAsIndexed) { diff --git a/src/util/floatingpoint.h.in b/src/util/floatingpoint.h.in index 0d62e9c3e..7e430ad87 100644 --- a/src/util/floatingpoint.h.in +++ b/src/util/floatingpoint.h.in @@ -33,8 +33,8 @@ namespace CVC4 { // Inline these! -inline bool CVC4_PUBLIC validExponentSize(unsigned e) { return e >= 2; } -inline bool CVC4_PUBLIC validSignificandSize(unsigned s) { return s >= 2; } +inline bool CVC4_PUBLIC validExponentSize(uint32_t e) { return e >= 2; } +inline bool CVC4_PUBLIC validSignificandSize(uint32_t s) { return s >= 2; } /* -------------------------------------------------------------------------- */ @@ -47,7 +47,7 @@ class CVC4_PUBLIC FloatingPointSize { public: /** Constructors. */ - FloatingPointSize(unsigned exp_size, unsigned sig_size); + FloatingPointSize(uint32_t exp_size, uint32_t sig_size); FloatingPointSize(const FloatingPointSize& old); /** Operator overload for equality comparison. */ @@ -59,14 +59,14 @@ class CVC4_PUBLIC FloatingPointSize /** Implement the interface that symfpu uses for floating-point formats. */ /** Get the exponent bit-width of this floating-point format. */ - inline unsigned exponentWidth(void) const { return this->d_exp_size; } + inline uint32_t exponentWidth(void) const { return this->d_exp_size; } /** Get the significand bit-width of this floating-point format. */ - inline unsigned significandWidth(void) const { return this->d_sig_size; } + inline uint32_t significandWidth(void) const { return this->d_sig_size; } /** * Get the bit-width of the packed representation of this floating-point * format (= exponent + significand bit-width, convenience wrapper). */ - inline unsigned packedWidth(void) const + inline uint32_t packedWidth(void) const { return this->exponentWidth() + this->significandWidth(); } @@ -74,7 +74,7 @@ class CVC4_PUBLIC FloatingPointSize * Get the exponent bit-width of the packed representation of this * floating-point format (= exponent bit-width). */ - inline unsigned packedExponentWidth(void) const + inline uint32_t packedExponentWidth(void) const { return this->exponentWidth(); } @@ -82,16 +82,16 @@ class CVC4_PUBLIC FloatingPointSize * Get the significand bit-width of the packed representation of this * floating-point format (= significand bit-width - 1). */ - inline unsigned packedSignificandWidth(void) const + inline uint32_t packedSignificandWidth(void) const { return this->significandWidth() - 1; } private: /** Exponent bit-width. */ - unsigned d_exp_size; + uint32_t d_exp_size; /** Significand bit-width. */ - unsigned d_sig_size; + uint32_t d_sig_size; }; /* class FloatingPointSize */ @@ -107,7 +107,7 @@ struct CVC4_PUBLIC FloatingPointSizeHashFunction inline size_t operator()(const FloatingPointSize& t) const { - return size_t(ROLL(t.exponentWidth(), 4 * sizeof(unsigned)) + return size_t(ROLL(t.exponentWidth(), 4 * sizeof(uint32_t)) | t.significandWidth()); } }; /* struct FloatingPointSizeHashFunction */ @@ -224,7 +224,7 @@ class wrappedBitVector : public BitVector public: /** Constructors. */ - wrappedBitVector(const CVC4BitWidth w, const unsigned v) : BitVector(w, v) {} + wrappedBitVector(const CVC4BitWidth w, const uint32_t v) : BitVector(w, v) {} wrappedBitVector(const CVC4Prop& p) : BitVector(1, p ? 1U : 0U) {} wrappedBitVector(const wrappedBitVector& old) : BitVector(old) {} wrappedBitVector(const BitVector& old) : BitVector(old) {} @@ -379,8 +379,8 @@ class CVC4_PUBLIC FloatingPointLiteral // representation is solver specific. void unfinished(void) const; - FloatingPointLiteral(unsigned, unsigned, double) { unfinished(); } - FloatingPointLiteral(unsigned, unsigned, const std::string&) { unfinished(); } + FloatingPointLiteral(uint32_t, uint32_t, double) { unfinished(); } + FloatingPointLiteral(uint32_t, uint32_t, const std::string&) { unfinished(); } FloatingPointLiteral(const FloatingPointLiteral&) { unfinished(); } bool operator==(const FloatingPointLiteral& op) const { @@ -408,7 +408,7 @@ class CVC4_PUBLIC FloatingPoint using PartialRational = std::pair; /** Constructors. */ - FloatingPoint(unsigned e, unsigned s, const BitVector& bv); + FloatingPoint(uint32_t e, uint32_t s, const BitVector& bv); FloatingPoint(const FloatingPointSize& size, const BitVector& bv); FloatingPoint(const FloatingPointSize& fp_size, @@ -635,7 +635,7 @@ class CVC4_PUBLIC FloatingPointConvertSort { public: /** Constructors. */ - FloatingPointConvertSort(unsigned _e, unsigned _s) : d_fp_size(_e, _s) {} + FloatingPointConvertSort(uint32_t _e, uint32_t _s) : d_fp_size(_e, _s) {} FloatingPointConvertSort(const FloatingPointSize& fps) : d_fp_size(fps) {} /** Operator overload for comparison of conversion sorts. */ @@ -649,7 +649,7 @@ class CVC4_PUBLIC FloatingPointConvertSort }; /** Hash function for conversion sorts. */ -template +template struct CVC4_PUBLIC FloatingPointConvertSortHashFunction { inline size_t operator()(const FloatingPointConvertSort& fpcs) const @@ -674,7 +674,7 @@ class CVC4_PUBLIC FloatingPointToFPIEEEBitVector { public: /** Constructors. */ - FloatingPointToFPIEEEBitVector(unsigned _e, unsigned _s) + FloatingPointToFPIEEEBitVector(uint32_t _e, uint32_t _s) : FloatingPointConvertSort(_e, _s) { } @@ -693,7 +693,7 @@ class CVC4_PUBLIC FloatingPointToFPFloatingPoint { public: /** Constructors. */ - FloatingPointToFPFloatingPoint(unsigned _e, unsigned _s) + FloatingPointToFPFloatingPoint(uint32_t _e, uint32_t _s) : FloatingPointConvertSort(_e, _s) { } @@ -710,7 +710,7 @@ class CVC4_PUBLIC FloatingPointToFPReal : public FloatingPointConvertSort { public: /** Constructors. */ - FloatingPointToFPReal(unsigned _e, unsigned _s) + FloatingPointToFPReal(uint32_t _e, uint32_t _s) : FloatingPointConvertSort(_e, _s) { } @@ -728,7 +728,7 @@ class CVC4_PUBLIC FloatingPointToFPSignedBitVector { public: /** Constructors. */ - FloatingPointToFPSignedBitVector(unsigned _e, unsigned _s) + FloatingPointToFPSignedBitVector(uint32_t _e, uint32_t _s) : FloatingPointConvertSort(_e, _s) { } @@ -746,7 +746,7 @@ class CVC4_PUBLIC FloatingPointToFPUnsignedBitVector { public: /** Constructors. */ - FloatingPointToFPUnsignedBitVector(unsigned _e, unsigned _s) + FloatingPointToFPUnsignedBitVector(uint32_t _e, uint32_t _s) : FloatingPointConvertSort(_e, _s) { } @@ -760,7 +760,7 @@ class CVC4_PUBLIC FloatingPointToFPGeneric : public FloatingPointConvertSort { public: /** Constructors. */ - FloatingPointToFPGeneric(unsigned _e, unsigned _s) + FloatingPointToFPGeneric(uint32_t _e, uint32_t _s) : FloatingPointConvertSort(_e, _s) { } @@ -777,12 +777,12 @@ class CVC4_PUBLIC FloatingPointToBV { public: /** Constructors. */ - FloatingPointToBV(unsigned s) : d_bv_size(s) {} + FloatingPointToBV(uint32_t s) : d_bv_size(s) {} FloatingPointToBV(const FloatingPointToBV& old) : d_bv_size(old.d_bv_size) {} FloatingPointToBV(const BitVectorSize& old) : d_bv_size(old) {} /** Return the bit-width of the bit-vector to convert to. */ - operator unsigned() const { return d_bv_size; } + operator uint32_t() const { return d_bv_size; } /** The bit-width of the bit-vector to converto to. */ BitVectorSize d_bv_size; @@ -794,7 +794,7 @@ class CVC4_PUBLIC FloatingPointToBV class CVC4_PUBLIC FloatingPointToUBV : public FloatingPointToBV { public: - FloatingPointToUBV(unsigned _s) : FloatingPointToBV(_s) {} + FloatingPointToUBV(uint32_t _s) : FloatingPointToBV(_s) {} FloatingPointToUBV(const FloatingPointToBV& old) : FloatingPointToBV(old) {} }; @@ -804,7 +804,7 @@ class CVC4_PUBLIC FloatingPointToUBV : public FloatingPointToBV class CVC4_PUBLIC FloatingPointToSBV : public FloatingPointToBV { public: - FloatingPointToSBV(unsigned _s) : FloatingPointToBV(_s) {} + FloatingPointToSBV(uint32_t _s) : FloatingPointToBV(_s) {} FloatingPointToSBV(const FloatingPointToBV& old) : FloatingPointToBV(old) {} }; @@ -814,7 +814,7 @@ class CVC4_PUBLIC FloatingPointToSBV : public FloatingPointToBV class CVC4_PUBLIC FloatingPointToUBVTotal : public FloatingPointToBV { public: - FloatingPointToUBVTotal(unsigned _s) : FloatingPointToBV(_s) {} + FloatingPointToUBVTotal(uint32_t _s) : FloatingPointToBV(_s) {} FloatingPointToUBVTotal(const FloatingPointToBV& old) : FloatingPointToBV(old) { } @@ -826,7 +826,7 @@ class CVC4_PUBLIC FloatingPointToUBVTotal : public FloatingPointToBV class CVC4_PUBLIC FloatingPointToSBVTotal : public FloatingPointToBV { public: - FloatingPointToSBVTotal(unsigned _s) : FloatingPointToBV(_s) {} + FloatingPointToSBVTotal(uint32_t _s) : FloatingPointToBV(_s) {} FloatingPointToSBVTotal(const FloatingPointToBV& old) : FloatingPointToBV(old) { } @@ -835,7 +835,7 @@ class CVC4_PUBLIC FloatingPointToSBVTotal : public FloatingPointToBV /** * Hash function for floating-point to bit-vector conversions. */ -template +template struct CVC4_PUBLIC FloatingPointToBVHashFunction { inline size_t operator()(const FloatingPointToBV& fptbv) const -- 2.30.2