Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Haniel Barbosa, Hans-Joerg Schurr
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 : : * The module for processing proof nodes.
14 : : */
15 : :
16 : : #include <functional>
17 : :
18 : : #include "cvc5_private.h"
19 : :
20 : : #ifndef CVC5__SMT__PROOF_POST_PROCESSOR_H
21 : : #define CVC5__SMT__PROOF_POST_PROCESSOR_H
22 : :
23 : : #include <map>
24 : : #include <sstream>
25 : : #include <unordered_set>
26 : :
27 : : #include "proof/proof_node_updater.h"
28 : : #include "rewriter/rewrites.h"
29 : : #include "smt/env_obj.h"
30 : : #include "smt/proof_post_processor_dsl.h"
31 : : #include "smt/witness_form.h"
32 : : #include "theory/inference_id.h"
33 : : #include "util/statistics_stats.h"
34 : :
35 : : namespace cvc5::internal {
36 : : namespace smt {
37 : :
38 : : /**
39 : : * A callback class used by SolverEngine for post-processing proof nodes by
40 : : * connecting proofs of preprocessing, and expanding macro ProofRule
41 : : * applications.
42 : : */
43 : : class ProofPostprocessCallback : public ProofNodeUpdaterCallback, protected EnvObj
44 : : {
45 : : public:
46 : : ProofPostprocessCallback(Env& env,
47 : : bool updateScopedAssumptions);
48 : 20146 : ~ProofPostprocessCallback() {}
49 : : /**
50 : : * Initialize, called once for each new ProofNode to process. This initializes
51 : : * static information to be used by successive calls to update.
52 : : *
53 : : * @param pppg The proof generator that has proofs of preprocessed assertions
54 : : * (derived from input assertions).
55 : : */
56 : : void initializeUpdate(ProofGenerator* pppg);
57 : : /**
58 : : * Set eliminate rule, which adds rule to the list of rules we will eliminate
59 : : * during update. This adds rule to d_elimRules. Supported rules for
60 : : * elimination include MACRO_*, SUBS and REWRITE. Otherwise, this method
61 : : * has no effect.
62 : : */
63 : : void setEliminateRule(ProofRule rule);
64 : : /**
65 : : * Set collecting all trusted rules. All proofs of trusted rules can be
66 : : * obtained by getTrustedProofs below.
67 : : */
68 : : void setCollectAllTrustedRules();
69 : : /**
70 : : * Get trusted proofs, which is the set of all trusted proofs
71 : : * that were encountered in the last call to process, collected at
72 : : * post-order traversal.
73 : : */
74 : : std::vector<std::shared_ptr<ProofNode>>& getTrustedProofs();
75 : : /** Should proof pn be updated? */
76 : : bool shouldUpdate(std::shared_ptr<ProofNode> pn,
77 : : const std::vector<Node>& fa,
78 : : bool& continueUpdate) override;
79 : : /** Should proof pn be updated? */
80 : : bool shouldUpdatePost(std::shared_ptr<ProofNode> pn,
81 : : const std::vector<Node>& fa) override;
82 : : /** Update the proof rule application. */
83 : : bool update(Node res,
84 : : ProofRule id,
85 : : const std::vector<Node>& children,
86 : : const std::vector<Node>& args,
87 : : CDProof* cdp,
88 : : bool& continueUpdate) override;
89 : : /**
90 : : * Can merge. This returns false if pn is a trusted proof, since we do not
91 : : * want the proof node updater to merge its contents into another proof,
92 : : * which we otherwise would not be informed of and would lead to trusted
93 : : * proofs that are not recorded in d_trustedPfs.
94 : : */
95 : : bool canMerge(std::shared_ptr<ProofNode> pn) override;
96 : :
97 : : private:
98 : : /** Common constants */
99 : : Node d_true;
100 : : /** The proof checker we are using */
101 : : ProofChecker* d_pc;
102 : : /** The preprocessing proof generator */
103 : : ProofGenerator* d_pppg;
104 : : /** The witness form proof generator */
105 : : WitnessFormGenerator d_wfpm;
106 : : /** The witness form assumptions used in the proof */
107 : : std::vector<Node> d_wfAssumptions;
108 : : /** Kinds of proof rules we are eliminating */
109 : : std::unordered_set<ProofRule, std::hash<ProofRule>> d_elimRules;
110 : : /** Whether we are collecting all trusted rules */
111 : : bool d_collectAllTrusted;
112 : : /** Set of all proofs to attempt to reconstruct */
113 : : std::vector<std::shared_ptr<ProofNode>> d_trustedPfs;
114 : : /** Whether we post-process assumptions in scope. */
115 : : bool d_updateScopedAssumptions;
116 : : //---------------------------------reset at the begining of each update
117 : : /** Mapping assumptions to their proof from preprocessing */
118 : : std::map<Node, std::shared_ptr<ProofNode> > d_assumpToProof;
119 : : //---------------------------------end reset at the begining of each update
120 : : /** Return true if id is a proof rule that we should expand */
121 : : bool shouldExpand(ProofRule id) const;
122 : : /**
123 : : * Expand rules in the given application, add the expanded proof to cdp.
124 : : * The set of rules we expand is configured by calls to setEliminateRule
125 : : * above. This method calls update to perform possible post-processing in the
126 : : * rules it introduces as a result of the expansion.
127 : : *
128 : : * @param id The rule of the application
129 : : * @param children The children of the application
130 : : * @param args The arguments of the application
131 : : * @param cdp The proof to add to
132 : : * @return The conclusion of the rule, or null if this rule is not eliminated.
133 : : */
134 : : Node expandMacros(ProofRule id,
135 : : const std::vector<Node>& children,
136 : : const std::vector<Node>& args,
137 : : CDProof* cdp,
138 : : Node res = Node::null());
139 : : /**
140 : : * Update the proof rule application, called during expand macros when
141 : : * we wish to apply the update method. This method has the same behavior
142 : : * as update apart from ignoring the continueUpdate flag.
143 : : */
144 : : bool updateInternal(Node res,
145 : : ProofRule id,
146 : : const std::vector<Node>& children,
147 : : const std::vector<Node>& args,
148 : : CDProof* cdp);
149 : : /**
150 : : * Add proof for witness form. This returns the equality t = toWitness(t)
151 : : * and ensures that the proof of this equality has been added to cdp.
152 : : * Notice the proof of this fact may have open assumptions of the form:
153 : : * k = toWitness(k)
154 : : * where k is a skolem. Furthermore, note that all open assumptions of this
155 : : * form are available via d_wfpm.getWitnessFormEqs() in the remainder of
156 : : * the lifetime of this class.
157 : : */
158 : : Node addProofForWitnessForm(Node t, CDProof* cdp);
159 : : /**
160 : : * Apply transivity if necessary for the arguments. The nodes in
161 : : * tchildren have been ordered such that they are legal arguments to TRANS.
162 : : *
163 : : * Returns the conclusion of the transitivity step, which is null if
164 : : * tchildren is empty. Also note if tchildren contains a single element,
165 : : * then no TRANS step is necessary to add to cdp.
166 : : *
167 : : * @param tchildren The children of a TRANS step
168 : : * @param cdp The proof to add the TRANS step to
169 : : * @return The conclusion of the TRANS step.
170 : : */
171 : : Node addProofForTrans(const std::vector<Node>& tchildren, CDProof* cdp);
172 : : /**
173 : : * Add proof for substitution step. Some substitutions are derived based
174 : : * on viewing a formula as a Boolean assignment (see MethodId::SB_LITERAL for
175 : : * example). This method ensures that the proof of var == subs exists
176 : : * in cdp, where var, subs were derived from BuiltinProofRuleChecker's
177 : : * getSubstitution method.
178 : : *
179 : : * @param var The variable of the substitution
180 : : * @param subs The substituted term
181 : : * @param assump The formula the substitution was derived from
182 : : * @param cdp The proof to add to
183 : : * @return var == subs, the conclusion of the substitution step.
184 : : */
185 : : Node addProofForSubsStep(Node var, Node subs, Node assump, CDProof* cdp);
186 : : /** Add eq (or its symmetry) to transivity children, if not reflexive */
187 : : bool addToTransChildren(Node eq,
188 : : std::vector<Node>& tchildren,
189 : : bool isSymm = false);
190 : :
191 : : };
192 : :
193 : : /**
194 : : * The proof postprocessor module. This postprocesses the final proof
195 : : * produced by an SolverEngine. Its main two tasks are to:
196 : : * (1) Connect proofs of preprocessing,
197 : : * (2) Expand macro ProofRule applications.
198 : : */
199 : : class ProofPostprocess : protected EnvObj
200 : : {
201 : : public:
202 : : /**
203 : : * @param env The environment we are using
204 : : * @param updateScopedAssumptions Whether we post-process assumptions in
205 : : * scope. Since doing so is sound and only problematic depending on who is
206 : : * consuming the proof, it's true by default.
207 : : */
208 : : ProofPostprocess(Env& env,
209 : : rewriter::RewriteDb* rdb,
210 : : bool updateScopedAssumptions = true);
211 : : ~ProofPostprocess();
212 : : /** post-process
213 : : *
214 : : * @param pf The proof to process.
215 : : * @param pppg The proof generator for pre-processing proofs.
216 : : */
217 : : void process(std::shared_ptr<ProofNode> pf, ProofGenerator* pppg);
218 : : /** set eliminate rule */
219 : : void setEliminateRule(ProofRule rule);
220 : : /** set eliminate all trusted rules via DSL */
221 : : void setEliminateAllTrustedRules();
222 : : /**
223 : : * Set assertions, which impacts which proofs can be merged during
224 : : * post-processing. In particular, any proof having only free
225 : : * assumptions in assertions can be used to replace another subproof
226 : : * of the same formula.
227 : : *
228 : : * If doDebug is true, then the assertions are furthermore used to
229 : : * debug whether the final proof is closed.
230 : : */
231 : : void setAssertions(const std::vector<Node>& assertions, bool doDebug);
232 : :
233 : : private:
234 : : /** The post process callback */
235 : : ProofPostprocessCallback d_cb;
236 : : /** The DSL post processor */
237 : : std::unique_ptr<ProofPostprocessDsl> d_ppdsl;
238 : : /**
239 : : * The updater, which is responsible for expanding macros in the final proof
240 : : * and connecting preprocessed assumptions to input assumptions.
241 : : */
242 : : ProofNodeUpdater d_updater;
243 : : };
244 : :
245 : : } // namespace smt
246 : : } // namespace cvc5::internal
247 : :
248 : : #endif
|
