From a24a67080965f676335388c177d7eb8a9d3fdb13 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 16 Nov 2020 10:40:30 -0600 Subject: [PATCH] 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. --- src/expr/symbol_manager.cpp | 40 ++++++++++++++++++++++++++++++++- src/expr/symbol_manager.h | 8 +++++++ src/parser/parser.cpp | 6 ++--- src/parser/parser.h | 10 +++++---- src/parser/smt2/Smt2.g | 45 ++++++++++++++++++++----------------- src/parser/smt2/smt2.cpp | 5 ++--- src/parser/smt2/smt2.h | 7 +++--- 7 files changed, 85 insertions(+), 36 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& ts, std::vector& names, bool areAssertions = false) const; + /** get expression names */ + std::map getExpressionNames(bool areAssertions) const; /** reset */ void reset(); /** Push a scope in the expression names. */ @@ -127,8 +129,31 @@ void SymbolManager::Implementation::getExpressionNames( } } +std::map +SymbolManager::Implementation::getExpressionNames(bool areAssertions) const +{ + std::map 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& ts, return d_implementation->getExpressionNames(ts, names, areAssertions); } +std::map 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& ts, std::vector& 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 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 def89e6b1..c5746020c 100644 --- 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 d30ea7c16..96a16b31f 100644 --- 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 a96686135..916e20d9b 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -258,7 +258,7 @@ command [std::unique_ptr* 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::const_iterator i = names.begin(), iend = names.end(); i != iend; @@ -319,7 +319,7 @@ command [std::unique_ptr* 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* cmd] // set the expression name, if there was a named term std::pair 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* 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 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* 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 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& i : sortedVarNames) { PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_SORT); @@ -818,7 +820,7 @@ smt25Command[std::unique_ptr* 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* 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* cmd] if( func_defs.size()pushDefineFunRecScope( sortedVarNamesList[j], funcs[j], - flattenVarsList[j], bvs, true); + flattenVarsList[j], bvs); } } )+ @@ -996,7 +998,7 @@ extendedCommand[std::unique_ptr* 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* 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* 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 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& 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 1decb3b1c..892c628dc 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -452,10 +452,9 @@ void Smt2::pushDefineFunRecScope( const std::vector>& sortedVarNames, api::Term func, const std::vector& flattenVars, - std::vector& bvs, - bool bindingLevel) + std::vector& 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 eeedbec55..734b00f92 100644 --- 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>& sortedVarNames, api::Term func, const std::vector& flattenVars, - std::vector& bvs, - bool bindingLevel = false); + std::vector& bvs); void reset() override; -- 2.30.2