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.

3 files changed, 38 insertions, 43 deletions

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 1584af893..def89e6b1 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -50,7 +50,6 @@ Parser::Parser(api::Solver* solver,
       d_symman(sm),
       d_symtab(sm->getSymbolTable()),
       d_assertionLevel(0),
-      d_globalDeclarations(false),
       d_anonymousFunctionCount(0),
       d_done(false),
       d_checksEnabled(true),
@@ -205,7 +204,8 @@ api::Term Parser::bindVar(const std::string& name,
                           uint32_t flags,
                           bool doOverload)
 {
-  if (d_globalDeclarations) {
+  if (d_symman->getGlobalDeclarations())
+  {
     flags |= ExprManager::VAR_FLAG_GLOBAL;
   }
   Debug("parser") << "bindVar(" << name << ", " << type << ")" << std::endl;
@@ -238,7 +238,9 @@ api::Term Parser::mkAnonymousFunction(const std::string& prefix,
                                       const api::Sort& type,
                                       uint32_t flags)
 {
-  if (d_globalDeclarations) {
+  bool globalDecls = d_symman->getGlobalDeclarations();
+  if (globalDecls)
+  {
     flags |= ExprManager::VAR_FLAG_GLOBAL;
   }
   stringstream name;
@@ -251,7 +253,9 @@ std::vector<api::Term> Parser::bindVars(const std::vector<std::string> names,
                                         uint32_t flags,
                                         bool doOverload)
 {
-  if (d_globalDeclarations) {
+  bool globalDecls = d_symman->getGlobalDeclarations();
+  if (globalDecls)
+  {
     flags |= ExprManager::VAR_FLAG_GLOBAL;
   }
   std::vector<api::Term> vars;
@@ -333,10 +337,9 @@ api::Sort Parser::mkSort(const std::string& name, uint32_t flags)
   Debug("parser") << "newSort(" << name << ")" << std::endl;
   api::Sort type =
       api::Sort(d_solver, d_solver->getExprManager()->mkSort(name, flags));
+  bool globalDecls = d_symman->getGlobalDeclarations();
   defineType(
-      name,
-      type,
-      d_globalDeclarations && !(flags & ExprManager::SORT_FLAG_PLACEHOLDER));
+      name, type, globalDecls && !(flags & ExprManager::SORT_FLAG_PLACEHOLDER));
   return type;
 }
 
@@ -349,11 +352,11 @@ api::Sort Parser::mkSortConstructor(const std::string& name,
   api::Sort type = api::Sort(
       d_solver,
       d_solver->getExprManager()->mkSortConstructor(name, arity, flags));
-  defineType(
-      name,
-      vector<api::Sort>(arity),
-      type,
-      d_globalDeclarations && !(flags & ExprManager::SORT_FLAG_PLACEHOLDER));
+  bool globalDecls = d_symman->getGlobalDeclarations();
+  defineType(name,
+             vector<api::Sort>(arity),
+             type,
+             globalDecls && !(flags & ExprManager::SORT_FLAG_PLACEHOLDER));
   return type;
 }
 
@@ -412,6 +415,7 @@ std::vector<api::Sort> Parser::bindMutualDatatypeTypes(
         d_solver->mkDatatypeSorts(datatypes, d_unresolved);
 
     assert(datatypes.size() == types.size());
+    bool globalDecls = d_symman->getGlobalDeclarations();
 
     for (unsigned i = 0; i < datatypes.size(); ++i) {
       api::Sort t = types[i];
@@ -424,11 +428,11 @@ std::vector<api::Sort> Parser::bindMutualDatatypeTypes(
       if (t.isParametricDatatype())
       {
         std::vector<api::Sort> paramTypes = t.getDatatypeParamSorts();
-        defineType(name, paramTypes, t, d_globalDeclarations);
+        defineType(name, paramTypes, t, globalDecls);
       }
       else
       {
-        defineType(name, t, d_globalDeclarations);
+        defineType(name, t, globalDecls);
       }
       std::unordered_set< std::string > consNames;
       std::unordered_set< std::string > selNames;
@@ -442,8 +446,7 @@ std::vector<api::Sort> Parser::bindMutualDatatypeTypes(
           if(!doOverload) {
             checkDeclaration(constructorName, CHECK_UNDECLARED);
           }
-          defineVar(
-              constructorName, constructor, d_globalDeclarations, doOverload);
+          defineVar(constructorName, constructor, globalDecls, doOverload);
           consNames.insert(constructorName);
         }else{
           throw ParserException(constructorName + " already declared in this datatype");
@@ -457,7 +460,7 @@ std::vector<api::Sort> Parser::bindMutualDatatypeTypes(
           {
             checkDeclaration(testerName, CHECK_UNDECLARED);
           }
-          defineVar(testerName, tester, d_globalDeclarations, doOverload);
+          defineVar(testerName, tester, globalDecls, doOverload);
         }
         for (size_t k = 0, nargs = ctor.getNumSelectors(); k < nargs; k++)
         {
@@ -469,7 +472,7 @@ std::vector<api::Sort> Parser::bindMutualDatatypeTypes(
             if(!doOverload) {
               checkDeclaration(selectorName, CHECK_UNDECLARED);
             }
-            defineVar(selectorName, selector, d_globalDeclarations, doOverload);
+            defineVar(selectorName, selector, globalDecls, doOverload);
             selNames.insert(selectorName);
           }else{
             throw ParserException(selectorName + " already declared in this datatype");
@@ -774,7 +777,7 @@ size_t Parser::scopeLevel() const { return d_symman->scopeLevel(); }
 
 void Parser::pushScope(bool bindingLevel)
 {
-  d_symman->pushScope();
+  d_symman->pushScope(!bindingLevel);
   if (!bindingLevel)
   {
     d_assertionLevel = scopeLevel();
@@ -793,6 +796,8 @@ void Parser::popScope()
 
 void Parser::reset() { d_symman->reset(); }
 
+SymbolManager* Parser::getSymbolManager() { return d_symman; }
+
 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 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? */
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 40c66eaa5..a96686135 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -127,6 +127,8 @@ using namespace CVC4::parser;
 #define PARSER_STATE ((Smt2*)PARSER->super)
 #undef SOLVER
 #define SOLVER PARSER_STATE->getSolver()
+#undef SYM_MAN
+#define SYM_MAN PARSER_STATE->getSymbolManager()
 #undef MK_TERM
 #define MK_TERM SOLVER->mkTerm
 #define UNSUPPORTED PARSER_STATE->unimplementedFeature
@@ -336,7 +338,7 @@ command [std::unique_ptr<CVC4::Command>* cmd]
       api::Term func = PARSER_STATE->bindVar(name, t,
                                       ExprManager::VAR_FLAG_DEFINED, true);
       cmd->reset(new DefineFunctionCommand(
-          name, func, terms, expr, PARSER_STATE->getGlobalDeclarations()));
+          name, func, terms, expr, SYM_MAN->getGlobalDeclarations()));
     }
   | DECLARE_DATATYPE_TOK datatypeDefCommand[false, cmd]
   | DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd]
@@ -745,8 +747,9 @@ setOptionInternal[std::unique_ptr<CVC4::Command>* cmd]
       // Ugly that this changes the state of the parser; but
       // global-declarations affects parsing, so we can't hold off
       // on this until some SmtEngine eventually (if ever) executes it.
-      if(name == ":global-declarations") {
-        PARSER_STATE->setGlobalDeclarations(sexpr.getValue() == "true");
+      if(name == ":global-declarations")
+      {
+        SYM_MAN->setGlobalDeclarations(sexpr.getValue() == "true");
       }
     }
   ;
@@ -823,7 +826,7 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd]
         expr = PARSER_STATE->mkHoApply( expr, flattenVars );
       }
       cmd->reset(new DefineFunctionRecCommand(
-          func, bvs, expr, PARSER_STATE->getGlobalDeclarations()));
+          func, bvs, expr, SYM_MAN->getGlobalDeclarations()));
     }
   | DEFINE_FUNS_REC_TOK
     { PARSER_STATE->checkThatLogicIsSet();}
@@ -887,7 +890,7 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd]
             "define-funs-rec"));
       }
       cmd->reset(new DefineFunctionRecCommand(
-          funcs, formals, func_defs, PARSER_STATE->getGlobalDeclarations()));
+          funcs, formals, func_defs, SYM_MAN->getGlobalDeclarations()));
     }
   ;
 
@@ -984,7 +987,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
         api::Term func = PARSER_STATE->bindVar(name, e.getSort(),
                                         ExprManager::VAR_FLAG_DEFINED);
         cmd->reset(new DefineFunctionCommand(
-            name, func, e, PARSER_STATE->getGlobalDeclarations()));
+            name, func, e, SYM_MAN->getGlobalDeclarations()));
       }
     | // (define (f (v U) ...) t)
       LPAREN_TOK
@@ -1015,7 +1018,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
         api::Term func = PARSER_STATE->bindVar(name, tt,
                                         ExprManager::VAR_FLAG_DEFINED);
         cmd->reset(new DefineFunctionCommand(
-            name, func, terms, e, PARSER_STATE->getGlobalDeclarations()));
+            name, func, terms, e, SYM_MAN->getGlobalDeclarations()));
       }
     )
   | // (define-const x U t)
@@ -1037,7 +1040,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
       api::Term func = PARSER_STATE->bindVar(name, t,
                                       ExprManager::VAR_FLAG_DEFINED);
       cmd->reset(new DefineFunctionCommand(
-          name, func, terms, e, PARSER_STATE->getGlobalDeclarations()));
+          name, func, terms, e, SYM_MAN->getGlobalDeclarations()));
     }
 
   | SIMPLIFY_TOK { PARSER_STATE->checkThatLogicIsSet(); }
@@ -1844,7 +1847,7 @@ attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr]
                                          func,
                                          std::vector<api::Term>(),
                                          expr,
-                                         PARSER_STATE->getGlobalDeclarations());
+                                         SYM_MAN->getGlobalDeclarations());
       c->setMuted(true);
       PARSER_STATE->preemptCommand(c);
     }