GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/util/floatingpoint_size.h Lines: 16 16 100.0 %
Date: 2021-03-22 Branches: 2 4 50.0 %

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