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