GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/proof/unsat_core.cpp Lines: 19 23 82.6 %
Date: 2021-03-23 Branches: 18 42 42.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file unsat_core.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Morgan Deters, Andrew Reynolds, Clark Barrett
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 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
15
#include "proof/unsat_core.h"
16
17
#include "base/check.h"
18
#include "expr/expr_iomanip.h"
19
#include "options/base_options.h"
20
#include "printer/printer.h"
21
#include "smt/smt_engine_scope.h"
22
23
namespace CVC4 {
24
25
911
UnsatCore::UnsatCore(const std::vector<Node>& core)
26
911
    : d_useNames(false), d_core(core), d_names()
27
{
28
911
  Debug("core") << "UnsatCore size " << d_core.size() << std::endl;
29
911
}
30
31
7
UnsatCore::UnsatCore(std::vector<std::string>& names)
32
7
    : d_useNames(true), d_core(), d_names(names)
33
{
34
7
  Debug("core") << "UnsatCore (names) size " << d_names.size() << std::endl;
35
7
}
36
37
const std::vector<Node>& UnsatCore::getCore() const { return d_core; }
38
7
const std::vector<std::string>& UnsatCore::getCoreNames() const
39
{
40
7
  return d_names;
41
}
42
43
919
UnsatCore::const_iterator UnsatCore::begin() const {
44
919
  return d_core.begin();
45
}
46
47
3543
UnsatCore::const_iterator UnsatCore::end() const {
48
3543
  return d_core.end();
49
}
50
51
10
void UnsatCore::toStream(std::ostream& out) const {
52
20
  expr::ExprDag::Scope scope(out, false);
53
10
  Printer::getPrinter(options::outputLanguage())->toStream(out, *this);
54
10
}
55
56
std::ostream& operator<<(std::ostream& out, const UnsatCore& core) {
57
  core.toStream(out);
58
  return out;
59
}
60
61
26685
}/* CVC4 namespace */