diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-26 09:15:30 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-11-26 09:15:30 -0600 |
commit | d3eb6f04bcdb6c22a2f796a19ff96094d2cfbb88 (patch) | |
tree | bd51ec106bd30add6a8a9e5f3300a6ae022f0e97 /src/smt/model.cpp | |
parent | 70f0cddbce01fa17622b7b70b638794181aefec5 (diff) |
Removing infrastructure related to SMT model (#5527)
Now, SMT models do not store an internal list of commands, and are not dependent on a reference to SmtEngine.
The next cleanup step will be to merge OutputManager, DumpManager, and SmtEngineNodeListener.
Diffstat (limited to 'src/smt/model.cpp')
-rw-r--r-- | src/smt/model.cpp | 14 |
1 files changed, 1 insertions, 13 deletions
diff --git a/src/smt/model.cpp b/src/smt/model.cpp index b734ad9e9..8a9f944d2 100644 --- a/src/smt/model.cpp +++ b/src/smt/model.cpp @@ -26,29 +26,17 @@ namespace CVC4 { namespace smt { -Model::Model(SmtEngine& smt, theory::TheoryModel* tm) - : d_smt(smt), d_isKnownSat(false), d_tmodel(tm) +Model::Model(theory::TheoryModel* tm) : d_isKnownSat(false), d_tmodel(tm) { Assert(d_tmodel != nullptr); } std::ostream& operator<<(std::ostream& out, const Model& m) { - smt::SmtScope smts(&m.d_smt); expr::ExprDag::Scope scope(out, false); Printer::getPrinter(options::outputLanguage())->toStream(out, m); return out; } -size_t Model::getNumCommands() const -{ - return d_smt.getDumpManager()->getNumModelCommands(); -} - -const NodeCommand* Model::getCommand(size_t i) const -{ - return d_smt.getDumpManager()->getModelCommand(i); -} - theory::TheoryModel* Model::getTheoryModel() { return d_tmodel; } const theory::TheoryModel* Model::getTheoryModel() const { return d_tmodel; } |