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