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.

diff --git a/src/expr/symbol_manager.cpp b/src/expr/symbol_manager.cpp
index be3673d326f218808aaebcd34c03ab03b6c11d21..75ffa4f620b0b6175d6d33e9b2c1eef3899cc39b 100644 (file)
--- 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 54f9732b919115581483b367ea1ae418c05fc2a8..a3ca8e780d2eda13dad0bb8c666365a575e299ce 100644 (file)
--- 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.

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index def89e6b1a6391b6b1008414f128e38cfdfa4bb2..c5746020c86679c242ee8c20b04492d53d898efb 100644 (file)
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -775,10 +775,10 @@ void Parser::attributeNotSupported(const std::string& attr) {
 
 size_t Parser::scopeLevel() const { return d_symman->scopeLevel(); }
 
-void Parser::pushScope(bool bindingLevel)
+void Parser::pushScope(bool isUserContext)
 {
-  d_symman->pushScope(!bindingLevel);
-  if (!bindingLevel)
+  d_symman->pushScope(isUserContext);
+  if (isUserContext)
   {
     d_assertionLevel = scopeLevel();
   }

diff --git a/src/parser/parser.h b/src/parser/parser.h
index d30ea7c16665578634e5a6befe60e0749786d9b6..96a16b31f6967f9d49f9dc11ca5c81a5c19d39b5 100644 (file)
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -751,11 +751,13 @@ public:
    * Pushes a scope. All subsequent symbol declarations made are only valid in
    * this scope, i.e. they are deleted on the next call to popScope.
    *
-   * The argument bindingLevel is true, the assertion level is set to the
-   * current scope level. This determines which scope assertions are declared
-   * at.
+   * The argument isUserContext is true, when we are pushing a user context
+   * e.g. via the smt2 command (push n). This may also include one initial
+   * pushScope when the parser is initialized. User-context pushes and pops
+   * have an impact on both expression names and the symbol table, whereas
+   * other pushes and pops only have an impact on the symbol table.
    */
-  void pushScope(bool bindingLevel = false);
+  void pushScope(bool isUserContext = false);
 
   void popScope();
 

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index a966861352192b728f184090437cf7b0def6eb74..916e20d9bfffb29720de2e1158d33ea689f4f734 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -258,7 +258,7 @@ command [std::unique_ptr<CVC4::Command>* cmd]
     symbol[name,CHECK_UNDECLARED,SYM_SORT]
     { PARSER_STATE->checkUserSymbol(name); }
     LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK
-    { PARSER_STATE->pushScope(true);
+    { PARSER_STATE->pushScope();
       for(std::vector<std::string>::const_iterator i = names.begin(),
             iend = names.end();
           i != iend;
@@ -319,7 +319,7 @@ command [std::unique_ptr<CVC4::Command>* cmd]
       }
 
       t = PARSER_STATE->mkFlatFunctionType(sorts, t, flattenVars);
-      PARSER_STATE->pushScope(true);
+      PARSER_STATE->pushScope();
       terms = PARSER_STATE->bindBoundVars(sortedVarNames);
     }
     term[expr, expr2]
@@ -365,6 +365,8 @@ command [std::unique_ptr<CVC4::Command>* cmd]
         // set the expression name, if there was a named term
         std::pair<api::Term, std::string> namedTerm =
             PARSER_STATE->lastNamedTerm();
+        // TODO (projects-248)
+        // SYM_MAN->setExpressionName(namedTerm.first, namedTerm.second, true);
         Command* csen =
             new SetExpressionNameCommand(namedTerm.first, namedTerm.second);
         csen->setMuted(true);
@@ -422,12 +424,12 @@ command [std::unique_ptr<CVC4::Command>* cmd]
         if(num == 0) {
           cmd->reset(new EmptyCommand());
         } else if(num == 1) {
-          PARSER_STATE->pushScope();
+          PARSER_STATE->pushScope(true);
           cmd->reset(new PushCommand());
         } else {
           std::unique_ptr<CommandSequence> seq(new CommandSequence());
           do {
-            PARSER_STATE->pushScope();
+            PARSER_STATE->pushScope(true);
             Command* push_cmd = new PushCommand();
             push_cmd->setMuted(num > 1);
             seq->addCommand(push_cmd);
@@ -441,7 +443,7 @@ command [std::unique_ptr<CVC4::Command>* cmd]
               "Strict compliance mode demands an integer to be provided to "
               "PUSH.  Maybe you want (push 1)?");
         } else {
-          PARSER_STATE->pushScope();
+          PARSER_STATE->pushScope(true);
           cmd->reset(new PushCommand());
         }
       } )
@@ -549,7 +551,7 @@ sygusCommand returns [std::unique_ptr<CVC4::Command> cmd]
     LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
     ( sortSymbol[range,CHECK_DECLARED] )?
     {
-      PARSER_STATE->pushScope(true);
+      PARSER_STATE->pushScope();
       sygusVars = PARSER_STATE->bindBoundVars(sortedVarNames);
     }
     (
@@ -661,7 +663,7 @@ sygusGrammar[CVC4::api::Grammar*& ret,
   RPAREN_TOK
   {
     // non-terminal symbols in the pre-declaration are locally scoped
-    PARSER_STATE->pushScope(true);
+    PARSER_STATE->pushScope();
     for (std::pair<std::string, api::Sort>& i : sortedVarNames)
     {
       PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_SORT);
@@ -818,7 +820,7 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd]
       func =
           PARSER_STATE->bindDefineFunRec(fname, sortedVarNames, t, flattenVars);
       PARSER_STATE->pushDefineFunRecScope(
-          sortedVarNames, func, flattenVars, bvs, true);
+          sortedVarNames, func, flattenVars, bvs);
     }
     term[expr, expr2]
     { PARSER_STATE->popScope();
@@ -862,7 +864,7 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd]
       }
       bvs.clear();
       PARSER_STATE->pushDefineFunRecScope( sortedVarNamesList[0], funcs[0],
-                                           flattenVarsList[0], bvs, true);
+                                           flattenVarsList[0], bvs);
     }
     (
     term[expr,expr2]
@@ -879,7 +881,7 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd]
       if( func_defs.size()<funcs.size() ){
         bvs.clear();
         PARSER_STATE->pushDefineFunRecScope( sortedVarNamesList[j], funcs[j],
-                                             flattenVarsList[j], bvs, true);
+                                             flattenVarsList[j], bvs);
       }
     }
     )+
@@ -996,7 +998,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
       sortedVarList[sortedVarNames] RPAREN_TOK
       { /* add variables to parser state before parsing term */
         Debug("parser") << "define fun: '" << name << "'" << std::endl;
-        PARSER_STATE->pushScope(true);
+        PARSER_STATE->pushScope();
         terms = PARSER_STATE->bindBoundVars(sortedVarNames);
       }
       term[e,e2]
@@ -1028,7 +1030,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
     sortSymbol[t,CHECK_DECLARED]
     { /* add variables to parser state before parsing term */
       Debug("parser") << "define const: '" << name << "'" << std::endl;
-      PARSER_STATE->pushScope(true);
+      PARSER_STATE->pushScope();
       terms = PARSER_STATE->bindBoundVars(sortedVarNames);
     }
     term[e, e2]
@@ -1104,7 +1106,7 @@ datatypes_2_5_DefCommand[bool isCo, std::unique_ptr<CVC4::Command>* cmd]
 }
   : { PARSER_STATE->checkThatLogicIsSet();
     /* open a scope to keep the UnresolvedTypes contained */
-    PARSER_STATE->pushScope(true); }
+    PARSER_STATE->pushScope(); }
   LPAREN_TOK /* parametric sorts */
   ( symbol[name,CHECK_UNDECLARED,SYM_SORT]
     {
@@ -1174,7 +1176,7 @@ datatypesDef[bool isCo,
   std::string name;
   std::vector<api::Sort> params;
 }
-  : { PARSER_STATE->pushScope(true);
+  : { PARSER_STATE->pushScope();
       // Declare the datatypes that are currently being defined as unresolved
       // types. If we do not know the arity of the datatype yet, we wait to
       // define it until parsing the preamble of its body, which may optionally
@@ -1201,7 +1203,7 @@ datatypesDef[bool isCo,
         PARSER_STATE->parseError("Too many datatypes defined in this block.");
       }
     }
-    ( PAR_TOK { PARSER_STATE->pushScope(true); } LPAREN_TOK
+    ( PAR_TOK { PARSER_STATE->pushScope(); } LPAREN_TOK
       ( symbol[name,CHECK_UNDECLARED,SYM_SORT]
         {
           params.push_back( PARSER_STATE->mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER)); }
@@ -1362,7 +1364,7 @@ termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2]
       {
         PARSER_STATE->parseError("Quantifier used in non-quantified logic.");
       }
-      PARSER_STATE->pushScope(true);
+      PARSER_STATE->pushScope();
     }
     boundVarList[bvl]
     term[f, f2] RPAREN_TOK
@@ -1377,7 +1379,7 @@ termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2]
       expr = MK_TERM(kind, args);
     }
   | LPAREN_TOK COMPREHENSION_TOK
-    { PARSER_STATE->pushScope(true); }
+    { PARSER_STATE->pushScope(); }
     boundVarList[bvl]
     {
       args.push_back(bvl);
@@ -1396,7 +1398,7 @@ termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2]
   | /* a let or sygus let binding */
     LPAREN_TOK 
       LET_TOK LPAREN_TOK
-      { PARSER_STATE->pushScope(true); }
+      { PARSER_STATE->pushScope(); }
       ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE]
         term[expr, f2]
         RPAREN_TOK
@@ -1434,7 +1436,7 @@ termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2]
       // case with non-nullary pattern
       LPAREN_TOK LPAREN_TOK term[f, f2] {
           args.clear();
-          PARSER_STATE->pushScope(true);
+          PARSER_STATE->pushScope();
           // f should be a constructor
           type = f.getSort();
           Debug("parser-dt") << "Pattern head : " << f << " " << type << std::endl;
@@ -1553,7 +1555,7 @@ termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2]
     }
   | /* lambda */
     LPAREN_TOK HO_LAMBDA_TOK
-    { PARSER_STATE->pushScope(true); }
+    { PARSER_STATE->pushScope(); }
     boundVarList[bvl]
     term[f, f2] RPAREN_TOK
     {
@@ -1842,6 +1844,7 @@ attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr]
       api::Term func = PARSER_STATE->setNamedAttribute(expr, sexpr);
       std::string name = sexpr.getValue();
       // bind name to expr with define-fun
+      // TODO (projects-248) SYM_MAN->setExpressionName(func, name, false);
       Command* c =
           new DefineNamedFunctionCommand(name,
                                          func,
@@ -2180,7 +2183,7 @@ datatypeDef[bool isCo, std::vector<CVC4::api::DatatypeDecl>& datatypes,
      * datatypes won't work, because this type will already be
      * "defined" as an unresolved type; don't worry, we check
      * below. */
-  : symbol[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(true); }
+  : symbol[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(); }
     {
       datatypes.push_back(SOLVER->mkDatatypeDecl(id, params, isCo));
     }

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 1decb3b1c517c30dde66ccdf48fbf7a0e5ae1829..892c628dc8aa36e621e78bdb7c56923f86ce7290 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -452,10 +452,9 @@ void Smt2::pushDefineFunRecScope(
     const std::vector<std::pair<std::string, api::Sort>>& sortedVarNames,
     api::Term func,
     const std::vector<api::Term>& flattenVars,
-    std::vector<api::Term>& bvs,
-    bool bindingLevel)
+    std::vector<api::Term>& bvs)
 {
-  pushScope(bindingLevel);
+  pushScope();
 
   // bound variables are those that are explicitly named in the preamble
   // of the define-fun(s)-rec command, we define them here

diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index eeedbec557aa8fbf7067a5005f0e539e9d45a21e..734b00f921d03911182a97a79933de08ee11bbb7 100644 (file)
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -169,7 +169,7 @@ class Smt2 : public Parser
 
   /** Push scope for define-fun-rec
    *
-   * This calls Parser::pushScope(bindingLevel) and sets up
+   * This calls Parser::pushScope() and sets up
    * initial information for reading a body of a function definition
    * in the define-fun-rec and define-funs-rec command.
    * The input parameters func/flattenVars are the result
@@ -180,7 +180,7 @@ class Smt2 : public Parser
    * flattenVars : the implicit variables introduced when defining func.
    *
    * This function:
-   * (1) Calls Parser::pushScope(bindingLevel).
+   * (1) Calls Parser::pushScope().
    * (2) Computes the bound variable list for the quantified formula
    *     that defined this definition and stores it in bvs.
    */
@@ -188,8 +188,7 @@ class Smt2 : public Parser
       const std::vector<std::pair<std::string, api::Sort>>& sortedVarNames,
       api::Term func,
       const std::vector<api::Term>& flattenVars,
-      std::vector<api::Term>& bvs,
-      bool bindingLevel = false);
+      std::vector<api::Term>& bvs);
 
   void reset() override;