diff options
Diffstat (limited to 'src/util/floatingpoint.h')
-rw-r--r-- | src/util/floatingpoint.h | 38 |
1 files changed, 2 insertions, 36 deletions
diff --git a/src/util/floatingpoint.h b/src/util/floatingpoint.h index e0678d389..132d67b1c 100644 --- a/src/util/floatingpoint.h +++ b/src/util/floatingpoint.h @@ -14,22 +14,16 @@ ** [[ 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 +#include <fenv.h> +#include "util/bitvector.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; } @@ -80,14 +74,6 @@ namespace CVC4 { }; /* struct FloatingPointSizeHashFunction */ - - - - - - - - /** * A concrete instance of the rounding mode sort */ @@ -106,14 +92,6 @@ namespace CVC4 { }; /* struct RoundingModeHashFunction */ - - - - - - - - /** * A concrete floating point number */ @@ -168,12 +146,6 @@ namespace CVC4 { } }; /* struct FloatingPointHashFunction */ - - - - - - /** * The parameter type for the conversions to floating point. */ @@ -261,9 +233,6 @@ namespace CVC4 { - - - inline std::ostream& operator <<(std::ostream& os, const FloatingPointLiteral& fp) CVC4_PUBLIC; inline std::ostream& operator <<(std::ostream& os, const FloatingPointLiteral& fp) { fp.unfinished(); @@ -285,9 +254,6 @@ namespace CVC4 { return os << "(_ to_fp " << fpcs.t.exponent() << " " << fpcs.t.significand() << ")"; } - - - }/* CVC4 namespace */ #endif /* __CVC4__FLOATINGPOINT_H */ |