Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Hans-Joerg Schurr, Abdalrhman Mohamed
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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 "options/proof_options.h"
26 : : #include "proof/lfsc/lfsc_list_sc_node_converter.h"
27 : : #include "proof/lfsc/lfsc_print_channel.h"
28 : :
29 : : using namespace cvc5::internal::kind;
30 : : using namespace cvc5::internal::rewriter;
31 : :
32 : : namespace cvc5::internal {
33 : : namespace proof {
34 : :
35 : 1696 : LfscPrinter::LfscPrinter(Env& env,
36 : : LfscNodeConverter& ltp,
37 : 1696 : rewriter::RewriteDb* rdb)
38 : : : EnvObj(env),
39 : : d_tproc(ltp),
40 : : d_assumpCounter(0),
41 : : d_trustChildPletCounter(0),
42 : : d_termLetPrefix("t"),
43 : : d_assumpPrefix("a"),
44 : : d_pletPrefix("p"),
45 : : d_pletTrustChildPrefix("q"),
46 : 1696 : d_rdb(rdb)
47 : : {
48 : 1696 : NodeManager* nm = nodeManager();
49 : 1696 : d_boolType = nm->booleanType();
50 : : // used for the `flag` type in LFSC
51 : 1696 : d_tt = d_tproc.mkInternalSymbol("tt", d_boolType);
52 : 1696 : d_ff = d_tproc.mkInternalSymbol("ff", d_boolType);
53 : 1696 : }
54 : :
55 : 1696 : void LfscPrinter::print(std::ostream& out, const ProofNode* pn)
56 : : {
57 [ + - ]: 1696 : Trace("lfsc-print-debug") << "; ORIGINAL PROOF: " << *pn << std::endl;
58 [ - + ][ - + ]: 1696 : Assert (!pn->getChildren().empty());
[ - - ]
59 : : // closing parentheses
60 : 3392 : std::stringstream cparen;
61 : 1696 : const std::vector<Node>& definitions = pn->getArguments();
62 : 3392 : std::unordered_set<Node> definedSymbols;
63 [ + + ]: 2253 : for (const Node& n : definitions)
64 : : {
65 : 557 : definedSymbols.insert(n[0]);
66 : : // Note that we don't have to convert it via the term processor (for the
67 : : // sake of inferring declared symbols), since this is already done in the
68 : : // lfsc post processor update method for the outermost SCOPE.
69 : : }
70 : 1696 : const std::vector<Node>& assertions = pn->getChildren()[0]->getArguments();
71 : 1696 : const ProofNode* pnBody = pn->getChildren()[0]->getChildren()[0].get();
72 : :
73 : : // clear the rules we have warned about
74 : 1696 : d_trustWarned.clear();
75 : :
76 : : // [1] convert assertions to internal and set up assumption map
77 [ + - ]: 1696 : Trace("lfsc-print-debug") << "; print declarations" << std::endl;
78 : 3392 : std::vector<Node> iasserts;
79 : 3392 : std::map<Node, size_t> passumeMap;
80 [ + + ]: 17662 : for (size_t i = 0, nasserts = assertions.size(); i < nasserts; i++)
81 : : {
82 : 15966 : Node a = assertions[i];
83 : 15966 : iasserts.push_back(d_tproc.convert(a));
84 : : // remember the assumption name
85 : 15966 : passumeMap[a] = i;
86 : : }
87 : 1696 : d_assumpCounter = assertions.size();
88 : :
89 : : // [2] compute the proof letification
90 [ + - ]: 1696 : Trace("lfsc-print-debug") << "; compute proof letification" << std::endl;
91 : 3392 : std::vector<const ProofNode*> pletList;
92 : 3392 : std::map<const ProofNode*, size_t> pletMap;
93 : 1696 : computeProofLetification(pnBody, pletList, pletMap);
94 : :
95 : : // [3] compute the global term letification and declared symbols and types
96 [ + - ]: 3392 : Trace("lfsc-print-debug")
97 : 1696 : << "; compute global term letification and declared symbols" << std::endl;
98 : 3392 : LetBinding lbind(d_termLetPrefix);
99 [ + + ]: 17662 : for (const Node& ia : iasserts)
100 : : {
101 : 15966 : lbind.process(ia);
102 : : }
103 : : // We do a "dry-run" of proof printing here, using the LetBinding print
104 : : // channel. This pass traverses the proof but does not print it, but instead
105 : : // updates the let binding data structure for all nodes that appear anywhere
106 : : // in the proof. It is also important for the term processor for collecting
107 : : // symbols and types that are used in the proof.
108 : 3392 : LfscPrintChannelPre lpcp(lbind);
109 : 3392 : LetBinding emptyLetBind(d_termLetPrefix);
110 : 1696 : std::map<const ProofNode*, size_t>::iterator itp;
111 [ + + ]: 142867 : for (const ProofNode* p : pletList)
112 : : {
113 : 141171 : itp = pletMap.find(p);
114 [ - + ][ - + ]: 141171 : Assert(itp != pletMap.end());
[ - - ]
115 : 141171 : size_t pid = itp->second;
116 : 141171 : pletMap.erase(p);
117 : 141171 : printProofInternal(&lpcp, p, emptyLetBind, pletMap, passumeMap);
118 : 141171 : pletMap[p] = pid;
119 : 141171 : Node resType = p->getResult();
120 : 141171 : lbind.process(d_tproc.convert(resType));
121 : : }
122 : : // Print the body of the outermost scope
123 : 1696 : printProofInternal(&lpcp, pnBody, emptyLetBind, pletMap, passumeMap);
124 : :
125 : : // [4] print declared sorts and symbols
126 : : // [4a] user declare function symbols
127 : : // Note that this is buffered into an output stream preambleSymDecl and then
128 : : // printed after types. We require printing the declared symbols here so that
129 : : // the set of collected declared types is complete at [4b].
130 [ + - ]: 1696 : Trace("lfsc-print-debug") << "; print user symbols" << std::endl;
131 : 3392 : std::stringstream preambleSymDecl;
132 : 1696 : const std::unordered_set<Node>& syms = d_tproc.getDeclaredSymbols();
133 [ + + ]: 17859 : for (const Node& s : syms)
134 : : {
135 : 16163 : TypeNode st = s.getType();
136 [ + - ]: 32326 : if (st.isDatatypeConstructor() || st.isDatatypeSelector()
137 [ + - ][ + - ]: 16163 : || st.isDatatypeTester() || st.isDatatypeUpdater()
138 [ + - ][ + + ]: 32326 : || definedSymbols.find(s) != definedSymbols.cend())
[ + + ]
139 : : {
140 : : // Constructors, selector, testers, updaters are defined by the datatype.
141 : : // Some definitions depend on declarations and other definitions. So, we
142 : : // print them in order after declarations.
143 : 557 : continue;
144 : : }
145 : 31212 : Node si = d_tproc.convert(s);
146 : 15606 : preambleSymDecl << "(define " << si << " (var "
147 : 15606 : << d_tproc.getOrAssignIndexForFVar(s) << " ";
148 : 15606 : printType(preambleSymDecl, st);
149 : 15606 : preambleSymDecl << "))" << std::endl;
150 : : }
151 : : // Note that definitions always use their own internal letification, since
152 : : // their bodies are not part of the main proof. It is possible to share term
153 : : // letification via global definitions, however, this requires further
154 : : // analysis to ensure symbols are printed in the correct order. This is
155 : : // not done for simplicity.
156 [ + + ]: 2253 : for (const Node& def : definitions)
157 : : {
158 : 1114 : Node si = d_tproc.convert(def[0]);
159 : 557 : preambleSymDecl << "(define " << si << ' ';
160 : 557 : print(preambleSymDecl, def[1]);
161 : 557 : preambleSymDecl << ')' << std::endl;
162 : : }
163 : : // [4b] user declared sorts
164 [ + - ]: 1696 : Trace("lfsc-print-debug") << "; print user sorts" << std::endl;
165 : 3392 : std::stringstream preamble;
166 : 3392 : std::unordered_set<TypeNode> sts;
167 : 3392 : std::unordered_set<size_t> tupleArity;
168 : : // get the types from the term processor, which has seen all terms occurring
169 : : // in the proof at this point
170 : : // The for loop below may add elements to the set of declared types, so we
171 : : // copy the set to ensure that the for loop iterators do not become outdated.
172 : 3392 : const std::unordered_set<TypeNode> types = d_tproc.getDeclaredTypes();
173 [ + + ]: 4862 : for (const TypeNode& st : types)
174 : : {
175 : : // note that we must get all "component types" of a type, so that
176 : : // e.g. U is printed as a sort declaration when we have type (Array U Int).
177 : 3166 : ensureTypeDefinitionPrinted(preamble, st, sts, tupleArity);
178 : : }
179 : : // print datatype definitions for the above sorts
180 [ + + ]: 4940 : for (const TypeNode& stc : sts)
181 : : {
182 [ + + ][ + + ]: 3244 : if (!stc.isDatatype() || stc.getKind() == Kind::PARAMETRIC_DATATYPE)
[ + + ]
183 : : {
184 : : // skip the instance of a parametric datatype
185 : 2811 : continue;
186 : : }
187 : 433 : const DType& dt = stc.getDType();
188 : 433 : preamble << "; DATATYPE " << dt.getName() << std::endl;
189 [ + + ]: 1145 : for (size_t i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
190 : : {
191 : 712 : const DTypeConstructor& cons = dt[i];
192 : 1424 : std::string cname = d_tproc.getNameForUserNameOf(cons.getConstructor());
193 : 1424 : Node cc = NodeManager::mkRawSymbol(cname, stc);
194 : : // print constructor/tester
195 : 712 : preamble << "(declare " << cc << " term)" << std::endl;
196 [ + + ]: 1489 : for (size_t j = 0, nargs = cons.getNumArgs(); j < nargs; j++)
197 : : {
198 : 777 : const DTypeSelector& arg = cons[j];
199 : : // print selector
200 : 1554 : std::string sname = d_tproc.getNameForUserNameOf(arg.getSelector());
201 : 777 : Node sc = NodeManager::mkRawSymbol(sname, stc);
202 : 777 : preamble << "(declare " << sc << " term)" << std::endl;
203 : : }
204 : : }
205 : : // testers and updaters are instances of parametric symbols
206 : : // shared selectors are instance of parametric symbol "sel"
207 : 433 : preamble << "; END DATATYPE " << std::endl;
208 : : }
209 : : // [4c] user declared function symbols
210 : 1696 : preamble << preambleSymDecl.str();
211 : :
212 : : // [5] print warnings
213 [ + + ]: 5292 : for (ProofRule r : d_trustWarned)
214 : : {
215 : 3596 : out << "; WARNING: adding trust step for " << r << std::endl;
216 : : }
217 : :
218 : : // [6] print the DSL rewrite rule declarations
219 : 1696 : const std::unordered_set<ProofRewriteRule>& dslrs = lpcp.getDslRewrites();
220 [ + + ]: 1698 : for (ProofRewriteRule dslr : dslrs)
221 : : {
222 : : // also computes the format for the rule
223 : 2 : printDslRule(out, dslr, d_dslFormat[dslr]);
224 : : }
225 : :
226 : : // [7] print the check command and term lets
227 : 1696 : out << preamble.str();
228 [ + + ]: 1696 : if (options().proof.lfscFlatten)
229 : : {
230 : : // print term lets as definitions
231 : 2 : std::stringstream cparenTmp;
232 : 1 : printLetList(out, cparenTmp, lbind, true);
233 : : }
234 : : else
235 : : {
236 : : // the outer check statement for the main proof
237 : 1695 : out << "(check" << std::endl;
238 : 1695 : cparen << ")";
239 : : // print the term let list wrapped around the body of the final proof
240 : 1695 : printLetList(out, cparen, lbind, false);
241 : : }
242 : :
243 [ + - ]: 1696 : Trace("lfsc-print-debug") << "; print asserts" << std::endl;
244 : : // [8] print the assertions, with letification
245 : : // the assumption identifier mapping
246 [ + + ]: 17662 : for (size_t i = 0, nasserts = iasserts.size(); i < nasserts; i++)
247 : : {
248 : 31932 : Node ia = iasserts[i];
249 [ + + ]: 15966 : if (options().proof.lfscFlatten)
250 : : {
251 : 1 : out << "(declare ";
252 : 1 : LfscPrintChannelOut::printId(out, i, d_assumpPrefix);
253 : 1 : out << " (holds ";
254 : 1 : printInternal(out, ia, lbind);
255 : 1 : out << "))" << std::endl;
256 : : }
257 : : else
258 : : {
259 : 15965 : out << "(# ";
260 : 15965 : LfscPrintChannelOut::printId(out, i, d_assumpPrefix);
261 : 15965 : out << " (holds ";
262 : 15965 : printInternal(out, ia, lbind);
263 : 15965 : out << ")" << std::endl;
264 : 15965 : cparen << ")";
265 : : }
266 : : }
267 : :
268 [ + - ]: 1696 : Trace("lfsc-print-debug") << "; print annotation" << std::endl;
269 : : // [9] print the annotation
270 [ + + ]: 1696 : if (!options().proof.lfscFlatten)
271 : : {
272 : 1695 : out << "(: (holds false)" << std::endl;
273 : 1695 : cparen << ")";
274 : : }
275 : :
276 [ + - ]: 1696 : Trace("lfsc-print-debug") << "; print proof body" << std::endl;
277 : : // [10] print the proof body
278 [ - + ][ - + ]: 1696 : Assert(pn->getRule() == ProofRule::SCOPE);
[ - - ]
279 : : // the outermost scope can be ignored (it is the scope of the assertions,
280 : : // which are already printed above).
281 : 1696 : LfscPrintChannelOut lout(out);
282 : :
283 [ + + ]: 1696 : if (options().proof.lfscFlatten)
284 : : {
285 : : // print the proof letification as separate check statements, followed
286 : : // by the main proof.
287 [ + + ]: 7 : for (size_t i = 0; i <= pletList.size(); i++)
288 : : {
289 : 6 : bool isFinal = (i == pletList.size());
290 [ + + ]: 6 : const ProofNode* p = isFinal ? pnBody : pletList[i];
291 : 12 : Node res = p->getResult();
292 : 12 : std::stringstream resType;
293 : 6 : printInternal(resType, d_tproc.convert(res), lbind);
294 : 6 : out << "(check (: (holds " << resType.str() << ")" << std::endl;
295 : : // print the letified proof
296 [ + + ]: 6 : if (isFinal)
297 : : {
298 : 1 : printProofInternal(&lout, p, lbind, pletMap, passumeMap);
299 : 1 : out << "))" << std::endl;
300 : : }
301 : : else
302 : : {
303 : 5 : itp = pletMap.find(p);
304 [ - + ][ - + ]: 5 : Assert(itp != pletMap.end());
[ - - ]
305 : 5 : size_t pid = itp->second;
306 : 5 : pletMap.erase(p);
307 : 5 : printProofInternal(&lout, p, lbind, pletMap, passumeMap);
308 : 5 : pletMap[p] = pid;
309 : 5 : out << "))" << std::endl;
310 : 5 : out << "(declare ";
311 : 5 : LfscPrintChannelOut::printId(out, pid, d_pletPrefix);
312 : 5 : out << " (holds " << resType.str() << "))" << std::endl;
313 : : }
314 : : }
315 : : }
316 : : else
317 : : {
318 : 1695 : printProofLetify(&lout, pnBody, lbind, pletList, pletMap, passumeMap);
319 : : }
320 : : // [11] print closing parantheses
321 : 1696 : out << cparen.str() << std::endl;
322 : 1696 : }
323 : :
324 : 3729 : void LfscPrinter::ensureTypeDefinitionPrinted(
325 : : std::ostream& os,
326 : : TypeNode tn,
327 : : std::unordered_set<TypeNode>& processed,
328 : : std::unordered_set<size_t>& tupleArityProcessed)
329 : : {
330 : : // note that we must get all "component types" of a type, so that
331 : : // e.g. U is printed as a sort declaration when we have type (Array U Int).
332 : 7458 : std::unordered_set<TypeNode> ctypes;
333 : 3729 : expr::getComponentTypes(tn, ctypes);
334 : :
335 [ + + ]: 7611 : for (const TypeNode& stc : ctypes)
336 : : {
337 : 3882 : printTypeDefinition(os, stc, processed, tupleArityProcessed);
338 : : }
339 : 3729 : }
340 : :
341 : 3882 : void LfscPrinter::printTypeDefinition(
342 : : std::ostream& os,
343 : : TypeNode tn,
344 : : std::unordered_set<TypeNode>& processed,
345 : : std::unordered_set<size_t>& tupleArityProcessed)
346 : : {
347 [ + + ]: 3882 : if (processed.find(tn) != processed.end())
348 : : {
349 : 638 : return;
350 : : }
351 : 3244 : processed.insert(tn);
352 : : // print uninterpreted sorts and uninterpreted sort constructors here
353 [ + + ]: 3244 : if (tn.getKind() == Kind::SORT_TYPE)
354 : : {
355 : 1210 : os << "(declare ";
356 : 1210 : printType(os, tn);
357 : 1210 : uint64_t arity = 0;
358 [ + + ]: 1210 : if (tn.isUninterpretedSortConstructor())
359 : : {
360 : 11 : arity = tn.getUninterpretedSortConstructorArity();
361 : : }
362 : 1210 : std::stringstream tcparen;
363 [ + + ]: 1222 : for (uint64_t i = 0; i < arity; i++)
364 : : {
365 : 12 : os << " (! s" << i << " sort";
366 : 12 : tcparen << ")";
367 : : }
368 : 1210 : os << " sort" << tcparen.str() << ")" << std::endl;
369 : : }
370 [ + + ]: 2034 : else if (tn.isDatatype())
371 : : {
372 : 442 : const DType& dt = tn.getDType();
373 [ + + ][ + + ]: 442 : if (tn.getKind() == Kind::PARAMETRIC_DATATYPE || dt.isNullable())
[ + + ]
374 : : {
375 : : // skip the instance of a parametric datatype
376 : : // nullables don't need printing
377 : 12 : return;
378 : : }
379 [ + + ]: 430 : if (dt.isTuple())
380 : : {
381 : 88 : const DTypeConstructor& cons = dt[0];
382 : 88 : size_t arity = cons.getNumArgs();
383 [ + + ]: 88 : if (tupleArityProcessed.find(arity) == tupleArityProcessed.end())
384 : : {
385 : 84 : tupleArityProcessed.insert(arity);
386 [ + + ]: 84 : if (arity>0)
387 : : {
388 : 83 : os << "(declare Tuple";
389 : 83 : os << "_" << arity;
390 : : }
391 : : else
392 : : {
393 : 1 : os << "(declare UnitTuple";
394 : : }
395 : 84 : os << " ";
396 : 84 : std::stringstream tcparen;
397 [ + + ]: 270 : for (size_t j = 0, nargs = cons.getNumArgs(); j < nargs; j++)
398 : : {
399 : 186 : os << "(! s" << j << " sort ";
400 : 186 : tcparen << ")";
401 : : }
402 : 84 : os << "sort" << tcparen.str() << ")";
403 : : }
404 : 88 : os << std::endl;
405 : : }
406 : : else
407 : : {
408 : 342 : os << "(declare ";
409 : 342 : printType(os, tn);
410 : 342 : std::stringstream cdttparens;
411 [ + + ]: 342 : if (dt.isParametric())
412 : : {
413 : 18 : std::vector<TypeNode> params = dt.getParameters();
414 [ + + ]: 20 : for (const TypeNode& p : params)
415 : : {
416 : 11 : os << " (! " << p << " sort";
417 : 11 : cdttparens << ")";
418 : : }
419 : : }
420 : 342 : os << " sort)" << cdttparens.str() << std::endl;
421 : : }
422 : : // must also ensure the subfield types of the datatype are printed
423 : 860 : std::unordered_set<TypeNode> sftypes = dt.getSubfieldTypes();
424 [ + + ]: 993 : for (const TypeNode& sft : sftypes)
425 : : {
426 : 563 : ensureTypeDefinitionPrinted(os, sft, processed, tupleArityProcessed);
427 : : }
428 : : }
429 : : // all other sorts are builtin into the LFSC signature
430 : : }
431 : :
432 : 411707 : void LfscPrinter::printProofLetify(
433 : : LfscPrintChannel* out,
434 : : const ProofNode* pn,
435 : : const LetBinding& lbind,
436 : : const std::vector<const ProofNode*>& pletList,
437 : : std::map<const ProofNode*, size_t>& pletMap,
438 : : std::map<Node, size_t>& passumeMap)
439 : : {
440 : : // closing parentheses
441 : 411707 : size_t cparen = 0;
442 : :
443 : : // define the let proofs
444 [ + + ]: 411707 : if (!pletList.empty())
445 : : {
446 : 45913 : std::map<const ProofNode*, size_t>::iterator itp;
447 [ + + ]: 1401950 : for (const ProofNode* p : pletList)
448 : : {
449 : 1356040 : itp = pletMap.find(p);
450 [ - + ][ - + ]: 1356040 : Assert(itp != pletMap.end());
[ - - ]
451 : 1356040 : size_t pid = itp->second;
452 : 1356040 : pletMap.erase(p);
453 : 1356040 : printPLet(out, p, pid, d_pletPrefix, lbind, pletMap, passumeMap);
454 : 1356040 : pletMap[p] = pid;
455 : : // printPLet opens two parentheses
456 : 1356040 : cparen = cparen + 2;
457 : : }
458 : 45913 : out->printEndLine();
459 : : }
460 : :
461 : : // [2] print the proof body
462 : 411707 : printProofInternal(out, pn, lbind, pletMap, passumeMap);
463 : :
464 : : // print the closing parenthesis
465 : 411707 : out->printCloseRule(cparen);
466 : 411707 : }
467 : :
468 : 1356040 : void LfscPrinter::printPLet(LfscPrintChannel* out,
469 : : const ProofNode* p,
470 : : size_t pid,
471 : : const std::string& prefix,
472 : : const LetBinding& lbind,
473 : : const std::map<const ProofNode*, size_t>& pletMap,
474 : : std::map<Node, size_t>& passumeMap)
475 : : {
476 : : // print (plet _ _
477 : 1356040 : out->printOpenLfscRule(LfscRule::PLET);
478 : 1356040 : out->printHole();
479 : 1356040 : out->printHole();
480 : 1356040 : out->printEndLine();
481 : : // print the letified proof
482 : 1356040 : printProofInternal(out, p, lbind, pletMap, passumeMap);
483 : : // print the lambda (\ __pX
484 : 1356040 : out->printOpenLfscRule(LfscRule::LAMBDA);
485 : 1356040 : out->printId(pid, prefix);
486 : 1356040 : out->printEndLine();
487 : 1356040 : }
488 : :
489 : 1910620 : void LfscPrinter::printProofInternal(
490 : : LfscPrintChannel* out,
491 : : const ProofNode* pn,
492 : : const LetBinding& lbind,
493 : : const std::map<const ProofNode*, size_t>& pletMap,
494 : : std::map<Node, size_t>& passumeMap)
495 : : {
496 : : // the stack
497 : 3821240 : std::vector<PExpr> visit;
498 : : // whether we have to process children
499 : 3821240 : std::unordered_set<const ProofNode*> processingChildren;
500 : : // helper iterators
501 : 1910620 : std::unordered_set<const ProofNode*>::iterator pit;
502 : 1910620 : std::map<const ProofNode*, size_t>::const_iterator pletIt;
503 : 1910620 : std::map<Node, size_t>::iterator passumeIt;
504 : 3821240 : Node curn;
505 : 3821240 : TypeNode curtn;
506 : : const ProofNode* cur;
507 : 1910620 : visit.push_back(PExpr(pn));
508 : 76668800 : do
509 : : {
510 : 78579500 : curn = visit.back().d_node;
511 : 78579500 : curtn = visit.back().d_typeNode;
512 : 78579500 : cur = visit.back().d_pnode;
513 : 78579500 : visit.pop_back();
514 : : // case 1: printing a proof
515 [ + + ]: 78579500 : if (cur != nullptr)
516 : : {
517 : 35981100 : ProofRule r = cur->getRule();
518 : : // maybe it is letified
519 : 35981100 : pletIt = pletMap.find(cur);
520 [ + + ]: 35981100 : if (pletIt != pletMap.end())
521 : : {
522 : : // a letified proof
523 : 4985310 : out->printId(pletIt->second, d_pletPrefix);
524 : 4985310 : continue;
525 : : }
526 : 30995800 : pit = processingChildren.find(cur);
527 [ + + ]: 30995800 : if (pit == processingChildren.end())
528 : : {
529 : 16573300 : bool isLambda = false;
530 [ + + ]: 16573300 : if (r == ProofRule::LFSC_RULE)
531 : : {
532 [ - + ][ - + ]: 8093190 : Assert(!cur->getArguments().empty());
[ - - ]
533 : 8093190 : LfscRule lr = getLfscRule(cur->getArguments()[0]);
534 : 8093190 : isLambda = (lr == LfscRule::LAMBDA);
535 : : }
536 [ + + ]: 16573300 : if (r == ProofRule::ASSUME)
537 : : {
538 : : // an assumption, must have a name
539 : 573000 : passumeIt = passumeMap.find(cur->getResult());
540 [ - + ][ - + ]: 573000 : Assert(passumeIt != passumeMap.end());
[ - - ]
541 : 573000 : out->printId(passumeIt->second, d_assumpPrefix);
542 : : }
543 [ + + ]: 16000300 : else if (isLambda)
544 : : {
545 [ - + ][ - + ]: 410012 : Assert(cur->getArguments().size() == 3);
[ - - ]
546 : : // lambdas are handled specially. We print in a self contained way
547 : : // here.
548 : : // allocate an assumption, if necessary
549 : : size_t pid;
550 : 820024 : Node assumption = cur->getArguments()[2];
551 : 410012 : passumeIt = passumeMap.find(assumption);
552 [ + + ]: 410012 : if (passumeIt == passumeMap.end())
553 : : {
554 : 23551 : pid = d_assumpCounter;
555 : 23551 : d_assumpCounter++;
556 : 23551 : passumeMap[assumption] = pid;
557 : : }
558 : : else
559 : : {
560 : 386461 : pid = passumeIt->second;
561 : : }
562 : : // make the node whose name is the assumption id, where notice that
563 : : // the type of this node does not matter
564 : 820024 : std::stringstream pidNodeName;
565 : 410012 : LfscPrintChannelOut::printId(pidNodeName, pid, d_assumpPrefix);
566 : : // must be an internal symbol so that it is not turned into (bvar ...)
567 : : Node pidNode =
568 : 1230040 : d_tproc.mkInternalSymbol(pidNodeName.str(), d_boolType);
569 : : // print "(\ "
570 : 410012 : out->printOpenRule(cur);
571 : : // print the identifier
572 : 410012 : out->printNode(pidNode);
573 : : // Print the body of the proof with a fresh proof letification. We can
574 : : // keep the assumption map and the let binding (for terms).
575 : 820024 : std::vector<const ProofNode*> pletListNested;
576 : 820024 : std::map<const ProofNode*, size_t> pletMapNested;
577 : 410012 : const ProofNode* curBody = cur->getChildren()[0].get();
578 : 410012 : computeProofLetification(curBody, pletListNested, pletMapNested);
579 : 410012 : printProofLetify(
580 : : out, curBody, lbind, pletListNested, pletMapNested, passumeMap);
581 : : // print ")"
582 : 410012 : out->printCloseRule();
583 : : }
584 : : else
585 : : {
586 : : // assert that we should traverse cur when letifying
587 [ - + ][ - + ]: 15590300 : Assert(d_lpltc.shouldTraverse(cur));
[ - - ]
588 : : // a normal rule application, compute the proof arguments, which
589 : : // notice in the case of PI also may modify our passumeMap.
590 : 31180600 : std::vector<PExpr> args;
591 [ + + ]: 15590300 : if (computeProofArgs(cur, args))
592 : : {
593 : 14422500 : processingChildren.insert(cur);
594 : : // will revisit this proof node to close parentheses
595 : 14422500 : visit.push_back(PExpr(cur));
596 : 14422500 : std::reverse(args.begin(), args.end());
597 : 14422500 : visit.insert(visit.end(), args.begin(), args.end());
598 : : // print the rule name
599 : 14422500 : out->printOpenRule(cur);
600 : : }
601 : : else
602 : : {
603 : : // Could not print the rule, trust for now.
604 : : // If we are expanding trusted steps, its children are printed as
605 : : // plet applications that wrap this term, so that all subproofs are
606 : : // recorded in the proof.
607 : 1167820 : size_t cparenTrustChild = 0;
608 [ + + ]: 1167820 : if (options().proof.lfscExpandTrust)
609 : : {
610 : : const std::vector<std::shared_ptr<ProofNode>>& children =
611 : 22 : cur->getChildren();
612 [ - + ]: 22 : for (const std::shared_ptr<ProofNode>& c : children)
613 : : {
614 : 0 : size_t pid = d_trustChildPletCounter;
615 : 0 : d_trustChildPletCounter++;
616 : 0 : printPLet(out,
617 : 0 : c.get(),
618 : : pid,
619 : 0 : d_pletTrustChildPrefix,
620 : : lbind,
621 : : pletMap,
622 : : passumeMap);
623 : 0 : cparenTrustChild = cparenTrustChild + 2;
624 : : }
625 : : }
626 : 2335640 : Node res = d_tproc.convert(cur->getResult());
627 : 1167820 : res = lbind.convert(res, true);
628 : 1167820 : out->printTrust(res, r);
629 : 1167820 : d_trustWarned.insert(r);
630 : 1167820 : out->printCloseRule(cparenTrustChild);
631 : : }
632 : : }
633 : : }
634 : : else
635 : : {
636 : 14422500 : processingChildren.erase(cur);
637 : 14422500 : out->printCloseRule();
638 : : }
639 : : }
640 : : // case 2: printing a node
641 [ + + ]: 42598300 : else if (!curn.isNull())
642 : : {
643 : : // it has already been converted to internal form, we letify it here
644 : 6420690 : Node curni = lbind.convert(curn, true);
645 : 6420690 : out->printNode(curni);
646 : : }
647 : : // case 3: printing a type node
648 [ + + ]: 36177600 : else if (!curtn.isNull())
649 : : {
650 : 40192 : out->printTypeNode(curtn);
651 : : }
652 : : // case 4: a hole
653 : : else
654 : : {
655 : 36137400 : out->printHole();
656 : : }
657 [ + + ]: 78579500 : } while (!visit.empty());
658 : 1910620 : }
659 : :
660 : 15590300 : bool LfscPrinter::computeProofArgs(const ProofNode* pn,
661 : : std::vector<PExpr>& pargs)
662 : : {
663 : 15590300 : const std::vector<std::shared_ptr<ProofNode>>& children = pn->getChildren();
664 : 31180600 : std::vector<const ProofNode*> cs;
665 [ + + ]: 35252700 : for (const std::shared_ptr<ProofNode>& c : children)
666 : : {
667 : 19662300 : cs.push_back(c.get());
668 : : }
669 : 15590300 : ProofRule r = pn->getRule();
670 : 15590300 : const std::vector<Node>& args = pn->getArguments();
671 : 31180600 : std::vector<Node> as;
672 [ + + ]: 40751900 : for (const Node& a : args)
673 : : {
674 : 50323100 : Node ac = d_tproc.convert(a);
675 : 25161600 : Assert(!ac.isNull()) << "Could not convert " << a << " in " << r;
676 : 25161600 : as.push_back(ac);
677 : : }
678 : : // The proof expression stream, which packs the next expressions (proofs,
679 : : // terms, sorts, LFSC datatypes) into a print-expression vector pargs. This
680 : : // stream can be used via "pf << e" which appends an expression to the
681 : : // vector maintained by this stream.
682 : 46771000 : PExprStream pf(pargs, d_tt, d_ff);
683 : : // hole
684 : 31180600 : PExpr h;
685 [ + - ]: 31180600 : Trace("lfsc-print-debug2")
686 : 0 : << "Compute proof args " << r << " #children= " << cs.size()
687 : 15590300 : << " #args=" << as.size() << std::endl;
688 [ + + ][ + + ]: 15590300 : switch (r)
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
689 : : {
690 : : // SAT
691 : 792490 : case ProofRule::RESOLUTION:
692 : 792490 : pf << h << h << h << cs[0] << cs[1] << args[0].getConst<bool>() << as[1];
693 : 792490 : break;
694 : 120224 : case ProofRule::REORDERING: pf << h << as[0] << cs[0]; break;
695 : 139732 : case ProofRule::FACTORING: pf << h << h << cs[0]; break;
696 : : // Boolean
697 : 34 : case ProofRule::SPLIT: pf << as[0]; break;
698 : 1694 : case ProofRule::NOT_NOT_ELIM: pf << h << cs[0]; break;
699 : 5144 : case ProofRule::CONTRA: pf << h << cs[0] << cs[1]; break;
700 : 260622 : case ProofRule::MODUS_PONENS:
701 : 260622 : case ProofRule::EQ_RESOLVE: pf << h << h << cs[0] << cs[1]; break;
702 : 14650 : case ProofRule::NOT_AND: pf << h << h << cs[0]; break;
703 : 235142 : case ProofRule::NOT_OR_ELIM:
704 : 235142 : case ProofRule::AND_ELIM: pf << h << h << args[0] << cs[0]; break;
705 : 45708 : case ProofRule::IMPLIES_ELIM:
706 : : case ProofRule::NOT_IMPLIES_ELIM1:
707 : : case ProofRule::NOT_IMPLIES_ELIM2:
708 : : case ProofRule::EQUIV_ELIM1:
709 : : case ProofRule::EQUIV_ELIM2:
710 : : case ProofRule::NOT_EQUIV_ELIM1:
711 : : case ProofRule::NOT_EQUIV_ELIM2:
712 : : case ProofRule::XOR_ELIM1:
713 : : case ProofRule::XOR_ELIM2:
714 : : case ProofRule::NOT_XOR_ELIM1:
715 : 45708 : case ProofRule::NOT_XOR_ELIM2: pf << h << h << cs[0]; break;
716 : 5180 : case ProofRule::ITE_ELIM1:
717 : : case ProofRule::ITE_ELIM2:
718 : : case ProofRule::NOT_ITE_ELIM1:
719 : 5180 : case ProofRule::NOT_ITE_ELIM2: pf << h << h << h << cs[0]; break;
720 : : // CNF
721 : 27354 : case ProofRule::CNF_AND_POS:
722 : : case ProofRule::CNF_OR_NEG:
723 : : // print second argument as a raw integer (mpz)
724 : 27354 : pf << h << as[0] << args[1];
725 : 27354 : break;
726 : 22222 : case ProofRule::CNF_AND_NEG: pf << h << as[0]; break;
727 : 5078 : case ProofRule::CNF_OR_POS:
728 : 5078 : pf << as[0];
729 : 5078 : break;
730 : : break;
731 : 10458 : case ProofRule::CNF_IMPLIES_POS:
732 : : case ProofRule::CNF_IMPLIES_NEG1:
733 : : case ProofRule::CNF_IMPLIES_NEG2:
734 : : case ProofRule::CNF_EQUIV_POS1:
735 : : case ProofRule::CNF_EQUIV_POS2:
736 : : case ProofRule::CNF_EQUIV_NEG1:
737 : : case ProofRule::CNF_EQUIV_NEG2:
738 : : case ProofRule::CNF_XOR_POS1:
739 : : case ProofRule::CNF_XOR_POS2:
740 : : case ProofRule::CNF_XOR_NEG1:
741 : 10458 : case ProofRule::CNF_XOR_NEG2: pf << as[0][0] << as[0][1]; break;
742 : 2878 : case ProofRule::CNF_ITE_POS1:
743 : : case ProofRule::CNF_ITE_POS2:
744 : : case ProofRule::CNF_ITE_POS3:
745 : : case ProofRule::CNF_ITE_NEG1:
746 : : case ProofRule::CNF_ITE_NEG2:
747 : 2878 : case ProofRule::CNF_ITE_NEG3: pf << as[0][0] << as[0][1] << as[0][2]; break;
748 : : // equality
749 : 3725870 : case ProofRule::REFL: pf << as[0]; break;
750 : 184408 : case ProofRule::SYMM: pf << h << h << cs[0]; break;
751 : 968750 : case ProofRule::TRANS: pf << h << h << h << cs[0] << cs[1]; break;
752 : 54234 : case ProofRule::TRUE_INTRO:
753 : : case ProofRule::FALSE_INTRO:
754 : : case ProofRule::TRUE_ELIM:
755 : 54234 : case ProofRule::FALSE_ELIM: pf << h << cs[0]; break;
756 : : // arithmetic
757 : 32506 : case ProofRule::ARITH_MULT_POS:
758 : : case ProofRule::ARITH_MULT_NEG:
759 : : {
760 : 32506 : pf << h << as[0] << as[1] << d_tproc.convertType(as[0].getType());
761 : : }
762 : 32506 : break;
763 : 2756 : case ProofRule::ARITH_TRICHOTOMY:
764 : : {
765 : : // should be robust to different orderings
766 : 2756 : pf << h << h << h << cs[0] << cs[1];
767 : : }
768 : 2756 : break;
769 : 4550 : case ProofRule::INT_TIGHT_UB:
770 : : case ProofRule::INT_TIGHT_LB:
771 : : {
772 : 4550 : Node res = pn->getResult();
773 [ - + ][ - + ]: 4550 : Assert(res.getNumChildren() == 2);
[ - - ]
774 [ - + ][ - + ]: 4550 : Assert(res[1].isConst());
[ - - ]
775 : 4550 : pf << h << h << d_tproc.convert(res[1]) << cs[0];
776 : : }
777 : 4550 : break;
778 : : // strings
779 : 972 : case ProofRule::STRING_LENGTH_POS:
780 : 972 : pf << as[0] << d_tproc.convertType(as[0].getType()) << h;
781 : 972 : break;
782 : 204 : case ProofRule::STRING_LENGTH_NON_EMPTY: pf << h << h << cs[0]; break;
783 : 14 : case ProofRule::RE_INTER: pf << h << h << h << cs[0] << cs[1]; break;
784 : 764 : case ProofRule::CONCAT_EQ:
785 : 1528 : pf << h << h << h << args[0].getConst<bool>()
786 : 764 : << d_tproc.convertType(children[0]->getResult()[0].getType()) << cs[0];
787 : 764 : break;
788 : 664 : case ProofRule::CONCAT_UNIFY:
789 : 1328 : pf << h << h << h << h << args[0].getConst<bool>()
790 : 1328 : << d_tproc.convertType(children[0]->getResult()[0].getType()) << cs[0]
791 : 664 : << cs[1];
792 : 664 : break;
793 : 300 : case ProofRule::CONCAT_CSPLIT:
794 : 600 : pf << h << h << h << h << args[0].getConst<bool>()
795 : 600 : << d_tproc.convertType(children[0]->getResult()[0].getType()) << cs[0]
796 : 300 : << cs[1];
797 : 300 : break;
798 : 864 : case ProofRule::RE_UNFOLD_POS:
799 [ + + ]: 864 : if (children[0]->getResult()[1].getKind() != Kind::REGEXP_CONCAT)
800 : : {
801 : 48 : return false;
802 : : }
803 : 816 : pf << h << h << h << cs[0];
804 : 816 : break;
805 : 808 : case ProofRule::STRING_EAGER_REDUCTION:
806 : : {
807 : 808 : Kind k = as[0].getKind();
808 [ + + ][ + + ]: 808 : if (k == Kind::STRING_TO_CODE || k == Kind::STRING_CONTAINS
809 [ + + ]: 150 : || k == Kind::STRING_INDEXOF)
810 : : {
811 : 768 : pf << h << as[0] << as[0][0].getType();
812 : : }
813 : : else
814 : : {
815 : : // not yet defined for other kinds
816 : 40 : return false;
817 : : }
818 : : }
819 : 768 : break;
820 : 6820 : case ProofRule::STRING_REDUCTION:
821 : : {
822 : 6820 : Kind k = as[0].getKind();
823 [ + + ][ + + ]: 6820 : if (k == Kind::STRING_SUBSTR || k == Kind::STRING_INDEXOF)
824 : : {
825 : 4218 : pf << h << as[0] << d_tproc.convertType(as[0][0].getType());
826 : : }
827 : : else
828 : : {
829 : : // not yet defined for other kinds
830 : 2602 : return false;
831 : : }
832 : : }
833 : 4218 : break;
834 : : // quantifiers
835 : 68906 : case ProofRule::SKOLEM_INTRO:
836 : : {
837 : 68906 : pf << d_tproc.convert(SkolemManager::getUnpurifiedForm(args[0]));
838 : : }
839 : 68906 : break;
840 : : // ---------- arguments of non-translated rules go here
841 : 7683180 : case ProofRule::LFSC_RULE:
842 : : {
843 : 7683180 : LfscRule lr = getLfscRule(args[0]);
844 : : // lambda should be processed elsewhere
845 : 7683180 : Assert(lr != LfscRule::LAMBDA);
846 : : // Note that `args` has 2 builtin arguments, thus the first real argument
847 : : // begins at index 2
848 : : switch (lr)
849 : : {
850 : 4798 : case LfscRule::DEFINITION: pf << as[1][0]; break;
851 : 410012 : case LfscRule::SCOPE: pf << h << as[2] << cs[0]; break;
852 : 684 : case LfscRule::NEG_SYMM: pf << h << h << cs[0]; break;
853 : 6913330 : case LfscRule::CONG: pf << h << h << h << h << cs[0] << cs[1]; break;
854 : 67524 : case LfscRule::AND_INTRO1: pf << h << cs[0]; break;
855 : 17402 : case LfscRule::NOT_AND_REV: pf << h << h << cs[0]; break;
856 : 70056 : case LfscRule::PROCESS_SCOPE: pf << h << h << as[2] << cs[0]; break;
857 : 135210 : case LfscRule::AND_INTRO2: pf << h << h << cs[0] << cs[1]; break;
858 : 52310 : case LfscRule::ARITH_SUM_UB: pf << h << h << h << cs[0] << cs[1]; break;
859 : 11850 : case LfscRule::INSTANTIATE:
860 : 11850 : pf << h << h << h << h << as[2] << cs[0];
861 : 11850 : break;
862 : 0 : case LfscRule::BETA_REDUCE: pf << h << as[2]; break;
863 : 0 : default: return false; break;
864 : : }
865 : : }
866 : 7683180 : break;
867 : 8 : case ProofRule::DSL_REWRITE:
868 : : {
869 : 8 : ProofRewriteRule di = ProofRewriteRule::NONE;
870 [ - + ]: 8 : if (!rewriter::getRewriteRule(args[0], di))
871 : : {
872 : 0 : DebugUnhandled();
873 : : }
874 [ + - ]: 8 : Trace("lfsc-print-debug2") << "Printing dsl rule " << di << std::endl;
875 : 8 : const rewriter::RewriteProofRule& rpr = d_rdb->getRule(di);
876 : 8 : const std::vector<Node>& varList = rpr.getVarList();
877 [ - + ][ - + ]: 8 : Assert(as.size() == varList.size() + 1);
[ - - ]
878 : : // print holes/terms based on whether variables are explicit
879 [ + + ]: 20 : for (size_t i = 1, nargs = as.size(); i < nargs; i++)
880 : : {
881 : 24 : Node v = varList[i - 1];
882 [ + - ]: 12 : if (rpr.isExplicitVar(v))
883 : : {
884 : : // If the variable is a list variable, we must convert its value to
885 : : // the proper term. This is based on its context.
886 [ - + ]: 12 : if (as[i].getKind() == Kind::SEXPR)
887 : : {
888 : 0 : Assert(args[i].getKind() == Kind::SEXPR);
889 : 0 : NodeManager* nm = nodeManager();
890 : 0 : Kind k = rpr.getListContext(v);
891 : : // notice we use d_tproc.getNullTerminator and not
892 : : // expr::getNullTerminator here, which has subtle differences
893 : : // e.g. re.empty vs (str.to_re "").
894 : 0 : Node null = d_tproc.getNullTerminator(nm, k, v.getType());
895 : 0 : Node t;
896 [ - - ]: 0 : if (as[i].getNumChildren() == 1)
897 : : {
898 : : // Singleton list uses null terminator. We first construct an
899 : : // original term and convert it.
900 : 0 : Node tt = nm->mkNode(k, args[i][0], null);
901 : 0 : tt = d_tproc.convert(tt);
902 : : // Since conversion adds a null terminator, we have that
903 : : // tt is of the form (f t (f null null)). We reconstruct
904 : : // the proper term (f t null) below.
905 : 0 : Assert(tt.getNumChildren() == 2);
906 : 0 : Assert(tt[1].getNumChildren() == 2);
907 : 0 : std::vector<Node> tchildren;
908 [ - - ]: 0 : if (tt.getMetaKind() == metakind::PARAMETERIZED)
909 : : {
910 : 0 : tchildren.push_back(tt.getOperator());
911 : : }
912 : 0 : tchildren.push_back(tt[0]);
913 : 0 : tchildren.push_back(tt[1][0]);
914 : 0 : t = nm->mkNode(tt.getKind(), tchildren);
915 : : }
916 : : else
917 : : {
918 [ - - ]: 0 : if (k == Kind::UNDEFINED_KIND)
919 : : {
920 : 0 : Unhandled() << "Unknown context for list variable " << v
921 : 0 : << " in rule " << di;
922 : : }
923 [ - - ]: 0 : if (as[i].getNumChildren() == 0)
924 : : {
925 : 0 : t = null;
926 : : }
927 : : else
928 : : {
929 : : // re-convert it
930 : 0 : std::vector<Node> vec(args[i].begin(), args[i].end());
931 : 0 : t = nm->mkNode(k, vec);
932 : : }
933 : 0 : t = d_tproc.convert(t);
934 : : }
935 : 0 : pf << t;
936 : : }
937 : : else
938 : : {
939 : 12 : pf << as[i];
940 : : }
941 : : }
942 : : else
943 : : {
944 : 0 : pf << h;
945 : : }
946 : : }
947 : : // print child proofs, which is based on the format computed for the rule
948 : 8 : size_t ccounter = 0;
949 : : std::map<ProofRewriteRule, std::vector<Node>>::iterator itf =
950 : 8 : d_dslFormat.find(di);
951 [ + + ]: 8 : if (itf == d_dslFormat.end())
952 : : {
953 : : // We may not have computed the format yet, e.g. if we are printing
954 : : // via the pre print channel. In this case, just print all the children.
955 [ - + ]: 4 : for (const ProofNode* c : cs)
956 : : {
957 : 0 : pf << c;
958 : : }
959 : : }
960 : : else
961 : : {
962 [ - + ]: 4 : for (const Node& f : itf->second)
963 : : {
964 [ - - ]: 0 : if (f.isNull())
965 : : {
966 : : // this position is a hole
967 : 0 : pf << h;
968 : 0 : continue;
969 : : }
970 : 0 : Assert(ccounter < cs.size());
971 : 0 : pf << cs[ccounter];
972 : 0 : ccounter++;
973 : : }
974 [ - + ][ - + ]: 4 : Assert(ccounter == cs.size());
[ - - ]
975 : : }
976 : : }
977 : 8 : break;
978 : 1165130 : default:
979 : : {
980 : 1165130 : return false;
981 : : break;
982 : : }
983 : : }
984 : 14422500 : return true;
985 : : }
986 : :
987 : 411708 : void LfscPrinter::computeProofLetification(
988 : : const ProofNode* pn,
989 : : std::vector<const ProofNode*>& pletList,
990 : : std::map<const ProofNode*, size_t>& pletMap)
991 : : {
992 : : // use callback to specify to stop at LAMBDA
993 : 411708 : ProofLetify::computeProofLet(pn, pletList, pletMap, 2, &d_lpltc);
994 : 411708 : }
995 : :
996 : 559 : void LfscPrinter::print(std::ostream& out, Node n)
997 : : {
998 : 559 : Node ni = d_tproc.convert(n);
999 : 559 : printLetify(out, ni);
1000 : 559 : }
1001 : :
1002 : 559 : void LfscPrinter::printLetify(std::ostream& out, Node n)
1003 : : {
1004 : : // closing parentheses
1005 : 1118 : std::stringstream cparen;
1006 : :
1007 : 559 : LetBinding lbind(d_termLetPrefix);
1008 : 559 : lbind.process(n);
1009 : :
1010 : : // [1] print the letification
1011 : 559 : printLetList(out, cparen, lbind);
1012 : :
1013 : : // [2] print the body
1014 : 559 : printInternal(out, n, lbind);
1015 : :
1016 : 559 : out << cparen.str();
1017 : 559 : }
1018 : :
1019 : 2255 : void LfscPrinter::printLetList(std::ostream& out,
1020 : : std::ostream& cparen,
1021 : : LetBinding& lbind,
1022 : : bool asDefs)
1023 : : {
1024 : 4510 : std::vector<Node> letList;
1025 : 2255 : lbind.letify(letList);
1026 : 2255 : std::map<Node, size_t>::const_iterator it;
1027 [ + + ]: 398387 : for (size_t i = 0, nlets = letList.size(); i < nlets; i++)
1028 : : {
1029 : 792264 : Node nl = letList[i];
1030 : 396132 : size_t id = lbind.getId(nl);
1031 [ - + ][ - + ]: 396132 : Assert(id != 0);
[ - - ]
1032 [ + + ]: 396132 : if (asDefs)
1033 : : {
1034 : 28 : out << "(define ";
1035 : 28 : LfscPrintChannelOut::printId(out, id, d_termLetPrefix);
1036 : 28 : out << " ";
1037 : : // do not letify the top term
1038 : 28 : printInternal(out, nl, lbind, false);
1039 : 28 : out << ")" << std::endl;
1040 : : }
1041 : : else
1042 : : {
1043 : 396104 : out << "(@ ";
1044 : 396104 : LfscPrintChannelOut::printId(out, id, d_termLetPrefix);
1045 : 396104 : out << " ";
1046 : : // do not letify the top term
1047 : 396104 : printInternal(out, nl, lbind, false);
1048 : 396104 : out << std::endl;
1049 : 396104 : cparen << ")";
1050 : : }
1051 : : }
1052 : 2255 : }
1053 : :
1054 : 0 : void LfscPrinter::printInternal(std::ostream& out, Node n)
1055 : : {
1056 : 0 : LetBinding lbind(d_termLetPrefix);
1057 : 0 : printInternal(out, n, lbind);
1058 : 0 : }
1059 : 412663 : void LfscPrinter::printInternal(std::ostream& out,
1060 : : Node n,
1061 : : LetBinding& lbind,
1062 : : bool letTop)
1063 : : {
1064 : 412663 : Node nc = lbind.convert(n, letTop);
1065 : 412663 : LfscPrintChannelOut::printNodeInternal(out, nc);
1066 : 412663 : }
1067 : :
1068 : 17158 : void LfscPrinter::printType(std::ostream& out, TypeNode tn)
1069 : : {
1070 : 17158 : TypeNode tni = d_tproc.convertType(tn);
1071 : 17158 : LfscPrintChannelOut::printTypeNodeInternal(out, tni);
1072 : 17158 : }
1073 : :
1074 : 2 : void LfscPrinter::printDslRule(std::ostream& out,
1075 : : ProofRewriteRule id,
1076 : : std::vector<Node>& format)
1077 : : {
1078 : 2 : const rewriter::RewriteProofRule& rpr = d_rdb->getRule(id);
1079 : 2 : const std::vector<Node>& varList = rpr.getVarList();
1080 : 2 : const std::vector<Node>& uvarList = rpr.getUserVarList();
1081 : 2 : const std::vector<Node>& conds = rpr.getConditions();
1082 : 4 : Node conc = rpr.getConclusion();
1083 : :
1084 : 4 : std::stringstream oscs;
1085 : 4 : std::stringstream odecl;
1086 : :
1087 : 4 : std::stringstream rparen;
1088 : 2 : odecl << "(declare ";
1089 : 2 : LfscPrintChannelOut::printProofRewriteRule(odecl, id);
1090 : 4 : std::vector<Node> vlsubs;
1091 : : // streams for printing the computation of term in side conditions or
1092 : : // list semantics substitutions
1093 : 4 : std::stringstream argList;
1094 : 4 : std::stringstream argListTerms;
1095 : : // the list variables
1096 : 2 : std::unordered_set<Node> listVars;
1097 : 2 : argList << "(";
1098 : : // use the names from the user variable list (uvarList)
1099 [ + + ]: 5 : for (const Node& v : uvarList)
1100 : : {
1101 : 6 : std::stringstream sss;
1102 : 3 : sss << v;
1103 : 9 : Node s = d_tproc.mkInternalSymbol(sss.str(), v.getType());
1104 : 3 : odecl << " (! " << sss.str() << " term";
1105 : 3 : argList << "(" << sss.str() << " term)";
1106 : 3 : argListTerms << " " << sss.str();
1107 : 3 : rparen << ")";
1108 : 3 : vlsubs.push_back(s);
1109 : : // remember if v was a list variable, we must convert these in side
1110 : : // condition printing below
1111 [ - + ]: 3 : if (expr::isListVar(v))
1112 : : {
1113 : 0 : listVars.insert(s);
1114 : : }
1115 : : }
1116 : 2 : argList << ")";
1117 : : // print conditions
1118 : 2 : size_t termCount = 0;
1119 : 2 : size_t scCount = 0;
1120 : : // print conditions, then conclusion
1121 [ + + ]: 4 : for (size_t i = 0, nconds = conds.size(); i <= nconds; i++)
1122 : : {
1123 : 2 : bool isConclusion = i == nconds;
1124 [ + - ]: 2 : Node term = isConclusion ? conc : conds[i];
1125 : : Node sterm = term.substitute(
1126 : 2 : varList.begin(), varList.end(), vlsubs.begin(), vlsubs.end());
1127 [ - + ]: 2 : if (expr::hasListVar(term))
1128 : : {
1129 : 0 : Assert(!listVars.empty());
1130 : 0 : scCount++;
1131 : 0 : std::stringstream scName;
1132 : 0 : scName << "dsl.sc." << scCount << "." << id;
1133 : : // generate the side condition
1134 : 0 : oscs << "(function " << scName.str() << " " << argList.str() << " term"
1135 : 0 : << std::endl;
1136 : : // body must be converted to incorporate list semantics for substitutions
1137 : : // first traversal applies nary_elim to required n-ary applications
1138 : 0 : LfscListScNodeConverter llsncp(nodeManager(), d_tproc, listVars, true);
1139 : 0 : Node tscp;
1140 [ - - ]: 0 : if (isConclusion)
1141 : : {
1142 : 0 : Assert(sterm.getKind() == Kind::EQUAL);
1143 : : // optimization: don't need nary_elim for heads
1144 : 0 : tscp = llsncp.convert(sterm[1]);
1145 : 0 : tscp = sterm[0].eqNode(tscp);
1146 : : }
1147 : : else
1148 : : {
1149 : 0 : tscp = llsncp.convert(sterm);
1150 : : }
1151 : : // second traversal converts to LFSC form
1152 : 0 : Node t = d_tproc.convert(tscp);
1153 : : // third traversal applies nary_concat where list variables are used
1154 : 0 : LfscListScNodeConverter llsnc(nodeManager(), d_tproc, listVars, false);
1155 : 0 : Node tsc = llsnc.convert(t);
1156 : 0 : oscs << " ";
1157 : 0 : print(oscs, tsc);
1158 : 0 : oscs << ")" << std::endl;
1159 : 0 : termCount++;
1160 : : // introduce a term computed by side condition
1161 : 0 : odecl << " (! _t" << termCount << " term";
1162 : 0 : rparen << ")";
1163 : 0 : format.push_back(Node::null());
1164 : : // side condition, which is an implicit argument
1165 : 0 : odecl << " (! _s" << scCount << " (^ (" << scName.str();
1166 : 0 : rparen << ")";
1167 : : // arguments to side condition
1168 : 0 : odecl << argListTerms.str() << ") ";
1169 : : // matches condition
1170 : 0 : odecl << "_t" << termCount << ")";
1171 [ - - ]: 0 : if (!isConclusion)
1172 : : {
1173 : : // the child proof
1174 : 0 : odecl << " (! _u" << i;
1175 : 0 : rparen << ")";
1176 : 0 : format.push_back(term);
1177 : : }
1178 : 0 : odecl << " (holds _t" << termCount << ")";
1179 : 0 : continue;
1180 : : }
1181 : : // ordinary condition/conclusion, print the term directly
1182 [ - + ]: 2 : if (!isConclusion)
1183 : : {
1184 : 0 : odecl << " (! _u" << i;
1185 : 0 : rparen << ")";
1186 : 0 : format.push_back(term);
1187 : : }
1188 : 2 : odecl << " (holds ";
1189 : 4 : Node t = d_tproc.convert(sterm);
1190 : 2 : print(odecl, t);
1191 : 2 : odecl << ")";
1192 : : }
1193 : 2 : odecl << rparen.str() << ")" << std::endl;
1194 : : // print the side conditions
1195 : 2 : out << oscs.str();
1196 : : // print the rule declaration
1197 : 2 : out << odecl.str();
1198 : 2 : }
1199 : :
1200 : : } // namespace proof
1201 : : } // namespace cvc5::internal
|
