From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Mon, 29 Mar 2021 09:11:19 +0000 (-0700)
Subject: FloatingPointLiteral: Constructor for special consts. (#6220)
X-Git-Tag: cvc5-1.0.0~2021
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=38f797f5aa577a643e00ebc42e933a2552de575f;p=cvc5.git

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 23b8253d8..26bdb65f4 100644
--- 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 59b14001d..1d40292f7 100644
--- 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 2424bad66..8857728ce 100644
--- 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.