blob: a5b7a336c600ce7955b6a682e82e741f148404eb (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
|
/******************************************************************************
* Top contributors (to current version):
* Aina Niemetz, Martin Brain, Mathias Preiner
*
* This file is part of the cvc5 project.
*
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
* in the top-level source directory and their institutional affiliations.
* All rights reserved. See the file COPYING in the top-level source
* directory for licensing information.
* ****************************************************************************
*
* The class representing a floating-point format.
*/
#include "cvc5_public.h"
#ifndef CVC5__FLOATINGPOINT_SIZE_H
#define CVC5__FLOATINGPOINT_SIZE_H
namespace cvc5 {
// Inline these!
inline bool validExponentSize(uint32_t e) { return e >= 2; }
inline bool validSignificandSize(uint32_t s) { return s >= 2; }
/**
* Floating point sorts are parameterised by two constants > 1 giving the
* width (in bits) of the exponent and significand (including the hidden bit).
* So, IEEE-754 single precision, a.k.a. float, is described as 8 24.
*/
class FloatingPointSize
{
public:
/** Constructors. */
FloatingPointSize(uint32_t exp_size, uint32_t sig_size);
FloatingPointSize(const FloatingPointSize& old);
/** Operator overload for equality comparison. */
bool operator==(const FloatingPointSize& fps) const
{
return (d_exp_size == fps.d_exp_size) && (d_sig_size == fps.d_sig_size);
}
/** Implement the interface that symfpu uses for floating-point formats. */
/** Get the exponent bit-width of this floating-point format. */
inline uint32_t exponentWidth(void) const { return d_exp_size; }
/** Get the significand bit-width of this floating-point format. */
inline uint32_t significandWidth(void) const { return d_sig_size; }
/**
* Get the bit-width of the packed representation of this floating-point
* format (= exponent + significand bit-width, convenience wrapper).
*/
inline uint32_t packedWidth(void) const
{
return exponentWidth() + significandWidth();
}
/**
* Get the exponent bit-width of the packed representation of this
* floating-point format (= exponent bit-width).
*/
inline uint32_t packedExponentWidth(void) const { return exponentWidth(); }
/**
* Get the significand bit-width of the packed representation of this
* floating-point format (= significand bit-width - 1).
*/
inline uint32_t packedSignificandWidth(void) const
{
return significandWidth() - 1;
}
private:
/** Exponent bit-width. */
uint32_t d_exp_size;
/** Significand bit-width. */
uint32_t d_sig_size;
}; /* class FloatingPointSize */
/**
* Hash function for floating point formats.
*/
struct FloatingPointSizeHashFunction
{
static inline size_t ROLL(size_t X, size_t N)
{
return (((X) << (N)) | ((X) >> (8 * sizeof((X)) - (N))));
}
inline size_t operator()(const FloatingPointSize& t) const
{
return size_t(ROLL(t.exponentWidth(), 4 * sizeof(uint32_t))
| t.significandWidth());
}
}; /* struct FloatingPointSizeHashFunction */
} // namespace cvc5
#endif
|
