Merge branch 'master' into fixClangWarnings

1 files changed, 16 insertions, 7 deletions

diff --git a/src/proof/unsat_core.cpp b/src/proof/unsat_core.cpp
index e54d976c9..dd470b299 100644
--- a/src/proof/unsat_core.cpp
+++ b/src/proof/unsat_core.cpp
@@ -5,13 +5,11 @@
  **   Morgan Deters, Clark Barrett, 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
  **
  ** \brief Representation of unsat cores
- **
- ** Representation of unsat cores.
  **/
 
 #include "proof/unsat_core.h"
@@ -20,15 +18,28 @@
 #include "expr/expr_iomanip.h"
 #include "options/base_options.h"
 #include "printer/printer.h"
-#include "smt/command.h"
 #include "smt/smt_engine_scope.h"
 
 namespace CVC4 {
 
-void UnsatCore::initMessage() const {
+UnsatCore::UnsatCore(const std::vector<Node>& core)
+    : d_useNames(false), d_core(core), d_names()
+{
   Debug("core") << "UnsatCore size " << d_core.size() << std::endl;
 }
 
+UnsatCore::UnsatCore(std::vector<std::string>& names)
+    : d_useNames(true), d_core(), d_names(names)
+{
+  Debug("core") << "UnsatCore (names) size " << d_names.size() << std::endl;
+}
+
+const std::vector<Node>& UnsatCore::getCore() const { return d_core; }
+const std::vector<std::string>& UnsatCore::getCoreNames() const
+{
+  return d_names;
+}
+
 UnsatCore::const_iterator UnsatCore::begin() const {
   return d_core.begin();
 }
@@ -38,8 +49,6 @@ UnsatCore::const_iterator UnsatCore::end() const {
 }
 
 void UnsatCore::toStream(std::ostream& out) const {
-  Assert(d_smt != NULL);
-  smt::SmtScope smts(d_smt);
   expr::ExprDag::Scope scope(out, false);
   Printer::getPrinter(options::outputLanguage())->toStream(out, *this);
 }