diff options
Diffstat (limited to 'src/smt/model.cpp')
-rw-r--r-- | src/smt/model.cpp | 47 |
1 files changed, 29 insertions, 18 deletions
diff --git a/src/smt/model.cpp b/src/smt/model.cpp index 6f6a09f38..fc9ea8fbb 100644 --- a/src/smt/model.cpp +++ b/src/smt/model.cpp @@ -5,7 +5,7 @@ ** Morgan Deters, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. + ** in the top-level source directory and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** @@ -14,19 +14,23 @@ #include "smt/model.h" -#include <vector> - #include "expr/expr_iomanip.h" #include "options/base_options.h" #include "printer/printer.h" -#include "smt/command.h" -#include "smt/command_list.h" +#include "smt/dump_manager.h" +#include "smt/node_command.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" - -using namespace std; +#include "theory/theory_model.h" namespace CVC4 { +namespace smt { + +Model::Model(SmtEngine& smt, theory::TheoryModel* tm) + : d_smt(smt), 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); @@ -35,20 +39,27 @@ std::ostream& operator<<(std::ostream& out, const Model& m) { return out; } -Model::Model() : d_smt(*smt::currentSmtEngine()), d_isKnownSat(false) {} +size_t Model::getNumCommands() const +{ + return d_smt.getDumpManager()->getNumModelCommands(); +} -size_t Model::getNumCommands() const { - return d_smt.d_modelCommands->size() + d_smt.d_modelGlobalCommands.size(); +const NodeCommand* Model::getCommand(size_t i) const +{ + return d_smt.getDumpManager()->getModelCommand(i); } -const Command* Model::getCommand(size_t i) const { - Assert(i < getNumCommands()); - // index the global commands first, then the locals - if(i < d_smt.d_modelGlobalCommands.size()) { - return d_smt.d_modelGlobalCommands[i]; - } else { - return (*d_smt.d_modelCommands)[i - d_smt.d_modelGlobalCommands.size()]; - } +theory::TheoryModel* Model::getTheoryModel() { return d_tmodel; } + +const theory::TheoryModel* Model::getTheoryModel() const { return d_tmodel; } + +bool Model::isModelCoreSymbol(TNode sym) const +{ + return d_tmodel->isModelCoreSymbol(sym); } +Node Model::getValue(TNode n) const { return d_tmodel->getValue(n); } + +bool Model::hasApproximations() const { return d_tmodel->hasApproximations(); } +} // namespace smt }/* CVC4 namespace */ |