src/proof/unsat_core.cpp

   1 /*********************                                                        */
   2 /*! \file unsat_core.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Clark Barrett, Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Representation of unsat cores
  13  **
  14  ** Representation of unsat cores.
  15  **/
  16
  17 #include "proof/unsat_core.h"
  18
  19 #include "base/check.h"
  20 #include "expr/expr_iomanip.h"
  21 #include "options/base_options.h"
  22 #include "printer/printer.h"
  23 #include "smt/command.h"
  24 #include "smt/smt_engine_scope.h"
  25
  26 namespace CVC4 {
  27
  28 void UnsatCore::initMessage() const {
  29   Debug("core") << "UnsatCore size " << d_core.size() << std::endl;
  30 }
  31
  32 UnsatCore::const_iterator UnsatCore::begin() const {
  33   return d_core.begin();
  34 }
  35
  36 UnsatCore::const_iterator UnsatCore::end() const {
  37   return d_core.end();
  38 }
  39
  40 void UnsatCore::toStream(std::ostream& out) const {
  41   Assert(d_smt != NULL);
  42   smt::SmtScope smts(d_smt);
  43   expr::ExprDag::Scope scope(out, false);
  44   Printer::getPrinter(options::outputLanguage())->toStream(out, *this);
  45 }
  46
  47 std::ostream& operator<<(std::ostream& out, const UnsatCore& core) {
  48   core.toStream(out);
  49   return out;
  50 }
  51
  52 }/* CVC4 namespace */