GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/term_registration_visitor.cpp Lines: 109 136 80.1 %
Date: 2021-03-23 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
5653051
bool isAlreadyVisited(TheoryIdSet visitedTheories, TNode current, TNode parent)
44
{
45
5653051
  TheoryId currentTheoryId = Theory::theoryOf(current);
46
5653051
  if (!TheoryIdSetUtil::setContains(currentTheoryId, visitedTheories))
47
  {
48
    // current theory not visited, return false
49
    return false;
50
  }
51
52
5653051
  if (current == parent)
53
  {
54
    // top-level and current visited, return true
55
839454
    return true;
56
  }
57
58
  // The current theory has already visited it, so now it depends on the parent
59
  // and the type
60
4813597
  TheoryId parentTheoryId = Theory::theoryOf(parent);
61
4813597
  if (!TheoryIdSetUtil::setContains(parentTheoryId, visitedTheories))
62
  {
63
    // parent theory not visited, return false
64
95953
    return false;
65
  }
66
67
  // do we need to consider the type?
68
9435288
  TypeNode type = current.getType();
69
4717644
  if (currentTheoryId == parentTheoryId && !type.isInterpretedFinite())
70
  {
71
    // current and parent are the same theory, and we are infinite, return true
72
2788335
    return true;
73
  }
74
1929309
  TheoryId typeTheoryId = Theory::theoryOf(type);
75
1929309
  return TheoryIdSetUtil::setContains(typeTheoryId, visitedTheories);
76
}
77
78
1204263
bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) {
79
80
1204263
  Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl;
81
82
2408526
  if ((parent.isClosure()
83
1199637
       || parent.getKind() == kind::SEP_STAR
84
1199637
       || parent.getKind() == kind::SEP_WAND
85
2403900
       || (parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean())
86
       // parent.getKind() == kind::CARDINALITY_CONSTRAINT
87
       )
88
2413152
      && 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
1202397
  TNodeToTheorySetMap::iterator find = d_visited.find(current);
96
1202397
  if (find == d_visited.end()) {
97
    // not visited at all, return false
98
651831
    return false;
99
  }
100
101
550566
  TheoryIdSet visitedTheories = (*find).second;
102
550566
  return isAlreadyVisited(visitedTheories, current, parent);
103
}
104
105
258641
void PreRegisterVisitor::visit(TNode current, TNode parent) {
106
107
258641
  Debug("register") << "PreRegisterVisitor::visit(" << current << "," << parent << ")" << std::endl;
108
258641
  if (Debug.isOn("register::internal")) {
109
    Debug("register::internal") << toString() << std::endl;
110
  }
111
112
  // get the theories we already preregistered with
113
258641
  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
258642
  preRegister(d_engine, visitedTheories, current, parent, visitedTheories);
119
120
517280
  Debug("register::internal")
121
258640
      << "PreRegisterVisitor::visit(" << current << "," << parent
122
258640
      << "): now registered with "
123
258640
      << TheoryIdSetUtil::setToString(visitedTheories) << std::endl;
124
  // update the theories set for current
125
258640
  d_visited[current] = visitedTheories;
126
258640
  Assert(d_visited.find(current) != d_visited.end());
127
258640
  Assert(alreadyVisited(current, parent));
128
258640
}
129
130
4553003
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
4553003
  TheoryId currentTheoryId = Theory::theoryOf(current);
138
4553007
  preRegisterWithTheory(
139
      te, visitedTheories, currentTheoryId, current, parent, preregTheories);
140
141
4552999
  if (current != parent)
142
  {
143
    // preregister with parent theory, if necessary
144
3713655
    TheoryId parentTheoryId = Theory::theoryOf(parent);
145
3713655
    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
7427310
    TypeNode type = current.getType();
151
3713655
    if (currentTheoryId != parentTheoryId || type.isInterpretedFinite())
152
    {
153
      // preregister with the type's theory, if necessary
154
1382238
      TheoryId typeTheoryId = Theory::theoryOf(type);
155
1382238
      preRegisterWithTheory(
156
          te, visitedTheories, typeTheoryId, current, parent, preregTheories);
157
    }
158
  }
159
4552999
}
160
9648896
void PreRegisterVisitor::preRegisterWithTheory(TheoryEngine* te,
161
                                               TheoryIdSet& visitedTheories,
162
                                               TheoryId id,
163
                                               TNode current,
164
                                               TNode parent,
165
                                               TheoryIdSet preregTheories)
166
{
167
9648896
  if (TheoryIdSetUtil::setContains(id, visitedTheories))
168
  {
169
    // already visited
170
4093024
    return;
171
  }
172
5555872
  visitedTheories = TheoryIdSetUtil::setInsert(id, visitedTheories);
173
5555872
  if (TheoryIdSetUtil::setContains(id, preregTheories))
174
  {
175
    // already pregregistered
176
3899050
    return;
177
  }
178
1656822
  if (Configuration::isAssertionBuild())
179
  {
180
3313644
    Debug("register::internal")
181
1656822
        << "PreRegisterVisitor::visit(" << current << "," << parent
182
1656822
        << "): 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
1656822
    if (!options::finiteModelFind())
189
    {
190
1580198
      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
1656822
  Theory* th = te->theoryOf(id);
208
1656826
  th->preRegisterTerm(current);
209
}
210
211
124857
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
17490586
bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const {
224
225
17490586
  Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl;
226
227
34981172
  if ((parent.isClosure()
228
17351609
       || parent.getKind() == kind::SEP_STAR
229
17350944
       || parent.getKind() == kind::SEP_WAND
230
34841431
       || (parent.getKind() == kind::SEP_LABEL && current.getType().isBoolean())
231
       // parent.getKind() == kind::CARDINALITY_CONSTRAINT
232
       )
233
35122949
      && current != parent)
234
  {
235
59408
    Debug("register::internal") << "quantifier:true" << std::endl;
236
59408
    return true;
237
  }
238
17431178
  TNodeVisitedMap::const_iterator find = d_visited.find(current);
239
  // If node is not visited at all, just return false
240
17431178
  if (find == d_visited.end()) {
241
12328693
    Debug("register::internal") << "1:false" << std::endl;
242
12328693
    return false;
243
  }
244
245
5102485
  TheoryIdSet visitedTheories = (*find).second;
246
5102485
  return isAlreadyVisited(visitedTheories, current, parent);
247
}
248
249
4294362
void SharedTermsVisitor::visit(TNode current, TNode parent) {
250
251
4294362
  Debug("register") << "SharedTermsVisitor::visit(" << current << "," << parent << ")" << std::endl;
252
4294362
  if (Debug.isOn("register::internal")) {
253
    Debug("register::internal") << toString() << std::endl;
254
  }
255
4294362
  TheoryIdSet visitedTheories = d_visited[current];
256
4294362
  TheoryIdSet preregTheories = d_preregistered[current];
257
258
  // preregister the term with the current, parent or type theories, as needed
259
4294365
  PreRegisterVisitor::preRegister(
260
      d_engine, visitedTheories, current, parent, preregTheories);
261
262
  // Record the new theories that we visited
263
4294359
  d_visited[current] = visitedTheories;
264
265
  // add visited theories to those who have preregistered
266
4294359
  d_preregistered[current] =
267
8588718
      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
4294359
  TheoryId currentTheoryId = Theory::theoryOf(current);
271
8588718
  if (TheoryIdSetUtil::setDifference(
272
4294359
          visitedTheories, TheoryIdSetUtil::setInsert(currentTheoryId)))
273
  {
274
1015906
    d_sharedTerms.addSharedTerm(d_atom, current, visitedTheories);
275
  }
276
277
4294359
  Assert(d_visited.find(current) != d_visited.end());
278
4294359
  Assert(alreadyVisited(current, parent));
279
4294359
}
280
281
714601
void SharedTermsVisitor::start(TNode node) {
282
714601
  d_visited.clear();
283
714601
  d_atom = node;
284
714601
}
285
286
714598
void SharedTermsVisitor::done(TNode node) {
287
714598
  clear();
288
714598
}
289
290
714598
void SharedTermsVisitor::clear() {
291
714598
  d_atom = TNode();
292
714598
  d_visited.clear();
293
714598
}
294
295
26685
}  // namespace CVC4