diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-16 10:40:30 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-11-16 10:40:30 -0600 |
commit | a24a67080965f676335388c177d7eb8a9d3fdb13 (patch) | |
tree | dd34520a8206a8d42d28aaca6df15b7879f6b831 /src/expr/symbol_manager.cpp | |
parent | db84323caa3009cf418f959313e49f5bea5d35a6 (diff) |
Cleaning up scopes in preparation for symbol manager (#5442)
This changes the default of Parser::pushScope and prepares symbol manager further for maintaining expression names.
Diffstat (limited to 'src/expr/symbol_manager.cpp')
-rw-r--r-- | src/expr/symbol_manager.cpp | 40 |
1 files changed, 39 insertions, 1 deletions
diff --git a/src/expr/symbol_manager.cpp b/src/expr/symbol_manager.cpp index be3673d32..75ffa4f62 100644 --- a/src/expr/symbol_manager.cpp +++ b/src/expr/symbol_manager.cpp @@ -51,6 +51,8 @@ class SymbolManager::Implementation void getExpressionNames(const std::vector<api::Term>& ts, std::vector<std::string>& names, bool areAssertions = false) const; + /** get expression names */ + std::map<api::Term, std::string> getExpressionNames(bool areAssertions) const; /** reset */ void reset(); /** Push a scope in the expression names. */ @@ -127,8 +129,31 @@ void SymbolManager::Implementation::getExpressionNames( } } +std::map<api::Term, std::string> +SymbolManager::Implementation::getExpressionNames(bool areAssertions) const +{ + std::map<api::Term, std::string> emap; + for (TermStringMap::const_iterator it = d_names.begin(), + itend = d_names.end(); + it != itend; + ++it) + { + api::Term t = (*it).first; + if (areAssertions && d_namedAsserts.find(t) == d_namedAsserts.end()) + { + continue; + } + emap[t] = (*it).second; + } + return emap; +} + void SymbolManager::Implementation::pushScope(bool isUserContext) { + Trace("sym-manager") << "pushScope, isUserContext = " << isUserContext + << std::endl; + PrettyCheckArgument(!d_hasPushedScope.get() || !isUserContext, + "cannot push a user context within a scope context"); d_context.push(); if (!isUserContext) { @@ -138,11 +163,14 @@ void SymbolManager::Implementation::pushScope(bool isUserContext) void SymbolManager::Implementation::popScope() { + Trace("sym-manager") << "popScope" << std::endl; if (d_context.getLevel() == 0) { throw ScopeException(); } d_context.pop(); + Trace("sym-manager-debug") + << "d_hasPushedScope is now " << d_hasPushedScope.get() << std::endl; } void SymbolManager::Implementation::reset() @@ -184,6 +212,12 @@ void SymbolManager::getExpressionNames(const std::vector<api::Term>& ts, return d_implementation->getExpressionNames(ts, names, areAssertions); } +std::map<api::Term, std::string> SymbolManager::getExpressionNames( + bool areAssertions) const +{ + return d_implementation->getExpressionNames(areAssertions); +} + size_t SymbolManager::scopeLevel() const { return d_symtabAllocated.getLevel(); @@ -195,7 +229,11 @@ void SymbolManager::pushScope(bool isUserContext) d_symtabAllocated.pushScope(); } -void SymbolManager::popScope() { d_symtabAllocated.popScope(); } +void SymbolManager::popScope() +{ + d_symtabAllocated.popScope(); + d_implementation->popScope(); +} void SymbolManager::setGlobalDeclarations(bool flag) { |