diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-03-13 15:03:41 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-03-13 15:03:41 -0700 |
commit | 10f091e4fc23f80c884520ff484cacb125b45172 (patch) | |
tree | 4b637901582f7b776516ba1ed7a16a3a851833da /src | |
parent | c93aa9c154b51220607e0eda46109cf509b96a34 (diff) |
SmtEngine::getModel() is now public. (#1665)
Diffstat (limited to 'src')
-rw-r--r-- | src/smt/smt_engine.h | 16 |
1 files 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; @@ -489,6 +480,13 @@ class CVC4_PUBLIC SmtEngine { /* 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. */ CVC4::SExpr getOption(const std::string& key) const |