GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/fp/type_enumerator.h Lines: 27 44 61.4 %
Date: 2021-03-23 Branches: 17 70 24.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file type_enumerator.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Tim King, Martin Brain, Aina Niemetz
6
 ** Copyright (c) 2009-2015  New York University and The University of Iowa
7
 ** This file is part of the CVC4 project.
8
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
9
 ** in the top-level source directory and their institutional affiliations.
10
 ** All rights reserved.  See the file COPYING in the top-level source
11
 ** directory for licensing information.\endverbatim
12
 **
13
 ** \brief An enumerator for floating-point numbers.
14
 **
15
 ** An enumerator for floating-point numbers.
16
 **/
17
18
#include "cvc4_private.h"
19
20
#ifndef CVC4__THEORY__FP__TYPE_ENUMERATOR_H
21
#define CVC4__THEORY__FP__TYPE_ENUMERATOR_H
22
23
#include "expr/kind.h"
24
#include "expr/type_node.h"
25
#include "theory/type_enumerator.h"
26
#include "util/bitvector.h"
27
#include "util/floatingpoint.h"
28
29
namespace CVC4 {
30
namespace theory {
31
namespace fp {
32
33
28
class FloatingPointEnumerator
34
    : public TypeEnumeratorBase<FloatingPointEnumerator> {
35
 public:
36
14
  FloatingPointEnumerator(TypeNode type,
37
                          TypeEnumeratorProperties* tep = nullptr)
38
14
      : TypeEnumeratorBase<FloatingPointEnumerator>(type),
39
14
        d_e(type.getFloatingPointExponentSize()),
40
14
        d_s(type.getFloatingPointSignificandSize()),
41
14
        d_state(d_e + d_s, 0U),
42
56
        d_enumerationComplete(false) {}
43
44
  /** Throws NoMoreValuesException if the enumeration is complete. */
45
28
  Node operator*() override {
46
28
    if (d_enumerationComplete) {
47
      throw NoMoreValuesException(getType());
48
    }
49
28
    return NodeManager::currentNM()->mkConst(createFP());
50
  }
51
52
  FloatingPointEnumerator& operator++() override {
53
    const FloatingPoint current(createFP());
54
    if (current.isNaN()) {
55
      d_enumerationComplete = true;
56
    } else {
57
      d_state = d_state + BitVector(d_state.getSize(), 1U);
58
    }
59
    return *this;
60
  }
61
62
28
  bool isFinished() override { return d_enumerationComplete; }
63
64
 protected:
65
28
  FloatingPoint createFP(void) const {
66
    // Rotate the LSB into the sign so that NaN is the last value
67
28
    uint64_t vone = 1;
68
28
    uint64_t vmax = d_state.getSize() - 1;
69
    BitVector bva =
70
56
        d_state.logicalRightShift(BitVector(d_state.getSize(), vone));
71
56
    BitVector bvb = d_state.leftShift(BitVector(d_state.getSize(), vmax));
72
56
    const BitVector value = (bva | bvb);
73
74
56
    return FloatingPoint(d_e, d_s, value);
75
  }
76
77
 private:
78
  const unsigned d_e;
79
  const unsigned d_s;
80
  BitVector d_state;
81
  bool d_enumerationComplete;
82
}; /* FloatingPointEnumerator */
83
84
2
class RoundingModeEnumerator
85
    : public TypeEnumeratorBase<RoundingModeEnumerator> {
86
 public:
87
1
  RoundingModeEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr)
88
1
      : TypeEnumeratorBase<RoundingModeEnumerator>(type),
89
        d_rm(ROUND_NEAREST_TIES_TO_EVEN),
90
1
        d_enumerationComplete(false)
91
  {
92
1
  }
93
94
  /** Throws NoMoreValuesException if the enumeration is complete. */
95
2
  Node operator*() override {
96
2
    if (d_enumerationComplete) {
97
      throw NoMoreValuesException(getType());
98
    }
99
2
    return NodeManager::currentNM()->mkConst(d_rm);
100
  }
101
102
  RoundingModeEnumerator& operator++() override {
103
    switch (d_rm) {
104
      case ROUND_NEAREST_TIES_TO_EVEN: d_rm = ROUND_TOWARD_POSITIVE; break;
105
      case ROUND_TOWARD_POSITIVE: d_rm = ROUND_TOWARD_NEGATIVE; break;
106
      case ROUND_TOWARD_NEGATIVE: d_rm = ROUND_TOWARD_ZERO; break;
107
      case ROUND_TOWARD_ZERO: d_rm = ROUND_NEAREST_TIES_TO_AWAY; break;
108
      case ROUND_NEAREST_TIES_TO_AWAY: d_enumerationComplete = true; break;
109
      default: Unreachable() << "Unknown rounding mode?"; break;
110
    }
111
    return *this;
112
  }
113
114
2
  bool isFinished() override { return d_enumerationComplete; }
115
116
 private:
117
  RoundingMode d_rm;
118
  bool d_enumerationComplete;
119
}; /* RoundingModeEnumerator */
120
121
}  // namespace fp
122
}  // namespace theory
123
}  // namespace CVC4
124
125
#endif /* CVC4__THEORY__FP__TYPE_ENUMERATOR_H */