1 /******************************************************************************
2 * Top contributors (to current version):
3 * Andrew Reynolds, Haniel Barbosa, Gereon Kremer
5 * This file is part of the cvc5 project.
7 * Copyright (c) 2009-2021 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 * ****************************************************************************
13 * Proof rule enumeration.
16 #include "cvc4_private.h"
18 #ifndef CVC5__EXPR__PROOF_RULE_H
19 #define CVC5__EXPR__PROOF_RULE_H
26 * An enumeration for proof rules. This enumeration is analogous to Kind for
27 * Node objects. In the documentation below, P:F denotes a ProofNode that
30 * Conceptually, the following proof rules form a calculus whose target
31 * user is the Node-level theory solvers. This means that the rules below
32 * are designed to reason about, among other things, common operations on Node
33 * objects like Rewriter::rewrite or Node::substitute. It is intended to be
34 * translated or printed in other formats.
36 * The following PfRule values include core rules and those categorized by
37 * theory, including the theory of equality.
39 * The "core rules" include two distinguished rules which have special status:
40 * (1) ASSUME, which represents an open leaf in a proof.
41 * (2) SCOPE, which closes the scope of assumptions.
42 * The core rules additionally correspond to generic operations that are done
43 * internally on nodes, e.g. calling Rewriter::rewrite.
45 enum class PfRule
: uint32_t
47 //================================================= Core rules
48 //======================== Assume and Scope
49 // ======== Assumption (a leaf)
55 // This rule has special status, in that an application of assume is an
56 // open leaf in a proof that is not (yet) justified. An assume leaf is
57 // analogous to a free variable in a term, where we say "F is a free
58 // assumption in proof P" if it contains an application of F that is not
59 // bound by SCOPE (see below).
61 // ======== Scope (a binder for assumptions)
63 // Arguments: (F1, ..., Fn)
65 // Conclusion: (=> (and F1 ... Fn) F) or (not (and F1 ... Fn)) if F is false
67 // This rule has a dual purpose with ASSUME. It is a way to close
68 // assumptions in a proof. We require that F1 ... Fn are free assumptions in
69 // P and say that F1, ..., Fn are not free in (SCOPE P). In other words, they
70 // are bound by this application. For example, the proof node:
71 // (SCOPE (ASSUME F) :args F)
72 // has the conclusion (=> F F) and has no free assumptions. More generally, a
73 // proof with no free assumptions always concludes a valid formula.
76 //======================== Builtin theory (common node operations)
77 // ======== Substitution
78 // Children: (P1:F1, ..., Pn:Fn)
79 // Arguments: (t, (ids)?)
80 // ---------------------------------------------------------------
81 // Conclusion: (= t t*sigma{ids}(Fn)*...*sigma{ids}(F1))
82 // where sigma{ids}(Fi) are substitutions, which notice are applied in
84 // Notice that ids is a MethodId identifier, which determines how to convert
85 // the formulas F1, ..., Fn into substitutions.
89 // Arguments: (t, (idr)?)
90 // ----------------------------------------
91 // Conclusion: (= t Rewriter{idr}(t))
92 // where idr is a MethodId identifier, which determines the kind of rewriter
93 // to apply, e.g. Rewriter::rewrite.
98 // ----------------------------------------
99 // Conclusion: (= t Evaluator::evaluate(t))
100 // Note this is equivalent to:
101 // (REWRITE t MethodId::RW_EVALUATE)
103 // ======== Substitution + Rewriting equality introduction
105 // In this rule, we provide a term t and conclude that it is equal to its
106 // rewritten form under a (proven) substitution.
108 // Children: (P1:F1, ..., Pn:Fn)
109 // Arguments: (t, (ids (idr)?)?)
110 // ---------------------------------------------------------------
111 // Conclusion: (= t t')
114 // Rewriter{idr}(t*sigma{ids}(Fn)*...*sigma{ids}(F1))
116 // In other words, from the point of view of Skolem forms, this rule
117 // transforms t to t' by standard substitution + rewriting.
119 // The argument ids and idr is optional and specify the identifier of the
120 // substitution and rewriter respectively to be used. For details, see
121 // theory/builtin/proof_checker.h.
123 // ======== Substitution + Rewriting predicate introduction
125 // In this rule, we provide a formula F and conclude it, under the condition
126 // that it rewrites to true under a proven substitution.
128 // Children: (P1:F1, ..., Pn:Fn)
129 // Arguments: (F, (ids (idr)?)?)
130 // ---------------------------------------------------------------
133 // Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)) == true
134 // where ids and idr are method identifiers.
136 // More generally, this rule also holds when:
137 // Rewriter::rewrite(toOriginal(F')) == true
138 // where F' is the result of the left hand side of the equality above. Here,
139 // notice that we apply rewriting on the original form of F', meaning that
140 // this rule may conclude an F whose Skolem form is justified by the
141 // definition of its (fresh) Skolem variables. For example, this rule may
142 // justify the conclusion (= k t) where k is the purification Skolem for t,
143 // e.g. where the original form of k is t.
145 // Furthermore, notice that the rewriting and substitution is applied only
146 // within the side condition, meaning the rewritten form of the original form
147 // of F does not escape this rule.
149 // ======== Substitution + Rewriting predicate elimination
151 // In this rule, if we have proven a formula F, then we may conclude its
152 // rewritten form under a proven substitution.
154 // Children: (P1:F, P2:F1, ..., P_{n+1}:Fn)
155 // Arguments: ((ids (idr)?)?)
156 // ----------------------------------------
160 // Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)).
161 // where ids and idr are method identifiers.
163 // We rewrite only on the Skolem form of F, similar to MACRO_SR_EQ_INTRO.
165 // ======== Substitution + Rewriting predicate transform
167 // In this rule, if we have proven a formula F, then we may provide a formula
168 // G and conclude it if F and G are equivalent after rewriting under a proven
171 // Children: (P1:F, P2:F1, ..., P_{n+1}:Fn)
172 // Arguments: (G, (ids (idr)?)?)
173 // ----------------------------------------
176 // Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)) ==
177 // Rewriter{idr}(G*sigma{ids}(Fn)*...*sigma{ids}(F1))
179 // More generally, this rule also holds when:
180 // Rewriter::rewrite(toOriginal(F')) == Rewriter::rewrite(toOriginal(G'))
181 // where F' and G' are the result of each side of the equation above. Here,
182 // original forms are used in a similar manner to MACRO_SR_PRED_INTRO above.
183 MACRO_SR_PRED_TRANSFORM
,
185 //================================================= Processing rules
186 // ======== Remove Term Formulas Axiom
189 // ---------------------------------------------------------------
190 // Conclusion: RemoveTermFormulas::getAxiomFor(t).
191 REMOVE_TERM_FORMULA_AXIOM
,
193 //================================================= Trusted rules
194 // ======== Theory lemma
196 // Arguments: (F, tid)
197 // ---------------------------------------------------------------
199 // where F is a (T-valid) theory lemma generated by theory with TheoryId tid.
200 // This is a "coarse-grained" rule that is used as a placeholder if a theory
201 // did not provide a proof for a lemma or conflict.
203 // ======== Theory Rewrite
205 // Arguments: (F, tid, rid)
206 // ----------------------------------------
208 // where F is an equality of the form (= t t') where t' is obtained by
209 // applying the kind of rewriting given by the method identifier rid, which
211 // { RW_REWRITE_THEORY_PRE, RW_REWRITE_THEORY_POST, RW_REWRITE_EQ_EXT }
212 // Notice that the checker for this rule does not replay the rewrite to ensure
213 // correctness, since theory rewriter methods are not static. For example,
214 // the quantifiers rewriter involves constructing new bound variables that are
215 // not guaranteed to be consistent on each call.
217 // The rules in this section have the signature of a "trusted rule":
221 // ---------------------------------------------------------------
224 // where F is an equality of the form t = t' where t was replaced by t'
225 // based on some preprocessing pass, or otherwise F was added as a new
226 // assertion by some preprocessing pass.
228 // where F was added as a new assertion by some preprocessing pass.
230 // where F is an equality of the form t = Theory::ppRewrite(t) for some
231 // theory. Notice this is a "trusted" rule.
233 // where F was added as a new assertion by theory preprocessing.
234 THEORY_PREPROCESS_LEMMA
,
235 // where F is an equality of the form t = t' where t was replaced by t'
236 // based on theory expand definitions.
238 // where F is an existential (exists ((x T)) (P x)) used for introducing
239 // a witness term (witness ((x T)) (P x)).
241 // where F is an equality (= t t') that holds by a form of rewriting that
242 // could not be replayed during proof postprocessing.
244 // where F is an equality (= t t') that holds by a form of substitution that
245 // could not be replayed during proof postprocessing.
247 // where F is an equality (= t t') that holds by a form of substitution that
248 // could not be determined by the TrustSubstitutionMap.
251 //================================================= Boolean rules
252 // ======== Resolution
255 // Arguments: (pol, L)
256 // ---------------------
259 // - C1 and C2 are nodes viewed as clauses, i.e., either an OR node with
260 // each children viewed as a literal or a node viewed as a literal. Note
261 // that an OR node could also be a literal.
262 // - pol is either true or false, representing the polarity of the pivot on
264 // - L is the pivot of the resolution, which occurs as is (resp. under a
265 // NOT) in C1 and negatively (as is) in C2 if pol = true (pol = false).
266 // C is a clause resulting from collecting all the literals in C1, minus the
267 // first occurrence of the pivot or its negation, and C2, minus the first
268 // occurrence of the pivot or its negation, according to the policy above.
269 // If the resulting clause has a single literal, that literal itself is the
270 // result; if it has no literals, then the result is false; otherwise it's
271 // an OR node of the resulting literals.
273 // Note that it may be the case that the pivot does not occur in the
274 // clauses. In this case the rule is not unsound, but it does not correspond
275 // to resolution but rather to a weakening of the clause that did not have a
276 // literal eliminated.
278 // ======== N-ary Resolution
279 // Children: (P1:C_1, ..., Pm:C_n)
280 // Arguments: (pol_1, L_1, ..., pol_{n-1}, L_{n-1})
281 // ---------------------
284 // - let C_1 ... C_n be nodes viewed as clauses, as defined above
285 // - let "C_1 <>_{L,pol} C_2" represent the resolution of C_1 with C_2 with
286 // pivot L and polarity pol, as defined above
287 // - let C_1' = C_1 (from P1),
288 // - for each i > 1, let C_i' = C_{i-1} <>_{L_{i-1}, pol_{i-1}} C_i'
289 // The result of the chain resolution is C = C_n'
291 // ======== Factoring
294 // ---------------------
297 // Set representations of C1 and C2 is the same and the number of literals in
298 // C2 is smaller than that of C1
300 // ======== Reordering
303 // ---------------------
306 // Set representations of C1 and C2 are the same and the number of literals
307 // in C2 is the same of that of C1
309 // ======== N-ary Resolution + Factoring + Reordering
310 // Children: (P1:C_1, ..., Pm:C_n)
311 // Arguments: (C, pol_1, L_1, ..., pol_{n-1}, L_{n-1})
312 // ---------------------
315 // - let C_1 ... C_n be nodes viewed as clauses, as defined in RESOLUTION
316 // - let "C_1 <>_{L,pol} C_2" represent the resolution of C_1 with C_2 with
317 // pivot L and polarity pol, as defined in RESOLUTION
318 // - let C_1' be equal, in its set representation, to C_1 (from P1),
319 // - for each i > 1, let C_i' be equal, it its set representation, to
320 // C_{i-1} <>_{L_{i-1}, pol_{i-1}} C_i'
321 // The result of the chain resolution is C, which is equal, in its set
322 // representation, to C_n'
324 // As above but not checked
325 MACRO_RESOLUTION_TRUST
,
330 // ---------------------
331 // Conclusion: (or F (not F))
333 // ======== Equality resolution
334 // Children: (P1:F1, P2:(= F1 F2))
336 // ---------------------
338 // Note this can optionally be seen as a macro for EQUIV_ELIM1+RESOLUTION.
340 // ======== Modus ponens
341 // Children: (P1:F1, P2:(=> F1 F2))
343 // ---------------------
345 // Note this can optionally be seen as a macro for IMPLIES_ELIM+RESOLUTION.
347 // ======== Double negation elimination
348 // Children: (P:(not (not F)))
350 // ---------------------
353 // ======== Contradiction
354 // Children: (P1:F P2:(not F))
356 // ---------------------
359 // ======== And elimination
360 // Children: (P:(and F1 ... Fn))
362 // ---------------------
365 // ======== And introduction
366 // Children: (P1:F1 ... Pn:Fn))
368 // ---------------------
369 // Conclusion: (and P1 ... Pn)
371 // ======== Not Or elimination
372 // Children: (P:(not (or F1 ... Fn)))
374 // ---------------------
375 // Conclusion: (not Fi)
377 // ======== Implication elimination
378 // Children: (P:(=> F1 F2))
380 // ---------------------
381 // Conclusion: (or (not F1) F2)
383 // ======== Not Implication elimination version 1
384 // Children: (P:(not (=> F1 F2)))
386 // ---------------------
389 // ======== Not Implication elimination version 2
390 // Children: (P:(not (=> F1 F2)))
392 // ---------------------
393 // Conclusion: (not F2)
395 // ======== Equivalence elimination version 1
396 // Children: (P:(= F1 F2))
398 // ---------------------
399 // Conclusion: (or (not F1) F2)
401 // ======== Equivalence elimination version 2
402 // Children: (P:(= F1 F2))
404 // ---------------------
405 // Conclusion: (or F1 (not F2))
407 // ======== Not Equivalence elimination version 1
408 // Children: (P:(not (= F1 F2)))
410 // ---------------------
411 // Conclusion: (or F1 F2)
413 // ======== Not Equivalence elimination version 2
414 // Children: (P:(not (= F1 F2)))
416 // ---------------------
417 // Conclusion: (or (not F1) (not F2))
419 // ======== XOR elimination version 1
420 // Children: (P:(xor F1 F2)))
422 // ---------------------
423 // Conclusion: (or F1 F2)
425 // ======== XOR elimination version 2
426 // Children: (P:(xor F1 F2)))
428 // ---------------------
429 // Conclusion: (or (not F1) (not F2))
431 // ======== Not XOR elimination version 1
432 // Children: (P:(not (xor F1 F2)))
434 // ---------------------
435 // Conclusion: (or F1 (not F2))
437 // ======== Not XOR elimination version 2
438 // Children: (P:(not (xor F1 F2)))
440 // ---------------------
441 // Conclusion: (or (not F1) F2)
443 // ======== ITE elimination version 1
444 // Children: (P:(ite C F1 F2))
446 // ---------------------
447 // Conclusion: (or (not C) F1)
449 // ======== ITE elimination version 2
450 // Children: (P:(ite C F1 F2))
452 // ---------------------
453 // Conclusion: (or C F2)
455 // ======== Not ITE elimination version 1
456 // Children: (P:(not (ite C F1 F2)))
458 // ---------------------
459 // Conclusion: (or (not C) (not F1))
461 // ======== Not ITE elimination version 1
462 // Children: (P:(not (ite C F1 F2)))
464 // ---------------------
465 // Conclusion: (or C (not F2))
468 //================================================= De Morgan rules
470 // Children: (P:(not (and F1 ... Fn))
472 // ---------------------
473 // Conclusion: (or (not F1) ... (not Fn))
475 //================================================= CNF rules
476 // ======== CNF And Pos
478 // Arguments: ((and F1 ... Fn), i)
479 // ---------------------
480 // Conclusion: (or (not (and F1 ... Fn)) Fi)
482 // ======== CNF And Neg
484 // Arguments: ((and F1 ... Fn))
485 // ---------------------
486 // Conclusion: (or (and F1 ... Fn) (not F1) ... (not Fn))
488 // ======== CNF Or Pos
490 // Arguments: ((or F1 ... Fn))
491 // ---------------------
492 // Conclusion: (or (not (or F1 ... Fn)) F1 ... Fn)
494 // ======== CNF Or Neg
496 // Arguments: ((or F1 ... Fn), i)
497 // ---------------------
498 // Conclusion: (or (or F1 ... Fn) (not Fi))
500 // ======== CNF Implies Pos
502 // Arguments: ((implies F1 F2))
503 // ---------------------
504 // Conclusion: (or (not (implies F1 F2)) (not F1) F2)
506 // ======== CNF Implies Neg version 1
508 // Arguments: ((implies F1 F2))
509 // ---------------------
510 // Conclusion: (or (implies F1 F2) F1)
512 // ======== CNF Implies Neg version 2
514 // Arguments: ((implies F1 F2))
515 // ---------------------
516 // Conclusion: (or (implies F1 F2) (not F2))
518 // ======== CNF Equiv Pos version 1
520 // Arguments: ((= F1 F2))
521 // ---------------------
522 // Conclusion: (or (not (= F1 F2)) (not F1) F2)
524 // ======== CNF Equiv Pos version 2
526 // Arguments: ((= F1 F2))
527 // ---------------------
528 // Conclusion: (or (not (= F1 F2)) F1 (not F2))
530 // ======== CNF Equiv Neg version 1
532 // Arguments: ((= F1 F2))
533 // ---------------------
534 // Conclusion: (or (= F1 F2) F1 F2)
536 // ======== CNF Equiv Neg version 2
538 // Arguments: ((= F1 F2))
539 // ---------------------
540 // Conclusion: (or (= F1 F2) (not F1) (not F2))
542 // ======== CNF Xor Pos version 1
544 // Arguments: ((xor F1 F2))
545 // ---------------------
546 // Conclusion: (or (not (xor F1 F2)) F1 F2)
548 // ======== CNF Xor Pos version 2
550 // Arguments: ((xor F1 F2))
551 // ---------------------
552 // Conclusion: (or (not (xor F1 F2)) (not F1) (not F2))
554 // ======== CNF Xor Neg version 1
556 // Arguments: ((xor F1 F2))
557 // ---------------------
558 // Conclusion: (or (xor F1 F2) (not F1) F2)
560 // ======== CNF Xor Neg version 2
562 // Arguments: ((xor F1 F2))
563 // ---------------------
564 // Conclusion: (or (xor F1 F2) F1 (not F2))
566 // ======== CNF ITE Pos version 1
568 // Arguments: ((ite C F1 F2))
569 // ---------------------
570 // Conclusion: (or (not (ite C F1 F2)) (not C) F1)
572 // ======== CNF ITE Pos version 2
574 // Arguments: ((ite C F1 F2))
575 // ---------------------
576 // Conclusion: (or (not (ite C F1 F2)) C F2)
578 // ======== CNF ITE Pos version 3
580 // Arguments: ((ite C F1 F2))
581 // ---------------------
582 // Conclusion: (or (not (ite C F1 F2)) F1 F2)
584 // ======== CNF ITE Neg version 1
586 // Arguments: ((ite C F1 F2))
587 // ---------------------
588 // Conclusion: (or (ite C F1 F2) (not C) (not F1))
590 // ======== CNF ITE Neg version 2
592 // Arguments: ((ite C F1 F2))
593 // ---------------------
594 // Conclusion: (or (ite C F1 F2) C (not F2))
596 // ======== CNF ITE Neg version 3
598 // Arguments: ((ite C F1 F2))
599 // ---------------------
600 // Conclusion: (or (ite C F1 F2) (not F1) (not F2))
603 //================================================= Equality rules
604 // ======== Reflexive
607 // ---------------------
608 // Conclusion: (= t t)
610 // ======== Symmetric
611 // Children: (P:(= t1 t2)) or (P:(not (= t1 t2)))
613 // -----------------------
614 // Conclusion: (= t2 t1) or (not (= t2 t1))
616 // ======== Transitivity
617 // Children: (P1:(= t1 t2), ..., Pn:(= t{n-1} tn))
619 // -----------------------
620 // Conclusion: (= t1 tn)
622 // ======== Congruence
623 // Children: (P1:(= t1 s1), ..., Pn:(= tn sn))
624 // Arguments: (<kind> f?)
625 // ---------------------------------------------
626 // Conclusion: (= (<kind> f? t1 ... tn) (<kind> f? s1 ... sn))
627 // Notice that f must be provided iff <kind> is a parameterized kind, e.g.
628 // APPLY_UF. The actual node for <kind> is constructible via
629 // ProofRuleChecker::mkKindNode.
631 // ======== True intro
634 // ----------------------------------------
635 // Conclusion: (= F true)
637 // ======== True elim
638 // Children: (P:(= F true))
640 // ----------------------------------------
643 // ======== False intro
644 // Children: (P:(not F))
646 // ----------------------------------------
647 // Conclusion: (= F false)
649 // ======== False elim
650 // Children: (P:(= F false))
652 // ----------------------------------------
653 // Conclusion: (not F)
658 // ---------------------
659 // Conclusion: (= t TheoryUfRewriter::getHoApplyForApplyUf(t))
660 // For example, this rule concludes (f x y) = (HO_APPLY (HO_APPLY f x) y)
662 // ======== Congruence
663 // Children: (P1:(= f g), P2:(= t1 s1), ..., Pn+1:(= tn sn))
665 // ---------------------------------------------
666 // Conclusion: (= (f t1 ... tn) (g s1 ... sn))
667 // Notice that this rule is only used when the application kinds are APPLY_UF.
670 //================================================= Array rules
671 // ======== Read over write
672 // Children: (P:(not (= i1 i2)))
673 // Arguments: ((select (store a i2 e) i1))
674 // ----------------------------------------
675 // Conclusion: (= (select (store a i2 e) i1) (select a i1))
676 ARRAYS_READ_OVER_WRITE
,
677 // ======== Read over write, contrapositive
678 // Children: (P:(not (= (select (store a i2 e) i1) (select a i1)))
680 // ----------------------------------------
681 // Conclusion: (= i1 i2)
682 ARRAYS_READ_OVER_WRITE_CONTRA
,
683 // ======== Read over write 1
685 // Arguments: ((select (store a i e) i))
686 // ----------------------------------------
687 // Conclusion: (= (select (store a i e) i) e)
688 ARRAYS_READ_OVER_WRITE_1
,
689 // ======== Extensionality
690 // Children: (P:(not (= a b)))
692 // ----------------------------------------
693 // Conclusion: (not (= (select a k) (select b k)))
694 // where k is arrays::SkolemCache::getExtIndexSkolem((not (= a b))).
696 // ======== Array Trust
697 // Children: (P1 ... Pn)
699 // ---------------------
703 //================================================= Bit-Vector rules
707 // ---------------------
708 // Conclusion: (= t bitblast(t))
710 // ======== Eager Atom
713 // ---------------------
714 // Conclusion: (= F F[0])
715 // where F is of kind BITVECTOR_EAGER_ATOM
718 //================================================= Datatype rules
719 // ======== Unification
720 // Children: (P:(= (C t1 ... tn) (C s1 ... sn)))
722 // ----------------------------------------
723 // Conclusion: (= ti si)
724 // where C is a constructor.
726 // ======== Instantiate
729 // ----------------------------------------
730 // Conclusion: (= ((_ is C) t) (= t (C (sel_1 t) ... (sel_n t))))
731 // where C is the n^th constructor of the type of T, and (_ is C) is the
732 // discriminator (tester) for C.
736 // Arguments: ((sel_i (C_j t_1 ... t_n)))
737 // ----------------------------------------
738 // Conclusion: (= (sel_i (C_j t_1 ... t_n)) r)
739 // where C_j is a constructor, r is t_i if sel_i is a correctly applied
740 // selector, or TypeNode::mkGroundTerm() of the proper type otherwise. Notice
741 // that the use of mkGroundTerm differs from the rewriter which uses
742 // mkGroundValue in this case.
747 // ----------------------------------------
748 // Conclusion: (or ((_ is C1) t) ... ((_ is Cn) t))
751 // Children: (P1:((_ is Ci) t), P2: ((_ is Cj) t))
753 // ----------------------------------------
757 // ======== Datatype Trust
758 // Children: (P1 ... Pn)
760 // ---------------------
764 //================================================= Quantifiers rules
765 // ======== Skolem intro
768 // ----------------------------------------
769 // Conclusion: (= k t)
770 // where t is the original form of skolem k.
772 // ======== Exists intro
773 // Children: (P:F[t])
774 // Arguments: ((exists ((x T)) F[x]))
775 // ----------------------------------------
776 // Conclusion: (exists ((x T)) F[x])
777 // This rule verifies that F[x] indeed matches F[t] with a substitution
780 // ======== Skolemize
781 // Children: (P:(exists ((x1 T1) ... (xn Tn)) F))
783 // ----------------------------------------
784 // Conclusion: F*sigma
785 // sigma maps x1 ... xn to their representative skolems obtained by
786 // SkolemManager::mkSkolemize, returned in the skolems argument of that
787 // method. Alternatively, can use negated forall as a premise. The witness
788 // terms for the returned skolems can be obtained by
789 // SkolemManager::getWitnessForm.
791 // ======== Instantiate
792 // Children: (P:(forall ((x1 T1) ... (xn Tn)) F))
793 // Arguments: (t1 ... tn)
794 // ----------------------------------------
795 // Conclusion: F*sigma
796 // sigma maps x1 ... xn to t1 ... tn.
799 //================================================= String rules
800 //======================== Core solver
801 // ======== Concat eq
802 // Children: (P1:(= (str.++ t1 ... tn t) (str.++ t1 ... tn s)))
803 // Arguments: (b), indicating if reverse direction
804 // ---------------------
805 // Conclusion: (= t s)
807 // Notice that t or s may be empty, in which case they are implicit in the
808 // concatenation above. For example, if
809 // P1 concludes (= x (str.++ x z)), then
810 // (CONCAT_EQ P1 :args false) concludes (= "" z)
812 // Also note that constants are split, such that if
813 // P1 concludes (= (str.++ "abc" x) (str.++ "a" y)), then
814 // (CONCAT_EQ P1 :args false) concludes (= (str.++ "bc" x) y)
815 // This splitting is done only for constants such that Word::splitConstant
818 // ======== Concat unify
819 // Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)),
820 // P2:(= (str.len t1) (str.len s1)))
821 // Arguments: (b), indicating if reverse direction
822 // ---------------------
823 // Conclusion: (= t1 s1)
825 // ======== Concat conflict
826 // Children: (P1:(= (str.++ c1 t) (str.++ c2 s)))
827 // Arguments: (b), indicating if reverse direction
828 // ---------------------
830 // Where c1, c2 are constants such that Word::splitConstant(c1,c2,index,b)
831 // is null, in other words, neither is a prefix of the other.
833 // ======== Concat split
834 // Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)),
835 // P2:(not (= (str.len t1) (str.len s1))))
836 // Arguments: (false)
837 // ---------------------
838 // Conclusion: (or (= t1 (str.++ s1 r_t)) (= s1 (str.++ t1 r_s)))
840 // r_t = (witness ((z String)) (= z (suf t1 (str.len s1)))),
841 // r_s = (witness ((z String)) (= z (suf s1 (str.len t1)))).
843 // or the reverse form of the above:
845 // Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)),
846 // P2:(not (= (str.len t2) (str.len s2))))
848 // ---------------------
849 // Conclusion: (or (= t2 (str.++ r_t s2)) (= s2 (str.++ r_s t2)))
851 // r_t = (witness ((z String)) (= z (pre t2 (- (str.len t2) (str.len
852 // s2))))), r_s = (witness ((z String)) (= z (pre s2 (- (str.len s2)
855 // Above, (suf x n) is shorthand for (str.substr x n (- (str.len x) n)) and
856 // (pre x n) is shorthand for (str.substr x 0 n).
858 // ======== Concat constant split
859 // Children: (P1:(= (str.++ t1 t2) (str.++ c s2)),
860 // P2:(not (= (str.len t1) 0)))
861 // Arguments: (false)
862 // ---------------------
863 // Conclusion: (= t1 (str.++ c r))
865 // r = (witness ((z String)) (= z (suf t1 1))).
867 // or the reverse form of the above:
869 // Children: (P1:(= (str.++ t1 t2) (str.++ s1 c)),
870 // P2:(not (= (str.len t2) 0)))
872 // ---------------------
873 // Conclusion: (= t2 (str.++ r c))
875 // r = (witness ((z String)) (= z (pre t2 (- (str.len t2) 1)))).
877 // ======== Concat length propagate
878 // Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)),
879 // P2:(> (str.len t1) (str.len s1)))
880 // Arguments: (false)
881 // ---------------------
882 // Conclusion: (= t1 (str.++ s1 r_t))
884 // r_t = (witness ((z String)) (= z (suf t1 (str.len s1))))
886 // or the reverse form of the above:
888 // Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)),
889 // P2:(> (str.len t2) (str.len s2)))
890 // Arguments: (false)
891 // ---------------------
892 // Conclusion: (= t2 (str.++ r_t s2))
894 // r_t = (witness ((z String)) (= z (pre t2 (- (str.len t2) (str.len
897 // ======== Concat constant propagate
898 // Children: (P1:(= (str.++ t1 w1 t2) (str.++ w2 s)),
899 // P2:(not (= (str.len t1) 0)))
900 // Arguments: (false)
901 // ---------------------
902 // Conclusion: (= t1 (str.++ w3 r))
904 // w1, w2, w3, w4 are words,
907 // p = Word::overlap((suf w2 1), w1),
908 // r = (witness ((z String)) (= z (suf t1 (str.len w3)))).
909 // In other words, w4 is the largest suffix of (suf w2 1) that can contain a
910 // prefix of w1; since t1 is non-empty, w3 must therefore be contained in t1.
912 // or the reverse form of the above:
914 // Children: (P1:(= (str.++ t1 w1 t2) (str.++ s w2)),
915 // P2:(not (= (str.len t2) 0)))
917 // ---------------------
918 // Conclusion: (= t2 (str.++ r w3))
920 // w1, w2, w3, w4 are words,
921 // w3 is (suf w2 (- (str.len w2) p)),
922 // w4 is (pre w2 (- (str.len w2) p)),
923 // p = Word::roverlap((pre w2 (- (str.len w2) 1)), w1),
924 // r = (witness ((z String)) (= z (pre t2 (- (str.len t2) (str.len w3))))).
925 // In other words, w4 is the largest prefix of (pre w2 (- (str.len w2) 1))
926 // that can contain a suffix of w1; since t2 is non-empty, w3 must therefore
927 // be contained in t2.
929 // ======== String decompose
930 // Children: (P1: (>= (str.len t) n)
931 // Arguments: (false)
932 // ---------------------
933 // Conclusion: (and (= t (str.++ w1 w2)) (= (str.len w1) n))
935 // Children: (P1: (>= (str.len t) n)
937 // ---------------------
938 // Conclusion: (and (= t (str.++ w1 w2)) (= (str.len w2) n))
940 // w1 is (witness ((z String)) (= z (pre t n)))
941 // w2 is (witness ((z String)) (= z (suf t n)))
943 // ======== Length positive
946 // ---------------------
947 // Conclusion: (or (and (= (str.len t) 0) (= t "")) (> (str.len t 0)))
949 // ======== Length non-empty
950 // Children: (P1:(not (= t "")))
952 // ---------------------
953 // Conclusion: (not (= (str.len t) 0))
954 STRING_LENGTH_NON_EMPTY
,
955 //======================== Extended functions
956 // ======== Reduction
959 // ---------------------
960 // Conclusion: (and R (= t w))
961 // where w = strings::StringsPreprocess::reduce(t, R, ...).
962 // In other words, R is the reduction predicate for extended term t, and w is
963 // (witness ((z T)) (= z t))
964 // Notice that the free variables of R are w and the free variables of t.
966 // ======== Eager Reduction
968 // Arguments: (t, id?)
969 // ---------------------
971 // where R = strings::TermRegistry::eagerReduce(t, id).
972 STRING_EAGER_REDUCTION
,
973 //======================== Regular expressions
974 // ======== Regular expression intersection
975 // Children: (P:(str.in.re t R1), P:(str.in.re t R2))
977 // ---------------------
978 // Conclusion: (str.in.re t (re.inter R1 R2)).
980 // ======== Regular expression unfold positive
981 // Children: (P:(str.in.re t R))
983 // ---------------------
984 // Conclusion:(RegExpOpr::reduceRegExpPos((str.in.re t R))),
985 // corresponding to the one-step unfolding of the premise.
987 // ======== Regular expression unfold negative
988 // Children: (P:(not (str.in.re t R)))
990 // ---------------------
991 // Conclusion:(RegExpOpr::reduceRegExpNeg((not (str.in.re t R)))),
992 // corresponding to the one-step unfolding of the premise.
994 // ======== Regular expression unfold negative concat fixed
995 // Children: (P:(not (str.in.re t R)))
997 // ---------------------
998 // Conclusion:(RegExpOpr::reduceRegExpNegConcatFixed((not (str.in.re t
999 // R)),L,i)) where RegExpOpr::getRegExpConcatFixed((not (str.in.re t R)), i) =
1000 // L. corresponding to the one-step unfolding of the premise, optimized for
1001 // fixed length of component i of the regular expression concatenation R.
1002 RE_UNFOLD_NEG_CONCAT_FIXED
,
1003 // ======== Regular expression elimination
1005 // Arguments: (F, b)
1006 // ---------------------
1007 // Conclusion: (= F strings::RegExpElimination::eliminate(F, b))
1008 // where b is a Boolean indicating whether we are using aggressive
1009 // eliminations. Notice this rule concludes (= F F) if no eliminations
1010 // are performed for F.
1012 //======================== Code points
1014 // Arguments: (t, s)
1015 // ---------------------
1016 // Conclusion:(or (= (str.code t) (- 1))
1017 // (not (= (str.code t) (str.code s)))
1020 //======================== Sequence unit
1021 // Children: (P:(= (seq.unit x) (seq.unit y)))
1023 // ---------------------
1024 // Conclusion:(= x y)
1025 // Also applies to the case where (seq.unit y) is a constant sequence
1027 STRING_SEQ_UNIT_INJ
,
1028 // ======== String Trust
1031 // ---------------------
1035 //================================================= Arithmetic rules
1036 // ======== Adding Inequalities
1037 // Note: an ArithLiteral is a term of the form (>< poly const)
1039 // >< is >=, >, ==, <, <=, or not(== ...).
1040 // poly is a polynomial
1041 // const is a rational constant
1043 // Children: (P1:l1, ..., Pn:ln)
1044 // where each li is an ArithLiteral
1045 // not(= ...) is dis-allowed!
1047 // Arguments: (k1, ..., kn), non-zero reals
1048 // ---------------------
1049 // Conclusion: (>< t1 t2)
1050 // where >< is the fusion of the combination of the ><i, (flipping each it
1051 // its ki is negative). >< is always one of <, <=
1052 // NB: this implies that lower bounds must have negative ki,
1053 // and upper bounds must have positive ki.
1054 // t1 is the sum of the scaled polynomials (k_1 * poly_1 + ... + k_n *
1055 // poly_n) t2 is the sum of the scaled constants (k_1 * const_1 + ... + k_n
1057 ARITH_SCALE_SUM_UPPER_BOUNDS
,
1059 // ======== Sum Upper Bounds
1060 // Children: (P1, ... , Pn)
1061 // where each Pi has form (><i, Li, Ri)
1062 // for ><i in {<, <=, ==}
1063 // Conclusion: (>< L R)
1064 // where >< is < if any ><i is <, and <= otherwise.
1065 // L is (+ L1 ... Ln)
1066 // R is (+ R1 ... Rn)
1068 // ======== Tightening Strict Integer Upper Bounds
1069 // Children: (P:(< i c))
1070 // where i has integer type.
1072 // ---------------------
1073 // Conclusion: (<= i greatestIntLessThan(c)})
1076 // ======== Tightening Strict Integer Lower Bounds
1077 // Children: (P:(> i c))
1078 // where i has integer type.
1080 // ---------------------
1081 // Conclusion: (>= i leastIntGreaterThan(c)})
1084 // ======== Trichotomy of the reals
1087 // ---------------------
1089 // where (not A) (not B) and C
1090 // are (> x c) (< x c) and (= x c)
1092 // note that "not" here denotes arithmetic negation, flipping
1096 // ======== Arithmetic operator elimination
1099 // ---------------------
1100 // Conclusion: arith::OperatorElim::getAxiomFor(t)
1101 ARITH_OP_ELIM_AXIOM
,
1103 // ======== Int Trust
1104 // Children: (P1 ... Pn)
1106 // ---------------------
1110 //======== Multiplication sign inference
1112 // Arguments: (f1, ..., fk, m)
1113 // ---------------------
1114 // Conclusion: (=> (and f1 ... fk) (~ m 0))
1115 // Where f1, ..., fk are variables compared to zero (less, greater or not
1116 // equal), m is a monomial from these variables, and ~ is the comparison (less
1117 // or greater) that results from the signs of the variables. All variables
1118 // with even exponent in m should be given as not equal to zero while all
1119 // variables with odd exponent in m should be given as less or greater than
1122 //======== Multiplication with positive factor
1124 // Arguments: (m, (rel lhs rhs))
1125 // ---------------------
1126 // Conclusion: (=> (and (> m 0) (rel lhs rhs)) (rel (* m lhs) (* m rhs)))
1127 // Where rel is a relation symbol.
1129 //======== Multiplication with negative factor
1131 // Arguments: (m, (rel lhs rhs))
1132 // ---------------------
1133 // Conclusion: (=> (and (< m 0) (rel lhs rhs)) (rel_inv (* m lhs) (* m rhs)))
1134 // Where rel is a relation symbol and rel_inv the inverted relation symbol.
1136 //======== Multiplication tangent plane
1138 // Arguments: (t, x, y, a, b, sgn)
1139 // ---------------------
1141 // sgn=-1: (= (<= t tplane) (or (and (<= x a) (>= y b)) (and (>= x a) (<= y
1142 // b))) sgn= 1: (= (>= t tplane) (or (and (<= x a) (<= y b)) (and (>= x a)
1144 // Where x,y are real terms (variables or extended terms), t = (* x y)
1145 // (possibly under rewriting), a,b are real constants, and sgn is either -1
1146 // or 1. tplane is the tangent plane of x*y at (a,b): b*x + a*y - a*b
1149 // ================ Lemmas for transcendentals
1150 //======== Assert bounds on PI
1152 // Arguments: (l, u)
1153 // ---------------------
1154 // Conclusion: (and (>= real.pi l) (<= real.pi u))
1155 // Where l (u) is a valid lower (upper) bound on pi.
1158 //======== Exp at negative values
1161 // ---------------------
1162 // Conclusion: (= (< t 0) (< (exp t) 1))
1163 ARITH_TRANS_EXP_NEG
,
1164 //======== Exp is always positive
1167 // ---------------------
1168 // Conclusion: (> (exp t) 0)
1169 ARITH_TRANS_EXP_POSITIVITY
,
1170 //======== Exp grows super-linearly for positive values
1173 // ---------------------
1174 // Conclusion: (or (<= t 0) (> exp(t) (+ t 1)))
1175 ARITH_TRANS_EXP_SUPER_LIN
,
1176 //======== Exp at zero
1179 // ---------------------
1180 // Conclusion: (= (= t 0) (= (exp t) 1))
1181 ARITH_TRANS_EXP_ZERO
,
1182 //======== Exp is approximated from above for negative values
1184 // Arguments: (d, t, l, u)
1185 // ---------------------
1186 // Conclusion: (=> (and (>= t l) (<= t u)) (<= (exp t) (secant exp l u t))
1187 // Where d is an even positive number, t an arithmetic term and l (u) a lower
1188 // (upper) bound on t. Let p be the d'th taylor polynomial at zero (also
1189 // called the Maclaurin series) of the exponential function. (secant exp l u
1190 // t) denotes the secant of p from (l, exp(l)) to (u, exp(u)) evaluated at t,
1191 // calculated as follows:
1192 // (p(l) - p(u)) / (l - u) * (t - l) + p(l)
1193 // The lemma states that if t is between l and u, then (exp t) is below the
1194 // secant of p from l to u.
1195 ARITH_TRANS_EXP_APPROX_ABOVE_NEG
,
1196 //======== Exp is approximated from above for positive values
1198 // Arguments: (d, t, l, u)
1199 // ---------------------
1200 // Conclusion: (=> (and (>= t l) (<= t u)) (<= (exp t) (secant-pos exp l u t))
1201 // Where d is an even positive number, t an arithmetic term and l (u) a lower
1202 // (upper) bound on t. Let p* be a modification of the d'th taylor polynomial
1203 // at zero (also called the Maclaurin series) of the exponential function as
1204 // follows where p(d-1) is the regular Maclaurin series of degree d-1:
1205 // p* = p(d-1) * (1 + t^n / n!)
1206 // (secant-pos exp l u t) denotes the secant of p from (l, exp(l)) to (u,
1207 // exp(u)) evaluated at t, calculated as follows:
1208 // (p(l) - p(u)) / (l - u) * (t - l) + p(l)
1209 // The lemma states that if t is between l and u, then (exp t) is below the
1210 // secant of p from l to u.
1211 ARITH_TRANS_EXP_APPROX_ABOVE_POS
,
1212 //======== Exp is approximated from below
1214 // Arguments: (d, t)
1215 // ---------------------
1216 // Conclusion: (>= (exp t) (maclaurin exp d t))
1217 // Where d is an odd positive number and (maclaurin exp d t) is the d'th
1218 // taylor polynomial at zero (also called the Maclaurin series) of the
1219 // exponential function evaluated at t. The Maclaurin series for the
1220 // exponential function is the following:
1221 // e^x = \sum_{n=0}^{\infty} x^n / n!
1222 ARITH_TRANS_EXP_APPROX_BELOW
,
1224 //======== Sine is always between -1 and 1
1227 // ---------------------
1228 // Conclusion: (and (<= (sin t) 1) (>= (sin t) (- 1)))
1229 ARITH_TRANS_SINE_BOUNDS
,
1230 //======== Sine arg shifted to -pi..pi
1232 // Arguments: (x, y, s)
1233 // ---------------------
1236 // (= (sin y) (sin x))
1237 // (ite (<= -pi x pi) (= x y) (= x (+ y (* 2 pi s))))
1239 // Where x is the argument to sine, y is a new real skolem that is x shifted
1240 // into -pi..pi and s is a new integer skolem that is the number of phases y
1242 ARITH_TRANS_SINE_SHIFT
,
1243 //======== Sine is symmetric with respect to negation of the argument
1246 // ---------------------
1247 // Conclusion: (= (- (sin t) (sin (- t))) 0)
1248 ARITH_TRANS_SINE_SYMMETRY
,
1249 //======== Sine is bounded by the tangent at zero
1252 // ---------------------
1254 // (=> (> t 0) (< (sin t) t))
1255 // (=> (< t 0) (> (sin t) t))
1257 ARITH_TRANS_SINE_TANGENT_ZERO
,
1258 //======== Sine is bounded by the tangents at -pi and pi
1261 // ---------------------
1263 // (=> (> t -pi) (> (sin t) (- -pi t)))
1264 // (=> (< t pi) (< (sin t) (- pi t)))
1266 ARITH_TRANS_SINE_TANGENT_PI
,
1267 //======== Sine is approximated from above for negative values
1269 // Arguments: (d, t, lb, ub, l, u)
1270 // ---------------------
1271 // Conclusion: (=> (and (>= t lb) (<= t ub)) (<= (sin t) (secant sin l u t))
1272 // Where d is an even positive number, t an arithmetic term, lb (ub) a
1273 // symbolic lower (upper) bound on t (possibly containing pi) and l (u) the
1274 // evaluated lower (upper) bound on t. Let p be the d'th taylor polynomial at
1275 // zero (also called the Maclaurin series) of the sine function. (secant sin l
1276 // u t) denotes the secant of p from (l, sin(l)) to (u, sin(u)) evaluated at
1277 // t, calculated as follows:
1278 // (p(l) - p(u)) / (l - u) * (t - l) + p(l)
1279 // The lemma states that if t is between l and u, then (sin t) is below the
1280 // secant of p from l to u.
1281 ARITH_TRANS_SINE_APPROX_ABOVE_NEG
,
1282 //======== Sine is approximated from above for positive values
1284 // Arguments: (d, t, c, lb, ub)
1285 // ---------------------
1286 // Conclusion: (=> (and (>= t lb) (<= t ub)) (<= (sin t) (upper sin c))
1287 // Where d is an even positive number, t an arithmetic term, c an arithmetic
1288 // constant, and lb (ub) a symbolic lower (upper) bound on t (possibly
1289 // containing pi). Let p be the d'th taylor polynomial at zero (also called
1290 // the Maclaurin series) of the sine function. (upper sin c) denotes the upper
1291 // bound on sin(c) given by p and lb,ub are such that sin(t) is the maximum of
1292 // the sine function on (lb,ub).
1293 ARITH_TRANS_SINE_APPROX_ABOVE_POS
,
1294 //======== Sine is approximated from below for negative values
1296 // Arguments: (d, t, c, lb, ub)
1297 // ---------------------
1298 // Conclusion: (=> (and (>= t lb) (<= t ub)) (>= (sin t) (lower sin c))
1299 // Where d is an even positive number, t an arithmetic term, c an arithmetic
1300 // constant, and lb (ub) a symbolic lower (upper) bound on t (possibly
1301 // containing pi). Let p be the d'th taylor polynomial at zero (also called
1302 // the Maclaurin series) of the sine function. (lower sin c) denotes the lower
1303 // bound on sin(c) given by p and lb,ub are such that sin(t) is the minimum of
1304 // the sine function on (lb,ub).
1305 ARITH_TRANS_SINE_APPROX_BELOW_NEG
,
1306 //======== Sine is approximated from below for positive values
1308 // Arguments: (d, t, lb, ub, l, u)
1309 // ---------------------
1310 // Conclusion: (=> (and (>= t lb) (<= t ub)) (>= (sin t) (secant sin l u t))
1311 // Where d is an even positive number, t an arithmetic term, lb (ub) a
1312 // symbolic lower (upper) bound on t (possibly containing pi) and l (u) the
1313 // evaluated lower (upper) bound on t. Let p be the d'th taylor polynomial at
1314 // zero (also called the Maclaurin series) of the sine function. (secant sin l
1315 // u t) denotes the secant of p from (l, sin(l)) to (u, sin(u)) evaluated at
1316 // t, calculated as follows:
1317 // (p(l) - p(u)) / (l - u) * (t - l) + p(l)
1318 // The lemma states that if t is between l and u, then (sin t) is above the
1319 // secant of p from l to u.
1320 ARITH_TRANS_SINE_APPROX_BELOW_POS
,
1322 // ================ CAD Lemmas
1323 // We use IRP for IndexedRootPredicate.
1325 // A formula "Interval" describes that a variable (xn is none is given) is
1326 // within a particular interval whose bounds are given as IRPs. It is either
1327 // an open interval or a point interval:
1328 // (IRP k poly) < xn < (IRP k poly)
1329 // xn == (IRP k poly)
1331 // A formula "Cell" describes a portion
1332 // of the real space in the following form:
1333 // Interval(x1) and Interval(x2) and ...
1334 // We implicitly assume a Cell to go up to n-1 (and can be empty).
1336 // A formula "Covering" is a set of Intervals, implying that xn can be in
1337 // neither of these intervals. To be a covering (of the real line), the union
1338 // of these intervals should be the real numbers.
1339 // ======== CAD direct conflict
1340 // Children (Cell, A)
1341 // ---------------------
1342 // Conclusion: (false)
1343 // A direct interval is generated from an assumption A (in variables x1...xn)
1344 // over a Cell (in variables x1...xn). It derives that A evaluates to false
1345 // over the Cell. In the actual algorithm, it means that xn can not be in the
1346 // topmost interval of the Cell.
1347 ARITH_NL_CAD_DIRECT
,
1348 // ======== CAD recursive interval
1349 // Children (Cell, Covering)
1350 // ---------------------
1351 // Conclusion: (false)
1352 // A recursive interval is generated from a Covering (for xn) over a Cell
1353 // (in variables x1...xn-1). It generates the conclusion that no xn exists
1354 // that extends the Cell and satisfies all assumptions.
1355 ARITH_NL_CAD_RECURSIVE
,
1357 //================================================= Unknown rule
1362 * Converts a proof rule to a string. Note: This function is also used in
1363 * `safe_print()`. Changing this function name or signature will result in
1364 * `safe_print()` printing "<unsupported>" instead of the proper strings for
1367 * @param id The proof rule
1368 * @return The name of the proof rule
1370 const char* toString(PfRule id
);
1373 * Writes a proof rule name to a stream.
1375 * @param out The stream to write to
1376 * @param id The proof rule to write to the stream
1377 * @return The stream
1379 std::ostream
& operator<<(std::ostream
& out
, PfRule id
);
1381 /** Hash function for proof rules */
1382 struct PfRuleHashFunction
1384 size_t operator()(PfRule id
) const;
1385 }; /* struct PfRuleHashFunction */
1389 #endif /* CVC5__EXPR__PROOF_RULE_H */