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
|
/******************************************************************************
* Top contributors (to current version):
* Hanna Lachnitt, Haniel Barbosa
*
* This file is part of the cvc5 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.
* ****************************************************************************
*
* The module for processing proof nodes into Alethe proof nodes
*/
#ifndef CVC4__PROOF__ALETHE_PROOF_PROCESSOR_H
#define CVC4__PROOF__ALETHE_PROOF_PROCESSOR_H
#include "proof/proof_node_updater.h"
#include "proof/alethe/alethe_node_converter.h"
#include "proof/alethe/alethe_proof_rule.h"
namespace cvc5 {
namespace proof {
/**
* A callback class used by the Alethe converter for post-processing proof nodes
* by replacing internal rules by the rules in the Alethe calculus.
*/
class AletheProofPostprocessCallback : public ProofNodeUpdaterCallback
{
public:
AletheProofPostprocessCallback(ProofNodeManager* pnm,
AletheNodeConverter& anc);
~AletheProofPostprocessCallback() {}
/** Should proof pn be updated? Only if its top-level proof rule is not an
* Alethe proof rule.
*/
bool shouldUpdate(std::shared_ptr<ProofNode> pn,
const std::vector<Node>& fa,
bool& continueUpdate) override;
/**
* This method updates the proof rule application depending on the given
* rule and translating it into a proof node in terms of the Alethe rules.
*/
bool update(Node res,
PfRule id,
const std::vector<Node>& children,
const std::vector<Node>& args,
CDProof* cdp,
bool& continueUpdate) override;
private:
/** The proof node manager */
ProofNodeManager* d_pnm;
/** The Alethe node converter */
AletheNodeConverter& d_anc;
/** The cl operator
* For every step the conclusion is a clause. But since the or operator
*requires at least two arguments it is extended by the cl operator. In case
*of more than one argument it corresponds to or otherwise it is the identity.
**/
Node d_cl;
/**
* This method adds a new ALETHE_RULE step to the proof, with `rule` as the
* first argument, the original conclusion `res` as the second and
* `conclusion`, the result to be printed (which may or may not differ from
* `res`), as the third.
*
* @param rule The id of the Alethe rule,
* @param res The expected result of the application,
* @param conclusion The conclusion to be printed for the step
* @param children The children of the application,
* @param args The arguments of the application
* @param cdp The proof to add to
* @return True if the step could be added, or false if not.
*/
bool addAletheStep(AletheRule rule,
Node res,
Node conclusion,
const std::vector<Node>& children,
const std::vector<Node>& args,
CDProof& cdp);
/**
* As above, but for proof nodes with original conclusions of the form `(or F1
* ... Fn)` whose conclusion-to-be-printed must be `(cl F1 ... Fn)`.
*
* This method internally calls addAletheStep. The kind of the given Node has
* to be OR.
*
* @param res The expected result of the application in form (or F1 ... Fn),
* @param rule The id of the Alethe rule,
* @param children The children of the application,
* @param args The arguments of the application
* @param cdp The proof to add to
* @return True if the step could be added, or false if not.
*/
bool addAletheStepFromOr(Node res,
AletheRule rule,
const std::vector<Node>& children,
const std::vector<Node>& args,
CDProof& cdp);
};
/**
* Final callback class used by the Alethe converter to add the last step to a
* proof in the following two cases. The last step should always be printed as
* (cl).
*
* 1. If the last step of a proof which is false is reached it is printed as (cl
* false).
* 2. If one of the assumptions is false it is printed as false.
*
* Thus, an additional resolution step with (cl (not true)) has to be added to
* transfer (cl false) into (cl).
*/
class AletheProofPostprocessFinalCallback : public ProofNodeUpdaterCallback
{
public:
AletheProofPostprocessFinalCallback(ProofNodeManager* pnm,
AletheNodeConverter& anc);
~AletheProofPostprocessFinalCallback() {}
/** Should proof pn be updated? It should, if the last step is printed as (cl
* false) or if it is an assumption (in that case it is printed as false).
* Since the proof node should not be traversed, this method will always set
* continueUpdate to false.
*/
bool shouldUpdate(std::shared_ptr<ProofNode> pn,
const std::vector<Node>& fa,
bool& continueUpdate) override;
/**
* This method gets a proof node pn. If the last step of the proof is false
* which is printed as (cl false) it updates the proof for false such that
* (cl) is printed instead.
*/
bool update(Node res,
PfRule id,
const std::vector<Node>& children,
const std::vector<Node>& args,
CDProof* cdp,
bool& continueUpdate) override;
private:
/** The proof node manager */
ProofNodeManager* d_pnm;
/** The Alethe node converter */
AletheNodeConverter& d_anc;
/** The cl operator is defined as described in the
* AletheProofPostprocessCallback class above
**/
Node d_cl;
};
/**
* The proof postprocessor module. This postprocesses a proof node into one
* using the rules from the Alethe calculus.
*/
class AletheProofPostprocess
{
public:
AletheProofPostprocess(ProofNodeManager* pnm, AletheNodeConverter& anc);
~AletheProofPostprocess();
/** post-process */
void process(std::shared_ptr<ProofNode> pf);
private:
/** The proof node manager */
ProofNodeManager* d_pnm;
/** The post process callback */
AletheProofPostprocessCallback d_cb;
/** The final post process callback */
AletheProofPostprocessFinalCallback d_fcb;
};
} // namespace proof
} // namespace cvc5
#endif
|
