Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/uf/equality_engine_iterator.cpp	Lines:	47	60	78.3 %
Date:	2021-09-30	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	22	EqClassesIterator::EqClassesIterator() : d_ee(nullptr), d_it(0) {}
25
26	196522	EqClassesIterator::EqClassesIterator(const eq::EqualityEngine* ee) : d_ee(ee)
27		{
28	196522	Assert(d_ee->consistent());
29	196522	d_it = 0;
30		// Go to the first non-internal node that is it's own representative
31	393044	if (d_it < d_ee->d_nodesCount
32	196522	&& (d_ee->d_isInternal[d_it]
33	196522	\|\| d_ee->getEqualityNode(d_it).getFind() != d_it))
34		{
35		++d_it;
36		}
37	196522	}
38
39	5446449	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	5433204	EqClassesIterator& EqClassesIterator::operator++()
52		{
53	5433204	++d_it;
54	54257302	while (d_it < d_ee->d_nodesCount
55	54257302	&& (d_ee->d_isInternal[d_it]
56	25729377	\|\| d_ee->getEqualityNode(d_it).getFind() != d_it))
57		{
58	24412049	++d_it;
59		}
60	5433204	return *this;
61		}
62
63		EqClassesIterator EqClassesIterator::operator++(int)
64		{
65		EqClassesIterator i = *this;
66		++*this;
67		return i;
68		}
69
70	5629441	bool EqClassesIterator::isFinished() const
71		{
72	5629441	return d_it >= d_ee->d_nodesCount;
73		}
74
75	13255	EqClassIterator::EqClassIterator()
76	13255	: d_ee(nullptr), d_start(null_id), d_current(null_id)
77		{
78	13255	}
79
80	4142382	EqClassIterator::EqClassIterator(Node eqc, const eq::EqualityEngine* ee)
81	4142382	: d_ee(ee)
82		{
83	4142382	Assert(d_ee->consistent());
84	4142382	d_current = d_start = d_ee->getNodeId(eqc);
85	4142382	Assert(d_start == d_ee->getEqualityNode(d_start).getFind());
86	4142382	Assert(!d_ee->d_isInternal[d_start]);
87	4142382	}
88
89	21760537	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	21437735	EqClassIterator& EqClassIterator::operator++()
102		{
103	21437735	Assert(!isFinished());
104
105	21437735	Assert(d_start == d_ee->getEqualityNode(d_current).getFind());
106	21437735	Assert(!d_ee->d_isInternal[d_current]);
107
108		// Find the next one
109	236092	do
110		{
111	21673827	d_current = d_ee->getEqualityNode(d_current).getNext();
112	21673827	} while (d_ee->d_isInternal[d_current]);
113
114	21437735	Assert(d_start == d_ee->getEqualityNode(d_current).getFind());
115	21437735	Assert(!d_ee->d_isInternal[d_current]);
116
117	21437735	if (d_current == d_start)
118		{
119		// we end when we have cycled back to the original representative
120	3989573	d_current = null_id;
121		}
122	21437735	return *this;
123		}
124
125	51111	EqClassIterator EqClassIterator::operator++(int)
126		{
127	51111	EqClassIterator i = *this;
128	51111	++*this;
129	51111	return i;
130		}
131
132	46994597	bool EqClassIterator::isFinished() const { return d_current == null_id; }
133
134		} // namespace eq
135		} // Namespace theory
136	22755	} // namespace cvc5