1 /********************* */
2 /*! \file type_enumerator.h
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-2020 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
13 ** \brief An enumerator for floating-point numbers.
15 ** An enumerator for floating-point numbers.
18 #include "cvc4_private.h"
20 #ifndef CVC4__THEORY__FP__TYPE_ENUMERATOR_H
21 #define CVC4__THEORY__FP__TYPE_ENUMERATOR_H
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"
33 class FloatingPointEnumerator
34 : public TypeEnumeratorBase
<FloatingPointEnumerator
> {
36 FloatingPointEnumerator(TypeNode type
,
37 TypeEnumeratorProperties
* tep
= nullptr)
38 : TypeEnumeratorBase
<FloatingPointEnumerator
>(type
),
39 d_e(type
.getFloatingPointExponentSize()),
40 d_s(type
.getFloatingPointSignificandSize()),
41 d_state(d_e
+ d_s
, 0U),
42 d_enumerationComplete(false) {}
44 /** Throws NoMoreValuesException if the enumeration is complete. */
45 Node
operator*() override
{
46 if (d_enumerationComplete
) {
47 throw NoMoreValuesException(getType());
49 return NodeManager::currentNM()->mkConst(createFP());
52 FloatingPointEnumerator
& operator++() override
{
53 const FloatingPoint
current(createFP());
54 if (current
.isNaN()) {
55 d_enumerationComplete
= true;
57 d_state
= d_state
+ BitVector(d_state
.getSize(), 1U);
62 bool isFinished() override
{ return d_enumerationComplete
; }
65 FloatingPoint
createFP(void) const {
66 // Rotate the LSB into the sign so that NaN is the last value
68 uint64_t vmax
= d_state
.getSize() - 1;
70 d_state
.logicalRightShift(BitVector(d_state
.getSize(), vone
));
71 BitVector bvb
= d_state
.leftShift(BitVector(d_state
.getSize(), vmax
));
72 const BitVector value
= (bva
| bvb
);
74 return FloatingPoint(d_e
, d_s
, value
);
81 bool d_enumerationComplete
;
82 }; /* FloatingPointEnumerator */
84 class RoundingModeEnumerator
85 : public TypeEnumeratorBase
<RoundingModeEnumerator
> {
87 RoundingModeEnumerator(TypeNode type
, TypeEnumeratorProperties
* tep
= nullptr)
88 : TypeEnumeratorBase
<RoundingModeEnumerator
>(type
),
89 d_rm(ROUND_NEAREST_TIES_TO_EVEN
),
90 d_enumerationComplete(false)
94 /** Throws NoMoreValuesException if the enumeration is complete. */
95 Node
operator*() override
{
96 if (d_enumerationComplete
) {
97 throw NoMoreValuesException(getType());
99 return NodeManager::currentNM()->mkConst(d_rm
);
102 RoundingModeEnumerator
& operator++() override
{
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;
114 bool isFinished() override
{ return d_enumerationComplete
; }
118 bool d_enumerationComplete
;
119 }; /* RoundingModeEnumerator */
122 } // namespace theory
125 #endif /* CVC4__THEORY__FP__TYPE_ENUMERATOR_H */