3 files changed, 52 insertions, 60 deletions
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
@@ -288,6 +288,18 @@ class FloatingPointLiteral
 
  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
    * FloatingPointSize::exponentWidth().
@@ -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.