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 : 18845 : ~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 : : /** Should proof pn be updated? */
65 : : bool shouldUpdate(std::shared_ptr<ProofNode> pn,
66 : : const std::vector<Node>& fa,
67 : : bool& continueUpdate) override;
68 : : /** Should proof pn be updated? */
69 : : bool shouldUpdatePost(std::shared_ptr<ProofNode> pn,
70 : : const std::vector<Node>& fa) override;
71 : : /** Update the proof rule application. */
72 : : bool update(Node res,
73 : : ProofRule id,
74 : : const std::vector<Node>& children,
75 : : const std::vector<Node>& args,
76 : : CDProof* cdp,
77 : : bool& continueUpdate) override;
78 : :
79 : : private:
80 : : /** Common constants */
81 : : Node d_true;
82 : : /** The proof checker we are using */
83 : : ProofChecker* d_pc;
84 : : /** The preprocessing proof generator */
85 : : ProofGenerator* d_pppg;
86 : : /** The witness form proof generator */
87 : : WitnessFormGenerator d_wfpm;
88 : : /** The witness form assumptions used in the proof */
89 : : std::vector<Node> d_wfAssumptions;
90 : : /** Kinds of proof rules we are eliminating */
91 : : std::unordered_set<ProofRule, std::hash<ProofRule>> d_elimRules;
92 : : /**
93 : : * Counts number of proof nodes for each rule that were
94 : : * expanded in macro elimination by this class.
95 : : */
96 : : HistogramStat<ProofRule> d_macroExpand;
97 : : /** Whether we post-process assumptions in scope. */
98 : : bool d_updateScopedAssumptions;
99 : : //---------------------------------reset at the begining of each update
100 : : /** Mapping assumptions to their proof from preprocessing */
101 : : std::map<Node, std::shared_ptr<ProofNode> > d_assumpToProof;
102 : : //---------------------------------end reset at the begining of each update
103 : : /** Return true if id is a proof rule that we should expand */
104 : : bool shouldExpand(ProofRule id) const;
105 : : /**
106 : : * Expand rules in the given application, add the expanded proof to cdp.
107 : : * The set of rules we expand is configured by calls to setEliminateRule
108 : : * above. This method calls update to perform possible post-processing in the
109 : : * rules it introduces as a result of the expansion.
110 : : *
111 : : * @param id The rule of the application
112 : : * @param children The children of the application
113 : : * @param args The arguments of the application
114 : : * @param cdp The proof to add to
115 : : * @return The conclusion of the rule, or null if this rule is not eliminated.
116 : : */
117 : : Node expandMacros(ProofRule id,
118 : : const std::vector<Node>& children,
119 : : const std::vector<Node>& args,
120 : : CDProof* cdp,
121 : : Node res = Node::null());
122 : : /**
123 : : * Called when we require expanding a macro step from within the method above.
124 : : * This makes a recursive call to the above method.
125 : : * @param id The rule of the application
126 : : * @param children The children of the application
127 : : * @param args The arguments of the application
128 : : * @param cdp The proof to add to
129 : : * @return The conclusion of the rule, or null if this rule is not eliminated.
130 : : */
131 : : Node addExpandStep(ProofRule id,
132 : : const std::vector<Node>& children,
133 : : const std::vector<Node>& args,
134 : : CDProof* cdp);
135 : : /**
136 : : * Update the proof rule application, called during expand macros when
137 : : * we wish to apply the update method. This method has the same behavior
138 : : * as update apart from ignoring the continueUpdate flag.
139 : : */
140 : : bool updateInternal(Node res,
141 : : ProofRule id,
142 : : const std::vector<Node>& children,
143 : : const std::vector<Node>& args,
144 : : CDProof* cdp);
145 : : /**
146 : : * Add proof for witness form. This returns the equality t = toWitness(t)
147 : : * and ensures that the proof of this equality has been added to cdp.
148 : : * Notice the proof of this fact may have open assumptions of the form:
149 : : * k = toWitness(k)
150 : : * where k is a skolem. Furthermore, note that all open assumptions of this
151 : : * form are available via d_wfpm.getWitnessFormEqs() in the remainder of
152 : : * the lifetime of this class.
153 : : */
154 : : Node addProofForWitnessForm(Node t, CDProof* cdp);
155 : : /**
156 : : * Apply transivity if necessary for the arguments. The nodes in
157 : : * tchildren have been ordered such that they are legal arguments to TRANS.
158 : : *
159 : : * Returns the conclusion of the transitivity step, which is null if
160 : : * tchildren is empty. Also note if tchildren contains a single element,
161 : : * then no TRANS step is necessary to add to cdp.
162 : : *
163 : : * @param tchildren The children of a TRANS step
164 : : * @param cdp The proof to add the TRANS step to
165 : : * @return The conclusion of the TRANS step.
166 : : */
167 : : Node addProofForTrans(const std::vector<Node>& tchildren, CDProof* cdp);
168 : : /**
169 : : * Add proof for substitution step. Some substitutions are derived based
170 : : * on viewing a formula as a Boolean assignment (see MethodId::SB_LITERAL for
171 : : * example). This method ensures that the proof of var == subs exists
172 : : * in cdp, where var, subs were derived from BuiltinProofRuleChecker's
173 : : * getSubstitution method.
174 : : *
175 : : * @param var The variable of the substitution
176 : : * @param subs The substituted term
177 : : * @param assump The formula the substitution was derived from
178 : : * @param cdp The proof to add to
179 : : * @return var == subs, the conclusion of the substitution step.
180 : : */
181 : : Node addProofForSubsStep(Node var, Node subs, Node assump, CDProof* cdp);
182 : : /** Add eq (or its symmetry) to transivity children, if not reflexive */
183 : : bool addToTransChildren(Node eq,
184 : : std::vector<Node>& tchildren,
185 : : bool isSymm = false);
186 : :
187 : : };
188 : :
189 : : /**
190 : : * The proof postprocessor module. This postprocesses the final proof
191 : : * produced by an SolverEngine. Its main two tasks are to:
192 : : * (1) Connect proofs of preprocessing,
193 : : * (2) Expand macro ProofRule applications.
194 : : */
195 : : class ProofPostprocess : protected EnvObj
196 : : {
197 : : public:
198 : : /**
199 : : * @param env The environment we are using
200 : : * @param updateScopedAssumptions Whether we post-process assumptions in
201 : : * scope. Since doing so is sound and only problematic depending on who is
202 : : * consuming the proof, it's true by default.
203 : : */
204 : : ProofPostprocess(Env& env,
205 : : rewriter::RewriteDb* rdb,
206 : : bool updateScopedAssumptions = true);
207 : : ~ProofPostprocess();
208 : : /** post-process
209 : : *
210 : : * @param pf The proof to process.
211 : : * @param pppg The proof generator for pre-processing proofs.
212 : : */
213 : : void process(std::shared_ptr<ProofNode> pf, ProofGenerator* pppg);
214 : : /** set eliminate rule */
215 : : void setEliminateRule(ProofRule rule);
216 : : /** set eliminate all trusted rules via DSL */
217 : : void setEliminateAllTrustedRules();
218 : : /**
219 : : * Set assertions, which impacts which proofs can be merged during
220 : : * post-processing. In particular, any proof having only free
221 : : * assumptions in assertions can be used to replace another subproof
222 : : * of the same formula.
223 : : *
224 : : * If doDebug is true, then the assertions are furthermore used to
225 : : * debug whether the final proof is closed.
226 : : */
227 : : void setAssertions(const std::vector<Node>& assertions, bool doDebug);
228 : :
229 : : private:
230 : : /** The post process callback */
231 : : ProofPostprocessCallback d_cb;
232 : : /** The DSL post processor */
233 : : std::unique_ptr<ProofPostprocessDsl> d_ppdsl;
234 : : /** Eliminate trusted rules? */
235 : : bool d_elimTrustedRules;
236 : : /**
237 : : * The updater, which is responsible for expanding macros in the final proof
238 : : * and connecting preprocessed assumptions to input assumptions.
239 : : */
240 : : ProofNodeUpdater d_updater;
241 : : };
242 : :
243 : : } // namespace smt
244 : : } // namespace cvc5::internal
245 : :
246 : : #endif
|
