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