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.

4 files changed, 153 insertions, 35 deletions

diff --git a/src/expr/symbol_manager.cpp b/src/expr/symbol_manager.cpp
index ac3b5d211..3247e9609 100644
--- a/src/expr/symbol_manager.cpp
+++ b/src/expr/symbol_manager.cpp
@@ -14,15 +14,54 @@
 
 #include "expr/symbol_manager.h"
 
+#include "context/cdhashmap.h"
+#include "context/cdhashset.h"
+
+using namespace CVC4::context;
+
 namespace CVC4 {
 
-SymbolManager::SymbolManager(api::Solver* s) : d_solver(s) {}
+// ---------------------------------------------- SymbolManager::Implementation
 
-SymbolTable* SymbolManager::getSymbolTable() { return &d_symtabAllocated; }
+class SymbolManager::Implementation
+{
+  using TermStringMap = CDHashMap<api::Term, std::string, api::TermHashFunction>;
+  using TermSet = CDHashSet<api::Term, api::TermHashFunction>;
 
-bool SymbolManager::setExpressionName(api::Term t,
-                                      const std::string& name,
-                                      bool isAssertion)
+ public:
+  Implementation()
+      : d_context(), d_names(&d_context), d_namedAsserts(&d_context)
+  {
+  }
+
+  ~Implementation() {}
+  /** set expression name */
+  bool setExpressionName(api::Term t,
+                         const std::string& name,
+                         bool isAssertion = false);
+  /** get expression name */
+  bool getExpressionName(api::Term t,
+                         std::string& name,
+                         bool isAssertion = false) const;
+  /** get expression names */
+  void getExpressionNames(const std::vector<api::Term>& ts,
+                          std::vector<std::string>& names,
+                          bool areAssertions = false) const;
+  /** reset */
+  void reset();
+
+ private:
+  /** The context manager for the scope maps. */
+  Context d_context;
+  /** Map terms to names */
+  TermStringMap d_names;
+  /** The set of terms with assertion names */
+  TermSet d_namedAsserts;
+};
+
+bool SymbolManager::Implementation::setExpressionName(api::Term t,
+                                                      const std::string& name,
+                                                      bool isAssertion)
 {
   if (d_names.find(t) != d_names.end())
   {
@@ -37,11 +76,11 @@ bool SymbolManager::setExpressionName(api::Term t,
   return true;
 }
 
-bool SymbolManager::getExpressionName(api::Term t,
-                                      std::string& name,
-                                      bool isAssertion) const
+bool SymbolManager::Implementation::getExpressionName(api::Term t,
+                                                      std::string& name,
+                                                      bool isAssertion) const
 {
-  std::map<api::Term, std::string>::const_iterator it = d_names.find(t);
+  TermStringMap::const_iterator it = d_names.find(t);
   if (it == d_names.end())
   {
     return false;
@@ -54,13 +93,14 @@ bool SymbolManager::getExpressionName(api::Term t,
       return false;
     }
   }
-  name = it->second;
+  name = (*it).second;
   return true;
 }
 
-void SymbolManager::getExpressionNames(const std::vector<api::Term>& ts,
-                                       std::vector<std::string>& names,
-                                       bool areAssertions) const
+void SymbolManager::Implementation::getExpressionNames(
+    const std::vector<api::Term>& ts,
+    std::vector<std::string>& names,
+    bool areAssertions) const
 {
   for (const api::Term& t : ts)
   {
@@ -72,4 +112,56 @@ void SymbolManager::getExpressionNames(const std::vector<api::Term>& ts,
   }
 }
 
+void SymbolManager::Implementation::reset()
+{
+  // clear names?
+}
+
+// ---------------------------------------------- SymbolManager
+
+SymbolManager::SymbolManager(api::Solver* s)
+    : d_solver(s), d_implementation(new SymbolManager::Implementation())
+{
+}
+
+SymbolManager::~SymbolManager() {}
+
+SymbolTable* SymbolManager::getSymbolTable() { return &d_symtabAllocated; }
+
+bool SymbolManager::setExpressionName(api::Term t,
+                                      const std::string& name,
+                                      bool isAssertion)
+{
+  return d_implementation->setExpressionName(t, name, isAssertion);
+}
+
+bool SymbolManager::getExpressionName(api::Term t,
+                                      std::string& name,
+                                      bool isAssertion) const
+{
+  return d_implementation->getExpressionName(t, name, isAssertion);
+}
+
+void SymbolManager::getExpressionNames(const std::vector<api::Term>& ts,
+                                       std::vector<std::string>& names,
+                                       bool areAssertions) const
+{
+  return d_implementation->getExpressionNames(ts, names, areAssertions);
+}
+
+size_t SymbolManager::scopeLevel() const
+{
+  return d_symtabAllocated.getLevel();
+}
+
+void SymbolManager::pushScope() { d_symtabAllocated.pushScope(); }
+
+void SymbolManager::popScope() { d_symtabAllocated.popScope(); }
+
+void SymbolManager::reset()
+{
+  d_symtabAllocated.reset();
+  d_implementation->reset();
+}
+
 }  // namespace CVC4
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
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;