From: Andrew Reynolds Date: Fri, 13 Nov 2020 15:49:36 +0000 (-0600) Subject: Add more features to symbol manager (#5434) X-Git-Tag: cvc5-1.0.0~2601 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=74be116f3956dab6be0b8e3e18f723957a351fbf;p=cvc5.git 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 3247e9609..be3673d32 100644 --- 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 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 412621b8a..54f9732b9 100644 --- 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 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 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 Parser::bindVars(const std::vector names, uint32_t flags, bool doOverload) { - if (d_globalDeclarations) { + bool globalDecls = d_symman->getGlobalDeclarations(); + if (globalDecls) + { flags |= ExprManager::VAR_FLAG_GLOBAL; } std::vector 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(arity), - type, - d_globalDeclarations && !(flags & ExprManager::SORT_FLAG_PLACEHOLDER)); + bool globalDecls = d_symman->getGlobalDeclarations(); + defineType(name, + vector(arity), + type, + globalDecls && !(flags & ExprManager::SORT_FLAG_PLACEHOLDER)); return type; } @@ -412,6 +415,7 @@ std::vector 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 Parser::bindMutualDatatypeTypes( if (t.isParametricDatatype()) { std::vector 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 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 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 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 Parser::processAdHocStringEsc(const std::string& s) { std::vector 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 @@ -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 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* 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* 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* 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* 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* 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* 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* 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(), expr, - PARSER_STATE->getGlobalDeclarations()); + SYM_MAN->getGlobalDeclarations()); c->setMuted(true); PARSER_STATE->preemptCommand(c); }