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 the Eunoia format.
11 : : */
12 : :
13 : : #include "proof/eo/eo_printer.h"
14 : :
15 : : #include <cctype>
16 : : #include <iostream>
17 : : #include <memory>
18 : : #include <ostream>
19 : : #include <sstream>
20 : :
21 : : #include "expr/aci_norm.h"
22 : : #include "expr/node_algorithm.h"
23 : : #include "expr/sequence.h"
24 : : #include "expr/subs.h"
25 : : #include "options/base_options.h"
26 : : #include "options/main_options.h"
27 : : #include "options/strings_options.h"
28 : : #include "printer/printer.h"
29 : : #include "printer/smt2/smt2_printer.h"
30 : : #include "proof/eo/eo_dependent_type_converter.h"
31 : : #include "proof/proof_node_to_sexpr.h"
32 : : #include "rewriter/rewrite_db.h"
33 : : #include "smt/print_benchmark.h"
34 : : #include "theory/builtin/generic_op.h"
35 : : #include "theory/strings/theory_strings_utils.h"
36 : : #include "theory/theory.h"
37 : : #include "util/string.h"
38 : :
39 : : namespace cvc5::internal {
40 : :
41 : : namespace proof {
42 : :
43 : 2000 : EoPrinter::EoPrinter(Env& env,
44 : : BaseEoNodeConverter& atp,
45 : : rewriter::RewriteDb* rdb,
46 : 2000 : uint32_t letThresh)
47 : : : EnvObj(env),
48 : 2000 : d_tproc(atp),
49 : 2000 : d_pfIdCounter(0),
50 : 2000 : d_alreadyPrinted(&d_passumeCtx),
51 : 2000 : d_passumeMap(&d_passumeCtx),
52 : 2000 : d_termLetPrefix("@t"),
53 : 2000 : d_rdb(rdb),
54 : : // Use a let binding if proofDagGlobal is true. We can traverse binders
55 : : // due to the way we print global declare-var, since terms beneath
56 : : // binders will always have their variables in scope and hence can be
57 : : // printed in define commands. We additionally traverse skolems with this
58 : : // utility.
59 : 2000 : d_lbind(d_termLetPrefix, letThresh, true, true),
60 [ + - ]: 2000 : d_lbindUse(options().proof.proofDagGlobal ? &d_lbind : nullptr),
61 : 8000 : d_eletify(d_lbindUse)
62 : : {
63 : 2000 : d_pfType = nodeManager()->mkSort("proofType");
64 : 2000 : d_false = nodeManager()->mkConst(false);
65 : 2000 : d_absType = nodeManager()->mkAbstractType(Kind::ABSTRACT_TYPE);
66 : 2000 : }
67 : :
68 : 4027223 : bool EoPrinter::isHandled(const Options& opts, const ProofNode* pfn)
69 : : {
70 : 4027223 : const std::vector<Node> pargs = pfn->getArguments();
71 [ + + ][ + + ]: 4027223 : switch (pfn->getRule())
[ + + ][ + + ]
[ + + ]
72 : : {
73 : : // List of handled rules
74 : 3859169 : case ProofRule::ASSUME:
75 : : case ProofRule::SCOPE:
76 : : case ProofRule::REFL:
77 : : case ProofRule::SYMM:
78 : : case ProofRule::TRANS:
79 : : case ProofRule::CONG:
80 : : case ProofRule::NARY_CONG:
81 : : case ProofRule::PAIRWISE_CONG:
82 : : case ProofRule::HO_CONG:
83 : : case ProofRule::TRUE_INTRO:
84 : : case ProofRule::TRUE_ELIM:
85 : : case ProofRule::FALSE_INTRO:
86 : : case ProofRule::FALSE_ELIM:
87 : : case ProofRule::SPLIT:
88 : : case ProofRule::EQ_RESOLVE:
89 : : case ProofRule::MODUS_PONENS:
90 : : case ProofRule::NOT_NOT_ELIM:
91 : : case ProofRule::CONTRA:
92 : : case ProofRule::AND_ELIM:
93 : : case ProofRule::AND_INTRO:
94 : : case ProofRule::NOT_OR_ELIM:
95 : : case ProofRule::IMPLIES_ELIM:
96 : : case ProofRule::NOT_IMPLIES_ELIM1:
97 : : case ProofRule::NOT_IMPLIES_ELIM2:
98 : : case ProofRule::EQUIV_ELIM1:
99 : : case ProofRule::EQUIV_ELIM2:
100 : : case ProofRule::NOT_EQUIV_ELIM1:
101 : : case ProofRule::NOT_EQUIV_ELIM2:
102 : : case ProofRule::XOR_ELIM1:
103 : : case ProofRule::XOR_ELIM2:
104 : : case ProofRule::NOT_XOR_ELIM1:
105 : : case ProofRule::NOT_XOR_ELIM2:
106 : : case ProofRule::ITE_ELIM1:
107 : : case ProofRule::ITE_ELIM2:
108 : : case ProofRule::NOT_ITE_ELIM1:
109 : : case ProofRule::NOT_ITE_ELIM2:
110 : : case ProofRule::NOT_AND:
111 : : case ProofRule::CNF_AND_NEG:
112 : : case ProofRule::CNF_OR_POS:
113 : : case ProofRule::CNF_OR_NEG:
114 : : case ProofRule::CNF_IMPLIES_POS:
115 : : case ProofRule::CNF_IMPLIES_NEG1:
116 : : case ProofRule::CNF_IMPLIES_NEG2:
117 : : case ProofRule::CNF_EQUIV_POS1:
118 : : case ProofRule::CNF_EQUIV_POS2:
119 : : case ProofRule::CNF_EQUIV_NEG1:
120 : : case ProofRule::CNF_EQUIV_NEG2:
121 : : case ProofRule::CNF_XOR_POS1:
122 : : case ProofRule::CNF_XOR_POS2:
123 : : case ProofRule::CNF_XOR_NEG1:
124 : : case ProofRule::CNF_XOR_NEG2:
125 : : case ProofRule::CNF_ITE_POS1:
126 : : case ProofRule::CNF_ITE_POS2:
127 : : case ProofRule::CNF_ITE_POS3:
128 : : case ProofRule::CNF_ITE_NEG1:
129 : : case ProofRule::CNF_ITE_NEG2:
130 : : case ProofRule::CNF_ITE_NEG3:
131 : : case ProofRule::CNF_AND_POS:
132 : : case ProofRule::FACTORING:
133 : : case ProofRule::REORDERING:
134 : : case ProofRule::RESOLUTION:
135 : : case ProofRule::CHAIN_RESOLUTION:
136 : : case ProofRule::CHAIN_M_RESOLUTION:
137 : : case ProofRule::ARRAYS_READ_OVER_WRITE:
138 : : case ProofRule::ARRAYS_READ_OVER_WRITE_CONTRA:
139 : : case ProofRule::ARRAYS_READ_OVER_WRITE_1:
140 : : case ProofRule::ARRAYS_EXT:
141 : : case ProofRule::ARITH_SUM_UB:
142 : : case ProofRule::ARITH_MULT_POS:
143 : : case ProofRule::ARITH_MULT_NEG:
144 : : case ProofRule::ARITH_MULT_TANGENT:
145 : : case ProofRule::ARITH_MULT_SIGN:
146 : : case ProofRule::ARITH_MULT_ABS_COMPARISON:
147 : : case ProofRule::ARITH_TRICHOTOMY:
148 : : case ProofRule::INT_TIGHT_LB:
149 : : case ProofRule::INT_TIGHT_UB:
150 : : case ProofRule::SKOLEM_INTRO:
151 : : case ProofRule::SETS_SINGLETON_INJ:
152 : : case ProofRule::SETS_EXT:
153 : : case ProofRule::CONCAT_EQ:
154 : : case ProofRule::CONCAT_UNIFY:
155 : : case ProofRule::CONCAT_CSPLIT:
156 : : case ProofRule::CONCAT_CPROP:
157 : : case ProofRule::CONCAT_SPLIT:
158 : : case ProofRule::CONCAT_LPROP:
159 : : case ProofRule::STRING_LENGTH_POS:
160 : : case ProofRule::STRING_LENGTH_NON_EMPTY:
161 : : case ProofRule::RE_INTER:
162 : : case ProofRule::RE_CONCAT:
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::STRING_EXT:
170 : : case ProofRule::DT_SPLIT:
171 : : case ProofRule::ITE_EQ:
172 : : case ProofRule::INSTANTIATE:
173 : : case ProofRule::SKOLEMIZE:
174 : : case ProofRule::ALPHA_EQUIV:
175 : : case ProofRule::QUANT_VAR_REORDERING:
176 : : case ProofRule::ENCODE_EQ_INTRO:
177 : : case ProofRule::HO_APP_ENCODE:
178 : : case ProofRule::BV_EAGER_ATOM:
179 : : case ProofRule::ACI_NORM:
180 : : case ProofRule::ABSORB:
181 : : case ProofRule::ARITH_POLY_NORM:
182 : : case ProofRule::ARITH_POLY_NORM_REL:
183 : : case ProofRule::BV_POLY_NORM:
184 : : case ProofRule::BV_POLY_NORM_EQ:
185 : : case ProofRule::EXISTS_STRING_LENGTH:
186 : 3859169 : case ProofRule::DSL_REWRITE: return true;
187 : 13556 : case ProofRule::BV_BITBLAST_STEP:
188 : : {
189 : 13556 : return isHandledBitblastStep(pfn->getArguments()[0]);
190 : : }
191 : : break;
192 : 13032 : case ProofRule::THEORY_REWRITE:
193 : : {
194 : : ProofRewriteRule id;
195 : 13032 : rewriter::getRewriteRule(pfn->getArguments()[0], id);
196 : 13032 : return isHandledTheoryRewrite(opts, id, pfn->getArguments()[1]);
197 : : }
198 : : break;
199 : 766 : case ProofRule::ARITH_REDUCTION:
200 : : {
201 : 766 : Kind k = pargs[0].getKind();
202 [ + + ]: 746 : return k == Kind::TO_INTEGER || k == Kind::IS_INTEGER
203 [ + + ][ + + ]: 700 : || k == Kind::DIVISION || k == Kind::DIVISION_TOTAL
204 [ + + ][ + + ]: 612 : || k == Kind::INTS_DIVISION || k == Kind::INTS_DIVISION_TOTAL
205 [ + + ][ + + ]: 376 : || k == Kind::INTS_MODULUS || k == Kind::INTS_MODULUS_TOTAL
206 [ + + ][ + + ]: 1512 : || k == Kind::ABS || k == Kind::INTS_LOG2;
[ + + ]
207 : : }
208 : : break;
209 : 642 : case ProofRule::STRING_REDUCTION:
210 : : {
211 : : // depends on the operator
212 [ - + ][ - + ]: 642 : Assert(!pargs.empty());
[ - - ]
213 : 642 : Kind k = pargs[0].getKind();
214 [ + - ]: 642 : switch (k)
215 : : {
216 : 642 : case Kind::STRING_CONTAINS:
217 : : case Kind::STRING_SUBSTR:
218 : : case Kind::STRING_INDEXOF:
219 : : case Kind::STRING_INDEXOF_RE:
220 : : case Kind::STRING_REPLACE:
221 : : case Kind::STRING_REPLACE_ALL:
222 : : case Kind::STRING_REPLACE_RE:
223 : : case Kind::STRING_REPLACE_RE_ALL:
224 : : case Kind::STRING_STOI:
225 : : case Kind::STRING_ITOS:
226 : : case Kind::SEQ_NTH:
227 : : case Kind::STRING_UPDATE:
228 : : case Kind::STRING_LEQ:
229 : : case Kind::STRING_REV:
230 : : case Kind::STRING_TO_LOWER:
231 : 642 : case Kind::STRING_TO_UPPER: return true;
232 : 0 : default: break;
233 : : }
234 [ - - ]: 0 : Trace("eo-printer-debug") << "Cannot STRING_REDUCTION " << k << std::endl;
235 : 0 : return false;
236 : : }
237 : : break;
238 : 290 : case ProofRule::STRING_EAGER_REDUCTION:
239 : : {
240 : : // depends on the operator
241 [ - + ][ - + ]: 290 : Assert(!pargs.empty());
[ - - ]
242 : 290 : Kind k = pargs[0].getKind();
243 [ + + ][ + + ]: 290 : if (k == Kind::STRING_TO_CODE || k == Kind::STRING_FROM_CODE)
244 : : {
245 : : // must use standard alphabet size
246 : 112 : return opts.strings.stringsAlphaCard == String::num_codes();
247 : : }
248 [ + + ]: 66 : return k == Kind::STRING_CONTAINS || k == Kind::STRING_INDEXOF
249 [ + + ][ + + ]: 26 : || k == Kind::STRING_INDEXOF_RE || k == Kind::STRING_IN_REGEXP
250 [ + + ][ + - ]: 244 : || k == Kind::STRING_STOI;
251 : : }
252 : : break;
253 : : //
254 : 136072 : case ProofRule::EVALUATE:
255 : : {
256 [ + - ]: 136072 : if (canEvaluate(pargs[0]))
257 : : {
258 [ + - ]: 136072 : Trace("eo-printer-debug") << "Can evaluate " << pargs[0] << std::endl;
259 : 136072 : return true;
260 : : }
261 : : }
262 : 0 : break;
263 : 118 : case ProofRule::DISTINCT_VALUES:
264 : : {
265 : 118 : if (isHandledDistinctValues(pargs[0])
266 [ + + ][ + - ]: 118 : && isHandledDistinctValues(pargs[1]))
[ + + ]
267 : : {
268 [ + - ]: 92 : Trace("eo-printer-debug") << "Can distinguish values " << pargs[0]
269 : 46 : << " " << pargs[1] << std::endl;
270 : 46 : return true;
271 : : }
272 : : }
273 : 72 : break;
274 : 76 : case ProofRule::ARITH_TRANS_EXP_NEG:
275 : : case ProofRule::ARITH_TRANS_EXP_POSITIVITY:
276 : : case ProofRule::ARITH_TRANS_EXP_SUPER_LIN:
277 : : case ProofRule::ARITH_TRANS_EXP_ZERO:
278 : : case ProofRule::ARITH_TRANS_SINE_BOUNDS:
279 : : case ProofRule::ARITH_TRANS_SINE_SYMMETRY:
280 : : case ProofRule::ARITH_TRANS_SINE_TANGENT_ZERO:
281 : : case ProofRule::ARITH_TRANS_SINE_TANGENT_PI:
282 : : case ProofRule::SETS_FILTER_UP:
283 : : case ProofRule::SETS_FILTER_DOWN:
284 : : {
285 : : // only supported in unrestricted builds
286 [ + - ]: 76 : if (opts.base.safeMode == options::SafeMode::UNRESTRICTED)
287 : : {
288 : 76 : return true;
289 : : }
290 : : }
291 : 0 : break;
292 : : // otherwise not handled
293 : 3502 : default: break;
294 : : }
295 : 3574 : return false;
296 : 4027223 : }
297 : :
298 : 13032 : bool EoPrinter::isHandledTheoryRewrite(const Options& opts,
299 : : ProofRewriteRule id,
300 : : const Node& n)
301 : : {
302 [ + + ][ + + ]: 13032 : switch (id)
303 : : {
304 : 12784 : case ProofRewriteRule::DISTINCT_ELIM:
305 : : case ProofRewriteRule::DISTINCT_CARD_CONFLICT:
306 : : case ProofRewriteRule::DISTINCT_TRUE:
307 : : case ProofRewriteRule::DISTINCT_FALSE:
308 : : case ProofRewriteRule::BETA_REDUCE:
309 : : case ProofRewriteRule::UBV_TO_INT_ELIM:
310 : : case ProofRewriteRule::INT_TO_BV_ELIM:
311 : : case ProofRewriteRule::ARITH_STRING_PRED_ENTAIL:
312 : : case ProofRewriteRule::ARITH_STRING_PRED_SAFE_APPROX:
313 : : case ProofRewriteRule::EXISTS_ELIM:
314 : : case ProofRewriteRule::QUANT_UNUSED_VARS:
315 : : case ProofRewriteRule::DT_INST:
316 : : case ProofRewriteRule::DT_COLLAPSE_SELECTOR:
317 : : case ProofRewriteRule::DT_COLLAPSE_TESTER:
318 : : case ProofRewriteRule::DT_COLLAPSE_TESTER_SINGLETON:
319 : : case ProofRewriteRule::DT_CONS_EQ:
320 : : case ProofRewriteRule::DT_CONS_EQ_CLASH:
321 : : case ProofRewriteRule::DT_CYCLE:
322 : : case ProofRewriteRule::DT_COLLAPSE_UPDATER:
323 : : case ProofRewriteRule::DT_UPDATER_ELIM:
324 : : case ProofRewriteRule::QUANT_MERGE_PRENEX:
325 : : case ProofRewriteRule::QUANT_MINISCOPE_AND:
326 : : case ProofRewriteRule::QUANT_MINISCOPE_OR:
327 : : case ProofRewriteRule::QUANT_MINISCOPE_ITE:
328 : : case ProofRewriteRule::QUANT_VAR_ELIM_EQ:
329 : : case ProofRewriteRule::QUANT_DT_SPLIT:
330 : : case ProofRewriteRule::RE_LOOP_ELIM:
331 : : case ProofRewriteRule::RE_EQ_ELIM:
332 : : case ProofRewriteRule::SETS_EVAL_OP:
333 : : case ProofRewriteRule::SETS_INSERT_ELIM:
334 : : case ProofRewriteRule::STR_IN_RE_CONCAT_STAR_CHAR:
335 : : case ProofRewriteRule::STR_IN_RE_SIGMA:
336 : : case ProofRewriteRule::STR_IN_RE_SIGMA_STAR:
337 : : case ProofRewriteRule::STR_IN_RE_CONSUME:
338 : : case ProofRewriteRule::STR_INDEXOF_RE_EVAL:
339 : : case ProofRewriteRule::STR_REPLACE_RE_EVAL:
340 : : case ProofRewriteRule::STR_REPLACE_RE_ALL_EVAL:
341 : : case ProofRewriteRule::RE_INTER_INCLUSION:
342 : : case ProofRewriteRule::RE_UNION_INCLUSION:
343 : : case ProofRewriteRule::BV_SMULO_ELIM:
344 : : case ProofRewriteRule::BV_UMULO_ELIM:
345 : : case ProofRewriteRule::BV_REPEAT_ELIM:
346 : : case ProofRewriteRule::BV_BITWISE_SLICING:
347 : : case ProofRewriteRule::STR_OVERLAP_SPLIT_CTN:
348 : : case ProofRewriteRule::STR_OVERLAP_ENDPOINTS_CTN:
349 : : case ProofRewriteRule::STR_OVERLAP_ENDPOINTS_INDEXOF:
350 : : case ProofRewriteRule::STR_OVERLAP_ENDPOINTS_REPLACE:
351 : : case ProofRewriteRule::STR_CTN_MULTISET_SUBSET:
352 : 12784 : case ProofRewriteRule::SEQ_EVAL_OP: return true;
353 : 182 : case ProofRewriteRule::STR_IN_RE_EVAL:
354 : 182 : Assert(n[0].getKind() == Kind::STRING_IN_REGEXP && n[0][0].isConst());
355 : 182 : return canEvaluateRegExp(n[0][1]);
356 : 38 : case ProofRewriteRule::ARITH_POW_ELIM:
357 : : case ProofRewriteRule::ARRAYS_SELECT_CONST:
358 : : case ProofRewriteRule::LAMBDA_ELIM:
359 : : // only supported in unrestricted builds
360 [ + - ]: 38 : if (opts.base.safeMode == options::SafeMode::UNRESTRICTED)
361 : : {
362 : 38 : return true;
363 : : }
364 : 0 : break;
365 : 28 : default: break;
366 : : }
367 : 28 : return false;
368 : : }
369 : :
370 : 13556 : bool EoPrinter::isHandledBitblastStep(const Node& eq)
371 : : {
372 [ - + ][ - + ]: 13556 : Assert(eq.getKind() == Kind::EQUAL);
[ - - ]
373 [ + + ]: 13556 : if (theory::Theory::isLeafOf(eq[0], theory::THEORY_BV))
374 : : {
375 : 3202 : return true;
376 : : }
377 [ + - ]: 10354 : switch (eq[0].getKind())
378 : : {
379 : 10354 : case Kind::CONST_BITVECTOR:
380 : : case Kind::BITVECTOR_EXTRACT:
381 : : case Kind::BITVECTOR_CONCAT:
382 : : case Kind::BITVECTOR_AND:
383 : : case Kind::BITVECTOR_OR:
384 : : case Kind::BITVECTOR_XOR:
385 : : case Kind::BITVECTOR_XNOR:
386 : : case Kind::BITVECTOR_NOT:
387 : : case Kind::BITVECTOR_ADD:
388 : : case Kind::BITVECTOR_SUB:
389 : : case Kind::BITVECTOR_NEG:
390 : : case Kind::BITVECTOR_MULT:
391 : : case Kind::BITVECTOR_SIGN_EXTEND:
392 : : case Kind::BITVECTOR_SHL:
393 : : case Kind::BITVECTOR_ASHR:
394 : : case Kind::BITVECTOR_LSHR:
395 : : case Kind::BITVECTOR_UDIV:
396 : : case Kind::BITVECTOR_UREM:
397 : : case Kind::EQUAL:
398 : : case Kind::BITVECTOR_SLT:
399 : : case Kind::BITVECTOR_SLE:
400 : : case Kind::BITVECTOR_ULT:
401 : : case Kind::BITVECTOR_ULE:
402 : : case Kind::BITVECTOR_ITE:
403 : : case Kind::BITVECTOR_COMP:
404 : : case Kind::BITVECTOR_ULTBV:
405 : 10354 : case Kind::BITVECTOR_SLTBV: return true;
406 : 0 : default:
407 : 0 : Trace("eo-printer-debug") << "Cannot bitblast " << eq[0] << std::endl;
408 : 0 : break;
409 : : }
410 : 0 : return false;
411 : : }
412 : :
413 : 136254 : bool EoPrinter::canEvaluate(Node n)
414 : : {
415 : 136254 : std::unordered_set<TNode> visited;
416 : 136254 : std::vector<TNode> visit;
417 : 136254 : TNode cur;
418 : 136254 : visit.push_back(n);
419 : : do
420 : : {
421 : 454707 : cur = visit.back();
422 : 454707 : visit.pop_back();
423 [ + + ]: 454707 : if (visited.find(cur) == visited.end())
424 : : {
425 : 389498 : visited.insert(cur);
426 : 389498 : Kind k = cur.getKind();
427 [ + + ]: 389498 : if (k == Kind::APPLY_INDEXED_SYMBOLIC)
428 : : {
429 : 210 : k = cur.getOperator().getConst<GenericOp>().getKind();
430 : : }
431 [ + + ][ - ]: 389498 : switch (k)
432 : : {
433 : 385904 : case Kind::ITE:
434 : : case Kind::NOT:
435 : : case Kind::AND:
436 : : case Kind::OR:
437 : : case Kind::IMPLIES:
438 : : case Kind::XOR:
439 : : case Kind::CONST_BOOLEAN:
440 : : case Kind::CONST_INTEGER:
441 : : case Kind::CONST_RATIONAL:
442 : : case Kind::CONST_STRING:
443 : : case Kind::CONST_BITVECTOR:
444 : : case Kind::ADD:
445 : : case Kind::SUB:
446 : : case Kind::NEG:
447 : : case Kind::LT:
448 : : case Kind::GT:
449 : : case Kind::GEQ:
450 : : case Kind::LEQ:
451 : : case Kind::MULT:
452 : : case Kind::NONLINEAR_MULT:
453 : : case Kind::INTS_MODULUS:
454 : : case Kind::INTS_MODULUS_TOTAL:
455 : : case Kind::DIVISION:
456 : : case Kind::DIVISION_TOTAL:
457 : : case Kind::INTS_DIVISION:
458 : : case Kind::INTS_DIVISION_TOTAL:
459 : : case Kind::INTS_ISPOW2:
460 : : case Kind::INTS_LOG2:
461 : : case Kind::POW2:
462 : : case Kind::TO_REAL:
463 : : case Kind::TO_INTEGER:
464 : : case Kind::IS_INTEGER:
465 : : case Kind::ABS:
466 : : case Kind::STRING_CONCAT:
467 : : case Kind::STRING_SUBSTR:
468 : : case Kind::STRING_LENGTH:
469 : : case Kind::STRING_CONTAINS:
470 : : case Kind::STRING_REPLACE:
471 : : case Kind::STRING_REPLACE_ALL:
472 : : case Kind::STRING_INDEXOF:
473 : : case Kind::STRING_TO_CODE:
474 : : case Kind::STRING_FROM_CODE:
475 : : case Kind::STRING_PREFIX:
476 : : case Kind::STRING_SUFFIX:
477 : : case Kind::STRING_ITOS:
478 : : case Kind::STRING_STOI:
479 : : case Kind::STRING_TO_LOWER:
480 : : case Kind::STRING_TO_UPPER:
481 : : case Kind::STRING_REV:
482 : : case Kind::STRING_CHARAT:
483 : : case Kind::STRING_UPDATE:
484 : : case Kind::STRING_LEQ:
485 : : case Kind::BITVECTOR_EXTRACT:
486 : : case Kind::BITVECTOR_CONCAT:
487 : : case Kind::BITVECTOR_ADD:
488 : : case Kind::BITVECTOR_SUB:
489 : : case Kind::BITVECTOR_NEG:
490 : : case Kind::BITVECTOR_NOT:
491 : : case Kind::BITVECTOR_MULT:
492 : : case Kind::BITVECTOR_UDIV:
493 : : case Kind::BITVECTOR_UREM:
494 : : case Kind::BITVECTOR_SHL:
495 : : case Kind::BITVECTOR_LSHR:
496 : : case Kind::BITVECTOR_ASHR:
497 : : case Kind::BITVECTOR_AND:
498 : : case Kind::BITVECTOR_OR:
499 : : case Kind::BITVECTOR_XOR:
500 : : case Kind::BITVECTOR_ULT:
501 : : case Kind::BITVECTOR_ULE:
502 : : case Kind::BITVECTOR_UGT:
503 : : case Kind::BITVECTOR_UGE:
504 : : case Kind::BITVECTOR_SLT:
505 : : case Kind::BITVECTOR_SLE:
506 : : case Kind::BITVECTOR_SGT:
507 : : case Kind::BITVECTOR_SGE:
508 : : case Kind::BITVECTOR_REPEAT:
509 : : case Kind::BITVECTOR_SIGN_EXTEND:
510 : : case Kind::BITVECTOR_ZERO_EXTEND:
511 : : case Kind::CONST_BITVECTOR_SYMBOLIC:
512 : : case Kind::BITVECTOR_UBV_TO_INT:
513 : : case Kind::BITVECTOR_SBV_TO_INT:
514 : : case Kind::INT_TO_BITVECTOR:
515 : 385904 : case Kind::EQUAL: break; // note that equality falls through
516 : 3594 : case Kind::BITVECTOR_SIZE:
517 : : // special case, evaluates no matter what is inside
518 : 3594 : continue;
519 : 0 : default:
520 [ - - ]: 0 : Trace("eo-printer-debug")
521 : 0 : << "Cannot evaluate " << cur.getKind() << std::endl;
522 : 0 : return false;
523 : : }
524 [ + + ]: 704357 : for (const Node& cn : cur)
525 : : {
526 : 318453 : visit.push_back(cn);
527 : 318453 : }
528 : : }
529 [ + + ]: 454707 : } while (!visit.empty());
530 : 136254 : return true;
531 : 136254 : }
532 : :
533 : 164 : bool EoPrinter::isHandledDistinctValues(const Node& n)
534 : : {
535 : 164 : std::unordered_set<TNode> visited;
536 : 164 : std::vector<TNode> visit;
537 : 164 : TNode cur;
538 : 164 : visit.push_back(n);
539 : : do
540 : : {
541 : 282 : cur = visit.back();
542 : 282 : visit.pop_back();
543 [ + + ]: 282 : if (visited.find(cur) == visited.end())
544 : : {
545 : 278 : visited.insert(cur);
546 : : // Note we don't currently handle constants in expert theories
547 : : // or array constants.
548 [ + + ][ + ]: 278 : switch (cur.getKind())
549 : : {
550 : 182 : case Kind::CONST_BOOLEAN:
551 : : case Kind::CONST_INTEGER:
552 : : case Kind::CONST_RATIONAL:
553 : : case Kind::CONST_STRING:
554 : : case Kind::CONST_BITVECTOR:
555 : : case Kind::SET_SINGLETON:
556 : : case Kind::SET_UNION:
557 : : case Kind::SET_EMPTY:
558 : : case Kind::APPLY_CONSTRUCTOR:
559 : 182 : case Kind::SEQ_UNIT: break;
560 : 24 : case Kind::CONST_SEQUENCE:
561 [ + + ]: 24 : if (!cur.getConst<Sequence>().empty())
562 : : {
563 : : // must traverse on component values
564 : 20 : cur = theory::strings::utils::mkConcatForConstSequence(cur);
565 : : }
566 : 24 : break;
567 : 72 : default:
568 [ + - ]: 144 : Trace("eo-printer-debug")
569 : 72 : << "Cannot distinct values " << cur.getKind() << std::endl;
570 : 72 : return false;
571 : : }
572 [ + + ]: 324 : for (const Node& cn : cur)
573 : : {
574 : 118 : visit.push_back(cn);
575 : 118 : }
576 : : }
577 [ + + ]: 210 : } while (!visit.empty());
578 : 92 : return true;
579 : 164 : }
580 : :
581 : 182 : bool EoPrinter::canEvaluateRegExp(Node r)
582 : : {
583 [ - + ][ - + ]: 182 : Assert(r.getType().isRegExp());
[ - - ]
584 [ + - ]: 182 : Trace("eo-printer-debug") << "canEvaluateRegExp? " << r << std::endl;
585 : 182 : std::unordered_set<TNode> visited;
586 : 182 : std::vector<TNode> visit;
587 : 182 : TNode cur;
588 : 182 : visit.push_back(r);
589 : : do
590 : : {
591 : 1072 : cur = visit.back();
592 : 1072 : visit.pop_back();
593 [ + + ]: 1072 : if (visited.find(cur) == visited.end())
594 : : {
595 : 648 : visited.insert(cur);
596 [ + + ][ + - ]: 648 : switch (cur.getKind())
597 : : {
598 : 414 : case Kind::REGEXP_ALL:
599 : : case Kind::REGEXP_ALLCHAR:
600 : : case Kind::REGEXP_COMPLEMENT:
601 : : case Kind::REGEXP_NONE:
602 : : case Kind::REGEXP_UNION:
603 : : case Kind::REGEXP_INTER:
604 : : case Kind::REGEXP_CONCAT:
605 : 414 : case Kind::REGEXP_STAR: break;
606 : 52 : case Kind::REGEXP_RANGE:
607 [ - + ]: 52 : if (!theory::strings::utils::isCharacterRange(cur))
608 : : {
609 [ - - ]: 0 : Trace("eo-printer-debug") << "Non-char range" << std::endl;
610 : 0 : return false;
611 : : }
612 : 52 : continue;
613 : 182 : case Kind::STRING_TO_REGEXP:
614 [ - + ]: 182 : if (!canEvaluate(cur[0]))
615 : : {
616 [ - - ]: 0 : Trace("eo-printer-debug") << "Non-evaluatable string" << std::endl;
617 : 0 : return false;
618 : : }
619 : 182 : continue;
620 : 0 : default:
621 [ - - ]: 0 : Trace("eo-printer-debug") << "Cannot evaluate " << cur.getKind()
622 : 0 : << " in regular expressions" << std::endl;
623 : 0 : return false;
624 : : }
625 [ + + ]: 1304 : for (const Node& cn : cur)
626 : : {
627 : 890 : visit.push_back(cn);
628 : 890 : }
629 : : }
630 [ + + ]: 1072 : } while (!visit.empty());
631 : 182 : return true;
632 : 182 : }
633 : :
634 : 4023607 : std::string EoPrinter::getRuleName(const ProofNode* pfn) const
635 : : {
636 : 4023607 : ProofRule r = pfn->getRule();
637 [ + + ]: 4023607 : if (r == ProofRule::DSL_REWRITE)
638 : : {
639 : : ProofRewriteRule id;
640 : 211809 : rewriter::getRewriteRule(pfn->getArguments()[0], id);
641 : 211809 : std::stringstream ss;
642 : 211809 : ss << id;
643 : 211809 : return ss.str();
644 : 211809 : }
645 [ + + ]: 3811798 : else if (r == ProofRule::THEORY_REWRITE)
646 : : {
647 : : ProofRewriteRule id;
648 : 13004 : rewriter::getRewriteRule(pfn->getArguments()[0], id);
649 : 13004 : std::stringstream ss;
650 : 13004 : ss << id;
651 : 13004 : return ss.str();
652 : 13004 : }
653 [ + + ][ + + ]: 3798794 : else if (r == ProofRule::ENCODE_EQ_INTRO || r == ProofRule::HO_APP_ENCODE
654 [ + + ]: 3792116 : || r == ProofRule::BV_EAGER_ATOM)
655 : : {
656 : : // ENCODE_EQ_INTRO proves (= t (convert t)) from argument t,
657 : : // where (convert t) is indistinguishable from t according to the proof.
658 : : // Similarly, HO_APP_ENCODE proves an equality between a term of kind
659 : : // Kind::HO_APPLY and Kind::APPLY_UF, which denotes the same term in Eunoia.
660 : : // BV_EAGER_ATOM also is indistinguishable as the eager atom predicate is
661 : : // ignored in the printer.
662 : 6686 : return "refl";
663 : : }
664 [ + + ]: 3792108 : else if (r == ProofRule::ACI_NORM)
665 : : {
666 : 50086 : Node eq = pfn->getArguments()[0];
667 [ - + ][ - + ]: 50086 : Assert(eq.getKind() == Kind::EQUAL);
[ - - ]
668 : : // may have to use the "expert" version.
669 : : Kind k;
670 : 100172 : if (eq[0].getKind() == eq[1].getKind()
671 : 100172 : || expr::getACINormalForm(eq[0]) == eq[1])
672 : : {
673 : 49906 : k = eq[0].getKind();
674 : : }
675 : : else
676 : : {
677 : 180 : k = eq[1].getKind();
678 : : }
679 : 50086 : std::stringstream ss;
680 : 50086 : ss << "aci_norm";
681 [ + + ]: 50086 : switch (k)
682 : : {
683 : 200 : case Kind::SEP_STAR:
684 : : case Kind::FINITE_FIELD_ADD:
685 : 200 : case Kind::FINITE_FIELD_MULT: ss << "_expert"; break;
686 : 49886 : default: break;
687 : : }
688 : 50086 : return ss.str();
689 : 50086 : }
690 : 7484044 : std::string name = toString(r);
691 : 3742022 : std::transform(name.begin(), name.end(), name.begin(), [](unsigned char c) {
692 : 29964812 : return std::tolower(c);
693 : : });
694 : 3742022 : return name;
695 : : }
696 : :
697 : 0 : void EoPrinter::printDslRule(std::ostream& out, ProofRewriteRule r)
698 : : {
699 : 0 : options::ioutils::applyPrintArithLitToken(out, true);
700 : 0 : options::ioutils::applyPrintSkolemDefinitions(out, true);
701 : 0 : const rewriter::RewriteProofRule& rpr = d_rdb->getRule(r);
702 : 0 : const std::vector<Node>& varList = rpr.getVarList();
703 : 0 : const std::vector<Node>& uvarList = rpr.getUserVarList();
704 : 0 : const std::vector<Node>& conds = rpr.getConditions();
705 : 0 : Node conc = rpr.getConclusion(true);
706 : : // We must map variables of the rule to internal symbols (via
707 : : // mkInternalSymbol) so that the Eunoia node converter will not treat the
708 : : // BOUND_VARIABLE of this rule as user provided variables. The substitution
709 : : // su stores this mapping.
710 : 0 : Subs su;
711 : 0 : out << "(declare-rule " << r << " (";
712 : 0 : EoDependentTypeConverter adtc(nodeManager(), d_tproc);
713 : 0 : std::stringstream ssExplicit;
714 : 0 : std::map<std::string, size_t> nameCount;
715 : 0 : std::vector<Node> uviList;
716 : 0 : std::map<Node, Node> adtcConvMap;
717 [ - - ]: 0 : for (size_t i = 0, nvars = uvarList.size(); i < nvars; i++)
718 : : {
719 [ - - ]: 0 : if (i > 0)
720 : : {
721 : 0 : ssExplicit << " ";
722 : : }
723 : 0 : const Node& uv = uvarList[i];
724 : 0 : std::stringstream sss;
725 : 0 : sss << uv;
726 : : // Use a consistent variable name, which e.g. ensures that minor changes
727 : : // to the RARE rules do not induce major changes in the CPC definition.
728 : : // Below, we have a variable when the user has named x (which itself may
729 : : // contain digits), and the cvc5 RARE parser has renamed to xN where N is
730 : : // <numeral>+. We rename this to xM where M is the number of times we have
731 : : // seen a variable with prefix M. For example, the variable `x1s2` may be
732 : : // renamed to `x1s2123`, which will be renamed to `x1s1` here.
733 : 0 : std::string str = sss.str();
734 : 0 : size_t index = str.find_last_not_of("0123456789");
735 : 0 : std::string result = str.substr(0, index + 1);
736 : 0 : sss.str("");
737 : 0 : nameCount[result]++;
738 : 0 : sss << result << nameCount[result];
739 : 0 : Node uvi = d_tproc.mkInternalSymbol(sss.str(), uv.getType());
740 : 0 : uviList.emplace_back(uvi);
741 : 0 : su.add(varList[i], uvi);
742 : 0 : ssExplicit << "(" << sss.str() << " ";
743 : 0 : TypeNode uvt = uv.getType();
744 : 0 : Node uvtp = adtc.process(uvt);
745 : 0 : adtcConvMap[uvi] = uvtp;
746 : 0 : ssExplicit << uvtp;
747 [ - - ]: 0 : if (expr::isListVar(uv))
748 : : {
749 : : // carry over whether it is a list variable
750 : 0 : expr::markListVar(uvi);
751 : 0 : ssExplicit << " :list";
752 : : }
753 : 0 : ssExplicit << ")";
754 : 0 : }
755 : : // print implicit parameters introduced in dependent type conversion
756 : 0 : const std::vector<Node>& params = adtc.getFreeParameters();
757 [ - - ]: 0 : for (const Node& p : params)
758 : : {
759 : 0 : out << "(" << p << " " << p.getType() << ") ";
760 : : }
761 : : // carry the mapping from symbols to their types, which is used when
762 : : // eliminating internal-only operators for representing empty set and sequence
763 : 0 : EoListNodeConverter ltproc(nodeManager(), d_tproc, adtcConvMap);
764 : : // now print variables of the proof rule
765 : 0 : out << ssExplicit.str();
766 : 0 : out << ")" << std::endl;
767 [ - - ]: 0 : if (!conds.empty())
768 : : {
769 : 0 : out << " :premises (";
770 : 0 : bool firstTime = true;
771 [ - - ]: 0 : for (const Node& c : conds)
772 : : {
773 [ - - ]: 0 : if (firstTime)
774 : : {
775 : 0 : firstTime = false;
776 : : }
777 : : else
778 : : {
779 : 0 : out << " ";
780 : : }
781 : : // note we apply list conversion to premises as well.
782 : 0 : Node cc = d_tproc.convert(su.apply(c));
783 : 0 : cc = ltproc.convert(cc);
784 : 0 : out << cc;
785 : 0 : }
786 : 0 : out << ")" << std::endl;
787 : : }
788 : 0 : out << " :args (";
789 : 0 : bool printedArg = false;
790 [ - - ]: 0 : for (const Node& v : uviList)
791 : : {
792 [ - - ]: 0 : out << (printedArg ? " " : "");
793 : 0 : printedArg = true;
794 : 0 : out << v;
795 : : }
796 : : // Special case: must print explicit types.
797 : : // This is to handle rules where Kind::TYPE_OF appears in the conclusion
798 : : // or in the premises. Since RARE rules do not take types as arguments,
799 : : // we must add them here. The printer for proof steps will add them in
800 : : // a similar manner.
801 : 0 : std::vector<Node> explictTypeOf = rpr.getExplicitTypeOfList();
802 : 0 : std::map<Node, Node>::iterator itet;
803 [ - - ]: 0 : for (const Node& et : explictTypeOf)
804 : : {
805 [ - - ]: 0 : out << (printedArg ? " " : "");
806 : 0 : printedArg = true;
807 : 0 : Assert(et.getKind() == Kind::TYPE_OF);
808 : 0 : Node v = su.apply(et[0]);
809 : 0 : itet = adtcConvMap.find(v);
810 : 0 : Assert(itet != adtcConvMap.end());
811 : 0 : out << itet->second;
812 : 0 : }
813 : 0 : out << ")" << std::endl;
814 : 0 : Node sconc = d_tproc.convert(su.apply(conc));
815 : 0 : Node rhs = ltproc.convert(sconc[1]);
816 : : // do not apply singleton elimination to head
817 : 0 : EoListNodeConverter ltprocNse(nodeManager(), d_tproc, adtcConvMap, false);
818 : 0 : Node lhs = ltprocNse.convert(sconc[0]);
819 : 0 : Assert(sconc.getKind() == Kind::EQUAL);
820 : 0 : out << " :conclusion (= " << lhs << " " << rhs << ")" << std::endl;
821 : 0 : out << ")" << std::endl;
822 : 0 : }
823 : :
824 : 0 : LetBinding* EoPrinter::getLetBinding() { return d_lbindUse; }
825 : :
826 : 2000 : void EoPrinter::printLetList(std::ostream& out, LetBinding& lbind)
827 : : {
828 : 2000 : std::vector<Node> letList;
829 : 2000 : lbind.letify(letList);
830 : 2000 : std::map<Node, size_t>::const_iterator it;
831 [ + + ]: 1110985 : for (size_t i = 0, nlets = letList.size(); i < nlets; i++)
832 : : {
833 : 1108985 : Node n = letList[i];
834 : : // use define command which does not invoke type checking
835 : 1108985 : out << "(define " << d_termLetPrefix << lbind.getId(n);
836 : 1108985 : out << " () ";
837 : 1108985 : Printer::getPrinter(out)->toStream(out, n, &lbind, false);
838 : 1108985 : out << ")" << std::endl;
839 : 1108985 : }
840 : 2000 : }
841 : :
842 : 2000 : void EoPrinter::print(std::ostream& out,
843 : : std::shared_ptr<ProofNode> pfn,
844 : : ProofScopeMode psm)
845 : : {
846 : : // ensures options are set once and for all
847 : 2000 : options::ioutils::applyOutputLanguage(out, Language::LANG_SMTLIB_V2_6);
848 : 2000 : options::ioutils::applyPrintArithLitToken(out, true);
849 : 2000 : options::ioutils::applyPrintSkolemDefinitions(out, true);
850 : : // allocate a print channel
851 : 2000 : EoPrintChannelOut aprint(out, d_lbindUse, d_termLetPrefix, true);
852 : 2000 : print(aprint, pfn, psm);
853 : 2000 : }
854 : :
855 : 2000 : void EoPrinter::print(EoPrintChannelOut& aout,
856 : : std::shared_ptr<ProofNode> pfn,
857 : : ProofScopeMode psm)
858 : : {
859 : 2000 : std::ostream& out = aout.getOStream();
860 [ - + ][ - + ]: 2000 : Assert(d_pletMap.empty());
[ - - ]
861 : 2000 : d_pfIdCounter = 0;
862 : :
863 : 2000 : const ProofNode* ascope = nullptr;
864 : 2000 : const ProofNode* dscope = nullptr;
865 : 2000 : const ProofNode* pnBody = nullptr;
866 [ - + ]: 2000 : if (psm == ProofScopeMode::NONE)
867 : : {
868 : 0 : pnBody = pfn.get();
869 : : }
870 [ - + ]: 2000 : else if (psm == ProofScopeMode::UNIFIED)
871 : : {
872 : 0 : ascope = pfn.get();
873 : 0 : Assert(ascope->getRule() == ProofRule::SCOPE);
874 : 0 : pnBody = pfn->getChildren()[0].get();
875 : : }
876 [ + - ]: 2000 : else if (psm == ProofScopeMode::DEFINITIONS_AND_ASSERTIONS)
877 : : {
878 : 2000 : dscope = pfn.get();
879 [ - + ][ - + ]: 2000 : Assert(dscope->getRule() == ProofRule::SCOPE);
[ - - ]
880 : 2000 : ascope = pfn->getChildren()[0].get();
881 [ - + ][ - + ]: 2000 : Assert(ascope->getRule() == ProofRule::SCOPE);
[ - - ]
882 : 2000 : pnBody = pfn->getChildren()[0]->getChildren()[0].get();
883 : : }
884 : :
885 : : // Get the definitions and assertions and print the declarations from them
886 : : const std::vector<Node>& definitions =
887 [ + - ]: 2000 : dscope != nullptr ? dscope->getArguments() : d_emptyVec;
888 : : const std::vector<Node>& assertions =
889 [ + - ]: 2000 : ascope != nullptr ? ascope->getArguments() : d_emptyVec;
890 : :
891 : : bool wasAlloc;
892 [ + + ]: 6000 : for (size_t i = 0; i < 2; i++)
893 : : {
894 : : EoPrintChannel* ao;
895 [ + + ]: 4000 : if (i == 0)
896 : : {
897 : 2000 : ao = &d_eletify;
898 : : }
899 : : else
900 : : {
901 : 2000 : ao = &aout;
902 : : }
903 [ + + ]: 4000 : if (i == 1)
904 : : {
905 : : // do not need to print DSL rules
906 [ + - ]: 2000 : if (!options().proof.proofPrintReference)
907 : : {
908 : : // [1] print the declarations
909 : 2000 : printer::smt2::Smt2Printer eprinter(printer::smt2::Variant::eo_variant);
910 : : // we do not print declarations in a sorted manner to reduce overhead
911 : 2000 : smt::PrintBenchmark pb(nodeManager(), &eprinter, false, &d_tproc);
912 : 2000 : std::stringstream outDecl;
913 : 2000 : std::stringstream outDef;
914 : 2000 : options::ioutils::applyPrintArithLitToken(outDef, true);
915 : 2000 : pb.printDeclarationsFrom(outDecl, outDef, definitions, assertions);
916 : 2000 : out << outDecl.str();
917 : : // [2] print the definitions
918 : 2000 : out << outDef.str();
919 : 2000 : }
920 : : // [3] print proof-level term bindings
921 : 2000 : printLetList(out, d_lbind);
922 : : }
923 : : // [4] print (unique) assumptions, including definitions
924 : 4000 : std::unordered_set<Node> processed;
925 [ + + ]: 37526 : for (const Node& n : assertions)
926 : : {
927 [ + + ]: 33526 : if (processed.find(n) != processed.end())
928 : : {
929 : 682 : continue;
930 : : }
931 : 32844 : processed.insert(n);
932 : 32844 : size_t id = allocateAssumeId(n, wasAlloc);
933 : 32844 : Node nc = d_tproc.convert(n);
934 : 32844 : ao->printAssume(nc, id, false);
935 : 32844 : }
936 [ + + ]: 5118 : for (const Node& n : definitions)
937 : : {
938 [ - + ]: 1118 : if (n.getKind() != Kind::EQUAL)
939 : : {
940 : : // skip define-fun-rec?
941 : 0 : continue;
942 : : }
943 [ - + ]: 1118 : if (processed.find(n) != processed.end())
944 : : {
945 : 0 : continue;
946 : : }
947 : 1118 : processed.insert(n);
948 : : // define-fun are HO equalities that can be proven by refl
949 : 1118 : size_t id = allocateAssumeId(n, wasAlloc);
950 : 1118 : Node f = d_tproc.convert(n[0]);
951 : 1118 : Node lam = d_tproc.convert(n[1]);
952 : 2236 : ao->printStep("refl", f.eqNode(lam), id, {}, {lam});
953 : 1118 : }
954 : : // [5] print proof body
955 : 4000 : printProofInternal(ao, pnBody, i == 1);
956 : 4000 : }
957 : 2000 : }
958 : :
959 : 0 : void EoPrinter::printNext(EoPrintChannelOut& aout,
960 : : std::shared_ptr<ProofNode> pfn)
961 : : {
962 : 0 : const ProofNode* pnBody = pfn.get();
963 : : // print with letification
964 : 0 : printProofInternal(&d_eletify, pnBody, false);
965 : : // print the new let bindings
966 : 0 : std::ostream& out = aout.getOStream();
967 : : // Print new terms from the let binding. note that this should print only
968 : : // the terms we have yet to see so far.
969 : 0 : printLetList(out, d_lbind);
970 : : // print the proof
971 : 0 : printProofInternal(&aout, pnBody, true);
972 : 0 : }
973 : :
974 : 4000 : void EoPrinter::printProofInternal(EoPrintChannel* out,
975 : : const ProofNode* pn,
976 : : bool addToCache)
977 : : {
978 : : // the stack
979 : 4000 : std::vector<const ProofNode*> visit;
980 : : // Whether we have to process children.
981 : : // This map is dependent on the proof assumption context, e.g. subproofs of
982 : : // SCOPE are reprocessed if they happen to occur in different proof scopes.
983 : 4000 : context::CDHashMap<const ProofNode*, bool> processingChildren(&d_passumeCtx);
984 : : // helper iterators
985 : 4000 : context::CDHashMap<const ProofNode*, bool>::iterator pit;
986 : : const ProofNode* cur;
987 : 4000 : visit.push_back(pn);
988 : : do
989 : : {
990 : 12898391 : cur = visit.back();
991 [ + + ]: 12898391 : if (d_alreadyPrinted.find(cur) != d_alreadyPrinted.end())
992 : : {
993 : 1736504 : visit.pop_back();
994 : 1736504 : continue;
995 : : }
996 : 11161887 : pit = processingChildren.find(cur);
997 [ + + ]: 11161887 : if (pit == processingChildren.end())
998 : : {
999 : 5395624 : ProofRule r = cur->getRule();
1000 [ + + ]: 5395624 : if (r == ProofRule::ASSUME)
1001 : : {
1002 : : // ignore
1003 : 1368401 : visit.pop_back();
1004 : 1368401 : continue;
1005 : : }
1006 : : // print preorder traversal
1007 : 4027223 : printStepPre(out, cur);
1008 : 4027223 : processingChildren[cur] = true;
1009 : : // will revisit this proof node
1010 : 4027223 : std::vector<std::shared_ptr<ProofNode>> children;
1011 : 4027223 : getChildrenFromProofRule(cur, children);
1012 : : // visit each child
1013 [ + + ]: 12894391 : for (const std::shared_ptr<ProofNode>& c : children)
1014 : : {
1015 : 8867168 : visit.push_back(c.get());
1016 : : }
1017 : 4027223 : continue;
1018 : 4027223 : }
1019 : 5766263 : visit.pop_back();
1020 [ + + ]: 5766263 : if (pit->second)
1021 : : {
1022 : 4027223 : processingChildren[cur] = false;
1023 : : // print postorder traversal
1024 : 4027223 : printStepPost(out, cur);
1025 [ + + ]: 4027223 : if (addToCache)
1026 : : {
1027 : 1995502 : d_alreadyPrinted.insert(cur);
1028 : : }
1029 : : }
1030 [ + + ]: 12898391 : } while (!visit.empty());
1031 : 4000 : }
1032 : :
1033 : 4027223 : void EoPrinter::printStepPre(EoPrintChannel* out, const ProofNode* pn)
1034 : : {
1035 : : // if we haven't yet allocated a proof id, do it now
1036 : 4027223 : ProofRule r = pn->getRule();
1037 [ + + ]: 4027223 : if (r == ProofRule::SCOPE)
1038 : : {
1039 : : // The assumptions only are valid within the body of the SCOPE, thus
1040 : : // we push a context scope.
1041 : 145214 : d_passumeCtx.push();
1042 : 145214 : const std::vector<Node>& args = pn->getArguments();
1043 [ + + ]: 1125942 : for (const Node& a : args)
1044 : : {
1045 : 980728 : size_t aid = allocateAssumePushId(pn, a);
1046 : 980728 : Node aa = d_tproc.convert(a);
1047 : : // print a push
1048 : 980728 : out->printAssume(aa, aid, true);
1049 : 980728 : }
1050 : : }
1051 : 4027223 : }
1052 : :
1053 : 8054446 : void EoPrinter::getChildrenFromProofRule(
1054 : : const ProofNode* pn, std::vector<std::shared_ptr<ProofNode>>& children)
1055 : : {
1056 : 8054446 : const std::vector<std::shared_ptr<ProofNode>>& cc = pn->getChildren();
1057 [ + + ]: 8054446 : switch (pn->getRule())
1058 : : {
1059 : 1179020 : case ProofRule::CONG:
1060 : : {
1061 : : // Ignore prefix of premises that are just REFL. Moreover this is required
1062 : : // to ensure CONG over APPLY_INDEXED_SYMBOLIC do not include premises
1063 : : // stating equality over indices to indexed operators, which cong does
1064 : : // not handle.
1065 : 1179020 : size_t start = 0;
1066 : 1179020 : while (start < cc.size()
1067 : 1633762 : && cc[start]->getResult()[0] == cc[start]->getResult()[1])
1068 : : {
1069 : 454742 : start++;
1070 : : }
1071 : 1179020 : Node res = pn->getResult();
1072 [ + + ]: 1179020 : if (res[0].isClosure())
1073 : : {
1074 : : // Ignore the children after the required arguments.
1075 : : // This ensures that we ignore e.g. equalities between patterns
1076 : : // which can appear in term conversion proofs.
1077 : 25388 : size_t arity = kind::metakind::getMinArityForKind(res[0].getKind());
1078 : 76164 : children.insert(
1079 : 76164 : children.end(), cc.begin() + start, cc.begin() + arity - 1);
1080 : 25388 : return;
1081 : : }
1082 [ + + ]: 1153632 : else if (start > 0)
1083 : : {
1084 : 441614 : children.insert(children.end(), cc.begin() + start, cc.end());
1085 : 441614 : return;
1086 : : }
1087 [ + + ]: 1179020 : }
1088 : 712018 : break;
1089 : 6875426 : default: break;
1090 : : }
1091 : 7587444 : children.insert(children.end(), cc.begin(), cc.end());
1092 : : }
1093 : :
1094 : 4023607 : void EoPrinter::getArgsFromProofRule(const ProofNode* pn,
1095 : : std::vector<Node>& args)
1096 : : {
1097 : 4023607 : Node res = pn->getResult();
1098 : 4023607 : const std::vector<Node> pargs = pn->getArguments();
1099 : 4023607 : ProofRule r = pn->getRule();
1100 [ + + ][ + + ]: 4023607 : switch (r)
[ + ]
1101 : : {
1102 : 952 : case ProofRule::HO_CONG:
1103 : : {
1104 : : // argument is ignored
1105 : 952 : return;
1106 : : }
1107 : 3536 : case ProofRule::INSTANTIATE:
1108 : : {
1109 : : // ignore arguments past the term vector
1110 : 3536 : Node ts = d_tproc.convert(pargs[0]);
1111 : 3536 : args.push_back(ts);
1112 : 3536 : return;
1113 : 3536 : }
1114 : 211809 : case ProofRule::DSL_REWRITE:
1115 : : {
1116 : : ProofRewriteRule dr;
1117 [ - + ]: 211809 : if (!rewriter::getRewriteRule(pargs[0], dr))
1118 : : {
1119 : 0 : Unhandled() << "Failed to get DSL proof rule";
1120 : : }
1121 [ + - ]: 211809 : Trace("eo-printer-debug") << "Get args for " << dr << std::endl;
1122 : 211809 : const rewriter::RewriteProofRule& rpr = d_rdb->getRule(dr);
1123 : 211809 : std::vector<Node> ss(pargs.begin() + 1, pargs.end());
1124 : 211809 : std::vector<std::pair<Kind, std::vector<Node>>> witnessTerms;
1125 : 211809 : rpr.getConclusionFor(ss, witnessTerms);
1126 : : // the arguments are the computed witness terms
1127 [ + + ]: 612984 : for (const std::pair<Kind, std::vector<Node>>& w : witnessTerms)
1128 : : {
1129 [ + + ]: 401175 : if (w.first == Kind::UNDEFINED_KIND)
1130 : : {
1131 [ - + ][ - + ]: 393590 : Assert(w.second.size() == 1);
[ - - ]
1132 : 393590 : args.push_back(d_tproc.convert(w.second[0]));
1133 : : }
1134 : : else
1135 : : {
1136 : 7585 : std::vector<Node> wargs;
1137 [ + + ]: 271480 : for (const Node& wc : w.second)
1138 : : {
1139 : 263895 : wargs.push_back(d_tproc.convert(wc));
1140 : : }
1141 : 7585 : args.push_back(d_tproc.mkInternalApp(
1142 : 15170 : printer::smt2::Smt2Printer::smtKindString(w.first),
1143 : : wargs,
1144 : 7585 : d_absType));
1145 : 7585 : }
1146 : : }
1147 : : // special case: explicit type-of terms, which require explicit type
1148 : : // arguments
1149 : : std::map<ProofRewriteRule, std::vector<Node>>::iterator it =
1150 : 211809 : d_explicitTypeOf.find(dr);
1151 [ + + ]: 211809 : if (it == d_explicitTypeOf.end())
1152 : : {
1153 : 10091 : d_explicitTypeOf[dr] = rpr.getExplicitTypeOfList();
1154 : 10091 : it = d_explicitTypeOf.find(dr);
1155 : : }
1156 [ + + ]: 211809 : if (!it->second.empty())
1157 : : {
1158 : 526 : const std::vector<Node>& fvs = rpr.getVarList();
1159 [ - + ][ - + ]: 526 : AlwaysAssert(fvs.size() == ss.size());
[ - - ]
1160 [ + + ]: 1052 : for (const Node& t : it->second)
1161 : : {
1162 [ - + ][ - + ]: 526 : Assert(t.getKind() == Kind::TYPE_OF);
[ - - ]
1163 : : Node tts =
1164 : 526 : t[0].substitute(fvs.begin(), fvs.end(), ss.begin(), ss.end());
1165 : 526 : args.push_back(d_tproc.typeAsNode(tts.getType()));
1166 : 526 : }
1167 : : }
1168 : 211809 : return;
1169 : 211809 : }
1170 : 13004 : case ProofRule::THEORY_REWRITE:
1171 : : {
1172 : : // ignore the identifier
1173 [ - + ][ - + ]: 13004 : Assert(pargs.size() == 2);
[ - - ]
1174 : 13004 : args.push_back(d_tproc.convert(pargs[1]));
1175 : 13004 : return;
1176 : : }
1177 : : break;
1178 : 3794306 : default: break;
1179 : : }
1180 [ + + ]: 7264868 : for (size_t i = 0, nargs = pargs.size(); i < nargs; i++)
1181 : : {
1182 : 3470562 : Node av = d_tproc.convert(pargs[i]);
1183 : 3470562 : args.push_back(av);
1184 : 3470562 : }
1185 [ + + ][ + + ]: 4252908 : }
1186 : :
1187 : 4027223 : void EoPrinter::printStepPost(EoPrintChannel* out, const ProofNode* pn)
1188 : : {
1189 [ - + ][ - + ]: 4027223 : Assert(pn->getRule() != ProofRule::ASSUME);
[ - - ]
1190 : : // if we have yet to allocate a proof id, do it now
1191 : 4027223 : bool wasAlloc = false;
1192 : 8054446 : TNode conclusion = d_tproc.convert(pn->getResult());
1193 : 4027223 : TNode conclusionPrint;
1194 : : // print conclusion only if option is set, or this is false
1195 [ + + ][ + + ]: 4027223 : if (options().proof.proofPrintConclusion || conclusion == d_false)
[ + + ]
1196 : : {
1197 : 3991765 : conclusionPrint = conclusion;
1198 : : }
1199 : 4027223 : ProofRule r = pn->getRule();
1200 : 4027223 : std::vector<std::shared_ptr<ProofNode>> children;
1201 : 4027223 : getChildrenFromProofRule(pn, children);
1202 : 4027223 : std::vector<Node> args;
1203 : 4027223 : bool handled = isHandled(options(), pn);
1204 [ + + ]: 4027223 : if (handled)
1205 : : {
1206 : 4023607 : getArgsFromProofRule(pn, args);
1207 : : }
1208 : 4027223 : size_t id = allocateProofId(pn, wasAlloc);
1209 : 4027223 : std::vector<size_t> premises;
1210 : : // get the premises
1211 : 4027223 : context::CDHashMap<Node, size_t>::iterator ita;
1212 : 4027223 : std::map<const ProofNode*, size_t>::iterator itp;
1213 [ + + ]: 12894391 : for (const std::shared_ptr<ProofNode>& c : children)
1214 : : {
1215 : : size_t pid;
1216 : : // if assume, lookup in passumeMap
1217 [ + + ]: 8867168 : if (c->getRule() == ProofRule::ASSUME)
1218 : : {
1219 : 1368371 : ita = d_passumeMap.find(c->getResult());
1220 [ - + ][ - + ]: 1368371 : Assert(ita != d_passumeMap.end());
[ - - ]
1221 : 1368371 : pid = ita->second;
1222 : : }
1223 : : else
1224 : : {
1225 : 7498797 : itp = d_pletMap.find(c.get());
1226 [ - + ][ - + ]: 7498797 : Assert(itp != d_pletMap.end());
[ - - ]
1227 : 7498797 : pid = itp->second;
1228 : : }
1229 : 8867168 : premises.push_back(pid);
1230 : : }
1231 : : // if we don't handle the rule, print trust
1232 [ + + ]: 4027223 : if (!handled)
1233 : : {
1234 [ - + ]: 3616 : if (!options().proof.proofAllowTrust)
1235 : : {
1236 : 0 : std::stringstream ss;
1237 : 0 : ss << pn->getRule();
1238 [ - - ]: 0 : if (pn->getRule() == ProofRule::THEORY_REWRITE)
1239 : : {
1240 : : ProofRewriteRule prid;
1241 : 0 : rewriter::getRewriteRule(pn->getArguments()[0], prid);
1242 : 0 : ss << " (" << prid << ")";
1243 : : }
1244 [ - - ]: 0 : else if (pn->getRule() == ProofRule::TRUST)
1245 : : {
1246 : : TrustId tid;
1247 : 0 : getTrustId(pn->getArguments()[0], tid);
1248 : 0 : ss << " (" << tid << ")";
1249 : : }
1250 : 0 : Trace("eo-pf-hole") << "Proof rule " << ss.str() << ": "
1251 : 0 : << pn->getResult() << std::endl;
1252 : 0 : Unreachable() << "A Eunoia proof requires a trust step for " << ss.str()
1253 : : << ", but --" << options::proof::longName::proofAllowTrust
1254 : 0 : << " is false" << std::endl;
1255 : 0 : }
1256 : 3616 : out->printTrustStep(pn->getRule(),
1257 : : conclusionPrint,
1258 : : id,
1259 : : premises,
1260 : : pn->getArguments(),
1261 : : conclusion);
1262 : 3616 : return;
1263 : : }
1264 : 4023607 : std::string rname = getRuleName(pn);
1265 [ + + ]: 4023607 : if (r == ProofRule::SCOPE)
1266 : : {
1267 [ - + ]: 145214 : if (args.empty())
1268 : : {
1269 : : // If there are no premises, any reference to this proof can just refer to
1270 : : // the body.
1271 : 0 : d_pletMap[pn] = premises[0];
1272 : : }
1273 : : else
1274 : : {
1275 : : // Assuming the body of the scope has identifier id_0, the following
1276 : : // prints: (step-pop id_1 :rule scope :premises (id_0))
1277 : : // ...
1278 : : // (step-pop id_n :rule scope :premises (id_{n-1}))
1279 : : // (step id :rule process_scope :premises (id_n) :args (C))
1280 : : size_t tmpId;
1281 [ + + ]: 1125942 : for (size_t i = 0, nargs = args.size(); i < nargs; i++)
1282 : : {
1283 : : // Manually increment proof id counter and premises. Note they will only
1284 : : // be used locally here to chain together the pops mentioned above.
1285 : 980728 : d_pfIdCounter++;
1286 : 980728 : tmpId = d_pfIdCounter;
1287 : 980728 : out->printStep(rname, Node::null(), tmpId, premises, {}, true);
1288 : : // The current id is the premises of the next.
1289 : 980728 : premises.clear();
1290 : 980728 : premises.push_back(tmpId);
1291 : : }
1292 : : // Finish with the process scope step.
1293 : 145214 : std::vector<Node> pargs;
1294 : 145214 : pargs.push_back(d_tproc.convert(children[0]->getResult()));
1295 : 145214 : out->printStep("process_scope", conclusionPrint, id, premises, pargs);
1296 : 145214 : }
1297 : : // We are done with the assumptions in scope, pop a context.
1298 : 145214 : d_passumeCtx.pop();
1299 : : }
1300 : : else
1301 : : {
1302 : 3878393 : out->printStep(rname, conclusionPrint, id, premises, args);
1303 : : }
1304 [ + + ][ + + ]: 4041687 : }
[ + + ][ + + ]
[ + + ]
1305 : :
1306 : 980728 : size_t EoPrinter::allocateAssumePushId(const ProofNode* pn, const Node& a)
1307 : : {
1308 : 980728 : std::pair<const ProofNode*, Node> key(pn, a);
1309 : :
1310 : 980728 : bool wasAlloc = false;
1311 : 980728 : size_t aid = allocateAssumeId(a, wasAlloc);
1312 : : // if we assigned an id to the assumption
1313 [ + + ]: 980728 : if (!wasAlloc)
1314 : : {
1315 : : // otherwise we shadow, just use a dummy
1316 : 339897 : d_pfIdCounter++;
1317 : 339897 : aid = d_pfIdCounter;
1318 : : }
1319 : 980728 : return aid;
1320 : 980728 : }
1321 : :
1322 : 1014690 : size_t EoPrinter::allocateAssumeId(const Node& n, bool& wasAlloc)
1323 : : {
1324 : 1014690 : context::CDHashMap<Node, size_t>::iterator it = d_passumeMap.find(n);
1325 [ + + ]: 1014690 : if (it != d_passumeMap.end())
1326 : : {
1327 : 356878 : wasAlloc = false;
1328 : 356878 : return it->second;
1329 : : }
1330 : 657812 : wasAlloc = true;
1331 : 657812 : d_pfIdCounter++;
1332 : 657812 : d_passumeMap[n] = d_pfIdCounter;
1333 : 657812 : return d_pfIdCounter;
1334 : : }
1335 : :
1336 : 4027223 : size_t EoPrinter::allocateProofId(const ProofNode* pn, bool& wasAlloc)
1337 : : {
1338 : 4027223 : std::map<const ProofNode*, size_t>::iterator it = d_pletMap.find(pn);
1339 [ + + ]: 4027223 : if (it != d_pletMap.end())
1340 : : {
1341 : 2333910 : wasAlloc = false;
1342 : 2333910 : return it->second;
1343 : : }
1344 : 1693313 : wasAlloc = true;
1345 : 1693313 : d_pfIdCounter++;
1346 : 1693313 : d_pletMap[pn] = d_pfIdCounter;
1347 : 1693313 : return d_pfIdCounter;
1348 : : }
1349 : :
1350 : : } // namespace proof
1351 : : } // namespace cvc5::internal
|
