FloatingPoint: Separate out symFPU glue code. (#5492)

This works towards having the symFPU headers only included where it's
absolutely needed (only in the .cpp files, not in any other headers).

Note: src/util/floatingpoint.h.in will be converted to a regular .h file
      in the next step to simplify reviewing.

4 files changed, 36 insertions, 68 deletions

diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp
index 0d088fe41..f7c58af7b 100644
--- a/src/theory/fp/fp_converter.cpp
+++ b/src/theory/fp/fp_converter.cpp
@@ -13,11 +13,13 @@
  **/
 
 #include "theory/fp/fp_converter.h"
-#include "theory/theory.h"
-// theory.h Only needed for the leaf test
 
 #include <vector>
 
+#include "theory/theory.h"  // theory.h Only needed for the leaf test
+#include "util/floatingpoint.h"
+#include "util/symfpu_literal.h"
+
 #ifdef CVC4_USE_SYMFPU
 #include "symfpu/core/add.h"
 #include "symfpu/core/classify.h"
@@ -919,9 +921,11 @@ Node FpConverter::convert(TNode node)
           if (current.getKind() == kind::CONST_FLOATINGPOINT)
           {
             /******** Constants ********/
-            d_fpMap.insert(current,
-                           symfpu::unpackedFloat<traits>(
-                               current.getConst<FloatingPoint>().getLiteral()));
+            d_fpMap.insert(
+                current,
+                symfpu::unpackedFloat<traits>(current.getConst<FloatingPoint>()
+                                                  .getLiteral()
+                                                  ->getSymUF()));
           }
           else
           {
@@ -1711,43 +1715,23 @@ Node FpConverter::getValue(Valuation &val, TNode var)
 #ifdef CVC4_USE_SYMFPU
   TypeNode t(var.getType());
 
+  Assert(t.isRoundingMode() || t.isFloatingPoint())
+      << "Asking for the value of a type that is not managed by the "
+         "floating-point theory";
+
   if (t.isRoundingMode())
   {
     rmMap::const_iterator i(d_rmMap.find(var));
 
-    if (i == d_rmMap.end())
-    {
-      Unreachable() << "Asking for the value of an unregistered expression";
-    }
-    else
-    {
-      Node value = rmToNode((*i).second);
-      return value;
-    }
+    Assert(i != d_rmMap.end())
+        << "Asking for the value of an unregistered expression";
+    return rmToNode((*i).second);
   }
-  else if (t.isFloatingPoint())
-  {
-    fpMap::const_iterator i(d_fpMap.find(var));
-
-    if (i == d_fpMap.end())
-    {
-      Unreachable() << "Asking for the value of an unregistered expression";
-    }
-    else
-    {
-      Node value = ufToNode(fpt(t), (*i).second);
-      return value;
-    }
-  }
-  else
-  {
-    Unreachable()
-        << "Asking for the value of a type that is not managed by the "
-           "floating-point theory";
-  }
-
-  Unreachable() << "Unable to find value";
+  fpMap::const_iterator i(d_fpMap.find(var));
 
+  Assert(i != d_fpMap.end())
+      << "Asking for the value of an unregistered expression";
+  return ufToNode(fpt(t), (*i).second);
 #else
   Unimplemented() << "Conversion is dependent on SymFPU";
 #endif
diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h
index fd4434832..59e65c9e1 100644
--- a/src/theory/fp/fp_converter.h
+++ b/src/theory/fp/fp_converter.h
@@ -29,7 +29,7 @@
 #include "expr/type.h"
 #include "theory/valuation.h"
 #include "util/bitvector.h"
-#include "util/floatingpoint.h"
+#include "util/floatingpoint_size.h"
 #include "util/hash.h"
 
 #ifdef CVC4_USE_SYMFPU
diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp
index 49b4e85c5..b56fa259c 100644
--- a/src/theory/fp/theory_fp_rewriter.cpp
+++ b/src/theory/fp/theory_fp_rewriter.cpp
@@ -887,18 +887,10 @@ namespace constantFold {
     switch (k)
     {
 #ifdef CVC4_USE_SYMFPU
-      case kind::FLOATINGPOINT_COMPONENT_NAN:
-        result = arg0.getLiteral().nan;
-        break;
-      case kind::FLOATINGPOINT_COMPONENT_INF:
-        result = arg0.getLiteral().inf;
-        break;
-      case kind::FLOATINGPOINT_COMPONENT_ZERO:
-        result = arg0.getLiteral().zero;
-        break;
-      case kind::FLOATINGPOINT_COMPONENT_SIGN:
-        result = arg0.getLiteral().sign;
-        break;
+      case kind::FLOATINGPOINT_COMPONENT_NAN: result = arg0.isNaN(); break;
+      case kind::FLOATINGPOINT_COMPONENT_INF: result = arg0.isInfinite(); break;
+      case kind::FLOATINGPOINT_COMPONENT_ZERO: result = arg0.isZero(); break;
+      case kind::FLOATINGPOINT_COMPONENT_SIGN: result = arg0.getSign(); break;
 #endif
       default: Unreachable() << "Unknown kind used in componentFlag"; break;
     }
@@ -919,11 +911,11 @@ namespace constantFold {
     return RewriteResponse(
         REWRITE_DONE,
 #ifdef CVC4_USE_SYMFPU
-        NodeManager::currentNM()->mkConst((BitVector)arg0.getLiteral().exponent)
+        NodeManager::currentNM()->mkConst((BitVector)arg0.getExponent())
 #else
         node
 #endif
-            );
+    );
   }
 
   RewriteResponse componentSignificand(TNode node, bool)
@@ -932,14 +924,14 @@ namespace constantFold {
 
     FloatingPoint arg0(node[0].getConst<FloatingPoint>());
 
-    return RewriteResponse(REWRITE_DONE,
+    return RewriteResponse(
+        REWRITE_DONE,
 #ifdef CVC4_USE_SYMFPU
-                           NodeManager::currentNM()->mkConst(
-                               (BitVector)arg0.getLiteral().significand)
+        NodeManager::currentNM()->mkConst((BitVector)arg0.getSignificand())
 #else
-                           node
+        node
 #endif
-                               );
+    );
   }
 
   RewriteResponse roundingModeBitBlast(TNode node, bool)
diff --git a/src/theory/fp/theory_fp_type_rules.h b/src/theory/fp/theory_fp_type_rules.h
index 4d4f3c660..d632e80c8 100644
--- a/src/theory/fp/theory_fp_type_rules.h
+++ b/src/theory/fp/theory_fp_type_rules.h
@@ -19,6 +19,7 @@
 
 // This is only needed for checking that components are only applied to leaves.
 #include "theory/theory.h"
+#include "util/roundingmode.h"
 
 #ifndef CVC4__THEORY__FP__THEORY_FP_TYPE_RULES_H
 #define CVC4__THEORY__FP__THEORY_FP_TYPE_RULES_H
@@ -693,12 +694,10 @@ class FloatingPointComponentExponent
      * Here we use types from floatingpoint.h which are the literal
      * back-end but it should't make a difference. */
     FloatingPointSize fps = operandType.getConst<FloatingPointSize>();
-    symfpuLiteral::CVC4FPSize format(fps);  // The symfpu interface to type info
-    unsigned bw = FloatingPointLiteral::exponentWidth(format);
+    unsigned bw = FloatingPoint::getUnpackedExponentWidth(fps);
 #else
     unsigned bw = 2;
 #endif
-
     return nodeManager->mkBitVectorType(bw);
   }
 };
@@ -736,12 +735,10 @@ class FloatingPointComponentSignificand
 #ifdef CVC4_USE_SYMFPU
     /* As before we need to use some of sympfu. */
     FloatingPointSize fps = operandType.getConst<FloatingPointSize>();
-    symfpuLiteral::CVC4FPSize format(fps);
-    unsigned bw = FloatingPointLiteral::significandWidth(format);
+    unsigned bw = FloatingPoint::getUnpackedSignificandWidth(fps);
 #else
     unsigned bw = 1;
 #endif
-
     return nodeManager->mkBitVectorType(bw);
   }
 };
@@ -771,12 +768,7 @@ class RoundingModeBitBlast
       }
     }
 
-#ifdef CVC4_USE_SYMFPU
-    /* Uses sympfu for the macro. */
-    return nodeManager->mkBitVectorType(SYMFPU_NUMBER_OF_ROUNDING_MODES);
-#else
-    return nodeManager->mkBitVectorType(5);
-#endif
+    return nodeManager->mkBitVectorType(CVC4_NUM_ROUNDING_MODES);
   }
 };