Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Haniel Barbosa, Hanna Lachnitt, Aina Niemetz
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 by the authors listed in the file AUTHORS
8 : : * in the top-level source directory and their institutional affiliations.
9 : : * All rights reserved. See the file COPYING in the top-level source
10 : : * directory for licensing information.
11 : : * ****************************************************************************
12 : : *
13 : : * The module for processing proof nodes into Alethe proof nodes
14 : : */
15 : :
16 : : #include "proof/alethe/alethe_post_processor.h"
17 : :
18 : : #include <sstream>
19 : :
20 : : #include "expr/node_algorithm.h"
21 : : #include "expr/skolem_manager.h"
22 : : #include "proof/alethe/alethe_post_processor_algorithm.h"
23 : : #include "proof/alethe/alethe_proof_rule.h"
24 : : #include "proof/proof.h"
25 : : #include "proof/proof_checker.h"
26 : : #include "proof/proof_node_algorithm.h"
27 : : #include "proof/proof_node_manager.h"
28 : : #include "proof/resolution_proofs_util.h"
29 : : #include "rewriter/rewrite_proof_rule.h"
30 : : #include "smt/env.h"
31 : : #include "theory/builtin/proof_checker.h"
32 : : #include "util/rational.h"
33 : :
34 : : using namespace cvc5::internal::kind;
35 : :
36 : : namespace cvc5::internal {
37 : :
38 : : namespace proof {
39 : :
40 : : std::unordered_map<Kind, AletheRule> s_bvKindToAletheRule = {
41 : : {Kind::BITVECTOR_COMP, AletheRule::BV_BITBLAST_STEP_BVCOMP},
42 : : {Kind::BITVECTOR_ULT, AletheRule::BV_BITBLAST_STEP_BVULT},
43 : : {Kind::BITVECTOR_ULE, AletheRule::BV_BITBLAST_STEP_BVULE},
44 : : {Kind::BITVECTOR_SLT, AletheRule::BV_BITBLAST_STEP_BVSLT},
45 : : {Kind::BITVECTOR_AND, AletheRule::BV_BITBLAST_STEP_BVAND},
46 : : {Kind::BITVECTOR_OR, AletheRule::BV_BITBLAST_STEP_BVOR},
47 : : {Kind::BITVECTOR_XOR, AletheRule::BV_BITBLAST_STEP_BVXOR},
48 : : {Kind::BITVECTOR_XNOR, AletheRule::BV_BITBLAST_STEP_BVXNOR},
49 : : {Kind::BITVECTOR_NOT, AletheRule::BV_BITBLAST_STEP_BVNOT},
50 : : {Kind::BITVECTOR_ADD, AletheRule::BV_BITBLAST_STEP_BVADD},
51 : : {Kind::BITVECTOR_NEG, AletheRule::BV_BITBLAST_STEP_BVNEG},
52 : : {Kind::BITVECTOR_MULT, AletheRule::BV_BITBLAST_STEP_BVMULT},
53 : : {Kind::BITVECTOR_CONCAT, AletheRule::BV_BITBLAST_STEP_CONCAT},
54 : : {Kind::CONST_BITVECTOR, AletheRule::BV_BITBLAST_STEP_CONST},
55 : : {Kind::BITVECTOR_EXTRACT, AletheRule::BV_BITBLAST_STEP_EXTRACT},
56 : : {Kind::BITVECTOR_SIGN_EXTEND, AletheRule::BV_BITBLAST_STEP_SIGN_EXTEND},
57 : : {Kind::EQUAL, AletheRule::BV_BITBLAST_STEP_BVEQUAL},
58 : : };
59 : :
60 : 2116 : AletheProofPostprocessCallback::AletheProofPostprocessCallback(
61 : 2116 : Env& env, AletheNodeConverter& anc, bool resPivots)
62 : 2116 : : EnvObj(env), d_anc(anc), d_resPivots(resPivots)
63 : : {
64 : 2116 : NodeManager* nm = nodeManager();
65 : 2116 : d_cl = NodeManager::mkBoundVar("cl", nm->sExprType());
66 : 2116 : d_true = nm->mkConst(true);
67 : 2116 : d_false = nm->mkConst(false);
68 : 2116 : }
69 : :
70 : 2661 : const std::string& AletheProofPostprocessCallback::getError()
71 : : {
72 : 2661 : return d_reasonForConversionFailure;
73 : : }
74 : :
75 : 3048880 : bool AletheProofPostprocessCallback::shouldUpdate(
76 : : std::shared_ptr<ProofNode> pn,
77 : : CVC5_UNUSED const std::vector<Node>& fa,
78 : : CVC5_UNUSED bool& continueUpdate)
79 : : {
80 : 3048880 : return d_reasonForConversionFailure.empty()
81 [ + + ][ + + ]: 3048880 : && pn->getRule() != ProofRule::ALETHE_RULE;
82 : : }
83 : :
84 : 2154140 : bool AletheProofPostprocessCallback::shouldUpdatePost(
85 : : std::shared_ptr<ProofNode> pn, CVC5_UNUSED const std::vector<Node>& fa)
86 : : {
87 [ + + ][ - + ]: 2154140 : if (!d_reasonForConversionFailure.empty() || pn->getArguments().empty())
[ + + ]
88 : : {
89 : 280768 : return false;
90 : : }
91 : 1873370 : AletheRule rule = getAletheRule(pn->getArguments()[0]);
92 [ + + ]: 1760510 : return rule == AletheRule::RESOLUTION_OR || rule == AletheRule::REORDERING
93 [ + + ][ + + ]: 3633890 : || rule == AletheRule::CONTRACTION;
94 : : }
95 : :
96 : 24 : bool AletheProofPostprocessCallback::updateTheoryRewriteProofRewriteRule(
97 : : Node res,
98 : : const std::vector<Node>& children,
99 : : CVC5_UNUSED const std::vector<Node>& args,
100 : : CDProof* cdp,
101 : : ProofRewriteRule di)
102 : : {
103 : 24 : NodeManager* nm = nodeManager();
104 : 48 : std::vector<Node> new_args = std::vector<Node>();
105 [ + - ][ + - ]: 24 : switch (di)
[ - - ][ - - ]
[ - + ]
106 : : {
107 : : // ======== DISTINCT_ELIM
108 : : // ======== DISTINCT_CARD_CONFLICT
109 : : // Both rules are translated according to the clauses pattern to
110 : : // distinct_elim. The only exception to this is when DISTINCT_ELIM results
111 : : // in a term with exactly two boolean arguments. The Alethe distinct_elim
112 : : // rule has a special handling in this case and rewrites the distinct term
113 : : // to False directly (as the DISTINCT_CARD_CONFLICT rule does in cvc5).
114 : : // Instead, we output a RARE_REWRITE step using the distinct_two_bool_elim
115 : : // rule.
116 : : //
117 : : // (define-rule distinct_bin_bool_elim ((t1 Bool) (t2 Bool))
118 : : // (distinct t1 t2)
119 : : // (not (= t1 t2)))
120 : 1 : case ProofRewriteRule::DISTINCT_ELIM:
121 : : case ProofRewriteRule::DISTINCT_CARD_CONFLICT:
122 : : {
123 : 2 : Node eq = res[0];
124 : 2 : Node t1 = eq[0];
125 [ - + ][ - + ]: 2 : if (di == ProofRewriteRule::DISTINCT_ELIM && t1.getType().isBoolean()
[ - - ]
126 [ + - ][ - - ]: 2 : && eq.getNumChildren() == 2)
[ + - ]
127 : : {
128 : 0 : return addAletheStep(
129 : : AletheRule::RARE_REWRITE,
130 : : res,
131 : 0 : nm->mkNode(Kind::SEXPR, d_cl, res),
132 : : {},
133 : 0 : {nm->mkRawSymbol("\"distinct_bin_bool_elim\"", nm->sExprType()),
134 : : t1,
135 : : eq[1]},
136 : 0 : *cdp);
137 : : }
138 : 2 : return addAletheStep(AletheRule::DISTINCT_ELIM,
139 : : res,
140 : 2 : nm->mkNode(Kind::SEXPR, d_cl, res),
141 : : children,
142 : : new_args,
143 : 1 : *cdp);
144 : : }
145 : : // ======== EXISTS_ELIM
146 : : // This rule is translated according to the clause pattern.
147 : 0 : case ProofRewriteRule::EXISTS_ELIM:
148 : : {
149 : 0 : return addAletheStep(AletheRule::CONNECTIVE_DEF,
150 : : res,
151 : 0 : nm->mkNode(Kind::SEXPR, d_cl, res),
152 : : {},
153 : : {},
154 : 0 : *cdp);
155 : : }
156 : : // ======== QUANT_MERGE_PRENEX
157 : : // This rule is translated according to the clause pattern.
158 : 1 : case ProofRewriteRule::QUANT_MERGE_PRENEX:
159 : : {
160 : 4 : return addAletheStep(AletheRule::QNT_JOIN,
161 : : res,
162 : 2 : nm->mkNode(Kind::SEXPR, d_cl, res),
163 : : {},
164 : : {},
165 : 1 : *cdp);
166 : : }
167 : : // ======== QUANT_MINISCOPE_AND
168 : : // This rule is translated according to the clause pattern.
169 : 0 : case ProofRewriteRule::QUANT_MINISCOPE_AND:
170 : : {
171 : 0 : return addAletheStep(AletheRule::MINISCOPE_DISTRIBUTE,
172 : : res,
173 : 0 : nm->mkNode(Kind::SEXPR, d_cl, res),
174 : : {},
175 : : {},
176 : 0 : *cdp);
177 : : }
178 : : // ======== QUANT_MINISCOPE_OR
179 : : // This rule is translated according to the clause pattern.
180 : 0 : case ProofRewriteRule::QUANT_MINISCOPE_OR:
181 : : {
182 : 0 : return addAletheStep(AletheRule::MINISCOPE_SPLIT,
183 : : res,
184 : 0 : nm->mkNode(Kind::SEXPR, d_cl, res),
185 : : {},
186 : : {},
187 : 0 : *cdp);
188 : : }
189 : : // ======== QUANT_MINISCOPE_ITE
190 : : // This rule is translated according to the clause pattern.
191 : 0 : case ProofRewriteRule::QUANT_MINISCOPE_ITE:
192 : : {
193 : 0 : return addAletheStep(AletheRule::MINISCOPE_ITE,
194 : : res,
195 : 0 : nm->mkNode(Kind::SEXPR, d_cl, res),
196 : : {},
197 : : {},
198 : 0 : *cdp);
199 : : }
200 : : // ======== QUANT_UNUSED_VARS
201 : : // This rule is translated according to the clause pattern.
202 : 0 : case ProofRewriteRule::QUANT_UNUSED_VARS:
203 : : {
204 : 0 : return addAletheStep(AletheRule::QNT_RM_UNUSED,
205 : : res,
206 : 0 : nm->mkNode(Kind::SEXPR, d_cl, res),
207 : : {},
208 : : {},
209 : 0 : *cdp);
210 : : }
211 : : // ======== BV_BITWISE_SLICING
212 : : // This rule is translated according to the clause pattern.
213 : 0 : case ProofRewriteRule::BV_BITWISE_SLICING:
214 : : {
215 : 0 : return addAletheStep(AletheRule::BV_BITWISE_SLICING,
216 : : res,
217 : 0 : nm->mkNode(Kind::SEXPR, d_cl, res),
218 : : children,
219 : : {},
220 : 0 : *cdp);
221 : : }
222 : : // ======== BV_REPEAT_ELIM
223 : : // This rule is translated according to the clause pattern.
224 : 0 : case ProofRewriteRule::BV_REPEAT_ELIM:
225 : : {
226 : 0 : return addAletheStep(AletheRule::BV_REPEAT_ELIM,
227 : : res,
228 : 0 : nm->mkNode(Kind::SEXPR, d_cl, res),
229 : : children,
230 : : {},
231 : 0 : *cdp);
232 : : }
233 : 22 : default: break;
234 : : }
235 : 22 : return false;
236 : : }
237 : :
238 : 1146720 : bool AletheProofPostprocessCallback::update(Node res,
239 : : ProofRule id,
240 : : const std::vector<Node>& children,
241 : : const std::vector<Node>& args,
242 : : CDProof* cdp,
243 : : CVC5_UNUSED bool& continueUpdate)
244 : : {
245 [ + - ]: 2293450 : Trace("alethe-proof") << "...Alethe pre-update " << res << " " << id << " "
246 : 1146720 : << children << " / " << args << std::endl;
247 : :
248 : 1146720 : NodeManager* nm = nodeManager();
249 : 2293450 : std::vector<Node> new_args = std::vector<Node>();
250 : :
251 : : // See proof_rule.h for documentation on the proof rules translated below. Any
252 : : // comment might use variable names as introduced there.
253 [ + + ][ - + ]: 1146720 : switch (id)
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + - ][ - + ]
[ + - ][ - + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
254 : : {
255 : : // To keep the original shape of the proof node it is necessary to rederive
256 : : // the original conclusion. However, the term that should be printed might
257 : : // be different from that conclusion. Thus, it is stored as an additional
258 : : // argument in the proof node. Usually, the only difference is an additional
259 : : // cl operator or the outmost or operator being replaced by a cl operator.
260 : : //
261 : : // When steps are added to the proof that have not been there previously,
262 : : // it is unwise to add them in the same manner. To illustrate this the
263 : : // following counterexample shows the pitfalls of this approach:
264 : : //
265 : : // (or a (or b c)) (not a)
266 : : // --------------------------- RESOLUTION
267 : : // (or b c)
268 : : //
269 : : // is converted into an Alethe proof that should be printed as
270 : : //
271 : : // (cl a (or b c)) (cl (not a))
272 : : // -------------------------------- RESOLUTION
273 : : // (cl (or b c))
274 : : // --------------- OR
275 : : // (cl b c)
276 : : //
277 : : // Here, (cl (or b c)) and (cl b c) cannot correspond to the same proof node
278 : : // (or b c). Thus, we build a new proof node using the kind SEXPR
279 : : // that is then printed as (cl (or b c)).
280 : : //
281 : : // Adding an OR node to a premises will take place in the finalize function
282 : : // where in the case that a step is printed as (cl (or F1 ... Fn)) but used
283 : : // as (cl F1 ... Fn) an OR step is added to transform it to this very thing.
284 : : // This is necessary for rules that work on clauses, i.e. RESOLUTION,
285 : : // CHAIN_RESOLUTION, REORDERING and FACTORING.
286 : : //
287 : : // Some proof rules have a close correspondence in Alethe. There are two
288 : : // very frequent patterns that, to avoid repetition, are described here and
289 : : // referred to in the comments on the specific proof rules below.
290 : : //
291 : : // The first pattern, which will be called singleton pattern in the
292 : : // following, adds the original proof node F with the corresponding rule R'
293 : : // of the Alethe calculus and uses the same premises as the original proof
294 : : // node (P1:F1) ... (Pn:Fn). However, the conclusion is printed as (cl F).
295 : : //
296 : : // This means a cvc5 rule R that looks as follows:
297 : : //
298 : : // (P1:F1) ... (Pn:Fn)
299 : : // --------------------- R
300 : : // F
301 : : //
302 : : // is transformed into:
303 : : //
304 : : // (P1:F1) ... (Pn:Fn)
305 : : // --------------------- R'
306 : : // (cl F)*
307 : : //
308 : : // * the corresponding proof node is F
309 : : //
310 : : // The second pattern, which will be called clause pattern in the following,
311 : : // has a disjunction (or G1 ... Gn) as conclusion. It also adds the orignal
312 : : // proof node (or G1 ... Gn) with the corresponding rule R' of the Alethe
313 : : // calculus and uses the same premises as the original proof node (P1:F1)
314 : : // ... (Pn:Fn). However, the conclusion is printed as (cl G1 ... Gn), i.e.
315 : : // the or is replaced by the cl operator.
316 : : //
317 : : // This means a cvc5 rule R that looks as follows:
318 : : //
319 : : // (P1:F1) ... (Pn:Fn)
320 : : // --------------------- R
321 : : // (or G1 ... Gn)
322 : : //
323 : : // Is transformed into:
324 : : //
325 : : // (P1:F1) ... (Pn:Fn)
326 : : // --------------------- R'
327 : : // (cl G1 ... Gn)*
328 : : //
329 : : // * the corresponding proof node is (or G1 ... Gn)
330 : : //
331 : : // The documentation for each translation below will use variable names as
332 : : // defined in the original documentation of the rules in proof_rule.h.
333 : : //================================================= Core rules
334 : : //======================== Assume and Scope
335 : : // nothing happens
336 : 128756 : case ProofRule::ASSUME:
337 : : {
338 : 128756 : return false;
339 : : }
340 : : // The SCOPE rule is translated into Alethe using the "subproof" rule. The
341 : : // conclusion is either (=> (and F1 ... Fn) F) or (not (and F1 ... Fn)), so
342 : : // it must be converted into (cl (not F1) ... (not Fn) F), and extra steps
343 : : // must be added to derive the original conclusion, which is the one to be
344 : : // used in the steps depending on this one.
345 : : //
346 : : // The following transformation is applied. Let (not (and F1 ... Fn))^i
347 : : // denote the repetition of (not (and F1 ... Fn)) for i times.
348 : : //
349 : : // T1:
350 : : //
351 : : // -------------------------------- anchor
352 : : // ---- assume ---- assume
353 : : // F1 ... Fn
354 : : // ...
355 : : // -----
356 : : // F
357 : : // ----- subproof ------- ... ------- and_pos
358 : : // VP1 VP2_1 ... VP2_n
359 : : // ------------------------------------ resolution
360 : : // VP2a
361 : : // ------------------------------------ reordering
362 : : // VP2b
363 : : // ------ contraction ------- implies_neg1
364 : : // VP3 VP4
365 : : // ------------------------------------ resolution ------- implies_neg2
366 : : // VP5 VP6
367 : : // ----------------------------------------------------------- resolution
368 : : // VP7
369 : : //
370 : : // VP1: (cl (not F1) ... (not Fn) F)
371 : : // VP2_i: (cl (not (and F1 ... Fn)) Fi), for i = 1 to n
372 : : // VP2a: (cl F (not (and F1 ... Fn))^n)
373 : : // VP2b: (cl (not (and F1 ... Fn))^n F)
374 : : // VP3: (cl (not (and F1 ... Fn)) F)
375 : : // VP4: (cl (=> (and F1 ... Fn) F) (and F1 ... Fn)))
376 : : // VP5: (cl (=> (and F1 ... Fn) F) F)
377 : : // VP6: (cl (=> (and F1 ... Fn) F) (not F))
378 : : // VP7: (cl (=> (and F1 ... Fn) F) (=> (and F1 ... Fn) F))
379 : : //
380 : : // Note that if n = 1, then the "subproof" step yields (cl (not F1) F),
381 : : // which is the same as VP3. Since VP1 = VP3, the steps for that
382 : : // transformation are not generated.
383 : : //
384 : : //
385 : : // If F = false:
386 : : //
387 : : // --------- implies_simplify
388 : : // T1 VP9
389 : : // --------- contraction --------- equiv_1
390 : : // VP8 VP10
391 : : // -------------------------------------------- resolution
392 : : // (cl (not (and F1 ... Fn)))*
393 : : //
394 : : // VP8: (cl (=> (and F1 ... Fn) false))
395 : : // VP9: (cl (= (=> (and F1 ... Fn) false) (not (and F1 ... Fn))))
396 : : // VP10: (cl (not (=> (and F1 ... Fn) false)) (not (and F1 ... Fn)))
397 : : //
398 : : // Otherwise,
399 : : // T1
400 : : // ------------------------------ contraction
401 : : // (cl (=> (and F1 ... Fn) F))**
402 : : //
403 : : //
404 : : // * the corresponding proof node is (not (and F1 ... Fn))
405 : : // ** the corresponding proof node is (=> (and F1 ... Fn) F)
406 : 34416 : case ProofRule::SCOPE:
407 : : {
408 : 34416 : bool success = true;
409 : :
410 : : // Build vp1
411 : 137664 : std::vector<Node> negNode{d_cl};
412 [ + + ]: 217894 : for (const Node& arg : args)
413 : : {
414 : 183478 : negNode.push_back(arg.notNode()); // (not F1) ... (not Fn)
415 : : }
416 : 34416 : negNode.push_back(children[0]); // (cl (not F1) ... (not Fn) F)
417 : 68832 : Node vp1 = nm->mkNode(Kind::SEXPR, negNode);
418 : 68832 : success &= addAletheStep(
419 : 34416 : AletheRule::ANCHOR_SUBPROOF, vp1, vp1, children, args, *cdp);
420 : :
421 : 68832 : Node andNode, vp3;
422 [ + + ]: 34416 : if (args.size() == 1)
423 : : {
424 : 7179 : vp3 = vp1;
425 : 7179 : andNode = args[0]; // F1
426 : : }
427 : : else
428 : : {
429 : : // Build vp2i
430 : 27237 : andNode = nm->mkNode(Kind::AND, args); // (and F1 ... Fn)
431 : 108948 : std::vector<Node> premisesVP2 = {vp1};
432 : 136185 : std::vector<Node> notAnd = {d_cl, children[0]}; // cl F
433 : 54474 : Node vp2_i;
434 [ + + ]: 203536 : for (size_t i = 0, size = args.size(); i < size; i++)
435 : : {
436 : 176299 : vp2_i = nm->mkNode(Kind::SEXPR, d_cl, andNode.notNode(), args[i]);
437 : 352598 : success &= addAletheStep(AletheRule::AND_POS,
438 : : vp2_i,
439 : : vp2_i,
440 : : {},
441 : 528897 : std::vector<Node>{nm->mkConstInt(i)},
442 : 176299 : *cdp);
443 : 176299 : premisesVP2.push_back(vp2_i);
444 : 176299 : notAnd.push_back(andNode.notNode()); // cl F (not (and F1 ... Fn))^i
445 : : }
446 : :
447 : 54474 : Node vp2a = nm->mkNode(Kind::SEXPR, notAnd);
448 [ + + ]: 27237 : if (d_resPivots)
449 : : {
450 : 10 : std::vector<Node> newArgs;
451 [ + + ]: 43 : for (const Node& arg : args)
452 : : {
453 : 33 : newArgs.push_back(arg);
454 : 33 : newArgs.push_back(d_false);
455 : : }
456 : 20 : success &= addAletheStep(
457 : 10 : AletheRule::RESOLUTION, vp2a, vp2a, premisesVP2, newArgs, *cdp);
458 : : }
459 : : else
460 : : {
461 : 54454 : success &= addAletheStep(AletheRule::RESOLUTION,
462 : : vp2a,
463 : : vp2a,
464 : : premisesVP2,
465 : 54454 : std::vector<Node>(),
466 : 27227 : *cdp);
467 : : }
468 : :
469 : 27237 : notAnd.erase(notAnd.begin() + 1); //(cl (not (and F1 ... Fn))^n)
470 : 27237 : notAnd.push_back(children[0]); //(cl (not (and F1 ... Fn))^n F)
471 : 27237 : Node vp2b = nm->mkNode(Kind::SEXPR, notAnd);
472 : 27237 : success &=
473 : 54474 : addAletheStep(AletheRule::REORDERING, vp2b, vp2b, {vp2a}, {}, *cdp);
474 : :
475 : 27237 : vp3 = nm->mkNode(Kind::SEXPR, d_cl, andNode.notNode(), children[0]);
476 : 27237 : success &=
477 : 54474 : addAletheStep(AletheRule::CONTRACTION, vp3, vp3, {vp2b}, {}, *cdp);
478 : : }
479 : :
480 : : Node vp8 = nm->mkNode(
481 : 103248 : Kind::SEXPR, d_cl, nm->mkNode(Kind::IMPLIES, andNode, children[0]));
482 : :
483 : 103248 : Node vp4 = nm->mkNode(Kind::SEXPR, d_cl, vp8[1], andNode);
484 : 34416 : success &=
485 : 34416 : addAletheStep(AletheRule::IMPLIES_NEG1, vp4, vp4, {}, {}, *cdp);
486 : :
487 : 103248 : Node vp5 = nm->mkNode(Kind::SEXPR, d_cl, vp8[1], children[0]);
488 [ + + ][ - - ]: 137664 : success &= addAletheStep(AletheRule::RESOLUTION,
489 : : vp5,
490 : : vp5,
491 : : {vp4, vp3},
492 : 68854 : d_resPivots ? std::vector<Node>{andNode, d_true}
493 : : : std::vector<Node>(),
494 : 103248 : *cdp);
495 : :
496 : 103248 : Node vp6 = nm->mkNode(Kind::SEXPR, d_cl, vp8[1], children[0].notNode());
497 : 34416 : success &=
498 : 34416 : addAletheStep(AletheRule::IMPLIES_NEG2, vp6, vp6, {}, {}, *cdp);
499 : :
500 : 68832 : Node vp7 = nm->mkNode(Kind::SEXPR, d_cl, vp8[1], vp8[1]);
501 : 34416 : success &=
502 [ + + ][ - - ]: 137664 : addAletheStep(AletheRule::RESOLUTION,
503 : : vp7,
504 : : vp7,
505 : : {vp5, vp6},
506 : 68854 : d_resPivots ? std::vector<Node>{children[0], d_true}
507 : : : std::vector<Node>(),
508 : 103248 : *cdp);
509 : :
510 [ + + ]: 34416 : if (children[0] != d_false)
511 : : {
512 : 25366 : success &=
513 : 50732 : addAletheStep(AletheRule::CONTRACTION, res, vp8, {vp7}, {}, *cdp);
514 : : }
515 : : else
516 : : {
517 : 9050 : success &=
518 : 18100 : addAletheStep(AletheRule::CONTRACTION, vp8, vp8, {vp7}, {}, *cdp);
519 : :
520 : : Node vp9 =
521 : : nm->mkNode(Kind::SEXPR,
522 : 9050 : d_cl,
523 : 27150 : nm->mkNode(Kind::EQUAL, vp8[1], andNode.notNode()));
524 : 9050 : success &=
525 : 9050 : addAletheStep(AletheRule::IMPLIES_SIMPLIFY, vp9, vp9, {}, {}, *cdp);
526 : :
527 : : Node vp10 =
528 : 18100 : nm->mkNode(Kind::SEXPR, d_cl, vp8[1].notNode(), andNode.notNode());
529 : 9050 : success &=
530 : 18100 : addAletheStep(AletheRule::EQUIV1, vp10, vp10, {vp9}, {}, *cdp);
531 : :
532 [ + + ][ - - ]: 45250 : success &= addAletheStep(AletheRule::RESOLUTION,
533 : : res,
534 : 18100 : nm->mkNode(Kind::SEXPR, d_cl, res),
535 : : {vp8, vp10},
536 : 18100 : d_resPivots ? std::vector<Node>{vp8[1], d_true}
537 : : : std::vector<Node>(),
538 : 27150 : *cdp);
539 : : }
540 : :
541 : 34416 : return success;
542 : : }
543 : : // ======== Absorb
544 : : //
545 : : // ------- ac_simp ------- <op>_simplify
546 : : // VP1 VP2
547 : : // ------------------------- trans
548 : : // res
549 : : //
550 : : // VP1: (cl (= t tf))
551 : : // VP2: (cl (= tf z))
552 : : //
553 : : // where tf = applyAcSimp(t) and <op> is the top-level operator of t. Note
554 : : // that ac_simp is over-eager in flattening the formula but since this step
555 : : // simplifies to a zero element this does not matter and only impacts
556 : : // performance marginally.
557 : 0 : case ProofRule::ABSORB:
558 : : {
559 : 0 : std::map<Node, Node> emptyMap;
560 : 0 : Node t = res[0];
561 : 0 : Node tf = applyAcSimp(d_env, emptyMap, t);
562 : 0 : Kind k = res.getKind();
563 : : // if the simplification did not result in a term that would simplify to
564 : : // the expected constant, abort. For this the kind of tf must be the same
565 : : // as of t and one of its arguments must be res[1].
566 : 0 : bool success = false;
567 [ - - ]: 0 : for (const Node& ch : tf)
568 : : {
569 [ - - ]: 0 : if (ch == res[1])
570 : : {
571 : 0 : success = true;
572 : 0 : break;
573 : : }
574 : : }
575 : 0 : if (!success || k != tf.getKind())
576 : : {
577 : 0 : return addAletheStep(AletheRule::HOLE,
578 : : res,
579 : 0 : nm->mkNode(Kind::SEXPR, d_cl, res),
580 : : {},
581 : : {},
582 : 0 : *cdp);
583 : : }
584 : 0 : Node vp1 = nm->mkNode(Kind::EQUAL, t, tf);
585 : 0 : Node vp2 = nm->mkNode(Kind::EQUAL, tf, res[1]);
586 : : // if the kind was not one of these, the simplification above would have failed
587 : 0 : Assert(k == Kind::OR || k == Kind::AND);
588 : 0 : AletheRule rule =
589 [ - - ]: 0 : k == Kind::OR ? AletheRule::OR_SIMPLIFY : AletheRule::AND_SIMPLIFY;
590 [ - - ][ - - ]: 0 : return addAletheStep(AletheRule::AC_SIMP,
[ - - ][ - - ]
591 : : vp1,
592 : 0 : nm->mkNode(Kind::SEXPR, d_cl, vp1),
593 : : {},
594 : : {},
595 : : *cdp)
596 : 0 : && addAletheStep(
597 : 0 : rule, vp2, nm->mkNode(Kind::SEXPR, d_cl, vp2), {}, {}, *cdp)
598 : 0 : && addAletheStep(AletheRule::TRANS,
599 : : res,
600 : 0 : nm->mkNode(Kind::SEXPR, d_cl, res),
601 : : {vp1, vp2},
602 : : {},
603 [ - - ]: 0 : *cdp);
604 : : }
605 : : // ======== Encode equality introduction
606 : : // This rule is translated according to the singleton pattern.
607 : 6 : case ProofRule::ENCODE_EQ_INTRO:
608 : : {
609 : 24 : return addAletheStep(AletheRule::REFL,
610 : : res,
611 : 12 : nm->mkNode(Kind::SEXPR, d_cl, res),
612 : : {},
613 : : {},
614 : 6 : *cdp);
615 : : }
616 : : // The conversion is into a "rare_rewrite" step where the first argument is
617 : : // a string literal with the name of the rewrite, followed by the arguments,
618 : : // where lists are built using the Alethe operator "rare-list", which takes
619 : : // 0 or more arguments.
620 : 3409 : case ProofRule::DSL_REWRITE:
621 : : {
622 : : // get the name
623 : : ProofRewriteRule di;
624 : 3409 : Node rule;
625 [ + - ]: 3409 : if (rewriter::getRewriteRule(args[0], di))
626 : : {
627 : 3409 : std::stringstream ss;
628 : 3409 : ss << "\"" << di << "\"";
629 : 3409 : rule = NodeManager::mkRawSymbol(ss.str(), nm->sExprType());
630 : : }
631 : : else
632 : : {
633 : 0 : Unreachable();
634 : : }
635 : 3409 : new_args.push_back(rule);
636 [ + + ]: 9587 : for (int i = 1, size = args.size(); i < size; i++)
637 : : {
638 [ + - ]: 6178 : if (!args[i].isNull())
639 : : {
640 [ - + ]: 6178 : if (args[i].toString() == "")
641 : : { // TODO: better way
642 : 0 : new_args.push_back(
643 : 0 : NodeManager::mkBoundVar("rare-list", nm->sExprType()));
644 : : }
645 [ - + ]: 6178 : else if (args[i].getKind() == Kind::SEXPR)
646 : : {
647 : : std::vector<Node> list_arg{
648 : 0 : NodeManager::mkBoundVar("rare-list", nm->sExprType())};
649 : 0 : list_arg.insert(list_arg.end(), args[i].begin(), args[i].end());
650 : 0 : new_args.push_back(nm->mkNode(Kind::SEXPR, list_arg));
651 : : }
652 : : else
653 : : {
654 : 6178 : new_args.push_back(args[i]);
655 : : }
656 : : }
657 : : }
658 : 6818 : return addAletheStep(AletheRule::RARE_REWRITE,
659 : : res,
660 : 6818 : nm->mkNode(Kind::SEXPR, d_cl, res),
661 : : children,
662 : : new_args,
663 : 3409 : *cdp);
664 : : }
665 : 24 : case ProofRule::THEORY_REWRITE:
666 : : {
667 : : ProofRewriteRule di;
668 : :
669 [ + - ]: 24 : if (rewriter::getRewriteRule(args[0], di))
670 : : {
671 [ + + ]: 24 : if (updateTheoryRewriteProofRewriteRule(res, children, args, cdp, di))
672 : : {
673 : 2 : return true;
674 : : }
675 : 22 : std::stringstream ss;
676 : 22 : ss << "\"" << di << "\"";
677 : 22 : new_args.push_back(NodeManager::mkRawSymbol(ss.str(), nm->sExprType()));
678 : : }
679 : 44 : return addAletheStep(AletheRule::HOLE,
680 : : res,
681 : 44 : nm->mkNode(Kind::SEXPR, d_cl, res),
682 : : children,
683 : : new_args,
684 : 22 : *cdp);
685 : : }
686 : : // Both ARITH_POLY_NORM and EVALUATE, which are used by the Rare
687 : : // elaboration, are captured by the "rare_rewrite" rule.
688 : 428 : case ProofRule::ARITH_POLY_NORM:
689 : : {
690 : 2140 : return addAletheStep(
691 : : AletheRule::RARE_REWRITE,
692 : : res,
693 : 856 : nm->mkNode(Kind::SEXPR, d_cl, res),
694 : : children,
695 : 856 : {NodeManager::mkRawSymbol("\"arith-poly-norm\"", nm->sExprType())},
696 : 856 : *cdp);
697 : : }
698 : 3106 : case ProofRule::EVALUATE:
699 : : {
700 : 15530 : return addAletheStep(
701 : : AletheRule::RARE_REWRITE,
702 : : res,
703 : 6212 : nm->mkNode(Kind::SEXPR, d_cl, res),
704 : : children,
705 : 6212 : {NodeManager::mkRawSymbol("\"evaluate\"", nm->sExprType())},
706 : 6212 : *cdp);
707 : : }
708 : : // If the trusted rule is a theory lemma from arithmetic, we try to phrase
709 : : // it with "lia_generic".
710 : 5608 : case ProofRule::TRUST:
711 : : {
712 : : // check for case where the trust step is introducing an equality between
713 : : // a term and another whose Alethe conversion is itself, in which case we
714 : : // justify this as a REFL step. This happens with trusted purification
715 : : // steps, for example.
716 : 11216 : Node resConv = d_anc.maybeConvert(res);
717 [ + + ]: 5607 : if (!resConv.isNull() && resConv.getKind() == Kind::EQUAL
718 : 11215 : && resConv[0] == resConv[1])
719 : : {
720 : 0 : return addAletheStep(AletheRule::REFL,
721 : : res,
722 : 0 : nm->mkNode(Kind::SEXPR, d_cl, res),
723 : : children,
724 : : {},
725 : 0 : *cdp);
726 : : }
727 : : TrustId tid;
728 : 5608 : bool hasTrustId = getTrustId(args[0], tid);
729 [ + - ][ + + ]: 5608 : if (hasTrustId && tid == TrustId::THEORY_LEMMA)
730 : : {
731 : : // if we are in the arithmetic case, we rather add a LIA_GENERIC step
732 [ - + ][ - - ]: 24 : if (res.getKind() == Kind::NOT && res[0].getKind() == Kind::AND)
[ - + ][ - + ]
[ - - ]
733 : : {
734 [ - - ]: 0 : Trace("alethe-proof") << "... test each arg if ineq\n";
735 : 0 : bool allIneqs = true;
736 [ - - ]: 0 : for (const Node& arg : res[0])
737 : : {
738 [ - - ]: 0 : Node toTest = arg.getKind() == Kind::NOT ? arg[0] : arg;
739 : 0 : Kind k = toTest.getKind();
740 [ - - ][ - - ]: 0 : if (k != Kind::LT && k != Kind::LEQ && k != Kind::GT
[ - - ]
741 [ - - ][ - - ]: 0 : && k != Kind::GEQ && k != Kind::EQUAL)
742 : : {
743 [ - - ]: 0 : Trace("alethe-proof") << "... arg " << arg << " not ineq\n";
744 : 0 : allIneqs = false;
745 : 0 : break;
746 : : }
747 : : }
748 [ - - ]: 0 : if (allIneqs)
749 : : {
750 : 0 : return addAletheStep(AletheRule::LIA_GENERIC,
751 : : res,
752 : 0 : nm->mkNode(Kind::SEXPR, d_cl, res),
753 : : children,
754 : : {},
755 : 0 : *cdp);
756 : : }
757 : : }
758 : : }
759 : 11216 : std::stringstream ss;
760 [ + - ]: 5608 : if (hasTrustId)
761 : : {
762 : 5608 : ss << "\"" << tid << "\"";
763 : : cvc5::internal::theory::TheoryId thid;
764 [ + - ]: 5608 : if (theory::builtin::BuiltinProofRuleChecker::getTheoryId(args[0],
765 : : thid))
766 : : {
767 : 5608 : ss << " \"" << thid << "\"";
768 : : }
769 : : }
770 : : else
771 : : {
772 : 0 : ss << "\"" << args[0] << "\"";
773 : : }
774 : : std::vector<Node> newArgs{
775 : 22432 : NodeManager::mkRawSymbol(ss.str(), nm->sExprType())};
776 : 5608 : newArgs.insert(newArgs.end(), args.begin() + 1, args.end());
777 : 11216 : return addAletheStep(AletheRule::HOLE,
778 : : res,
779 : 11216 : nm->mkNode(Kind::SEXPR, d_cl, res),
780 : : children,
781 : : newArgs,
782 : 5608 : *cdp);
783 : : }
784 : : // ======== Resolution and N-ary Resolution
785 : : // Because the RESOLUTION rule is merely a special case of CHAIN_RESOLUTION,
786 : : // the same translation can be used for both.
787 : : //
788 : : // The main complication for the translation of the rule is that in the case
789 : : // that the conclusion is (or G1 ... Gn), the result is ambigous. E.g.,
790 : : //
791 : : // (cl F1 (or F2 F3)) (cl (not F1))
792 : : // -------------------------------------- resolution
793 : : // (cl (or F2 F3))
794 : : //
795 : : // (cl F1 F2 F3) (cl (not F1))
796 : : // -------------------------------------- resolution
797 : : // (cl F2 F3)
798 : : //
799 : : // both (cl (or F2 F3)) and (cl F2 F3) could be represented by the same node
800 : : // (or F2 F3). Thus, it has to be checked if the conclusion C is a singleton
801 : : // clause or not.
802 : : //
803 : : // If C = (or F1 ... Fn) is a non-singleton clause, then:
804 : : //
805 : : // VP1 ... VPn
806 : : // ------------------ resolution
807 : : // (cl F1 ... Fn)*
808 : : //
809 : : // Else if, C = false:
810 : : //
811 : : // VP1 ... VPn
812 : : // ------------------ resolution
813 : : // (cl)*
814 : : //
815 : : // Otherwise:
816 : : //
817 : : // VP1 ... VPn
818 : : // ------------------ resolution
819 : : // (cl C)*
820 : : //
821 : : // * the corresponding proof node is C
822 : 60134 : case ProofRule::RESOLUTION:
823 : : case ProofRule::CHAIN_RESOLUTION:
824 : : case ProofRule::CHAIN_M_RESOLUTION:
825 : : {
826 : 120268 : std::vector<Node> cargs;
827 [ + + ]: 60134 : if (id == ProofRule::CHAIN_RESOLUTION)
828 : : {
829 [ + + ]: 123 : for (size_t i = 0, nargs = args[0].getNumChildren(); i < nargs; i++)
830 : : {
831 : 80 : cargs.push_back(args[0][i]);
832 : 80 : cargs.push_back(args[1][i]);
833 : : }
834 : : }
835 [ + + ]: 60091 : else if (id == ProofRule::CHAIN_M_RESOLUTION)
836 : : {
837 [ + - ][ + - ]: 98948 : Assert(args.size() == 3
[ - + ][ - - ]
838 : : && args[1].getNumChildren() == args[2].getNumChildren());
839 : : // Alethe expects the polarity/literals to be interleaved
840 [ + + ]: 1689390 : for (size_t i = 0, nsteps = args[1].getNumChildren(); i < nsteps; i++)
841 : : {
842 : 1639910 : cargs.push_back(args[1][i]);
843 : 1639910 : cargs.push_back(args[2][i]);
844 : : }
845 : : }
846 : : else
847 : : {
848 : 10617 : cargs = args;
849 : : }
850 : 120268 : Node conclusion;
851 [ + + ]: 60134 : if (!isSingletonClause(res, children, cargs))
852 : : {
853 : 131754 : std::vector<Node> concChildren{d_cl};
854 : 43918 : concChildren.insert(concChildren.end(), res.begin(), res.end());
855 : 43918 : conclusion = nm->mkNode(Kind::SEXPR, concChildren);
856 : : }
857 [ + + ]: 16216 : else if (res == d_false)
858 : : {
859 : 1212 : conclusion = nm->mkNode(Kind::SEXPR, d_cl);
860 : : }
861 : : else
862 : : {
863 : 15004 : conclusion = nm->mkNode(Kind::SEXPR, d_cl, res);
864 : : }
865 : : // checker expects opposite order. We always keep the pivots because we
866 : : // need them to compute in updatePost whether we will add OR steps. If
867 : : // d_resPivots is off we will remove the pivots after that.
868 : 60134 : std::vector<Node> newArgs;
869 [ + + ]: 1710740 : for (size_t i = 0, size = cargs.size(); i < size; i = i + 2)
870 : : {
871 : 1650610 : newArgs.push_back(cargs[i + 1]);
872 : 1650610 : newArgs.push_back(cargs[i]);
873 : : }
874 : 120268 : return addAletheStep(
875 : 60134 : AletheRule::RESOLUTION_OR, res, conclusion, children, newArgs, *cdp);
876 : : }
877 : : // ======== Factoring
878 : : //
879 : : // If C2 = (or F1 ... Fn) but C1 != (or C2 ... C2), then VC2 = (cl F1 ...
880 : : // Fn) Otherwise, VC2 = (cl C2).
881 : : //
882 : : // P
883 : : // ------- contraction
884 : : // VC2*
885 : : //
886 : : // * the corresponding proof node is C2
887 : 74 : case ProofRule::FACTORING:
888 : : {
889 [ + - ]: 74 : if (res.getKind() == Kind::OR)
890 : : {
891 [ + - ]: 74 : for (const Node& child : children[0])
892 : : {
893 [ + - ]: 74 : if (child != res)
894 : : {
895 : 148 : return addAletheStepFromOr(
896 : 74 : AletheRule::CONTRACTION, res, children, {}, *cdp);
897 : : }
898 : : }
899 : : }
900 : 0 : return addAletheStep(AletheRule::CONTRACTION,
901 : : res,
902 : 0 : nm->mkNode(Kind::SEXPR, d_cl, res),
903 : : children,
904 : : {},
905 : 0 : *cdp);
906 : : }
907 : : // ======== Reordering
908 : : // This rule is translated according to the clauses pattern.
909 : 55374 : case ProofRule::REORDERING:
910 : : {
911 : 110748 : return addAletheStepFromOr(
912 : 55374 : AletheRule::REORDERING, res, children, {}, *cdp);
913 : : }
914 : : // ======== Split
915 : : //
916 : : // --------- not_not --------- not_not
917 : : // VP1 VP2
918 : : // -------------------------------- resolution
919 : : // (cl F (not F))*
920 : : //
921 : : // VP1: (cl (not (not (not F))) F)
922 : : // VP2: (cl (not (not (not (not F)))) (not F))
923 : : //
924 : : // * the corresponding proof node is (or F (not F))
925 : 4 : case ProofRule::SPLIT:
926 : : {
927 : : Node vp1 = nm->mkNode(
928 : 12 : Kind::SEXPR, d_cl, args[0].notNode().notNode().notNode(), args[0]);
929 : : Node vp2 = nm->mkNode(Kind::SEXPR,
930 : 4 : d_cl,
931 : 8 : args[0].notNode().notNode().notNode().notNode(),
932 : 16 : args[0].notNode());
933 [ + - ][ + - ]: 4 : return addAletheStep(AletheRule::NOT_NOT, vp2, vp2, {}, {}, *cdp)
[ + - ][ - - ]
[ - - ][ - - ]
[ - - ]
934 : 8 : && addAletheStep(AletheRule::NOT_NOT, vp1, vp1, {}, {}, *cdp)
935 : 20 : && addAletheStepFromOr(
936 : : AletheRule::RESOLUTION,
937 : : res,
938 : : {vp1, vp2},
939 : 4 : d_resPivots
940 : 8 : ? std::vector<Node>{args[0].notNode().notNode().notNode(),
941 : 0 : d_true}
942 : : : std::vector<Node>(),
943 [ + - ]: 12 : *cdp);
944 : : }
945 : : // ======== Equality resolution
946 : : //
947 : : // ------ EQUIV_POS2
948 : : // VP1 P2 P1
949 : : // --------------------------------- resolution
950 : : // (cl F2)*
951 : : //
952 : : // VP1: (cl (not (= F1 F2)) (not F1) F2)
953 : : //
954 : : // * the corresponding proof node is F2
955 : 53668 : case ProofRule::EQ_RESOLVE:
956 : : {
957 : : Node equivPos2Cl =
958 : : nm->mkNode(Kind::SEXPR,
959 : 322008 : {d_cl, children[1].notNode(), children[0].notNode(), res});
960 : 53668 : bool success = addAletheStep(
961 : : AletheRule::EQUIV_POS2, equivPos2Cl, equivPos2Cl, {}, {}, *cdp);
962 : : // we will use an RESOLUTION_OR step for the resolution because the proof
963 : : // of children[0], if it is for (or t1 ... tn), may actually conclude (cl
964 : : // t1 ... tn). Using RESOLUTION_OR will guarantee that in post-visit time
965 : : // the resolution step is fixed if need be
966 : : return success
967 : 535600 : && addAletheStep(
968 : : AletheRule::RESOLUTION_OR,
969 : : res,
970 : 107201 : nm->mkNode(Kind::SEXPR, d_cl, res),
971 : 107066 : {equivPos2Cl, children[1], children[0]},
972 : 321333 : std::vector<Node>{children[1], d_false, children[0], d_false},
973 [ + + ]: 214267 : *cdp);
974 : : }
975 : : // ======== Modus ponens
976 : : //
977 : : // (P2:(=> F1 F2))
978 : : // ------------------------ implies
979 : : // (VP1:(cl (not F1) F2)) (P1:F1)
980 : : // -------------------------------------------- resolution
981 : : // (cl F2)*
982 : : //
983 : : // * the corresponding proof node is F2
984 : 28233 : case ProofRule::MODUS_PONENS:
985 : : {
986 : 56466 : Node vp1 = nm->mkNode(Kind::SEXPR, d_cl, children[0].notNode(), res);
987 : :
988 : 84699 : return addAletheStep(
989 : 28233 : AletheRule::IMPLIES, vp1, vp1, {children[1]}, {}, *cdp)
990 : 254091 : && addAletheStep(AletheRule::RESOLUTION,
991 : : res,
992 : 56465 : nm->mkNode(Kind::SEXPR, d_cl, res),
993 : 28232 : {vp1, children[0]},
994 : 28232 : d_resPivots
995 : 56465 : ? std::vector<Node>{children[0], d_false}
996 : : : std::vector<Node>(),
997 [ + + ]: 84697 : *cdp);
998 : : }
999 : : // ======== Double negation elimination
1000 : : //
1001 : : // ---------------------------------- not_not
1002 : : // (VP1:(cl (not (not (not F))) F)) (P:(not (not F)))
1003 : : // ------------------------------------------------------------- resolution
1004 : : // (cl F)*
1005 : : //
1006 : : // * the corresponding proof node is F
1007 : 85 : case ProofRule::NOT_NOT_ELIM:
1008 : : {
1009 : 170 : Node vp1 = nm->mkNode(Kind::SEXPR, d_cl, children[0].notNode(), res);
1010 : :
1011 [ + - ][ + - ]: 85 : return addAletheStep(AletheRule::NOT_NOT, vp1, vp1, {}, {}, *cdp)
[ + - ][ - - ]
[ - - ][ - - ]
[ - - ]
1012 : 680 : && addAletheStep(AletheRule::RESOLUTION,
1013 : : res,
1014 : 170 : nm->mkNode(Kind::SEXPR, d_cl, res),
1015 : 85 : {vp1, children[0]},
1016 : 85 : d_resPivots
1017 : 170 : ? std::vector<Node>{children[0], d_false}
1018 : : : std::vector<Node>(),
1019 [ + - ]: 255 : *cdp);
1020 : : }
1021 : : // ======== Contradiction
1022 : : //
1023 : : // P1 P2
1024 : : // --------- resolution
1025 : : // (cl)*
1026 : : //
1027 : : // * the corresponding proof node is false
1028 : 2316 : case ProofRule::CONTRA:
1029 : : {
1030 : 4632 : return addAletheStep(AletheRule::RESOLUTION,
1031 : : res,
1032 : 4632 : nm->mkNode(Kind::SEXPR, d_cl),
1033 : : children,
1034 : 4632 : d_resPivots ? std::vector<Node>{children[0], d_true}
1035 : : : std::vector<Node>(),
1036 : 2316 : *cdp);
1037 : : }
1038 : : // ======== And elimination
1039 : : // This rule is translated according to the singleton pattern.
1040 : 8724 : case ProofRule::AND_ELIM:
1041 : : {
1042 : 17448 : return addAletheStep(AletheRule::AND,
1043 : : res,
1044 : 17448 : nm->mkNode(Kind::SEXPR, d_cl, res),
1045 : : children,
1046 : : args,
1047 : 8724 : *cdp);
1048 : : }
1049 : : // ======== And introduction
1050 : : //
1051 : : //
1052 : : // ----- and_neg
1053 : : // VP1 P1 ... Pn
1054 : : // -------------------------- resolution
1055 : : // (cl (and F1 ... Fn))*
1056 : : //
1057 : : // VP1:(cl (and F1 ... Fn) (not F1) ... (not Fn))
1058 : : //
1059 : : // * the corresponding proof node is (and F1 ... Fn)
1060 : 28266 : case ProofRule::AND_INTRO:
1061 : : {
1062 : 141330 : std::vector<Node> neg_Nodes = {d_cl, res};
1063 [ + + ]: 112949 : for (size_t i = 0, size = children.size(); i < size; i++)
1064 : : {
1065 : 84683 : neg_Nodes.push_back(children[i].notNode());
1066 : : }
1067 : 56532 : Node vp1 = nm->mkNode(Kind::SEXPR, neg_Nodes);
1068 : :
1069 : 113064 : std::vector<Node> new_children = {vp1};
1070 : 28266 : new_children.insert(new_children.end(), children.begin(), children.end());
1071 : 28266 : std::vector<Node> newArgs;
1072 [ - + ]: 28266 : if (d_resPivots)
1073 : : {
1074 [ - - ]: 0 : for (const Node& child : children)
1075 : : {
1076 : 0 : newArgs.push_back(child);
1077 : 0 : newArgs.push_back(d_false);
1078 : : }
1079 : : }
1080 [ + - ][ + - ]: 28266 : return addAletheStep(AletheRule::AND_NEG, vp1, vp1, {}, {}, *cdp)
[ + - ][ - - ]
[ - - ][ - - ]
[ - - ]
1081 [ + - ][ + - ]: 84798 : && addAletheStep(AletheRule::RESOLUTION,
[ - - ]
1082 : : res,
1083 : 56532 : nm->mkNode(Kind::SEXPR, d_cl, res),
1084 : : new_children,
1085 : : newArgs,
1086 [ + - ]: 28266 : *cdp);
1087 : : }
1088 : : // ======== Not Or elimination
1089 : : // This rule is translated according to the singleton pattern.
1090 : 81 : case ProofRule::NOT_OR_ELIM:
1091 : : {
1092 : 162 : return addAletheStep(AletheRule::NOT_OR,
1093 : : res,
1094 : 162 : nm->mkNode(Kind::SEXPR, d_cl, res),
1095 : : children,
1096 : : args,
1097 : 81 : *cdp);
1098 : : }
1099 : : // ======== Implication elimination
1100 : : // This rule is translated according to the clause pattern.
1101 : 12597 : case ProofRule::IMPLIES_ELIM:
1102 : : {
1103 : 12597 : return addAletheStepFromOr(AletheRule::IMPLIES, res, children, {}, *cdp);
1104 : : }
1105 : : // ======== Not Implication elimination version 1
1106 : : // This rule is translated according to the singleton pattern.
1107 : 96 : case ProofRule::NOT_IMPLIES_ELIM1:
1108 : : {
1109 : 384 : return addAletheStep(AletheRule::NOT_IMPLIES1,
1110 : : res,
1111 : 192 : nm->mkNode(Kind::SEXPR, d_cl, res),
1112 : : children,
1113 : : {},
1114 : 96 : *cdp);
1115 : : }
1116 : : // ======== Not Implication elimination version 2
1117 : : // This rule is translated according to the singleton pattern.
1118 : 105 : case ProofRule::NOT_IMPLIES_ELIM2:
1119 : : {
1120 : 420 : return addAletheStep(AletheRule::NOT_IMPLIES2,
1121 : : res,
1122 : 210 : nm->mkNode(Kind::SEXPR, d_cl, res),
1123 : : children,
1124 : : {},
1125 : 105 : *cdp);
1126 : : }
1127 : : // ======== Various elimination rules
1128 : : // The following rules are all translated according to the clause pattern.
1129 : 1196 : case ProofRule::EQUIV_ELIM1:
1130 : : {
1131 : 1196 : return addAletheStepFromOr(AletheRule::EQUIV1, res, children, {}, *cdp);
1132 : : }
1133 : 833 : case ProofRule::EQUIV_ELIM2:
1134 : : {
1135 : 833 : return addAletheStepFromOr(AletheRule::EQUIV2, res, children, {}, *cdp);
1136 : : }
1137 : 39 : case ProofRule::NOT_EQUIV_ELIM1:
1138 : : {
1139 : 78 : return addAletheStepFromOr(
1140 : 39 : AletheRule::NOT_EQUIV1, res, children, {}, *cdp);
1141 : : }
1142 : 39 : case ProofRule::NOT_EQUIV_ELIM2:
1143 : : {
1144 : 78 : return addAletheStepFromOr(
1145 : 39 : AletheRule::NOT_EQUIV2, res, children, {}, *cdp);
1146 : : }
1147 : 4 : case ProofRule::XOR_ELIM1:
1148 : : {
1149 : 4 : return addAletheStepFromOr(AletheRule::XOR1, res, children, {}, *cdp);
1150 : : }
1151 : 2 : case ProofRule::XOR_ELIM2:
1152 : : {
1153 : 2 : return addAletheStepFromOr(AletheRule::XOR2, res, children, {}, *cdp);
1154 : : }
1155 : 0 : case ProofRule::NOT_XOR_ELIM1:
1156 : : {
1157 : 0 : return addAletheStepFromOr(AletheRule::NOT_XOR1, res, children, {}, *cdp);
1158 : : }
1159 : 0 : case ProofRule::NOT_XOR_ELIM2:
1160 : : {
1161 : 0 : return addAletheStepFromOr(AletheRule::NOT_XOR2, res, children, {}, *cdp);
1162 : : }
1163 : 664 : case ProofRule::ITE_ELIM1:
1164 : : {
1165 : 664 : return addAletheStepFromOr(AletheRule::ITE2, res, children, {}, *cdp);
1166 : : }
1167 : 834 : case ProofRule::ITE_ELIM2:
1168 : : {
1169 : 834 : return addAletheStepFromOr(AletheRule::ITE1, res, children, {}, *cdp);
1170 : : }
1171 : 0 : case ProofRule::NOT_ITE_ELIM1:
1172 : : {
1173 : 0 : return addAletheStepFromOr(AletheRule::NOT_ITE2, res, children, {}, *cdp);
1174 : : }
1175 : 0 : case ProofRule::NOT_ITE_ELIM2:
1176 : : {
1177 : 0 : return addAletheStepFromOr(AletheRule::NOT_ITE1, res, children, {}, *cdp);
1178 : : }
1179 : : //================================================= De Morgan rules
1180 : : // ======== Not And
1181 : : // This rule is translated according to the clause pattern.
1182 : 8020 : case ProofRule::NOT_AND:
1183 : : {
1184 : 8020 : return addAletheStepFromOr(AletheRule::NOT_AND, res, children, {}, *cdp);
1185 : : }
1186 : :
1187 : : //================================================= CNF rules
1188 : : // The following rules are all translated according to the clause pattern.
1189 : 21712 : case ProofRule::CNF_AND_POS:
1190 : : {
1191 : 43424 : return addAletheStepFromOr(AletheRule::AND_POS,
1192 : : res,
1193 : : children,
1194 : 65136 : std::vector<Node>{args.back()},
1195 : 21712 : *cdp);
1196 : : }
1197 : 11495 : case ProofRule::CNF_AND_NEG:
1198 : : {
1199 : 11495 : return addAletheStepFromOr(AletheRule::AND_NEG, res, children, {}, *cdp);
1200 : : }
1201 : 3536 : case ProofRule::CNF_OR_POS:
1202 : : {
1203 : 3536 : return addAletheStepFromOr(AletheRule::OR_POS, res, children, {}, *cdp);
1204 : : }
1205 : 3646 : case ProofRule::CNF_OR_NEG:
1206 : : {
1207 : 7292 : return addAletheStepFromOr(AletheRule::OR_NEG,
1208 : : res,
1209 : : children,
1210 : 10938 : std::vector<Node>{args.back()},
1211 : 3646 : *cdp);
1212 : : }
1213 : 51 : case ProofRule::CNF_IMPLIES_POS:
1214 : : {
1215 : 102 : return addAletheStepFromOr(
1216 : 51 : AletheRule::IMPLIES_POS, res, children, {}, *cdp);
1217 : : }
1218 : 77 : case ProofRule::CNF_IMPLIES_NEG1:
1219 : : {
1220 : 154 : return addAletheStepFromOr(
1221 : 77 : AletheRule::IMPLIES_NEG1, res, children, {}, *cdp);
1222 : : }
1223 : 223 : case ProofRule::CNF_IMPLIES_NEG2:
1224 : : {
1225 : 446 : return addAletheStepFromOr(
1226 : 223 : AletheRule::IMPLIES_NEG2, res, children, {}, *cdp);
1227 : : }
1228 : 1283 : case ProofRule::CNF_EQUIV_POS1:
1229 : : {
1230 : 2566 : return addAletheStepFromOr(
1231 : 1283 : AletheRule::EQUIV_POS2, res, children, {}, *cdp);
1232 : : }
1233 : 1306 : case ProofRule::CNF_EQUIV_POS2:
1234 : : {
1235 : 2612 : return addAletheStepFromOr(
1236 : 1306 : AletheRule::EQUIV_POS1, res, children, {}, *cdp);
1237 : : }
1238 : 1004 : case ProofRule::CNF_EQUIV_NEG1:
1239 : : {
1240 : 2008 : return addAletheStepFromOr(
1241 : 1004 : AletheRule::EQUIV_NEG2, res, children, {}, *cdp);
1242 : : }
1243 : 804 : case ProofRule::CNF_EQUIV_NEG2:
1244 : : {
1245 : 1608 : return addAletheStepFromOr(
1246 : 804 : AletheRule::EQUIV_NEG1, res, children, {}, *cdp);
1247 : : }
1248 : 1500 : case ProofRule::CNF_XOR_POS1:
1249 : : {
1250 : 1500 : return addAletheStepFromOr(AletheRule::XOR_POS1, res, children, {}, *cdp);
1251 : : }
1252 : 563 : case ProofRule::CNF_XOR_POS2:
1253 : : {
1254 : 563 : return addAletheStepFromOr(AletheRule::XOR_POS2, res, children, {}, *cdp);
1255 : : }
1256 : 675 : case ProofRule::CNF_XOR_NEG1:
1257 : : {
1258 : 675 : return addAletheStepFromOr(AletheRule::XOR_NEG2, res, children, {}, *cdp);
1259 : : }
1260 : 688 : case ProofRule::CNF_XOR_NEG2:
1261 : : {
1262 : 688 : return addAletheStepFromOr(AletheRule::XOR_NEG1, res, children, {}, *cdp);
1263 : : }
1264 : 465 : case ProofRule::CNF_ITE_POS1:
1265 : : {
1266 : 465 : return addAletheStepFromOr(AletheRule::ITE_POS2, res, children, {}, *cdp);
1267 : : }
1268 : 570 : case ProofRule::CNF_ITE_POS2:
1269 : : {
1270 : 570 : return addAletheStepFromOr(AletheRule::ITE_POS1, res, children, {}, *cdp);
1271 : : }
1272 : 269 : case ProofRule::CNF_ITE_NEG1:
1273 : : {
1274 : 269 : return addAletheStepFromOr(AletheRule::ITE_NEG2, res, children, {}, *cdp);
1275 : : }
1276 : 404 : case ProofRule::CNF_ITE_NEG2:
1277 : : {
1278 : 404 : return addAletheStepFromOr(AletheRule::ITE_NEG1, res, children, {}, *cdp);
1279 : : }
1280 : : // ======== CNF ITE Pos version 3
1281 : : //
1282 : : // ----- ite_pos1 ----- ite_pos2
1283 : : // VP1 VP2
1284 : : // ------------------------------- resolution
1285 : : // VP3
1286 : : // ------------------------------- reordering
1287 : : // VP4
1288 : : // ------------------------------- contraction
1289 : : // (cl (not (ite C F1 F2)) F1 F2)
1290 : : //
1291 : : // VP1: (cl (not (ite C F1 F2)) C F2)
1292 : : // VP2: (cl (not (ite C F1 F2)) (not C) F1)
1293 : : // VP3: (cl (not (ite C F1 F2)) F2 (not (ite C F1 F2)) F1)
1294 : : // VP4: (cl (not (ite C F1 F2)) (not (ite C F1 F2)) F1 F2)
1295 : : //
1296 : : // * the corresponding proof node is (or (not (ite C F1 F2)) F1 F2)
1297 : 745 : case ProofRule::CNF_ITE_POS3:
1298 : : {
1299 : 5215 : Node vp1 = nm->mkNode(Kind::SEXPR, {d_cl, res[0], args[0][0], res[2]});
1300 : : Node vp2 =
1301 : 5215 : nm->mkNode(Kind::SEXPR, {d_cl, res[0], args[0][0].notNode(), res[1]});
1302 : : Node vp3 =
1303 : 5960 : nm->mkNode(Kind::SEXPR, {d_cl, res[0], res[2], res[0], res[1]});
1304 : : Node vp4 =
1305 : 5215 : nm->mkNode(Kind::SEXPR, {d_cl, res[0], res[0], res[1], res[2]});
1306 : :
1307 [ + - ][ + - ]: 745 : return addAletheStep(AletheRule::ITE_POS1, vp1, vp1, {}, {}, *cdp)
[ + - ][ - - ]
[ - - ][ - - ]
[ - - ]
1308 : 1490 : && addAletheStep(AletheRule::ITE_POS2, vp2, vp2, {}, {}, *cdp)
1309 : 2980 : && addAletheStep(AletheRule::RESOLUTION,
1310 : : vp3,
1311 : : vp3,
1312 : : {vp1, vp2},
1313 : 745 : d_resPivots
1314 : 1490 : ? std::vector<Node>{args[0][0], d_true}
1315 : : : std::vector<Node>(),
1316 : 1490 : *cdp)
1317 : 2235 : && addAletheStep(AletheRule::REORDERING, vp4, vp4, {vp3}, {}, *cdp)
1318 : 2980 : && addAletheStepFromOr(
1319 [ + - ]: 1490 : AletheRule::CONTRACTION, res, {vp4}, {}, *cdp);
1320 : : }
1321 : : // ======== CNF ITE Neg version 3
1322 : : //
1323 : : // ----- ite_neg1 ----- ite_neg2
1324 : : // VP1 VP2
1325 : : // ------------------------------- resolution
1326 : : // VP3
1327 : : // ------------------------------- reordering
1328 : : // VP4
1329 : : // ------------------------------- contraction
1330 : : // (cl (ite C F1 F2) C (not F2))
1331 : : //
1332 : : // VP1: (cl (ite C F1 F2) C (not F2))
1333 : : // VP2: (cl (ite C F1 F2) (not C) (not F1))
1334 : : // VP3: (cl (ite C F1 F2) (not F2) (ite C F1 F2) (not F1))
1335 : : // VP4: (cl (ite C F1 F2) (ite C F1 F2) (not F1) (not F2))
1336 : : //
1337 : : // * the corresponding proof node is (or (ite C F1 F2) C (not F2))
1338 : 274 : case ProofRule::CNF_ITE_NEG3:
1339 : : {
1340 : 1918 : Node vp1 = nm->mkNode(Kind::SEXPR, {d_cl, res[0], args[0][0], res[2]});
1341 : : Node vp2 =
1342 : 1918 : nm->mkNode(Kind::SEXPR, {d_cl, res[0], args[0][0].notNode(), res[1]});
1343 : : Node vp3 =
1344 : 2192 : nm->mkNode(Kind::SEXPR, {d_cl, res[0], res[2], res[0], res[1]});
1345 : : Node vp4 =
1346 : 1918 : nm->mkNode(Kind::SEXPR, {d_cl, res[0], res[0], res[1], res[2]});
1347 : :
1348 [ + - ][ + - ]: 274 : return addAletheStep(AletheRule::ITE_NEG1, vp1, vp1, {}, {}, *cdp)
[ + - ][ - - ]
[ - - ][ - - ]
[ - - ]
1349 : 548 : && addAletheStep(AletheRule::ITE_NEG2, vp2, vp2, {}, {}, *cdp)
1350 : 1096 : && addAletheStep(AletheRule::RESOLUTION,
1351 : : vp3,
1352 : : vp3,
1353 : : {vp1, vp2},
1354 : 274 : d_resPivots
1355 : 548 : ? std::vector<Node>{args[0][0], d_true}
1356 : : : std::vector<Node>(),
1357 : 548 : *cdp)
1358 : 822 : && addAletheStep(AletheRule::REORDERING, vp4, vp4, {vp3}, {}, *cdp)
1359 : 1096 : && addAletheStepFromOr(
1360 [ + - ]: 548 : AletheRule::CONTRACTION, res, {vp4}, {}, *cdp);
1361 : : }
1362 : : //================================================= Equality rules
1363 : : // The following rules are all translated according to the singleton
1364 : : // pattern.
1365 : 53830 : case ProofRule::REFL:
1366 : : {
1367 : 215320 : return addAletheStep(AletheRule::REFL,
1368 : : res,
1369 : 107660 : nm->mkNode(Kind::SEXPR, d_cl, res),
1370 : : children,
1371 : : {},
1372 : 53830 : *cdp);
1373 : : }
1374 : 49170 : case ProofRule::SYMM:
1375 : : {
1376 : 245850 : return addAletheStep(
1377 [ + + ]: 49170 : res.getKind() == Kind::NOT ? AletheRule::NOT_SYMM : AletheRule::SYMM,
1378 : : res,
1379 : 98340 : nm->mkNode(Kind::SEXPR, d_cl, res),
1380 : : children,
1381 : : {},
1382 : 49170 : *cdp);
1383 : : }
1384 : 157654 : case ProofRule::TRANS:
1385 : : {
1386 : 630616 : return addAletheStep(AletheRule::TRANS,
1387 : : res,
1388 : 315308 : nm->mkNode(Kind::SEXPR, d_cl, res),
1389 : : children,
1390 : : {},
1391 : 157654 : *cdp);
1392 : : }
1393 : : // ======== Congruence
1394 : : // In the case that the kind of the function symbol f? is FORALL or
1395 : : // EXISTS, the cong rule needs to be converted into a bind rule:
1396 : : //
1397 : : // (cl (= F G))
1398 : : // -------------------- bind, z1 ... zn (= y1 z1) ... (= yn zn)
1399 : : // (= (Q ((y1 T1) ... (yn Tn)) F) (Q ((z1 T1) ... (zn Tn)) G))
1400 : : //
1401 : : // Otherwise, the rule is regular congruence:
1402 : : //
1403 : : // P1 ... Pn
1404 : : // -------------------------------------------------------- cong
1405 : : // (cl (= (<kind> f? t1 ... tn) (<kind> f? s1 ... sn)))
1406 : 246135 : case ProofRule::CONG:
1407 : : case ProofRule::NARY_CONG:
1408 : : {
1409 [ + + ]: 246135 : if (res[0].isClosure())
1410 : : {
1411 : : // collect rhs variables
1412 : 3195 : new_args.insert(new_args.end(), res[1][0].begin(), res[1][0].end());
1413 [ + + ]: 9455 : for (size_t i = 0, size = res[0][0].getNumChildren(); i < size; ++i)
1414 : : {
1415 : 6260 : new_args.push_back(res[0][0][i].eqNode(res[1][0][i]));
1416 : : }
1417 : 3195 : Kind k = res[0].getKind();
1418 : 6390 : return addAletheStep(AletheRule::ANCHOR_BIND,
1419 : : res,
1420 : 6390 : nm->mkNode(Kind::SEXPR, d_cl, res),
1421 : : // be sure to ignore premise for pattern
1422 [ + + ]: 143 : (k == Kind::FORALL || k == Kind::EXISTS)
1423 : 9671 : ? std::vector<Node>{children[0]}
1424 : : : children,
1425 : : new_args,
1426 : 3195 : *cdp);
1427 : : }
1428 : 971760 : return addAletheStep(AletheRule::CONG,
1429 : : res,
1430 : 485880 : nm->mkNode(Kind::SEXPR, d_cl, res),
1431 : : children,
1432 : : {},
1433 : 242940 : *cdp);
1434 : : }
1435 : 112 : case ProofRule::HO_CONG:
1436 : : {
1437 : 448 : return addAletheStep(AletheRule::HO_CONG,
1438 : : res,
1439 : 224 : nm->mkNode(Kind::SEXPR, d_cl, res),
1440 : : children,
1441 : : {},
1442 : 112 : *cdp);
1443 : : }
1444 : : // ======== True intro
1445 : : //
1446 : : // ------------------------------- EQUIV_SIMPLIFY
1447 : : // (VP1:(cl (= (= F true) F)))
1448 : : // ------------------------------- EQUIV2
1449 : : // (VP2:(cl (= F true) (not F))) P
1450 : : // -------------------------------------------- RESOLUTION
1451 : : // (cl (= F true))*
1452 : : //
1453 : : // * the corresponding proof node is (= F true)
1454 : 759 : case ProofRule::TRUE_INTRO:
1455 : : {
1456 : 2277 : Node vp1 = nm->mkNode(Kind::SEXPR, d_cl, res.eqNode(children[0]));
1457 : 1518 : Node vp2 = nm->mkNode(Kind::SEXPR, d_cl, res, children[0].notNode());
1458 [ + - ][ + - ]: 759 : return addAletheStep(AletheRule::EQUIV_SIMPLIFY, vp1, vp1, {}, {}, *cdp)
[ + - ][ - - ]
[ - - ][ - - ]
[ - - ]
1459 : 2275 : && addAletheStep(AletheRule::EQUIV2, vp2, vp2, {vp1}, {}, *cdp)
1460 : 6066 : && addAletheStep(AletheRule::RESOLUTION,
1461 : : res,
1462 : 1517 : nm->mkNode(Kind::SEXPR, d_cl, res),
1463 : 758 : {vp2, children[0]},
1464 : 758 : d_resPivots
1465 : 1517 : ? std::vector<Node>{children[0], d_false}
1466 : : : std::vector<Node>(),
1467 [ + + ]: 2275 : *cdp);
1468 : : }
1469 : : // ======== True elim
1470 : : //
1471 : : // ------------------------------- EQUIV_SIMPLIFY
1472 : : // (VP1:(cl (= (= F true) F)))
1473 : : // ------------------------------- EQUIV1
1474 : : // (VP2:(cl (not (= F true)) F)) P
1475 : : // -------------------------------------------- RESOLUTION
1476 : : // (cl F)*
1477 : : //
1478 : : // * the corresponding proof node is F
1479 : 2903 : case ProofRule::TRUE_ELIM:
1480 : : {
1481 : 8709 : Node vp1 = nm->mkNode(Kind::SEXPR, d_cl, children[0].eqNode(res));
1482 : 5806 : Node vp2 = nm->mkNode(Kind::SEXPR, d_cl, children[0].notNode(), res);
1483 [ + - ][ + - ]: 2903 : return addAletheStep(AletheRule::EQUIV_SIMPLIFY, vp1, vp1, {}, {}, *cdp)
[ + - ][ - - ]
[ - - ][ - - ]
[ - - ]
1484 : 8709 : && addAletheStep(AletheRule::EQUIV1, vp2, vp2, {vp1}, {}, *cdp)
1485 : 23224 : && addAletheStep(AletheRule::RESOLUTION,
1486 : : res,
1487 : 5806 : nm->mkNode(Kind::SEXPR, d_cl, res),
1488 : 2903 : {vp2, children[0]},
1489 : 2903 : d_resPivots
1490 : 5806 : ? std::vector<Node>{children[0], d_false}
1491 : : : std::vector<Node>(),
1492 [ + - ]: 8709 : *cdp);
1493 : : }
1494 : : // ======== False intro
1495 : : //
1496 : : // ----- EQUIV_SIMPLIFY
1497 : : // VP1
1498 : : // ----- EQUIV2 ----- NOT_NOT
1499 : : // VP2 VP3
1500 : : // ---------------------- RESOLUTION
1501 : : // VP4 P
1502 : : // -------------------------------------- RESOLUTION
1503 : : // (cl (= F false))*
1504 : : //
1505 : : // VP1: (cl (= (= F false) (not F)))
1506 : : // VP2: (cl (= F false) (not (not F)))
1507 : : // VP3: (cl (not (not (not F))) F)
1508 : : // VP4: (cl (= F false) F)
1509 : : //
1510 : : // * the corresponding proof node is (= F false)
1511 : 1560 : case ProofRule::FALSE_INTRO:
1512 : : {
1513 : 4680 : Node vp1 = nm->mkNode(Kind::SEXPR, d_cl, res.eqNode(children[0]));
1514 : 4680 : Node vp2 = nm->mkNode(Kind::SEXPR, d_cl, res, children[0].notNode());
1515 : : Node vp3 = nm->mkNode(
1516 : 4680 : Kind::SEXPR, d_cl, children[0].notNode().notNode(), children[0][0]);
1517 : 3120 : Node vp4 = nm->mkNode(Kind::SEXPR, d_cl, res, children[0][0]);
1518 : :
1519 [ + - ][ + - ]: 1560 : return addAletheStep(AletheRule::EQUIV_SIMPLIFY, vp1, vp1, {}, {}, *cdp)
[ + - ][ - - ]
[ - - ][ - - ]
[ - - ]
1520 : 4678 : && addAletheStep(AletheRule::EQUIV2, vp2, vp2, {vp1}, {}, *cdp)
1521 : 3119 : && addAletheStep(AletheRule::NOT_NOT, vp3, vp3, {}, {}, *cdp)
1522 : 6237 : && addAletheStep(
1523 : : AletheRule::RESOLUTION,
1524 : : vp4,
1525 : : vp4,
1526 : : {vp2, vp3},
1527 : 3129 : d_resPivots ? std::vector<Node>{children[0].notNode(), d_true}
1528 : : : std::vector<Node>(),
1529 : 3118 : *cdp)
1530 : 12474 : && addAletheStep(AletheRule::RESOLUTION,
1531 : : res,
1532 : 3119 : nm->mkNode(Kind::SEXPR, d_cl, res),
1533 : 1559 : {vp4, children[0]},
1534 : 1559 : d_resPivots
1535 : 3129 : ? std::vector<Node>{children[0][0], d_true}
1536 : : : std::vector<Node>(),
1537 [ + + ]: 4678 : *cdp);
1538 : : }
1539 : : // ======== False elim
1540 : : //
1541 : : // ----- EQUIV_SIMPLIFY
1542 : : // VP1
1543 : : // ----- EQUIV1
1544 : : // VP2 P
1545 : : // ---------------------- RESOLUTION
1546 : : // (cl (not F))*
1547 : : //
1548 : : // VP1: (cl (= (= F false) (not F)))
1549 : : // VP2: (cl (not (= F false)) (not F))
1550 : : // VP3: (cl (not (not (not F))) F)
1551 : : // VP4: (cl (= F false) F)
1552 : : //
1553 : : // * the corresponding proof node is (not F)
1554 : 1448 : case ProofRule::FALSE_ELIM:
1555 : : {
1556 : 4344 : Node vp1 = nm->mkNode(Kind::SEXPR, d_cl, children[0].eqNode(res));
1557 : 2896 : Node vp2 = nm->mkNode(Kind::SEXPR, d_cl, children[0].notNode(), res);
1558 : :
1559 [ + - ][ + - ]: 1448 : return addAletheStep(AletheRule::EQUIV_SIMPLIFY, vp1, vp1, {}, {}, *cdp)
[ + - ][ - - ]
[ - - ][ - - ]
[ - - ]
1560 : 4344 : && addAletheStep(AletheRule::EQUIV1, vp2, vp2, {vp1}, {}, *cdp)
1561 : 11584 : && addAletheStep(AletheRule::RESOLUTION,
1562 : : res,
1563 : 2896 : nm->mkNode(Kind::SEXPR, d_cl, res),
1564 : 1448 : {vp2, children[0]},
1565 : 1448 : d_resPivots
1566 : 2906 : ? std::vector<Node>{children[0], d_false}
1567 : : : std::vector<Node>(),
1568 [ + - ]: 4344 : *cdp);
1569 : : }
1570 : : //================================================= Skolems rules
1571 : : // ======== Skolem intro
1572 : : // Since this rule just equates a term to its purification skolem, whose
1573 : : // conversion is the term itself, the converted conclusion is an equality
1574 : : // between the same terms.
1575 : 2727 : case ProofRule::SKOLEM_INTRO:
1576 : : {
1577 : 10908 : return addAletheStep(AletheRule::REFL,
1578 : : res,
1579 : 5454 : nm->mkNode(Kind::SEXPR, d_cl, res),
1580 : : {},
1581 : : {},
1582 : 2727 : *cdp);
1583 : : }
1584 : : // ======== If-then-else equivalence
1585 : : //
1586 : : // ------- rare_rewrite, ite_eq
1587 : : // VP1
1588 : : // ------- equiv2 ---------- true
1589 : : // VP2 d_true
1590 : : // ----------------------------------------------- resolution
1591 : : // (cl (C?(= (C?t1:t2) t1):(= (C?t1:t2) t2)))*
1592 : : //
1593 : : // VP1: (cl (= (C?(= (C?t1:t2) t1):(= (C?t1:t2) t2)) true))
1594 : : // VP2: (cl (C?(= (C?t1:t2) t1):(= (C?t1:t2) t2)) (not true))
1595 : : // d_true: (cl true)
1596 : : //
1597 : : // * the corresponding proof node is (C?(= (C?t1:t2) t1):(= (C?t1:t2) t2))
1598 : : //
1599 : : // (define-rule ite_eq ((C bool) (t1 ?) (t2 ?)) (ite C (= (C?t1:t2) t1) (=
1600 : : // (C?t1:t2) t2)) true)
1601 : : //
1602 : 818 : case ProofRule::ITE_EQ:
1603 : : {
1604 : 2454 : Node vp1 = nm->mkNode(Kind::EQUAL, res, d_true);
1605 : 2454 : Node vp2 = nm->mkNode(Kind::OR, res, d_true.notNode());
1606 : 818 : Node args_0 = args[0];
1607 : 5726 : return addAletheStep(AletheRule::RARE_REWRITE,
1608 : : vp1,
1609 : 1636 : nm->mkNode(Kind::SEXPR, d_cl, vp1),
1610 : : {},
1611 [ + - ][ - - ]: 818 : {nm->mkRawSymbol("\"ite-eq\"", nm->sExprType()),
1612 : : args_0[0],
1613 : : args_0[1],
1614 : : args_0[2]},
1615 : 3272 : *cdp)
1616 : 2454 : && addAletheStepFromOr(AletheRule::EQUIV2, vp2, {vp1}, {}, *cdp)
1617 : 3272 : && addAletheStep(AletheRule::TRUE,
1618 : 818 : d_true,
1619 : 1636 : nm->mkNode(Kind::SEXPR, d_cl, d_true),
1620 : : {},
1621 : : {},
1622 : : *cdp)
1623 : 8180 : && addAletheStep(AletheRule::RESOLUTION,
1624 : : res,
1625 : 1636 : nm->mkNode(Kind::SEXPR, d_cl, res),
1626 : 818 : {vp2, d_true},
1627 : 1636 : d_resPivots ? std::vector<Node>{d_true, d_false}
1628 : : : std::vector<Node>(),
1629 [ + - ]: 2454 : *cdp);
1630 : : }
1631 : : // ======== Skolemize
1632 : : //
1633 : : // In cvc5 this is applied solely to terms (not (forall (...) F)),
1634 : : // concluding (not F*sigma'), where sigma' is the cumulative substitution
1635 : : // built from sigma1...sigma_n, and each sigma_i replaces xi by the choice
1636 : : // term (epsilon ((xi Ti)) (forall ((xi+1 Ti+1) ... (xn+1 Tn+1)) (not
1637 : : // F))). The resulting Alethe Skolemization step is:
1638 : : //
1639 : : // ---------------- refl
1640 : : // (= F F*sigma')
1641 : : // ------------------------- anchor_sko_forall, sigma_1, ..., sigma_n
1642 : : // (= (forall ((x1 T1) ... (xn Tn)) F) F*sigma')
1643 : : // ----------------------------------------------- cong
1644 : : // (= (not (forall ((x1 T1) ... (xn Tn)) F)) (not F*sigma'))
1645 : : //
1646 : : // Then, we eliminate the equality to obtain (not F*sigma) from the premise:
1647 : : //
1648 : : // ---- equiv_pos2
1649 : : // VP1 (= (not (forall (...) F)) (not F*sigma')) (not (forall (...) F))
1650 : : // ------------------------------------------------------------- resolution
1651 : : // (not F*sigma')
1652 : : //
1653 : : // VP1 :
1654 : : // (cl
1655 : : // (not (= (not (forall (...) F)) (not F*sigma')))
1656 : : // (not (not (forall (...) F)))
1657 : : // (not F*sigma'))
1658 : : //
1659 : : // Note that F*sigma' is equivalent to F*sigma once its Skolem terms are
1660 : : // lifted to choice terms by the node converter.
1661 : 74 : case ProofRule::SKOLEMIZE:
1662 : : {
1663 : 74 : bool success = true;
1664 : 148 : Node quant = children[0][0], skolemized = res[0];
1665 : 148 : Assert(children[0].getKind() == Kind::NOT
1666 : : && children[0][0].getKind() == Kind::FORALL);
1667 : 148 : Node eq = quant[1].eqNode(skolemized);
1668 : : // add rfl step for final replacement
1669 : 222 : Node premise = nm->mkNode(Kind::SEXPR, d_cl, eq);
1670 : 74 : success &=
1671 : 74 : addAletheStep(AletheRule::REFL, premise, premise, {}, {}, *cdp);
1672 : 222 : std::vector<Node> bVars{quant[0].begin(), quant[0].end()};
1673 : 148 : std::vector<Node> skoSubstitutions;
1674 : 74 : SkolemManager* sm = nm->getSkolemManager();
1675 : 74 : const std::map<Node, Node>& skolemDefs = d_anc.getSkolemDefinitions();
1676 [ + + ]: 187 : for (size_t i = 0, size = quant[0].getNumChildren(); i < size; ++i)
1677 : : {
1678 : : // Make the Skolem corresponding to this variable and retrieve its
1679 : : // conversion from the node converter
1680 : 565 : std::vector<Node> cacheVals{quant, nm->mkConstInt(Rational(i))};
1681 : : Node sk =
1682 : 113 : sm->mkSkolemFunction(SkolemId::QUANTIFIERS_SKOLEMIZE, cacheVals);
1683 [ - + ][ - + ]: 113 : Assert(!sk.isNull());
[ - - ]
1684 [ - + ]: 113 : if (options().proof.proofAletheDefineSkolems)
1685 : : {
1686 : 0 : skoSubstitutions.push_back(quant[0][i].eqNode(sk));
1687 : 0 : continue;
1688 : : }
1689 : 113 : auto it = skolemDefs.find(sk);
1690 : 113 : Assert(it != skolemDefs.end()) << sk << " " << skolemDefs;
1691 : 113 : skoSubstitutions.push_back(quant[0][i].eqNode(it->second));
1692 : : }
1693 [ - + ][ - + ]: 74 : Assert(!d_anc.convert(quant.eqNode(skolemized)).isNull());
[ - - ]
1694 : : Node conclusion = nm->mkNode(
1695 : 222 : Kind::SEXPR, d_cl, d_anc.convert(quant.eqNode(skolemized)));
1696 : : // add the sko step
1697 : 222 : success &= addAletheStep(AletheRule::ANCHOR_SKO_FORALL,
1698 : : conclusion,
1699 : : conclusion,
1700 : : {premise},
1701 : : skoSubstitutions,
1702 : 148 : *cdp);
1703 : : // add congruence step with NOT for the forall case
1704 : : Node newConclusion = nm->mkNode(
1705 : 222 : Kind::SEXPR, d_cl, (quant.notNode()).eqNode(skolemized.notNode()));
1706 : 222 : success &= addAletheStep(AletheRule::CONG,
1707 : : newConclusion,
1708 : : newConclusion,
1709 : : {conclusion},
1710 : : {},
1711 : 148 : *cdp);
1712 : 74 : conclusion = newConclusion;
1713 : : // now equality resolution reasoning
1714 : : Node vp1 = nm->mkNode(
1715 : : Kind::SEXPR,
1716 : 444 : {d_cl, conclusion[1].notNode(), children[0].notNode(), res});
1717 : 74 : success &= addAletheStep(AletheRule::EQUIV_POS2, vp1, vp1, {}, {}, *cdp);
1718 : : return success
1719 : 666 : && addAletheStep(AletheRule::RESOLUTION,
1720 : : res,
1721 : 148 : nm->mkNode(Kind::SEXPR, d_cl, res),
1722 : 74 : {vp1, conclusion, children[0]},
1723 : 148 : d_resPivots ? std::vector<Node>{conclusion[1],
1724 : 0 : d_false,
1725 : 0 : children[0],
1726 : 0 : d_false}
1727 : : : std::vector<Node>(),
1728 [ + - ]: 296 : *cdp);
1729 : : }
1730 : : // ======== Bitvector
1731 : : //
1732 : : // ------------------------ BV_BITBLAST_STEP_BV<KIND>
1733 : : // (cl (= t bitblast(t)))
1734 : 4 : case ProofRule::BV_EAGER_ATOM:
1735 : : {
1736 : 8 : Assert(res.getKind() == Kind::EQUAL && res[0][0] == res[1]);
1737 : 8 : Node newRes = res[0][0].eqNode(res[1]);
1738 : 16 : return addAletheStep(AletheRule::REFL,
1739 : : res,
1740 : 8 : nm->mkNode(Kind::SEXPR, d_cl, newRes),
1741 : : children,
1742 : : {},
1743 : 4 : *cdp);
1744 : : }
1745 : : // ------------------------ BV_BITBLAST_STEP_BV<KIND>
1746 : : // (cl (= t bitblast(t)))
1747 : 5839 : case ProofRule::BV_BITBLAST_STEP:
1748 : : {
1749 : 5839 : Kind k = res[0].getKind();
1750 : : // no checking for those yet in Carcara or Isabelle, so we produce holes
1751 [ + + ][ + + ]: 5839 : if (k == Kind::BITVECTOR_UDIV || k == Kind::BITVECTOR_UREM
1752 [ + + ][ + + ]: 5830 : || k == Kind::BITVECTOR_SHL || k == Kind::BITVECTOR_LSHR
1753 [ + + ]: 5721 : || k == Kind::BITVECTOR_ASHR)
1754 : : {
1755 : 672 : return addAletheStep(AletheRule::HOLE,
1756 : : res,
1757 : 336 : nm->mkNode(Kind::SEXPR, d_cl, res),
1758 : : children,
1759 : : {},
1760 : 168 : *cdp);
1761 : : }
1762 : : // if the term being bitblasted is a variable or a nonbv term, then this
1763 : : // is a "bitblast var" step
1764 : 5671 : auto it = s_bvKindToAletheRule.find(k);
1765 [ + + ]: 27634 : return addAletheStep(it == s_bvKindToAletheRule.end()
1766 : : ? AletheRule::BV_BITBLAST_STEP_VAR
1767 : 4950 : : it->second,
1768 : : res,
1769 : 11342 : nm->mkNode(Kind::SEXPR, d_cl, res),
1770 : : children,
1771 : : {},
1772 : 5671 : *cdp);
1773 : : }
1774 : : //================================================= Quantifiers rules
1775 : : // ======== Instantiate
1776 : : //
1777 : : // ----- FORALL_INST, t1 ... tn
1778 : : // VP1
1779 : : // ----- OR
1780 : : // VP2 P
1781 : : // -------------------- RESOLUTION
1782 : : // (cl F*sigma)^
1783 : : //
1784 : : // VP1: (cl (or (not (forall ((x1 T1) ... (xn Tn)) F*sigma)
1785 : : // VP2: (cl (not (forall ((x1 T1) ... (xn Tn)) F)) F*sigma)
1786 : : //
1787 : : // ^ the corresponding proof node is F*sigma
1788 : 847 : case ProofRule::INSTANTIATE:
1789 : : {
1790 : : Node vp1 = nm->mkNode(
1791 : 2541 : Kind::SEXPR, d_cl, nm->mkNode(Kind::OR, children[0].notNode(), res));
1792 : 1694 : Node vp2 = nm->mkNode(Kind::SEXPR, d_cl, children[0].notNode(), res);
1793 [ + - ][ + - ]: 847 : return addAletheStep(AletheRule::FORALL_INST,
[ - - ][ - - ]
[ - - ]
1794 : : vp1,
1795 : : vp1,
1796 : : {},
1797 : 1694 : std::vector<Node>{args[0].begin(), args[0].end()},
1798 : : *cdp)
1799 : 2539 : && addAletheStep(AletheRule::OR, vp2, vp2, {vp1}, {}, *cdp)
1800 : 7617 : && addAletheStep(AletheRule::RESOLUTION,
1801 : : res,
1802 : 1693 : nm->mkNode(Kind::SEXPR, d_cl, res),
1803 : 846 : {vp2, children[0]},
1804 : 846 : d_resPivots
1805 : 1693 : ? std::vector<Node>{children[0], d_false}
1806 : : : std::vector<Node>(),
1807 [ + + ]: 2539 : *cdp);
1808 : : }
1809 : : // ======== Alpha Equivalence
1810 : : //
1811 : : // Given the formula F := (forall ((y1 A1) ... (yn An)) G) and a
1812 : : // substitution sigma, the resulting Alethe steps justifying the conclusion
1813 : : // (= F F*sigma) depend on a number of conditions, which are detailed below.
1814 : : //
1815 : : // If sigma is the identity, F*sigma is the same as F, and the resulting
1816 : : // step is
1817 : : //
1818 : : // ------------------ refl
1819 : : // (cl (= F F))
1820 : : //
1821 : : // When sigma is the substitution {y1->z1, ..., yn->zn, ..., yn+k->zn+k}, we
1822 : : // are in the case where G has quantifiers whose variables are yn+1 ... yn+k
1823 : : // and they will be renamed to zn+1 ... zn+k. The generated Alethe proof is
1824 : : //
1825 : : // --------------------------------------- refl
1826 : : // (cl (= G G*{y1 -> z1, ..., yn -> zn}))
1827 : : // --------------------------------- bind, z1 ... zn (= y1 z1) ... (= yn zn)
1828 : : // (cl (= F (forall ((z1 A1) ... (zn An)) G*{y1 -> z1, ..., yn -> zn})))
1829 : : //
1830 : : // i.e., we drop the suffix of the substitution beyond the variables of the
1831 : : // outermost quantifier. This is valid in Alethe because the validity of
1832 : : // "refl", under a rule that introduces a context, such as "bind", is itself
1833 : : // tested modulo alpha-equivalence. An alternative would be to use the rest
1834 : : // of the substitution to do new "bind" steps for the innermost quantifiers.
1835 : : //
1836 : : // If sigma contains more than one variable with the same name but with
1837 : : // different types (which makes them different for cvc5 but not in the
1838 : : // substitution induced by Alethe's context), we introduce an intermediate
1839 : : // alpha equivalence step with fresh variables. For example if F := (forall
1840 : : // ((y1 A1) (y2 A2)) G) and sigma is the substitution {y1 -> z1, y2 -> y1},
1841 : : // where the "y1" in the right hand side has another type "T" other than
1842 : : // "A2", then the resulting steps are
1843 : : //
1844 : : // --------------------------------------- refl
1845 : : // (cl (= G G*{y1 -> @v1, y2 -> @v2})
1846 : : // --------------------------------- bind, @v1 @v2 (= y1 @v1) (= y1 @v2)
1847 : : // (cl (= F (forall ((@v1 A1) (@v2 A2)) G*{y1 -> @v1, y2 -> @v2})
1848 : : //
1849 : : // --------------------------------------------------- refl
1850 : : // (cl (= G*{y1->@v1, y2->@v2} (G*{y1->@v1, y2->@v2})*{@v1->z1, @v1->y1})
1851 : : // --------------------------------------- bind, z1 y1 (= @v1 z1) (= @v2 z2)
1852 : : // (cl (=
1853 : : // (forall ((@v1 A1) (@v2 A2)) G*{y1 -> @v1, y2 -> @v2})
1854 : : // (forall ((z1 A1) (y1 A2)) (G*{y1->@v1, y2->@v2})*{@v1->z1, @v1->y1})))
1855 : : //
1856 : : // and finally a transitivity step to conclude an equality between F and
1857 : : // (forall ((z1 A1) (y1 A2)) (G*{y1->@v1, y2->@v2})*{@v1->z1, @v1->y1}).
1858 : : //
1859 : : // If none of the conditions above applies, the resulting Alethe steps are
1860 : : //
1861 : : // ------------------ refl
1862 : : // (cl (= G G*sigma))
1863 : : // -------------------- bind, z1 ... zn (= y1 z1) ... (= yn zn)
1864 : : // (cl (= F (forall ((z1 A1) ... (zn An)) G*sigma)))
1865 : 20 : case ProofRule::ALPHA_EQUIV:
1866 : : {
1867 : : // If y1 ... yn are mapped to y1 ... yn it suffices to use a refl step
1868 : 20 : bool allSame = true;
1869 : 40 : std::unordered_set<std::string> lhsNames;
1870 [ + + ]: 56 : for (size_t i = 0, size = res[0][0].getNumChildren(); i < size; ++i)
1871 : : {
1872 : 144 : Node v0 = res[0][0][i], v1 = res[1][0][i];
1873 : 36 : lhsNames.insert(v0.getName());
1874 [ + + ][ - + ]: 36 : allSame = allSame && v0 == v1;
1875 : : }
1876 : : // when no renaming, no-op
1877 [ - + ]: 20 : if (allSame)
1878 : : {
1879 : 0 : return addAletheStep(AletheRule::REFL,
1880 : : res,
1881 : 0 : nm->mkNode(Kind::SEXPR, d_cl, res),
1882 : : {},
1883 : : {},
1884 : 0 : *cdp);
1885 : : }
1886 : : // check if any name in the rhs variables clashes with a name in the lhs
1887 : 20 : bool hasClash = false;
1888 [ + + ]: 56 : for (const Node& v : res[1][0])
1889 : : {
1890 [ + + ]: 36 : if (lhsNames.count(v.getName()))
1891 : : {
1892 : 8 : hasClash = true;
1893 : : }
1894 : : }
1895 : 20 : bool success = true;
1896 : 40 : Node lhsQ = res[0];
1897 : 40 : std::vector<Node> transEqs;
1898 [ + + ]: 20 : if (hasClash)
1899 : : {
1900 : : // create the variables to substitute the lhs variables
1901 : 12 : std::vector<Node> freshRenaming;
1902 [ + + ]: 18 : for (const Node& v : res[0][0])
1903 : : {
1904 : 12 : freshRenaming.emplace_back(NodeManager::mkBoundVar(v.getType()));
1905 : : }
1906 : 18 : std::vector<Node> vars{res[0][0].begin(), res[0][0].end()};
1907 : : Node lhsRenamed = res[0].substitute(vars.begin(),
1908 : : vars.end(),
1909 : : freshRenaming.begin(),
1910 : 12 : freshRenaming.end());
1911 : : // Reflexivity over the quantified bodies
1912 : : Node reflConc =
1913 : 18 : nm->mkNode(Kind::SEXPR, d_cl, res[0][1].eqNode(lhsRenamed[1]));
1914 : 6 : addAletheStep(AletheRule::REFL, reflConc, reflConc, {}, {}, *cdp);
1915 : : // Collect RHS variables first for arguments, then add the entries for
1916 : : // the substitution. In a "bind" rule we must always list all the
1917 : : // variables
1918 : 12 : std::vector<Node> bindArgs{freshRenaming.begin(), freshRenaming.end()};
1919 [ + + ]: 18 : for (size_t i = 0, size = freshRenaming.size(); i < size; ++i)
1920 : : {
1921 : 12 : bindArgs.push_back(vars[i].eqNode(freshRenaming[i]));
1922 : : }
1923 : 6 : transEqs.push_back(res[0].eqNode(lhsRenamed));
1924 : 24 : success &= addAletheStep(AletheRule::ANCHOR_BIND,
1925 : 6 : transEqs.back(),
1926 : 12 : nm->mkNode(Kind::SEXPR, d_cl, transEqs.back()),
1927 : : {reflConc},
1928 : : bindArgs,
1929 : 12 : *cdp);
1930 : 6 : lhsQ = lhsRenamed;
1931 : : }
1932 : : // Reflexivity over the quantified bodies
1933 : 60 : Node reflConc = nm->mkNode(Kind::SEXPR, d_cl, lhsQ[1].eqNode(res[1][1]));
1934 : 20 : addAletheStep(AletheRule::REFL, reflConc, reflConc, {}, {}, *cdp);
1935 : : // Collect RHS variables first for arguments, then add the entries for
1936 : : // the substitution. In a "bind" rule we must always list all the
1937 : : // variables
1938 : 60 : std::vector<Node> bindArgs{res[1][0].begin(), res[1][0].end()};
1939 [ + + ]: 56 : for (size_t i = 0, size = res[1][0].getNumChildren(); i < size; ++i)
1940 : : {
1941 : 36 : bindArgs.push_back(lhsQ[0][i].eqNode(res[1][0][i]));
1942 : : }
1943 : 20 : transEqs.push_back(lhsQ.eqNode(res[1]));
1944 : 80 : success &= addAletheStep(AletheRule::ANCHOR_BIND,
1945 : 20 : transEqs.back(),
1946 : 40 : nm->mkNode(Kind::SEXPR, d_cl, transEqs.back()),
1947 : : {reflConc},
1948 : : bindArgs,
1949 : 40 : *cdp);
1950 [ + + ][ - + ]: 20 : Assert(!hasClash || transEqs.size() == 2);
[ - + ][ - - ]
1951 [ + + ]: 20 : if (hasClash)
1952 : : {
1953 : : return success
1954 : 24 : && addAletheStep(AletheRule::TRANS,
1955 : : res,
1956 : 12 : nm->mkNode(Kind::SEXPR, d_cl, res),
1957 : : transEqs,
1958 : : {},
1959 [ + - ]: 6 : *cdp);
1960 : : }
1961 [ - + ][ - + ]: 14 : Assert(cdp->hasStep(res));
[ - - ]
1962 : 14 : return success;
1963 : : }
1964 : : // ======== Variable reordering
1965 : : // Let X = ((x1 T1) ... (xn Tn)), Y = ((y1 U1) ... (yn Un))
1966 : : // and Z = ((x1 T1) ... (xn Tn) (y1 U1) ... (yn Un))
1967 : : // Then, res is (cl (= (forall ((x1 T1) ... (xn Tn)) F) (forall ((y1 U1) ...
1968 : : // (yn Un)) F)))
1969 : : //
1970 : : // ----- QNT_RM_UNUSED
1971 : : // VP1
1972 : : // ----- SYMM ----- QNT_RM_UNUSED
1973 : : // VP2 VP3
1974 : : // ----------------- TRANS
1975 : : // res
1976 : : //
1977 : : // VP1: (cl (= (forall Z F) (forall X F)))
1978 : : // VP2: (cl (= (forall X F) (forall Z F)))
1979 : : // VP3: (cl (= (forall Z F) (forall Y F)))
1980 : 4 : case ProofRule::QUANT_VAR_REORDERING:
1981 : : {
1982 : 8 : Node forall_X = res[0];
1983 : 8 : Node forall_Y = res[1];
1984 : 8 : Node F = forall_X[1];
1985 : 8 : Node X = forall_X[0];
1986 : 8 : Node Y = forall_Y[0];
1987 : 8 : std::vector<Node> Z(X.begin(), X.end());
1988 : 4 : Z.insert(Z.end(), Y.begin(), Y.end());
1989 : : Node forall_Z =
1990 : 12 : nm->mkNode(Kind::FORALL, nm->mkNode(Kind::BOUND_VAR_LIST, Z), F);
1991 : 12 : Node vp1 = nm->mkNode(Kind::EQUAL, forall_Z, forall_X);
1992 : 12 : Node vp2 = nm->mkNode(Kind::EQUAL, forall_X, forall_Z);
1993 : 8 : Node vp3 = nm->mkNode(Kind::EQUAL, forall_Z, forall_Y);
1994 : :
1995 [ + - ][ - - ]: 8 : return addAletheStep(AletheRule::QNT_RM_UNUSED,
[ - - ][ - - ]
1996 : : vp1,
1997 : 8 : nm->mkNode(Kind::SEXPR, d_cl, vp1),
1998 : : {},
1999 : : {},
2000 : : *cdp)
2001 : 20 : && addAletheStep(AletheRule::SYMM,
2002 : : vp2,
2003 : 8 : nm->mkNode(Kind::SEXPR, d_cl, vp2),
2004 : : {vp1},
2005 : : {},
2006 : 4 : *cdp)
2007 : 16 : && addAletheStep(AletheRule::QNT_RM_UNUSED,
2008 : : vp3,
2009 : 8 : nm->mkNode(Kind::SEXPR, d_cl, vp3),
2010 : : {},
2011 : : {},
2012 : : *cdp)
2013 : 32 : && addAletheStep(AletheRule::TRANS,
2014 : : res,
2015 : 8 : nm->mkNode(Kind::SEXPR, d_cl, res),
2016 : : {vp2, vp3},
2017 : : {},
2018 [ + - ]: 12 : *cdp);
2019 : : }
2020 : : //================================================= Arithmetic rules
2021 : : // ======== Adding Scaled Inequalities
2022 : : //
2023 : : // -------------------------------------- LA_GENERIC
2024 : : // (cl (not P1) ... (not Pn) (>< t1 t2)) P1 ... Pn
2025 : : // ------------------------------------------------------------- RESOLUTION
2026 : : // (cl (>< t1 t2))*
2027 : : //
2028 : : // * the corresponding proof node is (>< t1 t2)
2029 : 6303 : case ProofRule::ARITH_SUM_UB:
2030 : : {
2031 : : // if the conclusion were an equality we'd need to phrase LA_GENERIC in
2032 : : // terms of disequalities, but ARITH_SUM_UB does not have equalities as
2033 : : // conclusions
2034 [ - + ][ - + ]: 6303 : Assert(res.getKind() != Kind::EQUAL);
[ - - ]
2035 : 12606 : Node one = nm->mkConstReal(Rational(1));
2036 : 12606 : Node minusOne = nm->mkConstReal(Rational(-1));
2037 : 12606 : std::vector<Node> resArgs;
2038 : 12606 : std::vector<Node> resChildren;
2039 : 25212 : std::vector<Node> lits{d_cl};
2040 [ + + ]: 37059 : for (const Node& child : children)
2041 : : {
2042 : 30756 : lits.push_back(child.notNode());
2043 : : // equalities are multiplied by minus 1 rather than 1
2044 [ + + ]: 30756 : new_args.push_back(child.getKind() == Kind::EQUAL ? minusOne : one);
2045 : 30756 : resArgs.push_back(child);
2046 : 30756 : resArgs.push_back(d_false);
2047 : : }
2048 : 6303 : lits.push_back(res);
2049 : 6303 : new_args.push_back(one);
2050 : 6303 : Node laGen = nm->mkNode(Kind::SEXPR, lits);
2051 : 6303 : addAletheStep(AletheRule::LA_GENERIC, laGen, laGen, {}, new_args, *cdp);
2052 : 6303 : resChildren.push_back(laGen);
2053 : 6303 : resChildren.insert(resChildren.end(), children.begin(), children.end());
2054 : 12606 : return addAletheStep(AletheRule::RESOLUTION,
2055 : : res,
2056 : 12606 : nm->mkNode(Kind::SEXPR, d_cl, res),
2057 : : resChildren,
2058 [ - + ]: 12606 : d_resPivots ? resArgs : std::vector<Node>(),
2059 : 6303 : *cdp);
2060 : : }
2061 : : // Direct translation
2062 : 5612 : case ProofRule::ARITH_MULT_POS:
2063 : : case ProofRule::ARITH_MULT_NEG:
2064 : : {
2065 [ + + ]: 22448 : return addAletheStep(id == ProofRule::ARITH_MULT_POS
2066 : : ? AletheRule::LA_MULT_POS
2067 : : : AletheRule::LA_MULT_NEG,
2068 : : res,
2069 : 11224 : nm->mkNode(Kind::SEXPR, d_cl, res),
2070 : : children,
2071 : : {},
2072 : 5612 : *cdp);
2073 : : }
2074 : : // ======== Tightening Strict Integer Upper Bounds
2075 : : //
2076 : : // ----- LA_GENERIC, 1
2077 : : // VP1 P
2078 : : // ------------------------------------- RESOLUTION
2079 : : // (cl (<= i greatestIntLessThan(c)))*
2080 : : //
2081 : : // VP1: (cl (not (< i c)) (<= i greatestIntLessThan(c)))
2082 : : //
2083 : : // * the corresponding proof node is (<= i greatestIntLessThan(c))
2084 : 1326 : case ProofRule::INT_TIGHT_UB:
2085 : : {
2086 : 3978 : Node vp1 = nm->mkNode(Kind::SEXPR, d_cl, children[0].notNode(), res);
2087 : 6630 : std::vector<Node> new_children = {vp1, children[0]};
2088 : 1326 : Node one = nm->mkConstReal(Rational(1));
2089 : 1326 : new_args.push_back(one);
2090 : 1326 : new_args.push_back(one);
2091 [ + - ][ + - ]: 1326 : return addAletheStep(AletheRule::LA_GENERIC, vp1, vp1, {}, new_args, *cdp)
[ - - ][ - - ]
[ - - ]
2092 [ + - ][ + - ]: 3978 : && addAletheStep(AletheRule::RESOLUTION,
[ - - ]
2093 : : res,
2094 : 2652 : nm->mkNode(Kind::SEXPR, d_cl, res),
2095 : : new_children,
2096 : 1326 : d_resPivots
2097 : 2652 : ? std::vector<Node>{children[0], d_false}
2098 : : : std::vector<Node>(),
2099 [ + - ]: 1326 : *cdp);
2100 : : }
2101 : : // ======== Tightening Strict Integer Lower Bounds
2102 : : //
2103 : : // ----- LA_GENERIC, 1
2104 : : // VP1 P
2105 : : // ------------------------------------- RESOLUTION
2106 : : // (cl (>= i leastIntGreaterThan(c)))*
2107 : : //
2108 : : // VP1: (cl (not (> i c)) (>= i leastIntGreaterThan(c)))
2109 : : //
2110 : : // * the corresponding proof node is (>= i leastIntGreaterThan(c))
2111 : 133 : case ProofRule::INT_TIGHT_LB:
2112 : : {
2113 : 399 : Node vp1 = nm->mkNode(Kind::SEXPR, d_cl, children[0].notNode(), res);
2114 : 665 : std::vector<Node> new_children = {vp1, children[0]};
2115 : 133 : Node one = nm->mkConstReal(Rational(1));
2116 : 133 : new_args.push_back(one);
2117 : 133 : new_args.push_back(one);
2118 [ + - ][ + - ]: 133 : return addAletheStep(AletheRule::LA_GENERIC, vp1, vp1, {}, new_args, *cdp)
[ - - ][ - - ]
[ - - ]
2119 [ + - ][ + - ]: 399 : && addAletheStep(AletheRule::RESOLUTION,
[ - - ]
2120 : : res,
2121 : 266 : nm->mkNode(Kind::SEXPR, d_cl, res),
2122 : : new_children,
2123 : 133 : d_resPivots
2124 : 266 : ? std::vector<Node>{children[0], d_false}
2125 : : : std::vector<Node>(),
2126 [ + - ]: 133 : *cdp);
2127 : : }
2128 : : // ======== Trichotomy of the reals
2129 : : //
2130 : : // C is always of the format (= x c), (> x c) or (< x c). It has to be
2131 : : // concluded from A, B, which are (=> x c), (<= x c), or (not (= x c)). In
2132 : : // some cases, rather than (=> x c) we can actually have its negation, i.e.,
2133 : : // (not (< x c)), which is accounted for below.
2134 : : //
2135 : : // The convertion into Alethe is based on la_disequality, which has much
2136 : : // the same semantics as ARITH_TRICHOTOMY. The following subproof is
2137 : : // common to all the cases (we will refer to it as PI_0):
2138 : : //
2139 : : // ------------------------------------------------------ la_disequality
2140 : : // (cl (or (= x c) (not (<= x c)) (not (<= c x))))
2141 : : // -------------------------------------------------------- or
2142 : : // (cl (= x c) (not (<= x c)) (not (<= c x)))
2143 : : //
2144 : : // The transformations also use the COMP_SIMPLIFY rule in Alethe, which
2145 : : // connects strict and non-strict inequalities. The details for each
2146 : : // conversion are given for each case.
2147 : 874 : case ProofRule::ARITH_TRICHOTOMY:
2148 : : {
2149 : 874 : bool success = true;
2150 : 1748 : Node equal, lesser, greater;
2151 : 874 : Kind k = res.getKind();
2152 [ + + ][ + + ]: 874 : Assert(k == Kind::EQUAL || k == Kind::GT || k == Kind::LT)
[ - + ][ - + ]
[ - - ]
2153 : 0 : << "kind is " << k << "\n";
2154 : 1748 : Node x = res[0], c = res[1];
2155 : : switch (k)
2156 : : {
2157 : 568 : case Kind::EQUAL:
2158 : : {
2159 [ + - ]: 568 : Trace("alethe-proof") << "..case EQUAL\n";
2160 : 1136 : Node leq, geq;
2161 [ + + ]: 568 : if (children[0].getKind() == Kind::LEQ)
2162 : : {
2163 : 20 : leq = children[0];
2164 : 20 : geq = children[1];
2165 : : }
2166 : : else
2167 : : {
2168 : 548 : leq = children[1];
2169 : 548 : geq = children[0];
2170 : : }
2171 : 1704 : Node leqInverted = nm->mkNode(Kind::LEQ, geq[1], geq[0]);
2172 : : // The subproof built is (where @p1 is the premise for "geq", @p2 is
2173 : : // "leqInverted")
2174 : : //
2175 : : // PI_1:
2176 : : // with @p0: (= (=> x c) (<= c x))
2177 : : // with @p1: (=> x c)
2178 : : // with @p2: (<= c x)
2179 : : //
2180 : : // ----- comp_simplify -------------------equiv_pos2 --- geq
2181 : : // @p0 (cl (not @p0) (not @p1) @p2) @p1
2182 : : // ---------------------------------------------------- resolution
2183 : : // @p2
2184 : : //
2185 : : // Then we combine with the proof PI_0 and use the other premise
2186 : : // (for "leq")
2187 : : //
2188 : : // --------- leq
2189 : : // PI_0 (<= x c) PI_1
2190 : : // --------------------------- resolution
2191 : : // (= x c)
2192 : : //
2193 : : // where (= x c) is the expected result
2194 : :
2195 : : // We first build PI_0:
2196 : : Node laDiseqOr = nm->mkNode(
2197 : : Kind::SEXPR,
2198 : 568 : d_cl,
2199 : 1704 : nm->mkNode(Kind::OR, res, leq.notNode(), leqInverted.notNode()));
2200 : : Node laDiseqCl = nm->mkNode(
2201 : 3976 : Kind::SEXPR, {d_cl, res, leq.notNode(), leqInverted.notNode()});
2202 : 568 : success &=
2203 [ + - ][ + - ]: 568 : addAletheStep(AletheRule::LA_DISEQUALITY,
[ + - ][ - - ]
[ - - ][ - - ]
[ - - ]
2204 : : laDiseqOr,
2205 : : laDiseqOr,
2206 : : {},
2207 : : {},
2208 : : *cdp)
2209 : 1704 : && addAletheStep(
2210 [ + - ]: 1136 : AletheRule::OR, laDiseqCl, laDiseqCl, {laDiseqOr}, {}, *cdp);
2211 : : // Now we build PI_1:
2212 : 1136 : Node compSimp = geq.eqNode(leqInverted);
2213 : 1704 : Node compSimpCl = nm->mkNode(Kind::SEXPR, d_cl, compSimp);
2214 : 1136 : success &= addAletheStep(
2215 : 568 : AletheRule::COMP_SIMPLIFY, compSimpCl, compSimpCl, {}, {}, *cdp);
2216 : : Node equivPos2Cl = nm->mkNode(
2217 : : Kind::SEXPR,
2218 : 3976 : {d_cl, compSimp.notNode(), geq.notNode(), leqInverted});
2219 : 1136 : success &= addAletheStep(
2220 : 568 : AletheRule::EQUIV_POS2, equivPos2Cl, equivPos2Cl, {}, {}, *cdp);
2221 : 1704 : Node resPi1Conc = nm->mkNode(Kind::SEXPR, d_cl, leqInverted);
2222 [ + + ][ - - ]: 2840 : success &= addAletheStep(
2223 : : AletheRule::RESOLUTION,
2224 : : resPi1Conc,
2225 : : resPi1Conc,
2226 : : {compSimpCl, equivPos2Cl, geq},
2227 : 1136 : d_resPivots ? std::vector<Node>{compSimp, d_true, geq, d_false}
2228 : : : std::vector<Node>(),
2229 : 2272 : *cdp);
2230 : : // Now we build the final resultion
2231 [ + + ][ - - ]: 3408 : success &= addAletheStep(
2232 : : AletheRule::RESOLUTION,
2233 : : res,
2234 : 1136 : nm->mkNode(Kind::SEXPR, d_cl, res),
2235 : : {leq, laDiseqCl, resPi1Conc},
2236 : 1136 : d_resPivots ? std::vector<Node>{leq, d_true, leqInverted, d_false}
2237 : : : std::vector<Node>(),
2238 : 2272 : *cdp);
2239 : 568 : break;
2240 : : }
2241 : 210 : case Kind::GT:
2242 : : {
2243 [ + - ]: 210 : Trace("alethe-proof") << "..case GT\n";
2244 : 420 : Node geq, notEq;
2245 : 210 : Kind kc0 = children[0].getKind();
2246 : 210 : if (kc0 == Kind::GEQ
2247 [ + + ][ + - ]: 210 : || (kc0 == Kind::NOT && children[0][0].getKind() == Kind::LT))
[ + + ][ + + ]
[ + + ][ - - ]
2248 : : {
2249 : 151 : geq = children[0];
2250 : 151 : notEq = children[1];
2251 : : }
2252 : : else
2253 : : {
2254 : 59 : geq = children[1];
2255 : 59 : notEq = children[0];
2256 : : }
2257 : 630 : Node leq = nm->mkNode(Kind::LEQ, x, c);
2258 : 630 : Node leqInverted = nm->mkNode(Kind::LEQ, c, x);
2259 : 420 : Assert(notEq.getKind() == Kind::NOT
2260 : : && notEq[0].getKind() == Kind::EQUAL);
2261 : : // it may be that the premise supposed to be (>= x c) is actually the
2262 : : // literal (not (< x c)). In this case we use that premise to deriv
2263 : : // (>= x c), so that the reconstruction below remains the same
2264 [ + + ]: 210 : if (geq.getKind() != Kind::GEQ)
2265 : : {
2266 : 92 : Assert(geq.getKind() == Kind::NOT && geq[0].getKind() == Kind::LT);
2267 : 92 : Node notLt = geq;
2268 : 46 : geq = nm->mkNode(Kind::GEQ, x, c);
2269 : : // @pa: (= (< x c) (not (<= c x)))
2270 : : // @pb: (< x c)
2271 : : // @pc: (<= c x)
2272 : : // notLT : (not @pb)
2273 : : //
2274 : : // PI_a:
2275 : : //
2276 : : // --- comp_simplify --------------------- equiv_pos1 ----- notLT
2277 : : // @pa (cl (not @pa) @pb (not (not @pc))) (not @pb)
2278 : : // ------------------------------------------------------ resolution
2279 : : // (cl (not (not @pc)))
2280 : : //
2281 : : //
2282 : : // PI_b:
2283 : : //
2284 : : // ------------------------------ NOT_NOT -------------------- PI_a
2285 : : // (cl (not (not (not @pc))) @pc) (cl (not (not @pc)))
2286 : : // ------------------------------------------------------ resolution
2287 : : // @pc
2288 : : //
2289 : : // PI_c:
2290 : : //
2291 : : // @pd: (= (>= x c) (<= c x))
2292 : : //
2293 : : // --- comp_simplify -------------------------- equiv_pos1 --- PI_b
2294 : : // @pd (cl (not @pd) (>= x c) (not @pc)) @pc
2295 : : // ------------------------------------------------------ resolution
2296 : : // (cl (>= x c))
2297 : : //
2298 : 92 : Node pb = notLt[0];
2299 : 92 : Node pc = leqInverted;
2300 : 92 : Node pa = pb.eqNode(pc.notNode());
2301 : : // We first build PI_a:
2302 : 138 : Node compSimpCl = nm->mkNode(Kind::SEXPR, d_cl, pa);
2303 : 92 : success &= addAletheStep(AletheRule::COMP_SIMPLIFY,
2304 : : compSimpCl,
2305 : : compSimpCl,
2306 : : {},
2307 : : {},
2308 : 46 : *cdp);
2309 : : Node equivPos1Cl = nm->mkNode(
2310 : 322 : Kind::SEXPR, {d_cl, pa.notNode(), pb, pc.notNode().notNode()});
2311 : 92 : success &= addAletheStep(
2312 : 46 : AletheRule::EQUIV_POS1, equivPos1Cl, equivPos1Cl, {}, {}, *cdp);
2313 : : Node resPiAConc =
2314 : 138 : nm->mkNode(Kind::SEXPR, d_cl, pc.notNode().notNode());
2315 [ + + ][ - - ]: 230 : success &= addAletheStep(
2316 : : AletheRule::RESOLUTION,
2317 : : resPiAConc,
2318 : : resPiAConc,
2319 : : {compSimpCl, equivPos1Cl, pb.notNode()},
2320 : 92 : d_resPivots ? std::vector<Node>{pa, d_true, pb, d_true}
2321 : : : std::vector<Node>(),
2322 : 184 : *cdp);
2323 : : // We then build PI_b:
2324 : 138 : Node notNot = pc.notNode().notNode().notNode();
2325 : : Node notNotCl =
2326 : 138 : nm->mkNode(Kind::SEXPR, d_cl, pc.notNode().notNode().notNode());
2327 : 92 : success &= addAletheStep(
2328 : 46 : AletheRule::NOT_NOT, notNotCl, notNotCl, {}, {}, *cdp);
2329 : : Node resPiBConc =
2330 : 138 : nm->mkNode(Kind::SEXPR, d_cl, pc.notNode().notNode());
2331 [ + + ][ - - ]: 184 : success &= addAletheStep(
2332 : : AletheRule::RESOLUTION,
2333 : : resPiBConc,
2334 : : resPiBConc,
2335 : : {notNotCl, resPiAConc},
2336 : 92 : d_resPivots ? std::vector<Node>{pc.notNode().notNode(), d_false}
2337 : : : std::vector<Node>(),
2338 : 138 : *cdp);
2339 : : // Now we conclude, building PI_c
2340 : 46 : Node pd = geq.eqNode(pc);
2341 : 46 : compSimpCl = nm->mkNode(Kind::SEXPR, d_cl, pd);
2342 : 92 : success &= addAletheStep(AletheRule::COMP_SIMPLIFY,
2343 : : compSimpCl,
2344 : : compSimpCl,
2345 : : {},
2346 : : {},
2347 : 46 : *cdp);
2348 [ + + ][ - - ]: 322 : equivPos1Cl = nm->mkNode(Kind::SEXPR,
2349 : 368 : {d_cl, pd.notNode(), geq, pc.notNode()});
2350 : 92 : success &= addAletheStep(
2351 : 46 : AletheRule::EQUIV_POS1, equivPos1Cl, equivPos1Cl, {}, {}, *cdp);
2352 [ + + ][ - - ]: 276 : success &= addAletheStep(
2353 : : AletheRule::RESOLUTION,
2354 : : geq,
2355 : 92 : nm->mkNode(Kind::SEXPR, d_cl, geq),
2356 : : {compSimpCl, equivPos1Cl, resPiBConc},
2357 : 92 : d_resPivots ? std::vector<Node>{pd, d_true, pc, d_false}
2358 : : : std::vector<Node>(),
2359 : 184 : *cdp);
2360 : : }
2361 : : // The subproof built here uses the PI_1 defined in the case above,
2362 : : // where the premise for "geq" is used to conclude leqInverted. Here
2363 : : // @p4 is "res", @p5 is "leq". The goal of PI_2 is to conclude (not
2364 : : // (not @p5)), which can remove the element from the conclusion of
2365 : : // PI_0 that is (not @p5). The conclusion of PI_1 and notEq exclude
2366 : : // the other elements, such that only @p4 will remain, the expected
2367 : : // conclusion.
2368 : : //
2369 : : // PI_2:
2370 : : // with @p3: (= (> x c) (not (<= x c)))
2371 : : // with @p4: (> x c)
2372 : : // with @p5: (<= x c)
2373 : : //
2374 : : // ----- comp_simplify ----------------------------------- equiv_pos1
2375 : : // @p3 (cl (not @p3) @p4 (not (not @p5)))
2376 : : // ------------------------------------------------------- resolution
2377 : : // (cl @p4 (not (not @p5)))
2378 : : //
2379 : : // Then we combine the proofs PI_0, the premise for "notEq", and
2380 : : // PI_1 and PI_2:
2381 : : //
2382 : : // --------- notEq
2383 : : // PI_0 (not (= x c)) PI_1 PI_2
2384 : : // ------------------------------------- resolution
2385 : : // (> x c)
2386 : : //
2387 : : // where (= x c) is the expected result
2388 : :
2389 : : // We first build PI_0:
2390 : : Node laDiseqOr = nm->mkNode(
2391 : : Kind::SEXPR,
2392 : 210 : d_cl,
2393 : 840 : nm->mkNode(
2394 : 1260 : Kind::OR, notEq[0], leq.notNode(), leqInverted.notNode()));
2395 : : Node laDiseqCl = nm->mkNode(
2396 : : Kind::SEXPR,
2397 : 1470 : {d_cl, notEq[0], leq.notNode(), leqInverted.notNode()});
2398 : 210 : success &=
2399 [ + - ][ + - ]: 210 : addAletheStep(AletheRule::LA_DISEQUALITY,
[ + - ][ - - ]
[ - - ][ - - ]
[ - - ]
2400 : : laDiseqOr,
2401 : : laDiseqOr,
2402 : : {},
2403 : : {},
2404 : : *cdp)
2405 : 630 : && addAletheStep(
2406 [ + - ]: 420 : AletheRule::OR, laDiseqCl, laDiseqCl, {laDiseqOr}, {}, *cdp);
2407 : : // Now we build PI_1:
2408 : 420 : Node compSimp = geq.eqNode(leqInverted);
2409 : 630 : Node compSimpCl = nm->mkNode(Kind::SEXPR, d_cl, compSimp);
2410 : 420 : success &= addAletheStep(
2411 : 210 : AletheRule::COMP_SIMPLIFY, compSimpCl, compSimpCl, {}, {}, *cdp);
2412 : : Node equivPos2Cl = nm->mkNode(
2413 : : Kind::SEXPR,
2414 : 1470 : {d_cl, compSimp.notNode(), geq.notNode(), leqInverted});
2415 : 420 : success &= addAletheStep(
2416 : 210 : AletheRule::EQUIV_POS2, equivPos2Cl, equivPos2Cl, {}, {}, *cdp);
2417 : 630 : Node resPi1Conc = nm->mkNode(Kind::SEXPR, d_cl, leqInverted);
2418 [ + + ][ - - ]: 1050 : success &= addAletheStep(
2419 : : AletheRule::RESOLUTION,
2420 : : resPi1Conc,
2421 : : resPi1Conc,
2422 : : {compSimpCl, equivPos2Cl, geq},
2423 : 420 : d_resPivots ? std::vector<Node>{compSimp, d_true, geq, d_false}
2424 : : : std::vector<Node>(),
2425 : 840 : *cdp);
2426 : : // Now we build PI_2
2427 : 420 : Node compSimp2 = res.eqNode(leq.notNode());
2428 : 630 : Node compSimp2Cl = nm->mkNode(Kind::SEXPR, d_cl, compSimp2);
2429 : 420 : success &= addAletheStep(AletheRule::COMP_SIMPLIFY,
2430 : : compSimp2Cl,
2431 : : compSimp2Cl,
2432 : : {},
2433 : : {},
2434 : 210 : *cdp);
2435 : : Node equivPos1Cl = nm->mkNode(
2436 : : Kind::SEXPR,
2437 : 1470 : {d_cl, compSimp2.notNode(), res, leq.notNode().notNode()});
2438 : 420 : success &= addAletheStep(
2439 : 210 : AletheRule::EQUIV_POS1, equivPos1Cl, equivPos1Cl, {}, {}, *cdp);
2440 : : Node resPi2Conc =
2441 : 630 : nm->mkNode(Kind::SEXPR, d_cl, res, leq.notNode().notNode());
2442 : 210 : success &=
2443 [ + + ][ - - ]: 840 : addAletheStep(AletheRule::RESOLUTION,
2444 : : resPi2Conc,
2445 : : resPi2Conc,
2446 : : {compSimp2Cl, equivPos1Cl},
2447 : 420 : d_resPivots ? std::vector<Node>{compSimp2, d_true}
2448 : : : std::vector<Node>(),
2449 : 630 : *cdp);
2450 : : // Now we build the final resolution
2451 : 210 : success &=
2452 [ + + ][ - - ]: 1470 : addAletheStep(AletheRule::RESOLUTION,
2453 : : res,
2454 : 420 : nm->mkNode(Kind::SEXPR, d_cl, res),
2455 : : {notEq, laDiseqCl, resPi1Conc, resPi2Conc},
2456 : 420 : d_resPivots ? std::vector<Node>{notEq[0],
2457 : 0 : d_false,
2458 : : leqInverted,
2459 : 0 : d_false,
2460 : : leq.notNode(),
2461 : 0 : d_true}
2462 : : : std::vector<Node>(),
2463 : 1050 : *cdp);
2464 : 210 : break;
2465 : : }
2466 : 96 : case Kind::LT:
2467 : : {
2468 [ + - ]: 96 : Trace("alethe-proof") << "..case LT\n";
2469 : 192 : Node leq, notEq;
2470 : 96 : Kind kc0 = children[0].getKind();
2471 : 96 : if (kc0 == Kind::LEQ
2472 [ + + ][ + - ]: 96 : || (kc0 == Kind::NOT && children[0][0].getKind() == Kind::LT))
[ - + ][ + + ]
[ + + ][ - - ]
2473 : : {
2474 : 39 : leq = children[0];
2475 : 39 : notEq = children[1];
2476 : : }
2477 : : else
2478 : : {
2479 : 57 : leq = children[1];
2480 : 57 : notEq = children[0];
2481 : : }
2482 : 192 : Assert(notEq.getKind() == Kind::NOT
2483 : : && notEq[0].getKind() == Kind::EQUAL);
2484 [ - + ][ - + ]: 96 : Assert(leq.getKind() == Kind::LEQ);
[ - - ]
2485 : 288 : Node leqInverted = nm->mkNode(Kind::LEQ, c, x);
2486 : : // The subproof built here uses the PI_0 defined in the case
2487 : : // above. Note that @p7 is res and @p8 is leqInverted.
2488 : : //
2489 : : // PI_3:
2490 : : // with @p6: (= (< x c) (not (<= c x)))
2491 : : // with @p7: (< x c)
2492 : : // with @p8: (<= c x)
2493 : : //
2494 : : // ----- comp_simplify ----------------------------------- equiv_pos1
2495 : : // @p6 (cl (not @p6) @p7 (not (not @p8)))
2496 : : // -------------------------------------------------------- resolution
2497 : : // (cl @p7 (not (not @p8)))
2498 : : //
2499 : : // Then we combine the proofs PI_0, the premise for "notEq", the
2500 : : // premise for "leq", and PI_3 above:
2501 : : //
2502 : : // ------- notEq -----leq ---------------------------- PI_3
2503 : : // PI_0 (not (= x c)) (<= x c) (cl (< x c) (not (not (<= c x))))
2504 : : // -------------------------------------------------------- resolution
2505 : : // (< x c)
2506 : : //
2507 : : // where (< x c) is the expected result
2508 : :
2509 : : // We first build PI_0:
2510 : : Node laDiseqOr = nm->mkNode(
2511 : : Kind::SEXPR,
2512 : 96 : d_cl,
2513 : 384 : nm->mkNode(
2514 : 576 : Kind::OR, notEq[0], leq.notNode(), leqInverted.notNode()));
2515 : : Node laDiseqCl = nm->mkNode(
2516 : : Kind::SEXPR,
2517 : 672 : {d_cl, notEq[0], leq.notNode(), leqInverted.notNode()});
2518 : 96 : success &=
2519 [ + - ][ + - ]: 96 : addAletheStep(AletheRule::LA_DISEQUALITY,
[ + - ][ - - ]
[ - - ][ - - ]
[ - - ]
2520 : : laDiseqOr,
2521 : : laDiseqOr,
2522 : : {},
2523 : : {},
2524 : : *cdp)
2525 : 288 : && addAletheStep(
2526 [ + - ]: 192 : AletheRule::OR, laDiseqCl, laDiseqCl, {laDiseqOr}, {}, *cdp);
2527 : : // Now we build PI_3:
2528 : 192 : Node compSimp = res.eqNode(leqInverted.notNode());
2529 : 288 : Node compSimpCl = nm->mkNode(Kind::SEXPR, d_cl, compSimp);
2530 : 192 : success &= addAletheStep(
2531 : 96 : AletheRule::COMP_SIMPLIFY, compSimpCl, compSimpCl, {}, {}, *cdp);
2532 : : Node equivPos1Cl = nm->mkNode(
2533 : : Kind::SEXPR,
2534 : 672 : {d_cl, compSimp.notNode(), res, leqInverted.notNode().notNode()});
2535 : 192 : success &= addAletheStep(
2536 : 96 : AletheRule::EQUIV_POS1, equivPos1Cl, equivPos1Cl, {}, {}, *cdp);
2537 : : // We do a single resolution step , inlining the one finishing PI_3
2538 : : // above, to build the final resolution
2539 [ + + ][ - - ]: 768 : success &= addAletheStep(
2540 : : AletheRule::RESOLUTION,
2541 : : res,
2542 : 192 : nm->mkNode(Kind::SEXPR, d_cl, res),
2543 : : {laDiseqCl, notEq, leq, equivPos1Cl, compSimpCl},
2544 : 192 : d_resPivots ? std::vector<Node>{notEq[0],
2545 : 0 : d_true,
2546 : : leq,
2547 : 0 : d_false,
2548 : : leqInverted.notNode(),
2549 : 0 : d_true,
2550 : : compSimp,
2551 : 0 : d_false}
2552 : : : std::vector<Node>(),
2553 : 576 : *cdp);
2554 : 96 : break;
2555 : : }
2556 : 0 : default:
2557 : : {
2558 : 0 : Unreachable() << "should not have gotten here";
2559 : : }
2560 : : }
2561 : 874 : return success;
2562 : : }
2563 : 120141 : default:
2564 : : {
2565 [ + - ]: 240282 : Trace("alethe-proof")
2566 : 0 : << "... rule not translated yet " << id << " / " << res << " "
2567 : 120141 : << children << " " << args << std::endl;
2568 : 240282 : std::stringstream ss;
2569 : 120141 : ss << "\"" << id << "\"";
2570 : : std::vector<Node> newArgs{
2571 : 480564 : NodeManager::mkRawSymbol(ss.str(), nm->sExprType())};
2572 : 120141 : newArgs.insert(newArgs.end(), args.begin(), args.end());
2573 : 240282 : return addAletheStep(AletheRule::HOLE,
2574 : : res,
2575 : 240282 : nm->mkNode(Kind::SEXPR, d_cl, res),
2576 : : children,
2577 : : newArgs,
2578 : 120141 : *cdp);
2579 : : }
2580 : : }
2581 : : Trace("alethe-proof") << "... error translating rule " << id << " / " << res
2582 : : << " " << children << " " << args << std::endl;
2583 : : return false;
2584 : : }
2585 : :
2586 : 14893 : bool AletheProofPostprocessCallback::maybeReplacePremiseProof(Node premise,
2587 : : CDProof* cdp)
2588 : : {
2589 : : // Test if the proof of premise concludes a non-singleton clause. Assumptions
2590 : : // always succeed the test.
2591 : 29786 : std::shared_ptr<ProofNode> premisePf = cdp->getProofFor(premise);
2592 [ + + ]: 14893 : if (premisePf->getRule() == ProofRule::ASSUME)
2593 : : {
2594 : 332 : return false;
2595 : : }
2596 : 29122 : Node premisePfConclusion = premisePf->getArguments()[2];
2597 : : // not a proof of a non-singleton clause
2598 : 43683 : if (premisePfConclusion.getNumChildren() <= 2
2599 [ + + ][ - + ]: 14561 : || premisePfConclusion[0] != d_cl)
[ + + ][ + + ]
[ - - ]
2600 : : {
2601 : 3657 : return false;
2602 : : }
2603 : : // If this resolution child is used as a singleton OR but the rule
2604 : : // justifying it concludes a clause, then we are often in this scenario:
2605 : : //
2606 : : // (or t1 ... tn)
2607 : : // -------------- OR
2608 : : // (cl t1 ... tn)
2609 : : // ---------------- FACTORING/REORDERING
2610 : : // (cl t1' ... tn')
2611 : : //
2612 : : // where what is used in the resolution is actually (or t1' ... tn').
2613 : : //
2614 : : // This happens when (or t1' ... tn') has been added to the SAT solver as
2615 : : // a literal as well, and its node clashed with the conclusion of the
2616 : : // FACTORING/REORDERING step.
2617 : : //
2618 : : // When this is happening at one level, as in the example above, a solution is
2619 : : // to *not* use FACTORING/REORDERING (which in Alethe operate on clauses) but
2620 : : // generate a proof to obtain the expected node (or t1' ... tn') from the
2621 : : // original node (or t1 ... tn).
2622 : : //
2623 : : // If the change is due to FACTORING, this can be easily obtained via
2624 : : // rewriting (with OR_SIMPLIFY), equivalence elimination, and resolution.
2625 : : //
2626 : : // Otherise we are either in the case of REORDERING or in a case where we
2627 : : // cannot easily access a proof of (or t1 ... tn). In both case we will derive
2628 : : // (cl (or t1' ... tn')) using n or_neg steps, as shown below.
2629 : 10904 : NodeManager* nm = nodeManager();
2630 [ + - ]: 10904 : Trace("alethe-proof") << "\n";
2631 : 10904 : AletheRule premiseProofRule = getAletheRule(premisePf->getArguments()[0]);
2632 : 10904 : if (premiseProofRule == AletheRule::CONTRACTION
2633 [ + + ][ - + ]: 10904 : && getAletheRule(premisePf->getChildren()[0]->getArguments()[0])
[ + + ][ - + ]
[ - - ]
2634 : : == AletheRule::OR)
2635 : : {
2636 : : // get great grand child
2637 : : std::shared_ptr<ProofNode> premiseChildPf =
2638 : 0 : premisePf->getChildren()[0]->getChildren()[0];
2639 : 0 : Node premiseChildConclusion = premiseChildPf->getResult();
2640 : : // Note that we need to add this proof node explicitly to cdp because it
2641 : : // does not have a step for premiseChildConclusion. Rather it is only
2642 : : // present in cdp as a descendant of premisePf (which is in cdp), so if
2643 : : // premisePf is to be lost, then so will premiseChildPf. By adding
2644 : : // premiseChildPf explicitly, it can be retrieved to justify
2645 : : // premiseChildConclusion when requested.
2646 : 0 : cdp->addProof(premiseChildPf);
2647 : : // equate it to what we expect. If the premise rule is CONTRACTION, we can
2648 : : // justify it via OR_SIMPLIFY. Otherwise...
2649 : 0 : Node equiv = premiseChildConclusion.eqNode(premise);
2650 : 0 : bool success = true;
2651 [ - - ]: 0 : if (premiseProofRule == AletheRule::CONTRACTION)
2652 : : {
2653 : 0 : success &= addAletheStep(AletheRule::OR_SIMPLIFY,
2654 : : equiv,
2655 : 0 : nm->mkNode(Kind::SEXPR, d_cl, equiv),
2656 : : {},
2657 : : {},
2658 : 0 : *cdp);
2659 : : Node equivElim = nm->mkNode(
2660 : : Kind::SEXPR,
2661 : 0 : {d_cl, equiv.notNode(), premiseChildConclusion.notNode(), premise});
2662 : 0 : success &= addAletheStep(
2663 : 0 : AletheRule::EQUIV_POS2, equivElim, equivElim, {}, {}, *cdp);
2664 : 0 : Node newPremise = nm->mkNode(Kind::SEXPR, d_cl, premise);
2665 [ - - ]: 0 : Trace("alethe-proof")
2666 : 0 : << "Reverted handling as a clause for converting "
2667 : 0 : << premiseChildConclusion << " into " << premise << std::endl;
2668 : : return success
2669 : 0 : && addAletheStep(AletheRule::RESOLUTION,
2670 : : newPremise,
2671 : : newPremise,
2672 : : {equivElim, equiv, premiseChildConclusion},
2673 : 0 : d_resPivots
2674 : 0 : ? std::vector<Node>{equiv,
2675 : 0 : d_false,
2676 : : premiseChildConclusion,
2677 : 0 : d_false}
2678 : : : std::vector<Node>(),
2679 [ - - ]: 0 : *cdp);
2680 : : }
2681 : : }
2682 : : // Derive (cl (or t1' ... tn')) from (cl t1' ... tn') (i.e., the premise) with
2683 : : //
2684 : : // ----------------------- ... --------------------- or_neg
2685 : : // premise (cl premise, (not t1')) ... (cl premise, (not tn'))
2686 : : // ---------------------------- resolution
2687 : : // (cl premise ... premise)
2688 : : // ---------------------------- contraction
2689 : : // (cl premise)
2690 : 43616 : std::vector<Node> resPremises{premise};
2691 : 21808 : std::vector<Node> resArgs;
2692 : 43616 : std::vector<Node> contractionPremiseChildren{d_cl};
2693 : 10904 : bool success = true;
2694 : :
2695 [ + + ]: 71327 : for (size_t i = 0, size = premise.getNumChildren(); i < size; ++i)
2696 : : {
2697 : 120846 : Node nNeg = premise[i].notNode();
2698 : 60423 : resPremises.push_back(nm->mkNode(Kind::SEXPR, d_cl, premise, nNeg));
2699 : 241692 : success &= addAletheStep(AletheRule::OR_NEG,
2700 : 60423 : resPremises.back(),
2701 : 60423 : resPremises.back(),
2702 : : {},
2703 : 181269 : std::vector<Node>{nm->mkConstInt(i)},
2704 : 60423 : *cdp);
2705 : 60423 : resArgs.push_back(nNeg[0]);
2706 : 60423 : resArgs.push_back(d_true);
2707 : 60423 : contractionPremiseChildren.push_back(premise);
2708 : : }
2709 : 21808 : Node contractionPremise = nm->mkNode(Kind::SEXPR, contractionPremiseChildren);
2710 : 21808 : success &= addAletheStep(AletheRule::RESOLUTION,
2711 : : contractionPremise,
2712 : : contractionPremise,
2713 : : resPremises,
2714 [ + + ]: 21808 : d_resPivots ? resArgs : std::vector<Node>(),
2715 : 10904 : *cdp);
2716 : 21808 : Node newPremise = nm->mkNode(Kind::SEXPR, d_cl, premise);
2717 : : return success
2718 : 32712 : && addAletheStep(AletheRule::CONTRACTION,
2719 : : newPremise,
2720 : : newPremise,
2721 : : {contractionPremise},
2722 : : {},
2723 [ + - ]: 21808 : *cdp);
2724 : : }
2725 : :
2726 : 268962 : bool AletheProofPostprocessCallback::updatePost(
2727 : : Node res,
2728 : : CVC5_UNUSED ProofRule id,
2729 : : const std::vector<Node>& children,
2730 : : const std::vector<Node>& args,
2731 : : CDProof* cdp)
2732 : : {
2733 : 268962 : NodeManager* nm = nodeManager();
2734 : 268962 : AletheRule rule = getAletheRule(args[0]);
2735 [ + - ]: 537924 : Trace("alethe-proof") << "...Alethe post-update " << rule << " / " << res
2736 : 268962 : << " / args: " << args << std::endl;
2737 : 268962 : bool success = true;
2738 [ + + ][ - ]: 268962 : switch (rule)
2739 : : {
2740 : : // In the case of a resolution rule, the rule might originally have been a
2741 : : // cvc5 RESOLUTION or CHAIN_RESOLUTION rule, and it is possible that one of
2742 : : // the children was printed as (cl (or F1 ... Fn)) but it was actually used
2743 : : // as (cl F1 ... Fn). However, from the pivot of the resolution step for the
2744 : : // child we can determine if an additional OR step is necessary to convert
2745 : : // the clase (cl (or ...)) to (cl ...). This is done below.
2746 : 112860 : case AletheRule::RESOLUTION_OR:
2747 : : {
2748 : : // We need pivots to more easily do the computations here, so we require
2749 : : // them.
2750 [ - + ][ - + ]: 112860 : Assert(args.size() >= 4);
[ - - ]
2751 : 112860 : std::vector<Node> newChildren = children;
2752 : 112860 : bool hasUpdated = false;
2753 : :
2754 : : // Note that we will have inverted the order of polarity/pivot.
2755 : : size_t polIdx, pivIdx;
2756 : : // their starting positions in the arguments
2757 : 112860 : polIdx = 4;
2758 : 112860 : pivIdx = 3;
2759 : : // The first child is used as a non-singleton clause if it is not equal
2760 : : // to its pivot L_1. Since it's the first clause in the resolution it can
2761 : : // only be equal to the pivot in the case the polarity is true.
2762 : 112860 : if (children[0].getKind() == Kind::OR
2763 [ + + ][ + + ]: 112860 : && (args[polIdx] != d_true || args[pivIdx] != children[0]))
[ + - ][ + + ]
2764 : : {
2765 : 118582 : std::shared_ptr<ProofNode> childPf = cdp->getProofFor(children[0]);
2766 : 59291 : bool childPfIsAssume = childPf->getRule() == ProofRule::ASSUME;
2767 : : Node childConclusion =
2768 [ + + ]: 118582 : childPfIsAssume ? childPf->getResult() : childPf->getArguments()[2];
2769 : : // if child conclusion is of the form (sexpr cl (or ...)), then we need
2770 : : // to add an OR step, since this child must not be a singleton
2771 [ - + ]: 13284 : if ((childPfIsAssume && childConclusion.getKind() == Kind::OR)
2772 [ + + ][ + + ]: 74854 : || (childConclusion.getNumChildren() == 2
2773 [ + - ][ + + ]: 61570 : && childConclusion[0] == d_cl
[ - - ]
2774 [ + - ][ + + ]: 61570 : && childConclusion[1].getKind() == Kind::OR))
[ + + ][ - - ]
2775 : : {
2776 : 15563 : hasUpdated = true;
2777 : : // Add or step
2778 : 62252 : std::vector<Node> subterms{d_cl};
2779 [ + + ]: 15563 : if (childPfIsAssume)
2780 : : {
2781 : : subterms.insert(
2782 : 13284 : subterms.end(), childConclusion.begin(), childConclusion.end());
2783 : : }
2784 : : else
2785 : : {
2786 : 2279 : subterms.insert(subterms.end(),
2787 : : childConclusion[1].begin(),
2788 : 4558 : childConclusion[1].end());
2789 : : }
2790 : 15563 : Node newConclusion = nm->mkNode(Kind::SEXPR, subterms);
2791 : 62252 : success &= addAletheStep(AletheRule::OR,
2792 : : newConclusion,
2793 : : newConclusion,
2794 : 15563 : {children[0]},
2795 : : {},
2796 : 31126 : *cdp);
2797 : 15563 : newChildren[0] = newConclusion;
2798 [ + - ]: 31126 : Trace("alethe-proof") << "Added OR step for " << childConclusion
2799 : 15563 : << " / " << newConclusion << std::endl;
2800 : : }
2801 : : }
2802 : : // The premise is used a singleton clause. We must guarantee that its
2803 : : // proof indeed concludes a singleton clause.
2804 [ - + ]: 53569 : else if (children[0].getKind() == Kind::OR)
2805 : : {
2806 : 0 : Assert(args[polIdx] == d_true && args[pivIdx] == children[0]);
2807 [ - - ]: 0 : if (maybeReplacePremiseProof(children[0], cdp))
2808 : : {
2809 : 0 : hasUpdated = true;
2810 : 0 : newChildren[0] = nm->mkNode(Kind::SEXPR, d_cl, children[0]);
2811 : : }
2812 : : }
2813 : : // For all other children C_i the procedure is similar. There is however a
2814 : : // key difference in the choice of the pivot element which is now the
2815 : : // L_{i-1}, i.e. the pivot of the child with the result of the i-1
2816 : : // resolution steps between the children before it. Therefore, if the
2817 : : // policy id_{i-1} is true, the pivot has to appear negated in the child
2818 : : // in which case it should not be a (cl (or F1 ... Fn)) node. The same is
2819 : : // true if it isn't the pivot element.
2820 [ + + ]: 1865010 : for (std::size_t i = 1, size = children.size(); i < size; ++i)
2821 : : {
2822 : 1752150 : polIdx = 2 * (i - 1) + 3 + 1;
2823 : 1752150 : pivIdx = 2 * (i - 1) + 3;
2824 : 1752150 : if (children[i].getKind() == Kind::OR
2825 [ + + ][ + + ]: 4039840 : && (args[polIdx] != d_false
2826 : 2287700 : || d_anc.convert(args[pivIdx]) != d_anc.convert(children[i])))
2827 : : {
2828 : 1484180 : if (args[polIdx] == d_false
2829 : 2968370 : && d_anc.convert(args[pivIdx]) == d_anc.convert(children[i]))
2830 : : {
2831 : 0 : continue;
2832 : : }
2833 : 2968370 : std::shared_ptr<ProofNode> childPf = cdp->getProofFor(children[i]);
2834 : 1484180 : bool childPfIsAssume = childPf->getRule() == ProofRule::ASSUME;
2835 : : Node childConclusion = childPfIsAssume ? childPf->getResult()
2836 [ + + ]: 2968370 : : childPf->getArguments()[2];
2837 : : // Add or step
2838 [ - + ]: 166654 : if ((childPfIsAssume && childConclusion.getKind() == Kind::OR)
2839 [ + + ][ + + ]: 1709600 : || (childConclusion.getNumChildren() == 2
2840 [ + - ][ + + ]: 1542950 : && childConclusion[0] == d_cl
[ - - ]
2841 [ + - ][ + + ]: 1542950 : && childConclusion[1].getKind() == Kind::OR))
[ + + ][ - - ]
2842 : : {
2843 : 225420 : hasUpdated = true;
2844 : 901680 : std::vector<Node> lits{d_cl};
2845 [ + + ]: 225420 : if (childPfIsAssume)
2846 : : {
2847 : : lits.insert(
2848 : 166654 : lits.end(), childConclusion.begin(), childConclusion.end());
2849 : : }
2850 : : else
2851 : : {
2852 : 58766 : lits.insert(lits.end(),
2853 : : childConclusion[1].begin(),
2854 : 117532 : childConclusion[1].end());
2855 : : }
2856 : 225420 : Node conclusion = nm->mkNode(Kind::SEXPR, lits);
2857 : 901680 : success &= addAletheStep(AletheRule::OR,
2858 : : conclusion,
2859 : : conclusion,
2860 : 225420 : {children[i]},
2861 : : {},
2862 : 450840 : *cdp);
2863 : 225420 : newChildren[i] = conclusion;
2864 [ + - ]: 450840 : Trace("alethe-proof") << "Added OR step for " << childConclusion
2865 : 225420 : << " / " << conclusion << std::endl;
2866 : : }
2867 : : }
2868 : : // As for the first premise, we need to handle the case in which the
2869 : : // premise is a singleton but the rule concluding it yields a clause.
2870 [ + + ]: 267965 : else if (children[i].getKind() == Kind::OR)
2871 : : {
2872 : 29786 : Assert(args[polIdx] == d_false
2873 : : && d_anc.convert(args[pivIdx]) == d_anc.convert(children[i]));
2874 [ + + ]: 14893 : if (maybeReplacePremiseProof(children[i], cdp))
2875 : : {
2876 : 10904 : hasUpdated = true;
2877 : 10904 : newChildren[i] = nm->mkNode(Kind::SEXPR, d_cl, children[i]);
2878 : : }
2879 : : }
2880 : : }
2881 [ - + ]: 112860 : if (TraceIsOn("alethe-proof"))
2882 : : {
2883 [ - - ]: 0 : if (hasUpdated)
2884 : : {
2885 [ - - ]: 0 : Trace("alethe-proof")
2886 : 0 : << "... update alethe step in finalizer " << res << " "
2887 : 0 : << newChildren << " / " << args << std::endl;
2888 : : }
2889 : : else
2890 : : {
2891 [ - - ]: 0 : Trace("alethe-proof") << "... no update\n";
2892 : : }
2893 : : }
2894 : 225720 : success &= addAletheStep(
2895 : : AletheRule::RESOLUTION,
2896 : : res,
2897 : 112860 : args[2],
2898 : : newChildren,
2899 [ + + ][ + + ]: 225720 : d_resPivots ? std::vector<Node>{args.begin() + 3, args.end()}
[ - - ]
2900 : : : std::vector<Node>{},
2901 : 112860 : *cdp);
2902 : 112860 : return success;
2903 : : }
2904 : : // A application of the FACTORING rule:
2905 : : //
2906 : : // (or a a b)
2907 : : // ---------- FACTORING
2908 : : // (or a b)
2909 : : //
2910 : : // might be translated during pre-visit (update) to:
2911 : : //
2912 : : // (or (cl a a b))*
2913 : : // ---------------- CONTRACTION
2914 : : // (cl a b)**
2915 : : //
2916 : : // In this post-visit an additional OR step is added in that case:
2917 : : //
2918 : : // (cl (or a a b))*
2919 : : // ---------------- OR
2920 : : // (cl a a b)
2921 : : // ---------------- CONTRACTION
2922 : : // (cl a b)**
2923 : : //
2924 : : // * the corresponding proof node is (or a a b)
2925 : : // ** the corresponding proof node is (or a b)
2926 : : //
2927 : : // The process is analogous for REORDERING.
2928 : 156102 : case AletheRule::REORDERING:
2929 : : case AletheRule::CONTRACTION:
2930 : : {
2931 : 312204 : std::shared_ptr<ProofNode> childPf = cdp->getProofFor(children[0]);
2932 : 156102 : bool childPfIsAssume = childPf->getRule() == ProofRule::ASSUME;
2933 : : Node childConclusion =
2934 [ + + ]: 312204 : childPfIsAssume ? childPf->getResult() : childPf->getArguments()[2];
2935 [ - + ]: 2 : if ((childPfIsAssume && childConclusion.getKind() == Kind::OR)
2936 [ + + ][ + + ]: 165869 : || (childConclusion.getNumChildren() == 2
2937 [ + - ][ + + ]: 165867 : && childConclusion[0] == d_cl
[ - - ]
2938 [ + - ][ + + ]: 165867 : && childConclusion[1].getKind() == Kind::OR))
[ + + ][ - - ]
2939 : : {
2940 : : // Add or step for child
2941 : 39068 : std::vector<Node> subterms{d_cl};
2942 [ + + ]: 9767 : if (childPfIsAssume)
2943 : : {
2944 : : subterms.insert(
2945 : 2 : subterms.end(), childConclusion.begin(), childConclusion.end());
2946 : : }
2947 : : else
2948 : : {
2949 : 9765 : subterms.insert(subterms.end(),
2950 : : childConclusion[1].begin(),
2951 : 19530 : childConclusion[1].end());
2952 : : }
2953 : 9767 : Node newChild = nm->mkNode(Kind::SEXPR, subterms);
2954 : 39068 : success &= addAletheStep(
2955 : 29301 : AletheRule::OR, newChild, newChild, {children[0]}, {}, *cdp);
2956 [ + - ]: 19534 : Trace("alethe-proof")
2957 : 0 : << "Added OR step in finalizer to child " << childConclusion
2958 : 9767 : << " / " << newChild << std::endl;
2959 : : // update res step
2960 : 19534 : cdp->addStep(res, ProofRule::ALETHE_RULE, {newChild}, args);
2961 : 9767 : return success;
2962 : : }
2963 [ + - ]: 146335 : Trace("alethe-proof") << "... no update\n";
2964 : 146335 : return false;
2965 : : }
2966 : 0 : default:
2967 : : {
2968 [ - - ]: 0 : Trace("alethe-proof") << "... no update\n";
2969 : 0 : return false;
2970 : : }
2971 : : }
2972 : : Trace("alethe-proof") << "... no update\n";
2973 : : return false;
2974 : : }
2975 : :
2976 : 2043 : bool AletheProofPostprocessCallback::ensureFinalStep(
2977 : : Node res,
2978 : : CVC5_UNUSED ProofRule id,
2979 : : std::vector<Node>& children,
2980 : : const std::vector<Node>& args,
2981 : : CDProof* cdp)
2982 : : {
2983 : 2043 : bool success = true;
2984 : 2043 : NodeManager* nm = nodeManager();
2985 : 4086 : std::shared_ptr<ProofNode> childPf = cdp->getProofFor(children[0]);
2986 : :
2987 : : // convert inner proof, i.e., children[0], if its conclusion is (cl false) or
2988 : : // if it's a false assumption
2989 : : //
2990 : : // ...
2991 : : // ------------------- ---------------------- false
2992 : : // (cl false) (cl (not false))
2993 : : // -------------------------------------------------- resolution
2994 : : // (cl)
2995 : 2043 : if ((childPf->getRule() == ProofRule::ALETHE_RULE
2996 [ + + ]: 1552 : && childPf->getArguments()[2].getNumChildren() == 2
2997 [ - + ][ + + ]: 2491 : && childPf->getArguments()[2][1] == d_false)
[ - - ]
2998 [ + + ][ + + ]: 5651 : || (childPf->getRule() == ProofRule::ASSUME
2999 [ + - ][ + + ]: 2056 : && childPf->getResult() == d_false))
[ + + ][ - - ]
3000 : : {
3001 : : Node notFalse =
3002 : 1383 : nm->mkNode(Kind::SEXPR, d_cl, d_false.notNode()); // (cl (not false))
3003 : 922 : Node newChild = nm->mkNode(Kind::SEXPR, d_cl); // (cl)
3004 : :
3005 : 461 : success &=
3006 : 461 : addAletheStep(AletheRule::FALSE, notFalse, notFalse, {}, {}, *cdp);
3007 [ + + ][ - - ]: 1844 : success &= addAletheStep(
3008 : : AletheRule::RESOLUTION,
3009 : : newChild,
3010 : : newChild,
3011 : 461 : {children[0], notFalse},
3012 : 922 : d_resPivots ? std::vector<Node>{d_false, d_true} : std::vector<Node>(),
3013 : 1383 : *cdp);
3014 : 461 : children[0] = newChild;
3015 : : }
3016 : :
3017 : : // Sanitize original assumptions and create a double scope to hold them, where
3018 : : // the first scope is empty. This is needed because of the expected form a
3019 : : // proof node to be printed.
3020 : 4086 : std::vector<Node> sanitizedArgs;
3021 [ + + ]: 14593 : for (const Node& a : args)
3022 : : {
3023 : 12900 : Node conv = d_anc.maybeConvert(a, true);
3024 [ + + ]: 12900 : if (conv.isNull())
3025 : : {
3026 : 350 : d_reasonForConversionFailure = d_anc.getError();
3027 : 350 : success = false;
3028 : 350 : break;
3029 : : }
3030 : : // avoid repeated assumptions
3031 : 12550 : if (std::find(sanitizedArgs.begin(), sanitizedArgs.end(), conv)
3032 [ + + ]: 25100 : == sanitizedArgs.end())
3033 : : {
3034 : 12314 : sanitizedArgs.push_back(conv);
3035 : : }
3036 : : }
3037 : 2043 : Node placeHolder = nm->mkNode(Kind::SEXPR, res);
3038 : 2043 : cdp->addStep(placeHolder, ProofRule::SCOPE, children, sanitizedArgs);
3039 : 5779 : return success && cdp->addStep(res, ProofRule::SCOPE, {placeHolder}, {});
3040 : : }
3041 : :
3042 : 2070150 : bool AletheProofPostprocessCallback::addAletheStep(
3043 : : AletheRule rule,
3044 : : Node res,
3045 : : Node conclusion,
3046 : : const std::vector<Node>& children,
3047 : : const std::vector<Node>& args,
3048 : : CDProof& cdp)
3049 : : {
3050 : : std::vector<Node> newArgs{
3051 : 10350800 : nodeManager()->mkConstInt(Rational(static_cast<uint32_t>(rule)))};
3052 : 2070150 : newArgs.push_back(res);
3053 : 2070150 : conclusion = d_anc.maybeConvert(conclusion);
3054 [ + + ]: 2070150 : if (conclusion.isNull())
3055 : : {
3056 : 162 : d_reasonForConversionFailure = d_anc.getError();
3057 : 162 : return false;
3058 : : }
3059 : 2069990 : newArgs.push_back(conclusion);
3060 [ + + ]: 6597560 : for (const Node& arg : args)
3061 : : {
3062 : 4528020 : Node conv = d_anc.maybeConvert(arg);
3063 [ + + ]: 4528020 : if (conv.isNull())
3064 : : {
3065 : 443 : d_reasonForConversionFailure = d_anc.getError();
3066 : 443 : return false;
3067 : : }
3068 : 4527580 : newArgs.push_back(conv);
3069 : : }
3070 [ + - ]: 4139090 : Trace("alethe-proof") << "... add alethe step " << res << " / " << conclusion
3071 : 0 : << " " << rule << " " << children << " / " << newArgs
3072 : 2069550 : << std::endl;
3073 : 2069550 : return cdp.addStep(res, ProofRule::ALETHE_RULE, children, newArgs);
3074 : : }
3075 : :
3076 : 131788 : bool AletheProofPostprocessCallback::addAletheStepFromOr(
3077 : : AletheRule rule,
3078 : : Node res,
3079 : : const std::vector<Node>& children,
3080 : : const std::vector<Node>& args,
3081 : : CDProof& cdp)
3082 : : {
3083 [ - + ][ - + ]: 131788 : Assert(res.getKind() == Kind::OR);
[ - - ]
3084 : 527152 : std::vector<Node> subterms = {d_cl};
3085 : 131788 : subterms.insert(subterms.end(), res.begin(), res.end());
3086 : 131788 : Node conclusion = nodeManager()->mkNode(Kind::SEXPR, subterms);
3087 : 263576 : return addAletheStep(rule, res, conclusion, children, args, cdp);
3088 : : }
3089 : :
3090 : 2116 : AletheProofPostprocess::AletheProofPostprocess(Env& env,
3091 : 2116 : AletheNodeConverter& anc)
3092 : 2116 : : EnvObj(env), d_cb(env, anc, options().proof.proofAletheResPivots)
3093 : : {
3094 : 2116 : }
3095 : :
3096 : 2116 : AletheProofPostprocess::~AletheProofPostprocess() {}
3097 : :
3098 : 691 : const std::string& AletheProofPostprocess::getError()
3099 : : {
3100 : 691 : return d_reasonForConversionFailure;
3101 : : }
3102 : :
3103 : 2116 : bool AletheProofPostprocess::process(std::shared_ptr<ProofNode> pf)
3104 : : {
3105 [ + + ]: 2116 : if (logicInfo().isHigherOrder())
3106 : : {
3107 : 73 : std::stringstream ss;
3108 : 73 : ss << "\"Proof unsupported by Alethe: contains higher-order elements\"";
3109 : 73 : d_reasonForConversionFailure = ss.str();
3110 : 73 : return false;
3111 : : }
3112 : : // first two nodes are scopes for definitions and other assumptions. We
3113 : : // process only the internal proof node. And we merge these two scopes
3114 [ + - ][ + - ]: 4086 : Assert(pf->getRule() == ProofRule::SCOPE
[ - + ][ - - ]
3115 : : && pf->getChildren()[0]->getRule() == ProofRule::SCOPE);
3116 : 4086 : std::shared_ptr<ProofNode> definitionsScope = pf;
3117 : 4086 : std::shared_ptr<ProofNode> assumptionsScope = pf->getChildren()[0];
3118 : 4086 : std::shared_ptr<ProofNode> internalProof = assumptionsScope->getChildren()[0];
3119 : : // Translate proof node
3120 : 4086 : ProofNodeUpdater updater(d_env, d_cb, false, false);
3121 : 2043 : updater.process(internalProof);
3122 [ + - ]: 2043 : if (d_reasonForConversionFailure.empty())
3123 : : {
3124 : : // In the Alethe proof format the final step has to be (cl). However, after
3125 : : // the translation, the final step might still be (cl false). In that case
3126 : : // additional steps are required. The function has the additional purpose
3127 : : // of sanitizing the arguments of the outer SCOPEs
3128 : : CDProof cpf(d_env,
3129 : : nullptr,
3130 : : "AletheProofPostProcess::ensureFinalStep::CDProof",
3131 : 6129 : true);
3132 : 8172 : std::vector<Node> ccn{internalProof->getResult()};
3133 : 2043 : cpf.addProof(internalProof);
3134 : 2043 : std::vector<Node> args{definitionsScope->getArguments().begin(),
3135 : 4086 : definitionsScope->getArguments().end()};
3136 : 2043 : args.insert(args.end(),
3137 : 2043 : assumptionsScope->getArguments().begin(),
3138 : 6129 : assumptionsScope->getArguments().end());
3139 : 2043 : if (d_cb.ensureFinalStep(
3140 [ + + ]: 4086 : definitionsScope->getResult(), ProofRule::SCOPE, ccn, args, &cpf))
3141 : : {
3142 : : std::shared_ptr<ProofNode> npn =
3143 : 1693 : cpf.getProofFor(definitionsScope->getResult());
3144 : :
3145 : : // then, update the original proof node based on this one
3146 [ + - ]: 1693 : Trace("pf-process-debug") << "Update node..." << std::endl;
3147 : 1693 : d_env.getProofNodeManager()->updateNode(pf.get(), npn.get());
3148 [ + - ]: 1693 : Trace("pf-process-debug") << "...update node finished." << std::endl;
3149 : : }
3150 : : }
3151 : : // Since the final step may also lead to issues, need to test here again
3152 [ + + ]: 2043 : if (!d_cb.getError().empty())
3153 : : {
3154 : 618 : d_reasonForConversionFailure = d_cb.getError();
3155 : 618 : return false;
3156 : : }
3157 : 1425 : return true;
3158 : : }
3159 : :
3160 : : } // namespace proof
3161 : : } // namespace cvc5::internal
|
