1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Hanna Lachnitt, Haniel Barbosa |
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 module for processing proof nodes into Alethe proof nodes |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "proof/alethe/alethe_post_processor.h" |
17 |
|
|
18 |
|
#include "expr/node_algorithm.h" |
19 |
|
#include "proof/proof.h" |
20 |
|
#include "proof/proof_checker.h" |
21 |
|
#include "util/rational.h" |
22 |
|
#include "theory/builtin/proof_checker.h" |
23 |
|
|
24 |
|
namespace cvc5 { |
25 |
|
|
26 |
|
namespace proof { |
27 |
|
|
28 |
|
AletheProofPostprocessCallback::AletheProofPostprocessCallback( |
29 |
|
ProofNodeManager* pnm, AletheNodeConverter& anc) |
30 |
|
: d_pnm(pnm), d_anc(anc) |
31 |
|
{ |
32 |
|
NodeManager* nm = NodeManager::currentNM(); |
33 |
|
d_cl = nm->mkBoundVar("cl", nm->sExprType()); |
34 |
|
} |
35 |
|
|
36 |
|
bool AletheProofPostprocessCallback::shouldUpdate(std::shared_ptr<ProofNode> pn, |
37 |
|
const std::vector<Node>& fa, |
38 |
|
bool& continueUpdate) |
39 |
|
{ |
40 |
|
return pn->getRule() != PfRule::ALETHE_RULE; |
41 |
|
} |
42 |
|
|
43 |
|
bool AletheProofPostprocessCallback::update(Node res, |
44 |
|
PfRule id, |
45 |
|
const std::vector<Node>& children, |
46 |
|
const std::vector<Node>& args, |
47 |
|
CDProof* cdp, |
48 |
|
bool& continueUpdate) |
49 |
|
{ |
50 |
|
Trace("alethe-proof") << "- Alethe post process callback " << res << " " << id |
51 |
|
<< " " << children << " / " << args << std::endl; |
52 |
|
|
53 |
|
NodeManager* nm = NodeManager::currentNM(); |
54 |
|
std::vector<Node> new_args = std::vector<Node>(); |
55 |
|
|
56 |
|
switch (id) |
57 |
|
{ |
58 |
|
//================================================= Core rules |
59 |
|
//======================== Assume and Scope |
60 |
|
case PfRule::ASSUME: |
61 |
|
{ |
62 |
|
return addAletheStep(AletheRule::ASSUME, res, res, children, {}, *cdp); |
63 |
|
} |
64 |
|
// See proof_rule.h for documentation on the SCOPE rule. This comment uses |
65 |
|
// variable names as introduced there. Since the SCOPE rule originally |
66 |
|
// concludes |
67 |
|
// (=> (and F1 ... Fn) F) or (not (and F1 ... Fn)) but the ANCHOR rule |
68 |
|
// concludes (cl (not F1) ... (not Fn) F), to keep the original shape of the |
69 |
|
// proof node it is necessary to rederive the original conclusion. The |
70 |
|
// transformation is described below, depending on the form of SCOPE's |
71 |
|
// conclusion. |
72 |
|
// |
73 |
|
// Note that after the original conclusion is rederived the new proof node |
74 |
|
// will actually have to be printed, respectively, (cl (=> (and F1 ... Fn) |
75 |
|
// F)) or (cl (not (and F1 ... Fn))). |
76 |
|
// |
77 |
|
// Let (not (and F1 ... Fn))^i denote the repetition of (not (and F1 ... |
78 |
|
// Fn)) for i times. |
79 |
|
// |
80 |
|
// T1: |
81 |
|
// |
82 |
|
// P |
83 |
|
// ----- ANCHOR ------- ... ------- AND_POS |
84 |
|
// VP1 VP2_1 ... VP2_n |
85 |
|
// ------------------------------------ RESOLUTION |
86 |
|
// VP2a |
87 |
|
// ------------------------------------ REORDER |
88 |
|
// VP2b |
89 |
|
// ------ DUPLICATED_LITERALS ------- IMPLIES_NEG1 |
90 |
|
// VP3 VP4 |
91 |
|
// ------------------------------------ RESOLUTION ------- IMPLIES_NEG2 |
92 |
|
// VP5 VP6 |
93 |
|
// ----------------------------------------------------------- RESOLUTION |
94 |
|
// VP7 |
95 |
|
// |
96 |
|
// VP1: (cl (not F1) ... (not Fn) F) |
97 |
|
// VP2_i: (cl (not (and F1 ... Fn)) Fi), for i = 1 to n |
98 |
|
// VP2a: (cl F (not (and F1 ... Fn))^n) |
99 |
|
// VP2b: (cl (not (and F1 ... Fn))^n F) |
100 |
|
// VP3: (cl (not (and F1 ... Fn)) F) |
101 |
|
// VP4: (cl (=> (and F1 ... Fn) F) (and F1 ... Fn))) |
102 |
|
// VP5: (cl (=> (and F1 ... Fn) F) F) |
103 |
|
// VP6: (cl (=> (and F1 ... Fn) F) (not F)) |
104 |
|
// VP7: (cl (=> (and F1 ... Fn) F) (=> (and F1 ... Fn) F)) |
105 |
|
// |
106 |
|
// Note that if n = 1, then the ANCHOR step yields (cl (not F1) F), which is |
107 |
|
// the same as VP3. Since VP1 = VP3, the steps for that transformation are |
108 |
|
// not generated. |
109 |
|
// |
110 |
|
// |
111 |
|
// If F = false: |
112 |
|
// |
113 |
|
// --------- IMPLIES_SIMPLIFY |
114 |
|
// T1 VP9 |
115 |
|
// --------- DUPLICATED_LITERALS --------- EQUIV_1 |
116 |
|
// VP8 VP10 |
117 |
|
// -------------------------------------------- RESOLUTION |
118 |
|
// (cl (not (and F1 ... Fn)))* |
119 |
|
// |
120 |
|
// VP8: (cl (=> (and F1 ... Fn))) (cl (not (=> (and F1 ... Fn) false)) |
121 |
|
// (not (and F1 ... Fn))) |
122 |
|
// VP9: (cl (= (=> (and F1 ... Fn) false) (not (and F1 ... Fn)))) |
123 |
|
// |
124 |
|
// |
125 |
|
// Otherwise, |
126 |
|
// T1 |
127 |
|
// ------------------------------ DUPLICATED_LITERALS |
128 |
|
// (cl (=> (and F1 ... Fn) F))** |
129 |
|
// |
130 |
|
// |
131 |
|
// * the corresponding proof node is (not (and F1 ... Fn)) |
132 |
|
// ** the corresponding proof node is (=> (and F1 ... Fn) F) |
133 |
|
case PfRule::SCOPE: |
134 |
|
{ |
135 |
|
bool success = true; |
136 |
|
|
137 |
|
// Build vp1 |
138 |
|
std::vector<Node> negNode{d_cl}; |
139 |
|
std::vector<Node> sanitized_args; |
140 |
|
for (Node arg : args) |
141 |
|
{ |
142 |
|
negNode.push_back(arg.notNode()); // (not F1) ... (not Fn) |
143 |
|
sanitized_args.push_back(d_anc.convert(arg)); |
144 |
|
} |
145 |
|
negNode.push_back(children[0]); // (cl (not F1) ... (not Fn) F) |
146 |
|
Node vp1 = nm->mkNode(kind::SEXPR, negNode); |
147 |
|
success &= addAletheStep(AletheRule::ANCHOR_SUBPROOF, |
148 |
|
vp1, |
149 |
|
vp1, |
150 |
|
children, |
151 |
|
sanitized_args, |
152 |
|
*cdp); |
153 |
|
Node andNode, vp3; |
154 |
|
if (args.size() == 1) |
155 |
|
{ |
156 |
|
vp3 = vp1; |
157 |
|
andNode = args[0]; // F1 |
158 |
|
} |
159 |
|
else |
160 |
|
{ |
161 |
|
// Build vp2i |
162 |
|
andNode = nm->mkNode(kind::AND, args); // (and F1 ... Fn) |
163 |
|
std::vector<Node> premisesVP2 = {vp1}; |
164 |
|
std::vector<Node> notAnd = {d_cl, children[0]}; // cl F |
165 |
|
Node vp2_i; |
166 |
|
for (size_t i = 0, size = args.size(); i < size; i++) |
167 |
|
{ |
168 |
|
vp2_i = nm->mkNode(kind::SEXPR, d_cl, andNode.notNode(), args[i]); |
169 |
|
success &= |
170 |
|
addAletheStep(AletheRule::AND_POS, vp2_i, vp2_i, {}, {}, *cdp); |
171 |
|
premisesVP2.push_back(vp2_i); |
172 |
|
notAnd.push_back(andNode.notNode()); // cl F (not (and F1 ... Fn))^i |
173 |
|
} |
174 |
|
|
175 |
|
Node vp2a = nm->mkNode(kind::SEXPR, notAnd); |
176 |
|
success &= addAletheStep( |
177 |
|
AletheRule::RESOLUTION, vp2a, vp2a, premisesVP2, {}, *cdp); |
178 |
|
|
179 |
|
notAnd.erase(notAnd.begin() + 1); //(cl (not (and F1 ... Fn))^n) |
180 |
|
notAnd.push_back(children[0]); //(cl (not (and F1 ... Fn))^n F) |
181 |
|
Node vp2b = nm->mkNode(kind::SEXPR, notAnd); |
182 |
|
success &= |
183 |
|
addAletheStep(AletheRule::REORDER, vp2b, vp2b, {vp2a}, {}, *cdp); |
184 |
|
|
185 |
|
vp3 = nm->mkNode(kind::SEXPR, d_cl, andNode.notNode(), children[0]); |
186 |
|
success &= addAletheStep( |
187 |
|
AletheRule::DUPLICATED_LITERALS, vp3, vp3, {vp2b}, {}, *cdp); |
188 |
|
} |
189 |
|
|
190 |
|
Node vp8 = nm->mkNode( |
191 |
|
kind::SEXPR, d_cl, nm->mkNode(kind::IMPLIES, andNode, children[0])); |
192 |
|
|
193 |
|
Node vp4 = nm->mkNode(kind::SEXPR, d_cl, vp8[1], andNode); |
194 |
|
success &= |
195 |
|
addAletheStep(AletheRule::IMPLIES_NEG1, vp4, vp4, {}, {}, *cdp); |
196 |
|
|
197 |
|
Node vp5 = nm->mkNode(kind::SEXPR, d_cl, vp8[1], children[0]); |
198 |
|
success &= |
199 |
|
addAletheStep(AletheRule::RESOLUTION, vp5, vp5, {vp4, vp3}, {}, *cdp); |
200 |
|
|
201 |
|
Node vp6 = nm->mkNode(kind::SEXPR, d_cl, vp8[1], children[0].notNode()); |
202 |
|
success &= |
203 |
|
addAletheStep(AletheRule::IMPLIES_NEG2, vp6, vp6, {}, {}, *cdp); |
204 |
|
|
205 |
|
Node vp7 = nm->mkNode(kind::SEXPR, d_cl, vp8[1], vp8[1]); |
206 |
|
success &= |
207 |
|
addAletheStep(AletheRule::RESOLUTION, vp7, vp7, {vp5, vp6}, {}, *cdp); |
208 |
|
|
209 |
|
if (children[0] != nm->mkConst(false)) |
210 |
|
{ |
211 |
|
success &= addAletheStep( |
212 |
|
AletheRule::DUPLICATED_LITERALS, res, vp8, {vp7}, {}, *cdp); |
213 |
|
} |
214 |
|
else |
215 |
|
{ |
216 |
|
success &= addAletheStep( |
217 |
|
AletheRule::DUPLICATED_LITERALS, vp8, vp8, {vp7}, {}, *cdp); |
218 |
|
|
219 |
|
Node vp9 = |
220 |
|
nm->mkNode(kind::SEXPR, |
221 |
|
d_cl, |
222 |
|
nm->mkNode(kind::EQUAL, vp8[1], andNode.notNode())); |
223 |
|
|
224 |
|
success &= |
225 |
|
addAletheStep(AletheRule::IMPLIES_SIMPLIFY, vp9, vp9, {}, {}, *cdp); |
226 |
|
|
227 |
|
Node vp10 = |
228 |
|
nm->mkNode(kind::SEXPR, d_cl, vp8[1].notNode(), andNode.notNode()); |
229 |
|
success &= |
230 |
|
addAletheStep(AletheRule::EQUIV1, vp10, vp10, {vp9}, {}, *cdp); |
231 |
|
|
232 |
|
success &= addAletheStep(AletheRule::RESOLUTION, |
233 |
|
res, |
234 |
|
nm->mkNode(kind::SEXPR, d_cl, res), |
235 |
|
{vp8, vp10}, |
236 |
|
{}, |
237 |
|
*cdp); |
238 |
|
} |
239 |
|
|
240 |
|
return success; |
241 |
|
} |
242 |
|
// The rule is translated according to the theory id tid and the outermost |
243 |
|
// connective of the first term in the conclusion F, since F always has the |
244 |
|
// form (= t1 t2) where t1 is the term being rewritten. This is not an exact |
245 |
|
// translation but should work in most cases. |
246 |
|
// |
247 |
|
// E.g. if F is (= (* 0 d) 0) and tid = THEORY_ARITH, then prod_simplify |
248 |
|
// is correctly guessed as the rule. |
249 |
|
case PfRule::THEORY_REWRITE: |
250 |
|
{ |
251 |
|
AletheRule vrule = AletheRule::UNDEFINED; |
252 |
|
Node t = res[0]; |
253 |
|
|
254 |
|
theory::TheoryId tid; |
255 |
|
if (!theory::builtin::BuiltinProofRuleChecker::getTheoryId(args[1], tid)) |
256 |
|
{ |
257 |
|
return addAletheStep( |
258 |
|
vrule, res, nm->mkNode(kind::SEXPR, d_cl, res), children, {}, *cdp); |
259 |
|
} |
260 |
|
switch (tid) |
261 |
|
{ |
262 |
|
case theory::TheoryId::THEORY_BUILTIN: |
263 |
|
{ |
264 |
|
switch (t.getKind()) |
265 |
|
{ |
266 |
|
case kind::ITE: |
267 |
|
{ |
268 |
|
vrule = AletheRule::ITE_SIMPLIFY; |
269 |
|
break; |
270 |
|
} |
271 |
|
case kind::EQUAL: |
272 |
|
{ |
273 |
|
vrule = AletheRule::EQ_SIMPLIFY; |
274 |
|
break; |
275 |
|
} |
276 |
|
case kind::AND: |
277 |
|
{ |
278 |
|
vrule = AletheRule::AND_SIMPLIFY; |
279 |
|
break; |
280 |
|
} |
281 |
|
case kind::OR: |
282 |
|
{ |
283 |
|
vrule = AletheRule::OR_SIMPLIFY; |
284 |
|
break; |
285 |
|
} |
286 |
|
case kind::NOT: |
287 |
|
{ |
288 |
|
vrule = AletheRule::NOT_SIMPLIFY; |
289 |
|
break; |
290 |
|
} |
291 |
|
case kind::IMPLIES: |
292 |
|
{ |
293 |
|
vrule = AletheRule::IMPLIES_SIMPLIFY; |
294 |
|
break; |
295 |
|
} |
296 |
|
case kind::WITNESS: |
297 |
|
{ |
298 |
|
vrule = AletheRule::QNT_SIMPLIFY; |
299 |
|
break; |
300 |
|
} |
301 |
|
default: |
302 |
|
{ |
303 |
|
// In this case the rule is undefined |
304 |
|
} |
305 |
|
} |
306 |
|
break; |
307 |
|
} |
308 |
|
case theory::TheoryId::THEORY_BOOL: |
309 |
|
{ |
310 |
|
vrule = AletheRule::BOOL_SIMPLIFY; |
311 |
|
break; |
312 |
|
} |
313 |
|
case theory::TheoryId::THEORY_UF: |
314 |
|
{ |
315 |
|
if (t.getKind() == kind::EQUAL) |
316 |
|
{ |
317 |
|
// A lot of these seem to be symmetry rules but not all... |
318 |
|
vrule = AletheRule::EQUIV_SIMPLIFY; |
319 |
|
} |
320 |
|
break; |
321 |
|
} |
322 |
|
case theory::TheoryId::THEORY_ARITH: |
323 |
|
{ |
324 |
|
switch (t.getKind()) |
325 |
|
{ |
326 |
|
case kind::DIVISION: |
327 |
|
{ |
328 |
|
vrule = AletheRule::DIV_SIMPLIFY; |
329 |
|
break; |
330 |
|
} |
331 |
|
case kind::PRODUCT: |
332 |
|
{ |
333 |
|
vrule = AletheRule::PROD_SIMPLIFY; |
334 |
|
break; |
335 |
|
} |
336 |
|
case kind::MINUS: |
337 |
|
{ |
338 |
|
vrule = AletheRule::MINUS_SIMPLIFY; |
339 |
|
break; |
340 |
|
} |
341 |
|
case kind::UMINUS: |
342 |
|
{ |
343 |
|
vrule = AletheRule::UNARY_MINUS_SIMPLIFY; |
344 |
|
break; |
345 |
|
} |
346 |
|
case kind::PLUS: |
347 |
|
{ |
348 |
|
vrule = AletheRule::SUM_SIMPLIFY; |
349 |
|
break; |
350 |
|
} |
351 |
|
case kind::MULT: |
352 |
|
{ |
353 |
|
vrule = AletheRule::PROD_SIMPLIFY; |
354 |
|
break; |
355 |
|
} |
356 |
|
case kind::EQUAL: |
357 |
|
{ |
358 |
|
vrule = AletheRule::EQUIV_SIMPLIFY; |
359 |
|
break; |
360 |
|
} |
361 |
|
case kind::LT: |
362 |
|
{ |
363 |
|
[[fallthrough]]; |
364 |
|
} |
365 |
|
case kind::GT: |
366 |
|
{ |
367 |
|
[[fallthrough]]; |
368 |
|
} |
369 |
|
case kind::GEQ: |
370 |
|
{ |
371 |
|
[[fallthrough]]; |
372 |
|
} |
373 |
|
case kind::LEQ: |
374 |
|
{ |
375 |
|
vrule = AletheRule::COMP_SIMPLIFY; |
376 |
|
break; |
377 |
|
} |
378 |
|
case kind::CAST_TO_REAL: |
379 |
|
{ |
380 |
|
return addAletheStep(AletheRule::LA_GENERIC, |
381 |
|
res, |
382 |
|
nm->mkNode(kind::SEXPR, d_cl, res), |
383 |
|
children, |
384 |
|
{nm->mkConst(Rational(1))}, |
385 |
|
*cdp); |
386 |
|
} |
387 |
|
default: |
388 |
|
{ |
389 |
|
// In this case the rule is undefined |
390 |
|
} |
391 |
|
} |
392 |
|
break; |
393 |
|
} |
394 |
|
case theory::TheoryId::THEORY_QUANTIFIERS: |
395 |
|
{ |
396 |
|
vrule = AletheRule::QUANTIFIER_SIMPLIFY; |
397 |
|
break; |
398 |
|
} |
399 |
|
default: |
400 |
|
{ |
401 |
|
// In this case the rule is undefined |
402 |
|
}; |
403 |
|
} |
404 |
|
return addAletheStep( |
405 |
|
vrule, res, nm->mkNode(kind::SEXPR, d_cl, res), children, {}, *cdp); |
406 |
|
} |
407 |
|
default: |
408 |
|
{ |
409 |
|
return addAletheStep(AletheRule::UNDEFINED, |
410 |
|
res, |
411 |
|
nm->mkNode(kind::SEXPR, d_cl, res), |
412 |
|
children, |
413 |
|
args, |
414 |
|
*cdp); |
415 |
|
} |
416 |
|
} |
417 |
|
} |
418 |
|
|
419 |
|
bool AletheProofPostprocessCallback::addAletheStep( |
420 |
|
AletheRule rule, |
421 |
|
Node res, |
422 |
|
Node conclusion, |
423 |
|
const std::vector<Node>& children, |
424 |
|
const std::vector<Node>& args, |
425 |
|
CDProof& cdp) |
426 |
|
{ |
427 |
|
// delete attributes |
428 |
|
Node sanitized_conclusion = conclusion; |
429 |
|
if (expr::hasClosure(conclusion)) |
430 |
|
{ |
431 |
|
sanitized_conclusion = d_anc.convert(conclusion); |
432 |
|
} |
433 |
|
|
434 |
|
std::vector<Node> new_args = std::vector<Node>(); |
435 |
|
new_args.push_back( |
436 |
|
NodeManager::currentNM()->mkConst<Rational>(static_cast<unsigned>(rule))); |
437 |
|
new_args.push_back(res); |
438 |
|
new_args.push_back(sanitized_conclusion); |
439 |
|
new_args.insert(new_args.end(), args.begin(), args.end()); |
440 |
|
Trace("alethe-proof") << "... add Alethe step " << res << " / " << conclusion |
441 |
|
<< " " << rule << " " << children << " / " << new_args |
442 |
|
<< std::endl; |
443 |
|
return cdp.addStep(res, PfRule::ALETHE_RULE, children, new_args); |
444 |
|
} |
445 |
|
|
446 |
|
bool AletheProofPostprocessCallback::addAletheStepFromOr( |
447 |
|
AletheRule rule, |
448 |
|
Node res, |
449 |
|
const std::vector<Node>& children, |
450 |
|
const std::vector<Node>& args, |
451 |
|
CDProof& cdp) |
452 |
|
{ |
453 |
|
std::vector<Node> subterms = {d_cl}; |
454 |
|
subterms.insert(subterms.end(), res.begin(), res.end()); |
455 |
|
Node conclusion = NodeManager::currentNM()->mkNode(kind::SEXPR, subterms); |
456 |
|
return addAletheStep(rule, res, conclusion, children, args, cdp); |
457 |
|
} |
458 |
|
|
459 |
|
AletheProofPostprocessFinalCallback::AletheProofPostprocessFinalCallback( |
460 |
|
ProofNodeManager* pnm, AletheNodeConverter& anc) |
461 |
|
: d_pnm(pnm), d_anc(anc) |
462 |
|
{ |
463 |
|
NodeManager* nm = NodeManager::currentNM(); |
464 |
|
d_cl = nm->mkBoundVar("cl", nm->sExprType()); |
465 |
|
} |
466 |
|
|
467 |
|
bool AletheProofPostprocessFinalCallback::shouldUpdate( |
468 |
|
std::shared_ptr<ProofNode> pn, |
469 |
|
const std::vector<Node>& fa, |
470 |
|
bool& continueUpdate) |
471 |
|
{ |
472 |
|
return false; |
473 |
|
} |
474 |
|
|
475 |
|
bool AletheProofPostprocessFinalCallback::update( |
476 |
|
Node res, |
477 |
|
PfRule id, |
478 |
|
const std::vector<Node>& children, |
479 |
|
const std::vector<Node>& args, |
480 |
|
CDProof* cdp, |
481 |
|
bool& continueUpdate) |
482 |
|
{ |
483 |
|
return true; |
484 |
|
} |
485 |
|
|
486 |
|
AletheProofPostprocess::AletheProofPostprocess(ProofNodeManager* pnm, |
487 |
|
AletheNodeConverter& anc) |
488 |
|
: d_pnm(pnm), d_cb(d_pnm, anc), d_fcb(d_pnm, anc) |
489 |
|
{ |
490 |
|
} |
491 |
|
|
492 |
|
AletheProofPostprocess::~AletheProofPostprocess() {} |
493 |
|
|
494 |
|
void AletheProofPostprocess::process(std::shared_ptr<ProofNode> pf) {} |
495 |
|
|
496 |
|
} // namespace proof |
497 |
|
|
498 |
22746 |
} // namespace cvc5 |