From: Aina Niemetz Date: Mon, 30 Nov 2020 20:17:43 +0000 (-0800) Subject: floatingpoint: Use unique_ptr for FloatingPointLiteral pointer. (#5503) X-Git-Tag: cvc5-1.0.0~2541 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1b73aefa4a33b5033390f7d6c9c96fa58cd3a298;p=cvc5.git floatingpoint: Use unique_ptr for FloatingPointLiteral pointer. (#5503) --- diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp index c5ec4d0c6..5b291f3c5 100644 --- a/src/util/floatingpoint.cpp +++ b/src/util/floatingpoint.cpp @@ -129,35 +129,35 @@ FloatingPoint::FloatingPoint(const FloatingPointSize& size, #ifdef CVC4_USE_SYMFPU if (signedBV) { - d_fpl = new FloatingPointLiteral( + d_fpl.reset(new FloatingPointLiteral( symfpu::convertSBVToFloat( symfpuLiteral::CVC4FPSize(size), symfpuLiteral::CVC4RM(rm), - symfpuLiteral::CVC4SignedBitVector(bv))); + symfpuLiteral::CVC4SignedBitVector(bv)))); } else { - d_fpl = new FloatingPointLiteral( + d_fpl.reset(new FloatingPointLiteral( symfpu::convertUBVToFloat( symfpuLiteral::CVC4FPSize(size), symfpuLiteral::CVC4RM(rm), - symfpuLiteral::CVC4UnsignedBitVector(bv))); + symfpuLiteral::CVC4UnsignedBitVector(bv)))); } #else - d_fpl = new FloatingPointLiteral(2, 2, 0.0); + d_fpl.reset(new FloatingPointLiteral(2, 2, 0.0)); #endif } FloatingPoint::FloatingPoint(const FloatingPointSize& fp_size, - const FloatingPointLiteral* fpl) + FloatingPointLiteral* fpl) : d_fp_size(fp_size) { - d_fpl = new FloatingPointLiteral(*fpl); + d_fpl.reset(fpl); } FloatingPoint::FloatingPoint(const FloatingPoint& fp) : d_fp_size(fp.d_fp_size) { - d_fpl = new FloatingPointLiteral(*fp.d_fpl); + d_fpl.reset(new FloatingPointLiteral(*fp.d_fpl)); } FloatingPoint::FloatingPoint(const FloatingPointSize& size, @@ -171,10 +171,10 @@ FloatingPoint::FloatingPoint(const FloatingPointSize& size, { #ifdef CVC4_USE_SYMFPU // In keeping with the SMT-LIB standard - d_fpl = new FloatingPointLiteral( - SymFPUUnpackedFloatLiteral::makeZero(size, false)); + d_fpl.reset(new FloatingPointLiteral( + SymFPUUnpackedFloatLiteral::makeZero(size, false))); #else - d_fpl = new FloatingPointLiteral(2, 2, 0.0); + d_fpl.reset(new FloatingPointLiteral(2, 2, 0.0)); #endif } else @@ -285,8 +285,8 @@ FloatingPoint::FloatingPoint(const FloatingPointSize& size, negative, exactExp.signExtend(extension), sig); // Then cast... - d_fpl = new FloatingPointLiteral( - symfpu::convertFloatToFloat(exactFormat, size, rm, exactFloat.d_symuf)); + d_fpl.reset(new FloatingPointLiteral(symfpu::convertFloatToFloat( + exactFormat, size, rm, exactFloat.d_symuf))); #else Unreachable() << "no concrete implementation of FloatingPointLiteral"; #endif @@ -295,8 +295,6 @@ FloatingPoint::FloatingPoint(const FloatingPointSize& size, FloatingPoint::~FloatingPoint() { - delete d_fpl; - d_fpl = nullptr; } FloatingPoint FloatingPoint::makeNaN(const FloatingPointSize& size) diff --git a/src/util/floatingpoint.h b/src/util/floatingpoint.h index 754c38290..2d27b836e 100644 --- a/src/util/floatingpoint.h +++ b/src/util/floatingpoint.h @@ -20,6 +20,8 @@ #ifndef CVC4__FLOATINGPOINT_H #define CVC4__FLOATINGPOINT_H +#include + #include "util/bitvector.h" #include "util/floatingpoint_size.h" #include "util/rational.h" @@ -60,8 +62,6 @@ class CVC4_PUBLIC FloatingPoint /** Constructors. */ FloatingPoint(uint32_t e, uint32_t s, const BitVector& bv); FloatingPoint(const FloatingPointSize& size, const BitVector& bv); - FloatingPoint(const FloatingPointSize& fp_size, - const FloatingPointLiteral* fpl); FloatingPoint(const FloatingPoint& fp); FloatingPoint(const FloatingPointSize& size, const RoundingMode& rm, @@ -118,7 +118,7 @@ class CVC4_PUBLIC FloatingPoint static FloatingPoint makeMaxNormal(const FloatingPointSize& size, bool sign); /** Get the wrapped floating-point value. */ - const FloatingPointLiteral* getLiteral(void) const { return d_fpl; } + const FloatingPointLiteral* getLiteral(void) const { return d_fpl.get(); } /** * Return a string representation of this floating-point. @@ -258,8 +258,16 @@ class CVC4_PUBLIC FloatingPoint FloatingPointSize d_fp_size; private: + /** + * Constructor. + * + * Note: This constructor takes ownership of 'fpl' and is not intended for + * public use. + */ + FloatingPoint(const FloatingPointSize& fp_size, FloatingPointLiteral* fpl); + /** The floating-point literal of this floating-point value. */ - FloatingPointLiteral* d_fpl; + std::unique_ptr d_fpl; }; /* class FloatingPoint */