From f980e08b00ca9691f1f566455db446786994601b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 12 Nov 2020 07:21:09 -0600 Subject: [PATCH] Make symbol manager context dependent (#5424) This follows a similar style to symbol_table.h/cpp. This is required since context dependent data structures are cvc4_private, and symbol manager is cvc4_public. --- src/expr/symbol_manager.cpp | 118 ++++++++++++++++++++++++++++++++---- src/expr/symbol_manager.h | 26 ++++++-- src/parser/parser.cpp | 23 +++++++ src/parser/parser.h | 21 ++----- 4 files changed, 153 insertions(+), 35 deletions(-) diff --git a/src/expr/symbol_manager.cpp b/src/expr/symbol_manager.cpp index ac3b5d211..3247e9609 100644 --- a/src/expr/symbol_manager.cpp +++ b/src/expr/symbol_manager.cpp @@ -14,15 +14,54 @@ #include "expr/symbol_manager.h" +#include "context/cdhashmap.h" +#include "context/cdhashset.h" + +using namespace CVC4::context; + namespace CVC4 { -SymbolManager::SymbolManager(api::Solver* s) : d_solver(s) {} +// ---------------------------------------------- SymbolManager::Implementation -SymbolTable* SymbolManager::getSymbolTable() { return &d_symtabAllocated; } +class SymbolManager::Implementation +{ + using TermStringMap = CDHashMap; + using TermSet = CDHashSet; -bool SymbolManager::setExpressionName(api::Term t, - const std::string& name, - bool isAssertion) + public: + Implementation() + : d_context(), d_names(&d_context), d_namedAsserts(&d_context) + { + } + + ~Implementation() {} + /** set expression name */ + bool setExpressionName(api::Term t, + const std::string& name, + bool isAssertion = false); + /** get expression name */ + bool getExpressionName(api::Term t, + std::string& name, + bool isAssertion = false) const; + /** get expression names */ + void getExpressionNames(const std::vector& ts, + std::vector& names, + bool areAssertions = false) const; + /** reset */ + void reset(); + + private: + /** The context manager for the scope maps. */ + Context d_context; + /** Map terms to names */ + TermStringMap d_names; + /** The set of terms with assertion names */ + TermSet d_namedAsserts; +}; + +bool SymbolManager::Implementation::setExpressionName(api::Term t, + const std::string& name, + bool isAssertion) { if (d_names.find(t) != d_names.end()) { @@ -37,11 +76,11 @@ bool SymbolManager::setExpressionName(api::Term t, return true; } -bool SymbolManager::getExpressionName(api::Term t, - std::string& name, - bool isAssertion) const +bool SymbolManager::Implementation::getExpressionName(api::Term t, + std::string& name, + bool isAssertion) const { - std::map::const_iterator it = d_names.find(t); + TermStringMap::const_iterator it = d_names.find(t); if (it == d_names.end()) { return false; @@ -54,13 +93,14 @@ bool SymbolManager::getExpressionName(api::Term t, return false; } } - name = it->second; + name = (*it).second; return true; } -void SymbolManager::getExpressionNames(const std::vector& ts, - std::vector& names, - bool areAssertions) const +void SymbolManager::Implementation::getExpressionNames( + const std::vector& ts, + std::vector& names, + bool areAssertions) const { for (const api::Term& t : ts) { @@ -72,4 +112,56 @@ void SymbolManager::getExpressionNames(const std::vector& ts, } } +void SymbolManager::Implementation::reset() +{ + // clear names? +} + +// ---------------------------------------------- SymbolManager + +SymbolManager::SymbolManager(api::Solver* s) + : d_solver(s), d_implementation(new SymbolManager::Implementation()) +{ +} + +SymbolManager::~SymbolManager() {} + +SymbolTable* SymbolManager::getSymbolTable() { return &d_symtabAllocated; } + +bool SymbolManager::setExpressionName(api::Term t, + const std::string& name, + bool isAssertion) +{ + return d_implementation->setExpressionName(t, name, isAssertion); +} + +bool SymbolManager::getExpressionName(api::Term t, + std::string& name, + bool isAssertion) const +{ + return d_implementation->getExpressionName(t, name, isAssertion); +} + +void SymbolManager::getExpressionNames(const std::vector& ts, + std::vector& names, + bool areAssertions) const +{ + return d_implementation->getExpressionNames(ts, names, areAssertions); +} + +size_t SymbolManager::scopeLevel() const +{ + return d_symtabAllocated.getLevel(); +} + +void SymbolManager::pushScope() { d_symtabAllocated.pushScope(); } + +void SymbolManager::popScope() { d_symtabAllocated.popScope(); } + +void SymbolManager::reset() +{ + d_symtabAllocated.reset(); + d_implementation->reset(); +} + } // namespace CVC4 diff --git a/src/expr/symbol_manager.h b/src/expr/symbol_manager.h index 4890ed994..412621b8a 100644 --- a/src/expr/symbol_manager.h +++ b/src/expr/symbol_manager.h @@ -18,6 +18,7 @@ #define CVC4__EXPR__SYMBOL_MANAGER_H #include +#include #include #include @@ -38,7 +39,7 @@ class CVC4_PUBLIC SymbolManager { public: SymbolManager(api::Solver* s); - ~SymbolManager() {} + ~SymbolManager(); /** Get the underlying symbol table */ SymbolTable* getSymbolTable(); //---------------------------- named expressions @@ -84,6 +85,22 @@ class CVC4_PUBLIC SymbolManager std::vector& names, bool areAssertions = false) const; //---------------------------- end named expressions + /** + * Get the scope level of the symbol table. + */ + size_t scopeLevel() const; + /** + * Push a scope in the symbol table. + */ + void pushScope(); + /** + * Pop a scope in the symbol table. + */ + void popScope(); + /** + * Reset this symbol manager, which resets the symbol table. + */ + void reset(); private: /** The API Solver object. */ @@ -92,10 +109,9 @@ class CVC4_PUBLIC SymbolManager * The declaration scope that is "owned" by this symbol manager. */ SymbolTable d_symtabAllocated; - /** Map terms to names */ - std::map d_names; - /** The set of terms with assertion names */ - std::set d_namedAsserts; + /** The implementation of the symbol manager */ + class Implementation; + std::unique_ptr d_implementation; }; } // namespace CVC4 diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 710381f9b..1584af893 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -770,6 +770,29 @@ void Parser::attributeNotSupported(const std::string& attr) { } } +size_t Parser::scopeLevel() const { return d_symman->scopeLevel(); } + +void Parser::pushScope(bool bindingLevel) +{ + d_symman->pushScope(); + if (!bindingLevel) + { + d_assertionLevel = scopeLevel(); + } +} + +void Parser::popScope() +{ + d_symman->popScope(); + if (scopeLevel() < d_assertionLevel) + { + d_assertionLevel = scopeLevel(); + d_reservedSymbols.clear(); + } +} + +void Parser::reset() { d_symman->reset(); } + std::vector Parser::processAdHocStringEsc(const std::string& s) { std::vector str; diff --git a/src/parser/parser.h b/src/parser/parser.h index c762fc117..8987b928b 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -751,7 +751,7 @@ public: /** * Gets the current declaration level. */ - inline size_t scopeLevel() const { return d_symtab->getLevel(); } + size_t scopeLevel() const; /** * Pushes a scope. All subsequent symbol declarations made are only valid in @@ -761,24 +761,11 @@ public: * current scope level. This determines which scope assertions are declared * at. */ - inline void pushScope(bool bindingLevel = false) { - d_symtab->pushScope(); - if(!bindingLevel) { - d_assertionLevel = scopeLevel(); - } - } + void pushScope(bool bindingLevel = false); - inline void popScope() { - d_symtab->popScope(); - if(scopeLevel() < d_assertionLevel) { - d_assertionLevel = scopeLevel(); - d_reservedSymbols.clear(); - } - } + void popScope(); - virtual void reset() { - d_symtab->reset(); - } + virtual void reset(); void setGlobalDeclarations(bool flag) { d_globalDeclarations = flag; -- 2.30.2