GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/symbol_manager.cpp Lines: 131 136 96.3 %
Date: 2021-03-22 Branches: 116 220 52.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file symbol_manager.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds
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 The symbol manager
13
 **/
14
15
#include "expr/symbol_manager.h"
16
17
#include "context/cdhashmap.h"
18
#include "context/cdhashset.h"
19
#include "context/cdlist.h"
20
#include "context/cdo.h"
21
22
using namespace CVC4::context;
23
24
namespace CVC4 {
25
26
// ---------------------------------------------- SymbolManager::Implementation
27
28
class SymbolManager::Implementation
29
{
30
  using TermStringMap = CDHashMap<api::Term, std::string, api::TermHashFunction>;
31
  using TermSet = CDHashSet<api::Term, api::TermHashFunction>;
32
  using SortList = CDList<api::Sort>;
33
  using TermList = CDList<api::Term>;
34
35
 public:
36
5722
  Implementation()
37
5722
      : d_context(),
38
        d_names(&d_context),
39
        d_namedAsserts(&d_context),
40
        d_declareSorts(&d_context),
41
        d_declareTerms(&d_context),
42
5722
        d_hasPushedScope(&d_context, false)
43
  {
44
    // use an outermost push, to be able to clear all definitions
45
5722
    d_context.push();
46
5722
  }
47
48
5701
  ~Implementation() { d_context.pop(); }
49
  /** set expression name */
50
  bool setExpressionName(api::Term t,
51
                         const std::string& name,
52
                         bool isAssertion = false);
53
  /** get expression name */
54
  bool getExpressionName(api::Term t,
55
                         std::string& name,
56
                         bool isAssertion = false) const;
57
  /** get expression names */
58
  void getExpressionNames(const std::vector<api::Term>& ts,
59
                          std::vector<std::string>& names,
60
                          bool areAssertions = false) const;
61
  /** get expression names */
62
  std::map<api::Term, std::string> getExpressionNames(bool areAssertions) const;
63
  /** get model declare sorts */
64
  std::vector<api::Sort> getModelDeclareSorts() const;
65
  /** get model declare terms */
66
  std::vector<api::Term> getModelDeclareTerms() const;
67
  /** Add declared sort to the list of model declarations. */
68
  void addModelDeclarationSort(api::Sort s);
69
  /** Add declared term to the list of model declarations. */
70
  void addModelDeclarationTerm(api::Term t);
71
  /** reset */
72
  void reset();
73
  /** reset assertions */
74
  void resetAssertions();
75
  /** Push a scope in the expression names. */
76
  void pushScope(bool isUserContext);
77
  /** Pop a scope in the expression names. */
78
  void popScope();
79
  /** Have we pushed a scope (e.g. let or quantifier) in the current context? */
80
  bool hasPushedScope() const;
81
82
 private:
83
  /** The context manager for the scope maps. */
84
  Context d_context;
85
  /** Map terms to names */
86
  TermStringMap d_names;
87
  /** The set of terms with assertion names */
88
  TermSet d_namedAsserts;
89
  /** Declared sorts (for model printing) */
90
  SortList d_declareSorts;
91
  /** Declared terms (for model printing) */
92
  TermList d_declareTerms;
93
  /**
94
   * Have we pushed a scope (e.g. a let or quantifier) in the current context?
95
   */
96
  CDO<bool> d_hasPushedScope;
97
};
98
99
10544
bool SymbolManager::Implementation::setExpressionName(api::Term t,
100
                                                      const std::string& name,
101
                                                      bool isAssertion)
102
{
103
21088
  Trace("sym-manager") << "SymbolManager: set expression name: " << t << " -> "
104
10544
                       << name << ", isAssertion=" << isAssertion << std::endl;
105
  // cannot name subexpressions under quantifiers
106
10544
  PrettyCheckArgument(
107
      !d_hasPushedScope.get(), name, "cannot name function in a scope");
108
10544
  if (isAssertion)
109
  {
110
5921
    d_namedAsserts.insert(t);
111
  }
112
10544
  if (d_names.find(t) != d_names.end())
113
  {
114
    // already named assertion
115
4695
    return false;
116
  }
117
5849
  d_names[t] = name;
118
5849
  return true;
119
}
120
121
31
bool SymbolManager::Implementation::getExpressionName(api::Term t,
122
                                                      std::string& name,
123
                                                      bool isAssertion) const
124
{
125
31
  TermStringMap::const_iterator it = d_names.find(t);
126
31
  if (it == d_names.end())
127
  {
128
4
    return false;
129
  }
130
27
  if (isAssertion)
131
  {
132
    // must be an assertion name
133
27
    if (d_namedAsserts.find(t) == d_namedAsserts.end())
134
    {
135
      return false;
136
    }
137
  }
138
27
  name = (*it).second;
139
27
  return true;
140
}
141
142
7
void SymbolManager::Implementation::getExpressionNames(
143
    const std::vector<api::Term>& ts,
144
    std::vector<std::string>& names,
145
    bool areAssertions) const
146
{
147
38
  for (const api::Term& t : ts)
148
  {
149
62
    std::string name;
150
31
    if (getExpressionName(t, name, areAssertions))
151
    {
152
27
      names.push_back(name);
153
    }
154
  }
155
7
}
156
157
std::map<api::Term, std::string>
158
8
SymbolManager::Implementation::getExpressionNames(bool areAssertions) const
159
{
160
8
  std::map<api::Term, std::string> emap;
161
18
  for (TermStringMap::const_iterator it = d_names.begin(),
162
8
                                     itend = d_names.end();
163
18
       it != itend;
164
       ++it)
165
  {
166
20
    api::Term t = (*it).first;
167
10
    if (areAssertions && d_namedAsserts.find(t) == d_namedAsserts.end())
168
    {
169
      continue;
170
    }
171
10
    emap[t] = (*it).second;
172
  }
173
8
  return emap;
174
}
175
176
25
std::vector<api::Sort> SymbolManager::Implementation::getModelDeclareSorts()
177
    const
178
{
179
  std::vector<api::Sort> declareSorts(d_declareSorts.begin(),
180
25
                                      d_declareSorts.end());
181
25
  return declareSorts;
182
}
183
184
25
std::vector<api::Term> SymbolManager::Implementation::getModelDeclareTerms()
185
    const
186
{
187
  std::vector<api::Term> declareTerms(d_declareTerms.begin(),
188
25
                                      d_declareTerms.end());
189
25
  return declareTerms;
190
}
191
192
3905
void SymbolManager::Implementation::addModelDeclarationSort(api::Sort s)
193
{
194
7810
  Trace("sym-manager") << "SymbolManager: addModelDeclarationSort " << s
195
3905
                       << std::endl;
196
3905
  d_declareSorts.push_back(s);
197
3905
}
198
199
166565
void SymbolManager::Implementation::addModelDeclarationTerm(api::Term t)
200
{
201
333130
  Trace("sym-manager") << "SymbolManager: addModelDeclarationTerm " << t
202
166565
                       << std::endl;
203
166565
  d_declareTerms.push_back(t);
204
166565
}
205
206
102296
void SymbolManager::Implementation::pushScope(bool isUserContext)
207
{
208
204592
  Trace("sym-manager") << "SymbolManager: pushScope, isUserContext = "
209
102296
                       << isUserContext << std::endl;
210
102296
  PrettyCheckArgument(!d_hasPushedScope.get() || !isUserContext,
211
                      "cannot push a user context within a scope context");
212
102296
  d_context.push();
213
102296
  if (!isUserContext)
214
  {
215
99854
    d_hasPushedScope = true;
216
  }
217
102296
}
218
219
101856
void SymbolManager::Implementation::popScope()
220
{
221
101856
  Trace("sym-manager") << "SymbolManager: popScope" << std::endl;
222
101856
  if (d_context.getLevel() == 0)
223
  {
224
    throw ScopeException();
225
  }
226
101856
  d_context.pop();
227
203712
  Trace("sym-manager-debug")
228
101856
      << "d_hasPushedScope is now " << d_hasPushedScope.get() << std::endl;
229
101856
}
230
231
26
bool SymbolManager::Implementation::hasPushedScope() const
232
{
233
26
  return d_hasPushedScope.get();
234
}
235
236
47
void SymbolManager::Implementation::reset()
237
{
238
47
  Trace("sym-manager") << "SymbolManager: reset" << std::endl;
239
  // clear names by popping to context level 0
240
141
  while (d_context.getLevel() > 0)
241
  {
242
47
    d_context.pop();
243
  }
244
  // push the outermost context
245
47
  d_context.push();
246
47
}
247
248
31
void SymbolManager::Implementation::resetAssertions()
249
{
250
31
  Trace("sym-manager") << "SymbolManager: resetAssertions" << std::endl;
251
  // clear names by popping to context level 1
252
43
  while (d_context.getLevel() > 1)
253
  {
254
6
    d_context.pop();
255
  }
256
31
}
257
258
// ---------------------------------------------- SymbolManager
259
260
5722
SymbolManager::SymbolManager(api::Solver* s)
261
    : d_solver(s),
262
5722
      d_implementation(new SymbolManager::Implementation()),
263
11444
      d_globalDeclarations(false)
264
{
265
5722
}
266
267
5701
SymbolManager::~SymbolManager() {}
268
269
5722
SymbolTable* SymbolManager::getSymbolTable() { return &d_symtabAllocated; }
270
271
10544
bool SymbolManager::setExpressionName(api::Term t,
272
                                      const std::string& name,
273
                                      bool isAssertion)
274
{
275
10544
  return d_implementation->setExpressionName(t, name, isAssertion);
276
}
277
278
bool SymbolManager::getExpressionName(api::Term t,
279
                                      std::string& name,
280
                                      bool isAssertion) const
281
{
282
  return d_implementation->getExpressionName(t, name, isAssertion);
283
}
284
285
7
void SymbolManager::getExpressionNames(const std::vector<api::Term>& ts,
286
                                       std::vector<std::string>& names,
287
                                       bool areAssertions) const
288
{
289
7
  return d_implementation->getExpressionNames(ts, names, areAssertions);
290
}
291
292
8
std::map<api::Term, std::string> SymbolManager::getExpressionNames(
293
    bool areAssertions) const
294
{
295
8
  return d_implementation->getExpressionNames(areAssertions);
296
}
297
25
std::vector<api::Sort> SymbolManager::getModelDeclareSorts() const
298
{
299
25
  return d_implementation->getModelDeclareSorts();
300
}
301
25
std::vector<api::Term> SymbolManager::getModelDeclareTerms() const
302
{
303
25
  return d_implementation->getModelDeclareTerms();
304
}
305
306
3905
void SymbolManager::addModelDeclarationSort(api::Sort s)
307
{
308
3905
  d_implementation->addModelDeclarationSort(s);
309
3905
}
310
311
166565
void SymbolManager::addModelDeclarationTerm(api::Term t)
312
{
313
166565
  d_implementation->addModelDeclarationTerm(t);
314
166565
}
315
316
2115
size_t SymbolManager::scopeLevel() const
317
{
318
2115
  return d_symtabAllocated.getLevel();
319
}
320
321
102302
void SymbolManager::pushScope(bool isUserContext)
322
{
323
  // we do not push user contexts when global declarations is true. This
324
  // policy applies both to the symbol table and to the symbol manager.
325
102302
  if (d_globalDeclarations && isUserContext)
326
  {
327
6
    return;
328
  }
329
102296
  d_implementation->pushScope(isUserContext);
330
102296
  d_symtabAllocated.pushScope();
331
}
332
333
101860
void SymbolManager::popScope()
334
{
335
  // If global declarations is true, then if d_hasPushedScope is false, then
336
  // the pop corresponds to a user context, which we did not push. Note this
337
  // additionally relies on the fact that user contexts cannot be pushed
338
  // within scope contexts. Hence, since we did not push the context, we
339
  // do not pop a context here.
340
101860
  if (d_globalDeclarations && !d_implementation->hasPushedScope())
341
  {
342
4
    return;
343
  }
344
101856
  d_symtabAllocated.popScope();
345
101856
  d_implementation->popScope();
346
}
347
348
16
void SymbolManager::setGlobalDeclarations(bool flag)
349
{
350
16
  d_globalDeclarations = flag;
351
16
}
352
353
177214
bool SymbolManager::getGlobalDeclarations() const
354
{
355
177214
  return d_globalDeclarations;
356
}
357
358
47
void SymbolManager::reset()
359
{
360
47
  d_symtabAllocated.reset();
361
47
  d_implementation->reset();
362
47
}
363
364
31
void SymbolManager::resetAssertions()
365
{
366
31
  d_implementation->resetAssertions();
367
31
  d_symtabAllocated.resetAssertions();
368
31
}
369
370
26676
}  // namespace CVC4