diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-09-01 17:14:06 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-09-01 17:14:06 -0700 |
commit | 5ae076e726a013039c8392277437902600359b17 (patch) | |
tree | 3c840960cdf0199d9f7fe78fafaf2f8e79365c39 /src/smt/smt_engine.h | |
parent | b1582722951f6925d3422ec21906d24f5c8cdfc0 (diff) | |
parent | 351fe43811e35f04ced22ca459fa31f7dd94937f (diff) |
Merge branch 'master' into macos11macos11
Diffstat (limited to 'src/smt/smt_engine.h')
-rw-r--r-- | src/smt/smt_engine.h | 40 |
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; |