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