Merge branch 'master' into macos11macos11

1 files changed, 18 insertions, 22 deletions

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;