Merge branch 'master' into macos11macos11

8 files changed, 163 insertions, 164 deletions

diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp
index 0bc7ce99b..d3a2dfefa 100644
--- a/src/smt/check_models.cpp
+++ b/src/smt/check_models.cpp
@@ -18,13 +18,13 @@
 #include "base/modal_exception.h"
 #include "options/smt_options.h"
 #include "smt/env.h"
-#include "smt/model.h"
 #include "smt/node_command.h"
 #include "smt/preprocessor.h"
 #include "smt/smt_solver.h"
 #include "theory/rewriter.h"
 #include "theory/substitutions.h"
 #include "theory/theory_engine.h"
+#include "theory/theory_model.h"
 
 using namespace cvc5::theory;
 
@@ -34,7 +34,7 @@ namespace smt {
 CheckModels::CheckModels(Env& e) : d_env(e) {}
 CheckModels::~CheckModels() {}
 
-void CheckModels::checkModel(Model* m,
+void CheckModels::checkModel(TheoryModel* m,
                              context::CDList<Node>* al,
                              bool hardFailure)
 {
diff --git a/src/smt/check_models.h b/src/smt/check_models.h
index ce06bae07..fbfb1c2f5 100644
--- a/src/smt/check_models.h
+++ b/src/smt/check_models.h
@@ -25,9 +25,11 @@ namespace cvc5 {
 
 class Env;
 
-namespace smt {
+namespace theory {
+class TheoryModel;
+}
 
-class Model;
+namespace smt {
 
 /**
  * This utility is responsible for checking the current model.
@@ -43,7 +45,9 @@ class CheckModels
    * This throws an exception if we fail to verify that m is a proper model
    * given assertion list al based on the model checking policy.
    */
-  void checkModel(Model* m, context::CDList<Node>* al, bool hardFailure);
+  void checkModel(theory::TheoryModel* m,
+                  context::CDList<Node>* al,
+                  bool hardFailure);
 
  private:
   /** Reference to the environment */
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index e6be0a646..008d7a6d8 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -38,8 +38,6 @@
 #include "proof/unsat_core.h"
 #include "smt/dump.h"
 #include "smt/model.h"
-#include "smt/smt_engine.h"
-#include "smt/smt_engine_scope.h"
 #include "util/unsafe_interrupt_exception.h"
 #include "util/utility.h"
 
@@ -1748,27 +1746,17 @@ void GetAssignmentCommand::toStream(std::ostream& out,
 /* class GetModelCommand                                                      */
 /* -------------------------------------------------------------------------- */
 
-GetModelCommand::GetModelCommand() : d_result(nullptr) {}
+GetModelCommand::GetModelCommand() {}
 void GetModelCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
-    d_result = solver->getSmtEngine()->getModel();
-    // set the model declarations, which determines what is printed in the model
-    d_result->clearModelDeclarations();
     std::vector<api::Sort> declareSorts = sm->getModelDeclareSorts();
-    for (const api::Sort& s : declareSorts)
-    {
-      d_result->addDeclarationSort(sortToTypeNode(s));
-    }
     std::vector<api::Term> declareTerms = sm->getModelDeclareTerms();
-    for (const api::Term& t : declareTerms)
-    {
-      d_result->addDeclarationTerm(termToNode(t));
-    }
+    d_result = solver->getModel(declareSorts, declareTerms);
     d_commandStatus = CommandSuccess::instance();
   }
-  catch (RecoverableModalException& e)
+  catch (api::CVC5ApiRecoverableException& e)
   {
     d_commandStatus = new CommandRecoverableFailure(e.what());
   }
@@ -1782,12 +1770,6 @@ void GetModelCommand::invoke(api::Solver* solver, SymbolManager* sm)
   }
 }
 
-/* Model is private to the library -- for now
-Model* GetModelCommand::getResult() const  {
-  return d_result;
-}
-*/
-
 void GetModelCommand::printResult(std::ostream& out, uint32_t verbosity) const
 {
   if (!ok())
@@ -1796,13 +1778,13 @@ void GetModelCommand::printResult(std::ostream& out, uint32_t verbosity) const
   }
   else
   {
-    out << *d_result;
+    out << d_result;
   }
 }
 
 Command* GetModelCommand::clone() const
 {
-  GetModelCommand* c = new GetModelCommand();
+  GetModelCommand* c = new GetModelCommand;
   c->d_result = d_result;
   return c;
 }
diff --git a/src/smt/command.h b/src/smt/command.h
index d3e3679d2..627cb13c9 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -950,7 +950,8 @@ class CVC5_EXPORT GetModelCommand : public Command
                 Language language = Language::LANG_AUTO) const override;
 
  protected:
-  smt::Model* d_result;
+  /** Result of printing the model */
+  std::string d_result;
 }; /* class GetModelCommand */
 
 /** The command to block models. */
diff --git a/src/smt/model.cpp b/src/smt/model.cpp
index cf6a90f12..9a195cb51 100644
--- a/src/smt/model.cpp
+++ b/src/smt/model.cpp
@@ -18,18 +18,13 @@
 #include "expr/expr_iomanip.h"
 #include "options/base_options.h"
 #include "printer/printer.h"
-#include "smt/dump_manager.h"
-#include "smt/node_command.h"
-#include "smt/smt_engine.h"
-#include "smt/smt_engine_scope.h"
-#include "theory/theory_model.h"
 
 namespace cvc5 {
 namespace smt {
 
-Model::Model(theory::TheoryModel* tm) : d_isKnownSat(false), d_tmodel(tm)
+Model::Model(bool isKnownSat, const std::string& inputName)
+    : d_inputName(inputName), d_isKnownSat(isKnownSat)
 {
-  Assert(d_tmodel != nullptr);
 }
 
 std::ostream& operator<<(std::ostream& out, const Model& m) {
@@ -38,31 +33,55 @@ std::ostream& operator<<(std::ostream& out, const Model& m) {
   return out;
 }
 
-theory::TheoryModel* Model::getTheoryModel() { return d_tmodel; }
+const std::vector<Node>& Model::getDomainElements(TypeNode tn) const
+{
+  std::map<TypeNode, std::vector<Node>>::const_iterator it =
+      d_domainElements.find(tn);
+  Assert(it != d_domainElements.end());
+  return it->second;
+}
 
-const theory::TheoryModel* Model::getTheoryModel() const { return d_tmodel; }
+Node Model::getValue(TNode n) const
+{
+  std::map<Node, Node>::const_iterator it = d_declareTermValues.find(n);
+  Assert(it != d_declareTermValues.end());
+  return it->second;
+}
 
-bool Model::isModelCoreSymbol(TNode sym) const
+bool Model::getHeapModel(Node& h, Node& nilEq) const
 {
-  return d_tmodel->isModelCoreSymbol(sym);
+  if (d_sepHeap.isNull() || d_sepNilEq.isNull())
+  {
+    return false;
+  }
+  h = d_sepHeap;
+  nilEq = d_sepNilEq;
+  return true;
 }
-Node Model::getValue(TNode n) const { return d_tmodel->getValue(n); }
 
-bool Model::hasApproximations() const { return d_tmodel->hasApproximations(); }
+void Model::addDeclarationSort(TypeNode tn, const std::vector<Node>& elements)
+{
+  d_declareSorts.push_back(tn);
+  d_domainElements[tn] = elements;
+}
 
-void Model::clearModelDeclarations()
+void Model::addDeclarationTerm(Node n, Node value)
 {
-  d_declareTerms.clear();
-  d_declareSorts.clear();
+  d_declareTerms.push_back(n);
+  d_declareTermValues[n] = value;
 }
 
-void Model::addDeclarationSort(TypeNode tn) { d_declareSorts.push_back(tn); }
+void Model::setHeapModel(Node h, Node nilEq)
+{
+  d_sepHeap = h;
+  d_sepNilEq = nilEq;
+}
 
-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;
diff --git a/src/smt/model.h b/src/smt/model.h
index 342a9f3b0..5275ea680 100644
--- a/src/smt/model.h
+++ b/src/smt/model.h
@@ -15,8 +15,8 @@
 
 #include "cvc5_private.h"
 
-#ifndef CVC5__MODEL_H
-#define CVC5__MODEL_H
+#ifndef CVC5__SMT__MODEL_H
+#define CVC5__SMT__MODEL_H
 
 #include <iosfwd>
 #include <vector>
@@ -24,13 +24,6 @@
 #include "expr/node.h"
 
 namespace cvc5 {
-
-class SmtEngine;
-
-namespace theory {
-class TheoryModel;
-}
-
 namespace smt {
 
 class Model;
@@ -38,22 +31,15 @@ class Model;
 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.
+ * A utility for representing a model for pretty printing.
  */
 class Model {
-  friend std::ostream& operator<<(std::ostream&, const Model&);
-  friend class ::cvc5::SmtEngine;
-
  public:
-  /** construct */
-  Model(theory::TheoryModel* tm);
-  /** virtual destructor */
-  ~Model() {}
+  /** Constructor
+   * @param isKnownSat True if this model is associated with a "sat" response,
+   * or false if it is associated with an "unknown" response.
+   */
+  Model(bool isKnownSat, const std::string& inputName);
   /** get the input name (file name, etc.) this model is associated to */
   std::string getInputName() const { return d_inputName; }
   /**
@@ -63,31 +49,37 @@ class Model {
    * only a candidate solution.
    */
   bool isKnownSat() const { return d_isKnownSat; }
-  /** Get the underlying theory model */
-  theory::TheoryModel* getTheoryModel();
-  /** Get the underlying theory model (const version) */
-  const theory::TheoryModel* getTheoryModel() const;
-  //----------------------- helper methods in the underlying theory model
-  /** Is the node n a model core symbol? */
-  bool isModelCoreSymbol(TNode sym) const;
+  /** Get domain elements */
+  const std::vector<Node>& getDomainElements(TypeNode tn) const;
   /** Get value */
   Node getValue(TNode n) const;
-  /** Does this model have approximations? */
-  bool hasApproximations() const;
-  //----------------------- end helper methods
+  /** Get separation logic heap and nil, return true if they have been set */
+  bool getHeapModel(Node& h, Node& nilEq) 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.
+   *
+   * @param tn The uninterpreted sort
+   * @param elements The domain elements of tn in the model
    */
-  void addDeclarationSort(TypeNode tn);
+  void addDeclarationSort(TypeNode tn, const std::vector<Node>& elements);
   /**
    * Set that n is a variable that should be printed in the model, when
    * applicable, based on the output language.
+   *
+   * @param n The variable
+   * @param value The value of the variable in the model
+   */
+  void addDeclarationTerm(Node n, Node value);
+  /**
+   * Set the separation logic model information where h is the heap and nilEq
+   * is the value of sep.nil.
+   *
+   * @param h The value of heap in the heap model
+   * @param nilEq The value of sep.nil in the heap model
    */
-  void addDeclarationTerm(Node n);
+  void setHeapModel(Node h, Node nilEq);
   /** get declared sorts */
   const std::vector<TypeNode>& getDeclaredSorts() const;
   /** get declared terms */
@@ -102,23 +94,25 @@ class Model {
    */
   bool d_isKnownSat;
   /**
-   * Pointer to the underlying theory model, which maintains all data regarding
-   * 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 interpretation of the above sorts, as a list of domain elements. */
+  std::map<TypeNode, std::vector<Node>> d_domainElements;
   /**
    * The list of terms to print, is typically one-to-one with declare-fun
    * commands.
    */
   std::vector<Node> d_declareTerms;
+  /** Mapping terms to values */
+  std::map<Node, Node> d_declareTermValues;
+  /** Separation logic heap and nil */
+  Node d_sepHeap;
+  Node d_sepNilEq;
 };
 
 }  // namespace smt
 }  // namespace cvc5
 
-#endif /* CVC5__MODEL_H */
+#endif /* CVC5__SMT__MODEL_H */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 2276956b5..27e7b8530 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -92,7 +92,6 @@ SmtEngine::SmtEngine(NodeManager* nm, const Options* optr)
       d_routListener(new ResourceOutListener(*this)),
       d_snmListener(new SmtNodeManagerListener(*getDumpManager(), d_outMgr)),
       d_smtSolver(nullptr),
-      d_model(nullptr),
       d_checkModels(nullptr),
       d_pfManager(nullptr),
       d_ucManager(nullptr),
@@ -224,7 +223,6 @@ void SmtEngine::finishInit()
   TheoryModel* tm = te->getModel();
   if (tm != nullptr)
   {
-    d_model.reset(new Model(tm));
     // make the check models utility
     d_checkModels.reset(new CheckModels(*d_env.get()));
   }
@@ -305,7 +303,6 @@ SmtEngine::~SmtEngine()
 
     d_absValues.reset(nullptr);
     d_asserts.reset(nullptr);
-    d_model.reset(nullptr);
 
     d_abductSolver.reset(nullptr);
     d_interpolSolver.reset(nullptr);
@@ -712,7 +709,7 @@ Result SmtEngine::quickCheck() {
       Result::ENTAILMENT_UNKNOWN, Result::REQUIRES_FULL_CHECK, filename);
 }
 
-Model* SmtEngine::getAvailableModel(const char* c) const
+TheoryModel* SmtEngine::getAvailableModel(const char* c) const
 {
   if (!d_env->getOptions().theory.assignFunctionValues)
   {
@@ -751,7 +748,7 @@ Model* SmtEngine::getAvailableModel(const char* c) const
     throw RecoverableModalException(ss.str().c_str());
   }
 
-  return d_model.get();
+  return m;
 }
 
 QuantifiersEngine* SmtEngine::getAvailableQuantifiersEngine(const char* c) const
@@ -1121,7 +1118,7 @@ Node SmtEngine::getValue(const Node& ex) const
   }
 
   Trace("smt") << "--- getting value of " << n << endl;
-  Model* m = getAvailableModel("get-value");
+  TheoryModel* m = getAvailableModel("get-value");
   Assert(m != nullptr);
   Node resultNode = m->getValue(n);
   Trace("smt") << "--- got value " << n << " = " << resultNode << endl;
@@ -1163,8 +1160,8 @@ std::vector<Node> SmtEngine::getValues(const std::vector<Node>& exprs) const
 std::vector<Node> SmtEngine::getModelDomainElements(TypeNode tn) const
 {
   Assert(tn.isSort());
-  Model* m = getAvailableModel("getModelDomainElements");
-  return m->getTheoryModel()->getDomainElements(tn);
+  TheoryModel* m = getAvailableModel("getModelDomainElements");
+  return m->getDomainElements(tn);
 }
 
 bool SmtEngine::isModelCoreSymbol(Node n)
@@ -1177,8 +1174,7 @@ bool SmtEngine::isModelCoreSymbol(Node n)
     // if the model core mode is none, we are always a model core symbol
     return true;
   }
-  Model* m = getAvailableModel("isModelCoreSymbol");
-  TheoryModel* tm = m->getTheoryModel();
+  TheoryModel* tm = getAvailableModel("isModelCoreSymbol");
   // compute the model core if not done so already
   if (!tm->isUsingModelCore())
   {
@@ -1193,41 +1189,54 @@ bool SmtEngine::isModelCoreSymbol(Node n)
   return tm->isModelCoreSymbol(n);
 }
 
-// TODO(#1108): Simplify the error reporting of this method.
-Model* SmtEngine::getModel() {
-  Trace("smt") << "SMT getModel()" << endl;
+std::string SmtEngine::getModel(const std::vector<TypeNode>& declaredSorts,
+                                const std::vector<Node>& declaredFuns)
+{
   SmtScope smts(this);
-
-  finishInit();
-
-  if (Dump.isOn("benchmark"))
+  // !!! Note that all methods called here should have a version at the API
+  // level. This is to ensure that the information associated with a model is
+  // completely accessible by the user. This is currently not rigorously
+  // enforced. An alternative design would be to have this method implemented
+  // at the API level, but this makes exceptions in the text interface less
+  // intuitive and makes it impossible to implement raw-benchmark at the
+  // SmtEngine level.
+  if (Dump.isOn("raw-benchmark"))
   {
     getPrinter().toStreamCmdGetModel(d_env->getDumpOut());
   }
-
-  Model* m = getAvailableModel("get model");
-
-  // Notice that the returned model is (currently) accessed by the
-  // GetModelCommand only, and is not returned to the user. The information
-  // in that model may become stale after it is returned. This is safe
-  // since GetModelCommand always calls this command again when it prints
-  // a model.
-
-  if (d_env->getOptions().smt.modelCoresMode
-      != options::ModelCoresMode::NONE)
+  TheoryModel* tm = getAvailableModel("get model");
+  // use the smt::Model model utility for printing
+  const Options& opts = d_env->getOptions();
+  bool isKnownSat = (d_state->getMode() == SmtMode::SAT);
+  Model m(isKnownSat, opts.driver.filename);
+  // set the model declarations, which determines what is printed in the model
+  for (const TypeNode& tn : declaredSorts)
   {
-    // If we enabled model cores, we compute a model core for m based on our
-    // (expanded) assertions using the model core builder utility
-    std::vector<Node> asserts = getAssertionsInternal();
-    d_pp->expandDefinitions(asserts);
-    ModelCoreBuilder::setModelCore(
-        asserts, m->getTheoryModel(), d_env->getOptions().smt.modelCoresMode);
+    m.addDeclarationSort(tn, getModelDomainElements(tn));
   }
-  // set the information on the SMT-level model
-  Assert(m != nullptr);
-  m->d_inputName = d_env->getOptions().driver.filename;
-  m->d_isKnownSat = (d_state->getMode() == SmtMode::SAT);
-  return m;
+  bool usingModelCores =
+      (opts.smt.modelCoresMode != options::ModelCoresMode::NONE);
+  for (const Node& n : declaredFuns)
+  {
+    if (usingModelCores && !tm->isModelCoreSymbol(n))
+    {
+      // skip if not in model core
+      continue;
+    }
+    Node value = tm->getValue(n);
+    m.addDeclarationTerm(n, value);
+  }
+  // for separation logic
+  TypeNode locT, dataT;
+  if (getSepHeapTypes(locT, dataT))
+  {
+    std::pair<Node, Node> sh = getSepHeapAndNilExpr();
+    m.setHeapModel(sh.first, sh.second);
+  }
+  // print the model
+  std::stringstream ssm;
+  ssm << m;
+  return ssm.str();
 }
 
 Result SmtEngine::blockModel()
@@ -1242,7 +1251,7 @@ Result SmtEngine::blockModel()
     getPrinter().toStreamCmdBlockModel(d_env->getDumpOut());
   }
 
-  Model* m = getAvailableModel("block model");
+  TheoryModel* m = getAvailableModel("block model");
 
   if (d_env->getOptions().smt.blockModelsMode
       == options::BlockModelsMode::NONE)
@@ -1254,10 +1263,8 @@ Result SmtEngine::blockModel()
 
   // get expanded assertions
   std::vector<Node> eassertsProc = getExpandedAssertions();
-  Node eblocker =
-      ModelBlocker::getModelBlocker(eassertsProc,
-                                    m->getTheoryModel(),
-                                    d_env->getOptions().smt.blockModelsMode);
+  Node eblocker = ModelBlocker::getModelBlocker(
+      eassertsProc, m, d_env->getOptions().smt.blockModelsMode);
   Trace("smt") << "Block formula: " << eblocker << std::endl;
   return assertFormula(eblocker);
 }
@@ -1274,16 +1281,13 @@ Result SmtEngine::blockModelValues(const std::vector<Node>& exprs)
     getPrinter().toStreamCmdBlockModelValues(d_env->getDumpOut(), exprs);
   }
 
-  Model* m = getAvailableModel("block model values");
+  TheoryModel* m = getAvailableModel("block model values");
 
   // get expanded assertions
   std::vector<Node> eassertsProc = getExpandedAssertions();
   // we always do block model values mode here
-  Node eblocker =
-      ModelBlocker::getModelBlocker(eassertsProc,
-                                    m->getTheoryModel(),
-                                    options::BlockModelsMode::VALUES,
-                                    exprs);
+  Node eblocker = ModelBlocker::getModelBlocker(
+      eassertsProc, m, options::BlockModelsMode::VALUES, exprs);
   return assertFormula(eblocker);
 }
 
@@ -1299,8 +1303,7 @@ std::pair<Node, Node> SmtEngine::getSepHeapAndNilExpr(void)
   NodeManagerScope nms(getNodeManager());
   Node heap;
   Node nil;
-  Model* m = getAvailableModel("get separation logic heap and nil");
-  TheoryModel* tm = m->getTheoryModel();
+  TheoryModel* tm = getAvailableModel("get separation logic heap and nil");
   if (!tm->getHeapModel(heap, nil))
   {
     const char* msg =
@@ -1548,7 +1551,7 @@ void SmtEngine::checkModel(bool hardFailure) {
   TimerStat::CodeTimer checkModelTimer(d_stats->d_checkModelTime);
 
   Notice() << "SmtEngine::checkModel(): generating model" << endl;
-  Model* m = getAvailableModel("check model");
+  TheoryModel* m = getAvailableModel("check model");
   Assert(m != nullptr);
 
   // check the model with the theory engine for debugging
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 84501d35e..06a1c9ae4 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -42,7 +42,6 @@ class Env;
 class NodeManager;
 class TheoryEngine;
 class UnsatCore;
-class LogicRequest;
 class StatisticsRegistry;
 class Printer;
 class ResourceManager;
@@ -77,7 +76,6 @@ namespace prop {
 
 namespace smt {
 /** Utilities */
-class Model;
 class SmtEngineState;
 class AbstractValues;
 class Assertions;
@@ -104,9 +102,10 @@ class UnsatCoreManager;
 /* -------------------------------------------------------------------------- */
 
 namespace theory {
-  class Rewriter;
-  class QuantifiersEngine;
-  }  // namespace theory
+class TheoryModel;
+class Rewriter;
+class QuantifiersEngine;
+}  // namespace theory
 
 /* -------------------------------------------------------------------------- */
 
@@ -115,7 +114,6 @@ class CVC5_EXPORT SmtEngine
   friend class ::cvc5::api::Solver;
   friend class ::cvc5::smt::SmtEngineState;
   friend class ::cvc5::smt::SmtScope;
-  friend class ::cvc5::LogicRequest;
 
   /* .......................................................................  */
  public:
@@ -227,14 +225,6 @@ class CVC5_EXPORT SmtEngine
   bool isInternalSubsolver() const;
 
   /**
-   * Get the model (only if immediately preceded by a SAT or NOT_ENTAILED
-   * query).  Only permitted if produce-models is on.
-   *
-   * TODO (issues#287): eliminate this method.
-   */
-  smt::Model* getModel();
-
-  /**
    * Block the current model. Can be called only if immediately preceded by
    * a SAT or INVALID query. Only permitted if produce-models is on, and the
    * block-models option is set to a mode other than "none".
@@ -523,6 +513,19 @@ class CVC5_EXPORT SmtEngine
    */
   bool isModelCoreSymbol(Node v);
 
+  /**
+   * Get a model (only if immediately preceded by an SAT or unknown query).
+   * Only permitted if the model option is on.
+   *
+   * @param declaredSorts The sorts to print in the model
+   * @param declaredFuns The free constants to print in the model. A subset
+   * of these may be printed based on isModelCoreSymbol.
+   * @return the string corresponding to the model. If the output language is
+   * smt2, then this corresponds to a response to the get-model command.
+   */
+  std::string getModel(const std::vector<TypeNode>& declaredSorts,
+                       const std::vector<Node>& declaredFuns);
+
   /** print instantiations
    *
    * Print all instantiations for all quantified formulas on out,
@@ -936,7 +939,7 @@ class CVC5_EXPORT SmtEngine
    * @param c used for giving an error message to indicate the context
    * this method was called.
    */
-  smt::Model* getAvailableModel(const char* c) const;
+  theory::TheoryModel* getAvailableModel(const char* c) const;
   /**
    * Get available quantifiers engine, which throws a modal exception if it
    * does not exist. This can happen if a quantifiers-specific call (e.g.
@@ -1047,13 +1050,6 @@ class CVC5_EXPORT SmtEngine
   std::unique_ptr<smt::SmtSolver> d_smtSolver;
 
   /**
-   * The SMT-level model object, which contains information about how to
-   * print the model, as well as a pointer to the underlying TheoryModel
-   * implementation maintained by the SmtSolver.
-   */
-  std::unique_ptr<smt::Model> d_model;
-
-  /**
    * The utility used for checking models
    */
   std::unique_ptr<smt::CheckModels> d_checkModels;