diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-07-03 17:13:31 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-11-27 17:55:53 -0500 |
commit | a97891f9cc892fdc261cd4e3d3229ec68f05b45e (patch) | |
tree | a05c30ddbe81d9dd084a2e024875f829d6f1f3a7 /src/util/util_model.cpp | |
parent | b28a42c3a4fd8c9b079b157ad8ff36e581b60d29 (diff) |
General pre-release cleanup commit
* Rename {model,util_model}.{h,cpp} files to match class names
* Fix alreadyVisited() issue in TheoryEngine
* Remove spurious Message that causes compliance issues
* Update copyrights, fix public/private markings in headers
* minor comment fixes
* remove EXTRACT_OP as a special-case in typechecker
* note about rewriters in theoryskel readme
* Clean up some compiler warnings
* Code typos and spacing
Diffstat (limited to 'src/util/util_model.cpp')
-rw-r--r-- | src/util/util_model.cpp | 52 |
1 files changed, 0 insertions, 52 deletions
diff --git a/src/util/util_model.cpp b/src/util/util_model.cpp deleted file mode 100644 index 1c2dc2edf..000000000 --- a/src/util/util_model.cpp +++ /dev/null @@ -1,52 +0,0 @@ -/********************* */ -/*! \file util_model.cpp - ** \verbatim - ** Original author: Clark Barrett - ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 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 "util/util_model.h" -#include "expr/command.h" -#include "smt/smt_engine_scope.h" -#include "smt/command_list.h" -#include "printer/printer.h" - -#include <vector> - -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 */ |