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