Make symfpu a required dependency. (#6749)

20 files changed, 11 insertions, 365 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 2419e1e41..d7da67cbe 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -1204,9 +1204,8 @@ endif()
 if(USE_POLY)
   target_link_libraries(cvc5 PRIVATE Polyxx)
 endif()
-if(USE_SYMFPU)
-  target_link_libraries(cvc5 PRIVATE SymFPU)
-endif()
+
+target_link_libraries(cvc5 PRIVATE SymFPU)
 
 # Note: When linked statically GMP needs to be linked after CLN since CLN
 # depends on GMP.
diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 307222988..43bb3d2dc 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -5197,18 +5197,6 @@ void Solver::checkMkTerm(Kind kind, uint32_t nchildren) const
       << " children (the one under construction has " << nchildren << ")";
 }
 
-/* Solver Configuration                                                       */
-/* -------------------------------------------------------------------------- */
-
-bool Solver::supportsFloatingPoint() const
-{
-  CVC5_API_TRY_CATCH_BEGIN;
-  //////// all checks before this line
-  return Configuration::isBuiltWithSymFPU();
-  ////////
-  CVC5_API_TRY_CATCH_END;
-}
-
 /* Sorts Handling                                                             */
 /* -------------------------------------------------------------------------- */
 
@@ -5276,8 +5264,6 @@ Sort Solver::getRoundingModeSort(void) const
 {
   NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_CHECK(Configuration::isBuiltWithSymFPU())
-      << "Expected cvc5 to be compiled with SymFPU support";
   //////// all checks before this line
   return Sort(this, getNodeManager()->roundingModeType());
   ////////
@@ -5314,8 +5300,6 @@ Sort Solver::mkFloatingPointSort(uint32_t exp, uint32_t sig) const
 {
   NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_CHECK(Configuration::isBuiltWithSymFPU())
-      << "Expected cvc5 to be compiled with SymFPU support";
   CVC5_API_ARG_CHECK_EXPECTED(exp > 0, exp) << "exponent size > 0";
   CVC5_API_ARG_CHECK_EXPECTED(sig > 0, sig) << "significand size > 0";
   //////// all checks before this line
@@ -5794,8 +5778,6 @@ Term Solver::mkPosInf(uint32_t exp, uint32_t sig) const
 {
   NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_CHECK(Configuration::isBuiltWithSymFPU())
-      << "Expected cvc5 to be compiled with SymFPU support";
   //////// all checks before this line
   return mkValHelper<cvc5::FloatingPoint>(
       FloatingPoint::makeInf(FloatingPointSize(exp, sig), false));
@@ -5807,8 +5789,6 @@ Term Solver::mkNegInf(uint32_t exp, uint32_t sig) const
 {
   NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_CHECK(Configuration::isBuiltWithSymFPU())
-      << "Expected cvc5 to be compiled with SymFPU support";
   //////// all checks before this line
   return mkValHelper<cvc5::FloatingPoint>(
       FloatingPoint::makeInf(FloatingPointSize(exp, sig), true));
@@ -5820,8 +5800,6 @@ Term Solver::mkNaN(uint32_t exp, uint32_t sig) const
 {
   NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_CHECK(Configuration::isBuiltWithSymFPU())
-      << "Expected cvc5 to be compiled with SymFPU support";
   //////// all checks before this line
   return mkValHelper<cvc5::FloatingPoint>(
       FloatingPoint::makeNaN(FloatingPointSize(exp, sig)));
@@ -5833,8 +5811,6 @@ Term Solver::mkPosZero(uint32_t exp, uint32_t sig) const
 {
   NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_CHECK(Configuration::isBuiltWithSymFPU())
-      << "Expected cvc5 to be compiled with SymFPU support";
   //////// all checks before this line
   return mkValHelper<cvc5::FloatingPoint>(
       FloatingPoint::makeZero(FloatingPointSize(exp, sig), false));
@@ -5846,8 +5822,6 @@ Term Solver::mkNegZero(uint32_t exp, uint32_t sig) const
 {
   NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_CHECK(Configuration::isBuiltWithSymFPU())
-      << "Expected cvc5 to be compiled with SymFPU support";
   //////// all checks before this line
   return mkValHelper<cvc5::FloatingPoint>(
       FloatingPoint::makeZero(FloatingPointSize(exp, sig), true));
@@ -5859,8 +5833,6 @@ Term Solver::mkRoundingMode(RoundingMode rm) const
 {
   NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_CHECK(Configuration::isBuiltWithSymFPU())
-      << "Expected cvc5 to be compiled with SymFPU support";
   //////// all checks before this line
   return mkValHelper<cvc5::RoundingMode>(s_rmodes.at(rm));
   ////////
@@ -5914,8 +5886,6 @@ Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const
 {
   NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_CHECK(Configuration::isBuiltWithSymFPU())
-      << "Expected cvc5 to be compiled with SymFPU support";
   CVC5_API_SOLVER_CHECK_TERM(val);
   CVC5_API_ARG_CHECK_EXPECTED(exp > 0, exp) << "a value > 0";
   CVC5_API_ARG_CHECK_EXPECTED(sig > 0, sig) << "a value > 0";
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index a1421cf12..161522654 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -2752,12 +2752,6 @@ class CVC5_EXPORT Solver
   Solver& operator=(const Solver&) = delete;
 
   /* .................................................................... */
-  /* Solver Configuration                                                 */
-  /* .................................................................... */
-
-  bool supportsFloatingPoint() const;
-
-  /* .................................................................... */
   /* Sorts Handling                                                       */
   /* .................................................................... */
 
diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index fdc1872e7..9d980267d 100644
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -151,7 +151,6 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
 
     cdef cppclass Solver:
         Solver(Options*) except +
-        bint supportsFloatingPoint() except +
         Sort getBooleanSort() except +
         Sort getIntegerSort() except +
         Sort getRealSort() except +
diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 258005207..874c63c3d 100644
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -460,9 +460,6 @@ cdef class Solver:
     def __dealloc__(self):
         del self.csolver
 
-    def supportsFloatingPoint(self):
-        return self.csolver.supportsFloatingPoint()
-
     def getBooleanSort(self):
         cdef Sort sort = Sort(self)
         sort.csort = self.csolver.getBooleanSort()
diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp
index 61951841b..1befb34ea 100644
--- a/src/base/configuration.cpp
+++ b/src/base/configuration.cpp
@@ -123,7 +123,6 @@ std::string Configuration::copyright() {
   if (Configuration::isBuiltWithAbc() || Configuration::isBuiltWithCadical()
       || Configuration::isBuiltWithCryptominisat()
       || Configuration::isBuiltWithKissat()
-      || Configuration::isBuiltWithSymFPU()
       || Configuration::isBuiltWithEditline())
   {
     ss << "This version of cvc5 is linked against the following non-(L)GPL'ed\n"
@@ -151,12 +150,6 @@ std::string Configuration::copyright() {
          << "  See https://fmv.jku.at/kissat for copyright "
          << "information.\n\n";
     }
-    if (Configuration::isBuiltWithSymFPU())
-    {
-      ss << "  SymFPU - The Symbolic Floating Point Unit\n"
-         << "  See https://github.com/martin-cs/symfpu/tree/cvc5 for copyright "
-         << "information.\n\n";
-    }
     if (Configuration::isBuiltWithEditline())
     {
       ss << "  Editline Library\n"
@@ -165,6 +158,10 @@ std::string Configuration::copyright() {
     }
   }
 
+  ss << "  SymFPU - The Symbolic Floating Point Unit\n"
+     << "  See https://github.com/martin-cs/symfpu/tree/cvc5 for copyright "
+     << "information.\n\n";
+
   if (Configuration::isBuiltWithGmp() || Configuration::isBuiltWithPoly())
   {
     ss << "This version of cvc5 is linked against the following third party\n"
@@ -259,8 +256,6 @@ bool Configuration::isBuiltWithPoly()
   return IS_POLY_BUILD;
 }
 
-bool Configuration::isBuiltWithSymFPU() { return IS_SYMFPU_BUILD; }
-
 unsigned Configuration::getNumDebugTags() {
 #if defined(CVC5_DEBUG) && defined(CVC5_TRACING)
   /* -1 because a NULL pointer is inserted as the last value */
diff --git a/src/base/configuration.h b/src/base/configuration.h
index 78e86f920..2a7df1b4a 100644
--- a/src/base/configuration.h
+++ b/src/base/configuration.h
@@ -113,8 +113,6 @@ public:
 
   static bool isBuiltWithPoly();
 
-  static bool isBuiltWithSymFPU();
-
   /* Return the number of debug tags */
   static unsigned getNumDebugTags();
   /* Return a sorted array of the debug tags name */
diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h
index 3027b23bc..39c5e89e9 100644
--- a/src/base/configuration_private.h
+++ b/src/base/configuration_private.h
@@ -126,12 +126,6 @@ namespace cvc5 {
 #define IS_EDITLINE_BUILD false
 #endif /* HAVE_LIBEDITLINE */
 
-#ifdef CVC5_USE_SYMFPU
-#define IS_SYMFPU_BUILD true
-#else /* HAVE_SYMFPU_HEADERS */
-#define IS_SYMFPU_BUILD false
-#endif /* HAVE_SYMFPU_HEADERS */
-
 #if CVC5_GPL_DEPS
 #  define IS_GPL_BUILD true
 #else /* CVC5_GPL_DEPS */
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index e109ab44c..d31d2e58f 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -403,7 +403,6 @@ void OptionsHandler::showConfiguration(const std::string& option,
   print_config_cond("kissat", Configuration::isBuiltWithKissat());
   print_config_cond("poly", Configuration::isBuiltWithPoly());
   print_config_cond("editline", Configuration::isBuiltWithEditline());
-  print_config_cond("symfpu", Configuration::isBuiltWithSymFPU());
 
   exit(0);
 }
diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp
index 0d1b25549..0e196c0e0 100644
--- a/src/theory/fp/fp_converter.cpp
+++ b/src/theory/fp/fp_converter.cpp
@@ -23,7 +23,6 @@
 #include "util/floatingpoint.h"
 #include "util/floatingpoint_literal_symfpu.h"
 
-#ifdef CVC5_USE_SYMFPU
 #include "symfpu/core/add.h"
 #include "symfpu/core/classify.h"
 #include "symfpu/core/compare.h"
@@ -38,9 +37,7 @@
 #include "symfpu/core/sqrt.h"
 #include "symfpu/utils/numberOfRoundingModes.h"
 #include "symfpu/utils/properties.h"
-#endif
 
-#ifdef CVC5_USE_SYMFPU
 namespace symfpu {
 using namespace ::cvc5::theory::fp::symfpuSymbolic;
 
@@ -143,11 +140,6 @@ void probabilityAnnotation<traits, traits::prop>(const traits::prop &p,
   return;
 }
 };
-#endif
-
-#ifndef CVC5_USE_SYMFPU
-#define SYMFPU_NUMBER_OF_ROUNDING_MODES 5
-#endif
 
 namespace cvc5 {
 namespace theory {
@@ -242,11 +234,7 @@ symbolicProposition symbolicProposition::operator^(
 
 bool symbolicRoundingMode::checkNodeType(const TNode n)
 {
-#ifdef CVC5_USE_SYMFPU
   return n.getType(false).isBitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES);
-#else
-  return false;
-#endif
 }
 
 symbolicRoundingMode::symbolicRoundingMode(const Node n) : nodeWrapper(n)
@@ -254,7 +242,6 @@ symbolicRoundingMode::symbolicRoundingMode(const Node n) : nodeWrapper(n)
   Assert(checkNodeType(*this));
 }
 
-#ifdef CVC5_USE_SYMFPU
 symbolicRoundingMode::symbolicRoundingMode(const unsigned v)
     : nodeWrapper(NodeManager::currentNM()->mkConst(
           BitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES, v)))
@@ -262,14 +249,6 @@ symbolicRoundingMode::symbolicRoundingMode(const unsigned v)
   Assert((v & (v - 1)) == 0 && v != 0);  // Exactly one bit set
   Assert(checkNodeType(*this));
 }
-#else
-symbolicRoundingMode::symbolicRoundingMode(const unsigned v)
-    : nodeWrapper(NodeManager::currentNM()->mkConst(
-          BitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES, v)))
-{
-  Unreachable();
-}
-#endif
 
 symbolicRoundingMode::symbolicRoundingMode(const symbolicRoundingMode &old)
     : nodeWrapper(old)
@@ -755,20 +734,17 @@ TypeNode floatingPointTypeInfo::getTypeNode(void) const
 
 FpConverter::FpConverter(context::UserContext* user)
     : d_additionalAssertions(user)
-#ifdef CVC5_USE_SYMFPU
       ,
       d_fpMap(user),
       d_rmMap(user),
       d_boolMap(user),
       d_ubvMap(user),
       d_sbvMap(user)
-#endif
 {
 }
 
 FpConverter::~FpConverter() {}
 
-#ifdef CVC5_USE_SYMFPU
 Node FpConverter::ufToNode(const fpt &format, const uf &u) const
 {
   NodeManager *nm = NodeManager::currentNM();
@@ -843,7 +819,6 @@ FpConverter::uf FpConverter::buildComponents(TNode current)
 
   return tmp;
 }
-#endif
 
 // Non-convertible things should only be added to the stack at the very start,
 // thus...
@@ -851,7 +826,6 @@ FpConverter::uf FpConverter::buildComponents(TNode current)
 
 Node FpConverter::convert(TNode node)
 {
-#ifdef CVC5_USE_SYMFPU
   std::vector<TNode> workStack;
   TNode result = node;
 
@@ -1704,9 +1678,6 @@ Node FpConverter::convert(TNode node)
   }
 
   return result;
-#else
-  Unimplemented() << "Conversion is dependent on SymFPU";
-#endif
 }
 
 #undef CVC5_FPCONV_PASSTHROUGH
@@ -1715,7 +1686,6 @@ Node FpConverter::getValue(Valuation &val, TNode var)
 {
   Assert(Theory::isLeafOf(var, THEORY_FP));
 
-#ifdef CVC5_USE_SYMFPU
   TypeNode t(var.getType());
 
   Assert(t.isRoundingMode() || t.isFloatingPoint())
@@ -1735,9 +1705,6 @@ Node FpConverter::getValue(Valuation &val, TNode 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
 }
 
 }  // namespace fp
diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h
index f1b7c8a83..9900c2987 100644
--- a/src/theory/fp/fp_converter.h
+++ b/src/theory/fp/fp_converter.h
@@ -33,9 +33,7 @@
 #include "util/floatingpoint_size.h"
 #include "util/hash.h"
 
-#ifdef CVC5_USE_SYMFPU
 #include "symfpu/core/unpackedFloat.h"
-#endif
 
 #ifdef CVC5_SYM_SYMBOLIC_EVAL
 // This allows debugging of the cvc5 symbolic back-end.
@@ -120,9 +118,7 @@ class symbolicProposition : public nodeWrapper
  protected:
   bool checkNodeType(const TNode node);
 
-#ifdef CVC5_USE_SYMFPU
   friend ::symfpu::ite<symbolicProposition, symbolicProposition>;  // For ITE
-#endif
 
  public:
   symbolicProposition(const Node n);
@@ -141,9 +137,7 @@ class symbolicRoundingMode : public nodeWrapper
  protected:
   bool checkNodeType(const TNode n);
 
-#ifdef CVC5_USE_SYMFPU
   friend ::symfpu::ite<symbolicProposition, symbolicRoundingMode>;  // For ITE
-#endif
 
  public:
   symbolicRoundingMode(const Node n);
@@ -183,10 +177,8 @@ class symbolicBitVector : public nodeWrapper
   bool checkNodeType(const TNode n);
   friend symbolicBitVector<!isSigned>;  // To allow conversion between the types
 
-#ifdef CVC5_USE_SYMFPU
   friend ::symfpu::ite<symbolicProposition,
                        symbolicBitVector<isSigned> >;  // For ITE
-#endif
 
  public:
   symbolicBitVector(const Node n);
@@ -314,7 +306,6 @@ class FpConverter
   context::CDList<Node> d_additionalAssertions;
 
  protected:
-#ifdef CVC5_USE_SYMFPU
   typedef symfpuSymbolic::traits traits;
   typedef ::symfpu::unpackedFloat<symfpuSymbolic::traits> uf;
   typedef symfpuSymbolic::traits::rm rm;
@@ -348,7 +339,6 @@ class FpConverter
 
   /* Creates the relevant components for a variable */
   uf buildComponents(TNode current);
-#endif
 };
 
 }  // namespace fp
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 3d81a2995..77dba0724 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -661,7 +661,7 @@ bool TheoryFp::isRegistered(TNode node) {
 
 void TheoryFp::preRegisterTerm(TNode node)
 {
-  if (Configuration::isBuiltWithSymFPU() && !options::fpExp())
+  if (!options::fpExp())
   {
     TypeNode tn = node.getType();
     if (tn.isFloatingPoint())
diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp
index 76f7d55cf..8bc7900de 100644
--- a/src/theory/fp/theory_fp_rewriter.cpp
+++ b/src/theory/fp/theory_fp_rewriter.cpp
@@ -1026,12 +1026,10 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite)
     bool result;
     switch (k)
     {
-#ifdef CVC5_USE_SYMFPU
       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;
     }
 
@@ -1050,11 +1048,7 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite)
     // \todo Add a proper interface for this sort of thing to FloatingPoint #1915
     return RewriteResponse(
         REWRITE_DONE,
-#ifdef CVC5_USE_SYMFPU
         NodeManager::currentNM()->mkConst((BitVector)arg0.getExponent())
-#else
-        node
-#endif
     );
   }
 
@@ -1066,11 +1060,7 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite)
 
     return RewriteResponse(
         REWRITE_DONE,
-#ifdef CVC5_USE_SYMFPU
         NodeManager::currentNM()->mkConst((BitVector)arg0.getSignificand())
-#else
-        node
-#endif
     );
   }
 
@@ -1080,7 +1070,6 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite)
 
     BitVector value;
 
-#ifdef CVC5_USE_SYMFPU
     /* \todo fix the numbering of rounding modes so this doesn't need
      * to call symfpu at all and remove the dependency on fp_converter.h #1915 */
     RoundingMode arg0(node[0].getConst<RoundingMode>());
@@ -1110,9 +1099,6 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite)
         Unreachable() << "Unknown rounding mode in roundingModeBitBlast";
         break;
     }
-#else
-    value = BitVector(5U, 0U);
-#endif
     return RewriteResponse(REWRITE_DONE,
                            NodeManager::currentNM()->mkConst(value));
   }
diff --git a/src/theory/fp/theory_fp_type_rules.cpp b/src/theory/fp/theory_fp_type_rules.cpp
index b78ef24c7..77c1ef8f0 100644
--- a/src/theory/fp/theory_fp_type_rules.cpp
+++ b/src/theory/fp/theory_fp_type_rules.cpp
@@ -727,7 +727,6 @@ TypeNode FloatingPointComponentExponent::computeType(NodeManager* nodeManager,
     }
   }
 
-#ifdef CVC5_USE_SYMFPU
   /* Need to create some symfpu objects as the size of bit-vector
    * that is needed for this component is dependent on the encoding
    * used (i.e. whether subnormals are forcibly normalised or not).
@@ -735,9 +734,6 @@ TypeNode FloatingPointComponentExponent::computeType(NodeManager* nodeManager,
    * back-end but it should't make a difference. */
   FloatingPointSize fps = operandType.getConst<FloatingPointSize>();
   uint32_t bw = FloatingPoint::getUnpackedExponentWidth(fps);
-#else
-  uint32_t bw = 2;
-#endif
   return nodeManager->mkBitVectorType(bw);
 }
 
@@ -767,13 +763,9 @@ TypeNode FloatingPointComponentSignificand::computeType(
     }
   }
 
-#ifdef CVC5_USE_SYMFPU
   /* As before we need to use some of sympfu. */
   FloatingPointSize fps = operandType.getConst<FloatingPointSize>();
   uint32_t bw = FloatingPoint::getUnpackedSignificandWidth(fps);
-#else
-  uint32_t bw = 1;
-#endif
   return nodeManager->mkBitVectorType(bw);
 }
 
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index 8ba43aa1a..d53b06151 100644
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -44,10 +44,6 @@ LogicInfo::LogicInfo()
 {
   for (TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id)
   {
-    if (id == THEORY_FP && !Configuration::isBuiltWithSymFPU())
-    {
-      continue;
-    }
     enableTheory(id);
   }
 }
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index 2938ddcca..71742dfce 100644
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -13,9 +13,6 @@
 # The build system configuration.
 ##
 
-configure_file(floatingpoint_literal_symfpu.h.in floatingpoint_literal_symfpu.h)
-configure_file(floatingpoint_literal_symfpu_traits.h.in
-               floatingpoint_literal_symfpu_traits.h)
 configure_file(rational.h.in rational.h)
 configure_file(integer.h.in integer.h)
 configure_file(real_algebraic_number.h.in real_algebraic_number.h)
diff --git a/src/util/floatingpoint_literal_symfpu.cpp b/src/util/floatingpoint_literal_symfpu.cpp
index c2c3fe77b..dc3dce6b9 100644
--- a/src/util/floatingpoint_literal_symfpu.cpp
+++ b/src/util/floatingpoint_literal_symfpu.cpp
@@ -16,7 +16,6 @@
 
 #include "base/check.h"
 
-#ifdef CVC5_USE_SYMFPU
 #include "symfpu/core/add.h"
 #include "symfpu/core/classify.h"
 #include "symfpu/core/compare.h"
@@ -31,11 +30,9 @@
 #include "symfpu/core/sqrt.h"
 #include "symfpu/utils/numberOfRoundingModes.h"
 #include "symfpu/utils/properties.h"
-#endif
 
 /* -------------------------------------------------------------------------- */
 
-#ifdef CVC5_USE_SYMFPU
 namespace symfpu {
 
 #define CVC5_LIT_ITE_DFN(T)                                            \
@@ -57,7 +54,6 @@ CVC5_LIT_ITE_DFN(::cvc5::symfpuLiteral::traits::ubv);
 
 #undef CVC5_LIT_ITE_DFN
 }  // namespace symfpu
-#endif
 
 /* -------------------------------------------------------------------------- */
 
@@ -65,44 +61,30 @@ namespace cvc5 {
 
 uint32_t FloatingPointLiteral::getUnpackedExponentWidth(FloatingPointSize& size)
 {
-#ifdef CVC5_USE_SYMFPU
   return SymFPUUnpackedFloatLiteral::exponentWidth(size);
-#else
-  unimplemented();
-  return 2;
-#endif
 }
 
 uint32_t FloatingPointLiteral::getUnpackedSignificandWidth(
     FloatingPointSize& size)
 {
-#ifdef CVC5_USE_SYMFPU
   return SymFPUUnpackedFloatLiteral::significandWidth(size);
-#else
-  unimplemented();
-  return 2;
-#endif
 }
 
 FloatingPointLiteral::FloatingPointLiteral(uint32_t exp_size,
                                            uint32_t sig_size,
                                            const BitVector& bv)
     : d_fp_size(exp_size, sig_size)
-#ifdef CVC5_USE_SYMFPU
       ,
       d_symuf(symfpu::unpack<symfpuLiteral::traits>(
           symfpuLiteral::Cvc5FPSize(exp_size, sig_size), bv))
-#endif
 {
 }
 
 FloatingPointLiteral::FloatingPointLiteral(
     const FloatingPointSize& size, FloatingPointLiteral::SpecialConstKind kind)
     : d_fp_size(size)
-#ifdef CVC5_USE_SYMFPU
       ,
       d_symuf(SymFPUUnpackedFloatLiteral::makeNaN(size))
-#endif
 {
   Assert(kind == FloatingPointLiteral::SpecialConstKind::FPNAN);
 }
@@ -112,12 +94,10 @@ FloatingPointLiteral::FloatingPointLiteral(
     FloatingPointLiteral::SpecialConstKind kind,
     bool sign)
     : d_fp_size(size)
-#ifdef CVC5_USE_SYMFPU
       ,
       d_symuf(kind == FloatingPointLiteral::SpecialConstKind::FPINF
                   ? SymFPUUnpackedFloatLiteral::makeInf(size, sign)
                   : SymFPUUnpackedFloatLiteral::makeZero(size, sign))
-#endif
 {
   Assert(kind == FloatingPointLiteral::SpecialConstKind::FPINF
          || kind == FloatingPointLiteral::SpecialConstKind::FPZERO);
@@ -126,10 +106,8 @@ FloatingPointLiteral::FloatingPointLiteral(
 FloatingPointLiteral::FloatingPointLiteral(const FloatingPointSize& size,
                                            const BitVector& bv)
     : d_fp_size(size)
-#ifdef CVC5_USE_SYMFPU
       ,
       d_symuf(symfpu::unpack<symfpuLiteral::traits>(size, bv))
-#endif
 {
 }
 
@@ -138,7 +116,6 @@ FloatingPointLiteral::FloatingPointLiteral(const FloatingPointSize& size,
                                            const BitVector& bv,
                                            bool signedBV)
     : d_fp_size(size)
-#ifdef CVC5_USE_SYMFPU
       ,
       d_symuf(signedBV ? symfpu::convertSBVToFloat<symfpuLiteral::traits>(
                   symfpuLiteral::Cvc5FPSize(size),
@@ -148,97 +125,61 @@ FloatingPointLiteral::FloatingPointLiteral(const FloatingPointSize& size,
                            symfpuLiteral::Cvc5FPSize(size),
                            symfpuLiteral::Cvc5RM(rm),
                            symfpuLiteral::Cvc5UnsignedBitVector(bv)))
-#endif
 {
 }
 
 BitVector FloatingPointLiteral::pack(void) const
 {
-#ifdef CVC5_USE_SYMFPU
   BitVector bv(symfpu::pack<symfpuLiteral::traits>(d_fp_size, d_symuf));
-#else
-  unimplemented();
-  BitVector bv(4u, 0u);
-#endif
   return bv;
 }
 
 FloatingPointLiteral FloatingPointLiteral::absolute(void) const
 {
-#ifdef CVC5_USE_SYMFPU
   return FloatingPointLiteral(
       d_fp_size, symfpu::absolute<symfpuLiteral::traits>(d_fp_size, d_symuf));
-#else
-  unimplemented();
-  return *this;
-#endif
 }
 
 FloatingPointLiteral FloatingPointLiteral::negate(void) const
 {
-#ifdef CVC5_USE_SYMFPU
   return FloatingPointLiteral(
       d_fp_size, symfpu::negate<symfpuLiteral::traits>(d_fp_size, d_symuf));
-#else
-  unimplemented();
-  return *this;
-#endif
 }
 
 FloatingPointLiteral FloatingPointLiteral::add(
     const RoundingMode& rm, const FloatingPointLiteral& arg) const
 {
-#ifdef CVC5_USE_SYMFPU
   Assert(d_fp_size == arg.d_fp_size);
   return FloatingPointLiteral(d_fp_size,
                               symfpu::add<symfpuLiteral::traits>(
                                   d_fp_size, rm, d_symuf, arg.d_symuf, true));
-#else
-  unimplemented();
-  return *this;
-#endif
 }
 
 FloatingPointLiteral FloatingPointLiteral::sub(
     const RoundingMode& rm, const FloatingPointLiteral& arg) const
 {
-#ifdef CVC5_USE_SYMFPU
   Assert(d_fp_size == arg.d_fp_size);
   return FloatingPointLiteral(d_fp_size,
                               symfpu::add<symfpuLiteral::traits>(
                                   d_fp_size, rm, d_symuf, arg.d_symuf, false));
-#else
-  unimplemented();
-  return *this;
-#endif
 }
 
 FloatingPointLiteral FloatingPointLiteral::mult(
     const RoundingMode& rm, const FloatingPointLiteral& arg) const
 {
-#ifdef CVC5_USE_SYMFPU
   Assert(d_fp_size == arg.d_fp_size);
   return FloatingPointLiteral(d_fp_size,
                               symfpu::multiply<symfpuLiteral::traits>(
                                   d_fp_size, rm, d_symuf, arg.d_symuf));
-#else
-  unimplemented();
-  return *this;
-#endif
 }
 
 FloatingPointLiteral FloatingPointLiteral::div(
     const RoundingMode& rm, const FloatingPointLiteral& arg) const
 {
-#ifdef CVC5_USE_SYMFPU
   Assert(d_fp_size == arg.d_fp_size);
   return FloatingPointLiteral(d_fp_size,
                               symfpu::divide<symfpuLiteral::traits>(
                                   d_fp_size, rm, d_symuf, arg.d_symuf));
-#else
-  unimplemented();
-  return *this;
-#endif
 }
 
 FloatingPointLiteral FloatingPointLiteral::fma(
@@ -246,276 +187,150 @@ FloatingPointLiteral FloatingPointLiteral::fma(
     const FloatingPointLiteral& arg1,
     const FloatingPointLiteral& arg2) const
 {
-#ifdef CVC5_USE_SYMFPU
   Assert(d_fp_size == arg1.d_fp_size);
   Assert(d_fp_size == arg2.d_fp_size);
   return FloatingPointLiteral(
       d_fp_size,
       symfpu::fma<symfpuLiteral::traits>(
           d_fp_size, rm, d_symuf, arg1.d_symuf, arg2.d_symuf));
-#else
-  unimplemented();
-  return *this;
-#endif
 }
 
 FloatingPointLiteral FloatingPointLiteral::sqrt(const RoundingMode& rm) const
 {
-#ifdef CVC5_USE_SYMFPU
   return FloatingPointLiteral(
       d_fp_size, symfpu::sqrt<symfpuLiteral::traits>(d_fp_size, rm, d_symuf));
-#else
-  unimplemented();
-  return *this;
-#endif
 }
 
 FloatingPointLiteral FloatingPointLiteral::rti(const RoundingMode& rm) const
 {
-#ifdef CVC5_USE_SYMFPU
   return FloatingPointLiteral(
       d_fp_size,
       symfpu::roundToIntegral<symfpuLiteral::traits>(d_fp_size, rm, d_symuf));
-#else
-  unimplemented();
-  return *this;
-#endif
 }
 
 FloatingPointLiteral FloatingPointLiteral::rem(
     const FloatingPointLiteral& arg) const
 {
-#ifdef CVC5_USE_SYMFPU
   Assert(d_fp_size == arg.d_fp_size);
   return FloatingPointLiteral(d_fp_size,
                               symfpu::remainder<symfpuLiteral::traits>(
                                   d_fp_size, d_symuf, arg.d_symuf));
-#else
-  unimplemented();
-  return *this;
-#endif
 }
 
 FloatingPointLiteral FloatingPointLiteral::maxTotal(
     const FloatingPointLiteral& arg, bool zeroCaseLeft) const
 {
-#ifdef CVC5_USE_SYMFPU
   Assert(d_fp_size == arg.d_fp_size);
   return FloatingPointLiteral(
       d_fp_size,
       symfpu::max<symfpuLiteral::traits>(
           d_fp_size, d_symuf, arg.d_symuf, zeroCaseLeft));
-#else
-  unimplemented();
-  return *this;
-#endif
 }
 
 FloatingPointLiteral FloatingPointLiteral::minTotal(
     const FloatingPointLiteral& arg, bool zeroCaseLeft) const
 {
-#ifdef CVC5_USE_SYMFPU
   Assert(d_fp_size == arg.d_fp_size);
   return FloatingPointLiteral(
       d_fp_size,
       symfpu::min<symfpuLiteral::traits>(
           d_fp_size, d_symuf, arg.d_symuf, zeroCaseLeft));
-#else
-  unimplemented();
-  return *this;
-#endif
 }
 
 bool FloatingPointLiteral::operator==(const FloatingPointLiteral& fp) const
 {
-#ifdef CVC5_USE_SYMFPU
   return ((d_fp_size == fp.d_fp_size)
           && symfpu::smtlibEqual<symfpuLiteral::traits>(
               d_fp_size, d_symuf, fp.d_symuf));
-#else
-  unimplemented();
-  return ((d_fp_size == fp.d_fp_size));
-#endif
 }
 
 bool FloatingPointLiteral::operator<=(const FloatingPointLiteral& arg) const
 {
-#ifdef CVC5_USE_SYMFPU
   Assert(d_fp_size == arg.d_fp_size);
   return symfpu::lessThanOrEqual<symfpuLiteral::traits>(
       d_fp_size, d_symuf, arg.d_symuf);
-#else
-  unimplemented();
-  return false;
-#endif
 }
 
 bool FloatingPointLiteral::operator<(const FloatingPointLiteral& arg) const
 {
-#ifdef CVC5_USE_SYMFPU
   Assert(d_fp_size == arg.d_fp_size);
   return symfpu::lessThan<symfpuLiteral::traits>(
       d_fp_size, d_symuf, arg.d_symuf);
-#else
-  unimplemented();
-  return false;
-#endif
 }
 
 BitVector FloatingPointLiteral::getExponent() const
 {
-#ifdef CVC5_USE_SYMFPU
   return d_symuf.exponent;
-#else
-  unimplemented();
-  Unreachable() << "no concrete implementation of FloatingPointLiteral";
-  return BitVector();
-#endif
 }
 
 BitVector FloatingPointLiteral::getSignificand() const
 {
-#ifdef CVC5_USE_SYMFPU
   return d_symuf.significand;
-#else
-  unimplemented();
-  Unreachable() << "no concrete implementation of FloatingPointLiteral";
-  return BitVector();
-#endif
 }
 
 bool FloatingPointLiteral::getSign() const
 {
-#ifdef CVC5_USE_SYMFPU
   return d_symuf.sign;
-#else
-  unimplemented();
-  Unreachable() << "no concrete implementation of FloatingPointLiteral";
-  return false;
-#endif
 }
 
 bool FloatingPointLiteral::isNormal(void) const
 {
-#ifdef CVC5_USE_SYMFPU
   return symfpu::isNormal<symfpuLiteral::traits>(d_fp_size, d_symuf);
-#else
-  unimplemented();
-  return false;
-#endif
 }
 
 bool FloatingPointLiteral::isSubnormal(void) const
 {
-#ifdef CVC5_USE_SYMFPU
   return symfpu::isSubnormal<symfpuLiteral::traits>(d_fp_size, d_symuf);
-#else
-  unimplemented();
-  return false;
-#endif
 }
 
 bool FloatingPointLiteral::isZero(void) const
 {
-#ifdef CVC5_USE_SYMFPU
   return symfpu::isZero<symfpuLiteral::traits>(d_fp_size, d_symuf);
-#else
-  unimplemented();
-  return false;
-#endif
 }
 
 bool FloatingPointLiteral::isInfinite(void) const
 {
-#ifdef CVC5_USE_SYMFPU
   return symfpu::isInfinite<symfpuLiteral::traits>(d_fp_size, d_symuf);
-#else
-  unimplemented();
-  return false;
-#endif
 }
 
 bool FloatingPointLiteral::isNaN(void) const
 {
-#ifdef CVC5_USE_SYMFPU
   return symfpu::isNaN<symfpuLiteral::traits>(d_fp_size, d_symuf);
-#else
-  unimplemented();
-  return false;
-#endif
 }
 
 bool FloatingPointLiteral::isNegative(void) const
 {
-#ifdef CVC5_USE_SYMFPU
   return symfpu::isNegative<symfpuLiteral::traits>(d_fp_size, d_symuf);
-#else
-  unimplemented();
-  return false;
-#endif
 }
 
 bool FloatingPointLiteral::isPositive(void) const
 {
-#ifdef CVC5_USE_SYMFPU
   return symfpu::isPositive<symfpuLiteral::traits>(d_fp_size, d_symuf);
-#else
-  unimplemented();
-  return false;
-#endif
 }
 
 FloatingPointLiteral FloatingPointLiteral::convert(
     const FloatingPointSize& target, const RoundingMode& rm) const
 {
-#ifdef CVC5_USE_SYMFPU
   return FloatingPointLiteral(
       target,
       symfpu::convertFloatToFloat<symfpuLiteral::traits>(
           d_fp_size, target, rm, d_symuf));
-#else
-  unimplemented();
-  return *this;
-#endif
 }
 
 BitVector FloatingPointLiteral::convertToSBVTotal(BitVectorSize width,
                                                   const RoundingMode& rm,
                                                   BitVector undefinedCase) const
 {
-#ifdef CVC5_USE_SYMFPU
   return symfpu::convertFloatToSBV<symfpuLiteral::traits>(
       d_fp_size, rm, d_symuf, width, undefinedCase);
-#else
-  unimplemented();
-  return undefinedCase;
-#endif
 }
 
 BitVector FloatingPointLiteral::convertToUBVTotal(BitVectorSize width,
                                                   const RoundingMode& rm,
                                                   BitVector undefinedCase) const
 {
-#ifdef CVC5_USE_SYMFPU
   return symfpu::convertFloatToUBV<symfpuLiteral::traits>(
       d_fp_size, rm, d_symuf, width, undefinedCase);
-#else
-  unimplemented();
-  return undefinedCase;
-#endif
 }
 
-#ifndef CVC5_USE_SYMFPU
-void FloatingPointLiteral::unimplemented(void)
-{
-  Unimplemented() << "no concrete implementation of FloatingPointLiteral";
-}
-
-size_t FloatingPointLiteral::hash(void) const
-{
-  unimplemented();
-  return 23;
-}
-#endif
-
 }  // namespace cvc5
diff --git a/src/util/floatingpoint_literal_symfpu.h.in b/src/util/floatingpoint_literal_symfpu.h
index 54827a308..5b2b0f7c8 100644
--- a/src/util/floatingpoint_literal_symfpu.h.in
+++ b/src/util/floatingpoint_literal_symfpu.h
@@ -20,20 +20,16 @@
 #define CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_H
 
 #include "util/bitvector.h"
-#include "util/floatingpoint_size.h"
 #include "util/floatingpoint_literal_symfpu_traits.h"
+#include "util/floatingpoint_size.h"
 #include "util/roundingmode.h"
 
 /* -------------------------------------------------------------------------- */
 
 namespace cvc5 {
 
-// clang-format off
-#if @CVC5_USE_SYMFPU@
-// clang-format on
 using SymFPUUnpackedFloatLiteral =
     ::symfpu::unpackedFloat<symfpuLiteral::traits>;
-#endif
 
 class FloatingPointLiteral
 {
@@ -65,13 +61,6 @@ class FloatingPointLiteral
    */
   static uint32_t getUnpackedSignificandWidth(FloatingPointSize& size);
 
-// clang-format off
-#if !@CVC5_USE_SYMFPU@
-  // clang-format on
-  /** Catch-all for unimplemented functions. */
-  static void unimplemented(void);
-#endif
-
   /** Constructors. */
 
   /** Create a FP literal from its IEEE bit-vector representation. */
@@ -197,18 +186,10 @@ class FloatingPointLiteral
   BitVector convertToUBVTotal(BitVectorSize width,
                               const RoundingMode& rm,
                               BitVector undefinedCase) const;
-// clang-format off
-#if @CVC5_USE_SYMFPU@
-  // clang-format on
   /** Return wrapped floating-point literal. */
   const SymFPUUnpackedFloatLiteral& getSymUF() const { return d_symuf; }
-#else
-  /** Dummy hash function. */
-  size_t hash(void) const;
-#endif
 
  private:
-
   /**
    * Create a FP literal from unpacked representation.
    *
@@ -223,34 +204,19 @@ class FloatingPointLiteral
                        const bool sign,
                        const BitVector& exp,
                        const BitVector& sig)
-      : d_fp_size(size)
-// clang-format off
-#if @CVC5_USE_SYMFPU@
-        // clang-format on
-        ,
-        d_symuf(SymFPUUnpackedFloatLiteral(sign, exp, sig))
-#endif
+      : d_fp_size(size), d_symuf(SymFPUUnpackedFloatLiteral(sign, exp, sig))
   {
   }
 
-// clang-format off
-#if @CVC5_USE_SYMFPU@
-  // clang-format on
-
   /** Create a FP literal from a symFPU unpacked float. */
   FloatingPointLiteral(const FloatingPointSize& size,
                        SymFPUUnpackedFloatLiteral symuf)
       : d_fp_size(size), d_symuf(symuf){};
-#endif
 
   /** The floating-point size of this floating-point literal. */
   FloatingPointSize d_fp_size;
-// clang-format off
-#if @CVC5_USE_SYMFPU@
-  // clang-format on
   /** The actual floating-point value, a SymFPU unpackedFloat. */
   SymFPUUnpackedFloatLiteral d_symuf;
-#endif
 };
 
 /* -------------------------------------------------------------------------- */
diff --git a/src/util/floatingpoint_literal_symfpu_traits.cpp b/src/util/floatingpoint_literal_symfpu_traits.cpp
index 071b69912..0f46708b0 100644
--- a/src/util/floatingpoint_literal_symfpu_traits.cpp
+++ b/src/util/floatingpoint_literal_symfpu_traits.cpp
@@ -13,8 +13,6 @@
  * SymFPU glue code for floating-point values.
  */
 
-#if CVC5_USE_SYMFPU
-
 #include "util/floatingpoint_literal_symfpu_traits.h"
 
 #include "base/check.h"
@@ -413,4 +411,3 @@ void traits::invariant(const traits::prop& p)
 }
 }  // namespace symfpuLiteral
 }  // namespace cvc5
-#endif
diff --git a/src/util/floatingpoint_literal_symfpu_traits.h.in b/src/util/floatingpoint_literal_symfpu_traits.h
index 76d2f47e2..bc5caaf88 100644
--- a/src/util/floatingpoint_literal_symfpu_traits.h.in
+++ b/src/util/floatingpoint_literal_symfpu_traits.h
@@ -25,16 +25,12 @@
 #ifndef CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_TRAITS_H
 #define CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_TRAITS_H
 
-// clang-format off
-#if @CVC5_USE_SYMFPU@
-// clang-format on
+#include <symfpu/core/unpackedFloat.h>
 
 #include "util/bitvector.h"
 #include "util/floatingpoint_size.h"
 #include "util/roundingmode.h"
 
-#include <symfpu/core/unpackedFloat.h>
-
 /* -------------------------------------------------------------------------- */
 
 namespace cvc5 {
@@ -258,7 +254,6 @@ class wrappedBitVector : public BitVector
                                      Cvc5BitWidth lower) const;
 };
 }  // namespace symfpuLiteral
-}
+}  // namespace cvc5
 
 #endif
-#endif