FP: Rename FpConverter to FpWordBlaster. (#7170)

6 files changed, 190 insertions, 195 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 42434adab..223d3ff1f 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -705,8 +705,8 @@ libcvc5_add_sources(
   theory/evaluator.h
   theory/ext_theory.cpp
   theory/ext_theory.h
-  theory/fp/fp_converter.cpp
-  theory/fp/fp_converter.h
+  theory/fp/fp_word_blaster.cpp
+  theory/fp/fp_word_blaster.h
   theory/fp/fp_expand_defs.cpp
   theory/fp/fp_expand_defs.h
   theory/fp/theory_fp.cpp
diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_word_blaster.cpp
index f6f1f3bb3..70d77abed 100644
--- a/src/theory/fp/fp_converter.cpp
+++ b/src/theory/fp/fp_word_blaster.cpp
@@ -13,16 +13,12 @@
  * Conversion of floating-point operations to bit-vectors using symfpu.
  */
 
-#include "theory/fp/fp_converter.h"
+#include "theory/fp/fp_word_blaster.h"
 
 #include <vector>
 
 #include "base/check.h"
 #include "expr/node_builder.h"
-#include "theory/theory.h"  // theory.h Only needed for the leaf test
-#include "util/floatingpoint.h"
-#include "util/floatingpoint_literal_symfpu.h"
-
 #include "symfpu/core/add.h"
 #include "symfpu/core/classify.h"
 #include "symfpu/core/compare.h"
@@ -37,6 +33,9 @@
 #include "symfpu/core/sqrt.h"
 #include "symfpu/utils/numberOfRoundingModes.h"
 #include "symfpu/utils/properties.h"
+#include "theory/theory.h"  // theory.h Only needed for the leaf test
+#include "util/floatingpoint.h"
+#include "util/floatingpoint_literal_symfpu.h"
 
 namespace symfpu {
 using namespace ::cvc5::theory::fp::symfpuSymbolic;
@@ -120,26 +119,26 @@ CVC5_SYM_ITE_DFN(traits::ubv);
 #undef CVC5_SYM_ITE_DFN
 
 template <>
-traits::ubv orderEncode<traits, traits::ubv>(const traits::ubv &b)
+traits::ubv orderEncode<traits, traits::ubv>(const traits::ubv& b)
 {
   return orderEncodeBitwise<traits, traits::ubv>(b);
 }
 
 template <>
-stickyRightShiftResult<traits> stickyRightShift(const traits::ubv &input,
-                                                const traits::ubv &shiftAmount)
+stickyRightShiftResult<traits> stickyRightShift(const traits::ubv& input,
+                                                const traits::ubv& shiftAmount)
 {
   return stickyRightShiftBitwise<traits>(input, shiftAmount);
 }
 
 template <>
-void probabilityAnnotation<traits, traits::prop>(const traits::prop &p,
-                                                 const probability &pr)
+void probabilityAnnotation<traits, traits::prop>(const traits::prop& p,
+                                                 const probability& pr)
 {
   // For now, do nothing...
   return;
 }
-};
+};  // namespace symfpu
 
 namespace cvc5 {
 namespace theory {
@@ -168,9 +167,9 @@ void traits::invariant(const bool b)
   return;
 }
 
-void traits::precondition(const prop &p) { return; }
-void traits::postcondition(const prop &p) { return; }
-void traits::invariant(const prop &p) { return; }
+void traits::precondition(const prop& p) { return; }
+void traits::postcondition(const prop& p) { return; }
+void traits::invariant(const prop& p) { return; }
 // This allows us to use the symfpu literal / symbolic assertions in the
 // symbolic back-end
 typedef traits t;
@@ -187,46 +186,46 @@ symbolicProposition::symbolicProposition(const Node n) : nodeWrapper(n)
 }  // Only used within this header so could be friend'd
 symbolicProposition::symbolicProposition(bool v)
     : nodeWrapper(
-          NodeManager::currentNM()->mkConst(BitVector(1U, (v ? 1U : 0U))))
+        NodeManager::currentNM()->mkConst(BitVector(1U, (v ? 1U : 0U))))
 {
   Assert(checkNodeType(*this));
 }
 
-symbolicProposition::symbolicProposition(const symbolicProposition &old)
+symbolicProposition::symbolicProposition(const symbolicProposition& old)
     : nodeWrapper(old)
 {
   Assert(checkNodeType(*this));
 }
 
-symbolicProposition symbolicProposition::operator!(void)const
+symbolicProposition symbolicProposition::operator!(void) const
 {
   return symbolicProposition(
       NodeManager::currentNM()->mkNode(kind::BITVECTOR_NOT, *this));
 }
 
 symbolicProposition symbolicProposition::operator&&(
-    const symbolicProposition &op) const
+    const symbolicProposition& op) const
 {
   return symbolicProposition(
       NodeManager::currentNM()->mkNode(kind::BITVECTOR_AND, *this, op));
 }
 
 symbolicProposition symbolicProposition::operator||(
-    const symbolicProposition &op) const
+    const symbolicProposition& op) const
 {
   return symbolicProposition(
       NodeManager::currentNM()->mkNode(kind::BITVECTOR_OR, *this, op));
 }
 
 symbolicProposition symbolicProposition::operator==(
-    const symbolicProposition &op) const
+    const symbolicProposition& op) const
 {
   return symbolicProposition(
       NodeManager::currentNM()->mkNode(kind::BITVECTOR_COMP, *this, op));
 }
 
 symbolicProposition symbolicProposition::operator^(
-    const symbolicProposition &op) const
+    const symbolicProposition& op) const
 {
   return symbolicProposition(
       NodeManager::currentNM()->mkNode(kind::BITVECTOR_XOR, *this, op));
@@ -244,13 +243,13 @@ symbolicRoundingMode::symbolicRoundingMode(const Node n) : nodeWrapper(n)
 
 symbolicRoundingMode::symbolicRoundingMode(const unsigned v)
     : nodeWrapper(NodeManager::currentNM()->mkConst(
-          BitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES, v)))
+        BitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES, v)))
 {
   Assert((v & (v - 1)) == 0 && v != 0);  // Exactly one bit set
   Assert(checkNodeType(*this));
 }
 
-symbolicRoundingMode::symbolicRoundingMode(const symbolicRoundingMode &old)
+symbolicRoundingMode::symbolicRoundingMode(const symbolicRoundingMode& old)
     : nodeWrapper(old)
 {
   Assert(checkNodeType(*this));
@@ -258,7 +257,7 @@ symbolicRoundingMode::symbolicRoundingMode(const symbolicRoundingMode &old)
 
 symbolicProposition symbolicRoundingMode::valid(void) const
 {
-  NodeManager *nm = NodeManager::currentNM();
+  NodeManager* nm = NodeManager::currentNM();
   Node zero(nm->mkConst(BitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES, 0u)));
 
   // Is there a better encoding of this?
@@ -278,7 +277,7 @@ symbolicProposition symbolicRoundingMode::valid(void) const
 }
 
 symbolicProposition symbolicRoundingMode::operator==(
-    const symbolicRoundingMode &op) const
+    const symbolicRoundingMode& op) const
 {
   return symbolicProposition(
       NodeManager::currentNM()->mkNode(kind::BITVECTOR_COMP, *this, op));
@@ -288,7 +287,7 @@ template <bool isSigned>
 Node symbolicBitVector<isSigned>::boolNodeToBV(Node node) const
 {
   Assert(node.getType().isBoolean());
-  NodeManager *nm = NodeManager::currentNM();
+  NodeManager* nm = NodeManager::currentNM();
   return nm->mkNode(kind::ITE,
                     node,
                     nm->mkConst(BitVector(1U, 1U)),
@@ -300,7 +299,7 @@ Node symbolicBitVector<isSigned>::BVToBoolNode(Node node) const
 {
   Assert(node.getType().isBitVector());
   Assert(node.getType().getBitVectorSize() == 1);
-  NodeManager *nm = NodeManager::currentNM();
+  NodeManager* nm = NodeManager::currentNM();
   return nm->mkNode(kind::EQUAL, node, nm->mkConst(BitVector(1U, 1U)));
 }
 
@@ -334,19 +333,19 @@ symbolicBitVector<isSigned>::symbolicBitVector(const bwt w, const unsigned v)
   Assert(checkNodeType(*this));
 }
 template <bool isSigned>
-symbolicBitVector<isSigned>::symbolicBitVector(const symbolicProposition &p)
+symbolicBitVector<isSigned>::symbolicBitVector(const symbolicProposition& p)
     : nodeWrapper(fromProposition(p))
 {
 }
 template <bool isSigned>
 symbolicBitVector<isSigned>::symbolicBitVector(
-    const symbolicBitVector<isSigned> &old)
+    const symbolicBitVector<isSigned>& old)
     : nodeWrapper(old)
 {
   Assert(checkNodeType(*this));
 }
 template <bool isSigned>
-symbolicBitVector<isSigned>::symbolicBitVector(const BitVector &old)
+symbolicBitVector<isSigned>::symbolicBitVector(const BitVector& old)
     : nodeWrapper(NodeManager::currentNM()->mkConst(old))
 {
   Assert(checkNodeType(*this));
@@ -360,17 +359,17 @@ bwt symbolicBitVector<isSigned>::getWidth(void) const
 
 /*** Constant creation and test ***/
 template <bool isSigned>
-symbolicBitVector<isSigned> symbolicBitVector<isSigned>::one(const bwt &w)
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::one(const bwt& w)
 {
   return symbolicBitVector<isSigned>(w, 1);
 }
 template <bool isSigned>
-symbolicBitVector<isSigned> symbolicBitVector<isSigned>::zero(const bwt &w)
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::zero(const bwt& w)
 {
   return symbolicBitVector<isSigned>(w, 0);
 }
 template <bool isSigned>
-symbolicBitVector<isSigned> symbolicBitVector<isSigned>::allOnes(const bwt &w)
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::allOnes(const bwt& w)
 {
   return symbolicBitVector<isSigned>(~zero(w));
 }
@@ -387,7 +386,7 @@ symbolicProposition symbolicBitVector<isSigned>::isAllZeros() const
 }
 
 template <>
-symbolicBitVector<true> symbolicBitVector<true>::maxValue(const bwt &w)
+symbolicBitVector<true> symbolicBitVector<true>::maxValue(const bwt& w)
 {
   symbolicBitVector<true> leadingZero(symbolicBitVector<true>::zero(1));
   symbolicBitVector<true> base(symbolicBitVector<true>::allOnes(w - 1));
@@ -397,13 +396,13 @@ symbolicBitVector<true> symbolicBitVector<true>::maxValue(const bwt &w)
 }
 
 template <>
-symbolicBitVector<false> symbolicBitVector<false>::maxValue(const bwt &w)
+symbolicBitVector<false> symbolicBitVector<false>::maxValue(const bwt& w)
 {
   return symbolicBitVector<false>::allOnes(w);
 }
 
 template <>
-symbolicBitVector<true> symbolicBitVector<true>::minValue(const bwt &w)
+symbolicBitVector<true> symbolicBitVector<true>::minValue(const bwt& w)
 {
   symbolicBitVector<true> leadingOne(symbolicBitVector<true>::one(1));
   symbolicBitVector<true> base(symbolicBitVector<true>::zero(w - 1));
@@ -413,7 +412,7 @@ symbolicBitVector<true> symbolicBitVector<true>::minValue(const bwt &w)
 }
 
 template <>
-symbolicBitVector<false> symbolicBitVector<false>::minValue(const bwt &w)
+symbolicBitVector<false> symbolicBitVector<false>::minValue(const bwt& w)
 {
   return symbolicBitVector<false>::zero(w);
 }
@@ -421,7 +420,7 @@ symbolicBitVector<false> symbolicBitVector<false>::minValue(const bwt &w)
 /*** Operators ***/
 template <bool isSigned>
 symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator<<(
-    const symbolicBitVector<isSigned> &op) const
+    const symbolicBitVector<isSigned>& op) const
 {
   return symbolicBitVector<isSigned>(
       NodeManager::currentNM()->mkNode(kind::BITVECTOR_SHL, *this, op));
@@ -429,7 +428,7 @@ symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator<<(
 
 template <bool isSigned>
 symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator>>(
-    const symbolicBitVector<isSigned> &op) const
+    const symbolicBitVector<isSigned>& op) const
 {
   return symbolicBitVector<isSigned>(NodeManager::currentNM()->mkNode(
       (isSigned) ? kind::BITVECTOR_ASHR : kind::BITVECTOR_LSHR, *this, op));
@@ -437,7 +436,7 @@ symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator>>(
 
 template <bool isSigned>
 symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator|(
-    const symbolicBitVector<isSigned> &op) const
+    const symbolicBitVector<isSigned>& op) const
 {
   return symbolicBitVector<isSigned>(
       NodeManager::currentNM()->mkNode(kind::BITVECTOR_OR, *this, op));
@@ -445,7 +444,7 @@ symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator|(
 
 template <bool isSigned>
 symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator&(
-    const symbolicBitVector<isSigned> &op) const
+    const symbolicBitVector<isSigned>& op) const
 {
   return symbolicBitVector<isSigned>(
       NodeManager::currentNM()->mkNode(kind::BITVECTOR_AND, *this, op));
@@ -453,7 +452,7 @@ symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator&(
 
 template <bool isSigned>
 symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator+(
-    const symbolicBitVector<isSigned> &op) const
+    const symbolicBitVector<isSigned>& op) const
 {
   return symbolicBitVector<isSigned>(
       NodeManager::currentNM()->mkNode(kind::BITVECTOR_ADD, *this, op));
@@ -461,7 +460,7 @@ symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator+(
 
 template <bool isSigned>
 symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator-(
-    const symbolicBitVector<isSigned> &op) const
+    const symbolicBitVector<isSigned>& op) const
 {
   return symbolicBitVector<isSigned>(
       NodeManager::currentNM()->mkNode(kind::BITVECTOR_SUB, *this, op));
@@ -469,7 +468,7 @@ symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator-(
 
 template <bool isSigned>
 symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator*(
-    const symbolicBitVector<isSigned> &op) const
+    const symbolicBitVector<isSigned>& op) const
 {
   return symbolicBitVector<isSigned>(
       NodeManager::currentNM()->mkNode(kind::BITVECTOR_MULT, *this, op));
@@ -477,7 +476,7 @@ symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator*(
 
 template <bool isSigned>
 symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator/(
-    const symbolicBitVector<isSigned> &op) const
+    const symbolicBitVector<isSigned>& op) const
 {
   return symbolicBitVector<isSigned>(NodeManager::currentNM()->mkNode(
       (isSigned) ? kind::BITVECTOR_SDIV : kind::BITVECTOR_UDIV, *this, op));
@@ -485,7 +484,7 @@ symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator/(
 
 template <bool isSigned>
 symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator%(
-    const symbolicBitVector<isSigned> &op) const
+    const symbolicBitVector<isSigned>& op) const
 {
   return symbolicBitVector<isSigned>(NodeManager::currentNM()->mkNode(
       (isSigned) ? kind::BITVECTOR_SREM : kind::BITVECTOR_UREM, *this, op));
@@ -499,7 +498,7 @@ symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator-(void) const
 }
 
 template <bool isSigned>
-symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator~(void)const
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::operator~(void) const
 {
   return symbolicBitVector<isSigned>(
       NodeManager::currentNM()->mkNode(kind::BITVECTOR_NOT, *this));
@@ -521,7 +520,7 @@ symbolicBitVector<isSigned> symbolicBitVector<isSigned>::decrement() const
 
 template <bool isSigned>
 symbolicBitVector<isSigned> symbolicBitVector<isSigned>::signExtendRightShift(
-    const symbolicBitVector<isSigned> &op) const
+    const symbolicBitVector<isSigned>& op) const
 {
   return symbolicBitVector<isSigned>(
       NodeManager::currentNM()->mkNode(kind::BITVECTOR_ASHR, *this, op));
@@ -531,14 +530,14 @@ symbolicBitVector<isSigned> symbolicBitVector<isSigned>::signExtendRightShift(
 // No overflow checking so these are the same as other operations
 template <bool isSigned>
 symbolicBitVector<isSigned> symbolicBitVector<isSigned>::modularLeftShift(
-    const symbolicBitVector<isSigned> &op) const
+    const symbolicBitVector<isSigned>& op) const
 {
   return *this << op;
 }
 
 template <bool isSigned>
 symbolicBitVector<isSigned> symbolicBitVector<isSigned>::modularRightShift(
-    const symbolicBitVector<isSigned> &op) const
+    const symbolicBitVector<isSigned>& op) const
 {
   return *this >> op;
 }
@@ -559,7 +558,7 @@ symbolicBitVector<isSigned> symbolicBitVector<isSigned>::modularDecrement()
 
 template <bool isSigned>
 symbolicBitVector<isSigned> symbolicBitVector<isSigned>::modularAdd(
-    const symbolicBitVector<isSigned> &op) const
+    const symbolicBitVector<isSigned>& op) const
 {
   return *this + op;
 }
@@ -574,7 +573,7 @@ symbolicBitVector<isSigned> symbolicBitVector<isSigned>::modularNegate() const
 
 template <bool isSigned>
 symbolicProposition symbolicBitVector<isSigned>::operator==(
-    const symbolicBitVector<isSigned> &op) const
+    const symbolicBitVector<isSigned>& op) const
 {
   return symbolicProposition(
       NodeManager::currentNM()->mkNode(kind::BITVECTOR_COMP, *this, op));
@@ -582,7 +581,7 @@ symbolicProposition symbolicBitVector<isSigned>::operator==(
 
 template <bool isSigned>
 symbolicProposition symbolicBitVector<isSigned>::operator<=(
-    const symbolicBitVector<isSigned> &op) const
+    const symbolicBitVector<isSigned>& op) const
 {
   // Consider adding kind::BITVECTOR_SLEBV and BITVECTOR_ULEBV
   return (*this < op) || (*this == op);
@@ -590,14 +589,14 @@ symbolicProposition symbolicBitVector<isSigned>::operator<=(
 
 template <bool isSigned>
 symbolicProposition symbolicBitVector<isSigned>::operator>=(
-    const symbolicBitVector<isSigned> &op) const
+    const symbolicBitVector<isSigned>& op) const
 {
   return (*this > op) || (*this == op);
 }
 
 template <bool isSigned>
 symbolicProposition symbolicBitVector<isSigned>::operator<(
-    const symbolicBitVector<isSigned> &op) const
+    const symbolicBitVector<isSigned>& op) const
 {
   return symbolicProposition(NodeManager::currentNM()->mkNode(
       (isSigned) ? kind::BITVECTOR_SLTBV : kind::BITVECTOR_ULTBV, *this, op));
@@ -605,7 +604,7 @@ symbolicProposition symbolicBitVector<isSigned>::operator<(
 
 template <bool isSigned>
 symbolicProposition symbolicBitVector<isSigned>::operator>(
-    const symbolicBitVector<isSigned> &op) const
+    const symbolicBitVector<isSigned>& op) const
 {
   return symbolicProposition(NodeManager::currentNM()->mkNode(
       (isSigned) ? kind::BITVECTOR_SLTBV : kind::BITVECTOR_ULTBV, op, *this));
@@ -630,7 +629,7 @@ symbolicBitVector<true> symbolicBitVector<true>::extend(bwt extension) const
 {
   NodeBuilder construct(kind::BITVECTOR_SIGN_EXTEND);
   construct << NodeManager::currentNM()->mkConst<BitVectorSignExtend>(
-                   BitVectorSignExtend(extension))
+      BitVectorSignExtend(extension))
             << *this;
 
   return symbolicBitVector<true>(construct);
@@ -641,7 +640,7 @@ symbolicBitVector<false> symbolicBitVector<false>::extend(bwt extension) const
 {
   NodeBuilder construct(kind::BITVECTOR_ZERO_EXTEND);
   construct << NodeManager::currentNM()->mkConst<BitVectorZeroExtend>(
-                   BitVectorZeroExtend(extension))
+      BitVectorZeroExtend(extension))
             << *this;
 
   return symbolicBitVector<false>(construct);
@@ -655,7 +654,7 @@ symbolicBitVector<isSigned> symbolicBitVector<isSigned>::contract(
 
   NodeBuilder construct(kind::BITVECTOR_EXTRACT);
   construct << NodeManager::currentNM()->mkConst<BitVectorExtract>(
-                   BitVectorExtract((this->getWidth() - 1) - reduction, 0))
+      BitVectorExtract((this->getWidth() - 1) - reduction, 0))
             << *this;
 
   return symbolicBitVector<isSigned>(construct);
@@ -683,7 +682,7 @@ symbolicBitVector<isSigned> symbolicBitVector<isSigned>::resize(
 
 template <bool isSigned>
 symbolicBitVector<isSigned> symbolicBitVector<isSigned>::matchWidth(
-    const symbolicBitVector<isSigned> &op) const
+    const symbolicBitVector<isSigned>& op) const
 {
   Assert(this->getWidth() <= op.getWidth());
   return this->extend(op.getWidth() - this->getWidth());
@@ -691,7 +690,7 @@ symbolicBitVector<isSigned> symbolicBitVector<isSigned>::matchWidth(
 
 template <bool isSigned>
 symbolicBitVector<isSigned> symbolicBitVector<isSigned>::append(
-    const symbolicBitVector<isSigned> &op) const
+    const symbolicBitVector<isSigned>& op) const
 {
   return symbolicBitVector<isSigned>(
       NodeManager::currentNM()->mkNode(kind::BITVECTOR_CONCAT, *this, op));
@@ -706,7 +705,7 @@ symbolicBitVector<isSigned> symbolicBitVector<isSigned>::extract(
 
   NodeBuilder construct(kind::BITVECTOR_EXTRACT);
   construct << NodeManager::currentNM()->mkConst<BitVectorExtract>(
-                   BitVectorExtract(upper, lower))
+      BitVectorExtract(upper, lower))
             << *this;
 
   return symbolicBitVector<isSigned>(construct);
@@ -721,7 +720,7 @@ floatingPointTypeInfo::floatingPointTypeInfo(unsigned exp, unsigned sig)
     : FloatingPointSize(exp, sig)
 {
 }
-floatingPointTypeInfo::floatingPointTypeInfo(const floatingPointTypeInfo &old)
+floatingPointTypeInfo::floatingPointTypeInfo(const floatingPointTypeInfo& old)
     : FloatingPointSize(old)
 {
 }
@@ -730,11 +729,10 @@ TypeNode floatingPointTypeInfo::getTypeNode(void) const
 {
   return NodeManager::currentNM()->mkFloatingPointType(*this);
 }
-}
+}  // namespace symfpuSymbolic
 
-FpConverter::FpConverter(context::UserContext* user)
-    : d_additionalAssertions(user)
-      ,
+FpWordBlaster::FpWordBlaster(context::UserContext* user)
+    : d_additionalAssertions(user),
       d_fpMap(user),
       d_rmMap(user),
       d_boolMap(user),
@@ -743,11 +741,11 @@ FpConverter::FpConverter(context::UserContext* user)
 {
 }
 
-FpConverter::~FpConverter() {}
+FpWordBlaster::~FpWordBlaster() {}
 
-Node FpConverter::ufToNode(const fpt &format, const uf &u) const
+Node FpWordBlaster::ufToNode(const fpt& format, const uf& u) const
 {
-  NodeManager *nm = NodeManager::currentNM();
+  NodeManager* nm = NodeManager::currentNM();
 
   FloatingPointSize fps(format.getTypeNode().getConst<FloatingPointSize>());
 
@@ -761,9 +759,9 @@ Node FpConverter::ufToNode(const fpt &format, const uf &u) const
   return value;
 }
 
-Node FpConverter::rmToNode(const rm &r) const
+Node FpWordBlaster::rmToNode(const rm& r) const
 {
-  NodeManager *nm = NodeManager::currentNM();
+  NodeManager* nm = NodeManager::currentNM();
 
   Node transVar = r;
 
@@ -792,22 +790,22 @@ Node FpConverter::rmToNode(const rm &r) const
   return value;
 }
 
-Node FpConverter::propToNode(const prop &p) const
+Node FpWordBlaster::propToNode(const prop& p) const
 {
-  NodeManager *nm = NodeManager::currentNM();
+  NodeManager* nm = NodeManager::currentNM();
   Node value =
       nm->mkNode(kind::EQUAL, p, nm->mkConst(::cvc5::BitVector(1U, 1U)));
   return value;
 }
-Node FpConverter::ubvToNode(const ubv &u) const { return u; }
-Node FpConverter::sbvToNode(const sbv &s) const { return s; }
+Node FpWordBlaster::ubvToNode(const ubv& u) const { return u; }
+Node FpWordBlaster::sbvToNode(const sbv& s) const { return s; }
 // Creates the components constraint
-FpConverter::uf FpConverter::buildComponents(TNode current)
+FpWordBlaster::uf FpWordBlaster::buildComponents(TNode current)
 {
   Assert(Theory::isLeafOf(current, THEORY_FP)
          || current.getKind() == kind::FLOATINGPOINT_TO_FP_REAL);
 
-  NodeManager *nm = NodeManager::currentNM();
+  NodeManager* nm = NodeManager::currentNM();
   uf tmp(nm->mkNode(kind::FLOATINGPOINT_COMPONENT_NAN, current),
          nm->mkNode(kind::FLOATINGPOINT_COMPONENT_INF, current),
          nm->mkNode(kind::FLOATINGPOINT_COMPONENT_ZERO, current),
@@ -820,7 +818,7 @@ FpConverter::uf FpConverter::buildComponents(TNode current)
   return tmp;
 }
 
-Node FpConverter::convert(TNode node)
+Node FpWordBlaster::wordBlast(TNode node)
 {
   std::vector<TNode> visit;
   std::unordered_map<TNode, bool> visited;
@@ -936,18 +934,16 @@ Node FpConverter::convert(TNode node)
             /* ---- Arithmetic operators ---- */
             case kind::FLOATINGPOINT_ABS:
               Assert(d_fpMap.find(cur[0]) != d_fpMap.end());
-              d_fpMap.insert(
-                  cur,
-                  symfpu::absolute<traits>(fpt(t),
-                                           (*d_fpMap.find(cur[0])).second));
+              d_fpMap.insert(cur,
+                             symfpu::absolute<traits>(
+                                 fpt(t), (*d_fpMap.find(cur[0])).second));
               break;
 
             case kind::FLOATINGPOINT_NEG:
               Assert(d_fpMap.find(cur[0]) != d_fpMap.end());
-              d_fpMap.insert(
-                  cur,
-                  symfpu::negate<traits>(fpt(t),
-                                         (*d_fpMap.find(cur[0])).second));
+              d_fpMap.insert(cur,
+                             symfpu::negate<traits>(
+                                 fpt(t), (*d_fpMap.find(cur[0])).second));
               break;
 
             case kind::FLOATINGPOINT_SQRT:
@@ -1073,33 +1069,29 @@ Node FpConverter::convert(TNode node)
 
               Node IEEEBV(
                   nm->mkNode(kind::BITVECTOR_CONCAT, cur[0], cur[1], cur[2]));
-              d_fpMap.insert(
-                  cur, symfpu::unpack<traits>(fpt(t), IEEEBV));
+              d_fpMap.insert(cur, symfpu::unpack<traits>(fpt(t), IEEEBV));
             }
             break;
 
             case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR:
               Assert(cur[0].getType().isBitVector());
-              d_fpMap.insert(
-                  cur, symfpu::unpack<traits>(fpt(t), ubv(cur[0])));
+              d_fpMap.insert(cur, symfpu::unpack<traits>(fpt(t), ubv(cur[0])));
               break;
 
             case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR:
               Assert(d_rmMap.find(cur[0]) != d_rmMap.end());
-              d_fpMap.insert(cur,
-                             symfpu::convertSBVToFloat<traits>(
-                                 fpt(t),
-                                 (*d_rmMap.find(cur[0])).second,
-                                 sbv(cur[1])));
+              d_fpMap.insert(
+                  cur,
+                  symfpu::convertSBVToFloat<traits>(
+                      fpt(t), (*d_rmMap.find(cur[0])).second, sbv(cur[1])));
               break;
 
             case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR:
               Assert(d_rmMap.find(cur[0]) != d_rmMap.end());
-              d_fpMap.insert(cur,
-                             symfpu::convertUBVToFloat<traits>(
-                                 fpt(t),
-                                 (*d_rmMap.find(cur[0])).second,
-                                 ubv(cur[1])));
+              d_fpMap.insert(
+                  cur,
+                  symfpu::convertUBVToFloat<traits>(
+                      fpt(t), (*d_rmMap.find(cur[0])).second, ubv(cur[1])));
               break;
 
             case kind::FLOATINGPOINT_TO_FP_REAL:
@@ -1283,7 +1275,7 @@ Node FpConverter::convert(TNode node)
   return node;
 }
 
-Node FpConverter::getValue(Valuation &val, TNode var)
+Node FpWordBlaster::getValue(Valuation& val, TNode var)
 {
   Assert(Theory::isLeafOf(var, THEORY_FP));
 
diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_word_blaster.h
index d589eff60..f9ec4fd4e 100644
--- a/src/theory/fp/fp_converter.h
+++ b/src/theory/fp/fp_word_blaster.h
@@ -21,20 +21,19 @@
 
 #include "cvc5_private.h"
 
-#ifndef CVC5__THEORY__FP__FP_CONVERTER_H
-#define CVC5__THEORY__FP__FP_CONVERTER_H
+#ifndef CVC5__THEORY__FP__FP_WORD_BLASTER_H
+#define CVC5__THEORY__FP__FP_WORD_BLASTER_H
 
 #include "context/cdhashmap.h"
 #include "context/cdlist.h"
 #include "expr/node.h"
 #include "expr/type_node.h"
+#include "symfpu/core/unpackedFloat.h"
 #include "theory/valuation.h"
 #include "util/bitvector.h"
 #include "util/floatingpoint_size.h"
 #include "util/hash.h"
 
-#include "symfpu/core/unpackedFloat.h"
-
 #ifdef CVC5_SYM_SYMBOLIC_EVAL
 // This allows debugging of the cvc5 symbolic back-end.
 // By enabling this and disabling constant folding in the rewriter,
@@ -87,9 +86,9 @@ class traits
   static void precondition(const bool b);
   static void postcondition(const bool b);
   static void invariant(const bool b);
-  static void precondition(const prop &p);
-  static void postcondition(const prop &p);
-  static void invariant(const prop &p);
+  static void precondition(const prop& p);
+  static void postcondition(const prop& p);
+  static void invariant(const prop& p);
 };
 
 // Use the same type names as symfpu.
@@ -107,9 +106,9 @@ class nodeWrapper : public Node
  * allowing them to be traced via GDB.
  */
 #ifdef CVC5_SYM_SYMBOLIC_EVAL
-  nodeWrapper(const Node &n) : Node(theory::Rewriter::rewrite(n)) {}
+  nodeWrapper(const Node& n) : Node(theory::Rewriter::rewrite(n)) {}
 #else
-  nodeWrapper(const Node &n) : Node(n) {}
+  nodeWrapper(const Node& n) : Node(n) {}
 #endif
 };
 
@@ -123,13 +122,13 @@ class symbolicProposition : public nodeWrapper
  public:
   symbolicProposition(const Node n);
   symbolicProposition(bool v);
-  symbolicProposition(const symbolicProposition &old);
+  symbolicProposition(const symbolicProposition& old);
 
-  symbolicProposition operator!(void)const;
-  symbolicProposition operator&&(const symbolicProposition &op) const;
-  symbolicProposition operator||(const symbolicProposition &op) const;
-  symbolicProposition operator==(const symbolicProposition &op) const;
-  symbolicProposition operator^(const symbolicProposition &op) const;
+  symbolicProposition operator!(void) const;
+  symbolicProposition operator&&(const symbolicProposition& op) const;
+  symbolicProposition operator||(const symbolicProposition& op) const;
+  symbolicProposition operator==(const symbolicProposition& op) const;
+  symbolicProposition operator^(const symbolicProposition& op) const;
 };
 
 class symbolicRoundingMode : public nodeWrapper
@@ -142,10 +141,10 @@ class symbolicRoundingMode : public nodeWrapper
  public:
   symbolicRoundingMode(const Node n);
   symbolicRoundingMode(const unsigned v);
-  symbolicRoundingMode(const symbolicRoundingMode &old);
+  symbolicRoundingMode(const symbolicRoundingMode& old);
 
   symbolicProposition valid(void) const;
-  symbolicProposition operator==(const symbolicRoundingMode &op) const;
+  symbolicProposition operator==(const symbolicRoundingMode& op) const;
 };
 
 // Type function for mapping between types
@@ -183,68 +182,68 @@ class symbolicBitVector : public nodeWrapper
  public:
   symbolicBitVector(const Node n);
   symbolicBitVector(const bwt w, const unsigned v);
-  symbolicBitVector(const symbolicProposition &p);
-  symbolicBitVector(const symbolicBitVector<isSigned> &old);
-  symbolicBitVector(const BitVector &old);
+  symbolicBitVector(const symbolicProposition& p);
+  symbolicBitVector(const symbolicBitVector<isSigned>& old);
+  symbolicBitVector(const BitVector& old);
 
   bwt getWidth(void) const;
 
   /*** Constant creation and test ***/
-  static symbolicBitVector<isSigned> one(const bwt &w);
-  static symbolicBitVector<isSigned> zero(const bwt &w);
-  static symbolicBitVector<isSigned> allOnes(const bwt &w);
+  static symbolicBitVector<isSigned> one(const bwt& w);
+  static symbolicBitVector<isSigned> zero(const bwt& w);
+  static symbolicBitVector<isSigned> allOnes(const bwt& w);
 
   symbolicProposition isAllOnes() const;
   symbolicProposition isAllZeros() const;
 
-  static symbolicBitVector<isSigned> maxValue(const bwt &w);
-  static symbolicBitVector<isSigned> minValue(const bwt &w);
+  static symbolicBitVector<isSigned> maxValue(const bwt& w);
+  static symbolicBitVector<isSigned> minValue(const bwt& w);
 
   /*** Operators ***/
   symbolicBitVector<isSigned> operator<<(
-      const symbolicBitVector<isSigned> &op) const;
+      const symbolicBitVector<isSigned>& op) const;
   symbolicBitVector<isSigned> operator>>(
-      const symbolicBitVector<isSigned> &op) const;
+      const symbolicBitVector<isSigned>& op) const;
   symbolicBitVector<isSigned> operator|(
-      const symbolicBitVector<isSigned> &op) const;
+      const symbolicBitVector<isSigned>& op) const;
   symbolicBitVector<isSigned> operator&(
-      const symbolicBitVector<isSigned> &op) const;
+      const symbolicBitVector<isSigned>& op) const;
   symbolicBitVector<isSigned> operator+(
-      const symbolicBitVector<isSigned> &op) const;
+      const symbolicBitVector<isSigned>& op) const;
   symbolicBitVector<isSigned> operator-(
-      const symbolicBitVector<isSigned> &op) const;
+      const symbolicBitVector<isSigned>& op) const;
   symbolicBitVector<isSigned> operator*(
-      const symbolicBitVector<isSigned> &op) const;
+      const symbolicBitVector<isSigned>& op) const;
   symbolicBitVector<isSigned> operator/(
-      const symbolicBitVector<isSigned> &op) const;
+      const symbolicBitVector<isSigned>& op) const;
   symbolicBitVector<isSigned> operator%(
-      const symbolicBitVector<isSigned> &op) const;
+      const symbolicBitVector<isSigned>& op) const;
   symbolicBitVector<isSigned> operator-(void) const;
-  symbolicBitVector<isSigned> operator~(void)const;
+  symbolicBitVector<isSigned> operator~(void) const;
   symbolicBitVector<isSigned> increment() const;
   symbolicBitVector<isSigned> decrement() const;
   symbolicBitVector<isSigned> signExtendRightShift(
-      const symbolicBitVector<isSigned> &op) const;
+      const symbolicBitVector<isSigned>& op) const;
 
   /*** Modular operations ***/
   // This back-end doesn't do any overflow checking so these are the same as
   // other operations
   symbolicBitVector<isSigned> modularLeftShift(
-      const symbolicBitVector<isSigned> &op) const;
+      const symbolicBitVector<isSigned>& op) const;
   symbolicBitVector<isSigned> modularRightShift(
-      const symbolicBitVector<isSigned> &op) const;
+      const symbolicBitVector<isSigned>& op) const;
   symbolicBitVector<isSigned> modularIncrement() const;
   symbolicBitVector<isSigned> modularDecrement() const;
   symbolicBitVector<isSigned> modularAdd(
-      const symbolicBitVector<isSigned> &op) const;
+      const symbolicBitVector<isSigned>& op) const;
   symbolicBitVector<isSigned> modularNegate() const;
 
   /*** Comparisons ***/
-  symbolicProposition operator==(const symbolicBitVector<isSigned> &op) const;
-  symbolicProposition operator<=(const symbolicBitVector<isSigned> &op) const;
-  symbolicProposition operator>=(const symbolicBitVector<isSigned> &op) const;
-  symbolicProposition operator<(const symbolicBitVector<isSigned> &op) const;
-  symbolicProposition operator>(const symbolicBitVector<isSigned> &op) const;
+  symbolicProposition operator==(const symbolicBitVector<isSigned>& op) const;
+  symbolicProposition operator<=(const symbolicBitVector<isSigned>& op) const;
+  symbolicProposition operator>=(const symbolicBitVector<isSigned>& op) const;
+  symbolicProposition operator<(const symbolicBitVector<isSigned>& op) const;
+  symbolicProposition operator>(const symbolicBitVector<isSigned>& op) const;
 
   /*** Type conversion ***/
   // cvc5 nodes make no distinction between signed and unsigned, thus these are
@@ -257,9 +256,9 @@ class symbolicBitVector : public nodeWrapper
   symbolicBitVector<isSigned> contract(bwt reduction) const;
   symbolicBitVector<isSigned> resize(bwt newSize) const;
   symbolicBitVector<isSigned> matchWidth(
-      const symbolicBitVector<isSigned> &op) const;
+      const symbolicBitVector<isSigned>& op) const;
   symbolicBitVector<isSigned> append(
-      const symbolicBitVector<isSigned> &op) const;
+      const symbolicBitVector<isSigned>& op) const;
 
   // Inclusive of end points, thus if the same, extracts just one bit
   symbolicBitVector<isSigned> extract(bwt upper, bwt lower) const;
@@ -272,11 +271,11 @@ class floatingPointTypeInfo : public FloatingPointSize
  public:
   floatingPointTypeInfo(const TypeNode t);
   floatingPointTypeInfo(unsigned exp, unsigned sig);
-  floatingPointTypeInfo(const floatingPointTypeInfo &old);
+  floatingPointTypeInfo(const floatingPointTypeInfo& old);
 
   TypeNode getTypeNode(void) const;
 };
-}
+}  // namespace symfpuSymbolic
 
 /**
  * This class uses SymFPU to convert an expression containing floating-point
@@ -289,16 +288,16 @@ class floatingPointTypeInfo : public FloatingPointSize
  * and unpacking operations are avoided and to make best use of structural
  * sharing.
  */
-class FpConverter
+class FpWordBlaster
 {
  public:
   /** Constructor. */
-  FpConverter(context::UserContext*);
+  FpWordBlaster(context::UserContext*);
   /** Destructor. */
-  ~FpConverter();
+  ~FpWordBlaster();
 
   /** Adds a node to the conversion, returns the converted node */
-  Node convert(TNode);
+  Node wordBlast(TNode);
 
   /**
    * Gives the node representing the value of a word-blasted variable.
@@ -334,11 +333,11 @@ class FpConverter
    * constant of the right type.
    */
 
-  Node ufToNode(const fpt &, const uf &) const;
-  Node rmToNode(const rm &) const;
-  Node propToNode(const prop &) const;
-  Node ubvToNode(const ubv &) const;
-  Node sbvToNode(const sbv &) const;
+  Node ufToNode(const fpt&, const uf&) const;
+  Node rmToNode(const rm&) const;
+  Node propToNode(const prop&) const;
+  Node ubvToNode(const ubv&) const;
+  Node sbvToNode(const sbv&) const;
 
   /* Creates the relevant components for a variable */
   uf buildComponents(TNode current);
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index d4ecbd357..5ee5fd7d8 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -24,7 +24,7 @@
 #include "expr/skolem_manager.h"
 #include "options/fp_options.h"
 #include "smt/logic_exception.h"
-#include "theory/fp/fp_converter.h"
+#include "theory/fp/fp_word_blaster.h"
 #include "theory/fp/theory_fp_rewriter.h"
 #include "theory/output_channel.h"
 #include "theory/theory_model.h"
@@ -63,7 +63,7 @@ TheoryFp::TheoryFp(Env& env, OutputChannel& out, Valuation valuation)
     : Theory(THEORY_FP, env, out, valuation),
       d_notification(*this),
       d_registeredTerms(userContext()),
-      d_conv(new FpConverter(userContext())),
+      d_wordBlaster(new FpWordBlaster(userContext())),
       d_expansionRequested(false),
       d_realToFloatMap(userContext()),
       d_floatToRealMap(userContext()),
@@ -511,31 +511,34 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete)
   return false;
 }
 
-void TheoryFp::convertAndEquateTerm(TNode node)
+void TheoryFp::wordBlastAndEquateTerm(TNode node)
 {
-  Trace("fp-convertTerm") << "TheoryFp::convertTerm(): " << node << std::endl;
+  Trace("fp-wordBlastTerm")
+      << "TheoryFp::wordBlastTerm(): " << node << std::endl;
 
-  size_t oldSize = d_conv->d_additionalAssertions.size();
+  size_t oldSize = d_wordBlaster->d_additionalAssertions.size();
 
-  Node converted(d_conv->convert(node));
+  Node wordBlasted(d_wordBlaster->wordBlast(node));
 
-  size_t newSize = d_conv->d_additionalAssertions.size();
+  size_t newSize = d_wordBlaster->d_additionalAssertions.size();
 
-  if (converted != node) {
-    Debug("fp-convertTerm")
-        << "TheoryFp::convertTerm(): before " << node << std::endl;
-    Debug("fp-convertTerm")
-        << "TheoryFp::convertTerm(): after  " << converted << std::endl;
+  if (wordBlasted != node)
+  {
+    Debug("fp-wordBlastTerm")
+        << "TheoryFp::wordBlastTerm(): before " << node << std::endl;
+    Debug("fp-wordBlastTerm")
+        << "TheoryFp::wordBlastTerm(): after  " << wordBlasted << std::endl;
   }
 
   Assert(oldSize <= newSize);
 
   while (oldSize < newSize)
   {
-    Node addA = d_conv->d_additionalAssertions[oldSize];
+    Node addA = d_wordBlaster->d_additionalAssertions[oldSize];
 
-    Debug("fp-convertTerm") << "TheoryFp::convertTerm(): additional assertion  "
-                            << addA << std::endl;
+    Debug("fp-wordBlastTerm")
+        << "TheoryFp::wordBlastTerm(): additional assertion  " << addA
+        << std::endl;
 
     NodeManager* nm = NodeManager::currentNM();
 
@@ -546,13 +549,13 @@ void TheoryFp::convertAndEquateTerm(TNode node)
     ++oldSize;
   }
 
-  // Equate the floating-point atom and the converted one.
+  // Equate the floating-point atom and the wordBlasted one.
   // Also adds the bit-vectors to the bit-vector solver.
   if (node.getType().isBoolean())
   {
-    if (converted != node)
+    if (wordBlasted != node)
     {
-      Assert(converted.getType().isBitVector());
+      Assert(wordBlasted.getType().isBitVector());
 
       NodeManager* nm = NodeManager::currentNM();
 
@@ -560,7 +563,7 @@ void TheoryFp::convertAndEquateTerm(TNode node)
           nm->mkNode(kind::EQUAL,
                      node,
                      nm->mkNode(kind::EQUAL,
-                                converted,
+                                wordBlasted,
                                 nm->mkConst(::cvc5::BitVector(1U, 1U)))),
           InferenceId::FP_EQUATE_TERM);
     }
@@ -571,11 +574,12 @@ void TheoryFp::convertAndEquateTerm(TNode node)
   }
   else if (node.getType().isBitVector())
   {
-    if (converted != node) {
-      Assert(converted.getType().isBitVector());
+    if (wordBlasted != node)
+    {
+      Assert(wordBlasted.getType().isBitVector());
 
       handleLemma(
-          NodeManager::currentNM()->mkNode(kind::EQUAL, node, converted),
+          NodeManager::currentNM()->mkNode(kind::EQUAL, node, wordBlasted),
           InferenceId::FP_EQUATE_TERM);
     }
   }
@@ -657,7 +661,7 @@ void TheoryFp::registerTerm(TNode node)
      * registration. */
     if (!options().fp.fpLazyWb)
     {
-      convertAndEquateTerm(node);
+      wordBlastAndEquateTerm(node);
     }
   }
   return;
@@ -760,7 +764,7 @@ bool TheoryFp::preNotifyFact(
       && d_wbFactsCache.find(atom) == d_wbFactsCache.end())
   {
     d_wbFactsCache.insert(atom);
-    convertAndEquateTerm(atom);
+    wordBlastAndEquateTerm(atom);
   }
 
   if (atom.getKind() == kind::EQUAL)
@@ -793,7 +797,7 @@ void TheoryFp::notifySharedTerm(TNode n)
   if (options().fp.fpLazyWb && d_wbFactsCache.find(n) == d_wbFactsCache.end())
   {
     d_wbFactsCache.insert(n);
-    convertAndEquateTerm(n);
+    wordBlastAndEquateTerm(n);
   }
 }
 
@@ -818,7 +822,7 @@ TrustNode TheoryFp::explain(TNode n)
 }
 
 Node TheoryFp::getModelValue(TNode var) {
-  return d_conv->getValue(d_valuation, var);
+  return d_wordBlaster->getValue(d_valuation, var);
 }
 
 bool TheoryFp::collectModelInfo(TheoryModel* m,
@@ -880,10 +884,10 @@ bool TheoryFp::collectModelValues(TheoryModel* m,
         << "TheoryFp::collectModelInfo(): relevantVariable " << node
         << std::endl;
 
-    Node converted = d_conv->getValue(d_valuation, node);
-    // We only assign the value if the FpConverter actually has one, that is,
-    // if FpConverter::getValue() does not return a null node.
-    if (!converted.isNull() && !m->assertEquality(node, converted, true))
+    Node wordBlasted = d_wordBlaster->getValue(d_valuation, node);
+    // We only assign the value if the FpWordBlaster actually has one, that is,
+    // if FpWordBlaster::getValue() does not return a null node.
+    if (!wordBlasted.isNull() && !m->assertEquality(node, wordBlasted, true))
     {
       return false;
     }
diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h
index 663be2f81..9dd532a5d 100644
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -33,7 +33,7 @@ namespace cvc5 {
 namespace theory {
 namespace fp {
 
-class FpConverter;
+class FpWordBlaster;
 
 class TheoryFp : public Theory
 {
@@ -120,11 +120,11 @@ class TheoryFp : public Theory
   context::CDHashSet<Node> d_registeredTerms;
 
   /** The word-blaster. Translates FP -> BV. */
-  std::unique_ptr<FpConverter> d_conv;
+  std::unique_ptr<FpWordBlaster> d_wordBlaster;
 
   bool d_expansionRequested;
 
-  void convertAndEquateTerm(TNode node);
+  void wordBlastAndEquateTerm(TNode node);
 
   /** Interaction with the rest of the solver **/
   void handleLemma(Node node, InferenceId id);
diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp
index 8bc7900de..91fe183ec 100644
--- a/src/theory/fp/theory_fp_rewriter.cpp
+++ b/src/theory/fp/theory_fp_rewriter.cpp
@@ -38,7 +38,7 @@
 
 #include "base/check.h"
 #include "theory/bv/theory_bv_utils.h"
-#include "theory/fp/fp_converter.h"
+#include "theory/fp/fp_word_blaster.h"
 #include "util/floatingpoint.h"
 
 namespace cvc5 {