1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Morgan Deters, Tim King, Mathias Preiner |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
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. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Enumerators for rationals and integers. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "cvc5_private.h" |
17 |
|
|
18 |
|
#ifndef CVC5__THEORY__ARITH__TYPE_ENUMERATOR_H |
19 |
|
#define CVC5__THEORY__ARITH__TYPE_ENUMERATOR_H |
20 |
|
|
21 |
|
#include "expr/kind.h" |
22 |
|
#include "expr/type_node.h" |
23 |
|
#include "theory/type_enumerator.h" |
24 |
|
#include "util/integer.h" |
25 |
|
#include "util/rational.h" |
26 |
|
|
27 |
|
namespace cvc5 { |
28 |
|
namespace theory { |
29 |
|
namespace arith { |
30 |
|
|
31 |
567 |
class RationalEnumerator : public TypeEnumeratorBase<RationalEnumerator> { |
32 |
|
Rational d_rat; |
33 |
|
|
34 |
|
public: |
35 |
195 |
RationalEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr) |
36 |
195 |
: TypeEnumeratorBase<RationalEnumerator>(type), d_rat(0) |
37 |
|
{ |
38 |
195 |
Assert(type.getKind() == kind::TYPE_CONSTANT |
39 |
|
&& type.getConst<TypeConstant>() == REAL_TYPE); |
40 |
195 |
} |
41 |
|
|
42 |
1733 |
Node operator*() override { return NodeManager::currentNM()->mkConst(d_rat); } |
43 |
411 |
RationalEnumerator& operator++() override |
44 |
|
{ |
45 |
|
// sequence is 0, then diagonal with negatives interleaved |
46 |
|
// ( 0, 1/1, -1/1, 2/1, -2/1, 1/2, -1/2, 3/1, -3/1, 1/3, -1/3, |
47 |
|
// 4/1, -4/1, 3/2, -3/2, 2/3, -2/3, 1/4, -1/4, ...) |
48 |
411 |
if(d_rat == 0) { |
49 |
120 |
d_rat = 1; |
50 |
291 |
} else if(d_rat < 0) { |
51 |
119 |
d_rat = -d_rat; |
52 |
238 |
Integer num = d_rat.getNumerator(); |
53 |
238 |
Integer den = d_rat.getDenominator(); |
54 |
16 |
do { |
55 |
135 |
num -= 1; |
56 |
135 |
den += 1; |
57 |
135 |
if(num == 0) { |
58 |
67 |
num = den; |
59 |
67 |
den = 1; |
60 |
|
} |
61 |
135 |
d_rat = Rational(num, den); |
62 |
135 |
} while(d_rat.getNumerator() != num); |
63 |
|
} else { |
64 |
172 |
d_rat = -d_rat; |
65 |
|
} |
66 |
411 |
return *this; |
67 |
|
} |
68 |
|
|
69 |
2070 |
bool isFinished() override { return false; } |
70 |
|
};/* class RationalEnumerator */ |
71 |
|
|
72 |
30488 |
class IntegerEnumerator : public TypeEnumeratorBase<IntegerEnumerator> { |
73 |
|
Integer d_int; |
74 |
|
|
75 |
|
public: |
76 |
8146 |
IntegerEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr) |
77 |
8146 |
: TypeEnumeratorBase<IntegerEnumerator>(type), d_int(0) |
78 |
|
{ |
79 |
8146 |
Assert(type.getKind() == kind::TYPE_CONSTANT |
80 |
|
&& type.getConst<TypeConstant>() == INTEGER_TYPE); |
81 |
8146 |
} |
82 |
|
|
83 |
65807 |
Node operator*() override |
84 |
|
{ |
85 |
65807 |
return NodeManager::currentNM()->mkConst(Rational(d_int)); |
86 |
|
} |
87 |
|
|
88 |
12110 |
IntegerEnumerator& operator++() override |
89 |
|
{ |
90 |
|
// sequence is 0, 1, -1, 2, -2, 3, -3, ... |
91 |
12110 |
if(d_int <= 0) { |
92 |
6730 |
d_int = -d_int + 1; |
93 |
|
} else { |
94 |
5380 |
d_int = -d_int; |
95 |
|
} |
96 |
12110 |
return *this; |
97 |
|
} |
98 |
|
|
99 |
77992 |
bool isFinished() override { return false; } |
100 |
|
};/* class IntegerEnumerator */ |
101 |
|
|
102 |
|
} // namespace arith |
103 |
|
} // namespace theory |
104 |
|
} // namespace cvc5 |
105 |
|
|
106 |
|
#endif /* CVC5__THEORY__ARITH__TYPE_ENUMERATOR_H */ |