GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/type_enumerator.h Lines: 37 37 100.0 %
Date: 2021-03-22 Branches: 51 116 44.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file type_enumerator.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Morgan Deters, Tim King, Mathias Preiner
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 Enumerators for rationals and integers
13
 **
14
 ** Enumerators for rationals and integers.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__THEORY__ARITH__TYPE_ENUMERATOR_H
20
#define CVC4__THEORY__ARITH__TYPE_ENUMERATOR_H
21
22
#include "expr/kind.h"
23
#include "expr/type_node.h"
24
#include "theory/type_enumerator.h"
25
#include "util/integer.h"
26
#include "util/rational.h"
27
28
namespace CVC4 {
29
namespace theory {
30
namespace arith {
31
32
636
class RationalEnumerator : public TypeEnumeratorBase<RationalEnumerator> {
33
  Rational d_rat;
34
35
 public:
36
228
  RationalEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr)
37
228
      : TypeEnumeratorBase<RationalEnumerator>(type), d_rat(0)
38
  {
39
228
    Assert(type.getKind() == kind::TYPE_CONSTANT
40
           && type.getConst<TypeConstant>() == REAL_TYPE);
41
228
  }
42
43
1866
  Node operator*() override { return NodeManager::currentNM()->mkConst(d_rat); }
44
440
  RationalEnumerator& operator++() override
45
  {
46
    // sequence is 0, then diagonal with negatives interleaved
47
    // ( 0, 1/1, -1/1, 2/1, -2/1, 1/2, -1/2, 3/1, -3/1, 1/3, -1/3,
48
    // 4/1, -4/1, 3/2, -3/2, 2/3, -2/3, 1/4, -1/4, ...)
49
440
    if(d_rat == 0) {
50
129
      d_rat = 1;
51
311
    } else if(d_rat < 0) {
52
127
      d_rat = -d_rat;
53
254
      Integer num = d_rat.getNumerator();
54
254
      Integer den = d_rat.getDenominator();
55
16
      do {
56
143
        num -= 1;
57
143
        den += 1;
58
143
        if(num == 0) {
59
72
          num = den;
60
72
          den = 1;
61
        }
62
143
        d_rat = Rational(num, den);
63
143
      } while(d_rat.getNumerator() != num);
64
    } else {
65
184
      d_rat = -d_rat;
66
    }
67
440
    return *this;
68
  }
69
70
2232
  bool isFinished() override { return false; }
71
};/* class RationalEnumerator */
72
73
25082
class IntegerEnumerator : public TypeEnumeratorBase<IntegerEnumerator> {
74
  Integer d_int;
75
76
 public:
77
5368
  IntegerEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr)
78
5368
      : TypeEnumeratorBase<IntegerEnumerator>(type), d_int(0)
79
  {
80
5368
    Assert(type.getKind() == kind::TYPE_CONSTANT
81
           && type.getConst<TypeConstant>() == INTEGER_TYPE);
82
5368
  }
83
84
61428
  Node operator*() override
85
  {
86
61428
    return NodeManager::currentNM()->mkConst(Rational(d_int));
87
  }
88
89
12503
  IntegerEnumerator& operator++() override
90
  {
91
    // sequence is 0, 1, -1, 2, -2, 3, -3, ...
92
12503
    if(d_int <= 0) {
93
6898
      d_int = -d_int + 1;
94
    } else {
95
5605
      d_int = -d_int;
96
    }
97
12503
    return *this;
98
  }
99
100
73962
  bool isFinished() override { return false; }
101
};/* class IntegerEnumerator */
102
103
}/* CVC4::theory::arith namespace */
104
}/* CVC4::theory namespace */
105
}/* CVC4 namespace */
106
107
#endif /* CVC4__THEORY__ARITH__TYPE_ENUMERATOR_H */