floatingpoint: Use unique_ptr for FloatingPointLiteral pointer. (#5503)

2 files changed, 25 insertions, 19 deletions

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::traits>(
             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::traits>(
             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 <memory>
+
 #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<FloatingPointLiteral> d_fpl;
 
 }; /* class FloatingPoint */