1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Gereon Kremer |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 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 implementation of the module for proofs for preprocessing in an |
14 |
|
* SMT engine. |
15 |
|
*/ |
16 |
|
|
17 |
|
#include "smt/preprocess_proof_generator.h" |
18 |
|
|
19 |
|
#include <sstream> |
20 |
|
|
21 |
|
#include "expr/proof.h" |
22 |
|
#include "expr/proof_checker.h" |
23 |
|
#include "expr/proof_node.h" |
24 |
|
#include "options/proof_options.h" |
25 |
|
#include "theory/rewriter.h" |
26 |
|
|
27 |
|
namespace cvc5 { |
28 |
|
namespace smt { |
29 |
|
|
30 |
6234 |
PreprocessProofGenerator::PreprocessProofGenerator(ProofNodeManager* pnm, |
31 |
|
context::Context* c, |
32 |
|
std::string name, |
33 |
|
PfRule ra, |
34 |
6234 |
PfRule rpp) |
35 |
|
: d_pnm(pnm), |
36 |
6234 |
d_ctx(c ? c : &d_context), |
37 |
|
d_src(d_ctx), |
38 |
|
d_helperProofs(pnm, d_ctx), |
39 |
|
d_inputPf(pnm, nullptr), |
40 |
|
d_name(name), |
41 |
|
d_ra(ra), |
42 |
12468 |
d_rpp(rpp) |
43 |
|
{ |
44 |
6234 |
} |
45 |
|
|
46 |
34814 |
void PreprocessProofGenerator::notifyInput(Node n) |
47 |
|
{ |
48 |
34814 |
notifyNewAssert(n, &d_inputPf); |
49 |
34814 |
} |
50 |
|
|
51 |
81529 |
void PreprocessProofGenerator::notifyNewAssert(Node n, ProofGenerator* pg) |
52 |
|
{ |
53 |
163058 |
Trace("smt-proof-pp-debug") |
54 |
81529 |
<< "PreprocessProofGenerator::notifyNewAssert: " << n << std::endl; |
55 |
81529 |
if (d_src.find(n) == d_src.end()) |
56 |
|
{ |
57 |
|
// if no proof generator provided for (non-true) assertion |
58 |
78200 |
if (pg == nullptr && (!n.isConst() || !n.getConst<bool>())) |
59 |
|
{ |
60 |
1350 |
checkEagerPedantic(d_ra); |
61 |
|
} |
62 |
78200 |
d_src[n] = theory::TrustNode::mkTrustLemma(n, pg); |
63 |
|
} |
64 |
|
else |
65 |
|
{ |
66 |
3329 |
Trace("smt-proof-pp-debug") << "...already proven" << std::endl; |
67 |
|
} |
68 |
81529 |
} |
69 |
|
|
70 |
28683 |
void PreprocessProofGenerator::notifyNewTrustedAssert(theory::TrustNode tn) |
71 |
|
{ |
72 |
28683 |
notifyNewAssert(tn.getProven(), tn.getGenerator()); |
73 |
28683 |
} |
74 |
|
|
75 |
29309 |
void PreprocessProofGenerator::notifyPreprocessed(Node n, |
76 |
|
Node np, |
77 |
|
ProofGenerator* pg) |
78 |
|
{ |
79 |
|
// only do anything if indeed it rewrote |
80 |
29309 |
if (n == np) |
81 |
|
{ |
82 |
|
return; |
83 |
|
} |
84 |
|
// call the trusted version |
85 |
29309 |
notifyTrustedPreprocessed(theory::TrustNode::mkTrustRewrite(n, np, pg)); |
86 |
|
} |
87 |
|
|
88 |
44695 |
void PreprocessProofGenerator::notifyTrustedPreprocessed(theory::TrustNode tnp) |
89 |
|
{ |
90 |
44695 |
if (tnp.isNull()) |
91 |
|
{ |
92 |
|
// no rewrite, nothing to do |
93 |
|
return; |
94 |
|
} |
95 |
44695 |
Assert(tnp.getKind() == theory::TrustNodeKind::REWRITE); |
96 |
89390 |
Node np = tnp.getNode(); |
97 |
89390 |
Trace("smt-proof-pp-debug") |
98 |
89390 |
<< "PreprocessProofGenerator::notifyPreprocessed: " << tnp.getProven() |
99 |
44695 |
<< std::endl; |
100 |
44695 |
if (d_src.find(np) == d_src.end()) |
101 |
|
{ |
102 |
36742 |
if (tnp.getGenerator() == nullptr) |
103 |
|
{ |
104 |
2168 |
checkEagerPedantic(d_rpp); |
105 |
|
} |
106 |
36742 |
d_src[np] = tnp; |
107 |
|
} |
108 |
|
else |
109 |
|
{ |
110 |
7953 |
Trace("smt-proof-pp-debug") << "...already proven" << std::endl; |
111 |
|
} |
112 |
|
} |
113 |
|
|
114 |
52257 |
std::shared_ptr<ProofNode> PreprocessProofGenerator::getProofFor(Node f) |
115 |
|
{ |
116 |
52257 |
NodeTrustNodeMap::iterator it = d_src.find(f); |
117 |
52257 |
if (it == d_src.end()) |
118 |
|
{ |
119 |
|
// could be an assumption, return nullptr |
120 |
17424 |
return nullptr; |
121 |
|
} |
122 |
|
// make CDProof to construct the proof below |
123 |
69666 |
CDProof cdp(d_pnm); |
124 |
|
|
125 |
69666 |
Trace("smt-pppg") << "PreprocessProofGenerator::getProofFor: (" << d_name |
126 |
34833 |
<< ") input " << f << std::endl; |
127 |
69666 |
Node curr = f; |
128 |
69666 |
std::vector<Node> transChildren; |
129 |
69666 |
std::unordered_set<Node> processed; |
130 |
|
bool success; |
131 |
|
// we connect the proof of f to its source via the map d_src until we |
132 |
|
// discover that its source is a preprocessing lemma (a lemma stored in d_src) |
133 |
|
// or otherwise it is assumed to be an input assumption. |
134 |
45825 |
do |
135 |
|
{ |
136 |
45825 |
success = false; |
137 |
45825 |
if (it != d_src.end()) |
138 |
|
{ |
139 |
45825 |
Assert((*it).second.getNode() == curr); |
140 |
|
// get the proven node |
141 |
91650 |
Node proven = (*it).second.getProven(); |
142 |
45825 |
Assert(!proven.isNull()); |
143 |
45825 |
Trace("smt-pppg") << "...process proven " << proven << std::endl; |
144 |
45825 |
if (processed.find(proven) != processed.end()) |
145 |
|
{ |
146 |
|
Unhandled() << "Cyclic steps in preprocess proof generator"; |
147 |
|
continue; |
148 |
|
} |
149 |
45825 |
processed.insert(proven); |
150 |
45825 |
bool proofStepProcessed = false; |
151 |
|
|
152 |
|
// if a generator for the step was provided, it is stored in the proof |
153 |
45825 |
Trace("smt-pppg") << "...get provided proof" << std::endl; |
154 |
91650 |
std::shared_ptr<ProofNode> pfr = (*it).second.toProofNode(); |
155 |
45825 |
if (pfr != nullptr) |
156 |
|
{ |
157 |
45086 |
Trace("smt-pppg") << "...add provided" << std::endl; |
158 |
45086 |
Assert(pfr->getResult() == proven); |
159 |
45086 |
cdp.addProof(pfr); |
160 |
45086 |
proofStepProcessed = true; |
161 |
|
} |
162 |
|
|
163 |
45825 |
Trace("smt-pppg") << "...update" << std::endl; |
164 |
45825 |
theory::TrustNodeKind tnk = (*it).second.getKind(); |
165 |
45825 |
if (tnk == theory::TrustNodeKind::REWRITE) |
166 |
|
{ |
167 |
10992 |
Trace("smt-pppg") << "...rewritten from " << proven[0] << std::endl; |
168 |
10992 |
Assert(proven.getKind() == kind::EQUAL); |
169 |
10992 |
if (!proofStepProcessed) |
170 |
|
{ |
171 |
|
// maybe its just a simple rewrite? |
172 |
659 |
if (proven[1] == theory::Rewriter::rewrite(proven[0])) |
173 |
|
{ |
174 |
10 |
cdp.addStep(proven, PfRule::REWRITE, {}, {proven[0]}); |
175 |
10 |
proofStepProcessed = true; |
176 |
|
} |
177 |
|
} |
178 |
10992 |
transChildren.push_back(proven); |
179 |
|
// continue with source |
180 |
10992 |
curr = proven[0]; |
181 |
10992 |
success = true; |
182 |
|
// find the next node |
183 |
10992 |
it = d_src.find(curr); |
184 |
|
} |
185 |
|
else |
186 |
|
{ |
187 |
34833 |
Trace("smt-pppg") << "...lemma" << std::endl; |
188 |
34833 |
Assert(tnk == theory::TrustNodeKind::LEMMA); |
189 |
|
} |
190 |
|
|
191 |
45825 |
if (!proofStepProcessed) |
192 |
|
{ |
193 |
729 |
Trace("smt-pppg") << "...add missing step" << std::endl; |
194 |
|
// add trusted step, the rule depends on the kind of trust node |
195 |
1458 |
cdp.addStep(proven, |
196 |
|
tnk == theory::TrustNodeKind::LEMMA ? d_ra : d_rpp, |
197 |
|
{}, |
198 |
729 |
{proven}); |
199 |
|
} |
200 |
|
} |
201 |
|
} while (success); |
202 |
|
|
203 |
|
// prove ( curr == f ), which is not necessary if they are the same |
204 |
|
// modulo symmetry. |
205 |
34833 |
if (!CDProof::isSame(f, curr)) |
206 |
|
{ |
207 |
18696 |
Node fullRewrite = curr.eqNode(f); |
208 |
9348 |
if (transChildren.size() >= 2) |
209 |
|
{ |
210 |
988 |
Trace("smt-pppg") << "...apply trans to get " << fullRewrite << std::endl; |
211 |
988 |
std::reverse(transChildren.begin(), transChildren.end()); |
212 |
988 |
cdp.addStep(fullRewrite, PfRule::TRANS, transChildren, {}); |
213 |
|
} |
214 |
9348 |
Trace("smt-pppg") << "...eq_resolve to prove" << std::endl; |
215 |
|
// prove f |
216 |
9348 |
cdp.addStep(f, PfRule::EQ_RESOLVE, {curr, fullRewrite}, {}); |
217 |
9348 |
Trace("smt-pppg") << "...finished" << std::endl; |
218 |
|
} |
219 |
|
|
220 |
|
// overall, proof is: |
221 |
|
// --------- from proof generator ---------- from proof generator |
222 |
|
// F_1 = F_2 ... F_{n-1} = F_n |
223 |
|
// ---? -------------------------------------------------- TRANS |
224 |
|
// F_1 F_1 = F_n |
225 |
|
// ---------------- EQ_RESOLVE |
226 |
|
// F_n |
227 |
|
// Note F_1 may have been given a proof if it was not an input assumption. |
228 |
|
|
229 |
34833 |
return cdp.getProofFor(f); |
230 |
|
} |
231 |
|
|
232 |
3117 |
ProofNodeManager* PreprocessProofGenerator::getManager() { return d_pnm; } |
233 |
|
|
234 |
409 |
LazyCDProof* PreprocessProofGenerator::allocateHelperProof() |
235 |
|
{ |
236 |
409 |
return d_helperProofs.allocateProof(nullptr, d_ctx); |
237 |
|
} |
238 |
|
|
239 |
44186 |
std::string PreprocessProofGenerator::identify() const { return d_name; } |
240 |
|
|
241 |
3518 |
void PreprocessProofGenerator::checkEagerPedantic(PfRule r) |
242 |
|
{ |
243 |
3518 |
if (options::proofEagerChecking()) |
244 |
|
{ |
245 |
|
// catch a pedantic failure now, which otherwise would not be |
246 |
|
// triggered since we are doing lazy proof generation |
247 |
|
ProofChecker* pc = d_pnm->getChecker(); |
248 |
|
std::stringstream serr; |
249 |
|
if (pc->isPedanticFailure(r, serr)) |
250 |
|
{ |
251 |
|
Unhandled() << "PreprocessProofGenerator::checkEagerPedantic: " |
252 |
|
<< serr.str(); |
253 |
|
} |
254 |
|
} |
255 |
3518 |
} |
256 |
|
|
257 |
|
} // namespace smt |
258 |
27735 |
} // namespace cvc5 |