Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/uf/equality_engine_iterator.cpp	Lines:	47	60	78.3 %
Date:	2021-11-07	Branches:	38	182	20.9 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Dejan Jovanovic, Morgan Deters
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Implementation of iterator class for equality engine.
 */

#include "theory/uf/equality_engine_iterator.h"

#include "theory/uf/equality_engine.h"

namespace cvc5 {
namespace theory {
namespace eq {

EqClassesIterator::EqClassesIterator() : d_ee(nullptr), d_it(0) {}

EqClassesIterator::EqClassesIterator(const eq::EqualityEngine* ee) : d_ee(ee)
{
  Assert(d_ee->consistent());
  d_it = 0;
  // Go to the first non-internal node that is it's own representative
  if (d_it < d_ee->d_nodesCount
      && (d_ee->d_isInternal[d_it]
          || d_ee->getEqualityNode(d_it).getFind() != d_it))
  {
    ++d_it;
  }
}

Node EqClassesIterator::operator*() const { return d_ee->d_nodes[d_it]; }

bool EqClassesIterator::operator==(const EqClassesIterator& i) const
{
  return d_ee == i.d_ee && d_it == i.d_it;
}

bool EqClassesIterator::operator!=(const EqClassesIterator& i) const
{
  return !(*this == i);
}

EqClassesIterator& EqClassesIterator::operator++()
{
  ++d_it;
  while (d_it < d_ee->d_nodesCount
         && (d_ee->d_isInternal[d_it]
             || d_ee->getEqualityNode(d_it).getFind() != d_it))
  {
    ++d_it;
  }
  return *this;
}

EqClassesIterator EqClassesIterator::operator++(int)
{
  EqClassesIterator i = *this;
  ++*this;
  return i;
}

bool EqClassesIterator::isFinished() const
{
  return d_it >= d_ee->d_nodesCount;
}

EqClassIterator::EqClassIterator()
    : d_ee(nullptr), d_start(null_id), d_current(null_id)
{
}

EqClassIterator::EqClassIterator(Node eqc, const eq::EqualityEngine* ee)
    : d_ee(ee)
{
  Assert(d_ee->consistent());
  d_current = d_start = d_ee->getNodeId(eqc);
  Assert(d_start == d_ee->getEqualityNode(d_start).getFind());
  Assert(!d_ee->d_isInternal[d_start]);
}

Node EqClassIterator::operator*() const { return d_ee->d_nodes[d_current]; }

bool EqClassIterator::operator==(const EqClassIterator& i) const
{
  return d_ee == i.d_ee && d_current == i.d_current;
}

bool EqClassIterator::operator!=(const EqClassIterator& i) const
{
  return !(*this == i);
}

EqClassIterator& EqClassIterator::operator++()
{
  Assert(!isFinished());

  Assert(d_start == d_ee->getEqualityNode(d_current).getFind());
  Assert(!d_ee->d_isInternal[d_current]);

  // Find the next one
  do
  {
    d_current = d_ee->getEqualityNode(d_current).getNext();
  } while (d_ee->d_isInternal[d_current]);

  Assert(d_start == d_ee->getEqualityNode(d_current).getFind());
  Assert(!d_ee->d_isInternal[d_current]);

  if (d_current == d_start)
  {
    // we end when we have cycled back to the original representative
    d_current = null_id;
  }
  return *this;
}

EqClassIterator EqClassIterator::operator++(int)
{
  EqClassIterator i = *this;
  ++*this;
  return i;
}

bool EqClassIterator::isFinished() const { return d_current == null_id; }

}  // namespace eq
}  // Namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

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