From e11af4be0f3d1dee41aefa91d856de9035cb3a29 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 23 Nov 2020 06:40:47 -0600 Subject: Add declare model symbol methods to SymbolManager and Model (#5480) This is in preparation for the symbol manager determining which symbols are printed in the model. --- src/expr/symbol_manager.cpp | 63 +++++++++++++++++++++++++++++++++++++++++++++ src/expr/symbol_manager.h | 17 ++++++++++++ src/smt/model.cpp | 14 ++++++++++ src/smt/model.h | 39 +++++++++++++++++++++++++--- 4 files changed, 129 insertions(+), 4 deletions(-) diff --git a/src/expr/symbol_manager.cpp b/src/expr/symbol_manager.cpp index a163e503d..f82845fe3 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/cdlist.h" #include "context/cdo.h" using namespace CVC4::context; @@ -28,12 +29,16 @@ class SymbolManager::Implementation { using TermStringMap = CDHashMap; using TermSet = CDHashSet; + using SortList = CDList; + using TermList = CDList; public: Implementation() : d_context(), d_names(&d_context), d_namedAsserts(&d_context), + d_declareSorts(&d_context), + d_declareTerms(&d_context), d_hasPushedScope(&d_context, false) { } @@ -53,6 +58,14 @@ class SymbolManager::Implementation bool areAssertions = false) const; /** get expression names */ std::map getExpressionNames(bool areAssertions) const; + /** get model declare sorts */ + std::vector getModelDeclareSorts() const; + /** get model declare terms */ + std::vector getModelDeclareTerms() const; + /** Add declared sort to the list of model declarations. */ + void addModelDeclarationSort(api::Sort s); + /** Add declared term to the list of model declarations. */ + void addModelDeclarationTerm(api::Term t); /** reset */ void reset(); /** Push a scope in the expression names. */ @@ -67,6 +80,10 @@ class SymbolManager::Implementation TermStringMap d_names; /** The set of terms with assertion names */ TermSet d_namedAsserts; + /** Declared sorts (for model printing) */ + SortList d_declareSorts; + /** Declared terms (for model printing) */ + TermList d_declareTerms; /** * Have we pushed a scope (e.g. a let or quantifier) in the current context? */ @@ -150,6 +167,34 @@ SymbolManager::Implementation::getExpressionNames(bool areAssertions) const return emap; } +std::vector SymbolManager::Implementation::getModelDeclareSorts() + const +{ + std::vector declareSorts(d_declareSorts.begin(), + d_declareSorts.end()); + return declareSorts; +} + +std::vector SymbolManager::Implementation::getModelDeclareTerms() + const +{ + std::vector declareTerms(d_declareTerms.begin(), + d_declareTerms.end()); + return declareTerms; +} + +void SymbolManager::Implementation::addModelDeclarationSort(api::Sort s) +{ + Trace("sym-manager") << "addModelDeclarationSort " << s << std::endl; + d_declareSorts.push_back(s); +} + +void SymbolManager::Implementation::addModelDeclarationTerm(api::Term t) +{ + Trace("sym-manager") << "addModelDeclarationTerm " << t << std::endl; + d_declareTerms.push_back(t); +} + void SymbolManager::Implementation::pushScope(bool isUserContext) { Trace("sym-manager") << "pushScope, isUserContext = " << isUserContext @@ -219,6 +264,24 @@ std::map SymbolManager::getExpressionNames( { return d_implementation->getExpressionNames(areAssertions); } +std::vector SymbolManager::getModelDeclareSorts() const +{ + return d_implementation->getModelDeclareSorts(); +} +std::vector SymbolManager::getModelDeclareTerms() const +{ + return d_implementation->getModelDeclareTerms(); +} + +void SymbolManager::addModelDeclarationSort(api::Sort s) +{ + d_implementation->addModelDeclarationSort(s); +} + +void SymbolManager::addModelDeclarationTerm(api::Term t) +{ + d_implementation->addModelDeclarationTerm(t); +} size_t SymbolManager::scopeLevel() const { diff --git a/src/expr/symbol_manager.h b/src/expr/symbol_manager.h index a3ca8e780..06b01da8b 100644 --- a/src/expr/symbol_manager.h +++ b/src/expr/symbol_manager.h @@ -92,6 +92,23 @@ class CVC4_PUBLIC SymbolManager */ std::map getExpressionNames( bool areAssertions = false) const; + /** + * @return The sorts we have declared that should be printed in the model. + */ + std::vector getModelDeclareSorts() const; + /** + * @return The terms we have declared that should be printed in the model. + */ + std::vector getModelDeclareTerms() const; + /** + * Add declared sort to the list of model declarations. + */ + void addModelDeclarationSort(api::Sort s); + /** + * Add declared term to the list of model declarations. + */ + void addModelDeclarationTerm(api::Term t); + //---------------------------- end named expressions /** * Get the scope level of the symbol table. diff --git a/src/smt/model.cpp b/src/smt/model.cpp index fc9ea8fbb..b734ad9e9 100644 --- a/src/smt/model.cpp +++ b/src/smt/model.cpp @@ -61,5 +61,19 @@ Node Model::getValue(TNode n) const { return d_tmodel->getValue(n); } bool Model::hasApproximations() const { return d_tmodel->hasApproximations(); } +void Model::clearModelDeclarations() { d_declareSorts.clear(); } + +void Model::addDeclarationSort(TypeNode tn) { d_declareSorts.push_back(tn); } + +void Model::addDeclarationTerm(Node n) { d_declareTerms.push_back(n); } +const std::vector& Model::getDeclaredSorts() const +{ + return d_declareSorts; +} +const std::vector& Model::getDeclaredTerms() const +{ + return d_declareTerms; +} + } // namespace smt }/* CVC4 namespace */ diff --git a/src/smt/model.h b/src/smt/model.h index dc36b5d29..0913922d1 100644 --- a/src/smt/model.h +++ b/src/smt/model.h @@ -39,6 +39,9 @@ std::ostream& operator<<(std::ostream&, const Model&); * This is the SMT-level model object, that is responsible for maintaining * the necessary information for how to print the model, as well as * holding a pointer to the underlying implementation of the theory model. + * + * The model declarations maintained by this class are context-independent + * and should be updated when this model is printed. */ class Model { friend std::ostream& operator<<(std::ostream&, const Model&); @@ -49,10 +52,6 @@ class Model { Model(SmtEngine& smt, theory::TheoryModel* tm); /** virtual destructor */ ~Model() {} - /** get number of commands to report */ - size_t getNumCommands() const; - /** get command */ - const NodeCommand* getCommand(size_t i) const; /** get the smt engine that this model is hooked up to */ SmtEngine* getSmtEngine() { return &d_smt; } /** get the smt engine (as a pointer-to-const) that this model is hooked up to */ @@ -78,6 +77,28 @@ class Model { /** Does this model have approximations? */ bool hasApproximations() const; //----------------------- end helper methods + /** get number of commands to report */ + size_t getNumCommands() const; + /** get command */ + const NodeCommand* getCommand(size_t i) const; + //----------------------- model declarations + /** Clear the current model declarations. */ + void clearModelDeclarations(); + /** + * Set that tn is a sort that should be printed in the model, when applicable, + * based on the output language. + */ + void addDeclarationSort(TypeNode tn); + /** + * Set that n is a variable that should be printed in the model, when + * applicable, based on the output language. + */ + void addDeclarationTerm(Node n); + /** get declared sorts */ + const std::vector& getDeclaredSorts() const; + /** get declared terms */ + const std::vector& getDeclaredTerms() const; + //----------------------- end model declarations protected: /** The SmtEngine we're associated with */ SmtEngine& d_smt; @@ -93,6 +114,16 @@ class Model { * the values of sorts and terms. */ theory::TheoryModel* d_tmodel; + /** + * The list of types to print, generally corresponding to declare-sort + * commands. + */ + std::vector d_declareSorts; + /** + * The list of terms to print, is typically one-to-one with declare-fun + * commands. + */ + std::vector d_declareTerms; }; } // namespace smt -- cgit v1.2.3