Floating point theory solver based on SymFPU (#1895)

* Add some symfpu accessor functions to reduce the size of the literal 'back-end'.

* Enable the bit-vector theory when setting the logic, not in expandDefinition.

This is needed because it is possible to add variables of float or rounding mode
sort but not use any theory specific functions or predicates and thus not enable
the bit-vector theory.

* Use symfpu to implement the literal floating-point objects.

* Add kinds for bit-blasted components.

* Print the new kinds.

* Typing rules for the new kinds.

* Constant folding for the component kinds.

* Add support for components to the theory solver.

* Add explicit equivalences between classification functions and equalities.

* Use symfpu to do symbolic conversions of floating-point operations.

* Implement conversions via (over-)approximation and refinement.

* Correct a copy and paste error in the generation of uninterpretted functions for conversions.

2 files changed, 822 insertions, 22 deletions

diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp
index fe90279ec..74e6189ed 100644
--- a/src/util/floatingpoint.cpp
+++ b/src/util/floatingpoint.cpp
@@ -15,8 +15,55 @@
  **/
 
 #include "util/floatingpoint.h"
-
 #include "base/cvc4_assert.h"
+#include "util/integer.h"
+
+#include <math.h>
+
+#ifdef CVC4_USE_SYMFPU
+#include "symfpu/core/add.h"
+#include "symfpu/core/classify.h"
+#include "symfpu/core/compare.h"
+#include "symfpu/core/convert.h"
+#include "symfpu/core/divide.h"
+#include "symfpu/core/fma.h"
+#include "symfpu/core/ite.h"
+#include "symfpu/core/multiply.h"
+#include "symfpu/core/packing.h"
+#include "symfpu/core/remainder.h"
+#include "symfpu/core/sign.h"
+#include "symfpu/core/sqrt.h"
+#include "symfpu/utils/numberOfRoundingModes.h"
+#include "symfpu/utils/properties.h"
+#endif
+
+#ifdef CVC4_USE_SYMFPU
+namespace symfpu {
+
+#define CVC4_LIT_ITE_DFN(T)                                        \
+  template <>                                                      \
+  struct ite<::CVC4::symfpuLiteral::prop, T>                       \
+  {                                                                \
+    static const T &iteOp(const ::CVC4::symfpuLiteral::prop &cond, \
+                          const T &l,                              \
+                          const T &r)                              \
+    {                                                              \
+      return cond ? l : r;                                         \
+    }                                                              \
+  }
+
+CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::rm);
+CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::prop);
+CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::sbv);
+CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::ubv);
+
+#undef CVC4_LIT_ITE_DFN
+}
+#endif
+
+#ifndef CVC4_USE_SYMFPU
+#define PRECONDITION(X) Assert((X))
+#endif
 
 namespace CVC4 {
 
@@ -32,22 +79,428 @@ FloatingPointSize::FloatingPointSize (const FloatingPointSize &old) : e(old.e),
   PrettyCheckArgument(validSignificandSize(s),s,"Invalid significand size : %d",s);
 }
 
-void FloatingPointLiteral::unfinished (void) const {
-  Unimplemented("Floating-point literals not yet implemented.");
+namespace symfpuLiteral {
+
+// To simplify the property macros
+typedef traits t;
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::one(const bwt &w)
+{
+  return wrappedBitVector<isSigned>(w, 1);
 }
 
-  FloatingPoint::FloatingPoint (unsigned e, unsigned s, const BitVector &bv) :
-    fpl(e,s,0.0),
-    t(e,s) {}
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::zero(const bwt &w)
+{
+  return wrappedBitVector<isSigned>(w, 0);
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::allOnes(const bwt &w)
+{
+  return ~wrappedBitVector<isSigned>::zero(w);
+}
 
+template <bool isSigned>
+prop wrappedBitVector<isSigned>::isAllOnes() const
+{
+  return (*this == wrappedBitVector<isSigned>::allOnes(this->getWidth()));
+}
+template <bool isSigned>
+prop wrappedBitVector<isSigned>::isAllZeros() const
+{
+  return (*this == wrappedBitVector<isSigned>::zero(this->getWidth()));
+}
 
-  static FloatingPointLiteral constructorHelperBitVector (const FloatingPointSize &ct, const RoundingMode &rm, const BitVector &bv, bool signedBV) {
-    if (signedBV) {
-      return FloatingPointLiteral(2,2,0.0);
-    } else {
-      return FloatingPointLiteral(2,2,0.0);
-    }
-    Unreachable("Constructor helper broken");
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::maxValue(const bwt &w)
+{
+  if (isSigned)
+  {
+    BitVector base(w - 1, 0U);
+    return wrappedBitVector<true>((~base).zeroExtend(1));
+  }
+  else
+  {
+    return wrappedBitVector<false>::allOnes(w);
+  }
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::minValue(const bwt &w)
+{
+  if (isSigned)
+  {
+    BitVector base(w, 1U);
+    BitVector shiftAmount(w, w - 1);
+    BitVector result(base.leftShift(shiftAmount));
+    return wrappedBitVector<true>(result);
+  }
+  else
+  {
+    return wrappedBitVector<false>::zero(w);
+  }
+}
+
+/*** Operators ***/
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator<<(
+    const wrappedBitVector<isSigned> &op) const
+{
+  return this->BitVector::leftShift(op);
+}
+
+template <>
+wrappedBitVector<true> wrappedBitVector<true>::operator>>(
+    const wrappedBitVector<true> &op) const
+{
+  return this->BitVector::arithRightShift(op);
+}
+
+template <>
+wrappedBitVector<false> wrappedBitVector<false>::operator>>(
+    const wrappedBitVector<false> &op) const
+{
+  return this->BitVector::logicalRightShift(op);
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator|(
+    const wrappedBitVector<isSigned> &op) const
+{
+  return this->BitVector::operator|(op);
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator&(
+    const wrappedBitVector<isSigned> &op) const
+{
+  return this->BitVector::operator&(op);
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator+(
+    const wrappedBitVector<isSigned> &op) const
+{
+  return this->BitVector::operator+(op);
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator-(
+    const wrappedBitVector<isSigned> &op) const
+{
+  return this->BitVector::operator-(op);
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator*(
+    const wrappedBitVector<isSigned> &op) const
+{
+  return this->BitVector::operator*(op);
+}
+
+template <>
+wrappedBitVector<false> wrappedBitVector<false>::operator/(
+    const wrappedBitVector<false> &op) const
+{
+  return this->BitVector::unsignedDivTotal(op);
+}
+
+template <>
+wrappedBitVector<false> wrappedBitVector<false>::operator%(
+    const wrappedBitVector<false> &op) const
+{
+  return this->BitVector::unsignedRemTotal(op);
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator-(void) const
+{
+  return this->BitVector::operator-();
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator~(void)const
+{
+  return this->BitVector::operator~();
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::increment() const
+{
+  return *this + wrappedBitVector<isSigned>::one(this->getWidth());
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::decrement() const
+{
+  return *this - wrappedBitVector<isSigned>::one(this->getWidth());
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::signExtendRightShift(
+    const wrappedBitVector<isSigned> &op) const
+{
+  return this->BitVector::arithRightShift(BitVector(this->getWidth(), op));
+}
+
+/*** Modular opertaions ***/
+// No overflow checking so these are the same as other operations
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularLeftShift(
+    const wrappedBitVector<isSigned> &op) const
+{
+  return *this << op;
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularRightShift(
+    const wrappedBitVector<isSigned> &op) const
+{
+  return *this >> op;
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularIncrement() const
+{
+  return this->increment();
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularDecrement() const
+{
+  return this->decrement();
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularAdd(
+    const wrappedBitVector<isSigned> &op) const
+{
+  return *this + op;
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularNegate() const
+{
+  return -(*this);
+}
+
+/*** Comparisons ***/
+
+template <bool isSigned>
+prop wrappedBitVector<isSigned>::operator==(
+    const wrappedBitVector<isSigned> &op) const
+{
+  return this->BitVector::operator==(op);
+}
+
+template <>
+prop wrappedBitVector<true>::operator<=(const wrappedBitVector<true> &op) const
+{
+  return this->signedLessThanEq(op);
+}
+
+template <>
+prop wrappedBitVector<true>::operator>=(const wrappedBitVector<true> &op) const
+{
+  return !(this->signedLessThan(op));
+}
+
+template <>
+prop wrappedBitVector<true>::operator<(const wrappedBitVector<true> &op) const
+{
+  return this->signedLessThan(op);
+}
+
+template <>
+prop wrappedBitVector<true>::operator>(const wrappedBitVector<true> &op) const
+{
+  return !(this->signedLessThanEq(op));
+}
+
+template <>
+prop wrappedBitVector<false>::operator<=(
+    const wrappedBitVector<false> &op) const
+{
+  return this->unsignedLessThanEq(op);
+}
+
+template <>
+prop wrappedBitVector<false>::operator>=(
+    const wrappedBitVector<false> &op) const
+{
+  return !(this->unsignedLessThan(op));
+}
+
+template <>
+prop wrappedBitVector<false>::operator<(const wrappedBitVector<false> &op) const
+{
+  return this->unsignedLessThan(op);
+}
+
+template <>
+prop wrappedBitVector<false>::operator>(const wrappedBitVector<false> &op) const
+{
+  return !(this->unsignedLessThanEq(op));
+}
+
+/*** Type conversion ***/
+// CVC4 nodes make no distinction between signed and unsigned, thus ...
+template <bool isSigned>
+wrappedBitVector<true> wrappedBitVector<isSigned>::toSigned(void) const
+{
+  return wrappedBitVector<true>(*this);
+}
+
+template <bool isSigned>
+wrappedBitVector<false> wrappedBitVector<isSigned>::toUnsigned(void) const
+{
+  return wrappedBitVector<false>(*this);
+}
+
+/*** Bit hacks ***/
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::extend(
+    bwt extension) const
+{
+  if (isSigned)
+  {
+    return this->BitVector::signExtend(extension);
+  }
+  else
+  {
+    return this->BitVector::zeroExtend(extension);
+  }
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::contract(
+    bwt reduction) const
+{
+  PRECONDITION(this->getWidth() > reduction);
+
+  return this->extract((this->getWidth() - 1) - reduction, 0);
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::resize(bwt newSize) const
+{
+  bwt width = this->getWidth();
+
+  if (newSize > width)
+  {
+    return this->extend(newSize - width);
+  }
+  else if (newSize < width)
+  {
+    return this->contract(width - newSize);
+  }
+  else
+  {
+    return *this;
+  }
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::matchWidth(
+    const wrappedBitVector<isSigned> &op) const
+{
+  PRECONDITION(this->getWidth() <= op.getWidth());
+  return this->extend(op.getWidth() - this->getWidth());
+}
+
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::append(
+    const wrappedBitVector<isSigned> &op) const
+{
+  return this->BitVector::concat(op);
+}
+
+// Inclusive of end points, thus if the same, extracts just one bit
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::extract(bwt upper,
+                                                               bwt lower) const
+{
+  PRECONDITION(upper >= lower);
+  return this->BitVector::extract(upper, lower);
+}
+
+// Explicit instantiation
+template class wrappedBitVector<true>;
+template class wrappedBitVector<false>;
+
+rm traits::RNE(void) { return ::CVC4::roundNearestTiesToEven; };
+rm traits::RNA(void) { return ::CVC4::roundNearestTiesToAway; };
+rm traits::RTP(void) { return ::CVC4::roundTowardPositive; };
+rm traits::RTN(void) { return ::CVC4::roundTowardNegative; };
+rm traits::RTZ(void) { return ::CVC4::roundTowardZero; };
+// This is a literal back-end so props are actually bools
+// so these can be handled in the same way as the internal assertions above
+
+void traits::precondition(const prop &p)
+{
+  Assert(p);
+  return;
+}
+void traits::postcondition(const prop &p)
+{
+  Assert(p);
+  return;
+}
+void traits::invariant(const prop &p)
+{
+  Assert(p);
+  return;
+}
+}
+
+#ifndef CVC4_USE_SYMFPU
+void FloatingPointLiteral::unfinished(void) const
+{
+  Unimplemented("Floating-point literals not yet implemented.");
+}
+#endif
+
+FloatingPoint::FloatingPoint(unsigned e, unsigned s, const BitVector &bv)
+    :
+#ifdef CVC4_USE_SYMFPU
+      fpl(symfpu::unpack<symfpuLiteral::traits>(symfpuLiteral::fpt(e, s), bv)),
+#else
+      fpl(e, s, 0.0),
+#endif
+      t(e, s)
+{
+}
+
+static FloatingPointLiteral constructorHelperBitVector(
+    const FloatingPointSize &ct,
+    const RoundingMode &rm,
+    const BitVector &bv,
+    bool signedBV)
+{
+#ifdef CVC4_USE_SYMFPU
+  if (signedBV)
+  {
+    return FloatingPointLiteral(
+        symfpu::convertSBVToFloat<symfpuLiteral::traits>(
+            symfpuLiteral::fpt(ct),
+            symfpuLiteral::rm(rm),
+            symfpuLiteral::sbv(bv)));
+  }
+  else
+  {
+    return FloatingPointLiteral(
+        symfpu::convertUBVToFloat<symfpuLiteral::traits>(
+            symfpuLiteral::fpt(ct),
+            symfpuLiteral::rm(rm),
+            symfpuLiteral::ubv(bv)));
+  }
+#else
+  return FloatingPointLiteral(2, 2, 0.0);
+#endif
+  Unreachable("Constructor helper broken");
   }
   
   FloatingPoint::FloatingPoint (const FloatingPointSize &ct, const RoundingMode &rm, const BitVector &bv, bool signedBV) :
@@ -60,9 +513,16 @@ void FloatingPointLiteral::unfinished (void) const {
     Rational two(2,1);
     
     if (r.isZero()) {
+#ifdef CVC4_USE_SYMFPU
+      return FloatingPointLiteral::makeZero(
+          ct, false);  // In keeping with the SMT-LIB standard
+#else
       return FloatingPointLiteral(2,2,0.0);
+#endif
     } else {
-      //int negative = (r.sgn() < 0) ? 1 : 0;
+#ifdef CVC4_USE_SYMFPU
+      int negative = (r.sgn() < 0) ? 1 : 0;
+#endif
       r = r.abs();
 
       // Compute the exponent
@@ -114,7 +574,7 @@ void FloatingPointLiteral::unfinished (void) const {
       
       
       // Compute the significand.
-      unsigned sigBits = ct.significand() + 2; // guard and sticky bits
+      unsigned sigBits = ct.significandWidth() + 2;  // guard and sticky bits
       BitVector sig(sigBits, 0U);
       BitVector one(sigBits, 1U);
       Rational workingSig(0,1);
@@ -144,7 +604,20 @@ void FloatingPointLiteral::unfinished (void) const {
       // A small subtlety... if the format has expBits the unpacked format
       // may have more to allow subnormals to be normalised.
       // Thus...
+#ifdef CVC4_USE_SYMFPU
+      unsigned extension =
+          FloatingPointLiteral::exponentWidth(exactFormat) - expBits;
+
+      FloatingPointLiteral exactFloat(
+          negative, exactExp.signExtend(extension), sig);
+
+      // Then cast...
+      FloatingPointLiteral rounded(
+          symfpu::convertFloatToFloat(exactFormat, ct, rm, exactFloat));
+      return rounded;
+#else
       Unreachable("no concrete implementation of FloatingPointLiteral");
+#endif
     }
     Unreachable("Constructor helper broken");
   }
@@ -155,74 +628,146 @@ void FloatingPointLiteral::unfinished (void) const {
 
   
   FloatingPoint FloatingPoint::makeNaN (const FloatingPointSize &t) {
+#ifdef CVC4_USE_SYMFPU
+    return FloatingPoint(
+        t, symfpu::unpackedFloat<symfpuLiteral::traits>::makeNaN(t));
+#else
     return FloatingPoint(2, 2, BitVector(4U,0U));
+#endif
   }
 
   FloatingPoint FloatingPoint::makeInf (const FloatingPointSize &t, bool sign) {
+#ifdef CVC4_USE_SYMFPU
+    return FloatingPoint(
+        t, symfpu::unpackedFloat<symfpuLiteral::traits>::makeInf(t, sign));
+#else
     return FloatingPoint(2, 2, BitVector(4U,0U));
+#endif
   }
 
   FloatingPoint FloatingPoint::makeZero (const FloatingPointSize &t, bool sign) {
+#ifdef CVC4_USE_SYMFPU
+    return FloatingPoint(
+        t, symfpu::unpackedFloat<symfpuLiteral::traits>::makeZero(t, sign));
+#else
     return FloatingPoint(2, 2, BitVector(4U,0U));
+#endif
   }
 
 
   /* Operations implemented using symfpu */
   FloatingPoint FloatingPoint::absolute (void) const {
+#ifdef CVC4_USE_SYMFPU
+    return FloatingPoint(t, symfpu::absolute<symfpuLiteral::traits>(t, fpl));
+#else
     return *this;
+#endif
   }
   
   FloatingPoint FloatingPoint::negate (void) const {
+#ifdef CVC4_USE_SYMFPU
+    return FloatingPoint(t, symfpu::negate<symfpuLiteral::traits>(t, fpl));
+#else
     return *this;
+#endif
   }
   
   FloatingPoint FloatingPoint::plus (const RoundingMode &rm, const FloatingPoint &arg) const {
+#ifdef CVC4_USE_SYMFPU
     Assert(this->t == arg.t);
+    return FloatingPoint(
+        t, symfpu::add<symfpuLiteral::traits>(t, rm, fpl, arg.fpl, true));
+#else
     return *this;
+#endif
   }
 
   FloatingPoint FloatingPoint::sub (const RoundingMode &rm, const FloatingPoint &arg) const {
+#ifdef CVC4_USE_SYMFPU
     Assert(this->t == arg.t);
+    return FloatingPoint(
+        t, symfpu::add<symfpuLiteral::traits>(t, rm, fpl, arg.fpl, false));
+#else
     return *this;
+#endif
   }
 
   FloatingPoint FloatingPoint::mult (const RoundingMode &rm, const FloatingPoint &arg) const {
+#ifdef CVC4_USE_SYMFPU
     Assert(this->t == arg.t);
+    return FloatingPoint(
+        t, symfpu::multiply<symfpuLiteral::traits>(t, rm, fpl, arg.fpl));
+#else
     return *this;
+#endif
   }
 
   FloatingPoint FloatingPoint::fma (const RoundingMode &rm, const FloatingPoint &arg1, const FloatingPoint &arg2) const {
+#ifdef CVC4_USE_SYMFPU
     Assert(this->t == arg1.t);
     Assert(this->t == arg2.t);
+    return FloatingPoint(
+        t, symfpu::fma<symfpuLiteral::traits>(t, rm, fpl, arg1.fpl, arg2.fpl));
+#else
     return *this;
+#endif
   }
 
   FloatingPoint FloatingPoint::div (const RoundingMode &rm, const FloatingPoint &arg) const {
+#ifdef CVC4_USE_SYMFPU
     Assert(this->t == arg.t);
+    return FloatingPoint(
+        t, symfpu::divide<symfpuLiteral::traits>(t, rm, fpl, arg.fpl));
+#else
     return *this;
+#endif
   }
 
   FloatingPoint FloatingPoint::sqrt (const RoundingMode &rm) const {
+#ifdef CVC4_USE_SYMFPU
+    return FloatingPoint(t, symfpu::sqrt<symfpuLiteral::traits>(t, rm, fpl));
+#else
     return *this;
+#endif
   }
 
   FloatingPoint FloatingPoint::rti (const RoundingMode &rm) const {
+#ifdef CVC4_USE_SYMFPU
+    return FloatingPoint(
+        t, symfpu::roundToIntegral<symfpuLiteral::traits>(t, rm, fpl));
+#else
     return *this;
+#endif
   }
 
   FloatingPoint FloatingPoint::rem (const FloatingPoint &arg) const {
+#ifdef CVC4_USE_SYMFPU
     Assert(this->t == arg.t);
+    return FloatingPoint(
+        t, symfpu::remainder<symfpuLiteral::traits>(t, fpl, arg.fpl));
+#else
     return *this;
+#endif
   }
 
   FloatingPoint FloatingPoint::maxTotal (const FloatingPoint &arg, bool zeroCaseLeft) const {
+#ifdef CVC4_USE_SYMFPU
     Assert(this->t == arg.t);
+    return FloatingPoint(
+        t, symfpu::max<symfpuLiteral::traits>(t, fpl, arg.fpl, zeroCaseLeft));
+#else
     return *this;
+#endif
   }
   
   FloatingPoint FloatingPoint::minTotal (const FloatingPoint &arg, bool zeroCaseLeft) const {
+#ifdef CVC4_USE_SYMFPU
     Assert(this->t == arg.t);
+    return FloatingPoint(
+        t, symfpu::min<symfpuLiteral::traits>(t, fpl, arg.fpl, zeroCaseLeft));
+#else
     return *this;
+#endif
   }
 
   FloatingPoint::PartialFloatingPoint FloatingPoint::max (const FloatingPoint &arg) const {
@@ -236,56 +781,109 @@ void FloatingPointLiteral::unfinished (void) const {
   }
 
   bool FloatingPoint::operator ==(const FloatingPoint& fp) const {
+#ifdef CVC4_USE_SYMFPU
+    return ((t == fp.t)
+            && symfpu::smtlibEqual<symfpuLiteral::traits>(t, fpl, fp.fpl));
+#else
     return ( (t == fp.t) );
+#endif
   }
 
   bool FloatingPoint::operator <= (const FloatingPoint &arg) const {
+#ifdef CVC4_USE_SYMFPU
     Assert(this->t == arg.t);
+    return symfpu::lessThanOrEqual<symfpuLiteral::traits>(t, fpl, arg.fpl);
+#else
     return false;
+#endif
   }
 
   bool FloatingPoint::operator < (const FloatingPoint &arg) const {
+#ifdef CVC4_USE_SYMFPU
     Assert(this->t == arg.t);
+    return symfpu::lessThan<symfpuLiteral::traits>(t, fpl, arg.fpl);
+#else
     return false;
+#endif
   }
 
   bool FloatingPoint::isNormal (void) const {
+#ifdef CVC4_USE_SYMFPU
+    return symfpu::isNormal<symfpuLiteral::traits>(t, fpl);
+#else
     return false;
+#endif
   }
 
   bool FloatingPoint::isSubnormal (void) const {
+#ifdef CVC4_USE_SYMFPU
+    return symfpu::isSubnormal<symfpuLiteral::traits>(t, fpl);
+#else
     return false;
+#endif
   }
 
   bool FloatingPoint::isZero (void) const {
+#ifdef CVC4_USE_SYMFPU
+    return symfpu::isZero<symfpuLiteral::traits>(t, fpl);
+#else
     return false;
+#endif
   }
 
   bool FloatingPoint::isInfinite (void) const {
+#ifdef CVC4_USE_SYMFPU
+    return symfpu::isInfinite<symfpuLiteral::traits>(t, fpl);
+#else
     return false;
+#endif
   }
 
   bool FloatingPoint::isNaN (void) const {
+#ifdef CVC4_USE_SYMFPU
+    return symfpu::isNaN<symfpuLiteral::traits>(t, fpl);
+#else
     return false;
+#endif
   }
 
   bool FloatingPoint::isNegative (void) const {
+#ifdef CVC4_USE_SYMFPU
+    return symfpu::isNegative<symfpuLiteral::traits>(t, fpl);
+#else
     return false;
+#endif
   }
 
   bool FloatingPoint::isPositive (void) const {
+#ifdef CVC4_USE_SYMFPU
+    return symfpu::isPositive<symfpuLiteral::traits>(t, fpl);
+#else
     return false;
+#endif
   }
 
   FloatingPoint FloatingPoint::convert (const FloatingPointSize &target, const RoundingMode &rm) const {
+#ifdef CVC4_USE_SYMFPU
+    return FloatingPoint(
+        target,
+        symfpu::convertFloatToFloat<symfpuLiteral::traits>(t, target, rm, fpl));
+#else
     return *this;
+#endif
   }
   
   BitVector FloatingPoint::convertToBVTotal (BitVectorSize width, const RoundingMode &rm, bool signedBV, BitVector undefinedCase) const {
+#ifdef CVC4_USE_SYMFPU
     if (signedBV)
-      return undefinedCase;
+      return symfpu::convertFloatToSBV<symfpuLiteral::traits>(
+          t, rm, fpl, width, undefinedCase);
     else
-      return undefinedCase;
+      return symfpu::convertFloatToUBV<symfpuLiteral::traits>(
+          t, rm, fpl, width, undefinedCase);
+#else
+    return undefinedCase;
+#endif
   }
 
   Rational FloatingPoint::convertToRationalTotal (Rational undefinedCase) const {
@@ -309,10 +907,18 @@ void FloatingPointLiteral::unfinished (void) const {
       return PartialRational(Rational(0U, 1U), true);
       
     } else {
-
+#ifdef CVC4_USE_SYMFPU
+      Integer sign((this->fpl.getSign()) ? -1 : 1);
+      Integer exp(
+          this->fpl.getExponent().toSignedInteger()
+          - (Integer(t.significand()
+                     - 1)));  // -1 as forcibly normalised into the [1,2) range
+      Integer significand(this->fpl.getSignificand().toInteger());
+#else
       Integer sign(0);
       Integer exp(0);
       Integer significand(0);
+#endif
       Integer signedSignificand(sign * significand);
       
       // Only have pow(uint32_t) so we should check this.
@@ -333,7 +939,11 @@ void FloatingPointLiteral::unfinished (void) const {
   }
 
   BitVector FloatingPoint::pack (void) const {
+#ifdef CVC4_USE_SYMFPU
+    BitVector bv(symfpu::pack<symfpuLiteral::traits>(this->t, this->fpl));
+#else
     BitVector bv(4u,0u);
+#endif
     return bv;
   }
 
diff --git a/src/util/floatingpoint.h b/src/util/floatingpoint.h
index fa4573123..95bec903e 100644
--- a/src/util/floatingpoint.h
+++ b/src/util/floatingpoint.h
@@ -20,11 +20,15 @@
 #ifndef __CVC4__FLOATINGPOINT_H
 #define __CVC4__FLOATINGPOINT_H
 
-#include <fenv.h>
-
 #include "util/bitvector.h"
 #include "util/rational.h"
 
+#include <fenv.h>
+
+#ifdef CVC4_USE_SYMFPU
+#include "symfpu/core/unpackedFloat.h"
+#endif
+
 namespace CVC4 {
   // Inline these!
   inline bool CVC4_PUBLIC validExponentSize (unsigned e) { return e >= 2; }
@@ -62,6 +66,22 @@ namespace CVC4 {
       return (e == fps.e) && (s == fps.s);
     }
 
+    // Implement the interface that symfpu uses for floating-point formats.
+    inline unsigned exponentWidth(void) const { return this->exponent(); }
+    inline unsigned significandWidth(void) const { return this->significand(); }
+    inline unsigned packedWidth(void) const
+    {
+      return this->exponentWidth() + this->significandWidth();
+    }
+    inline unsigned packedExponentWidth(void) const
+    {
+      return this->exponentWidth();
+    }
+    inline unsigned packedSignificandWidth(void) const
+    {
+      return this->significandWidth() - 1;
+    }
+
   }; /* class FloatingPointSize */
 
   struct CVC4_PUBLIC FloatingPointSizeHashFunction {
@@ -95,11 +115,181 @@ namespace CVC4 {
     }
   }; /* struct RoundingModeHashFunction */
 
+  /**
+   * This is a symfpu literal "back-end".  It allows the library to be used as
+   * an arbitrary precision floating-point implementation.  This is effectively
+   * the glue between symfpu's notion of "signed bit-vector" and CVC4's
+   * BitVector.
+   */
+  namespace symfpuLiteral {
+  // Forward declaration of wrapper so that traits can be defined early and so
+  // used in the implementation of wrappedBitVector.
+  template <bool T>
+  class wrappedBitVector;
+
+  // This is the template parameter for symfpu's templates.
+  class traits
+  {
+   public:
+    // The six key types that symfpu uses.
+    typedef unsigned bwt;
+    typedef bool prop;
+    typedef ::CVC4::RoundingMode rm;
+    typedef ::CVC4::FloatingPointSize fpt;
+    typedef wrappedBitVector<true> sbv;
+    typedef wrappedBitVector<false> ubv;
+
+    // Give concrete instances of each rounding mode, mainly for comparisons.
+    static rm RNE(void);
+    static rm RNA(void);
+    static rm RTP(void);
+    static rm RTN(void);
+    static rm RTZ(void);
+
+    // The sympfu properties.
+    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.
+  typedef traits::bwt bwt;
+  typedef traits::prop prop;
+  typedef traits::rm rm;
+  typedef traits::fpt fpt;
+  typedef traits::ubv ubv;
+  typedef traits::sbv sbv;
+
+  // Type function for mapping between types
+  template <bool T>
+  struct signedToLiteralType;
+
+  template <>
+  struct signedToLiteralType<true>
+  {
+    typedef int literalType;
+  };
+  template <>
+  struct signedToLiteralType<false>
+  {
+    typedef unsigned int literalType;
+  };
+
+  // This is an additional interface for CVC4::BitVector.
+  // The template parameter distinguishes signed and unsigned bit-vectors, a
+  // distinction symfpu uses.
+  template <bool isSigned>
+  class wrappedBitVector : public BitVector
+  {
+   protected:
+    typedef typename signedToLiteralType<isSigned>::literalType literalType;
+
+    friend wrappedBitVector<!isSigned>;  // To allow conversion between the
+                                         // types
+#ifdef CVC4_USE_SYMFPU
+    friend ::symfpu::ite<prop, wrappedBitVector<isSigned> >;  // For ITE
+#endif
+
+   public:
+    wrappedBitVector(const bwt w, const unsigned v) : BitVector(w, v) {}
+    wrappedBitVector(const prop &p) : BitVector(1, p ? 1U : 0U) {}
+    wrappedBitVector(const wrappedBitVector<isSigned> &old) : BitVector(old) {}
+    wrappedBitVector(const BitVector &old) : BitVector(old) {}
+    bwt getWidth(void) const { return getSize(); }
+    /*** Constant creation and test ***/
+
+    static wrappedBitVector<isSigned> one(const bwt &w);
+    static wrappedBitVector<isSigned> zero(const bwt &w);
+    static wrappedBitVector<isSigned> allOnes(const bwt &w);
+
+    prop isAllOnes() const;
+    prop isAllZeros() const;
+
+    static wrappedBitVector<isSigned> maxValue(const bwt &w);
+    static wrappedBitVector<isSigned> minValue(const bwt &w);
+
+    /*** Operators ***/
+    wrappedBitVector<isSigned> operator<<(
+        const wrappedBitVector<isSigned> &op) const;
+    wrappedBitVector<isSigned> operator>>(
+        const wrappedBitVector<isSigned> &op) const;
+
+    /* Inherited but ...
+     * *sigh* if we use the inherited version then it will return a
+     * CVC4::BitVector which can be converted back to a
+     * wrappedBitVector<isSigned> but isn't done automatically when working
+     * out types for templates instantiation.  ITE is a particular
+     * problem as expressions and constants no longer derive the
+     * same type.  There aren't any good solutions in C++, we could
+     * use CRTP but Liana wouldn't appreciate that, so the following
+     * pointless wrapping functions are needed.
+     */
+    wrappedBitVector<isSigned> operator|(
+        const wrappedBitVector<isSigned> &op) const;
+    wrappedBitVector<isSigned> operator&(
+        const wrappedBitVector<isSigned> &op) const;
+    wrappedBitVector<isSigned> operator+(
+        const wrappedBitVector<isSigned> &op) const;
+    wrappedBitVector<isSigned> operator-(
+        const wrappedBitVector<isSigned> &op) const;
+    wrappedBitVector<isSigned> operator*(
+        const wrappedBitVector<isSigned> &op) const;
+    wrappedBitVector<isSigned> operator/(
+        const wrappedBitVector<isSigned> &op) const;
+    wrappedBitVector<isSigned> operator%(
+        const wrappedBitVector<isSigned> &op) const;
+    wrappedBitVector<isSigned> operator-(void) const;
+    wrappedBitVector<isSigned> operator~(void)const;
+
+    wrappedBitVector<isSigned> increment() const;
+    wrappedBitVector<isSigned> decrement() const;
+    wrappedBitVector<isSigned> signExtendRightShift(
+        const wrappedBitVector<isSigned> &op) const;
+
+    /*** Modular opertaions ***/
+    // No overflow checking so these are the same as other operations
+    wrappedBitVector<isSigned> modularLeftShift(
+        const wrappedBitVector<isSigned> &op) const;
+    wrappedBitVector<isSigned> modularRightShift(
+        const wrappedBitVector<isSigned> &op) const;
+    wrappedBitVector<isSigned> modularIncrement() const;
+    wrappedBitVector<isSigned> modularDecrement() const;
+    wrappedBitVector<isSigned> modularAdd(
+        const wrappedBitVector<isSigned> &op) const;
+    wrappedBitVector<isSigned> modularNegate() const;
+
+    /*** Comparisons ***/
+    // Inherited ... ish ...
+    prop operator==(const wrappedBitVector<isSigned> &op) const;
+    prop operator<=(const wrappedBitVector<isSigned> &op) const;
+    prop operator>=(const wrappedBitVector<isSigned> &op) const;
+    prop operator<(const wrappedBitVector<isSigned> &op) const;
+    prop operator>(const wrappedBitVector<isSigned> &op) const;
+
+    /*** Type conversion ***/
+    wrappedBitVector<true> toSigned(void) const;
+    wrappedBitVector<false> toUnsigned(void) const;
+
+    /*** Bit hacks ***/
+    wrappedBitVector<isSigned> extend(bwt extension) const;
+    wrappedBitVector<isSigned> contract(bwt reduction) const;
+    wrappedBitVector<isSigned> resize(bwt newSize) const;
+    wrappedBitVector<isSigned> matchWidth(
+        const wrappedBitVector<isSigned> &op) const;
+    wrappedBitVector<isSigned> append(
+        const wrappedBitVector<isSigned> &op) const;
+
+    // Inclusive of end points, thus if the same, extracts just one bit
+    wrappedBitVector<isSigned> extract(bwt upper, bwt lower) const;
+  };
+  }
 
   /**
    * A concrete floating point number
    */
-
+#ifdef CVC4_USE_SYMFPU
+  typedef ::symfpu::unpackedFloat<symfpuLiteral::traits> FloatingPointLiteral;
+#else
   class CVC4_PUBLIC FloatingPointLiteral {
   public :
     // This intentional left unfinished as the choice of literal
@@ -109,7 +299,6 @@ namespace CVC4 {
     FloatingPointLiteral(unsigned, unsigned, double) { unfinished(); }
     FloatingPointLiteral(unsigned, unsigned, const std::string &) { unfinished(); }
     FloatingPointLiteral(const FloatingPointLiteral &) { unfinished(); }
-
     bool operator == (const FloatingPointLiteral &op) const {
       unfinished();
       return false;
@@ -120,6 +309,7 @@ namespace CVC4 {
       return 23;
     }
   };
+#endif
 
   class CVC4_PUBLIC FloatingPoint {
   protected :