Cleaning up scopes in preparation for symbol manager (#5442)

This changes the default of Parser::pushScope and prepares symbol manager further for maintaining expression names.

2 files changed, 47 insertions, 1 deletions

diff --git a/src/expr/symbol_manager.cpp b/src/expr/symbol_manager.cpp
index be3673d32..75ffa4f62 100644
--- a/src/expr/symbol_manager.cpp
+++ b/src/expr/symbol_manager.cpp
@@ -51,6 +51,8 @@ class SymbolManager::Implementation
   void getExpressionNames(const std::vector<api::Term>& ts,
                           std::vector<std::string>& names,
                           bool areAssertions = false) const;
+  /** get expression names */
+  std::map<api::Term, std::string> getExpressionNames(bool areAssertions) const;
   /** reset */
   void reset();
   /** Push a scope in the expression names. */
@@ -127,8 +129,31 @@ void SymbolManager::Implementation::getExpressionNames(
   }
 }
 
+std::map<api::Term, std::string>
+SymbolManager::Implementation::getExpressionNames(bool areAssertions) const
+{
+  std::map<api::Term, std::string> emap;
+  for (TermStringMap::const_iterator it = d_names.begin(),
+                                     itend = d_names.end();
+       it != itend;
+       ++it)
+  {
+    api::Term t = (*it).first;
+    if (areAssertions && d_namedAsserts.find(t) == d_namedAsserts.end())
+    {
+      continue;
+    }
+    emap[t] = (*it).second;
+  }
+  return emap;
+}
+
 void SymbolManager::Implementation::pushScope(bool isUserContext)
 {
+  Trace("sym-manager") << "pushScope, isUserContext = " << isUserContext
+                       << std::endl;
+  PrettyCheckArgument(!d_hasPushedScope.get() || !isUserContext,
+                      "cannot push a user context within a scope context");
   d_context.push();
   if (!isUserContext)
   {
@@ -138,11 +163,14 @@ void SymbolManager::Implementation::pushScope(bool isUserContext)
 
 void SymbolManager::Implementation::popScope()
 {
+  Trace("sym-manager") << "popScope" << std::endl;
   if (d_context.getLevel() == 0)
   {
     throw ScopeException();
   }
   d_context.pop();
+  Trace("sym-manager-debug")
+      << "d_hasPushedScope is now " << d_hasPushedScope.get() << std::endl;
 }
 
 void SymbolManager::Implementation::reset()
@@ -184,6 +212,12 @@ void SymbolManager::getExpressionNames(const std::vector<api::Term>& ts,
   return d_implementation->getExpressionNames(ts, names, areAssertions);
 }
 
+std::map<api::Term, std::string> SymbolManager::getExpressionNames(
+    bool areAssertions) const
+{
+  return d_implementation->getExpressionNames(areAssertions);
+}
+
 size_t SymbolManager::scopeLevel() const
 {
   return d_symtabAllocated.getLevel();
@@ -195,7 +229,11 @@ void SymbolManager::pushScope(bool isUserContext)
   d_symtabAllocated.pushScope();
 }
 
-void SymbolManager::popScope() { d_symtabAllocated.popScope(); }
+void SymbolManager::popScope()
+{
+  d_symtabAllocated.popScope();
+  d_implementation->popScope();
+}
 
 void SymbolManager::setGlobalDeclarations(bool flag)
 {
diff --git a/src/expr/symbol_manager.h b/src/expr/symbol_manager.h
index 54f9732b9..a3ca8e780 100644
--- a/src/expr/symbol_manager.h
+++ b/src/expr/symbol_manager.h
@@ -84,6 +84,14 @@ class CVC4_PUBLIC SymbolManager
   void getExpressionNames(const std::vector<api::Term>& ts,
                           std::vector<std::string>& names,
                           bool areAssertions = false) const;
+  /**
+   * Get a mapping of all expression names.
+   *
+   * @param areAssertions Whether we only wish to include assertion names
+   * @return the mapping containing all expression names.
+   */
+  std::map<api::Term, std::string> getExpressionNames(
+      bool areAssertions = false) const;
   //---------------------------- end named expressions
   /**
    * Get the scope level of the symbol table.