SmtEngine::getModel() is now public. (#1665)

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 377888a5a452a58fb44fa2497b97f1f0a49f43a1..83300afc942a306622f7c3728abf4d8c85ac6fe5 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -387,8 +387,6 @@ class CVC4_PUBLIC SmtEngine {
   // to access d_modelCommands
   friend class ::CVC4::Model;
   friend class ::CVC4::theory::TheoryModel;
-  // to access getModel(), which is private (for now)
-  friend class GetModelCommand;
 
   StatisticsRegistry* d_statisticsRegistry;
 
@@ -403,13 +401,6 @@ class CVC4_PUBLIC SmtEngine {
    */
   void addToModelCommandAndDump(const Command& c, uint32_t flags = 0, bool userVisible = true, const char* dumpTag = "declarations");
 
-  /**
-   * Get the model (only if immediately preceded by a SAT
-   * or INVALID query).  Only permitted if CVC4 was built with model
-   * support and produce-models is on.
-   */
-  Model* getModel();
-
   // disallow copy/assignment
   SmtEngine(const SmtEngine&) CVC4_UNDEFINED;
   SmtEngine& operator=(const SmtEngine&) CVC4_UNDEFINED;
@@ -488,6 +479,13 @@ class CVC4_PUBLIC SmtEngine {
   void setOption(const std::string& key, const CVC4::SExpr& value)
       /* throw(OptionException, ModalException) */;
 
+  /**
+   * Get the model (only if immediately preceded by a SAT
+   * or INVALID query).  Only permitted if CVC4 was built with model
+   * support and produce-models is on.
+   */
+  Model* getModel();
+
   /**
    * Get an aspect of the current SMT execution environment.
    */