Floating point symfpu support (#1103)

- Update the parser to the new constant construction
- Fix the problem with parsing +/-zero and remove some dead code
- Extend the interface for literal floating-point values.
- Add a constructor so that a parameteric operator structure can be created from a type
- Add constructors so parametric operator constants can be easily converted
- Update SMT2 printing so that it uses the informative output

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 92f6b36d8188553a4508ed070067a76a5631f405..2aa85fbe374e72f0a91664e945ea7f990746451a 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -2271,17 +2271,25 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
         }
       }
     | FP_PINF_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
-      { expr = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb),
-                                      AntlrInput::tokenToUnsigned($sb),
-                                      +INFINITY)); }
+      { expr = MK_CONST(FloatingPoint::makeInf(FloatingPointSize(AntlrInput::tokenToUnsigned($eb),
+                                                                 AntlrInput::tokenToUnsigned($sb)),
+                                               false)); }
     | FP_NINF_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
-      { expr = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb),
-                                      AntlrInput::tokenToUnsigned($sb),
-                                     -INFINITY)); }
+      { expr = MK_CONST(FloatingPoint::makeInf(FloatingPointSize(AntlrInput::tokenToUnsigned($eb),
+                                                                 AntlrInput::tokenToUnsigned($sb)),
+                                               true)); }
     | FP_NAN_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
-      { expr = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb),
-                                      AntlrInput::tokenToUnsigned($sb),
-                                      NAN)); }
+      { expr = MK_CONST(FloatingPoint::makeNaN(FloatingPointSize(AntlrInput::tokenToUnsigned($eb),
+                                                                 AntlrInput::tokenToUnsigned($sb)))); }
+
+    | FP_PZERO_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
+      { expr = MK_CONST(FloatingPoint::makeZero(FloatingPointSize(AntlrInput::tokenToUnsigned($eb),
+                                                                AntlrInput::tokenToUnsigned($sb)),
+                                              false)); }
+    | FP_NZERO_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
+      { expr = MK_CONST(FloatingPoint::makeZero(FloatingPointSize(AntlrInput::tokenToUnsigned($eb),
+                                                                AntlrInput::tokenToUnsigned($sb)),
+                                              true)); }
     // NOTE: Theory parametric constants go here
 
     )
@@ -2505,26 +2513,6 @@ indexedFunctionName[CVC4::Expr& op, CVC4::Kind& kind]
               "bv2nat and int2bv are not part of SMT-LIB, and aren't available "
               "in SMT-LIB strict compliance mode");
         } }
-    | FP_PINF_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
-      { op = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb),
-                                    AntlrInput::tokenToUnsigned($sb),
-                                    +INFINITY)); }
-    | FP_NINF_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
-      { op = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb),
-                                    AntlrInput::tokenToUnsigned($sb),
-                                    -INFINITY)); }
-    | FP_NAN_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
-      { op = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb),
-                                    AntlrInput::tokenToUnsigned($sb),
-                                    NAN)); }
-    | FP_PZERO_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
-      { op = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb),
-                                    AntlrInput::tokenToUnsigned($sb),
-                                    +0.0)); }
-    | FP_NZERO_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
-      { op = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb),
-                                    AntlrInput::tokenToUnsigned($sb),
-                                    -0.0)); }
     | FP_TO_FP_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
       { op = MK_CONST(FloatingPointToFPGeneric(
                 AntlrInput::tokenToUnsigned($eb),

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 2f2a6ff18a0859b6d4cf85f208fbd5ce6e469882..ae65311de18331e07bc090c2a3a505129b27253e 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -202,7 +202,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
       break;
     }
     case kind::CONST_FLOATINGPOINT:
-      out << n.getConst<FloatingPoint>().getLiteral();
+      out << n.getConst<FloatingPoint>();
       break;
     case kind::CONST_ROUNDINGMODE:
       switch (n.getConst<RoundingMode>()) {

diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp
index 8c446d9d24fe2ae3a459a6032f661764ffacb6bd..fe90279ecfcf998f1f4d98e61d30542d9ef28777 100644 (file)
--- a/src/util/floatingpoint.cpp
+++ b/src/util/floatingpoint.cpp
@@ -36,4 +36,307 @@ void FloatingPointLiteral::unfinished (void) const {
   Unimplemented("Floating-point literals not yet implemented.");
 }
 
+  FloatingPoint::FloatingPoint (unsigned e, unsigned s, const BitVector &bv) :
+    fpl(e,s,0.0),
+    t(e,s) {}
+
+
+  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");
+  }
+  
+  FloatingPoint::FloatingPoint (const FloatingPointSize &ct, const RoundingMode &rm, const BitVector &bv, bool signedBV) :
+    fpl(constructorHelperBitVector(ct, rm, bv, signedBV)),
+    t(ct) {}
+
+  
+  static FloatingPointLiteral constructorHelperRational (const FloatingPointSize &ct, const RoundingMode &rm, const Rational &ri) {
+    Rational r(ri);
+    Rational two(2,1);
+    
+    if (r.isZero()) {
+      return FloatingPointLiteral(2,2,0.0);
+    } else {
+      //int negative = (r.sgn() < 0) ? 1 : 0;
+      r = r.abs();
+
+      // Compute the exponent
+      Integer exp(0U);
+      Integer inc(1U);
+      Rational working(1,1);
+
+      if (r == working) {
+
+      } else if ( r < working ) {
+       while (r < working) {
+         exp -= inc;
+         working /= two;
+       }
+      } else {
+       while (r >= working) {
+         exp += inc;
+         working *= two;
+       }
+       exp -= inc;
+       working /= two;
+      }
+
+      Assert(working <= r);
+      Assert(r < working * two);
+
+      // Work out the number of bits required to represent the exponent for a normal number
+      unsigned expBits = 2; // No point starting with an invalid amount
+
+      Integer doubleInt(2);
+      if (exp.strictlyPositive()) {
+       Integer representable(4);     // 1 more than exactly representable with expBits
+       while (representable <= exp) {// hence <=
+         representable *= doubleInt;
+         ++expBits;
+       }
+      } else if (exp.strictlyNegative()) {
+       Integer representable(-4);    // Exactly representable with expBits + sign
+                                     // but -2^n and -(2^n - 1) are both subnormal
+       while ((representable + doubleInt) > exp) {
+         representable *= doubleInt;
+         ++expBits;
+       }
+      }
+      ++expBits; // To allow for sign
+
+      BitVector exactExp(expBits, exp);
+
+      
+      
+      // Compute the significand.
+      unsigned sigBits = ct.significand() + 2; // guard and sticky bits
+      BitVector sig(sigBits, 0U);
+      BitVector one(sigBits, 1U);
+      Rational workingSig(0,1);
+      for (unsigned i = 0; i < sigBits - 1; ++i) {
+       Rational mid(workingSig + working);
+
+       if (mid <= r) {
+         sig = sig | one;
+         workingSig = mid;
+       }
+
+       sig = sig.leftShift(one);
+       working /= two;
+      }
+
+      // Compute the sticky bit
+      Rational remainder(r - workingSig);
+      Assert(Rational(0,1) <= remainder);
+
+      if (!remainder.isZero()) {
+       sig = sig | one;
+      }
+
+      // Build an exact float
+      FloatingPointSize exactFormat(expBits, sigBits);
+
+      // A small subtlety... if the format has expBits the unpacked format
+      // may have more to allow subnormals to be normalised.
+      // Thus...
+      Unreachable("no concrete implementation of FloatingPointLiteral");
+    }
+    Unreachable("Constructor helper broken");
+  }
+  
+  FloatingPoint::FloatingPoint (const FloatingPointSize &ct, const RoundingMode &rm, const Rational &r) :
+    fpl(constructorHelperRational(ct, rm, r)),
+    t(ct) {}
+
+  
+  FloatingPoint FloatingPoint::makeNaN (const FloatingPointSize &t) {
+    return FloatingPoint(2, 2, BitVector(4U,0U));
+  }
+
+  FloatingPoint FloatingPoint::makeInf (const FloatingPointSize &t, bool sign) {
+    return FloatingPoint(2, 2, BitVector(4U,0U));
+  }
+
+  FloatingPoint FloatingPoint::makeZero (const FloatingPointSize &t, bool sign) {
+    return FloatingPoint(2, 2, BitVector(4U,0U));
+  }
+
+
+  /* Operations implemented using symfpu */
+  FloatingPoint FloatingPoint::absolute (void) const {
+    return *this;
+  }
+  
+  FloatingPoint FloatingPoint::negate (void) const {
+    return *this;
+  }
+  
+  FloatingPoint FloatingPoint::plus (const RoundingMode &rm, const FloatingPoint &arg) const {
+    Assert(this->t == arg.t);
+    return *this;
+  }
+
+  FloatingPoint FloatingPoint::sub (const RoundingMode &rm, const FloatingPoint &arg) const {
+    Assert(this->t == arg.t);
+    return *this;
+  }
+
+  FloatingPoint FloatingPoint::mult (const RoundingMode &rm, const FloatingPoint &arg) const {
+    Assert(this->t == arg.t);
+    return *this;
+  }
+
+  FloatingPoint FloatingPoint::fma (const RoundingMode &rm, const FloatingPoint &arg1, const FloatingPoint &arg2) const {
+    Assert(this->t == arg1.t);
+    Assert(this->t == arg2.t);
+    return *this;
+  }
+
+  FloatingPoint FloatingPoint::div (const RoundingMode &rm, const FloatingPoint &arg) const {
+    Assert(this->t == arg.t);
+    return *this;
+  }
+
+  FloatingPoint FloatingPoint::sqrt (const RoundingMode &rm) const {
+    return *this;
+  }
+
+  FloatingPoint FloatingPoint::rti (const RoundingMode &rm) const {
+    return *this;
+  }
+
+  FloatingPoint FloatingPoint::rem (const FloatingPoint &arg) const {
+    Assert(this->t == arg.t);
+    return *this;
+  }
+
+  FloatingPoint FloatingPoint::maxTotal (const FloatingPoint &arg, bool zeroCaseLeft) const {
+    Assert(this->t == arg.t);
+    return *this;
+  }
+  
+  FloatingPoint FloatingPoint::minTotal (const FloatingPoint &arg, bool zeroCaseLeft) const {
+    Assert(this->t == arg.t);
+    return *this;
+  }
+
+  FloatingPoint::PartialFloatingPoint FloatingPoint::max (const FloatingPoint &arg) const {
+    FloatingPoint tmp(maxTotal(arg, true));
+    return PartialFloatingPoint(tmp, tmp == maxTotal(arg, false));
+  }
+
+  FloatingPoint::PartialFloatingPoint FloatingPoint::min (const FloatingPoint &arg) const {
+    FloatingPoint tmp(minTotal(arg, true));
+    return PartialFloatingPoint(tmp, tmp == minTotal(arg, false));
+  }
+
+  bool FloatingPoint::operator ==(const FloatingPoint& fp) const {
+    return ( (t == fp.t) );
+  }
+
+  bool FloatingPoint::operator <= (const FloatingPoint &arg) const {
+    Assert(this->t == arg.t);
+    return false;
+  }
+
+  bool FloatingPoint::operator < (const FloatingPoint &arg) const {
+    Assert(this->t == arg.t);
+    return false;
+  }
+
+  bool FloatingPoint::isNormal (void) const {
+    return false;
+  }
+
+  bool FloatingPoint::isSubnormal (void) const {
+    return false;
+  }
+
+  bool FloatingPoint::isZero (void) const {
+    return false;
+  }
+
+  bool FloatingPoint::isInfinite (void) const {
+    return false;
+  }
+
+  bool FloatingPoint::isNaN (void) const {
+    return false;
+  }
+
+  bool FloatingPoint::isNegative (void) const {
+    return false;
+  }
+
+  bool FloatingPoint::isPositive (void) const {
+    return false;
+  }
+
+  FloatingPoint FloatingPoint::convert (const FloatingPointSize &target, const RoundingMode &rm) const {
+    return *this;
+  }
+  
+  BitVector FloatingPoint::convertToBVTotal (BitVectorSize width, const RoundingMode &rm, bool signedBV, BitVector undefinedCase) const {
+    if (signedBV)
+      return undefinedCase;
+    else
+      return undefinedCase;
+  }
+
+  Rational FloatingPoint::convertToRationalTotal (Rational undefinedCase) const {
+    PartialRational p(convertToRational());
+
+    return p.second ? p.first : undefinedCase;
+  }
+
+  FloatingPoint::PartialBitVector FloatingPoint::convertToBV (BitVectorSize width, const RoundingMode &rm, bool signedBV) const {
+    BitVector tmp(convertToBVTotal (width, rm, signedBV, BitVector(width, 0U)));
+    BitVector confirm(convertToBVTotal (width, rm, signedBV, BitVector(width, 1U)));
+
+    return PartialBitVector(tmp, tmp == confirm);
+  }
+
+  FloatingPoint::PartialRational FloatingPoint::convertToRational (void) const {
+    if (this->isNaN() || this->isInfinite()) {
+      return PartialRational(Rational(0U, 1U), false);
+    }
+    if (this->isZero()) {
+      return PartialRational(Rational(0U, 1U), true);
+      
+    } else {
+
+      Integer sign(0);
+      Integer exp(0);
+      Integer significand(0);
+      Integer signedSignificand(sign * significand);
+      
+      // Only have pow(uint32_t) so we should check this.
+      Assert(this->t.significand() <= 32);
+      
+      if (!(exp.strictlyNegative())) {
+       Integer r(signedSignificand.multiplyByPow2(exp.toUnsignedInt()));
+       return PartialRational(Rational(r), true);
+      } else {
+       Integer one(1U);
+       Integer q(one.multiplyByPow2((-exp).toUnsignedInt()));
+       Rational r(signedSignificand, q);
+       return PartialRational(r, true);
+      }
+    }
+
+    Unreachable("Convert float literal to real broken.");
+  }
+
+  BitVector FloatingPoint::pack (void) const {
+    BitVector bv(4u,0u);
+    return bv;
+  }
+
+
+
 }/* CVC4 namespace */

diff --git a/src/util/floatingpoint.h b/src/util/floatingpoint.h
index b3be84f131629b9a3bdbd8faa7f73cc9aed2a72d..fa4573123bbf13663607524bf04eb5a24bc303a3 100644 (file)
--- a/src/util/floatingpoint.h
+++ b/src/util/floatingpoint.h
@@ -23,6 +23,7 @@
 #include <fenv.h>
 
 #include "util/bitvector.h"
+#include "util/rational.h"
 
 namespace CVC4 {
   // Inline these!
@@ -127,25 +128,83 @@ namespace CVC4 {
   public :
     FloatingPointSize t;
 
-    FloatingPoint (unsigned e, unsigned s, double d) : fpl(e,s,d), t(e,s) {}
-    FloatingPoint (unsigned e, unsigned s, const std::string &bitString) : fpl(e,s,bitString), t(e,s) {}
+    FloatingPoint (unsigned e, unsigned s, const BitVector &bv);
+    FloatingPoint (const FloatingPointSize &oldt, const FloatingPointLiteral &oldfpl) : fpl(oldfpl), t(oldt) {}
     FloatingPoint (const FloatingPoint &fp) : fpl(fp.fpl), t(fp.t) {}
+    FloatingPoint (const FloatingPointSize &ct, const RoundingMode &rm, const BitVector &bv, bool signedBV);
+    FloatingPoint (const FloatingPointSize &ct, const RoundingMode &rm, const Rational &r);
 
-    bool operator ==(const FloatingPoint& fp) const {
-      return ( (t == fp.t) && fpl == fp.fpl );
-    }
+
+    static FloatingPoint makeNaN (const FloatingPointSize &t);
+    static FloatingPoint makeInf (const FloatingPointSize &t, bool sign);
+    static FloatingPoint makeZero (const FloatingPointSize &t, bool sign);
 
     const FloatingPointLiteral & getLiteral (void) const {
       return this->fpl;
     }
 
+    // Gives the corresponding IEEE-754 transfer format
+    BitVector pack (void) const;
+
+
+    FloatingPoint absolute (void) const;
+    FloatingPoint negate (void) const;
+    FloatingPoint plus (const RoundingMode &rm, const FloatingPoint &arg) const;
+    FloatingPoint sub (const RoundingMode &rm, const FloatingPoint &arg) const;
+    FloatingPoint mult (const RoundingMode &rm, const FloatingPoint &arg) const;
+    FloatingPoint div (const RoundingMode &rm, const FloatingPoint &arg) const;
+    FloatingPoint fma (const RoundingMode &rm, const FloatingPoint &arg1, const FloatingPoint &arg2) const;
+    FloatingPoint sqrt (const RoundingMode &rm) const;
+    FloatingPoint rti (const RoundingMode &rm) const;
+    FloatingPoint rem (const FloatingPoint &arg) const;
+
+    // zeroCase is whether the left or right is returned in the case of min/max(-0,+0) or (+0,-0)
+    FloatingPoint maxTotal (const FloatingPoint &arg, bool zeroCaseLeft) const;
+    FloatingPoint minTotal (const FloatingPoint &arg, bool zeroCaseLeft) const;
+
+    // These detect when the answer is defined
+    typedef std::pair<FloatingPoint, bool> PartialFloatingPoint;
+
+    PartialFloatingPoint max (const FloatingPoint &arg) const;
+    PartialFloatingPoint min (const FloatingPoint &arg) const;
+
+
+    bool operator ==(const FloatingPoint& fp) const;
+    bool operator <= (const FloatingPoint &arg) const;
+    bool operator < (const FloatingPoint &arg) const;
+
+    bool isNormal (void) const;
+    bool isSubnormal (void) const;
+    bool isZero (void) const;
+    bool isInfinite (void) const;
+    bool isNaN (void) const;
+    bool isNegative (void) const;
+    bool isPositive (void) const;
+
+    FloatingPoint convert (const FloatingPointSize &target, const RoundingMode &rm) const;
+
+    // These require a value to return in the undefined case
+    BitVector convertToBVTotal (BitVectorSize width, const RoundingMode &rm,
+                               bool signedBV, BitVector undefinedCase) const;
+    Rational convertToRationalTotal (Rational undefinedCase) const;
+
+    // These detect when the answer is defined
+    typedef std::pair<BitVector, bool> PartialBitVector;
+    typedef std::pair<Rational, bool> PartialRational;
+
+    PartialBitVector convertToBV (BitVectorSize width, const RoundingMode &rm,
+                               bool signedBV) const;
+    PartialRational convertToRational (void) const;
+
   }; /* class FloatingPoint */
 
 
   struct CVC4_PUBLIC FloatingPointHashFunction {
-    inline size_t operator() (const FloatingPoint& fp) const {
-      FloatingPointSizeHashFunction h;
-      return h(fp.t) ^ fp.getLiteral().hash();
+    size_t operator() (const FloatingPoint& fp) const {
+      FloatingPointSizeHashFunction fpshf;
+      BitVectorHashFunction bvhf;
+
+      return fpshf(fp.t) ^ bvhf(fp.pack());
     }
   }; /* struct FloatingPointHashFunction */
 
@@ -158,6 +217,8 @@ namespace CVC4 {
 
     FloatingPointConvertSort (unsigned _e, unsigned _s)
       : t(_e,_s) {}
+    FloatingPointConvertSort (const FloatingPointSize &fps)
+      : t(fps) {}
 
     bool operator ==(const FloatingPointConvertSort& fpcs) const {
       return t == fpcs.t;
@@ -171,22 +232,39 @@ namespace CVC4 {
    */
 
   class CVC4_PUBLIC FloatingPointToFPIEEEBitVector : public FloatingPointConvertSort {
-  public : FloatingPointToFPIEEEBitVector (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {}
+  public :
+    FloatingPointToFPIEEEBitVector (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {}
+    FloatingPointToFPIEEEBitVector (const FloatingPointConvertSort &old) : FloatingPointConvertSort(old) {}
   };
+
   class CVC4_PUBLIC FloatingPointToFPFloatingPoint : public FloatingPointConvertSort {
-  public : FloatingPointToFPFloatingPoint (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {}
+  public :
+    FloatingPointToFPFloatingPoint (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {}
+    FloatingPointToFPFloatingPoint (const FloatingPointConvertSort &old) : FloatingPointConvertSort(old) {}
   };
+
   class CVC4_PUBLIC FloatingPointToFPReal : public FloatingPointConvertSort {
-  public : FloatingPointToFPReal (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {}
+  public :
+    FloatingPointToFPReal (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {}
+    FloatingPointToFPReal (const FloatingPointConvertSort &old) : FloatingPointConvertSort(old) {}
   };
+
   class CVC4_PUBLIC FloatingPointToFPSignedBitVector : public FloatingPointConvertSort {
-  public : FloatingPointToFPSignedBitVector (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {}
+  public :
+    FloatingPointToFPSignedBitVector (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {}
+    FloatingPointToFPSignedBitVector (const FloatingPointConvertSort &old) : FloatingPointConvertSort(old) {}
   };
+
   class CVC4_PUBLIC FloatingPointToFPUnsignedBitVector : public FloatingPointConvertSort {
-  public : FloatingPointToFPUnsignedBitVector (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {}
+  public :
+    FloatingPointToFPUnsignedBitVector (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {}
+    FloatingPointToFPUnsignedBitVector (const FloatingPointConvertSort &old) : FloatingPointConvertSort(old) {}
   };
+
   class CVC4_PUBLIC FloatingPointToFPGeneric : public FloatingPointConvertSort {
-  public : FloatingPointToFPGeneric (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {}
+  public :
+    FloatingPointToFPGeneric (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {}
+    FloatingPointToFPGeneric (const FloatingPointConvertSort &old) : FloatingPointConvertSort(old) {}
   };
 
 
@@ -215,14 +293,26 @@ namespace CVC4 {
 
     FloatingPointToBV (unsigned s)
       : bvs(s) {}
+    FloatingPointToBV (const FloatingPointToBV &old) : bvs(old.bvs) {}
+    FloatingPointToBV (const BitVectorSize &old) : bvs(old) {}
     operator unsigned () const { return bvs; }
   };
 
   class CVC4_PUBLIC FloatingPointToUBV : public FloatingPointToBV {
   public : FloatingPointToUBV (unsigned _s) : FloatingPointToBV(_s) {}
+    FloatingPointToUBV (const FloatingPointToBV &old) : FloatingPointToBV(old) {}
   };
   class CVC4_PUBLIC FloatingPointToSBV : public FloatingPointToBV {
   public : FloatingPointToSBV (unsigned _s) : FloatingPointToBV(_s) {}
+    FloatingPointToSBV (const FloatingPointToBV &old) : FloatingPointToBV(old) {}
+  };
+  class CVC4_PUBLIC FloatingPointToUBVTotal : public FloatingPointToBV {
+  public : FloatingPointToUBVTotal (unsigned _s) : FloatingPointToBV(_s) {}
+    FloatingPointToUBVTotal (const FloatingPointToBV &old) : FloatingPointToBV(old) {}
+  };
+  class CVC4_PUBLIC FloatingPointToSBVTotal : public FloatingPointToBV {
+  public : FloatingPointToSBVTotal (unsigned _s) : FloatingPointToBV(_s) {}
+    FloatingPointToSBVTotal (const FloatingPointToBV &old) : FloatingPointToBV(old) {}
   };
 
 
@@ -235,16 +325,28 @@ namespace CVC4 {
   }; /* struct FloatingPointToBVHashFunction */
 
 
-
+  // It is not possible to pack a number without a size to pack to,
+  // thus it is difficult to implement this in a sensible way.  Use
+  // FloatingPoint instead...
+  /*
   inline std::ostream& operator <<(std::ostream& os, const FloatingPointLiteral& fp) CVC4_PUBLIC;
   inline std::ostream& operator <<(std::ostream& os, const FloatingPointLiteral& fp) {
-    fp.unfinished();
-    return os;
+    return os << "FloatingPointLiteral";
   }
+  */
 
   inline std::ostream& operator <<(std::ostream& os, const FloatingPoint& fp) CVC4_PUBLIC;
   inline std::ostream& operator <<(std::ostream& os, const FloatingPoint& fp) {
-    return os << fp.getLiteral();
+    BitVector bv(fp.pack());
+
+    unsigned largestSignificandBit = fp.t.significand() - 2; // -1 for -inclusive, -1 for hidden
+    unsigned largestExponentBit = (fp.t.exponent() - 1) + (largestSignificandBit + 1);
+
+    return os
+      << "(fp #b" << bv.extract(largestExponentBit + 1, largestExponentBit + 1)
+      << " #b" << bv.extract(largestExponentBit, largestSignificandBit + 1)
+      << " #b" << bv.extract(largestSignificandBit, 0)
+      << ")";
   }
 
   inline std::ostream& operator <<(std::ostream& os, const FloatingPointSize& fps) CVC4_PUBLIC;