Merge branch 'master' into fixClangWarnings

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 */