From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Tue, 13 Mar 2018 22:03:41 +0000 (-0700)
Subject: SmtEngine::getModel() is now public. (#1665)
X-Git-Tag: cvc5-1.0.0~5238
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=10f091e4fc23f80c884520ff484cacb125b45172;p=cvc5.git

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

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 377888a5a..83300afc9 100644
--- 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.
    */