1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds |
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 printer for LFSC proofs |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "proof/lfsc/lfsc_printer.h" |
17 |
|
|
18 |
|
#include <sstream> |
19 |
|
|
20 |
|
#include "expr/dtype.h" |
21 |
|
#include "expr/dtype_cons.h" |
22 |
|
#include "expr/dtype_selector.h" |
23 |
|
#include "expr/node_algorithm.h" |
24 |
|
#include "expr/skolem_manager.h" |
25 |
|
#include "proof/lfsc/lfsc_list_sc_node_converter.h" |
26 |
|
#include "proof/lfsc/lfsc_print_channel.h" |
27 |
|
|
28 |
|
using namespace cvc5::kind; |
29 |
|
|
30 |
|
namespace cvc5 { |
31 |
|
namespace proof { |
32 |
|
|
33 |
1 |
LfscPrinter::LfscPrinter(LfscNodeConverter& ltp) |
34 |
1 |
: d_tproc(ltp), d_assumpCounter(0) |
35 |
|
{ |
36 |
1 |
NodeManager* nm = NodeManager::currentNM(); |
37 |
1 |
d_boolType = nm->booleanType(); |
38 |
|
// used for the `flag` type in LFSC |
39 |
1 |
d_tt = d_tproc.mkInternalSymbol("tt", d_boolType); |
40 |
1 |
d_ff = d_tproc.mkInternalSymbol("ff", d_boolType); |
41 |
1 |
} |
42 |
|
|
43 |
1 |
void LfscPrinter::print(std::ostream& out, |
44 |
|
const std::vector<Node>& assertions, |
45 |
|
const ProofNode* pn) |
46 |
|
{ |
47 |
1 |
Trace("lfsc-print-debug") << "; ORIGINAL PROOF: " << *pn << std::endl; |
48 |
1 |
Assert (!pn->getChildren().empty()); |
49 |
|
// closing parentheses |
50 |
2 |
std::stringstream cparen; |
51 |
1 |
const ProofNode* pnBody = pn->getChildren()[0].get(); |
52 |
|
|
53 |
|
// clear the rules we have warned about |
54 |
1 |
d_trustWarned.clear(); |
55 |
|
|
56 |
1 |
Trace("lfsc-print-debug") << "; print declarations" << std::endl; |
57 |
|
// [1] compute and print the declarations |
58 |
2 |
std::unordered_set<Node> syms; |
59 |
2 |
std::unordered_set<TNode> visited; |
60 |
2 |
std::vector<Node> iasserts; |
61 |
2 |
std::map<Node, size_t> passumeMap; |
62 |
2 |
std::unordered_set<TypeNode> types; |
63 |
2 |
std::unordered_set<TNode> typeVisited; |
64 |
4 |
for (size_t i = 0, nasserts = assertions.size(); i < nasserts; i++) |
65 |
|
{ |
66 |
6 |
Node a = assertions[i]; |
67 |
3 |
expr::getSymbols(a, syms, visited); |
68 |
3 |
expr::getTypes(a, types, typeVisited); |
69 |
3 |
iasserts.push_back(d_tproc.convert(a)); |
70 |
|
// remember the assumption name |
71 |
3 |
passumeMap[a] = i; |
72 |
|
} |
73 |
1 |
d_assumpCounter = assertions.size(); |
74 |
1 |
Trace("lfsc-print-debug") << "; print sorts" << std::endl; |
75 |
|
// [1a] user declared sorts |
76 |
2 |
std::stringstream preamble; |
77 |
2 |
std::unordered_set<TypeNode> sts; |
78 |
2 |
std::unordered_set<size_t> tupleArity; |
79 |
3 |
for (const TypeNode& st : types) |
80 |
|
{ |
81 |
|
// note that we must get all "component types" of a type, so that |
82 |
|
// e.g. U is printed as a sort declaration when we have type (Array U Int). |
83 |
4 |
std::unordered_set<TypeNode> ctypes; |
84 |
2 |
expr::getComponentTypes(st, ctypes); |
85 |
4 |
for (const TypeNode& stc : ctypes) |
86 |
|
{ |
87 |
2 |
if (sts.find(stc) != sts.end()) |
88 |
|
{ |
89 |
|
continue; |
90 |
|
} |
91 |
2 |
sts.insert(stc); |
92 |
2 |
if (stc.isSort()) |
93 |
|
{ |
94 |
1 |
preamble << "(declare "; |
95 |
1 |
printType(preamble, stc); |
96 |
1 |
preamble << " sort)" << std::endl; |
97 |
|
} |
98 |
1 |
else if (stc.isDatatype()) |
99 |
|
{ |
100 |
|
const DType& dt = stc.getDType(); |
101 |
|
if (stc.getKind() == PARAMETRIC_DATATYPE) |
102 |
|
{ |
103 |
|
// skip the instance of a parametric datatype |
104 |
|
continue; |
105 |
|
} |
106 |
|
preamble << "; DATATYPE " << dt.getName() << std::endl; |
107 |
|
if (dt.isTuple()) |
108 |
|
{ |
109 |
|
const DTypeConstructor& cons = dt[0]; |
110 |
|
size_t arity = cons.getNumArgs(); |
111 |
|
if (tupleArity.find(arity) == tupleArity.end()) |
112 |
|
{ |
113 |
|
tupleArity.insert(arity); |
114 |
|
preamble << "(declare Tuple_" << arity << " "; |
115 |
|
std::stringstream tcparen; |
116 |
|
for (size_t j = 0, nargs = cons.getNumArgs(); j < nargs; j++) |
117 |
|
{ |
118 |
|
preamble << "(! s" << j << " sort "; |
119 |
|
tcparen << ")"; |
120 |
|
} |
121 |
|
preamble << "sort" << tcparen.str() << ")"; |
122 |
|
} |
123 |
|
preamble << std::endl; |
124 |
|
} |
125 |
|
else |
126 |
|
{ |
127 |
|
preamble << "(declare "; |
128 |
|
printType(preamble, stc); |
129 |
|
std::stringstream cdttparens; |
130 |
|
if (dt.isParametric()) |
131 |
|
{ |
132 |
|
std::vector<TypeNode> params = dt.getParameters(); |
133 |
|
for (const TypeNode& tn : params) |
134 |
|
{ |
135 |
|
preamble << " (! " << tn << " sort"; |
136 |
|
cdttparens << ")"; |
137 |
|
} |
138 |
|
} |
139 |
|
preamble << " sort)" << cdttparens.str() << std::endl; |
140 |
|
} |
141 |
|
for (size_t i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) |
142 |
|
{ |
143 |
|
const DTypeConstructor& cons = dt[i]; |
144 |
|
std::stringstream sscons; |
145 |
|
sscons << d_tproc.convert(cons.getConstructor()); |
146 |
|
std::string cname = |
147 |
|
LfscNodeConverter::getNameForUserName(sscons.str()); |
148 |
|
// print construct/tester |
149 |
|
preamble << "(declare " << cname << " term)" << std::endl; |
150 |
|
for (size_t j = 0, nargs = cons.getNumArgs(); j < nargs; j++) |
151 |
|
{ |
152 |
|
const DTypeSelector& arg = cons[j]; |
153 |
|
// print selector |
154 |
|
Node si = d_tproc.convert(arg.getSelector()); |
155 |
|
std::stringstream sns; |
156 |
|
sns << si; |
157 |
|
std::string sname = |
158 |
|
LfscNodeConverter::getNameForUserName(sns.str()); |
159 |
|
preamble << "(declare " << sname << " term)" << std::endl; |
160 |
|
} |
161 |
|
} |
162 |
|
// testers and updaters are instances of parametric symbols |
163 |
|
// shared selectors are instance of parametric symbol "sel" |
164 |
|
preamble << "; END DATATYPE " << std::endl; |
165 |
|
} |
166 |
|
// all other sorts are builtin into the LFSC signature |
167 |
|
} |
168 |
|
} |
169 |
1 |
Trace("lfsc-print-debug") << "; print user symbols" << std::endl; |
170 |
|
// [1b] user declare function symbols |
171 |
6 |
for (const Node& s : syms) |
172 |
|
{ |
173 |
10 |
TypeNode st = s.getType(); |
174 |
15 |
if (st.isConstructor() || st.isSelector() || st.isTester() |
175 |
10 |
|| st.isUpdater()) |
176 |
|
{ |
177 |
|
// constructors, selector, testers, updaters are defined by the datatype |
178 |
|
continue; |
179 |
|
} |
180 |
10 |
Node si = d_tproc.convert(s); |
181 |
10 |
preamble << "(define " << si << " (var " |
182 |
5 |
<< d_tproc.getOrAssignIndexForVar(s) << " "; |
183 |
5 |
printType(preamble, st); |
184 |
5 |
preamble << "))" << std::endl; |
185 |
|
} |
186 |
|
|
187 |
1 |
Trace("lfsc-print-debug") << "; compute proof letification" << std::endl; |
188 |
|
// [2] compute the proof letification |
189 |
2 |
std::vector<const ProofNode*> pletList; |
190 |
2 |
std::map<const ProofNode*, size_t> pletMap; |
191 |
1 |
computeProofLetification(pnBody, pletList, pletMap); |
192 |
|
|
193 |
1 |
Trace("lfsc-print-debug") << "; compute term lets" << std::endl; |
194 |
|
// compute the term lets |
195 |
2 |
LetBinding lbind; |
196 |
4 |
for (const Node& ia : iasserts) |
197 |
|
{ |
198 |
3 |
lbind.process(ia); |
199 |
|
} |
200 |
|
// We do a "dry-run" of proof printing here, using the LetBinding print |
201 |
|
// channel. This pass traverses the proof but does not print it, but instead |
202 |
|
// updates the let binding data structure for all nodes that appear anywhere |
203 |
|
// in the proof. |
204 |
2 |
LfscPrintChannelPre lpcp(lbind); |
205 |
2 |
LetBinding emptyLetBind; |
206 |
1 |
std::map<const ProofNode*, size_t>::iterator itp; |
207 |
4 |
for (const ProofNode* p : pletList) |
208 |
|
{ |
209 |
3 |
itp = pletMap.find(p); |
210 |
3 |
Assert(itp != pletMap.end()); |
211 |
3 |
size_t pid = itp->second; |
212 |
3 |
pletMap.erase(p); |
213 |
3 |
printProofInternal(&lpcp, p, emptyLetBind, pletMap, passumeMap); |
214 |
3 |
pletMap[p] = pid; |
215 |
|
} |
216 |
|
// Print the body of the outermost scope |
217 |
1 |
printProofInternal(&lpcp, pnBody, emptyLetBind, pletMap, passumeMap); |
218 |
|
|
219 |
|
// [3] print warnings |
220 |
2 |
for (PfRule r : d_trustWarned) |
221 |
|
{ |
222 |
1 |
out << "; WARNING: adding trust step for " << r << std::endl; |
223 |
|
} |
224 |
|
|
225 |
|
// [4] print the DSL rewrite rule declarations |
226 |
|
// TODO cvc5-projects #285. |
227 |
|
|
228 |
|
// [5] print the check command and term lets |
229 |
1 |
out << preamble.str(); |
230 |
1 |
out << "(check" << std::endl; |
231 |
1 |
cparen << ")"; |
232 |
|
// print the term let list |
233 |
1 |
printLetList(out, cparen, lbind); |
234 |
|
|
235 |
1 |
Trace("lfsc-print-debug") << "; print asserts" << std::endl; |
236 |
|
// [6] print the assertions, with letification |
237 |
|
// the assumption identifier mapping |
238 |
4 |
for (size_t i = 0, nasserts = iasserts.size(); i < nasserts; i++) |
239 |
|
{ |
240 |
6 |
Node ia = iasserts[i]; |
241 |
3 |
out << "(% "; |
242 |
3 |
LfscPrintChannelOut::printAssumeId(out, i); |
243 |
3 |
out << " (holds "; |
244 |
3 |
printInternal(out, ia, lbind); |
245 |
3 |
out << ")" << std::endl; |
246 |
3 |
cparen << ")"; |
247 |
|
} |
248 |
|
|
249 |
1 |
Trace("lfsc-print-debug") << "; print annotation" << std::endl; |
250 |
|
// [7] print the annotation |
251 |
1 |
out << "(: (holds false)" << std::endl; |
252 |
1 |
cparen << ")"; |
253 |
|
|
254 |
1 |
Trace("lfsc-print-debug") << "; print proof body" << std::endl; |
255 |
|
// [8] print the proof body |
256 |
1 |
Assert(pn->getRule() == PfRule::SCOPE); |
257 |
|
// the outermost scope can be ignored (it is the scope of the assertions, |
258 |
|
// which are already printed above). |
259 |
2 |
LfscPrintChannelOut lout(out); |
260 |
1 |
printProofLetify(&lout, pnBody, lbind, pletList, pletMap, passumeMap); |
261 |
|
|
262 |
1 |
out << cparen.str() << std::endl; |
263 |
1 |
} |
264 |
|
|
265 |
1 |
void LfscPrinter::printProofLetify( |
266 |
|
LfscPrintChannel* out, |
267 |
|
const ProofNode* pn, |
268 |
|
const LetBinding& lbind, |
269 |
|
const std::vector<const ProofNode*>& pletList, |
270 |
|
std::map<const ProofNode*, size_t>& pletMap, |
271 |
|
std::map<Node, size_t>& passumeMap) |
272 |
|
{ |
273 |
|
// closing parentheses |
274 |
1 |
size_t cparen = 0; |
275 |
|
|
276 |
|
// define the let proofs |
277 |
1 |
if (!pletList.empty()) |
278 |
|
{ |
279 |
1 |
std::map<const ProofNode*, size_t>::iterator itp; |
280 |
4 |
for (const ProofNode* p : pletList) |
281 |
|
{ |
282 |
3 |
itp = pletMap.find(p); |
283 |
3 |
Assert(itp != pletMap.end()); |
284 |
3 |
size_t pid = itp->second; |
285 |
|
// print (plet _ _ |
286 |
3 |
out->printOpenLfscRule(LfscRule::PLET); |
287 |
3 |
cparen++; |
288 |
3 |
out->printHole(); |
289 |
3 |
out->printHole(); |
290 |
3 |
out->printEndLine(); |
291 |
|
// print the letified proof |
292 |
3 |
pletMap.erase(p); |
293 |
3 |
printProofInternal(out, p, lbind, pletMap, passumeMap); |
294 |
3 |
pletMap[p] = pid; |
295 |
|
// print the lambda (\ __pX |
296 |
3 |
out->printOpenLfscRule(LfscRule::LAMBDA); |
297 |
3 |
cparen++; |
298 |
3 |
out->printProofId(pid); |
299 |
3 |
out->printEndLine(); |
300 |
|
} |
301 |
1 |
out->printEndLine(); |
302 |
|
} |
303 |
|
|
304 |
|
// [2] print the proof body |
305 |
1 |
printProofInternal(out, pn, lbind, pletMap, passumeMap); |
306 |
|
|
307 |
|
// print the closing parenthesis |
308 |
1 |
out->printCloseRule(cparen); |
309 |
1 |
} |
310 |
|
|
311 |
8 |
void LfscPrinter::printProofInternal( |
312 |
|
LfscPrintChannel* out, |
313 |
|
const ProofNode* pn, |
314 |
|
const LetBinding& lbind, |
315 |
|
const std::map<const ProofNode*, size_t>& pletMap, |
316 |
|
std::map<Node, size_t>& passumeMap) |
317 |
|
{ |
318 |
|
// the stack |
319 |
16 |
std::vector<PExpr> visit; |
320 |
|
// whether we have to process children |
321 |
16 |
std::unordered_set<const ProofNode*> processingChildren; |
322 |
|
// helper iterators |
323 |
8 |
std::unordered_set<const ProofNode*>::iterator pit; |
324 |
8 |
std::map<const ProofNode*, size_t>::const_iterator pletIt; |
325 |
8 |
std::map<Node, size_t>::iterator passumeIt; |
326 |
16 |
Node curn; |
327 |
16 |
TypeNode curtn; |
328 |
|
const ProofNode* cur; |
329 |
8 |
visit.push_back(PExpr(pn)); |
330 |
366 |
do |
331 |
|
{ |
332 |
374 |
curn = visit.back().d_node; |
333 |
374 |
curtn = visit.back().d_typeNode; |
334 |
374 |
cur = visit.back().d_pnode; |
335 |
374 |
visit.pop_back(); |
336 |
|
// case 1: printing a proof |
337 |
374 |
if (cur != nullptr) |
338 |
|
{ |
339 |
172 |
PfRule r = cur->getRule(); |
340 |
|
// maybe it is letified |
341 |
172 |
pletIt = pletMap.find(cur); |
342 |
188 |
if (pletIt != pletMap.end()) |
343 |
|
{ |
344 |
|
// a letified proof |
345 |
16 |
out->printProofId(pletIt->second); |
346 |
16 |
continue; |
347 |
|
} |
348 |
156 |
pit = processingChildren.find(cur); |
349 |
156 |
if (pit == processingChildren.end()) |
350 |
|
{ |
351 |
84 |
bool isLambda = false; |
352 |
84 |
if (r == PfRule::LFSC_RULE) |
353 |
|
{ |
354 |
36 |
Assert(!cur->getArguments().empty()); |
355 |
36 |
LfscRule lr = getLfscRule(cur->getArguments()[0]); |
356 |
36 |
isLambda = (lr == LfscRule::LAMBDA); |
357 |
|
} |
358 |
84 |
if (r == PfRule::ASSUME) |
359 |
|
{ |
360 |
|
// an assumption, must have a name |
361 |
6 |
passumeIt = passumeMap.find(cur->getResult()); |
362 |
6 |
Assert(passumeIt != passumeMap.end()); |
363 |
6 |
out->printAssumeId(passumeIt->second); |
364 |
|
} |
365 |
78 |
else if (isLambda) |
366 |
|
{ |
367 |
|
Assert(cur->getArguments().size() == 3); |
368 |
|
// lambdas are handled specially. We print in a self contained way |
369 |
|
// here. |
370 |
|
// allocate an assumption, if necessary |
371 |
|
size_t pid; |
372 |
|
Node assumption = cur->getArguments()[2]; |
373 |
|
passumeIt = passumeMap.find(assumption); |
374 |
|
if (passumeIt == passumeMap.end()) |
375 |
|
{ |
376 |
|
pid = d_assumpCounter; |
377 |
|
d_assumpCounter++; |
378 |
|
passumeMap[assumption] = pid; |
379 |
|
} |
380 |
|
else |
381 |
|
{ |
382 |
|
pid = passumeIt->second; |
383 |
|
} |
384 |
|
// make the node whose name is the assumption id, where notice that |
385 |
|
// the type of this node does not matter |
386 |
|
std::stringstream pidNodeName; |
387 |
|
LfscPrintChannelOut::printAssumeId(pidNodeName, pid); |
388 |
|
// must be an internal symbol so that it is not turned into (bvar ...) |
389 |
|
Node pidNode = |
390 |
|
d_tproc.mkInternalSymbol(pidNodeName.str(), d_boolType); |
391 |
|
// print "(\ " |
392 |
|
out->printOpenRule(cur); |
393 |
|
// print the identifier |
394 |
|
out->printNode(pidNode); |
395 |
|
// Print the body of the proof with a fresh proof letification. We can |
396 |
|
// keep the assumption map and the let binding (for terms). |
397 |
|
std::vector<const ProofNode*> pletListNested; |
398 |
|
std::map<const ProofNode*, size_t> pletMapNested; |
399 |
|
const ProofNode* curBody = cur->getChildren()[0].get(); |
400 |
|
computeProofLetification(curBody, pletListNested, pletMapNested); |
401 |
|
printProofLetify( |
402 |
|
out, curBody, lbind, pletListNested, pletMapNested, passumeMap); |
403 |
|
// print ")" |
404 |
|
out->printCloseRule(); |
405 |
|
} |
406 |
|
else |
407 |
|
{ |
408 |
|
// assert that we should traverse cur when letifying |
409 |
78 |
Assert(d_lpltc.shouldTraverse(cur)); |
410 |
|
// a normal rule application, compute the proof arguments, which |
411 |
|
// notice in the case of PI also may modify our passumeMap. |
412 |
156 |
std::vector<PExpr> args; |
413 |
78 |
if (computeProofArgs(cur, args)) |
414 |
|
{ |
415 |
72 |
processingChildren.insert(cur); |
416 |
|
// will revisit this proof node to close parentheses |
417 |
72 |
visit.push_back(PExpr(cur)); |
418 |
72 |
std::reverse(args.begin(), args.end()); |
419 |
72 |
visit.insert(visit.end(), args.begin(), args.end()); |
420 |
|
// print the rule name |
421 |
72 |
out->printOpenRule(cur); |
422 |
|
} |
423 |
|
else |
424 |
|
{ |
425 |
|
// could not print the rule, trust for now |
426 |
12 |
Node res = d_tproc.convert(cur->getResult()); |
427 |
6 |
res = lbind.convert(res, "__t", true); |
428 |
6 |
out->printTrust(res, r); |
429 |
6 |
if (d_trustWarned.find(r) == d_trustWarned.end()) |
430 |
|
{ |
431 |
1 |
d_trustWarned.insert(r); |
432 |
|
} |
433 |
|
} |
434 |
|
} |
435 |
|
} |
436 |
|
else |
437 |
|
{ |
438 |
72 |
processingChildren.erase(cur); |
439 |
72 |
out->printCloseRule(); |
440 |
|
} |
441 |
|
} |
442 |
|
// case 2: printing a node |
443 |
202 |
else if (!curn.isNull()) |
444 |
|
{ |
445 |
|
// it has already been converted to internal form, we letify it here |
446 |
64 |
Node curni = lbind.convert(curn, "__t", true); |
447 |
32 |
out->printNode(curni); |
448 |
|
} |
449 |
|
// case 3: printing a type node |
450 |
170 |
else if (!curtn.isNull()) |
451 |
|
{ |
452 |
|
out->printTypeNode(curtn); |
453 |
|
} |
454 |
|
// case 4: a hole |
455 |
|
else |
456 |
|
{ |
457 |
170 |
out->printHole(); |
458 |
|
} |
459 |
374 |
} while (!visit.empty()); |
460 |
8 |
} |
461 |
|
|
462 |
78 |
bool LfscPrinter::computeProofArgs(const ProofNode* pn, |
463 |
|
std::vector<PExpr>& pargs) |
464 |
|
{ |
465 |
78 |
const std::vector<std::shared_ptr<ProofNode>>& children = pn->getChildren(); |
466 |
156 |
std::vector<const ProofNode*> cs; |
467 |
170 |
for (const std::shared_ptr<ProofNode>& c : children) |
468 |
|
{ |
469 |
92 |
cs.push_back(c.get()); |
470 |
|
} |
471 |
78 |
PfRule r = pn->getRule(); |
472 |
78 |
const std::vector<Node>& args = pn->getArguments(); |
473 |
156 |
std::vector<Node> as; |
474 |
200 |
for (const Node& a : args) |
475 |
|
{ |
476 |
244 |
Node ac = d_tproc.convert(a); |
477 |
122 |
Assert(!ac.isNull()); |
478 |
122 |
as.push_back(ac); |
479 |
|
} |
480 |
|
// The proof expression stream, which packs the next expressions (proofs, |
481 |
|
// terms, sorts, LFSC datatypes) into a print-expression vector pargs. This |
482 |
|
// stream can be used via "pf << e" which appends an expression to the |
483 |
|
// vector maintained by this stream. |
484 |
156 |
PExprStream pf(pargs, d_tt, d_ff); |
485 |
|
// hole |
486 |
156 |
PExpr h; |
487 |
156 |
Trace("lfsc-print-debug2") |
488 |
156 |
<< "Compute proof args " << r << " #children= " << cs.size() |
489 |
78 |
<< " #args=" << as.size() << std::endl; |
490 |
78 |
switch (r) |
491 |
|
{ |
492 |
|
// SAT |
493 |
2 |
case PfRule::RESOLUTION: |
494 |
2 |
pf << h << h << h << cs[0] << cs[1] << args[0].getConst<bool>() << as[1]; |
495 |
2 |
break; |
496 |
|
case PfRule::REORDERING: pf << h << as[0] << cs[0]; break; |
497 |
|
case PfRule::FACTORING: pf << h << h << cs[0]; break; |
498 |
|
// Boolean |
499 |
|
case PfRule::SPLIT: pf << as[0]; break; |
500 |
|
case PfRule::NOT_NOT_ELIM: pf << h << cs[0]; break; |
501 |
2 |
case PfRule::CONTRA: pf << h << cs[0] << cs[1]; break; |
502 |
2 |
case PfRule::MODUS_PONENS: |
503 |
2 |
case PfRule::EQ_RESOLVE: pf << h << h << cs[0] << cs[1]; break; |
504 |
|
case PfRule::NOT_AND: pf << h << h << cs[0]; break; |
505 |
4 |
case PfRule::NOT_OR_ELIM: |
506 |
4 |
case PfRule::AND_ELIM: pf << h << h << args[0] << cs[0]; break; |
507 |
|
case PfRule::IMPLIES_ELIM: |
508 |
|
case PfRule::NOT_IMPLIES_ELIM1: |
509 |
|
case PfRule::NOT_IMPLIES_ELIM2: |
510 |
|
case PfRule::EQUIV_ELIM1: |
511 |
|
case PfRule::EQUIV_ELIM2: |
512 |
|
case PfRule::NOT_EQUIV_ELIM1: |
513 |
|
case PfRule::NOT_EQUIV_ELIM2: |
514 |
|
case PfRule::XOR_ELIM1: |
515 |
|
case PfRule::XOR_ELIM2: |
516 |
|
case PfRule::NOT_XOR_ELIM1: |
517 |
|
case PfRule::NOT_XOR_ELIM2: pf << h << h << cs[0]; break; |
518 |
|
case PfRule::ITE_ELIM1: |
519 |
|
case PfRule::ITE_ELIM2: |
520 |
|
case PfRule::NOT_ITE_ELIM1: |
521 |
|
case PfRule::NOT_ITE_ELIM2: pf << h << h << h << cs[0]; break; |
522 |
|
// CNF |
523 |
|
case PfRule::CNF_AND_POS: |
524 |
|
case PfRule::CNF_OR_NEG: |
525 |
|
// print second argument as a raw integer (mpz) |
526 |
|
pf << h << as[0] << args[1]; |
527 |
|
break; |
528 |
|
case PfRule::CNF_AND_NEG: pf << h << as[0]; break; |
529 |
|
case PfRule::CNF_OR_POS: |
530 |
|
pf << as[0]; |
531 |
|
break; |
532 |
|
break; |
533 |
|
case PfRule::CNF_IMPLIES_POS: |
534 |
|
case PfRule::CNF_IMPLIES_NEG1: |
535 |
|
case PfRule::CNF_IMPLIES_NEG2: |
536 |
|
case PfRule::CNF_EQUIV_POS1: |
537 |
|
case PfRule::CNF_EQUIV_POS2: |
538 |
|
case PfRule::CNF_EQUIV_NEG1: |
539 |
|
case PfRule::CNF_EQUIV_NEG2: |
540 |
|
case PfRule::CNF_XOR_POS1: |
541 |
|
case PfRule::CNF_XOR_POS2: |
542 |
|
case PfRule::CNF_XOR_NEG1: |
543 |
|
case PfRule::CNF_XOR_NEG2: pf << as[0][0] << as[0][1]; break; |
544 |
|
case PfRule::CNF_ITE_POS1: |
545 |
|
case PfRule::CNF_ITE_POS2: |
546 |
|
case PfRule::CNF_ITE_POS3: |
547 |
|
case PfRule::CNF_ITE_NEG1: |
548 |
|
case PfRule::CNF_ITE_NEG2: |
549 |
|
case PfRule::CNF_ITE_NEG3: pf << as[0][0] << as[0][1] << as[0][2]; break; |
550 |
|
// equality |
551 |
24 |
case PfRule::REFL: pf << as[0]; break; |
552 |
|
case PfRule::SYMM: pf << h << h << cs[0]; break; |
553 |
2 |
case PfRule::TRANS: pf << h << h << h << cs[0] << cs[1]; break; |
554 |
|
case PfRule::TRUE_INTRO: |
555 |
|
case PfRule::FALSE_INTRO: |
556 |
|
case PfRule::TRUE_ELIM: |
557 |
|
case PfRule::FALSE_ELIM: pf << h << cs[0]; break; |
558 |
|
// arithmetic |
559 |
|
case PfRule::ARITH_MULT_POS: |
560 |
|
case PfRule::ARITH_MULT_NEG: |
561 |
|
{ |
562 |
|
pf << h << as[0] << as[1]; |
563 |
|
} |
564 |
|
break; |
565 |
|
case PfRule::ARITH_TRICHOTOMY: |
566 |
|
{ |
567 |
|
// should be robust to different orderings |
568 |
|
pf << h << h << h << cs[0] << cs[1]; |
569 |
|
} |
570 |
|
break; |
571 |
|
// strings |
572 |
|
case PfRule::STRING_LENGTH_POS: pf << as[0]; break; |
573 |
|
case PfRule::STRING_LENGTH_NON_EMPTY: pf << h << cs[0]; break; |
574 |
|
case PfRule::RE_INTER: pf << h << h << h << cs[0] << cs[1]; break; |
575 |
|
case PfRule::CONCAT_EQ: |
576 |
|
pf << h << h << h << args[0].getConst<bool>() << cs[0]; |
577 |
|
break; |
578 |
|
case PfRule::CONCAT_UNIFY: |
579 |
|
pf << h << h << h << h << args[0].getConst<bool>() << cs[0] << cs[1]; |
580 |
|
break; |
581 |
|
case PfRule::CONCAT_CSPLIT: |
582 |
|
pf << h << h << h << h << args[0].getConst<bool>() << cs[0] << cs[1]; |
583 |
|
break; |
584 |
|
break; |
585 |
|
case PfRule::RE_UNFOLD_POS: |
586 |
|
if (children[0]->getResult()[1].getKind() != REGEXP_CONCAT) |
587 |
|
{ |
588 |
|
return false; |
589 |
|
} |
590 |
|
pf << h << h << h << cs[0]; |
591 |
|
break; |
592 |
|
case PfRule::STRING_EAGER_REDUCTION: |
593 |
|
{ |
594 |
|
Kind k = as[0].getKind(); |
595 |
|
if (k == STRING_TO_CODE || k == STRING_CONTAINS || k == STRING_INDEXOF) |
596 |
|
{ |
597 |
|
pf << h << as[0] << as[0][0].getType(); |
598 |
|
} |
599 |
|
else |
600 |
|
{ |
601 |
|
// not yet defined for other kinds |
602 |
|
return false; |
603 |
|
} |
604 |
|
} |
605 |
|
break; |
606 |
|
case PfRule::STRING_REDUCTION: |
607 |
|
{ |
608 |
|
Kind k = as[0].getKind(); |
609 |
|
if (k == STRING_SUBSTR || k == STRING_INDEXOF) |
610 |
|
{ |
611 |
|
pf << h << as[0] << as[0][0].getType(); |
612 |
|
} |
613 |
|
else |
614 |
|
{ |
615 |
|
// not yet defined for other kinds |
616 |
|
return false; |
617 |
|
} |
618 |
|
} |
619 |
|
break; |
620 |
|
// quantifiers |
621 |
|
case PfRule::SKOLEM_INTRO: |
622 |
|
{ |
623 |
|
pf << h << d_tproc.convert(SkolemManager::getOriginalForm(args[0])); |
624 |
|
} |
625 |
|
break; |
626 |
|
// ---------- arguments of non-translated rules go here |
627 |
36 |
case PfRule::LFSC_RULE: |
628 |
|
{ |
629 |
36 |
LfscRule lr = getLfscRule(args[0]); |
630 |
|
// lambda should be processed elsewhere |
631 |
36 |
Assert(lr != LfscRule::LAMBDA); |
632 |
|
// Note that `args` has 2 builtin arguments, thus the first real argument |
633 |
|
// begins at index 2 |
634 |
36 |
switch (lr) |
635 |
|
{ |
636 |
|
case LfscRule::SCOPE: pf << h << as[2] << cs[0]; break; |
637 |
|
case LfscRule::NEG_SYMM: pf << h << h << cs[0]; break; |
638 |
36 |
case LfscRule::CONG: pf << h << h << h << h << cs[0] << cs[1]; break; |
639 |
|
case LfscRule::AND_INTRO1: pf << h << cs[0]; break; |
640 |
|
case LfscRule::NOT_AND_REV: pf << h << h << cs[0]; break; |
641 |
|
case LfscRule::PROCESS_SCOPE: pf << h << h << as[2] << cs[0]; break; |
642 |
|
case LfscRule::AND_INTRO2: pf << h << h << cs[0] << cs[1]; break; |
643 |
|
case LfscRule::ARITH_SUM_UB: pf << h << h << h << cs[0] << cs[1]; break; |
644 |
|
default: return false; break; |
645 |
|
} |
646 |
|
} |
647 |
36 |
break; |
648 |
6 |
default: |
649 |
|
{ |
650 |
6 |
return false; |
651 |
|
break; |
652 |
|
} |
653 |
|
} |
654 |
72 |
return true; |
655 |
|
} |
656 |
|
|
657 |
1 |
void LfscPrinter::computeProofLetification( |
658 |
|
const ProofNode* pn, |
659 |
|
std::vector<const ProofNode*>& pletList, |
660 |
|
std::map<const ProofNode*, size_t>& pletMap) |
661 |
|
{ |
662 |
|
// use callback to specify to stop at LAMBDA |
663 |
1 |
ProofLetify::computeProofLet(pn, pletList, pletMap, 2, &d_lpltc); |
664 |
1 |
} |
665 |
|
|
666 |
|
void LfscPrinter::print(std::ostream& out, Node n) |
667 |
|
{ |
668 |
|
Node ni = d_tproc.convert(n); |
669 |
|
printLetify(out, ni); |
670 |
|
} |
671 |
|
|
672 |
|
void LfscPrinter::printLetify(std::ostream& out, Node n) |
673 |
|
{ |
674 |
|
// closing parentheses |
675 |
|
std::stringstream cparen; |
676 |
|
|
677 |
|
LetBinding lbind; |
678 |
|
lbind.process(n); |
679 |
|
|
680 |
|
// [1] print the letification |
681 |
|
printLetList(out, cparen, lbind); |
682 |
|
|
683 |
|
// [2] print the body |
684 |
|
printInternal(out, n, lbind); |
685 |
|
|
686 |
|
out << cparen.str(); |
687 |
|
} |
688 |
|
|
689 |
1 |
void LfscPrinter::printLetList(std::ostream& out, |
690 |
|
std::ostream& cparen, |
691 |
|
LetBinding& lbind) |
692 |
|
{ |
693 |
2 |
std::vector<Node> letList; |
694 |
1 |
lbind.letify(letList); |
695 |
1 |
std::map<Node, size_t>::const_iterator it; |
696 |
9 |
for (size_t i = 0, nlets = letList.size(); i < nlets; i++) |
697 |
|
{ |
698 |
16 |
Node nl = letList[i]; |
699 |
8 |
out << "(@ "; |
700 |
8 |
size_t id = lbind.getId(nl); |
701 |
8 |
Assert(id != 0); |
702 |
8 |
LfscPrintChannelOut::printId(out, id); |
703 |
8 |
out << " "; |
704 |
|
// remove, print, insert again |
705 |
8 |
printInternal(out, nl, lbind, false); |
706 |
8 |
out << std::endl; |
707 |
8 |
cparen << ")"; |
708 |
|
} |
709 |
1 |
} |
710 |
|
|
711 |
|
void LfscPrinter::printInternal(std::ostream& out, Node n) |
712 |
|
{ |
713 |
|
LetBinding lbind; |
714 |
|
printInternal(out, n, lbind); |
715 |
|
} |
716 |
11 |
void LfscPrinter::printInternal(std::ostream& out, |
717 |
|
Node n, |
718 |
|
LetBinding& lbind, |
719 |
|
bool letTop) |
720 |
|
{ |
721 |
22 |
Node nc = lbind.convert(n, "__t", letTop); |
722 |
11 |
LfscPrintChannelOut::printNodeInternal(out, nc); |
723 |
11 |
} |
724 |
|
|
725 |
6 |
void LfscPrinter::printType(std::ostream& out, TypeNode tn) |
726 |
|
{ |
727 |
12 |
TypeNode tni = d_tproc.convertType(tn); |
728 |
6 |
LfscPrintChannelOut::printTypeNodeInternal(out, tni); |
729 |
6 |
} |
730 |
|
|
731 |
|
} // namespace proof |
732 |
31137 |
} // namespace cvc5 |