diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-12 07:21:09 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-11-12 07:21:09 -0600 |
commit | f980e08b00ca9691f1f566455db446786994601b (patch) | |
tree | b845d9e74b972f635089fd564461f21aecffdfab /src/parser/parser.h | |
parent | 80930ce4f6d21b417028a5ec207ddfbd7d85e66d (diff) |
Make symbol manager context dependent (#5424)
This follows a similar style to symbol_table.h/cpp. This is required since context dependent data structures are cvc4_private, and symbol manager is cvc4_public.
Diffstat (limited to 'src/parser/parser.h')
-rw-r--r-- | src/parser/parser.h | 21 |
1 files changed, 4 insertions, 17 deletions
diff --git a/src/parser/parser.h b/src/parser/parser.h index c762fc117..8987b928b 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -751,7 +751,7 @@ public: /** * Gets the current declaration level. */ - inline size_t scopeLevel() const { return d_symtab->getLevel(); } + size_t scopeLevel() const; /** * Pushes a scope. All subsequent symbol declarations made are only valid in @@ -761,24 +761,11 @@ public: * current scope level. This determines which scope assertions are declared * at. */ - inline void pushScope(bool bindingLevel = false) { - d_symtab->pushScope(); - if(!bindingLevel) { - d_assertionLevel = scopeLevel(); - } - } + void pushScope(bool bindingLevel = false); - inline void popScope() { - d_symtab->popScope(); - if(scopeLevel() < d_assertionLevel) { - d_assertionLevel = scopeLevel(); - d_reservedSymbols.clear(); - } - } + void popScope(); - virtual void reset() { - d_symtab->reset(); - } + virtual void reset(); void setGlobalDeclarations(bool flag) { d_globalDeclarations = flag; |