Floating point infrastructure.

Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>

4 files changed, 340 insertions, 1 deletions

diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index cca98db60..df787d049 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -100,6 +100,8 @@ libutil_la_SOURCES = \
 	didyoumean.cpp \
 	unsat_core.h \
 	unsat_core.cpp \
+	floatingpoint.h \
+	floatingpoint.cpp \
 	resource_manager.h \
 	resource_manager.cpp \
 	unsafe_interrupt_exception.h
@@ -164,7 +166,8 @@ EXTRA_DIST = \
 	resource_manager.i \
 	unsafe_interrupt_exception.i \
 	proof.i \
-	unsat_core.i
+	unsat_core.i \
+	floatingpoint.i
 
 DISTCLEANFILES = \
 	integer.h.tmp \
diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp
new file mode 100644
index 000000000..1aed6331e
--- /dev/null
+++ b/src/util/floatingpoint.cpp
@@ -0,0 +1,38 @@
+/*********************                                                        */
+/*! \file floatingpoint.cpp
+ ** \verbatim
+ ** Original author: Martin Brain
+ ** Major contributors:
+ ** Minor contributors (to current version):
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2013  University of Oxford
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Implementations of the utility functions for working with floating point theories. ]]
+ **
+ **/
+
+#include "util/cvc4_assert.h"
+#include "util/floatingpoint.h"
+
+namespace CVC4 {
+
+  FloatingPointSize::FloatingPointSize (unsigned _e, unsigned _s) : e(_e), s(_s)
+  {
+    CheckArgument(validExponentSize(_e),_e,"Invalid exponent size : %d",_e);
+    CheckArgument(validSignificandSize(_s),_s,"Invalid significand size : %d",_s);
+  }
+
+  FloatingPointSize::FloatingPointSize (const FloatingPointSize &old) : e(old.e), s(old.s)
+  {
+    CheckArgument(validExponentSize(e),e,"Invalid exponent size : %d",e);
+    CheckArgument(validSignificandSize(s),s,"Invalid significand size : %d",s);
+  }
+
+  void FloatingPointLiteral::unfinished (void) const {
+    Unimplemented("Floating-point literals not yet implemented.");
+  }
+
+}/* CVC4 namespace */
+
diff --git a/src/util/floatingpoint.h b/src/util/floatingpoint.h
new file mode 100644
index 000000000..e0678d389
--- /dev/null
+++ b/src/util/floatingpoint.h
@@ -0,0 +1,293 @@
+/*********************                                                        */
+/*! \file floatingpoint.h
+ ** \verbatim
+ ** Original author: Martin Brain
+ ** Major contributors:
+ ** Minor contributors (to current version):
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2013  University of Oxford
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Utility functions for working with floating point theories. ]]
+ **
+ ** [[ This file contains the data structures used by the constant and
+ **    parametric types of the floating point theory. ]]
+ **/
+
+#include <fenv.h>
+
+#include "cvc4_public.h"
+
+#include "util/bitvector.h"
+
+
+#ifndef __CVC4__FLOATINGPOINT_H
+#define __CVC4__FLOATINGPOINT_H
+
+
+
+namespace CVC4 {
+
+
+  // Inline these!
+  inline bool CVC4_PUBLIC validExponentSize (unsigned e) { return e >= 2; }
+  inline bool CVC4_PUBLIC validSignificandSize (unsigned s) { return s >= 2; }
+
+  /**
+   * Floating point sorts are parameterised by two non-zero constants
+   * giving the width (in bits) of the exponent and significand
+   * (including the hidden bit).
+   */
+  class CVC4_PUBLIC FloatingPointSize {
+    /*
+      Class invariants:
+      * VALIDEXPONENTSIZE(e)
+      * VALIDSIGNIFCANDSIZE(s)
+     */
+
+  private :
+    unsigned e;
+    unsigned s;
+
+  public :
+    FloatingPointSize (unsigned _e, unsigned _s);
+    FloatingPointSize (const FloatingPointSize &old);
+
+    inline unsigned exponent (void) const {
+      return this->e;
+    }
+
+    inline unsigned significand (void) const {
+      return this->s;
+    }
+
+    bool operator ==(const FloatingPointSize& fps) const {
+      return (e == fps.e) && (s == fps.s);
+    }
+
+  }; /* class FloatingPointSize */
+
+
+
+#define ROLL(X,N) (((X) << (N)) | ((X) >> (8*sizeof((X)) - (N)) ))
+
+  struct CVC4_PUBLIC FloatingPointSizeHashFunction {
+    inline size_t operator() (const FloatingPointSize& fpt) const {
+      return size_t(ROLL(fpt.exponent(), 4*sizeof(unsigned)) |
+		    fpt.significand());
+    }
+  }; /* struct FloatingPointSizeHashFunction */
+
+
+
+
+
+
+
+
+
+
+  /**
+   * A concrete instance of the rounding mode sort
+   */
+  enum CVC4_PUBLIC RoundingMode {
+    roundNearestTiesToEven = FE_TONEAREST,
+    roundNearestTiesToAway,
+    roundTowardPositive = FE_UPWARD,
+    roundTowardNegative = FE_DOWNWARD,
+    roundTowardZero = FE_TOWARDZERO
+  }; /* enum RoundingMode */
+
+  struct CVC4_PUBLIC RoundingModeHashFunction {
+    inline size_t operator() (const RoundingMode& rm) const {
+      return size_t(rm);
+    }
+  }; /* struct RoundingModeHashFunction */
+
+
+
+
+
+
+
+
+
+
+  /**
+   * A concrete floating point number
+   */
+
+  class CVC4_PUBLIC FloatingPointLiteral {
+  public :
+    // This intentional left unfinished as the choice of literal
+    // representation is solver specific.
+    void unfinished (void) const;
+
+    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;
+    }
+
+    size_t hash (void) const {
+      unfinished();
+      return 23;
+    }
+  };
+
+  class CVC4_PUBLIC FloatingPoint {
+  protected :
+    FloatingPointLiteral fpl;
+
+  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 (const FloatingPoint &fp) : fpl(fp.fpl), t(fp.t) {}
+
+    bool operator ==(const FloatingPoint& fp) const {
+      return ( (t == fp.t) && fpl == fp.fpl );
+    }
+
+    const FloatingPointLiteral & getLiteral (void) const {
+      return this->fpl;
+    }
+
+  }; /* class FloatingPoint */
+
+
+  struct CVC4_PUBLIC FloatingPointHashFunction {
+    inline size_t operator() (const FloatingPoint& fp) const {
+      FloatingPointSizeHashFunction h;
+      return h(fp.t) ^ fp.getLiteral().hash();
+    }
+  }; /* struct FloatingPointHashFunction */
+
+
+
+
+
+
+
+  /**
+   * The parameter type for the conversions to floating point.
+   */
+  class CVC4_PUBLIC FloatingPointConvertSort {
+  public :
+    FloatingPointSize t;
+
+    FloatingPointConvertSort (unsigned _e, unsigned _s)
+      : t(_e,_s) {}
+
+    bool operator ==(const FloatingPointConvertSort& fpcs) const {
+      return t == fpcs.t;
+    }
+
+  };
+
+  /**
+   * As different conversions are different parameterised kinds, there
+   * is a need for different (C++) types for each one.
+   */
+
+  class CVC4_PUBLIC FloatingPointToFPIEEEBitVector : public FloatingPointConvertSort {
+  public : FloatingPointToFPIEEEBitVector (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {}
+  };
+  class CVC4_PUBLIC FloatingPointToFPFloatingPoint : public FloatingPointConvertSort {
+  public : FloatingPointToFPFloatingPoint (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {}
+  };
+  class CVC4_PUBLIC FloatingPointToFPReal : public FloatingPointConvertSort {
+  public : FloatingPointToFPReal (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {}
+  };
+  class CVC4_PUBLIC FloatingPointToFPSignedBitVector : public FloatingPointConvertSort {
+  public : FloatingPointToFPSignedBitVector (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {}
+  };
+  class CVC4_PUBLIC FloatingPointToFPUnsignedBitVector : public FloatingPointConvertSort {
+  public : FloatingPointToFPUnsignedBitVector (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {}
+  };
+  class CVC4_PUBLIC FloatingPointToFPGeneric : public FloatingPointConvertSort {
+  public : FloatingPointToFPGeneric (unsigned _e, unsigned _s) : FloatingPointConvertSort(_e,_s) {}
+  };
+
+
+
+  template <unsigned key>
+  struct CVC4_PUBLIC FloatingPointConvertSortHashFunction {
+    inline size_t operator() (const FloatingPointConvertSort& fpcs) const {
+      FloatingPointSizeHashFunction f;
+      return f(fpcs.t) ^ (0x00005300 | (key << 24));
+    }
+  }; /* struct FloatingPointConvertSortHashFunction */
+
+
+
+
+
+
+
+
+  /**
+   * The parameter type for the conversion to bit vector.
+   */
+  class CVC4_PUBLIC FloatingPointToBV {
+  public :
+    BitVectorSize bvs;
+
+    FloatingPointToBV (unsigned s)
+      : bvs(s) {}
+    operator unsigned () const { return bvs; }
+  };
+
+  class CVC4_PUBLIC FloatingPointToUBV : public FloatingPointToBV {
+  public : FloatingPointToUBV (unsigned _s) : FloatingPointToBV(_s) {}
+  };
+  class CVC4_PUBLIC FloatingPointToSBV : public FloatingPointToBV {
+  public : FloatingPointToSBV (unsigned _s) : FloatingPointToBV(_s) {}
+  };
+
+
+  template <unsigned key>
+  struct CVC4_PUBLIC FloatingPointToBVHashFunction {
+    inline size_t operator() (const FloatingPointToBV& fptbv) const {
+      UnsignedHashFunction< ::CVC4::BitVectorSize > f;
+      return 	(key ^ 0x46504256) ^ f(fptbv.bvs);
+    }
+  }; /* struct FloatingPointToBVHashFunction */
+
+
+
+
+
+
+  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;
+  }
+
+  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();
+  }
+
+  inline std::ostream& operator <<(std::ostream& os, const FloatingPointSize& fps) CVC4_PUBLIC;
+  inline std::ostream& operator <<(std::ostream& os, const FloatingPointSize& fps) {
+    return os << "(_ FloatingPoint " << fps.exponent() << " " << fps.significand() << ")";
+  }
+
+  inline std::ostream& operator <<(std::ostream& os, const FloatingPointConvertSort& fpcs) CVC4_PUBLIC;
+  inline std::ostream& operator <<(std::ostream& os, const FloatingPointConvertSort& fpcs) {
+    return os << "(_ to_fp " << fpcs.t.exponent() << " " << fpcs.t.significand() << ")";
+  }
+
+
+
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__FLOATINGPOINT_H */
diff --git a/src/util/floatingpoint.i b/src/util/floatingpoint.i
new file mode 100644
index 000000000..c66cc311d
--- /dev/null
+++ b/src/util/floatingpoint.i
@@ -0,0 +1,5 @@
+%{
+#include "util/floatingpoint.h"
+%}
+
+%include "util/floatingpoint.h"