GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/type_set.cpp Lines: 57 59 96.6 %
Date: 2021-03-23 Branches: 60 104 57.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file type_set.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Clark Barrett
6
 ** This file is part of the CVC4 project.
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.\endverbatim
11
 **
12
 ** \brief Implementation of type set class
13
 **/
14
#include "theory/type_set.h"
15
16
using namespace std;
17
using namespace CVC4::kind;
18
19
namespace CVC4 {
20
namespace theory {
21
22
123510
TypeSet::~TypeSet()
23
{
24
61755
  iterator it;
25
168634
  for (it = d_typeSet.begin(); it != d_typeSet.end(); ++it)
26
  {
27
106879
    delete (*it).second;
28
  }
29
61755
  TypeToTypeEnumMap::iterator it2;
30
66947
  for (it2 = d_teMap.begin(); it2 != d_teMap.end(); ++it2)
31
  {
32
5192
    delete (*it2).second;
33
  }
34
61755
}
35
36
941
void TypeSet::setTypeEnumeratorProperties(TypeEnumeratorProperties* tep)
37
{
38
941
  d_tep = tep;
39
941
}
40
41
1025954
void TypeSet::add(TypeNode t, TNode n)
42
{
43
1025954
  iterator it = d_typeSet.find(t);
44
  std::set<Node>* s;
45
1025954
  if (it == d_typeSet.end())
46
  {
47
103756
    s = new std::set<Node>;
48
103756
    d_typeSet[t] = s;
49
  }
50
  else
51
  {
52
922198
    s = (*it).second;
53
  }
54
1025954
  s->insert(n);
55
1025954
}
56
57
687224
std::set<Node>* TypeSet::getSet(TypeNode t) const
58
{
59
687224
  const_iterator it = d_typeSet.find(t);
60
687224
  if (it == d_typeSet.end())
61
  {
62
292910
    return NULL;
63
  }
64
394314
  return (*it).second;
65
}
66
67
23902
Node TypeSet::nextTypeEnum(TypeNode t, bool useBaseType)
68
{
69
  TypeEnumerator* te;
70
23902
  TypeToTypeEnumMap::iterator it = d_teMap.find(t);
71
23902
  if (it == d_teMap.end())
72
  {
73
5192
    te = new TypeEnumerator(t, d_tep);
74
5192
    d_teMap[t] = te;
75
  }
76
  else
77
  {
78
18710
    te = (*it).second;
79
  }
80
23902
  if (te->isFinished())
81
  {
82
    return Node();
83
  }
84
85
23902
  if (useBaseType)
86
  {
87
23493
    t = t.getBaseType();
88
  }
89
23902
  iterator itSet = d_typeSet.find(t);
90
  std::set<Node>* s;
91
23902
  if (itSet == d_typeSet.end())
92
  {
93
3123
    s = new std::set<Node>;
94
3123
    d_typeSet[t] = s;
95
  }
96
  else
97
  {
98
20779
    s = (*itSet).second;
99
  }
100
47804
  Node n = **te;
101
37854
  while (s->find(n) != s->end())
102
  {
103
6976
    ++(*te);
104
6976
    if (te->isFinished())
105
    {
106
      return Node();
107
    }
108
6976
    n = **te;
109
  }
110
23902
  s->insert(n);
111
  // add all subterms of n to this set as well
112
  // this is necessary for parametric types whose values are constructed from
113
  // other types to ensure that we do not enumerate subterms of other
114
  // previously enumerated values
115
47804
  std::unordered_set<TNode, TNodeHashFunction> visited;
116
23902
  addSubTerms(n, visited);
117
23902
  ++(*te);
118
23902
  return n;
119
}
120
121
101297
void TypeSet::addSubTerms(TNode n,
122
                          std::unordered_set<TNode, TNodeHashFunction>& visited,
123
                          bool topLevel)
124
{
125
101297
  if (visited.find(n) == visited.end())
126
  {
127
77250
    visited.insert(n);
128
77250
    if (!topLevel)
129
    {
130
53348
      add(n.getType(), n);
131
    }
132
154645
    for (unsigned i = 0; i < n.getNumChildren(); i++)
133
    {
134
77395
      addSubTerms(n[i], visited, false);
135
    }
136
  }
137
101297
}
138
139
} /* namespace CVC4::theory */
140
26685
} /* namespace CVC4 */