Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Tim King, Andres Noetzli
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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.
11 : : * ****************************************************************************
12 : : *
13 : : * Convenience class for scoping variable and type declarations
14 : : * (implementation).
15 : : */
16 : :
17 : : #include "parser/symbol_table.h"
18 : :
19 : : #include <cvc5/cvc5.h>
20 : :
21 : : #include <ostream>
22 : : #include <string>
23 : : #include <unordered_map>
24 : : #include <utility>
25 : :
26 : : #include "base/check.h"
27 : : #include "context/cdhashmap.h"
28 : : #include "context/cdhashset.h"
29 : : #include "context/context.h"
30 : :
31 : : namespace cvc5::internal::parser {
32 : :
33 : : using context::CDHashMap;
34 : : using context::CDHashSet;
35 : : using 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 : : {
94 : : public:
95 : 25163 : OverloadedTypeTrie(Context* c, bool allowFunVariants = false)
96 : 25163 : : d_overloaded_symbols(new (true) CDHashSet<Term, std::hash<Term>>(c)),
97 : 25163 : d_allowFunctionVariants(allowFunVariants)
98 : : {
99 : 25163 : }
100 : 25114 : ~OverloadedTypeTrie() { d_overloaded_symbols->deleteSelf(); }
101 : :
102 : : /** is this function overloaded? */
103 : : bool isOverloadedFunction(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 : : Term getOverloadedConstantForType(const std::string& name, Sort t) const;
110 : :
111 : : /**
112 : : * If possible, returns a defined function for a name
113 : : * and a vector of expected argument types. Otherwise returns
114 : : * null expression.
115 : : */
116 : : Term getOverloadedFunctionForTypes(const std::string& name,
117 : : const std::vector<Sort>& argTypes) const;
118 : : /** called when obj is bound to name, and prev_bound_obj was already bound to
119 : : * name Returns false if the binding is invalid.
120 : : */
121 : : bool bind(const string& name, Term prev_bound_obj, Term obj);
122 : :
123 : : private:
124 : : /** Marks expression obj with name as overloaded.
125 : : * Adds relevant information to the type arg trie data structure.
126 : : * It returns false if there is already an expression bound to that name
127 : : * whose type expects the same arguments as the type of obj but is not
128 : : * identical to the type of obj. For example, if we declare :
129 : : *
130 : : * (declare-datatypes () ((List (cons (hd Int) (tl List)) (nil))))
131 : : * (declare-fun cons (Int List) List)
132 : : *
133 : : * cons : constructor_type( Int, List, List )
134 : : * cons : function_type( Int, List, List )
135 : : *
136 : : * These are put in the same place in the trie but do not have identical type,
137 : : * hence we return false.
138 : : */
139 : : bool markOverloaded(const string& name, Term obj);
140 : : /** the null expression */
141 : : Term d_nullTerm;
142 : : // The (context-independent) trie storing that maps expected argument
143 : : // vectors to symbols. All expressions stored in d_symbols are only
144 : : // interpreted as active if they also appear in the context-dependent
145 : : // set d_overloaded_symbols.
146 : : class TypeArgTrie
147 : : {
148 : : public:
149 : : // children of this node
150 : : std::map<Sort, TypeArgTrie> d_children;
151 : : // symbols at this node
152 : : std::map<Sort, 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<Term, std::hash<Term>>* 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 : : Term getOverloadedFunctionAt(const TypeArgTrie* tat,
171 : : bool reqUnique = true) const;
172 : : };
173 : :
174 : 6259790 : bool OverloadedTypeTrie::isOverloadedFunction(Term fun) const
175 : : {
176 : 6259790 : return d_overloaded_symbols->find(fun) != d_overloaded_symbols->end();
177 : : }
178 : :
179 : 6 : Term OverloadedTypeTrie::getOverloadedConstantForType(const std::string& name,
180 : : 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 : : {
186 : 6 : std::map<Sort, Term>::const_iterator its = it->second.d_symbols.find(t);
187 [ + - ]: 6 : if (its != it->second.d_symbols.end())
188 : : {
189 : 6 : Term expr = its->second;
190 : : // must be an active symbol
191 [ + - ]: 6 : if (isOverloadedFunction(expr))
192 : : {
193 : 6 : return expr;
194 : : }
195 : : }
196 : : }
197 : 0 : return d_nullTerm;
198 : : }
199 : :
200 : 259 : Term OverloadedTypeTrie::getOverloadedFunctionForTypes(
201 : : const std::string& name, const std::vector<Sort>& argTypes) const
202 : : {
203 : : std::unordered_map<std::string, TypeArgTrie>::const_iterator it =
204 : 259 : d_overload_type_arg_trie.find(name);
205 [ + - ]: 259 : if (it != d_overload_type_arg_trie.end())
206 : : {
207 : 259 : const TypeArgTrie* tat = &it->second;
208 [ + + ]: 697 : for (unsigned i = 0; i < argTypes.size(); i++)
209 : : {
210 : : std::map<Sort, TypeArgTrie>::const_iterator itc =
211 : 438 : tat->d_children.find(argTypes[i]);
212 [ + - ]: 438 : if (itc != tat->d_children.end())
213 : : {
214 : 438 : tat = &itc->second;
215 : : }
216 : : else
217 : : {
218 [ - - ]: 0 : Trace("parser-overloading")
219 : 0 : << "Could not find overloaded function " << name << std::endl;
220 : :
221 : : // no functions match
222 : 0 : return d_nullTerm;
223 : : }
224 : : }
225 : : // we ensure that there is *only* one active symbol at this node
226 : 259 : return getOverloadedFunctionAt(tat);
227 : : }
228 : 0 : return d_nullTerm;
229 : : }
230 : :
231 : 223 : bool OverloadedTypeTrie::bind(const string& name, Term prev_bound_obj, Term obj)
232 : : {
233 [ - + ][ - + ]: 223 : Assert(prev_bound_obj != obj);
[ - - ]
234 : 223 : bool retprev = true;
235 [ + + ]: 223 : if (!isOverloadedFunction(prev_bound_obj))
236 : : {
237 : : // mark previous as overloaded
238 : 162 : retprev = markOverloaded(name, prev_bound_obj);
239 : : }
240 : : // mark this as overloaded
241 : 223 : bool retobj = markOverloaded(name, obj);
242 [ + - ][ + + ]: 223 : return retprev && retobj;
243 : : }
244 : :
245 : 385 : bool OverloadedTypeTrie::markOverloaded(const string& name, Term obj)
246 : : {
247 [ + - ]: 385 : Trace("parser-overloading") << "Overloaded function : " << name;
248 [ + - ]: 770 : Trace("parser-overloading")
249 [ - + ][ - - ]: 385 : << " with type " << obj.getSort() << ", obj is " << obj << std::endl;
250 : : // get the argument types
251 : 770 : Sort t = obj.getSort();
252 : 770 : Sort rangeType = t;
253 : 770 : std::vector<Sort> argTypes;
254 [ + + ]: 385 : if (t.isFunction())
255 : : {
256 : 80 : argTypes = t.getFunctionDomainSorts();
257 : 80 : rangeType = t.getFunctionCodomainSort();
258 : : }
259 [ + + ]: 305 : else if (t.isDatatypeConstructor())
260 : : {
261 : 78 : argTypes = t.getDatatypeConstructorDomainSorts();
262 : 78 : rangeType = t.getDatatypeConstructorCodomainSort();
263 : : }
264 [ + + ]: 227 : else if (t.isDatatypeSelector())
265 : : {
266 : 98 : argTypes.push_back(t.getDatatypeSelectorDomainSort());
267 : 98 : rangeType = t.getDatatypeSelectorCodomainSort();
268 : : }
269 : : // add to the trie
270 : 385 : TypeArgTrie* tat = &d_overload_type_arg_trie[name];
271 [ + + ]: 780 : for (unsigned i = 0; i < argTypes.size(); i++)
272 : : {
273 : 395 : tat = &(tat->d_children[argTypes[i]]);
274 : : }
275 : :
276 : : // check if function variants are allowed here
277 [ + - ][ + + ]: 385 : if (d_allowFunctionVariants || argTypes.empty())
[ + + ]
278 : : {
279 : : // they are allowed, check for redefinition
280 : 129 : std::map<Sort, Term>::iterator it = tat->d_symbols.find(rangeType);
281 [ + + ]: 129 : if (it != tat->d_symbols.end())
282 : : {
283 : 2 : Term prev_obj = it->second;
284 : : // if there is already an active function with the same name and expects
285 : : // the same argument types and has the same return type, we reject the
286 : : // re-declaration here.
287 [ + - ]: 2 : if (isOverloadedFunction(prev_obj))
288 : : {
289 [ + - ]: 2 : Trace("parser-overloading") << "...existing overload" << std::endl;
290 : 2 : return false;
291 : : }
292 : : }
293 : : }
294 : : else
295 : : {
296 : : // they are not allowed, we cannot have any function defined here.
297 : 256 : Term existingFun = getOverloadedFunctionAt(tat, false);
298 [ - + ]: 256 : if (!existingFun.isNull())
299 : : {
300 [ - - ]: 0 : Trace("parser-overloading")
301 : 0 : << "...existing fun (no variant)" << std::endl;
302 : 0 : return false;
303 : : }
304 : : }
305 [ + - ]: 383 : Trace("parser-overloading") << "...update symbols" << std::endl;
306 : :
307 : : // otherwise, update the symbols
308 : 383 : d_overloaded_symbols->insert(obj);
309 : 383 : tat->d_symbols[rangeType] = obj;
310 : 383 : return true;
311 : : }
312 : :
313 : 515 : Term OverloadedTypeTrie::getOverloadedFunctionAt(
314 : : const OverloadedTypeTrie::TypeArgTrie* tat, bool reqUnique) const
315 : : {
316 : 1030 : Term retExpr;
317 : 774 : for (std::map<Sort, Term>::const_iterator its = tat->d_symbols.begin();
318 [ + + ]: 774 : its != tat->d_symbols.end();
319 : 259 : ++its)
320 : : {
321 : 259 : Term expr = its->second;
322 [ + - ]: 259 : if (isOverloadedFunction(expr))
323 : : {
324 [ + - ]: 259 : if (retExpr.isNull())
325 : : {
326 [ - + ]: 259 : if (!reqUnique)
327 : : {
328 : 0 : return expr;
329 : : }
330 : : else
331 : : {
332 : 259 : retExpr = expr;
333 : : }
334 : : }
335 : : else
336 : : {
337 : : // multiple functions match
338 : 0 : return d_nullTerm;
339 : : }
340 : : }
341 : : }
342 : 515 : return retExpr;
343 : : }
344 : :
345 : : class SymbolTable::Implementation
346 : : {
347 : : public:
348 : 25163 : Implementation()
349 : 25163 : : d_context(),
350 : : d_exprMap(&d_context),
351 : : d_typeMap(&d_context),
352 : 25163 : d_overload_trie(&d_context)
353 : : {
354 : 25163 : }
355 : :
356 : 25114 : ~Implementation() {}
357 : :
358 : : bool bind(const string& name, Term obj, bool doOverload);
359 : : void bindType(const string& name, Sort t);
360 : : void bindType(const string& name, const vector<Sort>& params, Sort t);
361 : : bool isBound(const string& name) const;
362 : : bool isBoundType(const string& name) const;
363 : : Term lookup(const string& name) const;
364 : : Sort lookupType(const string& name) const;
365 : : Sort lookupType(const string& name, const vector<Sort>& params) const;
366 : : size_t lookupArity(const string& name);
367 : : void popScope();
368 : : void pushScope();
369 : : size_t getLevel() const;
370 : : void reset();
371 : : void resetAssertions();
372 : : //------------------------ operator overloading
373 : : /** implementation of function from header */
374 : : bool isOverloadedFunction(Term fun) const;
375 : :
376 : : /** implementation of function from header */
377 : : Term getOverloadedConstantForType(const std::string& name, Sort t) const;
378 : :
379 : : /** implementation of function from header */
380 : : Term getOverloadedFunctionForTypes(const std::string& name,
381 : : const std::vector<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, Term> d_exprMap;
389 : :
390 : : /** A map for types. */
391 : : using TypeMap = CDHashMap<string, std::pair<vector<Sort>, Sort>>;
392 : : TypeMap d_typeMap;
393 : :
394 : : //------------------------ operator overloading
395 : : /** the null term */
396 : : Term d_nullTerm;
397 : : /** The null sort */
398 : : Sort d_nullSort;
399 : : // overloaded type trie, stores all information regarding overloading
400 : : OverloadedTypeTrie d_overload_trie;
401 : : /** bind with overloading
402 : : * This is called whenever obj is bound to name where overloading symbols is
403 : : * allowed. If a symbol is previously bound to that name, it marks both as
404 : : * overloaded. Returns false if the binding was invalid.
405 : : */
406 : : bool bindWithOverloading(const string& name, Term obj);
407 : : //------------------------ end operator overloading
408 : : }; /* SymbolTable::Implementation */
409 : :
410 : 1044850 : bool SymbolTable::Implementation::bind(const string& name,
411 : : Term obj,
412 : : bool doOverload)
413 : : {
414 [ - + ][ - + ]: 1044850 : Assert(!obj.isNull()) << "cannot bind to a null Term";
[ - - ]
415 [ + - ]: 2089700 : Trace("sym-table") << "SymbolTable: bind " << name << " to " << obj
416 : 1044850 : << ", doOverload=" << doOverload << std::endl;
417 [ + + ]: 1044850 : if (doOverload)
418 : : {
419 [ + + ]: 400430 : if (!bindWithOverloading(name, obj))
420 : : {
421 : 2 : return false;
422 : : }
423 : : }
424 : 1044850 : d_exprMap.insert(name, obj);
425 : :
426 : 1044850 : return true;
427 : : }
428 : :
429 : 1513530 : bool SymbolTable::Implementation::isBound(const string& name) const
430 : : {
431 : 1513530 : return d_exprMap.find(name) != d_exprMap.end();
432 : : }
433 : :
434 : 6259310 : Term SymbolTable::Implementation::lookup(const string& name) const
435 : : {
436 : 6259310 : CDHashMap<string, Term>::const_iterator it = d_exprMap.find(name);
437 [ + + ]: 6259310 : if (it == d_exprMap.end())
438 : : {
439 : 9 : return d_nullTerm;
440 : : }
441 : 12518600 : Term expr = it->second;
442 [ + + ]: 6259300 : if (isOverloadedFunction(expr))
443 : : {
444 : 265 : return d_nullTerm;
445 : : }
446 : 6259040 : return expr;
447 : : }
448 : :
449 : 172974 : void SymbolTable::Implementation::bindType(const string& name, Sort t)
450 : : {
451 : 172974 : d_typeMap.insert(name, make_pair(vector<Sort>(), t));
452 : 172974 : }
453 : :
454 : 11859 : void SymbolTable::Implementation::bindType(const string& name,
455 : : const vector<Sort>& params,
456 : : Sort t)
457 : : {
458 [ - + ]: 11859 : if (TraceIsOn("sort"))
459 : : {
460 [ - - ]: 0 : Trace("sort") << "bindType(" << name << ", [";
461 [ - - ]: 0 : if (params.size() > 0)
462 : : {
463 : 0 : copy(params.begin(),
464 : 0 : params.end() - 1,
465 [ - - ]: 0 : ostream_iterator<Sort>(Trace("sort"), ", "));
466 [ - - ]: 0 : Trace("sort") << params.back();
467 : : }
468 [ - - ]: 0 : Trace("sort") << "], " << t << ")" << endl;
469 : : }
470 : :
471 : 11859 : d_typeMap.insert(name, make_pair(params, t));
472 : 11859 : }
473 : :
474 : 367696 : bool SymbolTable::Implementation::isBoundType(const string& name) const
475 : : {
476 : 367696 : return d_typeMap.find(name) != d_typeMap.end();
477 : : }
478 : :
479 : 603692 : Sort SymbolTable::Implementation::lookupType(const string& name) const
480 : : {
481 : 603692 : TypeMap::const_iterator it = d_typeMap.find(name);
482 [ + + ]: 603692 : if (it == d_typeMap.end())
483 : : {
484 : 1 : return d_nullSort;
485 : : }
486 : 1207380 : std::pair<std::vector<Sort>, Sort> p = it->second;
487 [ - + ]: 603691 : if (p.first.size() != 0)
488 : : {
489 : 0 : std::stringstream ss;
490 : 0 : ss << "type constructor arity is wrong: `" << name << "' requires "
491 : 0 : << p.first.size() << " parameters but was provided 0";
492 : 0 : throw Exception(ss.str());
493 : : }
494 : 603691 : return p.second;
495 : : }
496 : :
497 : 1366 : Sort SymbolTable::Implementation::lookupType(const string& name,
498 : : const vector<Sort>& params) const
499 : : {
500 : 1366 : TypeMap::const_iterator it = d_typeMap.find(name);
501 [ + + ]: 1366 : if (it == d_typeMap.end())
502 : : {
503 : 2 : return d_nullSort;
504 : : }
505 : 2728 : std::pair<std::vector<Sort>, Sort> p = it->second;
506 [ + + ]: 1364 : if (p.first.size() != params.size())
507 : : {
508 : 2 : std::stringstream ss;
509 : 1 : ss << "type constructor arity is wrong: `" << name.c_str() << "' requires "
510 : 1 : << p.first.size() << " parameters but was provided " << params.size();
511 : 1 : throw Exception(ss.str());
512 : : }
513 [ - + ]: 1363 : if (p.first.size() == 0)
514 : : {
515 : 0 : Assert(p.second.isUninterpretedSort());
516 : 0 : return p.second;
517 : : }
518 [ + + ]: 1363 : if (p.second.isDatatype())
519 : : {
520 [ - + ][ - + ]: 489 : Assert(p.second.getDatatype().isParametric())
[ - - ]
521 : 0 : << "expected parametric datatype";
522 : 489 : return p.second.instantiate(params);
523 : : }
524 : : bool isUninterpretedSortConstructor =
525 : 874 : p.second.isUninterpretedSortConstructor();
526 [ - + ]: 874 : if (TraceIsOn("sort"))
527 : : {
528 [ - - ]: 0 : Trace("sort") << "instantiating using a sort "
529 [ - - ]: 0 : << (isUninterpretedSortConstructor ? "constructor"
530 : 0 : : "substitution")
531 : 0 : << std::endl;
532 [ - - ]: 0 : Trace("sort") << "have formals [";
533 : 0 : copy(p.first.begin(),
534 : 0 : p.first.end() - 1,
535 [ - - ]: 0 : ostream_iterator<Sort>(Trace("sort"), ", "));
536 [ - - ]: 0 : Trace("sort") << p.first.back() << "]" << std::endl << "parameters [";
537 : 0 : copy(params.begin(),
538 : 0 : params.end() - 1,
539 [ - - ]: 0 : ostream_iterator<Sort>(Trace("sort"), ", "));
540 [ - - ]: 0 : Trace("sort") << params.back() << "]" << endl
541 : 0 : << "type ctor " << name << std::endl
542 : 0 : << "type is " << p.second << std::endl;
543 : : }
544 : : Sort instantiation = isUninterpretedSortConstructor
545 : : ? p.second.instantiate(params)
546 [ + + ]: 1748 : : p.second.substitute(p.first, params);
547 [ + - ]: 874 : Trace("sort") << "instance is " << instantiation << std::endl;
548 : :
549 : 874 : return instantiation;
550 : : }
551 : :
552 : 0 : size_t SymbolTable::Implementation::lookupArity(const string& name)
553 : : {
554 : 0 : std::pair<std::vector<Sort>, Sort> p = (*d_typeMap.find(name)).second;
555 : 0 : return p.first.size();
556 : : }
557 : :
558 : 322116 : void SymbolTable::Implementation::popScope()
559 : : {
560 : : // should not pop beyond level one
561 [ + + ]: 322116 : if (d_context.getLevel() == 0)
562 : : {
563 : 1 : throw ScopeException();
564 : : }
565 : 322115 : d_context.pop();
566 : 322115 : }
567 : :
568 : 344179 : void SymbolTable::Implementation::pushScope() { d_context.push(); }
569 : :
570 : 16 : size_t SymbolTable::Implementation::getLevel() const
571 : : {
572 : 16 : return d_context.getLevel();
573 : : }
574 : :
575 : 92 : void SymbolTable::Implementation::reset()
576 : : {
577 [ + - ]: 92 : Trace("sym-table") << "SymbolTable: reset" << std::endl;
578 : 92 : this->SymbolTable::Implementation::~Implementation();
579 : 92 : new (this) SymbolTable::Implementation();
580 : 92 : }
581 : :
582 : 14 : void SymbolTable::Implementation::resetAssertions()
583 : : {
584 [ + - ]: 14 : Trace("sym-table") << "SymbolTable: resetAssertions" << std::endl;
585 : : // pop all contexts
586 [ + + ]: 34 : while (d_context.getLevel() > 0)
587 : : {
588 : 20 : d_context.pop();
589 : : }
590 : 14 : d_context.push();
591 : 14 : }
592 : :
593 : 6259300 : bool SymbolTable::Implementation::isOverloadedFunction(Term fun) const
594 : : {
595 : 6259300 : return d_overload_trie.isOverloadedFunction(fun);
596 : : }
597 : :
598 : 6 : Term SymbolTable::Implementation::getOverloadedConstantForType(
599 : : const std::string& name, Sort t) const
600 : : {
601 : 6 : return d_overload_trie.getOverloadedConstantForType(name, t);
602 : : }
603 : :
604 : 259 : Term SymbolTable::Implementation::getOverloadedFunctionForTypes(
605 : : const std::string& name, const std::vector<Sort>& argTypes) const
606 : : {
607 : 259 : return d_overload_trie.getOverloadedFunctionForTypes(name, argTypes);
608 : : }
609 : :
610 : 400430 : bool SymbolTable::Implementation::bindWithOverloading(const string& name,
611 : : Term obj)
612 : : {
613 : 400430 : CDHashMap<string, Term>::const_iterator it = d_exprMap.find(name);
614 [ + + ]: 400430 : if (it != d_exprMap.end())
615 : : {
616 : 475 : const Term& prev_bound_obj = (*it).second;
617 : : // Only bind if the object is different. Note this means we don't
618 : : // catch errors due to repeated function symbols when using
619 : : // --no-fresh-declarations.
620 : : // Note this is currently necessary to avoid rebinding symbols in
621 : : // the symbol manager.
622 [ + + ]: 475 : if (prev_bound_obj != obj)
623 : : {
624 : 223 : return d_overload_trie.bind(name, prev_bound_obj, obj);
625 : : }
626 : : }
627 : 400207 : return true;
628 : : }
629 : :
630 : 0 : bool SymbolTable::isOverloadedFunction(Term fun) const
631 : : {
632 : 0 : return d_implementation->isOverloadedFunction(fun);
633 : : }
634 : :
635 : 6 : Term SymbolTable::getOverloadedConstantForType(const std::string& name,
636 : : Sort t) const
637 : : {
638 : 6 : return d_implementation->getOverloadedConstantForType(name, t);
639 : : }
640 : :
641 : 259 : Term SymbolTable::getOverloadedFunctionForTypes(
642 : : const std::string& name, const std::vector<Sort>& argTypes) const
643 : : {
644 : 259 : return d_implementation->getOverloadedFunctionForTypes(name, argTypes);
645 : : }
646 : :
647 : 25071 : SymbolTable::SymbolTable() : d_implementation(new SymbolTable::Implementation())
648 : : {
649 : 25071 : }
650 : :
651 : 25022 : SymbolTable::~SymbolTable() {}
652 : 1044850 : bool SymbolTable::bind(const string& name, Term obj, bool doOverload)
653 : : {
654 : 1044850 : return d_implementation->bind(name, obj, doOverload);
655 : : }
656 : :
657 : 172974 : void SymbolTable::bindType(const string& name, Sort t)
658 : : {
659 : 172974 : d_implementation->bindType(name, t);
660 : 172974 : }
661 : :
662 : 11859 : void SymbolTable::bindType(const string& name,
663 : : const vector<Sort>& params,
664 : : Sort t)
665 : : {
666 : 11859 : d_implementation->bindType(name, params, t);
667 : 11859 : }
668 : :
669 : 1513530 : bool SymbolTable::isBound(const string& name) const
670 : : {
671 : 1513530 : return d_implementation->isBound(name);
672 : : }
673 : 367696 : bool SymbolTable::isBoundType(const string& name) const
674 : : {
675 : 367696 : return d_implementation->isBoundType(name);
676 : : }
677 : 6259310 : Term SymbolTable::lookup(const string& name) const
678 : : {
679 : 6259310 : return d_implementation->lookup(name);
680 : : }
681 : 603692 : Sort SymbolTable::lookupType(const string& name) const
682 : : {
683 : 603692 : return d_implementation->lookupType(name);
684 : : }
685 : :
686 : 1366 : Sort SymbolTable::lookupType(const string& name,
687 : : const vector<Sort>& params) const
688 : : {
689 : 1366 : return d_implementation->lookupType(name, params);
690 : : }
691 : 0 : size_t SymbolTable::lookupArity(const string& name)
692 : : {
693 : 0 : return d_implementation->lookupArity(name);
694 : : }
695 : 322116 : void SymbolTable::popScope() { d_implementation->popScope(); }
696 : 344179 : void SymbolTable::pushScope() { d_implementation->pushScope(); }
697 : 16 : size_t SymbolTable::getLevel() const { return d_implementation->getLevel(); }
698 : 92 : void SymbolTable::reset() { d_implementation->reset(); }
699 : 14 : void SymbolTable::resetAssertions() { d_implementation->resetAssertions(); }
700 : :
701 : : } // namespace cvc5::internal::parser
|
