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
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
|
/********************* */
/*! \file proof_node_manager.h
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds, Haniel Barbosa, 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 Proof node manager utility
**/
#include "cvc4_private.h"
#ifndef CVC4__EXPR__PROOF_NODE_MANAGER_H
#define CVC4__EXPR__PROOF_NODE_MANAGER_H
#include <vector>
#include "expr/node.h"
#include "expr/proof_rule.h"
namespace cvc5 {
class ProofChecker;
class ProofNode;
/**
* A manager for proof node objects. This is a trusted interface for creating
* and updating ProofNode objects.
*
* In more detail, we say a ProofNode is "well-formed (with respect to checker
* X)" if its d_proven field is non-null, and corresponds to the formula that
* the ProofNode proves according to X. The ProofNodeManager class constructs
* and update nodes that are well-formed with respect to its underlying checker.
*
* If no checker is provided, then the ProofNodeManager assigns the d_proven
* field of ProofNode based on the provided "expected" argument in mkNode below,
* which must be provided in this case.
*
* The ProofNodeManager is used as a trusted way of updating ProofNode objects
* via updateNode below. In particular, this method leaves the d_proven field
* unchanged and updates (if possible) the remaining content of a given proof
* node.
*
* Notice that ProofNode objects are mutable, and hence this class does not
* cache the results of mkNode. A version of this class that caches
* immutable version of ProofNode objects could be built as an extension
* or layer on top of this class.
*/
class ProofNodeManager
{
public:
ProofNodeManager(ProofChecker* pc = nullptr);
~ProofNodeManager() {}
/**
* This constructs a ProofNode with the given arguments. The expected
* argument, when provided, indicates the formula that the returned node
* is expected to prove. If we find that it does not, based on the underlying
* checker, this method returns nullptr.
*
* @param id The id of the proof node.
* @param children The children of the proof node.
* @param args The arguments of the proof node.
* @param expected (Optional) the expected conclusion of the proof node.
* @return the proof node, or nullptr if the given arguments do not
* consistute a proof of the expected conclusion according to the underlying
* checker, if both are provided. It also returns nullptr if neither the
* checker nor the expected field is provided, since in this case the
* conclusion is unknown.
*/
std::shared_ptr<ProofNode> mkNode(
PfRule id,
const std::vector<std::shared_ptr<ProofNode>>& children,
const std::vector<Node>& args,
Node expected = Node::null());
/**
* Make the proof node corresponding to the assumption of fact.
*
* @param fact The fact to assume.
* @return The ASSUME proof of fact.
*/
std::shared_ptr<ProofNode> mkAssume(Node fact);
/**
* Make transitivity proof, where children contains one or more proofs of
* equalities that form an ordered chain. In other words, the vector children
* is a legal set of children for an application of TRANS.
*/
std::shared_ptr<ProofNode> mkTrans(
const std::vector<std::shared_ptr<ProofNode>>& children,
Node expected = Node::null());
/**
* Make scope having body pf and arguments (assumptions-to-close) assumps.
* If ensureClosed is true, then this method throws an assertion failure if
* the returned proof is not closed. This is the case if a free assumption
* of pf is missing from the vector assumps.
*
* For conveinence, the proof pf may be modified to ensure that the overall
* result is closed. For instance, given input:
* pf = TRANS( ASSUME( x=y ), ASSUME( y=z ) )
* assumps = { y=x, y=z }
* This method will modify pf to be:
* pf = TRANS( SYMM( ASSUME( y=x ) ), ASSUME( y=z ) )
* so that y=x matches the free assumption. The returned proof is:
* SCOPE(TRANS( SYMM( ASSUME( y=x ) ), ASSUME( y=z ) ) :args { y=x, y=z })
*
* When ensureClosed is true, duplicates are eliminated from assumps. The
* reason for this is due to performance, since in this method, assumps is
* converted to an unordered_set to do the above check and hence it is a
* convienient time to eliminate duplicate literals.
*
* Additionally, if both ensureClosed and doMinimize are true, assumps is
* updated to contain exactly the free asumptions of pf. This also includes
* having no duplicates. Furthermore, if assumps is empty after minimization,
* this method is a no-op.
*
* In each case, the update vector assumps is passed as arguments to SCOPE.
*
* @param pf The body of the proof,
* @param assumps The assumptions-to-close of the scope,
* @param ensureClosed Whether to ensure that the proof is closed,
* @param doMinimize Whether to minimize assumptions.
* @param expected the node that the scope should prove.
* @return The scoped proof.
*/
std::shared_ptr<ProofNode> mkScope(std::shared_ptr<ProofNode> pf,
std::vector<Node>& assumps,
bool ensureClosed = true,
bool doMinimize = false,
Node expected = Node::null());
/**
* This method updates pn to be a proof of the form <id>( children, args ),
* while maintaining its d_proven field. This method returns false if this
* proof manager is using a checker, and we compute that the above proof
* is not a proof of the fact that pn previously proved.
*
* @param pn The proof node to update.
* @param id The updated id of the proof node.
* @param children The updated children of the proof node.
* @param args The updated arguments of the proof node.
* @return true if the update was successful.
*
* Notice that updateNode always returns true if there is no underlying
* checker.
*/
bool updateNode(ProofNode* pn,
PfRule id,
const std::vector<std::shared_ptr<ProofNode>>& children,
const std::vector<Node>& args);
/**
* Update node pn to have the contents of pnr. It should be the case that
* pn and pnr prove the same fact, otherwise false is returned and pn is
* unchanged.
*/
bool updateNode(ProofNode* pn, ProofNode* pnr);
/** Get the underlying proof checker */
ProofChecker* getChecker() const;
private:
/** The (optional) proof checker */
ProofChecker* d_checker;
/** the true node */
Node d_true;
/** Check internal
*
* This returns the result of proof checking a ProofNode with the provided
* arguments with an expected conclusion, which may not null if there is
* no expected conclusion.
*
* This throws an assertion error if we fail to check such a proof node, or
* if expected is provided (non-null) and is different what is proven by the
* other arguments.
*/
Node checkInternal(PfRule id,
const std::vector<std::shared_ptr<ProofNode>>& children,
const std::vector<Node>& args,
Node expected);
/**
* Update node internal, return true if successful. This is called by
* the update node methods above. The argument needsCheck is whether we
* need to check the correctness of the rule application. This is false
* for the updateNode routine where pnr is an (already checked) proof node.
*/
bool updateNodeInternal(
ProofNode* pn,
PfRule id,
const std::vector<std::shared_ptr<ProofNode>>& children,
const std::vector<Node>& args,
bool needsCheck);
};
} // namespace cvc5
#endif /* CVC4__EXPR__PROOF_NODE_H */
|
