diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-03 09:40:52 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-03 09:40:52 -0500 |
commit | 5a3569cbeba6c53c157f4fb8e88016c5a501cafb (patch) | |
tree | 8ed6fac7663c7ba722236f4b9e8c0d4cefbb4736 /src/smt/model.cpp | |
parent | 4caca6f74cc23b185757648bbf6f20daa6e78303 (diff) |
Split dump manager from SmtEngine (#4824)
Towards splitting SmtEngine.
This moves utilities related to managing information for dumping to its own utility, DumpManager.
Its current responsibilities are to track information about how to print a model, and the implementation of some dumping traces, although its responsibilities should be extended further so that SmtEngine is not responsible for any command dumping. This is future work.
Diffstat (limited to 'src/smt/model.cpp')
-rw-r--r-- | src/smt/model.cpp | 18 |
1 files changed, 7 insertions, 11 deletions
diff --git a/src/smt/model.cpp b/src/smt/model.cpp index 6f6a09f38..7924698ff 100644 --- a/src/smt/model.cpp +++ b/src/smt/model.cpp @@ -20,7 +20,7 @@ #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/smt_engine.h" #include "smt/smt_engine_scope.h" @@ -37,18 +37,14 @@ std::ostream& operator<<(std::ostream& out, const Model& m) { Model::Model() : d_smt(*smt::currentSmtEngine()), d_isKnownSat(false) {} -size_t Model::getNumCommands() const { - return d_smt.d_modelCommands->size() + d_smt.d_modelGlobalCommands.size(); +size_t Model::getNumCommands() const +{ + return d_smt.getDumpManager()->getNumModelCommands(); } -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()]; - } +const Command* Model::getCommand(size_t i) const +{ + return d_smt.getDumpManager()->getModelCommand(i); } }/* CVC4 namespace */ |