GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/uf/equality_engine_iterator.cpp Lines: 47 60 78.3 %
Date: 2021-03-22 Branches: 38 184 20.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file equality_engine_iterator.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Dejan Jovanovic, Morgan Deters
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 Implementation of iterator class for equality engine
13
 **/
14
15
#include "theory/uf/equality_engine_iterator.h"
16
17
#include "theory/uf/equality_engine.h"
18
19
namespace CVC4 {
20
namespace theory {
21
namespace eq {
22
23
71
EqClassesIterator::EqClassesIterator() : d_ee(nullptr), d_it(0) {}
24
25
310738
EqClassesIterator::EqClassesIterator(const eq::EqualityEngine* ee) : d_ee(ee)
26
{
27
310738
  Assert(d_ee->consistent());
28
310738
  d_it = 0;
29
  // Go to the first non-internal node that is it's own representative
30
621476
  if (d_it < d_ee->d_nodesCount
31
310738
      && (d_ee->d_isInternal[d_it]
32
310738
          || d_ee->getEqualityNode(d_it).getFind() != d_it))
33
  {
34
    ++d_it;
35
  }
36
310738
}
37
38
8279632
Node EqClassesIterator::operator*() const { return d_ee->d_nodes[d_it]; }
39
40
bool EqClassesIterator::operator==(const EqClassesIterator& i) const
41
{
42
  return d_ee == i.d_ee && d_it == i.d_it;
43
}
44
45
bool EqClassesIterator::operator!=(const EqClassesIterator& i) const
46
{
47
  return !(*this == i);
48
}
49
50
8276781
EqClassesIterator& EqClassesIterator::operator++()
51
{
52
8276781
  ++d_it;
53
70294275
  while (d_it < d_ee->d_nodesCount
54
70294275
         && (d_ee->d_isInternal[d_it]
55
31651727
             || d_ee->getEqualityNode(d_it).getFind() != d_it))
56
  {
57
31008747
    ++d_it;
58
  }
59
8276781
  return *this;
60
}
61
62
EqClassesIterator EqClassesIterator::operator++(int)
63
{
64
  EqClassesIterator i = *this;
65
  ++*this;
66
  return i;
67
}
68
69
8587014
bool EqClassesIterator::isFinished() const
70
{
71
8587014
  return d_it >= d_ee->d_nodesCount;
72
}
73
74
32602
EqClassIterator::EqClassIterator()
75
32602
    : d_ee(nullptr), d_start(null_id), d_current(null_id)
76
{
77
32602
}
78
79
5731922
EqClassIterator::EqClassIterator(Node eqc, const eq::EqualityEngine* ee)
80
5731922
    : d_ee(ee)
81
{
82
5731922
  Assert(d_ee->consistent());
83
5731922
  d_current = d_start = d_ee->getNodeId(eqc);
84
5731922
  Assert(d_start == d_ee->getEqualityNode(d_start).getFind());
85
5731922
  Assert(!d_ee->d_isInternal[d_start]);
86
5731922
}
87
88
20366142
Node EqClassIterator::operator*() const { return d_ee->d_nodes[d_current]; }
89
90
bool EqClassIterator::operator==(const EqClassIterator& i) const
91
{
92
  return d_ee == i.d_ee && d_current == i.d_current;
93
}
94
95
bool EqClassIterator::operator!=(const EqClassIterator& i) const
96
{
97
  return !(*this == i);
98
}
99
100
19736130
EqClassIterator& EqClassIterator::operator++()
101
{
102
19736130
  Assert(!isFinished());
103
104
19736130
  Assert(d_start == d_ee->getEqualityNode(d_current).getFind());
105
19736130
  Assert(!d_ee->d_isInternal[d_current]);
106
107
  // Find the next one
108
72220
  do
109
  {
110
19808350
    d_current = d_ee->getEqualityNode(d_current).getNext();
111
19808350
  } while (d_ee->d_isInternal[d_current]);
112
113
19736130
  Assert(d_start == d_ee->getEqualityNode(d_current).getFind());
114
19736130
  Assert(!d_ee->d_isInternal[d_current]);
115
116
19736130
  if (d_current == d_start)
117
  {
118
    // we end when we have cycled back to the original representative
119
5429088
    d_current = null_id;
120
  }
121
19736130
  return *this;
122
}
123
124
51518
EqClassIterator EqClassIterator::operator++(int)
125
{
126
51518
  EqClassIterator i = *this;
127
51518
  ++*this;
128
51518
  return i;
129
}
130
131
45092489
bool EqClassIterator::isFinished() const { return d_current == null_id; }
132
133
}  // namespace eq
134
}  // Namespace theory
135
26676
}  // Namespace CVC4