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 |
585 |
class RationalEnumerator : public TypeEnumeratorBase<RationalEnumerator> { |
32 |
|
Rational d_rat; |
33 |
|
|
34 |
|
public: |
35 |
204 |
RationalEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr) |
36 |
204 |
: TypeEnumeratorBase<RationalEnumerator>(type), d_rat(0) |
37 |
|
{ |
38 |
204 |
Assert(type.getKind() == kind::TYPE_CONSTANT |
39 |
|
&& type.getConst<TypeConstant>() == REAL_TYPE); |
40 |
204 |
} |
41 |
|
|
42 |
1673 |
Node operator*() override { return NodeManager::currentNM()->mkConst(d_rat); } |
43 |
379 |
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 |
379 |
if(d_rat == 0) { |
49 |
111 |
d_rat = 1; |
50 |
268 |
} else if(d_rat < 0) { |
51 |
107 |
d_rat = -d_rat; |
52 |
214 |
Integer num = d_rat.getNumerator(); |
53 |
214 |
Integer den = d_rat.getDenominator(); |
54 |
16 |
do { |
55 |
123 |
num -= 1; |
56 |
123 |
den += 1; |
57 |
123 |
if(num == 0) { |
58 |
57 |
num = den; |
59 |
57 |
den = 1; |
60 |
|
} |
61 |
123 |
d_rat = Rational(num, den); |
62 |
123 |
} while(d_rat.getNumerator() != num); |
63 |
|
} else { |
64 |
161 |
d_rat = -d_rat; |
65 |
|
} |
66 |
379 |
return *this; |
67 |
|
} |
68 |
|
|
69 |
1978 |
bool isFinished() override { return false; } |
70 |
|
};/* class RationalEnumerator */ |
71 |
|
|
72 |
30220 |
class IntegerEnumerator : public TypeEnumeratorBase<IntegerEnumerator> { |
73 |
|
Integer d_int; |
74 |
|
|
75 |
|
public: |
76 |
7982 |
IntegerEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr) |
77 |
7982 |
: TypeEnumeratorBase<IntegerEnumerator>(type), d_int(0) |
78 |
|
{ |
79 |
7982 |
Assert(type.getKind() == kind::TYPE_CONSTANT |
80 |
|
&& type.getConst<TypeConstant>() == INTEGER_TYPE); |
81 |
7982 |
} |
82 |
|
|
83 |
63250 |
Node operator*() override |
84 |
|
{ |
85 |
63250 |
return NodeManager::currentNM()->mkConst(Rational(d_int)); |
86 |
|
} |
87 |
|
|
88 |
11339 |
IntegerEnumerator& operator++() override |
89 |
|
{ |
90 |
|
// sequence is 0, 1, -1, 2, -2, 3, -3, ... |
91 |
11339 |
if(d_int <= 0) { |
92 |
6354 |
d_int = -d_int + 1; |
93 |
|
} else { |
94 |
4985 |
d_int = -d_int; |
95 |
|
} |
96 |
11339 |
return *this; |
97 |
|
} |
98 |
|
|
99 |
74664 |
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 */ |