Add more features to symbol manager (#5434)

This is in preparation for having the symbol manager manage expression names at the parser level instead of inside SmtEngine.

This adds some necessary features regarding scopes and global declarations.

This PR still does not change the behavior of the parser.

1 files changed, 2 insertions, 15 deletions

diff --git a/src/parser/parser.h b/src/parser/parser.h
index 8987b928b..d30ea7c16 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -128,12 +128,6 @@ private:
  size_t d_assertionLevel;
 
  /**
-  * Whether we're in global declarations mode (all definitions and
-  * declarations are global).
-  */
- bool d_globalDeclarations;
-
- /**
   * Maintains a list of reserved symbols at the assertion level that might
   * not occur in our symbol table.  This is necessary to e.g. support the
   * proper behavior of the :named annotation in SMT-LIBv2 when used under
@@ -767,15 +761,8 @@ public:
 
   virtual void reset();
 
-  void setGlobalDeclarations(bool flag) {
-    d_globalDeclarations = flag;
-  }
-
-  bool getGlobalDeclarations() { return d_globalDeclarations; }
-
-  inline SymbolTable* getSymbolTable() const {
-    return d_symtab;
-  }
+  /** Return the symbol manager used by this parser. */
+  SymbolManager* getSymbolManager();
 
   //------------------------ operator overloading
   /** is this function overloaded? */