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