diff options
Diffstat (limited to 'src/smt_util/model.cpp')
-rw-r--r-- | src/smt_util/model.cpp | 53 |
1 files changed, 53 insertions, 0 deletions
diff --git a/src/smt_util/model.cpp b/src/smt_util/model.cpp new file mode 100644 index 000000000..3f0423f49 --- /dev/null +++ b/src/smt_util/model.cpp @@ -0,0 +1,53 @@ +/********************* */ +/*! \file model.cpp + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: Morgan Deters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief implementation of Model class + **/ + +#include "smt_util/model.h" + +#include <vector> + +#include "smt_util/command.h" +#include "smt/smt_engine_scope.h" +#include "smt/command_list.h" +#include "printer/printer.h" + +using namespace std; + +namespace CVC4 { + +std::ostream& operator<<(std::ostream& out, const Model& m) { + smt::SmtScope smts(&m.d_smt); + Expr::dag::Scope scope(out, false); + Printer::getPrinter(options::outputLanguage())->toStream(out, m); + return out; +} + +Model::Model() : + d_smt(*smt::currentSmtEngine()) { +} + +size_t Model::getNumCommands() const { + return d_smt.d_modelCommands->size() + d_smt.d_modelGlobalCommands.size(); +} + +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()]; + } +} + +}/* CVC4 namespace */ |