Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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 the AletheLF format.
14 : : */
15 : :
16 : : #include "proof/alf/alf_printer.h"
17 : :
18 : : #include <cctype>
19 : : #include <iostream>
20 : : #include <memory>
21 : : #include <ostream>
22 : : #include <sstream>
23 : :
24 : : #include "expr/node_algorithm.h"
25 : : #include "expr/subs.h"
26 : : #include "options/main_options.h"
27 : : #include "printer/printer.h"
28 : : #include "printer/smt2/smt2_printer.h"
29 : : #include "proof/alf/alf_dependent_type_converter.h"
30 : : #include "proof/proof_node_to_sexpr.h"
31 : : #include "rewriter/rewrite_db.h"
32 : : #include "smt/print_benchmark.h"
33 : : #include "theory/strings/theory_strings_utils.h"
34 : :
35 : : namespace cvc5::internal {
36 : :
37 : : namespace proof {
38 : :
39 : 1614 : AlfPrinter::AlfPrinter(Env& env,
40 : : BaseAlfNodeConverter& atp,
41 : : rewriter::RewriteDb* rdb,
42 : 1614 : uint32_t letThresh)
43 : : : EnvObj(env),
44 : : d_tproc(atp),
45 : : d_pfIdCounter(0),
46 : : d_alreadyPrinted(&d_passumeCtx),
47 : : d_passumeMap(&d_passumeCtx),
48 : : d_termLetPrefix("@t"),
49 : : d_ltproc(nodeManager(), atp),
50 : : d_rdb(rdb),
51 : : // Use a let binding if proofDagGlobal is true. We can traverse binders
52 : : // due to the way we print global declare-var, since terms beneath
53 : : // binders will always have their variables in scope and hence can be
54 : : // printed in define commands. We additionally traverse skolems with this
55 : : // utility.
56 : 1614 : d_lbind(d_termLetPrefix, letThresh, true, true),
57 [ + - ]: 1614 : d_lbindUse(options().proof.proofDagGlobal ? &d_lbind : nullptr),
58 : 3228 : d_aletify(d_lbindUse)
59 : : {
60 : 1614 : d_pfType = nodeManager()->mkSort("proofType");
61 : 1614 : d_false = nodeManager()->mkConst(false);
62 : 1614 : }
63 : :
64 : 4234640 : bool AlfPrinter::isHandled(const ProofNode* pfn) const
65 : : {
66 : 8469280 : const std::vector<Node> pargs = pfn->getArguments();
67 [ + + ][ + + ]: 4234640 : switch (pfn->getRule())
[ + + ][ + + ]
[ + ]
68 : : {
69 : : // List of handled rules
70 : 3813900 : case ProofRule::SCOPE:
71 : : case ProofRule::REFL:
72 : : case ProofRule::SYMM:
73 : : case ProofRule::TRANS:
74 : : case ProofRule::CONG:
75 : : case ProofRule::NARY_CONG:
76 : : case ProofRule::HO_CONG:
77 : : case ProofRule::TRUE_INTRO:
78 : : case ProofRule::TRUE_ELIM:
79 : : case ProofRule::FALSE_INTRO:
80 : : case ProofRule::FALSE_ELIM:
81 : : case ProofRule::SPLIT:
82 : : case ProofRule::EQ_RESOLVE:
83 : : case ProofRule::MODUS_PONENS:
84 : : case ProofRule::NOT_NOT_ELIM:
85 : : case ProofRule::CONTRA:
86 : : case ProofRule::AND_ELIM:
87 : : case ProofRule::AND_INTRO:
88 : : case ProofRule::NOT_OR_ELIM:
89 : : case ProofRule::IMPLIES_ELIM:
90 : : case ProofRule::NOT_IMPLIES_ELIM1:
91 : : case ProofRule::NOT_IMPLIES_ELIM2:
92 : : case ProofRule::EQUIV_ELIM1:
93 : : case ProofRule::EQUIV_ELIM2:
94 : : case ProofRule::NOT_EQUIV_ELIM1:
95 : : case ProofRule::NOT_EQUIV_ELIM2:
96 : : case ProofRule::XOR_ELIM1:
97 : : case ProofRule::XOR_ELIM2:
98 : : case ProofRule::NOT_XOR_ELIM1:
99 : : case ProofRule::NOT_XOR_ELIM2:
100 : : case ProofRule::ITE_ELIM1:
101 : : case ProofRule::ITE_ELIM2:
102 : : case ProofRule::NOT_ITE_ELIM1:
103 : : case ProofRule::NOT_ITE_ELIM2:
104 : : case ProofRule::NOT_AND:
105 : : case ProofRule::CNF_AND_NEG:
106 : : case ProofRule::CNF_OR_POS:
107 : : case ProofRule::CNF_OR_NEG:
108 : : case ProofRule::CNF_IMPLIES_POS:
109 : : case ProofRule::CNF_IMPLIES_NEG1:
110 : : case ProofRule::CNF_IMPLIES_NEG2:
111 : : case ProofRule::CNF_EQUIV_POS1:
112 : : case ProofRule::CNF_EQUIV_POS2:
113 : : case ProofRule::CNF_EQUIV_NEG1:
114 : : case ProofRule::CNF_EQUIV_NEG2:
115 : : case ProofRule::CNF_XOR_POS1:
116 : : case ProofRule::CNF_XOR_POS2:
117 : : case ProofRule::CNF_XOR_NEG1:
118 : : case ProofRule::CNF_XOR_NEG2:
119 : : case ProofRule::CNF_ITE_POS1:
120 : : case ProofRule::CNF_ITE_POS2:
121 : : case ProofRule::CNF_ITE_POS3:
122 : : case ProofRule::CNF_ITE_NEG1:
123 : : case ProofRule::CNF_ITE_NEG2:
124 : : case ProofRule::CNF_ITE_NEG3:
125 : : case ProofRule::CNF_AND_POS:
126 : : case ProofRule::FACTORING:
127 : : case ProofRule::REORDERING:
128 : : case ProofRule::RESOLUTION:
129 : : case ProofRule::CHAIN_RESOLUTION:
130 : : case ProofRule::ARRAYS_READ_OVER_WRITE:
131 : : case ProofRule::ARRAYS_READ_OVER_WRITE_CONTRA:
132 : : case ProofRule::ARRAYS_READ_OVER_WRITE_1:
133 : : case ProofRule::ARRAYS_EXT:
134 : : case ProofRule::ARITH_SUM_UB:
135 : : case ProofRule::ARITH_MULT_POS:
136 : : case ProofRule::ARITH_MULT_NEG:
137 : : case ProofRule::ARITH_TRICHOTOMY:
138 : : case ProofRule::ARITH_TRANS_EXP_NEG:
139 : : case ProofRule::ARITH_TRANS_EXP_POSITIVITY:
140 : : case ProofRule::ARITH_TRANS_EXP_SUPER_LIN:
141 : : case ProofRule::ARITH_TRANS_EXP_ZERO:
142 : : case ProofRule::ARITH_TRANS_SINE_BOUNDS:
143 : : case ProofRule::ARITH_TRANS_SINE_SYMMETRY:
144 : : case ProofRule::ARITH_TRANS_SINE_TANGENT_ZERO:
145 : : case ProofRule::ARITH_TRANS_SINE_TANGENT_PI:
146 : : case ProofRule::INT_TIGHT_LB:
147 : : case ProofRule::INT_TIGHT_UB:
148 : : case ProofRule::SKOLEM_INTRO:
149 : : case ProofRule::SETS_SINGLETON_INJ:
150 : : case ProofRule::SETS_EXT:
151 : : case ProofRule::SETS_FILTER_UP:
152 : : case ProofRule::SETS_FILTER_DOWN:
153 : : case ProofRule::CONCAT_EQ:
154 : : case ProofRule::CONCAT_UNIFY:
155 : : case ProofRule::CONCAT_CSPLIT:
156 : : case ProofRule::CONCAT_CPROP:
157 : : case ProofRule::CONCAT_CONFLICT:
158 : : case ProofRule::CONCAT_SPLIT:
159 : : case ProofRule::CONCAT_LPROP:
160 : : case ProofRule::STRING_LENGTH_POS:
161 : : case ProofRule::STRING_LENGTH_NON_EMPTY:
162 : : case ProofRule::RE_INTER:
163 : : case ProofRule::RE_UNFOLD_POS:
164 : : case ProofRule::RE_UNFOLD_NEG_CONCAT_FIXED:
165 : : case ProofRule::RE_UNFOLD_NEG:
166 : : case ProofRule::STRING_CODE_INJ:
167 : : case ProofRule::STRING_SEQ_UNIT_INJ:
168 : : case ProofRule::STRING_DECOMPOSE:
169 : : case ProofRule::ITE_EQ:
170 : : case ProofRule::INSTANTIATE:
171 : : case ProofRule::SKOLEMIZE:
172 : : case ProofRule::ALPHA_EQUIV:
173 : : case ProofRule::ENCODE_EQ_INTRO:
174 : : case ProofRule::HO_APP_ENCODE:
175 : : case ProofRule::ACI_NORM:
176 : 3813900 : case ProofRule::DSL_REWRITE: return true;
177 : 9602 : case ProofRule::BV_BITBLAST_STEP:
178 : : {
179 : 9602 : return isHandledBitblastStep(pfn->getArguments()[0]);
180 : : }
181 : : break;
182 : 5430 : case ProofRule::THEORY_REWRITE:
183 : : {
184 : : ProofRewriteRule id;
185 : 5430 : rewriter::getRewriteRule(pfn->getArguments()[0], id);
186 : 5430 : return isHandledTheoryRewrite(id, pfn->getArguments()[1]);
187 : : }
188 : : break;
189 : 178067 : case ProofRule::ARITH_POLY_NORM:
190 : : {
191 : : // we don't support bitvectors yet
192 [ - + ][ - + ]: 178067 : Assert(pargs[0].getKind() == Kind::EQUAL);
[ - - ]
193 : 178067 : return pargs[0][0].getType().isRealOrInt();
194 : : }
195 : : break;
196 : 100711 : case ProofRule::ARITH_POLY_NORM_REL:
197 : : {
198 : : // we don't support bitvectors yet
199 : 100711 : Node res = pfn->getResult();
200 [ - + ][ - + ]: 100711 : Assert(res.getKind() == Kind::EQUAL);
[ - - ]
201 [ - + ][ - + ]: 100711 : Assert(res[0].getType().isBoolean());
[ - - ]
202 : 100711 : return res[0][0].getType().isRealOrInt();
203 : : }
204 : : break;
205 : 428 : case ProofRule::STRING_REDUCTION:
206 : : {
207 : : // depends on the operator
208 [ - + ][ - + ]: 428 : Assert(!pargs.empty());
[ - - ]
209 : 428 : Kind k = pargs[0].getKind();
210 [ + + ][ + + ]: 428 : return k == Kind::STRING_SUBSTR || k == Kind::STRING_INDEXOF;
211 : : }
212 : : break;
213 : 176 : case ProofRule::STRING_EAGER_REDUCTION:
214 : : {
215 : : // depends on the operator
216 [ - + ][ - + ]: 176 : Assert(!pargs.empty());
[ - - ]
217 : 176 : Kind k = pargs[0].getKind();
218 [ + + ]: 142 : return k == Kind::STRING_CONTAINS || k == Kind::STRING_TO_CODE
219 [ + + ][ + + ]: 318 : || k == Kind::STRING_INDEXOF || k == Kind::STRING_IN_REGEXP;
[ + + ]
220 : : }
221 : : break;
222 : : //
223 : 110865 : case ProofRule::EVALUATE:
224 : : {
225 [ + + ]: 110865 : if (canEvaluate(pargs[0]))
226 : : {
227 [ + - ]: 110227 : Trace("alf-printer-debug") << "Can evaluate " << pargs[0] << std::endl;
228 : 110227 : return true;
229 : : }
230 : : }
231 : 638 : break;
232 : : // otherwise not handled
233 : 15461 : default: break;
234 : : }
235 : 16099 : return false;
236 : : }
237 : :
238 : 5430 : bool AlfPrinter::isHandledTheoryRewrite(ProofRewriteRule id,
239 : : const Node& n) const
240 : : {
241 [ + + ][ + ]: 5430 : switch (id)
242 : : {
243 : 2098 : case ProofRewriteRule::DISTINCT_ELIM:
244 : : case ProofRewriteRule::BETA_REDUCE:
245 : : case ProofRewriteRule::ARITH_STRING_PRED_ENTAIL:
246 : : case ProofRewriteRule::ARITH_STRING_PRED_SAFE_APPROX:
247 : : case ProofRewriteRule::RE_LOOP_ELIM:
248 : : case ProofRewriteRule::SETS_IS_EMPTY_EVAL:
249 : : case ProofRewriteRule::STR_IN_RE_CONCAT_STAR_CHAR:
250 : : case ProofRewriteRule::STR_IN_RE_SIGMA:
251 : : case ProofRewriteRule::STR_IN_RE_SIGMA_STAR:
252 : : case ProofRewriteRule::STR_IN_RE_CONSUME:
253 : : case ProofRewriteRule::RE_INTER_UNION_INCLUSION:
254 : 2098 : case ProofRewriteRule::BV_BITWISE_SLICING: return true;
255 : 70 : case ProofRewriteRule::STR_IN_RE_EVAL:
256 : 140 : Assert(n[0].getKind() == Kind::STRING_IN_REGEXP && n[0][0].isConst());
257 : 70 : return canEvaluateRegExp(n[0][1]);
258 : 3262 : default: break;
259 : : }
260 : 3262 : return false;
261 : : }
262 : :
263 : 9602 : bool AlfPrinter::isHandledBitblastStep(const Node& eq) const
264 : : {
265 [ - + ][ - + ]: 9602 : Assert(eq.getKind() == Kind::EQUAL);
[ - - ]
266 [ + + ]: 9602 : if (eq[0].isVar())
267 : : {
268 : 1308 : return true;
269 : : }
270 [ + + ]: 8294 : switch (eq[0].getKind())
271 : : {
272 : 5086 : case Kind::CONST_BITVECTOR:
273 : : case Kind::BITVECTOR_EXTRACT:
274 : : case Kind::BITVECTOR_CONCAT:
275 : 5086 : case Kind::EQUAL: return true;
276 : 3208 : default:
277 [ + - ][ - + ]: 3208 : Trace("alf-printer-debug") << "Cannot bitblast " << eq[0] << std::endl;
[ - - ]
278 : 3208 : break;
279 : : }
280 : 3208 : return false;
281 : : }
282 : :
283 : 110915 : bool AlfPrinter::canEvaluate(Node n) const
284 : : {
285 : 221830 : std::unordered_set<TNode> visited;
286 : 221830 : std::vector<TNode> visit;
287 : 221830 : TNode cur;
288 : 110915 : visit.push_back(n);
289 : 260775 : do
290 : : {
291 : 371690 : cur = visit.back();
292 : 371690 : visit.pop_back();
293 [ + + ]: 371690 : if (visited.find(cur) == visited.end())
294 : : {
295 : 318406 : visited.insert(cur);
296 [ + + ][ + + ]: 318406 : switch (cur.getKind())
297 : : {
298 : 306864 : case Kind::ITE:
299 : : case Kind::NOT:
300 : : case Kind::AND:
301 : : case Kind::OR:
302 : : case Kind::XOR:
303 : : case Kind::CONST_BOOLEAN:
304 : : case Kind::CONST_INTEGER:
305 : : case Kind::CONST_RATIONAL:
306 : : case Kind::CONST_STRING:
307 : : case Kind::CONST_BITVECTOR:
308 : : case Kind::ADD:
309 : : case Kind::SUB:
310 : : case Kind::NEG:
311 : : case Kind::LT:
312 : : case Kind::GT:
313 : : case Kind::GEQ:
314 : : case Kind::LEQ:
315 : : case Kind::MULT:
316 : : case Kind::NONLINEAR_MULT:
317 : : case Kind::INTS_MODULUS:
318 : : case Kind::INTS_MODULUS_TOTAL:
319 : : case Kind::DIVISION:
320 : : case Kind::DIVISION_TOTAL:
321 : : case Kind::INTS_DIVISION:
322 : : case Kind::INTS_DIVISION_TOTAL:
323 : : case Kind::INTS_ISPOW2:
324 : : case Kind::INTS_LOG2:
325 : : case Kind::TO_REAL:
326 : : case Kind::TO_INTEGER:
327 : : case Kind::IS_INTEGER:
328 : : case Kind::STRING_CONCAT:
329 : : case Kind::STRING_SUBSTR:
330 : : case Kind::STRING_LENGTH:
331 : : case Kind::STRING_CONTAINS:
332 : : case Kind::STRING_REPLACE:
333 : : case Kind::STRING_INDEXOF:
334 : : case Kind::STRING_TO_CODE:
335 : : case Kind::STRING_FROM_CODE:
336 : : case Kind::BITVECTOR_EXTRACT:
337 : : case Kind::BITVECTOR_CONCAT:
338 : : case Kind::BITVECTOR_ADD:
339 : : case Kind::BITVECTOR_SUB:
340 : : case Kind::BITVECTOR_NEG:
341 : : case Kind::BITVECTOR_NOT:
342 : : case Kind::BITVECTOR_MULT:
343 : : case Kind::BITVECTOR_AND:
344 : : case Kind::BITVECTOR_OR:
345 : 306864 : case Kind::CONST_BITVECTOR_SYMBOLIC: break;
346 : 8868 : case Kind::EQUAL:
347 : : {
348 : 8868 : TypeNode tn = cur[0].getType();
349 [ + + ][ + + ]: 15082 : if (!tn.isBoolean() && !tn.isReal() && !tn.isInteger()
350 [ + + ][ + + ]: 15082 : && !tn.isString() && !tn.isBitVector())
[ - + ][ - + ]
351 : : {
352 : 0 : return false;
353 : : }
354 : : }
355 : 8868 : break;
356 : 2036 : case Kind::BITVECTOR_SIZE:
357 : : // special case, evaluates no matter what is inside
358 : 2036 : continue;
359 : 638 : default:
360 [ + - ]: 1276 : Trace("alf-printer-debug")
361 : 638 : << "Cannot evaluate " << cur.getKind() << std::endl;
362 : 2674 : return false;
363 : : }
364 [ + + ]: 576739 : for (const Node& cn : cur)
365 : : {
366 : 261007 : visit.push_back(cn);
367 : : }
368 : : }
369 [ + + ]: 371052 : } while (!visit.empty());
370 : 110277 : return true;
371 : : }
372 : :
373 : 70 : bool AlfPrinter::canEvaluateRegExp(Node r) const
374 : : {
375 [ - + ][ - + ]: 70 : Assert(r.getType().isRegExp());
[ - - ]
376 [ + - ]: 70 : Trace("alf-printer-debug") << "canEvaluateRegExp? " << r << std::endl;
377 : 140 : std::unordered_set<TNode> visited;
378 : 140 : std::vector<TNode> visit;
379 : 140 : TNode cur;
380 : 70 : visit.push_back(r);
381 : 420 : do
382 : : {
383 : 490 : cur = visit.back();
384 : 490 : visit.pop_back();
385 [ + + ]: 490 : if (visited.find(cur) == visited.end())
386 : : {
387 : 204 : visited.insert(cur);
388 [ + + ][ + - ]: 204 : switch (cur.getKind())
389 : : {
390 : 138 : case Kind::REGEXP_ALL:
391 : : case Kind::REGEXP_ALLCHAR:
392 : : case Kind::REGEXP_COMPLEMENT:
393 : : case Kind::REGEXP_NONE:
394 : : case Kind::REGEXP_UNION:
395 : : case Kind::REGEXP_INTER:
396 : : case Kind::REGEXP_CONCAT:
397 : 138 : case Kind::REGEXP_STAR: break;
398 : 16 : case Kind::REGEXP_RANGE:
399 [ - + ]: 16 : if (!theory::strings::utils::isCharacterRange(cur))
400 : : {
401 [ - - ]: 0 : Trace("alf-printer-debug") << "Non-char range" << std::endl;
402 : 0 : return false;
403 : : }
404 : 16 : continue;
405 : 50 : case Kind::STRING_TO_REGEXP:
406 [ - + ]: 50 : if (!canEvaluate(cur[0]))
407 : : {
408 [ - - ]: 0 : Trace("alf-printer-debug") << "Non-evaluatable string" << std::endl;
409 : 0 : return false;
410 : : }
411 : 50 : continue;
412 : 0 : default:
413 [ - - ]: 0 : Trace("alf-printer-debug") << "Cannot evaluate " << cur.getKind()
414 : 0 : << " in regular expressions" << std::endl;
415 : 0 : return false;
416 : : }
417 [ + + ]: 558 : for (const Node& cn : cur)
418 : : {
419 : 420 : visit.push_back(cn);
420 : : }
421 : : }
422 [ + + ]: 490 : } while (!visit.empty());
423 : 70 : return true;
424 : : }
425 : :
426 : 4207920 : std::string AlfPrinter::getRuleName(const ProofNode* pfn) const
427 : : {
428 : 4207920 : ProofRule r = pfn->getRule();
429 [ + + ]: 4207920 : if (r == ProofRule::DSL_REWRITE)
430 : : {
431 : : ProofRewriteRule id;
432 : 212458 : rewriter::getRewriteRule(pfn->getArguments()[0], id);
433 : 424916 : std::stringstream ss;
434 : 212458 : ss << id;
435 : 212458 : return ss.str();
436 : : }
437 [ + + ]: 3995460 : else if (r == ProofRule::THEORY_REWRITE)
438 : : {
439 : : ProofRewriteRule id;
440 : 2168 : rewriter::getRewriteRule(pfn->getArguments()[0], id);
441 : 4336 : std::stringstream ss;
442 : 2168 : ss << id;
443 : 2168 : return ss.str();
444 : : }
445 [ + + ][ + + ]: 3993290 : else if (r == ProofRule::ENCODE_EQ_INTRO || r == ProofRule::HO_APP_ENCODE)
446 : : {
447 : : // ENCODE_EQ_INTRO proves (= t (convert t)) from argument t,
448 : : // where (convert t) is indistinguishable from t according to the proof.
449 : : // Similarly, HO_APP_ENCODE proves an equality between a term of kind
450 : : // Kind::HO_APPLY and Kind::APPLY_UF, which denotes the same term in ALF.
451 : 11144 : return "refl";
452 : : }
453 : 7964300 : std::string name = toString(r);
454 : 35198900 : std::transform(name.begin(), name.end(), name.begin(), [](unsigned char c) {
455 : 35198900 : return std::tolower(c);
456 : 3982150 : });
457 : 3982150 : return name;
458 : : }
459 : :
460 : 0 : void AlfPrinter::printDslRule(std::ostream& out, ProofRewriteRule r)
461 : : {
462 : 0 : const rewriter::RewriteProofRule& rpr = d_rdb->getRule(r);
463 : 0 : const std::vector<Node>& varList = rpr.getVarList();
464 : 0 : const std::vector<Node>& uvarList = rpr.getUserVarList();
465 : 0 : const std::vector<Node>& conds = rpr.getConditions();
466 : 0 : Node conc = rpr.getConclusion(true);
467 : : // We must map variables of the rule to internal symbols (via
468 : : // mkInternalSymbol) so that the ALF node converter will not treat the
469 : : // BOUND_VARIABLE of this rule as user provided variables. The substitution
470 : : // su stores this mapping.
471 : 0 : Subs su;
472 : 0 : out << "(declare-rule " << r << " (";
473 : 0 : AlfDependentTypeConverter adtc(nodeManager(), d_tproc);
474 : 0 : std::stringstream ssExplicit;
475 : 0 : std::map<std::string, size_t> nameCount;
476 : 0 : std::vector<Node> uviList;
477 [ - - ]: 0 : for (size_t i = 0, nvars = uvarList.size(); i < nvars; i++)
478 : : {
479 [ - - ]: 0 : if (i > 0)
480 : : {
481 : 0 : ssExplicit << " ";
482 : : }
483 : 0 : const Node& uv = uvarList[i];
484 : 0 : std::stringstream sss;
485 : 0 : sss << uv;
486 : : // Use a consistent variable name, which e.g. ensures that minor changes
487 : : // to the RARE rules do not induce major changes in the CPC definition.
488 : : // Below, we have a variable when the user has named x (which itself may
489 : : // contain digits), and the cvc5 RARE parser has renamed to xN where N is
490 : : // <numeral>+. We rename this to xM where M is the number of times we have
491 : : // seen a variable with prefix M. For example, the variable `x1s2` may be
492 : : // renamed to `x1s2123`, which will be renamed to `x1s1` here.
493 : 0 : std::string str = sss.str();
494 : 0 : size_t index = str.find_last_not_of("0123456789");
495 : 0 : std::string result = str.substr(0, index + 1);
496 : 0 : sss.str("");
497 : 0 : nameCount[result]++;
498 : 0 : sss << result << nameCount[result];
499 : 0 : Node uvi = d_tproc.mkInternalSymbol(sss.str(), uv.getType());
500 : 0 : uviList.emplace_back(uvi);
501 : 0 : su.add(varList[i], uvi);
502 : 0 : ssExplicit << "(" << sss.str() << " ";
503 : 0 : TypeNode uvt = uv.getType();
504 : 0 : Node uvtp = adtc.process(uvt);
505 : 0 : ssExplicit << uvtp;
506 [ - - ]: 0 : if (expr::isListVar(uv))
507 : : {
508 : : // carry over whether it is a list variable
509 : 0 : expr::markListVar(uvi);
510 : 0 : ssExplicit << " :list";
511 : : }
512 : 0 : ssExplicit << ")";
513 : : }
514 : : // print implicit parameters introduced in dependent type conversion
515 : 0 : const std::vector<Node>& params = adtc.getFreeParameters();
516 [ - - ]: 0 : for (const Node& p : params)
517 : : {
518 : 0 : out << "(" << p << " " << p.getType() << ") ";
519 : : }
520 : : // now print variables of the proof rule
521 : 0 : out << ssExplicit.str();
522 : 0 : out << ")" << std::endl;
523 [ - - ]: 0 : if (!conds.empty())
524 : : {
525 : 0 : out << " :premises (";
526 : 0 : bool firstTime = true;
527 [ - - ]: 0 : for (const Node& c : conds)
528 : : {
529 [ - - ]: 0 : if (firstTime)
530 : : {
531 : 0 : firstTime = false;
532 : : }
533 : : else
534 : : {
535 : 0 : out << " ";
536 : : }
537 : : // note we apply list conversion to premises as well.
538 : 0 : Node cc = d_tproc.convert(su.apply(c));
539 : 0 : cc = d_ltproc.convert(cc);
540 : 0 : out << cc;
541 : : }
542 : 0 : out << ")" << std::endl;
543 : : }
544 : 0 : out << " :args (";
545 [ - - ]: 0 : for (size_t i = 0, nvars = uviList.size(); i < nvars; i++)
546 : : {
547 [ - - ]: 0 : if (i > 0)
548 : : {
549 : 0 : out << " ";
550 : : }
551 : 0 : out << uviList[i];
552 : : }
553 : 0 : out << ")" << std::endl;
554 : 0 : Node sconc = d_tproc.convert(su.apply(conc));
555 : 0 : sconc = d_ltproc.convert(sconc);
556 : 0 : Assert(sconc.getKind() == Kind::EQUAL);
557 : 0 : out << " :conclusion (= " << sconc[0] << " " << sconc[1] << ")" << std::endl;
558 : 0 : out << ")" << std::endl;
559 : 0 : }
560 : :
561 : 0 : LetBinding* AlfPrinter::getLetBinding() { return d_lbindUse; }
562 : :
563 : 1614 : void AlfPrinter::printLetList(std::ostream& out, LetBinding& lbind)
564 : : {
565 : 3228 : std::vector<Node> letList;
566 : 1614 : lbind.letify(letList);
567 : 1614 : std::map<Node, size_t>::const_iterator it;
568 [ + + ]: 913832 : for (size_t i = 0, nlets = letList.size(); i < nlets; i++)
569 : : {
570 : 1824440 : Node n = letList[i];
571 : : // use define command which does not invoke type checking
572 : 912218 : out << "(define " << d_termLetPrefix << lbind.getId(n);
573 : 912218 : out << " () ";
574 : 912218 : Printer::getPrinter(out)->toStream(out, n, &lbind, false);
575 : 912218 : out << ")" << std::endl;
576 : : }
577 : 1614 : }
578 : :
579 : 1614 : void AlfPrinter::print(std::ostream& out,
580 : : std::shared_ptr<ProofNode> pfn,
581 : : ProofScopeMode psm)
582 : : {
583 : : // ensures options are set once and for all
584 : 1614 : options::ioutils::applyOutputLanguage(out, Language::LANG_SMTLIB_V2_6);
585 : 1614 : options::ioutils::applyPrintArithLitToken(out, true);
586 : 1614 : options::ioutils::applyPrintSkolemDefinitions(out, true);
587 : : // allocate a print channel
588 : 1614 : AlfPrintChannelOut aprint(out, d_lbindUse, d_termLetPrefix, true);
589 : 1614 : print(aprint, pfn, psm);
590 : 1614 : }
591 : :
592 : 1614 : void AlfPrinter::print(AlfPrintChannelOut& aout,
593 : : std::shared_ptr<ProofNode> pfn,
594 : : ProofScopeMode psm)
595 : : {
596 : 1614 : std::ostream& out = aout.getOStream();
597 [ - + ][ - + ]: 1614 : Assert(d_pletMap.empty());
[ - - ]
598 : 1614 : d_pfIdCounter = 0;
599 : :
600 : 1614 : const ProofNode* ascope = nullptr;
601 : 1614 : const ProofNode* dscope = nullptr;
602 : 1614 : const ProofNode* pnBody = nullptr;
603 [ - + ]: 1614 : if (psm == ProofScopeMode::NONE)
604 : : {
605 : 0 : pnBody = pfn.get();
606 : : }
607 [ - + ]: 1614 : else if (psm == ProofScopeMode::UNIFIED)
608 : : {
609 : 0 : ascope = pfn.get();
610 : 0 : Assert(ascope->getRule() == ProofRule::SCOPE);
611 : 0 : pnBody = pfn->getChildren()[0].get();
612 : : }
613 [ + - ]: 1614 : else if (psm == ProofScopeMode::DEFINITIONS_AND_ASSERTIONS)
614 : : {
615 : 1614 : dscope = pfn.get();
616 [ - + ][ - + ]: 1614 : Assert(dscope->getRule() == ProofRule::SCOPE);
[ - - ]
617 : 1614 : ascope = pfn->getChildren()[0].get();
618 [ - + ][ - + ]: 1614 : Assert(ascope->getRule() == ProofRule::SCOPE);
[ - - ]
619 : 1614 : pnBody = pfn->getChildren()[0]->getChildren()[0].get();
620 : : }
621 : :
622 : : // Get the definitions and assertions and print the declarations from them
623 : : const std::vector<Node>& definitions =
624 [ + - ]: 1614 : dscope != nullptr ? dscope->getArguments() : d_emptyVec;
625 : : const std::vector<Node>& assertions =
626 [ + - ]: 1614 : ascope != nullptr ? ascope->getArguments() : d_emptyVec;
627 : : bool wasAlloc;
628 [ + + ]: 4842 : for (size_t i = 0; i < 2; i++)
629 : : {
630 : : AlfPrintChannel* ao;
631 [ + + ]: 3228 : if (i == 0)
632 : : {
633 : 1614 : ao = &d_aletify;
634 : : }
635 : : else
636 : : {
637 : 1614 : ao = &aout;
638 : : }
639 [ + + ]: 3228 : if (i == 1)
640 : : {
641 : : // do not need to print DSL rules
642 [ + - ]: 1614 : if (!options().proof.proofPrintReference)
643 : : {
644 : : // [1] print the declarations
645 : 3228 : printer::smt2::Smt2Printer alfp(printer::smt2::Variant::alf_variant);
646 : : // we do not print declarations in a sorted manner to reduce overhead
647 : 1614 : smt::PrintBenchmark pb(nodeManager(), &alfp, false, &d_tproc);
648 : 3228 : std::stringstream outDecl;
649 : 1614 : std::stringstream outDef;
650 : 1614 : pb.printDeclarationsFrom(outDecl, outDef, definitions, assertions);
651 : 1614 : out << outDecl.str();
652 : : // [2] print the definitions
653 : 1614 : out << outDef.str();
654 : : }
655 : : // [3] print proof-level term bindings
656 : 1614 : printLetList(out, d_lbind);
657 : : }
658 : : // [4] print (unique) assumptions, including definitions
659 : 6456 : std::unordered_set<Node> processed;
660 [ + + ]: 35192 : for (const Node& n : assertions)
661 : : {
662 [ + + ]: 31964 : if (processed.find(n) != processed.end())
663 : : {
664 : 736 : continue;
665 : : }
666 : 31228 : processed.insert(n);
667 : 31228 : size_t id = allocateAssumeId(n, wasAlloc);
668 : 31228 : Node nc = d_tproc.convert(n);
669 : 31228 : ao->printAssume(nc, id, false);
670 : : }
671 [ + + ]: 4026 : for (const Node& n : definitions)
672 : : {
673 [ - + ]: 798 : if (n.getKind() != Kind::EQUAL)
674 : : {
675 : : // skip define-fun-rec?
676 : 0 : continue;
677 : : }
678 [ - + ]: 798 : if (processed.find(n) != processed.end())
679 : : {
680 : 0 : continue;
681 : : }
682 : 798 : processed.insert(n);
683 : : // define-fun are HO equalities that can be proven by refl
684 : 798 : size_t id = allocateAssumeId(n, wasAlloc);
685 : 1596 : Node f = d_tproc.convert(n[0]);
686 : 798 : Node lam = d_tproc.convert(n[1]);
687 : 1596 : ao->printStep("refl", f.eqNode(lam), id, {}, {lam});
688 : : }
689 : : // [5] print proof body
690 : 3228 : printProofInternal(ao, pnBody, i == 1);
691 : : }
692 : 1614 : }
693 : :
694 : 0 : void AlfPrinter::printNext(AlfPrintChannelOut& aout,
695 : : std::shared_ptr<ProofNode> pfn)
696 : : {
697 : 0 : const ProofNode* pnBody = pfn.get();
698 : : // print with letification
699 : 0 : printProofInternal(&d_aletify, pnBody, false);
700 : : // print the new let bindings
701 : 0 : std::ostream& out = aout.getOStream();
702 : : // Print new terms from the let binding. note that this should print only
703 : : // the terms we have yet to see so far.
704 : 0 : printLetList(out, d_lbind);
705 : : // print the proof
706 : 0 : printProofInternal(&aout, pnBody, true);
707 : 0 : }
708 : :
709 : 3228 : void AlfPrinter::printProofInternal(AlfPrintChannel* out,
710 : : const ProofNode* pn,
711 : : bool addToCache)
712 : : {
713 : : // the stack
714 : 6456 : std::vector<const ProofNode*> visit;
715 : : // Whether we have to process children.
716 : : // This map is dependent on the proof assumption context, e.g. subproofs of
717 : : // SCOPE are reprocessed if they happen to occur in different proof scopes.
718 : 6456 : context::CDHashMap<const ProofNode*, bool> processingChildren(&d_passumeCtx);
719 : : // helper iterators
720 : 3228 : context::CDHashMap<const ProofNode*, bool>::iterator pit;
721 : : const ProofNode* cur;
722 : 3228 : visit.push_back(pn);
723 : 11813500 : do
724 : : {
725 : 11816700 : cur = visit.back();
726 [ + + ]: 11816700 : if (d_alreadyPrinted.find(cur) != d_alreadyPrinted.end())
727 : : {
728 : 1427330 : visit.pop_back();
729 : 1427330 : continue;
730 : : }
731 : 10389400 : pit = processingChildren.find(cur);
732 [ + + ]: 10389400 : if (pit == processingChildren.end())
733 : : {
734 : 4724850 : ProofRule r = cur->getRule();
735 [ + + ]: 4724850 : if (r == ProofRule::ASSUME)
736 : : {
737 : : // ignore
738 : 490214 : visit.pop_back();
739 : 490214 : continue;
740 : : }
741 : : // print preorder traversal
742 : 4234640 : printStepPre(out, cur);
743 : 4234640 : processingChildren[cur] = true;
744 : : // will revisit this proof node
745 : 8469280 : std::vector<std::shared_ptr<ProofNode>> children;
746 : 4234640 : getChildrenFromProofRule(cur, children);
747 : : // visit each child
748 [ + + ]: 11813500 : for (const std::shared_ptr<ProofNode>& c : children)
749 : : {
750 : 7578870 : visit.push_back(c.get());
751 : : }
752 : 4234640 : continue;
753 : : }
754 : 5664550 : visit.pop_back();
755 [ + + ]: 5664550 : if (pit->second)
756 : : {
757 : 4234640 : processingChildren[cur] = false;
758 : : // print postorder traversal
759 : 4234640 : printStepPost(out, cur);
760 [ + + ]: 4234640 : if (addToCache)
761 : : {
762 : 2099150 : d_alreadyPrinted.insert(cur);
763 : : }
764 : : }
765 [ + + ]: 11816700 : } while (!visit.empty());
766 : 3228 : }
767 : :
768 : 4234640 : void AlfPrinter::printStepPre(AlfPrintChannel* out, const ProofNode* pn)
769 : : {
770 : : // if we haven't yet allocated a proof id, do it now
771 : 4234640 : ProofRule r = pn->getRule();
772 [ + + ]: 4234640 : if (r == ProofRule::SCOPE)
773 : : {
774 : : // The assumptions only are valid within the body of the SCOPE, thus
775 : : // we push a context scope.
776 : 85243 : d_passumeCtx.push();
777 : 85243 : const std::vector<Node>& args = pn->getArguments();
778 [ + + ]: 505866 : for (const Node& a : args)
779 : : {
780 : 420623 : size_t aid = allocateAssumePushId(pn, a);
781 : 420623 : Node aa = d_tproc.convert(a);
782 : : // print a push
783 : 420623 : out->printAssume(aa, aid, true);
784 : : }
785 : : }
786 : 4234640 : }
787 : :
788 : 8469280 : void AlfPrinter::getChildrenFromProofRule(
789 : : const ProofNode* pn, std::vector<std::shared_ptr<ProofNode>>& children)
790 : : {
791 : 8469280 : const std::vector<std::shared_ptr<ProofNode>>& cc = pn->getChildren();
792 [ + + ]: 8469280 : switch (pn->getRule())
793 : : {
794 : 831236 : case ProofRule::CONG:
795 : : {
796 : 831236 : Node res = pn->getResult();
797 [ + + ]: 831236 : if (res[0].isClosure())
798 : : {
799 : : // Ignore the children after the required arguments.
800 : : // This ensures that we ignore e.g. equalities between patterns
801 : : // which can appear in term conversion proofs.
802 : 10684 : size_t arity = kind::metakind::getMinArityForKind(res[0].getKind());
803 : 10684 : children.insert(children.end(), cc.begin(), cc.begin() + arity - 1);
804 : 10684 : return;
805 : : }
806 : : }
807 : 820552 : break;
808 : 7638040 : default: break;
809 : : }
810 : 8458600 : children.insert(children.end(), cc.begin(), cc.end());
811 : : }
812 : :
813 : 4207920 : void AlfPrinter::getArgsFromProofRule(const ProofNode* pn,
814 : : std::vector<Node>& args)
815 : : {
816 : 4207920 : Node res = pn->getResult();
817 : 4207920 : const std::vector<Node> pargs = pn->getArguments();
818 : 4207920 : ProofRule r = pn->getRule();
819 [ + + ][ + + ]: 4207920 : switch (r)
[ + + ]
820 : : {
821 : 696179 : case ProofRule::CONG:
822 : : case ProofRule::NARY_CONG:
823 : : case ProofRule::ARITH_POLY_NORM_REL:
824 : : {
825 : 1392360 : Node op = d_tproc.getOperatorOfTerm(res[0], true);
826 : 696179 : args.push_back(d_tproc.convert(op));
827 : 696179 : return;
828 : : }
829 : : break;
830 : 514 : case ProofRule::HO_CONG:
831 : : {
832 : : // argument is ignored
833 : 514 : return;
834 : : }
835 : 2562 : case ProofRule::INSTANTIATE:
836 : : {
837 : : // ignore arguments past the term vector
838 : 5124 : Node ts = d_tproc.convert(pargs[0]);
839 : 2562 : args.push_back(ts);
840 : 2562 : return;
841 : : }
842 : 212458 : case ProofRule::DSL_REWRITE:
843 : : {
844 : : ProofRewriteRule dr;
845 [ - + ]: 212458 : if (!rewriter::getRewriteRule(pargs[0], dr))
846 : : {
847 : 0 : Unhandled() << "Failed to get DSL proof rule";
848 : : }
849 [ + - ]: 212458 : Trace("alf-printer-debug") << "Get args for " << dr << std::endl;
850 : 212458 : const rewriter::RewriteProofRule& rpr = d_rdb->getRule(dr);
851 : 424916 : std::vector<Node> ss(pargs.begin() + 1, pargs.end());
852 : 424916 : std::vector<std::pair<Kind, std::vector<Node>>> witnessTerms;
853 : 212458 : rpr.getConclusionFor(ss, witnessTerms);
854 : 424916 : TypeNode absType = nodeManager()->mkAbstractType(Kind::ABSTRACT_TYPE);
855 : : // the arguments are the computed witness terms
856 [ + + ]: 597108 : for (const std::pair<Kind, std::vector<Node>>& w : witnessTerms)
857 : : {
858 [ + + ]: 384650 : if (w.first == Kind::UNDEFINED_KIND)
859 : : {
860 [ - + ][ - + ]: 371360 : Assert(w.second.size() == 1);
[ - - ]
861 : 371360 : args.push_back(d_tproc.convert(w.second[0]));
862 : : }
863 : : else
864 : : {
865 : 13290 : std::vector<Node> wargs;
866 [ + + ]: 36698 : for (const Node& wc : w.second)
867 : : {
868 : 23408 : wargs.push_back(d_tproc.convert(wc));
869 : : }
870 : 26580 : args.push_back(d_tproc.mkInternalApp(
871 : 26580 : printer::smt2::Smt2Printer::smtKindString(w.first),
872 : : wargs,
873 : 13290 : absType));
874 : : }
875 : : }
876 : 212458 : return;
877 : : }
878 : 2168 : case ProofRule::THEORY_REWRITE:
879 : : {
880 : : // ignore the identifier
881 [ - + ][ - + ]: 2168 : Assert(pargs.size() == 2);
[ - - ]
882 : 2168 : args.push_back(d_tproc.convert(pargs[1]));
883 : 2168 : return;
884 : : }
885 : : break;
886 : 3294040 : default: break;
887 : : }
888 [ + + ]: 5786900 : for (size_t i = 0, nargs = pargs.size(); i < nargs; i++)
889 : : {
890 : 4985720 : Node av = d_tproc.convert(pargs[i]);
891 : 2492860 : args.push_back(av);
892 : : }
893 : : }
894 : :
895 : 4234640 : void AlfPrinter::printStepPost(AlfPrintChannel* out, const ProofNode* pn)
896 : : {
897 [ - + ][ - + ]: 4234640 : Assert(pn->getRule() != ProofRule::ASSUME);
[ - - ]
898 : : // if we have yet to allocate a proof id, do it now
899 : 4234640 : bool wasAlloc = false;
900 : 8469280 : TNode conclusion = d_tproc.convert(pn->getResult());
901 : 4234640 : TNode conclusionPrint;
902 : : // print conclusion only if option is set, or this is false
903 [ + + ][ + + ]: 4234640 : if (options().proof.proofPrintConclusion || conclusion == d_false)
[ + + ]
904 : : {
905 : 4209500 : conclusionPrint = conclusion;
906 : : }
907 : 4234640 : ProofRule r = pn->getRule();
908 : 4234640 : std::vector<std::shared_ptr<ProofNode>> children;
909 : 4234640 : getChildrenFromProofRule(pn, children);
910 : 4234640 : std::vector<Node> args;
911 : 4234640 : bool handled = isHandled(pn);
912 [ + + ]: 4234640 : if (handled)
913 : : {
914 : 4207920 : getArgsFromProofRule(pn, args);
915 : : }
916 : 4234640 : size_t id = allocateProofId(pn, wasAlloc);
917 : 4234640 : std::vector<size_t> premises;
918 : : // get the premises
919 : 4234640 : context::CDHashMap<Node, size_t>::iterator ita;
920 : 4234640 : std::map<const ProofNode*, size_t>::iterator itp;
921 [ + + ]: 11813500 : for (const std::shared_ptr<ProofNode>& c : children)
922 : : {
923 : : size_t pid;
924 : : // if assume, lookup in passumeMap
925 [ + + ]: 7578870 : if (c->getRule() == ProofRule::ASSUME)
926 : : {
927 : 490188 : ita = d_passumeMap.find(c->getResult());
928 [ - + ][ - + ]: 490188 : Assert(ita != d_passumeMap.end());
[ - - ]
929 : 490188 : pid = ita->second;
930 : : }
931 : : else
932 : : {
933 : 7088680 : itp = d_pletMap.find(c.get());
934 [ - + ][ - + ]: 7088680 : Assert(itp != d_pletMap.end());
[ - - ]
935 : 7088680 : pid = itp->second;
936 : : }
937 : 7578870 : premises.push_back(pid);
938 : : }
939 : : // if we don't handle the rule, print trust
940 [ + + ]: 4234640 : if (!handled)
941 : : {
942 [ - + ]: 26721 : if (!options().proof.proofAllowTrust)
943 : : {
944 : 0 : std::stringstream ss;
945 : 0 : ss << pn->getRule();
946 [ - - ]: 0 : if (pn->getRule() == ProofRule::THEORY_REWRITE)
947 : : {
948 : : ProofRewriteRule prid;
949 : 0 : rewriter::getRewriteRule(pn->getArguments()[0], prid);
950 : 0 : ss << " (" << prid << ")";
951 : : }
952 [ - - ]: 0 : else if (pn->getRule() == ProofRule::TRUST)
953 : : {
954 : : TrustId tid;
955 : 0 : getTrustId(pn->getArguments()[0], tid);
956 : 0 : ss << " (" << tid << ")";
957 : : }
958 : 0 : Trace("alf-pf-hole") << "Proof rule " << ss.str() << ": "
959 : 0 : << pn->getResult() << std::endl;
960 : 0 : Unreachable() << "An ALF proof equires a trust step for " << ss.str()
961 : : << ", but --" << options::proof::longName::proofAllowTrust
962 : 0 : << " is false" << std::endl;
963 : : }
964 : 26721 : out->printTrustStep(pn->getRule(),
965 : : conclusionPrint,
966 : : id,
967 : : premises,
968 : : pn->getArguments(),
969 : 26721 : conclusion);
970 : 26721 : return;
971 : : }
972 : 8415840 : std::string rname = getRuleName(pn);
973 [ + + ]: 4207920 : if (r == ProofRule::SCOPE)
974 : : {
975 [ + + ]: 85243 : if (args.empty())
976 : : {
977 : : // If there are no premises, any reference to this proof can just refer to
978 : : // the body.
979 : 12 : d_pletMap[pn] = premises[0];
980 : : }
981 : : else
982 : : {
983 : : // Assuming the body of the scope has identifier id_0, the following prints:
984 : : // (step-pop id_1 :rule scope :premises (id_0))
985 : : // ...
986 : : // (step-pop id_n :rule scope :premises (id_{n-1}))
987 : : // (step id :rule process_scope :premises (id_n) :args (C))
988 : : size_t tmpId;
989 [ + + ]: 505854 : for (size_t i = 0, nargs = args.size(); i < nargs; i++)
990 : : {
991 : : // Manually increment proof id counter and premises. Note they will only be
992 : : // used locally here to chain together the pops mentioned above.
993 : 420623 : tmpId = d_pfIdCounter;
994 : 420623 : d_pfIdCounter++;
995 : 420623 : out->printStep(rname, Node::null(), tmpId, premises, {}, true);
996 : : // The current id is the premises of the next.
997 : 420623 : premises.clear();
998 : 420623 : premises.push_back(tmpId);
999 : : }
1000 : : // Finish with the process scope step.
1001 : 85231 : std::vector<Node> pargs;
1002 : 85231 : pargs.push_back(d_tproc.convert(children[0]->getResult()));
1003 : 85231 : out->printStep("process_scope", conclusionPrint, id, premises, pargs);
1004 : : }
1005 : : // We are done with the assumptions in scope, pop a context.
1006 : 85243 : d_passumeCtx.pop();
1007 : : }
1008 : : else
1009 : : {
1010 : 4122680 : out->printStep(rname, conclusionPrint, id, premises, args);
1011 : : }
1012 : : }
1013 : :
1014 : 420623 : size_t AlfPrinter::allocateAssumePushId(const ProofNode* pn, const Node& a)
1015 : : {
1016 : 420623 : std::pair<const ProofNode*, Node> key(pn, a);
1017 : :
1018 : 420623 : bool wasAlloc = false;
1019 : 420623 : size_t aid = allocateAssumeId(a, wasAlloc);
1020 : : // if we assigned an id to the assumption
1021 [ + + ]: 420623 : if (!wasAlloc)
1022 : : {
1023 : : // otherwise we shadow, just use a dummy
1024 : 80419 : d_pfIdCounter++;
1025 : 80419 : aid = d_pfIdCounter;
1026 : : }
1027 : 841246 : return aid;
1028 : : }
1029 : :
1030 : 452649 : size_t AlfPrinter::allocateAssumeId(const Node& n, bool& wasAlloc)
1031 : : {
1032 : 452649 : context::CDHashMap<Node, size_t>::iterator it = d_passumeMap.find(n);
1033 [ + + ]: 452649 : if (it != d_passumeMap.end())
1034 : : {
1035 : 96432 : wasAlloc = false;
1036 : 96432 : return it->second;
1037 : : }
1038 : 356217 : wasAlloc = true;
1039 : 356217 : d_pfIdCounter++;
1040 : 356217 : d_passumeMap[n] = d_pfIdCounter;
1041 : 356217 : return d_pfIdCounter;
1042 : : }
1043 : :
1044 : 4234640 : size_t AlfPrinter::allocateProofId(const ProofNode* pn, bool& wasAlloc)
1045 : : {
1046 : 4234640 : std::map<const ProofNode*, size_t>::iterator it = d_pletMap.find(pn);
1047 [ + + ]: 4234640 : if (it != d_pletMap.end())
1048 : : {
1049 : 2412310 : wasAlloc = false;
1050 : 2412310 : return it->second;
1051 : : }
1052 : 1822330 : wasAlloc = true;
1053 : 1822330 : d_pfIdCounter++;
1054 : 1822330 : d_pletMap[pn] = d_pfIdCounter;
1055 : 1822330 : return d_pfIdCounter;
1056 : : }
1057 : :
1058 : : } // namespace proof
1059 : : } // namespace cvc5::internal
|
