diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-10-01 11:29:39 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-10-01 13:29:39 -0500 |
commit | 4c2c2de951c52ef48704dbffe7ec5848917f1398 (patch) | |
tree | 0e16a730323c09f5343e0e35073b9b9c63ff3879 /src/util/floatingpoint.h.in | |
parent | 25aaeabe85f8c3f2c6701fcd48f00f221f8dfccf (diff) |
FloatingPoint: Add utility functions for largest and smallest normal. (#5174)
Diffstat (limited to 'src/util/floatingpoint.h.in')
-rw-r--r-- | src/util/floatingpoint.h.in | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/src/util/floatingpoint.h.in b/src/util/floatingpoint.h.in index 637f01104..9e78c20c0 100644 --- a/src/util/floatingpoint.h.in +++ b/src/util/floatingpoint.h.in @@ -368,6 +368,20 @@ namespace CVC4 { */ static FloatingPoint makeMaxSubnormal(const FloatingPointSize& size, bool sign); + /** + * Create the smallest normal FP value of given size. + * t: The FP size (format). + * sign: True for positive sign, false otherwise. + */ + static FloatingPoint makeMinNormal(const FloatingPointSize& size, + bool sign); + /** + * Create the largest normal FP value of given size. + * t: The FP size (format). + * sign: True for positive sign, false otherwise. + */ + static FloatingPoint makeMaxNormal(const FloatingPointSize& size, + bool sign); const FloatingPointLiteral& getLiteral(void) const { return this->fpl; } |