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.

diff --git a/src/expr/symbol_manager.cpp b/src/expr/symbol_manager.cpp
index 3247e96099d45de0d9a4beb17e6fbd7d06697301..be3673d326f218808aaebcd34c03ab03b6c11d21 100644 (file)
--- a/src/expr/symbol_manager.cpp
+++ b/src/expr/symbol_manager.cpp
@@ -16,6 +16,7 @@
 
 #include "context/cdhashmap.h"
 #include "context/cdhashset.h"
+#include "context/cdo.h"
 
 using namespace CVC4::context;
 
@@ -30,7 +31,10 @@ class SymbolManager::Implementation
 
  public:
   Implementation()
-      : d_context(), d_names(&d_context), d_namedAsserts(&d_context)
+      : d_context(),
+        d_names(&d_context),
+        d_namedAsserts(&d_context),
+        d_hasPushedScope(&d_context, false)
   {
   }
 
@@ -49,6 +53,10 @@ class SymbolManager::Implementation
                           bool areAssertions = false) const;
   /** reset */
   void reset();
+  /** Push a scope in the expression names. */
+  void pushScope(bool isUserContext);
+  /** Pop a scope in the expression names. */
+  void popScope();
 
  private:
   /** The context manager for the scope maps. */
@@ -57,12 +65,19 @@ class SymbolManager::Implementation
   TermStringMap d_names;
   /** The set of terms with assertion names */
   TermSet d_namedAsserts;
+  /**
+   * Have we pushed a scope (e.g. a let or quantifier) in the current context?
+   */
+  CDO<bool> d_hasPushedScope;
 };
 
 bool SymbolManager::Implementation::setExpressionName(api::Term t,
                                                       const std::string& name,
                                                       bool isAssertion)
 {
+  // cannot name subexpressions under quantifiers
+  PrettyCheckArgument(
+      !d_hasPushedScope.get(), name, "cannot name function in a scope");
   if (d_names.find(t) != d_names.end())
   {
     // already named assertion
@@ -112,6 +127,24 @@ void SymbolManager::Implementation::getExpressionNames(
   }
 }
 
+void SymbolManager::Implementation::pushScope(bool isUserContext)
+{
+  d_context.push();
+  if (!isUserContext)
+  {
+    d_hasPushedScope = true;
+  }
+}
+
+void SymbolManager::Implementation::popScope()
+{
+  if (d_context.getLevel() == 0)
+  {
+    throw ScopeException();
+  }
+  d_context.pop();
+}
+
 void SymbolManager::Implementation::reset()
 {
   // clear names?
@@ -120,7 +153,9 @@ void SymbolManager::Implementation::reset()
 // ---------------------------------------------- SymbolManager
 
 SymbolManager::SymbolManager(api::Solver* s)
-    : d_solver(s), d_implementation(new SymbolManager::Implementation())
+    : d_solver(s),
+      d_implementation(new SymbolManager::Implementation()),
+      d_globalDeclarations(false)
 {
 }
 
@@ -154,10 +189,24 @@ size_t SymbolManager::scopeLevel() const
   return d_symtabAllocated.getLevel();
 }
 
-void SymbolManager::pushScope() { d_symtabAllocated.pushScope(); }
+void SymbolManager::pushScope(bool isUserContext)
+{
+  d_implementation->pushScope(isUserContext);
+  d_symtabAllocated.pushScope();
+}
 
 void SymbolManager::popScope() { d_symtabAllocated.popScope(); }
 
+void SymbolManager::setGlobalDeclarations(bool flag)
+{
+  d_globalDeclarations = flag;
+}
+
+bool SymbolManager::getGlobalDeclarations() const
+{
+  return d_globalDeclarations;
+}
+
 void SymbolManager::reset()
 {
   d_symtabAllocated.reset();

diff --git a/src/expr/symbol_manager.h b/src/expr/symbol_manager.h
index 412621b8a626dce9d9d8972c53504be8b2f4df27..54f9732b919115581483b367ea1ae418c05fc2a8 100644 (file)
--- a/src/expr/symbol_manager.h
+++ b/src/expr/symbol_manager.h
@@ -91,8 +91,12 @@ class CVC4_PUBLIC SymbolManager
   size_t scopeLevel() const;
   /**
    * Push a scope in the symbol table.
+   *
+   * @param isUserContext If true, this push is denoting a push of the user
+   * context, e.g. via an smt2 push/pop command. Otherwise, this push is
+   * due to a let/quantifier binding.
    */
-  void pushScope();
+  void pushScope(bool isUserContext);
   /**
    * Pop a scope in the symbol table.
    */
@@ -101,6 +105,10 @@ class CVC4_PUBLIC SymbolManager
    * Reset this symbol manager, which resets the symbol table.
    */
   void reset();
+  /** Set global declarations to the value flag. */
+  void setGlobalDeclarations(bool flag);
+  /** Get global declarations flag. */
+  bool getGlobalDeclarations() const;
 
  private:
   /** The API Solver object. */
@@ -112,6 +120,11 @@ class CVC4_PUBLIC SymbolManager
   /** The implementation of the symbol manager */
   class Implementation;
   std::unique_ptr<Implementation> d_implementation;
+  /**
+   * Whether the global declarations option is enabled. This corresponds to the
+   * SMT-LIB option :global-declarations. By default, its value is false.
+   */
+  bool d_globalDeclarations;
 };
 
 }  // namespace CVC4

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 1584af8936f3066146098b91653c8c23c5f45214..def89e6b1a6391b6b1008414f128e38cfdfa4bb2 100644 (file)
--- 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 8987b928b4d9b4fdcdb8f5fbff9fd9abf4394c55..d30ea7c16665578634e5a6befe60e0749786d9b6 100644 (file)
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -127,12 +127,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
@@ -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 40c66eaa52be25caf1daca12847de7f98a8facd8..a966861352192b728f184090437cf7b0def6eb74 100644 (file)
--- 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);
     }