1 files changed, 21 insertions, 5 deletions
diff --git a/src/expr/symbol_manager.h b/src/expr/symbol_manager.h
index 4890ed994..412621b8a 100644
--- a/src/expr/symbol_manager.h
+++ b/src/expr/symbol_manager.h
@@ -18,6 +18,7 @@
 #define CVC4__EXPR__SYMBOL_MANAGER_H
 
 #include <map>
+#include <memory>
 #include <set>
 #include <string>
 
@@ -38,7 +39,7 @@ class CVC4_PUBLIC SymbolManager
 {
  public:
   SymbolManager(api::Solver* s);
-  ~SymbolManager() {}
+  ~SymbolManager();
   /** Get the underlying symbol table */
   SymbolTable* getSymbolTable();
   //---------------------------- named expressions
@@ -84,6 +85,22 @@ class CVC4_PUBLIC SymbolManager
                           std::vector<std::string>& names,
                           bool areAssertions = false) const;
   //---------------------------- end named expressions
+  /**
+   * Get the scope level of the symbol table.
+   */
+  size_t scopeLevel() const;
+  /**
+   * Push a scope in the symbol table.
+   */
+  void pushScope();
+  /**
+   * Pop a scope in the symbol table.
+   */
+  void popScope();
+  /**
+   * Reset this symbol manager, which resets the symbol table.
+   */
+  void reset();
 
  private:
   /** The API Solver object. */
@@ -92,10 +109,9 @@ class CVC4_PUBLIC SymbolManager
    * The declaration scope that is "owned" by this symbol manager.
    */
   SymbolTable d_symtabAllocated;
-  /** Map terms to names */
-  std::map<api::Term, std::string> d_names;
-  /** The set of terms with assertion names */
-  std::set<api::Term> d_namedAsserts;
+  /** The implementation of the symbol manager */
+  class Implementation;
+  std::unique_ptr<Implementation> d_implementation;
 };
 
 }  // namespace CVC4