FloatingPointLiteral: Constructor for special consts. (#6220)

This replaces static helpers for creating special consts with
constructors. This is in preparation for a FP literal implementation
using MPFR. In the next step, I'll introduce a FloatingPointLiteral base
class, from which the specialization FloatingPointSymFPULiteral is
derived. The MPFR implementation will also be derived from the base class.
This is in order to make unit tests that compare between the two
possible. Further, in the worst case, MPFR will have to use SymFPU for
unsupported cases (to be determined).

diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp
index 23b8253d8815a56daa778ac5b74ee8ae8f5ffcd8..26bdb65f4ee5737846a256e698e459a28a90bf23 100644 (file)
--- a/src/util/floatingpoint.cpp
+++ b/src/util/floatingpoint.cpp
@@ -78,8 +78,8 @@ FloatingPoint::FloatingPoint(const FloatingPointSize& size,
   if (r.isZero())
   {
     // In keeping with the SMT-LIB standard
-    d_fpl.reset(
-        new FloatingPointLiteral(FloatingPointLiteral::makeZero(size, false)));
+    d_fpl.reset(new FloatingPointLiteral(
+        size, FloatingPointLiteral::SpecialConstKind::FPZERO, false));
   }
   else
   {
@@ -201,20 +201,20 @@ const FloatingPointSize& FloatingPoint::getSize() const
 
 FloatingPoint FloatingPoint::makeNaN(const FloatingPointSize& size)
 {
-  return FloatingPoint(
-      new FloatingPointLiteral(FloatingPointLiteral::makeNaN(size)));
+  return FloatingPoint(new FloatingPointLiteral(
+      size, FloatingPointLiteral::SpecialConstKind::FPNAN));
 }
 
 FloatingPoint FloatingPoint::makeInf(const FloatingPointSize& size, bool sign)
 {
-  return FloatingPoint(
-      new FloatingPointLiteral(FloatingPointLiteral::makeInf(size, sign)));
+  return FloatingPoint(new FloatingPointLiteral(
+      size, FloatingPointLiteral::SpecialConstKind::FPINF, sign));
 }
 
 FloatingPoint FloatingPoint::makeZero(const FloatingPointSize& size, bool sign)
 {
-  return FloatingPoint(
-      new FloatingPointLiteral(FloatingPointLiteral::makeZero(size, sign)));
+  return FloatingPoint(new FloatingPointLiteral(
+      size, FloatingPointLiteral::SpecialConstKind::FPZERO, sign));
 }
 
 FloatingPoint FloatingPoint::makeMinSubnormal(const FloatingPointSize& size,

diff --git a/src/util/floatingpoint_literal_symfpu.cpp b/src/util/floatingpoint_literal_symfpu.cpp
index 59b14001d2b2027c2ed9929a6b5b5b39d983e2df..1d40292f76237b5896f8df2167d9c24008891d53 100644 (file)
--- a/src/util/floatingpoint_literal_symfpu.cpp
+++ b/src/util/floatingpoint_literal_symfpu.cpp
@@ -83,51 +83,43 @@ uint32_t FloatingPointLiteral::getUnpackedSignificandWidth(
 #endif
 }
 
-FloatingPointLiteral FloatingPointLiteral::makeNaN(
-    const FloatingPointSize& size)
-{
+FloatingPointLiteral::FloatingPointLiteral(uint32_t exp_size,
+                                           uint32_t sig_size,
+                                           const BitVector& bv)
+    : d_fp_size(exp_size, sig_size)
 #ifdef CVC4_USE_SYMFPU
-  return FloatingPointLiteral(size, SymFPUUnpackedFloatLiteral::makeNaN(size));
-#else
-  unimplemented();
-  return FloatingPointLiteral(size, BitVector(4u, 0u));
+      ,
+      d_symuf(symfpu::unpack<symfpuLiteral::traits>(
+          symfpuLiteral::CVC4FPSize(exp_size, sig_size), bv))
 #endif
-}
-
-FloatingPointLiteral FloatingPointLiteral::makeInf(
-    const FloatingPointSize& size, bool sign)
 {
-#ifdef CVC4_USE_SYMFPU
-  return FloatingPointLiteral(size,
-                              SymFPUUnpackedFloatLiteral::makeInf(size, sign));
-#else
-  unimplemented();
-  return FloatingPointLiteral(size, BitVector(4u, 0u));
-#endif
 }
 
-FloatingPointLiteral FloatingPointLiteral::makeZero(
-    const FloatingPointSize& size, bool sign)
-{
+FloatingPointLiteral::FloatingPointLiteral(
+    const FloatingPointSize& size, FloatingPointLiteral::SpecialConstKind kind)
+    : d_fp_size(size)
 #ifdef CVC4_USE_SYMFPU
-  return FloatingPointLiteral(size,
-                              SymFPUUnpackedFloatLiteral::makeZero(size, sign));
-#else
-  unimplemented();
-  return FloatingPointLiteral(size, BitVector(4u, 0u));
+      ,
+      d_symuf(SymFPUUnpackedFloatLiteral::makeNaN(size))
 #endif
+{
+  Assert(kind == FloatingPointLiteral::SpecialConstKind::FPNAN);
 }
 
-FloatingPointLiteral::FloatingPointLiteral(uint32_t d_exp_size,
-                                           uint32_t d_sig_size,
-                                           const BitVector& bv)
-    : d_fp_size(d_exp_size, d_sig_size)
+FloatingPointLiteral::FloatingPointLiteral(
+    const FloatingPointSize& size,
+    FloatingPointLiteral::SpecialConstKind kind,
+    bool sign)
+    : d_fp_size(size)
 #ifdef CVC4_USE_SYMFPU
       ,
-      d_symuf(symfpu::unpack<symfpuLiteral::traits>(
-          symfpuLiteral::CVC4FPSize(d_exp_size, d_sig_size), bv))
+      d_symuf(kind == FloatingPointLiteral::SpecialConstKind::FPINF
+                  ? SymFPUUnpackedFloatLiteral::makeInf(size, sign)
+                  : SymFPUUnpackedFloatLiteral::makeZero(size, sign))
 #endif
 {
+  Assert(kind == FloatingPointLiteral::SpecialConstKind::FPINF
+         || kind == FloatingPointLiteral::SpecialConstKind::FPZERO);
 }
 
 FloatingPointLiteral::FloatingPointLiteral(const FloatingPointSize& size,

diff --git a/src/util/floatingpoint_literal_symfpu.h.in b/src/util/floatingpoint_literal_symfpu.h.in
index 2424bad66c8b00a581ac3ea77e5dac7bb1ab7621..8857728ce9dd3be45ff551994f1f915c3b2ffb39 100644 (file)
--- a/src/util/floatingpoint_literal_symfpu.h.in
+++ b/src/util/floatingpoint_literal_symfpu.h.in
@@ -287,6 +287,18 @@ class FloatingPointLiteral
   friend class FloatingPoint;
 
  public:
+  /**
+   * The kind of floating-point special constants that can be created via the
+   * corresponding constructor.
+   * These are prefixed with FP because of name clashes with NAN.
+   */
+  enum SpecialConstKind
+  {
+    FPINF,   // +-oo
+    FPNAN,   // NaN
+    FPZERO,  // +-zero
+  };
+
   /**
    * Get the number of exponent bits in the unpacked format corresponding to a
    * given packed format.  This is the unpacked counter-part of
@@ -300,24 +312,6 @@ class FloatingPointLiteral
    */
   static uint32_t getUnpackedSignificandWidth(FloatingPointSize& size);
 
-  /**
-   * Create a FP NaN literal of given size.
-   * size: The FP size (format).
-   */
-  static FloatingPointLiteral makeNaN(const FloatingPointSize& size);
-  /**
-   * Create a FP infinity literal of given size.
-   * size: The FP size (format).
-   * sign: True for -oo, false otherwise.
-   */
-  static FloatingPointLiteral makeInf(const FloatingPointSize& size, bool sign);
-  /**
-   * Create a FP zero literal of given size.
-   * size: The FP size (format).
-   * sign: True for -zero, false otherwise.
-   */
-  static FloatingPointLiteral makeZero(const FloatingPointSize& size,
-                                       bool sign);
 // clang-format off
 #if !@CVC4_USE_SYMFPU@
   // clang-format on
@@ -328,11 +322,17 @@ class FloatingPointLiteral
   /** Constructors. */
 
   /** Create a FP literal from its IEEE bit-vector representation. */
-  FloatingPointLiteral(uint32_t d_exp_size,
-                       uint32_t d_sig_size,
+  FloatingPointLiteral(uint32_t exp_size,
+                       uint32_t sig_size,
                        const BitVector& bv);
   FloatingPointLiteral(const FloatingPointSize& size, const BitVector& bv);
 
+  /** Create a FP literal that represents a special constants. */
+  FloatingPointLiteral(const FloatingPointSize& size, SpecialConstKind kind);
+  FloatingPointLiteral(const FloatingPointSize& size,
+                       SpecialConstKind kind,
+                       bool sign);
+
   /**
    * Create a FP literal from a signed or unsigned bit-vector value with
    * respect to given rounding mode.