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.

1 files changed, 14 insertions, 0 deletions

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<TypeNode>& Model::getDeclaredSorts() const
+{
+  return d_declareSorts;
+}
+const std::vector<Node>& Model::getDeclaredTerms() const
+{
+  return d_declareTerms;
+}
+
 }  // namespace smt
 }/* CVC4 namespace */