diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-23 06:40:47 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-11-23 06:40:47 -0600 |
commit | e11af4be0f3d1dee41aefa91d856de9035cb3a29 (patch) | |
tree | 264c21c4e6ab7fe60378b5713e21d2938a5dd5d0 /src/smt/model.h | |
parent | 961af5e182f65c976424fd2adc22fc9bd484f73c (diff) |
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.
Diffstat (limited to 'src/smt/model.h')
-rw-r--r-- | src/smt/model.h | 39 |
1 files changed, 35 insertions, 4 deletions
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<TypeNode>& getDeclaredSorts() const; + /** get declared terms */ + const std::vector<Node>& 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<TypeNode> d_declareSorts; + /** + * The list of terms to print, is typically one-to-one with declare-fun + * commands. + */ + std::vector<Node> d_declareTerms; }; } // namespace smt |