GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/term_registration_visitor.cpp Lines: 109 136 80.1 %
Date: 2021-03-22 Branches: 226 554 40.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file term_registration_visitor.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Dejan Jovanovic, Morgan Deters
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
 ** [[ Add lengthier description here ]]
13
 ** \todo document this file
14
 **/
15
16
#include "theory/term_registration_visitor.h"
17
18
#include "base/configuration.h"
19
#include "options/quantifiers_options.h"
20
#include "smt/logic_exception.h"
21
#include "theory/theory_engine.h"
22
23
using namespace CVC4::theory;
24
25
namespace CVC4 {
26
27
std::string PreRegisterVisitor::toString() const {
28
  std::stringstream ss;
29
  TNodeToTheorySetMap::const_iterator it = d_visited.begin();
30
  for (; it != d_visited.end(); ++ it) {
31
    ss << (*it).first << ": " << TheoryIdSetUtil::setToString((*it).second)
32
       << std::endl;
33
  }
34
  return ss.str();
35
}
36
37
/**
38
 * Return true if we already visited the term current with the given parent,
39
 * assuming that the set of theories in visitedTheories has already processed
40
 * current. This method is used by PreRegisterVisitor and SharedTermsVisitor
41
 * below.
42
 */
43
5651427
bool isAlreadyVisited(TheoryIdSet visitedTheories, TNode current, TNode parent)
44
{
45
5651427
  TheoryId currentTheoryId = Theory::theoryOf(current);
46
5651427
  if (!TheoryIdSetUtil::setContains(currentTheoryId, visitedTheories))
47
  {
48
    // current theory not visited, return false
49
    return false;
50
  }
51
52
5651427
  if (current == parent)
53
  {
54
    // top-level and current visited, return true
55
839132
    return true;
56
  }
57
58
  // The current theory has already visited it, so now it depends on the parent
59
  // and the type
60
4812295
  TheoryId parentTheoryId = Theory::theoryOf(parent);
61
4812295
  if (!TheoryIdSetUtil::setContains(parentTheoryId, visitedTheories))
62
  {
63
    // parent theory not visited, return false
64
95875
    return false;
65
  }
66
67
  // do we need to consider the type?
68
9432840
  TypeNode type = current.getType();
69
4716420
  if (currentTheoryId == parentTheoryId && !type.isInterpretedFinite())
70
  {
71
    // current and parent are the same theory, and we are infinite, return true
72
2787419
    return true;
73
  }
74
1929001
  TheoryId typeTheoryId = Theory::theoryOf(type);
75
1929001
  return TheoryIdSetUtil::setContains(typeTheoryId, visitedTheories);
76
}
77
78
1203247
bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) {
79
80
1203247
  Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl;
81
82
2406494
  if ((parent.isClosure()
83
1198621
       || parent.getKind() == kind::SEP_STAR
84
1198621
       || parent.getKind() == kind::SEP_WAND
85
2401868
       || (parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean())
86
       // parent.getKind() == kind::CARDINALITY_CONSTRAINT
87
       )
88
2411120
      && current != parent)
89
  {
90
1866
    Debug("register::internal") << "quantifier:true" << std::endl;
91
1866
    return true;
92
  }
93
94
  // Get the theories that have already visited this node
95
1201381
  TNodeToTheorySetMap::iterator find = d_visited.find(current);
96
1201381
  if (find == d_visited.end()) {
97
    // not visited at all, return false
98
651303
    return false;
99
  }
100
101
550078
  TheoryIdSet visitedTheories = (*find).second;
102
550078
  return isAlreadyVisited(visitedTheories, current, parent);
103
}
104
105
258425
void PreRegisterVisitor::visit(TNode current, TNode parent) {
106
107
258425
  Debug("register") << "PreRegisterVisitor::visit(" << current << "," << parent << ")" << std::endl;
108
258425
  if (Debug.isOn("register::internal")) {
109
    Debug("register::internal") << toString() << std::endl;
110
  }
111
112
  // get the theories we already preregistered with
113
258425
  TheoryIdSet visitedTheories = d_visited[current];
114
115
  // call the preregistration on current, parent or type theories and update
116
  // visitedTheories. The set of preregistering theories coincides with
117
  // visitedTheories here.
118
258426
  preRegister(d_engine, visitedTheories, current, parent, visitedTheories);
119
120
516848
  Debug("register::internal")
121
258424
      << "PreRegisterVisitor::visit(" << current << "," << parent
122
258424
      << "): now registered with "
123
258424
      << TheoryIdSetUtil::setToString(visitedTheories) << std::endl;
124
  // update the theories set for current
125
258424
  d_visited[current] = visitedTheories;
126
258424
  Assert(d_visited.find(current) != d_visited.end());
127
258424
  Assert(alreadyVisited(current, parent));
128
258424
}
129
130
4551731
void PreRegisterVisitor::preRegister(TheoryEngine* te,
131
                                     TheoryIdSet& visitedTheories,
132
                                     TNode current,
133
                                     TNode parent,
134
                                     TheoryIdSet preregTheories)
135
{
136
  // Preregister with the current theory, if necessary
137
4551731
  TheoryId currentTheoryId = Theory::theoryOf(current);
138
4551735
  preRegisterWithTheory(
139
      te, visitedTheories, currentTheoryId, current, parent, preregTheories);
140
141
4551727
  if (current != parent)
142
  {
143
    // preregister with parent theory, if necessary
144
3712705
    TheoryId parentTheoryId = Theory::theoryOf(parent);
145
3712705
    preRegisterWithTheory(
146
        te, visitedTheories, parentTheoryId, current, parent, preregTheories);
147
148
    // Note that if enclosed by different theories it's shared, for example,
149
    // in read(a, f(a)), f(a) should be shared with integers.
150
7425410
    TypeNode type = current.getType();
151
3712705
    if (currentTheoryId != parentTheoryId || type.isInterpretedFinite())
152
    {
153
      // preregister with the type's theory, if necessary
154
1381930
      TheoryId typeTheoryId = Theory::theoryOf(type);
155
1381930
      preRegisterWithTheory(
156
          te, visitedTheories, typeTheoryId, current, parent, preregTheories);
157
    }
158
  }
159
4551727
}
160
9646366
void PreRegisterVisitor::preRegisterWithTheory(TheoryEngine* te,
161
                                               TheoryIdSet& visitedTheories,
162
                                               TheoryId id,
163
                                               TNode current,
164
                                               TNode parent,
165
                                               TheoryIdSet preregTheories)
166
{
167
9646366
  if (TheoryIdSetUtil::setContains(id, visitedTheories))
168
  {
169
    // already visited
170
4092052
    return;
171
  }
172
5554314
  visitedTheories = TheoryIdSetUtil::setInsert(id, visitedTheories);
173
5554314
  if (TheoryIdSetUtil::setContains(id, preregTheories))
174
  {
175
    // already pregregistered
176
3898067
    return;
177
  }
178
1656247
  if (Configuration::isAssertionBuild())
179
  {
180
3312494
    Debug("register::internal")
181
1656247
        << "PreRegisterVisitor::visit(" << current << "," << parent
182
1656247
        << "): adding " << id << std::endl;
183
    // This should never throw an exception, since theories should be
184
    // guaranteed to be initialized.
185
    // These checks don't work with finite model finding, because it
186
    // uses Rational constants to represent cardinality constraints,
187
    // even though arithmetic isn't actually involved.
188
1656247
    if (!options::finiteModelFind())
189
    {
190
1579623
      if (!te->isTheoryEnabled(id))
191
      {
192
        const LogicInfo& l = te->getLogicInfo();
193
        LogicInfo newLogicInfo = l.getUnlockedCopy();
194
        newLogicInfo.enableTheory(id);
195
        newLogicInfo.lock();
196
        std::stringstream ss;
197
        ss << "The logic was specified as " << l.getLogicString()
198
           << ", which doesn't include " << id
199
           << ", but found a term in that theory." << std::endl
200
           << "You might want to extend your logic to "
201
           << newLogicInfo.getLogicString() << std::endl;
202
        throw LogicException(ss.str());
203
      }
204
    }
205
  }
206
  // call the theory's preRegisterTerm method
207
1656247
  Theory* th = te->theoryOf(id);
208
1656251
  th->preRegisterTerm(current);
209
}
210
211
124737
void PreRegisterVisitor::start(TNode node) {}
212
213
std::string SharedTermsVisitor::toString() const {
214
  std::stringstream ss;
215
  TNodeVisitedMap::const_iterator it = d_visited.begin();
216
  for (; it != d_visited.end(); ++ it) {
217
    ss << (*it).first << ": " << TheoryIdSetUtil::setToString((*it).second)
218
       << std::endl;
219
  }
220
  return ss.str();
221
}
222
223
17486550
bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const {
224
225
17486550
  Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl;
226
227
34973100
  if ((parent.isClosure()
228
17347597
       || parent.getKind() == kind::SEP_STAR
229
17346932
       || parent.getKind() == kind::SEP_WAND
230
34833383
       || (parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean())
231
       // parent.getKind() == kind::CARDINALITY_CONSTRAINT
232
       )
233
35114853
      && current != parent)
234
  {
235
59396
    Debug("register::internal") << "quantifier:true" << std::endl;
236
59396
    return true;
237
  }
238
17427154
  TNodeVisitedMap::const_iterator find = d_visited.find(current);
239
  // If node is not visited at all, just return false
240
17427154
  if (find == d_visited.end()) {
241
12325805
    Debug("register::internal") << "1:false" << std::endl;
242
12325805
    return false;
243
  }
244
245
5101349
  TheoryIdSet visitedTheories = (*find).second;
246
5101349
  return isAlreadyVisited(visitedTheories, current, parent);
247
}
248
249
4293306
void SharedTermsVisitor::visit(TNode current, TNode parent) {
250
251
4293306
  Debug("register") << "SharedTermsVisitor::visit(" << current << "," << parent << ")" << std::endl;
252
4293306
  if (Debug.isOn("register::internal")) {
253
    Debug("register::internal") << toString() << std::endl;
254
  }
255
4293306
  TheoryIdSet visitedTheories = d_visited[current];
256
4293306
  TheoryIdSet preregTheories = d_preregistered[current];
257
258
  // preregister the term with the current, parent or type theories, as needed
259
4293309
  PreRegisterVisitor::preRegister(
260
      d_engine, visitedTheories, current, parent, preregTheories);
261
262
  // Record the new theories that we visited
263
4293303
  d_visited[current] = visitedTheories;
264
265
  // add visited theories to those who have preregistered
266
4293303
  d_preregistered[current] =
267
8586606
      TheoryIdSetUtil::setUnion(preregTheories, visitedTheories);
268
269
  // If there is more than two theories and a new one has been added notify the shared terms database
270
4293303
  TheoryId currentTheoryId = Theory::theoryOf(current);
271
8586606
  if (TheoryIdSetUtil::setDifference(
272
4293303
          visitedTheories, TheoryIdSetUtil::setInsert(currentTheoryId)))
273
  {
274
1015598
    d_sharedTerms.addSharedTerm(d_atom, current, visitedTheories);
275
  }
276
277
4293303
  Assert(d_visited.find(current) != d_visited.end());
278
4293303
  Assert(alreadyVisited(current, parent));
279
4293303
}
280
281
714399
void SharedTermsVisitor::start(TNode node) {
282
714399
  d_visited.clear();
283
714399
  d_atom = node;
284
714399
}
285
286
714396
void SharedTermsVisitor::done(TNode node) {
287
714396
  clear();
288
714396
}
289
290
714396
void SharedTermsVisitor::clear() {
291
714396
  d_atom = TNode();
292
714396
  d_visited.clear();
293
714396
}
294
295
26676
}  // namespace CVC4