GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/proof/unsat_core.h Lines: 2 2 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file unsat_core.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Morgan Deters, Mathias Preiner
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 "cvc4_private.h"
16
17
#ifndef CVC4__UNSAT_CORE_H
18
#define CVC4__UNSAT_CORE_H
19
20
#include <iosfwd>
21
#include <vector>
22
23
#include "expr/node.h"
24
25
namespace CVC4 {
26
27
/**
28
 * An unsat core, which can optionally be initialized as a list of names
29
 * or as a list of formulas.
30
 */
31
class UnsatCore
32
{
33
 public:
34
  UnsatCore() {}
35
  /** Initialize using assertions */
36
  UnsatCore(const std::vector<Node>& core);
37
  /** Initialize using assertion names */
38
  UnsatCore(std::vector<std::string>& names);
39
918
  ~UnsatCore() {}
40
41
  /** Whether we are using names for this unsat core */
42
10
  bool useNames() const { return d_useNames; }
43
  /** Get the assertions in the unsat core */
44
  const std::vector<Node>& getCore() const;
45
  /** Get their names */
46
  const std::vector<std::string>& getCoreNames() const;
47
48
  typedef std::vector<Node>::const_iterator iterator;
49
  typedef std::vector<Node>::const_iterator const_iterator;
50
51
  const_iterator begin() const;
52
  const_iterator end() const;
53
54
  /**
55
   * prints this UnsatCore object to the stream out.
56
   */
57
  void toStream(std::ostream& out) const;
58
59
 private:
60
  /** Whether we are using names for this unsat core */
61
  bool d_useNames;
62
  /** The unsat core */
63
  std::vector<Node> d_core;
64
  /** The names of assertions in the above core */
65
  std::vector<std::string> d_names;
66
};/* class UnsatCore */
67
68
/** Print the unsat core to stream out */
69
std::ostream& operator<<(std::ostream& out, const UnsatCore& core);
70
71
}/* CVC4 namespace */
72
73
#endif /* CVC4__UNSAT_CORE_H */