Head

GCC Code Coverage Report

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


/******************************************************************************
 * 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	71	EqClassesIterator::EqClassesIterator() : d_ee(nullptr), d_it(0) {}
25
26	286434	EqClassesIterator::EqClassesIterator(const eq::EqualityEngine* ee) : d_ee(ee)
27		{
28	286434	Assert(d_ee->consistent());
29	286434	d_it = 0;
30		// Go to the first non-internal node that is it's own representative
31	572868	if (d_it < d_ee->d_nodesCount
32	286434	&& (d_ee->d_isInternal[d_it]
33	286434	\|\| d_ee->getEqualityNode(d_it).getFind() != d_it))
34		{
35		++d_it;
36		}
37	286434	}
38
39	6968798	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	6966033	EqClassesIterator& EqClassesIterator::operator++()
52		{
53	6966033	++d_it;
54	50460229	while (d_it < d_ee->d_nodesCount
55	50460229	&& (d_ee->d_isInternal[d_it]
56	24925020	\|\| d_ee->getEqualityNode(d_it).getFind() != d_it))
57		{
58	21747098	++d_it;
59		}
60	6966033	return *this;
61		}
62
63		EqClassesIterator EqClassesIterator::operator++(int)
64		{
65		EqClassesIterator i = *this;
66		++*this;
67		return i;
68		}
69
70	7251869	bool EqClassesIterator::isFinished() const
71		{
72	7251869	return d_it >= d_ee->d_nodesCount;
73		}
74
75	36081	EqClassIterator::EqClassIterator()
76	36081	: d_ee(nullptr), d_start(null_id), d_current(null_id)
77		{
78	36081	}
79
80	4929777	EqClassIterator::EqClassIterator(Node eqc, const eq::EqualityEngine* ee)
81	4929777	: d_ee(ee)
82		{
83	4929777	Assert(d_ee->consistent());
84	4929777	d_current = d_start = d_ee->getNodeId(eqc);
85	4929777	Assert(d_start == d_ee->getEqualityNode(d_start).getFind());
86	4929777	Assert(!d_ee->d_isInternal[d_start]);
87	4929777	}
88
89	16745108	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	16119898	EqClassIterator& EqClassIterator::operator++()
102		{
103	16119898	Assert(!isFinished());
104
105	16119898	Assert(d_start == d_ee->getEqualityNode(d_current).getFind());
106	16119898	Assert(!d_ee->d_isInternal[d_current]);
107
108		// Find the next one
109	65369	do
110		{
111	16185267	d_current = d_ee->getEqualityNode(d_current).getNext();
112	16185267	} while (d_ee->d_isInternal[d_current]);
113
114	16119898	Assert(d_start == d_ee->getEqualityNode(d_current).getFind());
115	16119898	Assert(!d_ee->d_isInternal[d_current]);
116
117	16119898	if (d_current == d_start)
118		{
119		// we end when we have cycled back to the original representative
120	4655395	d_current = null_id;
121		}
122	16119898	return *this;
123		}
124
125	51402	EqClassIterator EqClassIterator::operator++(int)
126		{
127	51402	EqClassIterator i = *this;
128	51402	++*this;
129	51402	return i;
130		}
131
132	37078560	bool EqClassIterator::isFinished() const { return d_current == null_id; }
133
134		} // namespace eq
135		} // Namespace theory
136	28194	} // namespace cvc5