Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Hanna Lachnitt, Haniel Barbosa, Andrew Reynolds
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 into Alethe proof nodes
14 : : */
15 : :
16 : : #ifndef CVC5__PROOF__ALETHE__ALETHE_PROOF_PROCESSOR_H
17 : : #define CVC5__PROOF__ALETHE__ALETHE_PROOF_PROCESSOR_H
18 : :
19 : : #include "proof/alethe/alethe_node_converter.h"
20 : : #include "proof/alethe/alethe_proof_rule.h"
21 : : #include "proof/proof_node_updater.h"
22 : :
23 : : namespace cvc5::internal {
24 : :
25 : : namespace proof {
26 : :
27 : : /**
28 : : * A callback class used by the Alethe converter for post-processing proof nodes
29 : : * by replacing internal rules by the rules in the Alethe calculus.
30 : : */
31 : : class AletheProofPostprocessCallback : protected EnvObj,
32 : : public ProofNodeUpdaterCallback
33 : : {
34 : : public:
35 : : /** The callback for post-processing proof nodes into the Alethe format.
36 : : *
37 : : * @param env The environment
38 : : * @param anc The Alethe node converter
39 : : * @param resPivots Whether pivots should be used in resolution
40 : : */
41 : : AletheProofPostprocessCallback(Env& env,
42 : : AletheNodeConverter& anc,
43 : : bool resPivots);
44 : :
45 : 2116 : ~AletheProofPostprocessCallback() {}
46 : :
47 : : /** Should proof pn be updated? Only if its top-level proof rule is not an
48 : : * Alethe proof rule and d_reasonForConversionFailure is not set.
49 : : */
50 : : bool shouldUpdate(std::shared_ptr<ProofNode> pn,
51 : : const std::vector<Node>& fa,
52 : : bool& continueUpdate) override;
53 : : /**
54 : : * This method updates the proof rule application depending on the given
55 : : * rule and translating it into a proof node in terms of the Alethe rules.
56 : : */
57 : : bool update(Node res,
58 : : ProofRule id,
59 : : const std::vector<Node>& children,
60 : : const std::vector<Node>& args,
61 : : CDProof* cdp,
62 : : bool& continueUpdate) override;
63 : : /** Should proof pn be updated at post-visit?
64 : : *
65 : : * Only if its top-level Alethe proof rule is RESOLUTION_OR, REORDERING, or
66 : : * CONTRACTION, which may require updates depending on how the children have
67 : : * changed. And as long as d_reasonForConversionFailure is not set.
68 : : */
69 : : bool shouldUpdatePost(std::shared_ptr<ProofNode> pn,
70 : : const std::vector<Node>& fa) override;
71 : : /**
72 : : * This method is used to add an additional application of the or-rule between
73 : : * a conclusion (cl (or F1 ... Fn)) and a rule that uses this conclusion as a
74 : : * premise and treats it as a clause, i.e. assumes that it has been printed
75 : : * as (cl F1 ... Fn).
76 : : */
77 : : bool updatePost(Node res,
78 : : ProofRule id,
79 : : const std::vector<Node>& children,
80 : : const std::vector<Node>& args,
81 : : CDProof* cdp) override;
82 : :
83 : : /** Ensure the final step of the proof concludes "(cl)".
84 : : *
85 : : * Also sanitizes the arguments of the outer scopes of the proof node.
86 : : */
87 : : bool ensureFinalStep(Node res,
88 : : ProofRule id,
89 : : std::vector<Node>& children,
90 : : const std::vector<Node>& args,
91 : : CDProof* cdp);
92 : :
93 : : /** Retrieve the saved error message, if any. */
94 : : const std::string& getError();
95 : :
96 : : private:
97 : : /** The Alethe node converter */
98 : : AletheNodeConverter& d_anc;
99 : : /** Error message saved during failed conversion. */
100 : : std::string d_reasonForConversionFailure;
101 : :
102 : : /** Whether to keep the pivots in the arguments of the resolution rule. */
103 : : bool d_resPivots;
104 : : /** The cl operator. */
105 : : Node d_cl;
106 : : /** Adds an Alethe step to the CDProof argument
107 : : *
108 : : * The added step to `cdp` uses ProofRule::ALETHE_RULE with `rule` as the
109 : : * first argument, the original conclusion `res` as the second and
110 : : * `conclusion`, the result to be printed (which may or may not differ from
111 : : * `res`), as the third.
112 : : *
113 : : * @param rule The id of the Alethe rule
114 : : * @param res The original conclusion
115 : : * @param conclusion The conclusion to be printed for the step
116 : : * @param children The children of the application
117 : : * @param args The arguments of the application
118 : : * @param cdp The proof to add to
119 : : * @return True if the step could be added, or false if not.
120 : : */
121 : : bool addAletheStep(AletheRule rule,
122 : : Node res,
123 : : Node conclusion,
124 : : const std::vector<Node>& children,
125 : : const std::vector<Node>& args,
126 : : CDProof& cdp);
127 : : /**
128 : : * As above, but `res` must be a node of the form `(or F1 ... Fn)` and the
129 : : * conclusion to be printed will be the clause `(cl F1 ... Fn)`.
130 : : *
131 : : * @param rule The id of the Alethe rule,
132 : : * @param res The original conclusion
133 : : * @param children The children of the application
134 : : * @param args The arguments of the application
135 : : * @param cdp The proof to add to
136 : : * @return True if the step could be added, or false if not.
137 : : */
138 : : bool addAletheStepFromOr(AletheRule rule,
139 : : Node res,
140 : : const std::vector<Node>& children,
141 : : const std::vector<Node>& args,
142 : : CDProof& cdp);
143 : :
144 : : /** Test whether the given resolution premise is being used as a singleton
145 : : * clause but is justified as a non-singleton clause, and fix if needed.
146 : : *
147 : : * This happens with `premise` is a node (or F1 ... Fn) whose proof in `cdp`
148 : : * justifies `(cl (or F1 ... Fn))`, but should justify `(cl F1 ... Fn)`. If
149 : : * that is the case, steps will be added to `cdp` to justify the needed
150 : : * clause.
151 : : */
152 : : bool maybeReplacePremiseProof(Node premise, CDProof* cdp);
153 : : /**
154 : : * This method updates applications of the `THEORY_REWRITE` rule that
155 : : * are explained by a specific `ProofRewriteRule` and translates them
156 : : * into a proof node in terms of the Alethe rules.
157 : : *
158 : : * @param res The original conclusion
159 : : * @param children The children of the application
160 : : * @param args The arguments of the application
161 : : * @param cdp The proof to add to
162 : : * @param di The id of the ProofRewriteRule the THEORY_REWRITE step expresses,
163 : : * @return True if the step could be added, or false if not.
164 : : */
165 : : bool updateTheoryRewriteProofRewriteRule(Node res,
166 : : const std::vector<Node>& children,
167 : : const std::vector<Node>& args,
168 : : CDProof* cdp,
169 : : ProofRewriteRule di);
170 : : /** Nodes corresponding to the Boolean values. */
171 : : Node d_true;
172 : : Node d_false;
173 : : };
174 : :
175 : : /**
176 : : * The proof postprocessor module. This postprocesses a proof node into one
177 : : * using the rules from the Alethe calculus.
178 : : */
179 : : class AletheProofPostprocess : protected EnvObj
180 : : {
181 : : public:
182 : : AletheProofPostprocess(Env& env, AletheNodeConverter& anc);
183 : : ~AletheProofPostprocess();
184 : : /** Convert the proof node into the Alethe proof format
185 : : *
186 : : * If the conversion is possible, true is returned. Otherwise, false. The
187 : : * conversion may fail if the proof contains unsupported elements in the
188 : : * Alethe proof calculus, such as uncategorized Skolems.
189 : : */
190 : : bool process(std::shared_ptr<ProofNode> pf);
191 : :
192 : : /** Retrieve the saved error message, if any. */
193 : : const std::string& getError();
194 : :
195 : : private:
196 : : /** The post process callback */
197 : : AletheProofPostprocessCallback d_cb;
198 : :
199 : : /** The reason for conversion failure, if any. */
200 : : std::string d_reasonForConversionFailure;
201 : : };
202 : :
203 : : } // namespace proof
204 : : } // namespace cvc5::internal
205 : :
206 : : #endif
|
