Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/type_set.cpp	Lines:	57	59	96.6 %
Date:	2021-05-22	Branches:	60	104	57.7 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Clark Barrett, Aina Niemetz
 *
 * 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 type set class.
 */
#include "theory/type_set.h"

using namespace std;
using namespace cvc5::kind;

namespace cvc5 {
namespace theory {

TypeSet::~TypeSet()
{
  iterator it;
  for (it = d_typeSet.begin(); it != d_typeSet.end(); ++it)
  {
    delete (*it).second;
  }
  TypeToTypeEnumMap::iterator it2;
  for (it2 = d_teMap.begin(); it2 != d_teMap.end(); ++it2)
  {
    delete (*it2).second;
  }
}

void TypeSet::setTypeEnumeratorProperties(TypeEnumeratorProperties* tep)
{
  d_tep = tep;
}

void TypeSet::add(TypeNode t, TNode n)
{
  iterator it = d_typeSet.find(t);
  std::set<Node>* s;
  if (it == d_typeSet.end())
  {
    s = new std::set<Node>;
    d_typeSet[t] = s;
  }
  else
  {
    s = (*it).second;
  }
  s->insert(n);
}

std::set<Node>* TypeSet::getSet(TypeNode t) const
{
  const_iterator it = d_typeSet.find(t);
  if (it == d_typeSet.end())
  {
    return NULL;
  }
  return (*it).second;
}

Node TypeSet::nextTypeEnum(TypeNode t, bool useBaseType)
{
  TypeEnumerator* te;
  TypeToTypeEnumMap::iterator it = d_teMap.find(t);
  if (it == d_teMap.end())
  {
    te = new TypeEnumerator(t, d_tep);
    d_teMap[t] = te;
  }
  else
  {
    te = (*it).second;
  }
  if (te->isFinished())
  {
    return Node();
  }

  if (useBaseType)
  {
    t = t.getBaseType();
  }
  iterator itSet = d_typeSet.find(t);
  std::set<Node>* s;
  if (itSet == d_typeSet.end())
  {
    s = new std::set<Node>;
    d_typeSet[t] = s;
  }
  else
  {
    s = (*itSet).second;
  }
  Node n = **te;
  while (s->find(n) != s->end())
  {
    ++(*te);
    if (te->isFinished())
    {
      return Node();
    }
    n = **te;
  }
  s->insert(n);
  // add all subterms of n to this set as well
  // this is necessary for parametric types whose values are constructed from
  // other types to ensure that we do not enumerate subterms of other
  // previously enumerated values
  std::unordered_set<TNode> visited;
  addSubTerms(n, visited);
  ++(*te);
  return n;
}

void TypeSet::addSubTerms(TNode n,
                          std::unordered_set<TNode>& visited,
                          bool topLevel)
{
  if (visited.find(n) == visited.end())
  {
    visited.insert(n);
    if (!topLevel)
    {
      add(n.getType(), n);
    }
    for (unsigned i = 0; i < n.getNumChildren(); i++)
    {
      addSubTerms(n[i], visited, false);
    }
  }
}

}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Clark Barrett, Aina Niemetz
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 type set class.
14		*/
15		#include "theory/type_set.h"
16
17		using namespace std;
18		using namespace cvc5::kind;
19
20		namespace cvc5 {
21		namespace theory {
22
23	101236	TypeSet::~TypeSet()
24		{
25	50618	iterator it;
26	130848	for (it = d_typeSet.begin(); it != d_typeSet.end(); ++it)
27		{
28	80230	delete (*it).second;
29		}
30	50618	TypeToTypeEnumMap::iterator it2;
31	55468	for (it2 = d_teMap.begin(); it2 != d_teMap.end(); ++it2)
32		{
33	4850	delete (*it2).second;
34		}
35	50618	}
36
37	1015	void TypeSet::setTypeEnumeratorProperties(TypeEnumeratorProperties* tep)
38		{
39	1015	d_tep = tep;
40	1015	}
41
42	903320	void TypeSet::add(TypeNode t, TNode n)
43		{
44	903320	iterator it = d_typeSet.find(t);
45		std::set<Node>* s;
46	903320	if (it == d_typeSet.end())
47		{
48	77200	s = new std::set<Node>;
49	77200	d_typeSet[t] = s;
50		}
51		else
52		{
53	826120	s = (*it).second;
54		}
55	903320	s->insert(n);
56	903320	}
57
58	626186	std::set<Node>* TypeSet::getSet(TypeNode t) const
59		{
60	626186	const_iterator it = d_typeSet.find(t);
61	626186	if (it == d_typeSet.end())
62		{
63	254384	return NULL;
64		}
65	371802	return (*it).second;
66		}
67
68	23080	Node TypeSet::nextTypeEnum(TypeNode t, bool useBaseType)
69		{
70		TypeEnumerator* te;
71	23080	TypeToTypeEnumMap::iterator it = d_teMap.find(t);
72	23080	if (it == d_teMap.end())
73		{
74	4850	te = new TypeEnumerator(t, d_tep);
75	4850	d_teMap[t] = te;
76		}
77		else
78		{
79	18230	te = (*it).second;
80		}
81	23080	if (te->isFinished())
82		{
83		return Node();
84		}
85
86	23080	if (useBaseType)
87		{
88	22673	t = t.getBaseType();
89		}
90	23080	iterator itSet = d_typeSet.find(t);
91		std::set<Node>* s;
92	23080	if (itSet == d_typeSet.end())
93		{
94	3030	s = new std::set<Node>;
95	3030	d_typeSet[t] = s;
96		}
97		else
98		{
99	20050	s = (*itSet).second;
100		}
101	46160	Node n = **te;
102	34924	while (s->find(n) != s->end())
103		{
104	5922	++(*te);
105	5922	if (te->isFinished())
106		{
107		return Node();
108		}
109	5922	n = **te;
110		}
111	23080	s->insert(n);
112		// add all subterms of n to this set as well
113		// this is necessary for parametric types whose values are constructed from
114		// other types to ensure that we do not enumerate subterms of other
115		// previously enumerated values
116	46160	std::unordered_set<TNode> visited;
117	23080	addSubTerms(n, visited);
118	23080	++(*te);
119	23080	return n;
120		}
121
122	99740	void TypeSet::addSubTerms(TNode n,
123		std::unordered_set<TNode>& visited,
124		bool topLevel)
125		{
126	99740	if (visited.find(n) == visited.end())
127		{
128	75763	visited.insert(n);
129	75763	if (!topLevel)
130		{
131	52683	add(n.getType(), n);
132		}
133	152423	for (unsigned i = 0; i < n.getNumChildren(); i++)
134		{
135	76660	addSubTerms(n[i], visited, false);
136		}
137		}
138	99740	}
139
140		} // namespace theory
141	28194	} // namespace cvc5