1 |
|
/********************* */ |
2 |
|
/*! \file lfsc_post_processor.cpp |
3 |
|
** \verbatim |
4 |
|
** Top contributors (to current version): |
5 |
|
** Andrew Reynolds |
6 |
|
** This file is part of the CVC4 project. |
7 |
|
** Copyright (c) 2009-2020 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.\endverbatim |
11 |
|
** |
12 |
|
** \brief Implementation of the Lfsc post proccessor |
13 |
|
**/ |
14 |
|
|
15 |
|
#include "proof/lfsc/lfsc_post_processor.h" |
16 |
|
|
17 |
|
#include "options/proof_options.h" |
18 |
|
#include "proof/lazy_proof.h" |
19 |
|
#include "proof/lfsc/lfsc_printer.h" |
20 |
|
#include "proof/proof_checker.h" |
21 |
|
#include "proof/proof_node_algorithm.h" |
22 |
|
#include "proof/proof_node_manager.h" |
23 |
|
#include "proof/proof_node_updater.h" |
24 |
|
|
25 |
|
using namespace cvc5::kind; |
26 |
|
|
27 |
|
namespace cvc5 { |
28 |
|
namespace proof { |
29 |
|
|
30 |
1 |
LfscProofPostprocessCallback::LfscProofPostprocessCallback( |
31 |
1 |
LfscNodeConverter& ltp, ProofNodeManager* pnm) |
32 |
1 |
: d_pnm(pnm), d_pc(pnm->getChecker()), d_tproc(ltp), d_firstTime(false) |
33 |
|
{ |
34 |
1 |
} |
35 |
|
|
36 |
1 |
void LfscProofPostprocessCallback::initializeUpdate() { d_firstTime = true; } |
37 |
|
|
38 |
49 |
bool LfscProofPostprocessCallback::shouldUpdate(std::shared_ptr<ProofNode> pn, |
39 |
|
const std::vector<Node>& fa, |
40 |
|
bool& continueUpdate) |
41 |
|
{ |
42 |
49 |
return pn->getRule() != PfRule::LFSC_RULE; |
43 |
|
} |
44 |
|
|
45 |
31 |
bool LfscProofPostprocessCallback::update(Node res, |
46 |
|
PfRule id, |
47 |
|
const std::vector<Node>& children, |
48 |
|
const std::vector<Node>& args, |
49 |
|
CDProof* cdp, |
50 |
|
bool& continueUpdate) |
51 |
|
{ |
52 |
62 |
Trace("lfsc-pp") << "LfscProofPostprocessCallback::update: " << id |
53 |
31 |
<< std::endl; |
54 |
31 |
Trace("lfsc-pp-debug") << "...proves " << res << std::endl; |
55 |
31 |
NodeManager* nm = NodeManager::currentNM(); |
56 |
31 |
Assert(id != PfRule::LFSC_RULE); |
57 |
31 |
bool isFirstTime = d_firstTime; |
58 |
|
// On the first call to update, the proof node is the outermost scope of the |
59 |
|
// proof. This scope should not be printed in the LFSC proof. Instead, the |
60 |
|
// LFSC proof printer will print the proper scope around the proof, which |
61 |
|
// e.g. involves an LFSC "check" command. |
62 |
31 |
d_firstTime = false; |
63 |
|
|
64 |
31 |
switch (id) |
65 |
|
{ |
66 |
1 |
case PfRule::SCOPE: |
67 |
|
{ |
68 |
1 |
if (isFirstTime) |
69 |
|
{ |
70 |
|
// Note that we do not want to modify the top-most SCOPE |
71 |
1 |
return false; |
72 |
|
} |
73 |
|
Assert(children.size() == 1); |
74 |
|
// (SCOPE P :args (F1 ... Fn)) |
75 |
|
// becomes |
76 |
|
// (scope _ _ (\ X1 ... (scope _ _ (\ Xn P)) ... )) |
77 |
|
Node curr = children[0]; |
78 |
|
for (size_t i = 0, nargs = args.size(); i < nargs; i++) |
79 |
|
{ |
80 |
|
size_t ii = (nargs - 1) - i; |
81 |
|
// Use a dummy conclusion for what LAMBDA proves, since there is no |
82 |
|
// FOL representation for its type. |
83 |
|
Node fconc = mkDummyPredicate(); |
84 |
|
addLfscRule(cdp, fconc, {curr}, LfscRule::LAMBDA, {args[ii]}); |
85 |
|
// we use a chained implication (=> F1 ... (=> Fn C)) which avoids |
86 |
|
// aliasing. |
87 |
|
Node next = nm->mkNode(OR, args[ii].notNode(), curr); |
88 |
|
addLfscRule(cdp, next, {fconc}, LfscRule::SCOPE, {args[ii]}); |
89 |
|
curr = next; |
90 |
|
} |
91 |
|
// In LFSC, we have now proved: |
92 |
|
// (or (not F1) (or (not F2) ... (or (not Fn) C) ... )) |
93 |
|
// We now must convert this to one of two cases |
94 |
|
if (res.getKind() == NOT) |
95 |
|
{ |
96 |
|
// we have C = false, |
97 |
|
// convert to (not (and F1 (and F2 ... (and Fn true) ... ))) |
98 |
|
// this also handles the case where the conclusion is simply F1, |
99 |
|
// when n=1. |
100 |
|
addLfscRule(cdp, res, {curr}, LfscRule::NOT_AND_REV, {}); |
101 |
|
} |
102 |
|
else |
103 |
|
{ |
104 |
|
// we have that C != false |
105 |
|
// convert to (=> (and F1 (and F2 ... (and Fn true) ... )) C) |
106 |
|
addLfscRule(cdp, res, {curr}, LfscRule::PROCESS_SCOPE, {children[0]}); |
107 |
1 |
} |
108 |
|
} |
109 |
|
break; |
110 |
1 |
case PfRule::CHAIN_RESOLUTION: |
111 |
|
{ |
112 |
|
// turn into binary resolution |
113 |
2 |
Node cur = children[0]; |
114 |
2 |
for (size_t i = 1, size = children.size(); i < size; i++) |
115 |
|
{ |
116 |
2 |
std::vector<Node> newChildren{cur, children[i]}; |
117 |
2 |
std::vector<Node> newArgs{args[(i - 1) * 2], args[(i - 1) * 2 + 1]}; |
118 |
1 |
cur = d_pc->checkDebug(PfRule::RESOLUTION, newChildren, newArgs); |
119 |
1 |
cdp->addStep(cur, PfRule::RESOLUTION, newChildren, newArgs); |
120 |
1 |
} |
121 |
|
} |
122 |
1 |
break; |
123 |
|
case PfRule::SYMM: |
124 |
|
{ |
125 |
|
if (res.getKind() != NOT) |
126 |
|
{ |
127 |
|
// no need to convert (positive) equality symmetry |
128 |
|
return false; |
129 |
|
} |
130 |
|
// must use alternate SYMM rule for disequality |
131 |
|
addLfscRule(cdp, res, {children[0]}, LfscRule::NEG_SYMM, {}); |
132 |
|
} |
133 |
|
break; |
134 |
1 |
case PfRule::TRANS: |
135 |
|
{ |
136 |
1 |
if (children.size() <= 2) |
137 |
|
{ |
138 |
|
// no need to change |
139 |
1 |
return false; |
140 |
|
} |
141 |
|
// turn into binary |
142 |
|
Node cur = children[0]; |
143 |
|
std::unordered_set<Node> processed; |
144 |
|
processed.insert(children.begin(), children.end()); |
145 |
|
for (size_t i = 1, size = children.size(); i < size; i++) |
146 |
|
{ |
147 |
|
std::vector<Node> newChildren{cur, children[i]}; |
148 |
|
cur = d_pc->checkDebug(PfRule::TRANS, newChildren, {}); |
149 |
|
if (processed.find(cur) != processed.end()) |
150 |
|
{ |
151 |
|
continue; |
152 |
|
} |
153 |
|
processed.insert(cur); |
154 |
|
cdp->addStep(cur, PfRule::TRANS, newChildren, {}); |
155 |
1 |
} |
156 |
|
} |
157 |
|
break; |
158 |
5 |
case PfRule::CONG: |
159 |
|
{ |
160 |
5 |
Assert(res.getKind() == EQUAL); |
161 |
5 |
Assert(res[0].getOperator() == res[1].getOperator()); |
162 |
10 |
Trace("lfsc-pp-cong") << "Processing congruence for " << res << " " |
163 |
5 |
<< res[0].getKind() << std::endl; |
164 |
|
// different for closures |
165 |
5 |
if (res[0].isClosure()) |
166 |
|
{ |
167 |
|
if (res[0][0] != res[1][0]) |
168 |
|
{ |
169 |
|
// cannot convert congruence with different variables currently |
170 |
|
return false; |
171 |
|
} |
172 |
|
Node cop = d_tproc.getOperatorOfClosure(res[0]); |
173 |
|
Trace("lfsc-pp-qcong") << "Operator for closure " << cop << std::endl; |
174 |
|
// start with base case body = body' |
175 |
|
Node curL = children[1][0]; |
176 |
|
Node curR = children[1][1]; |
177 |
|
Node currEq = children[1]; |
178 |
|
Trace("lfsc-pp-qcong") << "Base congruence " << currEq << std::endl; |
179 |
|
for (size_t i = 0, nvars = res[0][0].getNumChildren(); i < nvars; i++) |
180 |
|
{ |
181 |
|
Trace("lfsc-pp-qcong") << "Process child " << i << std::endl; |
182 |
|
// CONG rules for each variable |
183 |
|
Node v = res[0][0][nvars - 1 - i]; |
184 |
|
Node vop = d_tproc.getOperatorOfBoundVar(cop, v); |
185 |
|
Node vopEq = vop.eqNode(vop); |
186 |
|
cdp->addStep(vopEq, PfRule::REFL, {}, {vop}); |
187 |
|
Node nextEq; |
188 |
|
if (i + 1 == nvars) |
189 |
|
{ |
190 |
|
// if we are at the end, we prove the final equality |
191 |
|
nextEq = res; |
192 |
|
} |
193 |
|
else |
194 |
|
{ |
195 |
|
curL = nm->mkNode(HO_APPLY, vop, curL); |
196 |
|
curR = nm->mkNode(HO_APPLY, vop, curR); |
197 |
|
nextEq = curL.eqNode(curR); |
198 |
|
} |
199 |
|
addLfscRule(cdp, nextEq, {vopEq, currEq}, LfscRule::CONG, {}); |
200 |
|
currEq = nextEq; |
201 |
|
} |
202 |
|
return true; |
203 |
|
} |
204 |
5 |
Kind k = res[0].getKind(); |
205 |
5 |
if (k == HO_APPLY) |
206 |
|
{ |
207 |
|
// HO_APPLY congruence is a single application of LFSC congruence |
208 |
|
addLfscRule(cdp, res, children, LfscRule::CONG, {}); |
209 |
|
return true; |
210 |
|
} |
211 |
|
// We are proving f(t1, ..., tn) = f(s1, ..., sn), nested. |
212 |
|
// First, get the operator, which will be used for printing the base |
213 |
|
// REFL step. Notice this may be for interpreted or uninterpreted |
214 |
|
// function symbols. |
215 |
10 |
Node op = d_tproc.getOperatorOfTerm(res[0]); |
216 |
10 |
Trace("lfsc-pp-cong") << "Processing cong for op " << op << " " |
217 |
5 |
<< op.getType() << std::endl; |
218 |
5 |
Assert(!op.isNull()); |
219 |
|
// initial base step is REFL |
220 |
10 |
Node opEq = op.eqNode(op); |
221 |
5 |
cdp->addStep(opEq, PfRule::REFL, {}, {op}); |
222 |
5 |
size_t nchildren = children.size(); |
223 |
10 |
Node nullTerm = d_tproc.getNullTerminator(k, res[0].getType()); |
224 |
|
// Are we doing congruence of an n-ary operator? If so, notice that op |
225 |
|
// is a binary operator and we must apply congruence in a special way. |
226 |
|
// Note we use the first block of code if we have more than 2 children, |
227 |
|
// or if we have a null terminator. |
228 |
|
// special case: constructors and apply uf are not treated as n-ary; these |
229 |
|
// symbols have function types that expect n arguments. |
230 |
8 |
bool isNary = NodeManager::isNAryKind(k) && k != kind::APPLY_CONSTRUCTOR |
231 |
8 |
&& k != kind::APPLY_UF; |
232 |
5 |
if (isNary && (nchildren > 2 || !nullTerm.isNull())) |
233 |
|
{ |
234 |
|
// get the null terminator for the kind, which may mean we are doing |
235 |
|
// a special kind of congruence for n-ary kinds whose base is a REFL |
236 |
|
// step for the null terminator. |
237 |
6 |
Node currEq; |
238 |
3 |
if (!nullTerm.isNull()) |
239 |
|
{ |
240 |
3 |
currEq = nullTerm.eqNode(nullTerm); |
241 |
|
// if we have a null terminator, we do a final REFL step to add |
242 |
|
// the null terminator to both sides. |
243 |
3 |
cdp->addStep(currEq, PfRule::REFL, {}, {nullTerm}); |
244 |
|
} |
245 |
|
else |
246 |
|
{ |
247 |
|
// Otherwise, start with the last argument. |
248 |
|
currEq = children[nchildren - 1]; |
249 |
|
} |
250 |
11 |
for (size_t i = 0; i < nchildren; i++) |
251 |
|
{ |
252 |
8 |
size_t ii = (nchildren - 1) - i; |
253 |
16 |
Node uop = op; |
254 |
|
// special case: each bv concat in the chain has a different type, |
255 |
|
// so remake the operator here. |
256 |
8 |
if (k == kind::BITVECTOR_CONCAT) |
257 |
|
{ |
258 |
|
// we get the operator of the next argument concatenated with the |
259 |
|
// current accumulated remainder. |
260 |
|
Node currApp = |
261 |
|
nm->mkNode(kind::BITVECTOR_CONCAT, children[ii][0], currEq[0]); |
262 |
|
uop = d_tproc.getOperatorOfTerm(currApp); |
263 |
|
} |
264 |
|
Node argAppEq = |
265 |
16 |
nm->mkNode(HO_APPLY, uop, children[ii][0]) |
266 |
16 |
.eqNode(nm->mkNode(HO_APPLY, uop, children[ii][1])); |
267 |
8 |
addLfscRule(cdp, argAppEq, {opEq, children[ii]}, LfscRule::CONG, {}); |
268 |
|
// now, congruence to the current equality |
269 |
16 |
Node nextEq; |
270 |
8 |
if (ii == 0) |
271 |
|
{ |
272 |
|
// use final conclusion |
273 |
3 |
nextEq = res; |
274 |
|
} |
275 |
|
else |
276 |
|
{ |
277 |
|
// otherwise continue to apply |
278 |
15 |
nextEq = nm->mkNode(HO_APPLY, argAppEq[0], currEq[0]) |
279 |
10 |
.eqNode(nm->mkNode(HO_APPLY, argAppEq[1], currEq[1])); |
280 |
|
} |
281 |
8 |
addLfscRule(cdp, nextEq, {argAppEq, currEq}, LfscRule::CONG, {}); |
282 |
8 |
currEq = nextEq; |
283 |
|
} |
284 |
|
} |
285 |
|
else |
286 |
|
{ |
287 |
|
// non n-ary kinds do not have null terminators |
288 |
2 |
Assert(nullTerm.isNull()); |
289 |
4 |
Node curL = op; |
290 |
4 |
Node curR = op; |
291 |
4 |
Node currEq = opEq; |
292 |
4 |
for (size_t i = 0; i < nchildren; i++) |
293 |
|
{ |
294 |
|
// CONG rules for each child |
295 |
4 |
Node nextEq; |
296 |
2 |
if (i + 1 == nchildren) |
297 |
|
{ |
298 |
|
// if we are at the end, we prove the final equality |
299 |
2 |
nextEq = res; |
300 |
|
} |
301 |
|
else |
302 |
|
{ |
303 |
|
curL = nm->mkNode(HO_APPLY, curL, children[i][0]); |
304 |
|
curR = nm->mkNode(HO_APPLY, curR, children[i][1]); |
305 |
|
nextEq = curL.eqNode(curR); |
306 |
|
} |
307 |
2 |
addLfscRule(cdp, nextEq, {currEq, children[i]}, LfscRule::CONG, {}); |
308 |
2 |
currEq = nextEq; |
309 |
|
} |
310 |
5 |
} |
311 |
|
} |
312 |
5 |
break; |
313 |
|
case PfRule::AND_INTRO: |
314 |
|
{ |
315 |
|
Node cur = d_tproc.getNullTerminator(AND); |
316 |
|
size_t nchildren = children.size(); |
317 |
|
for (size_t j = 0; j < nchildren; j++) |
318 |
|
{ |
319 |
|
size_t jj = (nchildren - 1) - j; |
320 |
|
// conclude the final conclusion if we are finished |
321 |
|
Node next = jj == 0 ? res : nm->mkNode(AND, children[jj], cur); |
322 |
|
if (j == 0) |
323 |
|
{ |
324 |
|
addLfscRule(cdp, next, {children[jj]}, LfscRule::AND_INTRO1, {}); |
325 |
|
} |
326 |
|
else |
327 |
|
{ |
328 |
|
addLfscRule(cdp, next, {children[jj], cur}, LfscRule::AND_INTRO2, {}); |
329 |
|
} |
330 |
|
cur = next; |
331 |
|
} |
332 |
|
} |
333 |
|
break; |
334 |
|
case PfRule::ARITH_SUM_UB: |
335 |
|
{ |
336 |
|
// proof of null terminator base 0 = 0 |
337 |
|
Node zero = d_tproc.getNullTerminator(PLUS); |
338 |
|
Node cur = zero.eqNode(zero); |
339 |
|
cdp->addStep(cur, PfRule::REFL, {}, {zero}); |
340 |
|
for (size_t i = 0, size = children.size(); i < size; i++) |
341 |
|
{ |
342 |
|
size_t ii = (children.size() - 1) - i; |
343 |
|
std::vector<Node> newChildren{children[ii], cur}; |
344 |
|
if (ii == 0) |
345 |
|
{ |
346 |
|
// final rule must be the real conclusion |
347 |
|
addLfscRule(cdp, res, newChildren, LfscRule::ARITH_SUM_UB, {}); |
348 |
|
} |
349 |
|
else |
350 |
|
{ |
351 |
|
// rules build an n-ary chain of + on both sides |
352 |
|
cur = d_pc->checkDebug(PfRule::ARITH_SUM_UB, newChildren, {}); |
353 |
|
addLfscRule(cdp, cur, newChildren, LfscRule::ARITH_SUM_UB, {}); |
354 |
|
} |
355 |
|
} |
356 |
|
} |
357 |
|
break; |
358 |
23 |
default: return false; break; |
359 |
|
} |
360 |
6 |
AlwaysAssert(cdp->getProofFor(res)->getRule() != PfRule::ASSUME); |
361 |
6 |
return true; |
362 |
|
} |
363 |
|
|
364 |
18 |
void LfscProofPostprocessCallback::addLfscRule( |
365 |
|
CDProof* cdp, |
366 |
|
Node conc, |
367 |
|
const std::vector<Node>& children, |
368 |
|
LfscRule lr, |
369 |
|
const std::vector<Node>& args) |
370 |
|
{ |
371 |
36 |
std::vector<Node> largs; |
372 |
18 |
largs.push_back(mkLfscRuleNode(lr)); |
373 |
18 |
largs.push_back(conc); |
374 |
18 |
largs.insert(largs.end(), args.begin(), args.end()); |
375 |
18 |
cdp->addStep(conc, PfRule::LFSC_RULE, children, largs); |
376 |
18 |
} |
377 |
|
|
378 |
|
Node LfscProofPostprocessCallback::mkChain(Kind k, |
379 |
|
const std::vector<Node>& children) |
380 |
|
{ |
381 |
|
Assert(!children.empty()); |
382 |
|
NodeManager* nm = NodeManager::currentNM(); |
383 |
|
size_t nchildren = children.size(); |
384 |
|
size_t i = 0; |
385 |
|
// do we have a null terminator? If so, we start with it. |
386 |
|
Node ret = d_tproc.getNullTerminator(k, children[0].getType()); |
387 |
|
if (ret.isNull()) |
388 |
|
{ |
389 |
|
ret = children[nchildren - 1]; |
390 |
|
i = 1; |
391 |
|
} |
392 |
|
while (i < nchildren) |
393 |
|
{ |
394 |
|
ret = nm->mkNode(k, children[(nchildren - 1) - i], ret); |
395 |
|
i++; |
396 |
|
} |
397 |
|
return ret; |
398 |
|
} |
399 |
|
|
400 |
|
Node LfscProofPostprocessCallback::mkDummyPredicate() |
401 |
|
{ |
402 |
|
NodeManager* nm = NodeManager::currentNM(); |
403 |
|
return nm->mkBoundVar(nm->booleanType()); |
404 |
|
} |
405 |
|
|
406 |
1 |
LfscProofPostprocess::LfscProofPostprocess(LfscNodeConverter& ltp, |
407 |
1 |
ProofNodeManager* pnm) |
408 |
1 |
: d_cb(new proof::LfscProofPostprocessCallback(ltp, pnm)), d_pnm(pnm) |
409 |
|
{ |
410 |
1 |
} |
411 |
|
|
412 |
1 |
void LfscProofPostprocess::process(std::shared_ptr<ProofNode> pf) |
413 |
|
{ |
414 |
1 |
d_cb->initializeUpdate(); |
415 |
|
// do not automatically add symmetry steps, since this leads to |
416 |
|
// non-termination for example on policy_variable.smt2 |
417 |
2 |
ProofNodeUpdater updater(d_pnm, *(d_cb.get()), false, false); |
418 |
1 |
updater.process(pf); |
419 |
1 |
} |
420 |
|
|
421 |
|
} // namespace proof |
422 |
31137 |
} // namespace cvc5 |