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.

2 files changed, 27 insertions, 17 deletions

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 710381f9b..1584af893 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -770,6 +770,29 @@ void Parser::attributeNotSupported(const std::string& attr) {
   }
 }
 
+size_t Parser::scopeLevel() const { return d_symman->scopeLevel(); }
+
+void Parser::pushScope(bool bindingLevel)
+{
+  d_symman->pushScope();
+  if (!bindingLevel)
+  {
+    d_assertionLevel = scopeLevel();
+  }
+}
+
+void Parser::popScope()
+{
+  d_symman->popScope();
+  if (scopeLevel() < d_assertionLevel)
+  {
+    d_assertionLevel = scopeLevel();
+    d_reservedSymbols.clear();
+  }
+}
+
+void Parser::reset() { d_symman->reset(); }
+
 std::vector<unsigned> Parser::processAdHocStringEsc(const std::string& s)
 {
   std::vector<unsigned> str;
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;