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.

1 files changed, 20 insertions, 36 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