From 10f091e4fc23f80c884520ff484cacb125b45172 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 13 Mar 2018 15:03:41 -0700 Subject: [PATCH] SmtEngine::getModel() is now public. (#1665) --- src/smt/smt_engine.h | 16 +++++++--------- 1 file changed, 7 insertions(+), 9 deletions(-) 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. */ -- 2.30.2