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

Line Exec Source
1
/*********************                                                        */
2
/*! \file trust_node.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Gereon Kremer
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 The trust node utility
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__TRUST_NODE_H
18
#define CVC4__THEORY__TRUST_NODE_H
19
20
#include "expr/node.h"
21
22
namespace CVC4 {
23
24
class ProofGenerator;
25
class ProofNode;
26
27
namespace theory {
28
29
/** A kind for trust nodes */
30
enum class TrustNodeKind : uint32_t
31
{
32
  CONFLICT,
33
  LEMMA,
34
  PROP_EXP,
35
  REWRITE,
36
  INVALID
37
};
38
/**
39
 * Converts a proof rule to a string. Note: This function is also used in
40
 * `safe_print()`. Changing this function name or signature will result in
41
 * `safe_print()` printing "<unsupported>" instead of the proper strings for
42
 * the enum values.
43
 *
44
 * Returns a string with static lifetime: it should not be freed.
45
 *
46
 * @param tnk The trust node kind
47
 * @return The name of the trust node kind
48
 */
49
const char* toString(TrustNodeKind tnk);
50
51
/**
52
 * Writes a trust node kind name to a stream.
53
 *
54
 * @param out The stream to write to
55
 * @param tnk The trust node kind to write to the stream
56
 * @return The stream
57
 */
58
std::ostream& operator<<(std::ostream& out, TrustNodeKind tnk);
59
60
/**
61
 * A trust node is a pair (F, G) where F is a formula and G is a proof
62
 * generator that can construct a proof for F if asked.
63
 *
64
 * More generally, a trust node is any node that can be used for a specific
65
 * purpose that requires justification, such as being passed to
66
 * OutputChannel::lemma. That justification is intended to be given by the
67
 * generator that is required to construct this object.
68
 *
69
 * They are intended to be constructed by ProofGenerator objects themselves (a
70
 * proof generator wraps itself in TrustNode it returns) and passed
71
 * to ProofOutputChannel by theory solvers.
72
 *
73
 * The static functions for constructing them check that the generator, if
74
 * provided, is capable of proving the given conflict or lemma, or an assertion
75
 * failure occurs. Otherwise an assertion error is given.
76
 *
77
 * While this is not enforced, a `TrustNode` generally encapsulates a **closed** proof
78
 * of the formula: one without free assumptions.
79
 */
80
9319896
class TrustNode
81
{
82
 public:
83
3227636
  TrustNode() : d_tnk(TrustNodeKind::INVALID), d_gen(nullptr) {}
84
  /** Make a proven node for conflict */
85
  static TrustNode mkTrustConflict(Node conf, ProofGenerator* g = nullptr);
86
  /** Make a proven node for lemma */
87
  static TrustNode mkTrustLemma(Node lem, ProofGenerator* g = nullptr);
88
  /** Make a proven node for explanation of propagated literal */
89
  static TrustNode mkTrustPropExp(TNode lit,
90
                                  Node exp,
91
                                  ProofGenerator* g = nullptr);
92
  /** Make a proven node for rewrite */
93
  static TrustNode mkTrustRewrite(TNode n,
94
                                  Node nr,
95
                                  ProofGenerator* g = nullptr);
96
  /** The null proven node */
97
  static TrustNode null();
98
19210080
  ~TrustNode() {}
99
  /** get kind */
100
  TrustNodeKind getKind() const;
101
  /** get node
102
   *
103
   * This is the node that is used in a common interface, either:
104
   * (1) A T-unsat conjunction conf to pass to OutputChannel::conflict,
105
   * (2) A valid T-formula lem to pass to OutputChannel::lemma,
106
   * (3) A conjunction of literals exp to return in Theory::explain(lit), or
107
   * (4) A result of rewriting a term n into an equivalent one nr.
108
   *
109
   * Notice that this node does not necessarily correspond to a valid formula.
110
   * The call getProven() below retrieves a valid formula corresponding to
111
   * the above calls.
112
   */
113
  Node getNode() const;
114
  /** get proven
115
   *
116
   * This is the corresponding formula that is proven by the proof generator
117
   * for the above cases:
118
   * (1) (not conf), for conflicts,
119
   * (2) lem, for lemmas,
120
   * (3) (=> exp lit), for propagations from explanations,
121
   * (4) (= n nr), for results of rewriting.
122
   *
123
   * When constructing this trust node, the proof generator should be able to
124
   * provide a proof for this fact.
125
   */
126
  Node getProven() const;
127
  /** get generator */
128
  ProofGenerator* getGenerator() const;
129
  /** is null? */
130
  bool isNull() const;
131
  /**
132
   * Gets the proof node for this trust node, which is obtained by
133
   * calling the generator's getProofFor method on the proven node.
134
   */
135
  std::shared_ptr<ProofNode> toProofNode() const;
136
137
  /** Get the proven formula corresponding to a conflict call */
138
  static Node getConflictProven(Node conf);
139
  /** Get the proven formula corresponding to a lemma call */
140
  static Node getLemmaProven(Node lem);
141
  /** Get the proven formula corresponding to explanations for propagation */
142
  static Node getPropExpProven(TNode lit, Node exp);
143
  /** Get the proven formula corresponding to a rewrite */
144
  static Node getRewriteProven(TNode n, Node nr);
145
  /** For debugging */
146
  std::string identifyGenerator() const;
147
148
  /**
149
   * debug check closed on Trace c, context ctx is string for debugging
150
   *
151
   * @param reqNullGen Whether we consider a null generator to be a failure.
152
   */
153
  void debugCheckClosed(const char* c, const char* ctx, bool reqNullGen = true);
154
155
 private:
156
  TrustNode(TrustNodeKind tnk, Node p, ProofGenerator* g = nullptr);
157
  /** The kind */
158
  TrustNodeKind d_tnk;
159
  /** The proven node */
160
  Node d_proven;
161
  /** The generator */
162
  ProofGenerator* d_gen;
163
};
164
165
/**
166
 * Writes a trust node to a stream.
167
 *
168
 * @param out The stream to write to
169
 * @param n The trust node to write to the stream
170
 * @return The stream
171
 */
172
std::ostream& operator<<(std::ostream& out, TrustNode n);
173
174
}  // namespace theory
175
}  // namespace CVC4
176
177
#endif /* CVC4__THEORY__TRUST_NODE_H */