Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Hans-Joerg Schurr, Haniel Barbosa
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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.
11 : : * ****************************************************************************
12 : : *
13 : : * Proof node manager utility.
14 : : */
15 : :
16 : : #include "cvc5_private.h"
17 : :
18 : : #ifndef CVC5__PROOF__PROOF_NODE_MANAGER_H
19 : : #define CVC5__PROOF__PROOF_NODE_MANAGER_H
20 : :
21 : : #include <vector>
22 : :
23 : : #include "cvc5/cvc5_proof_rule.h"
24 : : #include "expr/node.h"
25 : : #include "proof/trust_id.h"
26 : :
27 : : namespace cvc5::internal {
28 : :
29 : : class ProofChecker;
30 : : class ProofNode;
31 : : class Options;
32 : :
33 : : namespace theory {
34 : : class Rewriter;
35 : : }
36 : :
37 : : /**
38 : : * A manager for proof node objects. This is a trusted interface for creating
39 : : * and updating ProofNode objects.
40 : : *
41 : : * In more detail, we say a ProofNode is "well-formed (with respect to checker
42 : : * X)" if its d_proven field is non-null, and corresponds to the formula that
43 : : * the ProofNode proves according to X. The ProofNodeManager class constructs
44 : : * and update nodes that are well-formed with respect to its underlying checker.
45 : : *
46 : : * If no checker is provided, then the ProofNodeManager assigns the d_proven
47 : : * field of ProofNode based on the provided "expected" argument in mkNode below,
48 : : * which must be provided in this case.
49 : : *
50 : : * The ProofNodeManager is used as a trusted way of updating ProofNode objects
51 : : * via updateNode below. In particular, this method leaves the d_proven field
52 : : * unchanged and updates (if possible) the remaining content of a given proof
53 : : * node.
54 : : *
55 : : * Notice that ProofNode objects are mutable, and hence this class does not
56 : : * cache the results of mkNode. A version of this class that caches
57 : : * immutable version of ProofNode objects could be built as an extension
58 : : * or layer on top of this class.
59 : : */
60 : : class ProofNodeManager
61 : : {
62 : : public:
63 : : ProofNodeManager(const Options& opts,
64 : : theory::Rewriter* rr,
65 : : ProofChecker* pc = nullptr);
66 : 19888 : ~ProofNodeManager() {}
67 : : /**
68 : : * This constructs a ProofNode with the given arguments. The expected
69 : : * argument, when provided, indicates the formula that the returned node
70 : : * is expected to prove. If we find that it does not, based on the underlying
71 : : * checker, this method returns nullptr.
72 : : *
73 : : * @param id The id of the proof node.
74 : : * @param children The children of the proof node.
75 : : * @param args The arguments of the proof node.
76 : : * @param expected (Optional) the expected conclusion of the proof node.
77 : : * @return the proof node, or nullptr if the given arguments do not
78 : : * consistute a proof of the expected conclusion according to the underlying
79 : : * checker, if both are provided. It also returns nullptr if neither the
80 : : * checker nor the expected field is provided, since in this case the
81 : : * conclusion is unknown.
82 : : */
83 : : std::shared_ptr<ProofNode> mkNode(
84 : : ProofRule id,
85 : : const std::vector<std::shared_ptr<ProofNode>>& children,
86 : : const std::vector<Node>& args,
87 : : Node expected = Node::null());
88 : : /**
89 : : * This constructs a ProofNode with rule ProofRule::TRUST with the given
90 : : * children and arguments.
91 : : *
92 : : * @param id The id of the proof node.
93 : : * @param children The children of the proof node.
94 : : * @param args The arguments of the proof node, which are optional additional
95 : : * arguments of ProofRule::TRUST beyond id and conc.
96 : : * @param conc The conclusion of the proof node.
97 : : * @param expected The conclusion of the proof node.
98 : : * @return the proof node, or nullptr if the given arguments do not
99 : : * consistute a proof of the expected conclusion according to the underlying
100 : : * checker, if both are provided. It also returns nullptr if neither the
101 : : * checker nor the expected field is provided, since in this case the
102 : : * conclusion is unknown.
103 : : */
104 : : std::shared_ptr<ProofNode> mkTrustedNode(
105 : : TrustId id,
106 : : const std::vector<std::shared_ptr<ProofNode>>& children,
107 : : const std::vector<Node>& args,
108 : : const Node& conc);
109 : : /**
110 : : * Make the proof node corresponding to the assumption of fact.
111 : : *
112 : : * @param fact The fact to assume.
113 : : * @return The ASSUME proof of fact.
114 : : */
115 : : std::shared_ptr<ProofNode> mkAssume(Node fact);
116 : : /**
117 : : * Make symm, which accounts for whether the child is already a SYMM
118 : : * node, in which case we return its child.
119 : : */
120 : : std::shared_ptr<ProofNode> mkSymm(std::shared_ptr<ProofNode> child,
121 : : Node expected = Node::null());
122 : : /**
123 : : * Make transitivity proof, where children contains one or more proofs of
124 : : * equalities that form an ordered chain. In other words, the vector children
125 : : * is a legal set of children for an application of TRANS.
126 : : */
127 : : std::shared_ptr<ProofNode> mkTrans(
128 : : const std::vector<std::shared_ptr<ProofNode>>& children,
129 : : Node expected = Node::null());
130 : :
131 : : /**
132 : : * Make scope having body pf and arguments (assumptions-to-close) assumps.
133 : : * If ensureClosed is true, then this method throws an assertion failure if
134 : : * the returned proof is not closed. This is the case if a free assumption
135 : : * of pf is missing from the vector assumps.
136 : : *
137 : : * For conveinence, the proof pf may be modified to ensure that the overall
138 : : * result is closed. For instance, given input:
139 : : * pf = TRANS( ASSUME( x=y ), ASSUME( y=z ) )
140 : : * assumps = { y=x, y=z }
141 : : * This method will modify pf to be:
142 : : * pf = TRANS( SYMM( ASSUME( y=x ) ), ASSUME( y=z ) )
143 : : * so that y=x matches the free assumption. The returned proof is:
144 : : * SCOPE(TRANS( SYMM( ASSUME( y=x ) ), ASSUME( y=z ) ) :args { y=x, y=z })
145 : : *
146 : : * When ensureClosed is true, duplicates are eliminated from assumps. The
147 : : * reason for this is due to performance, since in this method, assumps is
148 : : * converted to an unordered_set to do the above check and hence it is a
149 : : * convienient time to eliminate duplicate literals.
150 : : *
151 : : * Additionally, if both ensureClosed and doMinimize are true, assumps is
152 : : * updated to contain exactly the free asumptions of pf. This also includes
153 : : * having no duplicates. Furthermore, if assumps is empty after minimization,
154 : : * this method is a no-op.
155 : : *
156 : : * In each case, the update vector assumps is passed as arguments to SCOPE.
157 : : *
158 : : * @param pf The body of the proof,
159 : : * @param assumps The assumptions-to-close of the scope,
160 : : * @param ensureClosed Whether to ensure that the proof is closed,
161 : : * @param doMinimize Whether to minimize assumptions.
162 : : * @param expected the node that the scope should prove.
163 : : * @return The scoped proof.
164 : : */
165 : : std::shared_ptr<ProofNode> mkScope(std::shared_ptr<ProofNode> pf,
166 : : std::vector<Node>& assumps,
167 : : bool ensureClosed = true,
168 : : bool doMinimize = false,
169 : : Node expected = Node::null());
170 : : /**
171 : : * This method updates pn to be a proof of the form <id>( children, args ),
172 : : * while maintaining its d_proven field. This method returns false if this
173 : : * proof manager is using a checker, and we compute that the above proof
174 : : * is not a proof of the fact that pn previously proved.
175 : : *
176 : : * @param pn The proof node to update.
177 : : * @param id The updated id of the proof node.
178 : : * @param children The updated children of the proof node.
179 : : * @param args The updated arguments of the proof node.
180 : : * @return true if the update was successful.
181 : : *
182 : : * Notice that updateNode always returns true if there is no underlying
183 : : * checker.
184 : : */
185 : : bool updateNode(ProofNode* pn,
186 : : ProofRule id,
187 : : const std::vector<std::shared_ptr<ProofNode>>& children,
188 : : const std::vector<Node>& args);
189 : : /**
190 : : * Update node pn to have the contents of pnr. It should be the case that
191 : : * pn and pnr prove the same fact, otherwise false is returned and pn is
192 : : * unchanged.
193 : : */
194 : : bool updateNode(ProofNode* pn, ProofNode* pnr);
195 : : /**
196 : : * Ensure that pn is checked, regardless of the proof check format.
197 : : */
198 : : void ensureChecked(ProofNode* pn);
199 : : /** Get the underlying proof checker */
200 : : ProofChecker* getChecker() const;
201 : : /**
202 : : * Cancel double SYMM. Returns a proof node that is not a double application
203 : : * of SYMM, e.g. for (SYMM (SYMM (r P))), this returns (r P) where r != SYMM.
204 : : */
205 : : static ProofNode* cancelDoubleSymm(ProofNode* pn);
206 : :
207 : : private:
208 : : /** Reference to the options */
209 : : const Options& d_opts;
210 : : /** The rewriter */
211 : : theory::Rewriter* d_rewriter;
212 : : /** The (optional) proof checker */
213 : : ProofChecker* d_checker;
214 : : /** the true node */
215 : : Node d_true;
216 : : /** Check internal
217 : : *
218 : : * This returns the result of proof checking a ProofNode with the provided
219 : : * arguments with an expected conclusion, which may not null if there is
220 : : * no expected conclusion.
221 : : *
222 : : * This throws an assertion error if we fail to check such a proof node, or
223 : : * if expected is provided (non-null) and is different what is proven by the
224 : : * other arguments.
225 : : *
226 : : * The flag didCheck is set to true if the underlying proof checker was
227 : : * invoked. This may be false if e.g. the proof checking mode is lazy.
228 : : */
229 : : Node checkInternal(ProofRule id,
230 : : const std::vector<std::shared_ptr<ProofNode>>& children,
231 : : const std::vector<Node>& args,
232 : : Node expected,
233 : : bool& didCheck);
234 : : /**
235 : : * Update node internal, return true if successful. This is called by
236 : : * the update node methods above. The argument needsCheck is whether we
237 : : * need to check the correctness of the rule application. This is false
238 : : * for the updateNode routine where pnr is an (already checked) proof node.
239 : : */
240 : : bool updateNodeInternal(
241 : : ProofNode* pn,
242 : : ProofRule id,
243 : : const std::vector<std::shared_ptr<ProofNode>>& children,
244 : : const std::vector<Node>& args,
245 : : bool needsCheck);
246 : : };
247 : :
248 : : } // namespace cvc5::internal
249 : :
250 : : #endif /* CVC5__PROOF__PROOF_NODE_H */
|
