GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/symbol_table.cpp Lines: 194 231 84.0 %
Date: 2021-03-22 Branches: 188 492 38.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file symbol_table.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Tim King, 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
 ** \brief Convenience class for scoping variable and type
13
 ** declarations (implementation)
14
 **
15
 ** Convenience class for scoping variable and type declarations
16
 ** (implementation).
17
 **/
18
19
#include "expr/symbol_table.h"
20
21
#include <ostream>
22
#include <string>
23
#include <unordered_map>
24
#include <utility>
25
26
#include "api/cvc4cpp.h"
27
#include "context/cdhashmap.h"
28
#include "context/cdhashset.h"
29
#include "context/context.h"
30
31
namespace CVC4 {
32
33
using ::CVC4::context::CDHashMap;
34
using ::CVC4::context::CDHashSet;
35
using ::CVC4::context::Context;
36
using ::std::copy;
37
using ::std::endl;
38
using ::std::ostream_iterator;
39
using ::std::pair;
40
using ::std::string;
41
using ::std::vector;
42
43
/** Overloaded type trie.
44
 *
45
 * This data structure stores a trie of expressions with
46
 * the same name, and must be distinguished by their argument types.
47
 * It is context-dependent.
48
 *
49
 * Using the argument allowFunVariants,
50
 * it may either be configured to allow function variants or not,
51
 * where a function variant is function that expects the same
52
 * argument types as another.
53
 *
54
 * For example, the following definitions introduce function
55
 * variants for the symbol f:
56
 *
57
 * 1. (declare-fun f (Int) Int) and
58
 *    (declare-fun f (Int) Bool)
59
 *
60
 * 2. (declare-fun f (Int) Int) and
61
 *    (declare-fun f (Int) Int)
62
 *
63
 * 3. (declare-datatypes ((Tup 0)) ((f (data Int)))) and
64
 *    (declare-fun f (Int) Tup)
65
 *
66
 * 4. (declare-datatypes ((Tup 0)) ((mkTup (f Int)))) and
67
 *    (declare-fun f (Tup) Bool)
68
 *
69
 * If function variants is set to true, we allow function variants
70
 * but not function redefinition. In examples 2 and 3, f is
71
 * declared twice as a symbol of identical argument and range
72
 * types. We never accept these definitions. However, we do
73
 * allow examples 1 and 4 above when allowFunVariants is true.
74
 *
75
 * For 0-argument functions (constants), we always allow
76
 * function variants.  That is, we always accept these examples:
77
 *
78
 * 5.  (declare-fun c () Int)
79
 *     (declare-fun c () Bool)
80
 *
81
 * 6.  (declare-datatypes ((Enum 0)) ((c)))
82
 *     (declare-fun c () Int)
83
 *
84
 * and always reject constant redefinition such as:
85
 *
86
 * 7. (declare-fun c () Int)
87
 *    (declare-fun c () Int)
88
 *
89
 * 8. (declare-datatypes ((Enum 0)) ((c))) and
90
 *    (declare-fun c () Enum)
91
 */
92
class OverloadedTypeTrie {
93
 public:
94
5787
  OverloadedTypeTrie(Context* c, bool allowFunVariants = false)
95
5787
      : d_overloaded_symbols(
96
5787
            new (true) CDHashSet<api::Term, api::TermHashFunction>(c)),
97
11574
        d_allowFunctionVariants(allowFunVariants)
98
  {
99
5787
  }
100
5766
  ~OverloadedTypeTrie() { d_overloaded_symbols->deleteSelf(); }
101
102
  /** is this function overloaded? */
103
  bool isOverloadedFunction(api::Term fun) const;
104
105
  /** Get overloaded constant for type.
106
   * If possible, it returns a defined symbol with name
107
   * that has type t. Otherwise returns null expression.
108
   */
109
  api::Term getOverloadedConstantForType(const std::string& name,
110
                                         api::Sort t) const;
111
112
  /**
113
   * If possible, returns a defined function for a name
114
   * and a vector of expected argument types. Otherwise returns
115
   * null expression.
116
   */
117
  api::Term getOverloadedFunctionForTypes(
118
      const std::string& name, const std::vector<api::Sort>& argTypes) const;
119
  /** called when obj is bound to name, and prev_bound_obj was already bound to
120
   * name Returns false if the binding is invalid.
121
   */
122
  bool bind(const string& name, api::Term prev_bound_obj, api::Term obj);
123
124
 private:
125
  /** Marks expression obj with name as overloaded.
126
   * Adds relevant information to the type arg trie data structure.
127
   * It returns false if there is already an expression bound to that name
128
   * whose type expects the same arguments as the type of obj but is not
129
   * identical to the type of obj.  For example, if we declare :
130
   *
131
   * (declare-datatypes () ((List (cons (hd Int) (tl List)) (nil))))
132
   * (declare-fun cons (Int List) List)
133
   *
134
   * cons : constructor_type( Int, List, List )
135
   * cons : function_type( Int, List, List )
136
   *
137
   * These are put in the same place in the trie but do not have identical type,
138
   * hence we return false.
139
   */
140
  bool markOverloaded(const string& name, api::Term obj);
141
  /** the null expression */
142
  api::Term d_nullTerm;
143
  // The (context-independent) trie storing that maps expected argument
144
  // vectors to symbols. All expressions stored in d_symbols are only
145
  // interpreted as active if they also appear in the context-dependent
146
  // set d_overloaded_symbols.
147
88
  class TypeArgTrie {
148
   public:
149
    // children of this node
150
    std::map<api::Sort, TypeArgTrie> d_children;
151
    // symbols at this node
152
    std::map<api::Sort, api::Term> d_symbols;
153
  };
154
  /** for each string with operator overloading, this stores the data structure
155
   * above. */
156
  std::unordered_map<std::string, TypeArgTrie> d_overload_type_arg_trie;
157
  /** The set of overloaded symbols. */
158
  CDHashSet<api::Term, api::TermHashFunction>* d_overloaded_symbols;
159
  /** allow function variants
160
   * This is true if we allow overloading (non-constant) functions that expect
161
   * the same argument types.
162
   */
163
  bool d_allowFunctionVariants;
164
  /** get unique overloaded function
165
  * If tat->d_symbols contains an active overloaded function, it
166
  * returns that function, where that function must be unique
167
  * if reqUnique=true.
168
  * Otherwise, it returns the null expression.
169
  */
170
  api::Term getOverloadedFunctionAt(const TypeArgTrie* tat,
171
                                    bool reqUnique = true) const;
172
};
173
174
3806836
bool OverloadedTypeTrie::isOverloadedFunction(api::Term fun) const
175
{
176
3806836
  return d_overloaded_symbols->find(fun) != d_overloaded_symbols->end();
177
}
178
179
6
api::Term OverloadedTypeTrie::getOverloadedConstantForType(
180
    const std::string& name, api::Sort t) const
181
{
182
  std::unordered_map<std::string, TypeArgTrie>::const_iterator it =
183
6
      d_overload_type_arg_trie.find(name);
184
6
  if (it != d_overload_type_arg_trie.end()) {
185
    std::map<api::Sort, api::Term>::const_iterator its =
186
6
        it->second.d_symbols.find(t);
187
6
    if (its != it->second.d_symbols.end()) {
188
6
      api::Term expr = its->second;
189
      // must be an active symbol
190
6
      if (isOverloadedFunction(expr)) {
191
6
        return expr;
192
      }
193
    }
194
  }
195
  return d_nullTerm;
196
}
197
198
14
api::Term OverloadedTypeTrie::getOverloadedFunctionForTypes(
199
    const std::string& name, const std::vector<api::Sort>& argTypes) const
200
{
201
  std::unordered_map<std::string, TypeArgTrie>::const_iterator it =
202
14
      d_overload_type_arg_trie.find(name);
203
14
  if (it != d_overload_type_arg_trie.end()) {
204
14
    const TypeArgTrie* tat = &it->second;
205
30
    for (unsigned i = 0; i < argTypes.size(); i++) {
206
      std::map<api::Sort, TypeArgTrie>::const_iterator itc =
207
16
          tat->d_children.find(argTypes[i]);
208
16
      if (itc != tat->d_children.end()) {
209
16
        tat = &itc->second;
210
      } else {
211
        Trace("parser-overloading")
212
            << "Could not find overloaded function " << name << std::endl;
213
214
          // no functions match
215
        return d_nullTerm;
216
      }
217
    }
218
    // we ensure that there is *only* one active symbol at this node
219
14
    return getOverloadedFunctionAt(tat);
220
  }
221
  return d_nullTerm;
222
}
223
224
20
bool OverloadedTypeTrie::bind(const string& name,
225
                              api::Term prev_bound_obj,
226
                              api::Term obj)
227
{
228
20
  bool retprev = true;
229
20
  if (!isOverloadedFunction(prev_bound_obj)) {
230
    // mark previous as overloaded
231
16
    retprev = markOverloaded(name, prev_bound_obj);
232
  }
233
  // mark this as overloaded
234
20
  bool retobj = markOverloaded(name, obj);
235
20
  return retprev && retobj;
236
}
237
238
36
bool OverloadedTypeTrie::markOverloaded(const string& name, api::Term obj)
239
{
240
36
  Trace("parser-overloading") << "Overloaded function : " << name;
241
36
  Trace("parser-overloading") << " with type " << obj.getSort() << std::endl;
242
  // get the argument types
243
72
  api::Sort t = obj.getSort();
244
72
  api::Sort rangeType = t;
245
72
  std::vector<api::Sort> argTypes;
246
36
  if (t.isFunction())
247
  {
248
6
    argTypes = t.getFunctionDomainSorts();
249
6
    rangeType = t.getFunctionCodomainSort();
250
  }
251
30
  else if (t.isConstructor())
252
  {
253
14
    argTypes = t.getConstructorDomainSorts();
254
14
    rangeType = t.getConstructorCodomainSort();
255
  }
256
16
  else if (t.isTester())
257
  {
258
12
    argTypes.push_back(t.getTesterDomainSort());
259
12
    rangeType = t.getTesterCodomainSort();
260
  }
261
4
  else if (t.isSelector())
262
  {
263
4
    argTypes.push_back(t.getSelectorDomainSort());
264
4
    rangeType = t.getSelectorCodomainSort();
265
  }
266
  // add to the trie
267
36
  TypeArgTrie* tat = &d_overload_type_arg_trie[name];
268
66
  for (unsigned i = 0; i < argTypes.size(); i++) {
269
30
    tat = &(tat->d_children[argTypes[i]]);
270
  }
271
272
  // check if function variants are allowed here
273
36
  if (d_allowFunctionVariants || argTypes.empty())
274
  {
275
    // they are allowed, check for redefinition
276
    std::map<api::Sort, api::Term>::iterator it =
277
8
        tat->d_symbols.find(rangeType);
278
8
    if (it != tat->d_symbols.end())
279
    {
280
      api::Term prev_obj = it->second;
281
      // if there is already an active function with the same name and expects
282
      // the same argument types and has the same return type, we reject the
283
      // re-declaration here.
284
      if (isOverloadedFunction(prev_obj))
285
      {
286
        return false;
287
      }
288
    }
289
  }
290
  else
291
  {
292
    // they are not allowed, we cannot have any function defined here.
293
56
    api::Term existingFun = getOverloadedFunctionAt(tat, false);
294
28
    if (!existingFun.isNull())
295
    {
296
      return false;
297
    }
298
  }
299
300
  // otherwise, update the symbols
301
36
  d_overloaded_symbols->insert(obj);
302
36
  tat->d_symbols[rangeType] = obj;
303
36
  return true;
304
}
305
306
42
api::Term OverloadedTypeTrie::getOverloadedFunctionAt(
307
    const OverloadedTypeTrie::TypeArgTrie* tat, bool reqUnique) const
308
{
309
84
  api::Term retExpr;
310
14
  for (std::map<api::Sort, api::Term>::const_iterator its =
311
42
           tat->d_symbols.begin();
312
56
       its != tat->d_symbols.end();
313
       ++its)
314
  {
315
28
    api::Term expr = its->second;
316
14
    if (isOverloadedFunction(expr))
317
    {
318
14
      if (retExpr.isNull())
319
      {
320
14
        if (!reqUnique)
321
        {
322
          return expr;
323
        }
324
        else
325
        {
326
14
          retExpr = expr;
327
        }
328
      }
329
      else
330
      {
331
        // multiple functions match
332
        return d_nullTerm;
333
      }
334
    }
335
  }
336
42
  return retExpr;
337
}
338
339
class SymbolTable::Implementation {
340
 public:
341
5787
  Implementation()
342
5787
      : d_context(),
343
        d_exprMap(&d_context),
344
        d_typeMap(&d_context),
345
5787
        d_overload_trie(&d_context)
346
  {
347
    // use an outermost push, to be able to clear definitions not at level zero
348
5787
    d_context.push();
349
5787
  }
350
351
5766
  ~Implementation() { d_context.pop(); }
352
353
  bool bind(const string& name, api::Term obj, bool levelZero, bool doOverload);
354
  void bindType(const string& name, api::Sort t, bool levelZero = false);
355
  void bindType(const string& name,
356
                const vector<api::Sort>& params,
357
                api::Sort t,
358
                bool levelZero = false);
359
  bool isBound(const string& name) const;
360
  bool isBoundType(const string& name) const;
361
  api::Term lookup(const string& name) const;
362
  api::Sort lookupType(const string& name) const;
363
  api::Sort lookupType(const string& name,
364
                       const vector<api::Sort>& params) const;
365
  size_t lookupArity(const string& name);
366
  void popScope();
367
  void pushScope();
368
  size_t getLevel() const;
369
  void reset();
370
  void resetAssertions();
371
  //------------------------ operator overloading
372
  /** implementation of function from header */
373
  bool isOverloadedFunction(api::Term fun) const;
374
375
  /** implementation of function from header */
376
  api::Term getOverloadedConstantForType(const std::string& name,
377
                                         api::Sort t) const;
378
379
  /** implementation of function from header */
380
  api::Term getOverloadedFunctionForTypes(
381
      const std::string& name, const std::vector<api::Sort>& argTypes) const;
382
  //------------------------ end operator overloading
383
 private:
384
  /** The context manager for the scope maps. */
385
  Context d_context;
386
387
  /** A map for expressions. */
388
  CDHashMap<string, api::Term> d_exprMap;
389
390
  /** A map for types. */
391
  using TypeMap = CDHashMap<string, std::pair<vector<api::Sort>, api::Sort>>;
392
  TypeMap d_typeMap;
393
394
  //------------------------ operator overloading
395
  // the null expression
396
  api::Term d_nullTerm;
397
  // overloaded type trie, stores all information regarding overloading
398
  OverloadedTypeTrie d_overload_trie;
399
  /** bind with overloading
400
   * This is called whenever obj is bound to name where overloading symbols is
401
   * allowed. If a symbol is previously bound to that name, it marks both as
402
   * overloaded. Returns false if the binding was invalid.
403
   */
404
  bool bindWithOverloading(const string& name, api::Term obj);
405
  //------------------------ end operator overloading
406
}; /* SymbolTable::Implementation */
407
408
362456
bool SymbolTable::Implementation::bind(const string& name,
409
                                       api::Term obj,
410
                                       bool levelZero,
411
                                       bool doOverload)
412
{
413
362456
  PrettyCheckArgument(!obj.isNull(), obj, "cannot bind to a null api::Term");
414
724912
  Trace("sym-table") << "SymbolTable: bind " << name
415
362456
                     << ", levelZero=" << levelZero
416
362456
                     << ", doOverload=" << doOverload << std::endl;
417
362456
  if (doOverload) {
418
178818
    if (!bindWithOverloading(name, obj)) {
419
      return false;
420
    }
421
  }
422
362456
  if (levelZero) {
423
10150
    d_exprMap.insertAtContextLevelZero(name, obj);
424
  } else {
425
352306
    d_exprMap.insert(name, obj);
426
  }
427
362456
  return true;
428
}
429
430
19032502
bool SymbolTable::Implementation::isBound(const string& name) const {
431
19032502
  return d_exprMap.find(name) != d_exprMap.end();
432
}
433
434
3806796
api::Term SymbolTable::Implementation::lookup(const string& name) const
435
{
436
3806796
  Assert(isBound(name));
437
7613592
  api::Term expr = (*d_exprMap.find(name)).second;
438
3806796
  if (isOverloadedFunction(expr)) {
439
20
    return d_nullTerm;
440
  } else {
441
3806776
    return expr;
442
  }
443
}
444
445
28283
void SymbolTable::Implementation::bindType(const string& name,
446
                                           api::Sort t,
447
                                           bool levelZero)
448
{
449
28283
  if (levelZero) {
450
21520
    d_typeMap.insertAtContextLevelZero(name, make_pair(vector<api::Sort>(), t));
451
  } else {
452
6763
    d_typeMap.insert(name, make_pair(vector<api::Sort>(), t));
453
  }
454
28283
}
455
456
334
void SymbolTable::Implementation::bindType(const string& name,
457
                                           const vector<api::Sort>& params,
458
                                           api::Sort t,
459
                                           bool levelZero)
460
{
461
334
  if (Debug.isOn("sort")) {
462
    Debug("sort") << "bindType(" << name << ", [";
463
    if (params.size() > 0) {
464
      copy(params.begin(),
465
           params.end() - 1,
466
           ostream_iterator<api::Sort>(Debug("sort"), ", "));
467
      Debug("sort") << params.back();
468
    }
469
    Debug("sort") << "], " << t << ")" << endl;
470
  }
471
334
  if (levelZero) {
472
4
    d_typeMap.insertAtContextLevelZero(name, make_pair(params, t));
473
  } else {
474
330
    d_typeMap.insert(name, make_pair(params, t));
475
  }
476
334
}
477
478
624461
bool SymbolTable::Implementation::isBoundType(const string& name) const {
479
624461
  return d_typeMap.find(name) != d_typeMap.end();
480
}
481
482
273863
api::Sort SymbolTable::Implementation::lookupType(const string& name) const
483
{
484
  std::pair<std::vector<api::Sort>, api::Sort> p =
485
547726
      (*d_typeMap.find(name)).second;
486
273863
  PrettyCheckArgument(p.first.size() == 0, name,
487
                      "type constructor arity is wrong: "
488
                      "`%s' requires %u parameters but was provided 0",
489
                      name.c_str(), p.first.size());
490
547726
  return p.second;
491
}
492
493
588
api::Sort SymbolTable::Implementation::lookupType(
494
    const string& name, const vector<api::Sort>& params) const
495
{
496
  std::pair<std::vector<api::Sort>, api::Sort> p =
497
1176
      (*d_typeMap.find(name)).second;
498
588
  PrettyCheckArgument(p.first.size() == params.size(), params,
499
                      "type constructor arity is wrong: "
500
                      "`%s' requires %u parameters but was provided %u",
501
                      name.c_str(), p.first.size(), params.size());
502
588
  if (p.first.size() == 0) {
503
    PrettyCheckArgument(p.second.isUninterpretedSort(), name.c_str());
504
    return p.second;
505
  }
506
588
  if (p.second.isDatatype())
507
  {
508
172
    PrettyCheckArgument(
509
        p.second.isParametricDatatype(), name, "expected parametric datatype");
510
172
    return p.second.instantiate(params);
511
  }
512
416
  bool isSortConstructor = p.second.isSortConstructor();
513
416
  if (Debug.isOn("sort"))
514
  {
515
    Debug("sort") << "instantiating using a sort "
516
                  << (isSortConstructor ? "constructor" : "substitution")
517
                  << std::endl;
518
    Debug("sort") << "have formals [";
519
    copy(p.first.begin(),
520
         p.first.end() - 1,
521
         ostream_iterator<api::Sort>(Debug("sort"), ", "));
522
    Debug("sort") << p.first.back() << "]" << std::endl << "parameters   [";
523
    copy(params.begin(),
524
         params.end() - 1,
525
         ostream_iterator<api::Sort>(Debug("sort"), ", "));
526
    Debug("sort") << params.back() << "]" << endl
527
                  << "type ctor    " << name << std::endl
528
                  << "type is      " << p.second << std::endl;
529
  }
530
  api::Sort instantiation = isSortConstructor
531
                                ? p.second.instantiate(params)
532
832
                                : p.second.substitute(p.first, params);
533
534
416
  Debug("sort") << "instance is  " << instantiation << std::endl;
535
536
416
  return instantiation;
537
}
538
539
5488
size_t SymbolTable::Implementation::lookupArity(const string& name) {
540
  std::pair<std::vector<api::Sort>, api::Sort> p =
541
10976
      (*d_typeMap.find(name)).second;
542
10976
  return p.first.size();
543
}
544
545
101860
void SymbolTable::Implementation::popScope() {
546
  // should not pop beyond level one
547
101860
  if (d_context.getLevel() == 1)
548
  {
549
2
    throw ScopeException();
550
  }
551
101858
  d_context.pop();
552
101858
}
553
554
102298
void SymbolTable::Implementation::pushScope() { d_context.push(); }
555
556
2115
size_t SymbolTable::Implementation::getLevel() const {
557
2115
  return d_context.getLevel();
558
}
559
560
47
void SymbolTable::Implementation::reset() {
561
47
  Trace("sym-table") << "SymbolTable: reset" << std::endl;
562
47
  this->SymbolTable::Implementation::~Implementation();
563
47
  new (this) SymbolTable::Implementation();
564
47
}
565
566
31
void SymbolTable::Implementation::resetAssertions()
567
{
568
31
  Trace("sym-table") << "SymbolTable: resetAssertions" << std::endl;
569
  // pop all contexts
570
105
  while (d_context.getLevel() > 0)
571
  {
572
37
    d_context.pop();
573
  }
574
31
  d_context.push();
575
31
}
576
577
3806796
bool SymbolTable::Implementation::isOverloadedFunction(api::Term fun) const
578
{
579
3806796
  return d_overload_trie.isOverloadedFunction(fun);
580
}
581
582
6
api::Term SymbolTable::Implementation::getOverloadedConstantForType(
583
    const std::string& name, api::Sort t) const
584
{
585
6
  return d_overload_trie.getOverloadedConstantForType(name, t);
586
}
587
588
14
api::Term SymbolTable::Implementation::getOverloadedFunctionForTypes(
589
    const std::string& name, const std::vector<api::Sort>& argTypes) const
590
{
591
14
  return d_overload_trie.getOverloadedFunctionForTypes(name, argTypes);
592
}
593
594
178818
bool SymbolTable::Implementation::bindWithOverloading(const string& name,
595
                                                      api::Term obj)
596
{
597
178818
  CDHashMap<string, api::Term>::const_iterator it = d_exprMap.find(name);
598
178818
  if (it != d_exprMap.end())
599
  {
600
20
    const api::Term& prev_bound_obj = (*it).second;
601
20
    if (prev_bound_obj != obj) {
602
20
      return d_overload_trie.bind(name, prev_bound_obj, obj);
603
    }
604
  }
605
178798
  return true;
606
}
607
608
bool SymbolTable::isOverloadedFunction(api::Term fun) const
609
{
610
  return d_implementation->isOverloadedFunction(fun);
611
}
612
613
6
api::Term SymbolTable::getOverloadedConstantForType(const std::string& name,
614
                                                    api::Sort t) const
615
{
616
6
  return d_implementation->getOverloadedConstantForType(name, t);
617
}
618
619
14
api::Term SymbolTable::getOverloadedFunctionForTypes(
620
    const std::string& name, const std::vector<api::Sort>& argTypes) const
621
{
622
14
  return d_implementation->getOverloadedFunctionForTypes(name, argTypes);
623
}
624
625
5740
SymbolTable::SymbolTable() : d_implementation(new SymbolTable::Implementation())
626
{
627
5740
}
628
629
5719
SymbolTable::~SymbolTable() {}
630
362456
bool SymbolTable::bind(const string& name,
631
                       api::Term obj,
632
                       bool levelZero,
633
                       bool doOverload)
634
{
635
362456
  return d_implementation->bind(name, obj, levelZero, doOverload);
636
}
637
638
28283
void SymbolTable::bindType(const string& name, api::Sort t, bool levelZero)
639
{
640
28283
  d_implementation->bindType(name, t, levelZero);
641
28283
}
642
643
334
void SymbolTable::bindType(const string& name,
644
                           const vector<api::Sort>& params,
645
                           api::Sort t,
646
                           bool levelZero)
647
{
648
334
  d_implementation->bindType(name, params, t, levelZero);
649
334
}
650
651
15225706
bool SymbolTable::isBound(const string& name) const
652
{
653
15225706
  return d_implementation->isBound(name);
654
}
655
624461
bool SymbolTable::isBoundType(const string& name) const
656
{
657
624461
  return d_implementation->isBoundType(name);
658
}
659
3806796
api::Term SymbolTable::lookup(const string& name) const
660
{
661
3806796
  return d_implementation->lookup(name);
662
}
663
273863
api::Sort SymbolTable::lookupType(const string& name) const
664
{
665
273863
  return d_implementation->lookupType(name);
666
}
667
668
588
api::Sort SymbolTable::lookupType(const string& name,
669
                                  const vector<api::Sort>& params) const
670
{
671
588
  return d_implementation->lookupType(name, params);
672
}
673
5488
size_t SymbolTable::lookupArity(const string& name) {
674
5488
  return d_implementation->lookupArity(name);
675
}
676
101860
void SymbolTable::popScope() { d_implementation->popScope(); }
677
102298
void SymbolTable::pushScope() { d_implementation->pushScope(); }
678
2115
size_t SymbolTable::getLevel() const { return d_implementation->getLevel(); }
679
47
void SymbolTable::reset() { d_implementation->reset(); }
680
31
void SymbolTable::resetAssertions() { d_implementation->resetAssertions(); }
681
682
26676
}  // namespace CVC4