1 /********************* */
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Haniel Barbosa, Alex Ozdemir
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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.\endverbatim
12 ** \brief Proof rule enumeration
15 #include "cvc4_private.h"
17 #ifndef CVC4__EXPR__PROOF_RULE_H
18 #define CVC4__EXPR__PROOF_RULE_H
25 * An enumeration for proof rules. This enumeration is analogous to Kind for
26 * Node objects. In the documentation below, P:F denotes a ProofNode that
29 * Conceptually, the following proof rules form a calculus whose target
30 * user is the Node-level theory solvers. This means that the rules below
31 * are designed to reason about, among other things, common operations on Node
32 * objects like Rewriter::rewrite or Node::substitute. It is intended to be
33 * translated or printed in other formats.
35 * The following PfRule values include core rules and those categorized by
36 * theory, including the theory of equality.
38 * The "core rules" include two distinguished rules which have special status:
39 * (1) ASSUME, which represents an open leaf in a proof.
40 * (2) SCOPE, which closes the scope of assumptions.
41 * The core rules additionally correspond to generic operations that are done
42 * internally on nodes, e.g. calling Rewriter::rewrite.
44 enum class PfRule
: uint32_t
46 //================================================= Core rules
47 //======================== Assume and Scope
48 // ======== Assumption (a leaf)
54 // This rule has special status, in that an application of assume is an
55 // open leaf in a proof that is not (yet) justified. An assume leaf is
56 // analogous to a free variable in a term, where we say "F is a free
57 // assumption in proof P" if it contains an application of F that is not
58 // bound by SCOPE (see below).
60 // ======== Scope (a binder for assumptions)
62 // Arguments: (F1, ..., Fn)
64 // Conclusion: (=> (and F1 ... Fn) F) or (not (and F1 ... Fn)) if F is false
66 // This rule has a dual purpose with ASSUME. It is a way to close
67 // assumptions in a proof. We require that F1 ... Fn are free assumptions in
68 // P and say that F1, ..., Fn are not free in (SCOPE P). In other words, they
69 // are bound by this application. For example, the proof node:
70 // (SCOPE (ASSUME F) :args F)
71 // has the conclusion (=> F F) and has no free assumptions. More generally, a
72 // proof with no free assumptions always concludes a valid formula.
75 //======================== Builtin theory (common node operations)
76 // ======== Substitution
77 // Children: (P1:F1, ..., Pn:Fn)
78 // Arguments: (t, (ids)?)
79 // ---------------------------------------------------------------
80 // Conclusion: (= t t*sigma{ids}(Fn)*...*sigma{ids}(F1))
81 // where sigma{ids}(Fi) are substitutions, which notice are applied in
83 // Notice that ids is a MethodId identifier, which determines how to convert
84 // the formulas F1, ..., Fn into substitutions.
88 // Arguments: (t, (idr)?)
89 // ----------------------------------------
90 // Conclusion: (= t Rewriter{idr}(t))
91 // where idr is a MethodId identifier, which determines the kind of rewriter
92 // to apply, e.g. Rewriter::rewrite.
97 // ----------------------------------------
98 // Conclusion: (= t Evaluator::evaluate(t))
99 // Note this is equivalent to:
100 // (REWRITE t MethodId::RW_EVALUATE)
102 // ======== Substitution + Rewriting equality introduction
104 // In this rule, we provide a term t and conclude that it is equal to its
105 // rewritten form under a (proven) substitution.
107 // Children: (P1:F1, ..., Pn:Fn)
108 // Arguments: (t, (ids (idr)?)?)
109 // ---------------------------------------------------------------
110 // Conclusion: (= t t')
113 // Rewriter{idr}(t*sigma{ids}(Fn)*...*sigma{ids}(F1))
115 // In other words, from the point of view of Skolem forms, this rule
116 // transforms t to t' by standard substitution + rewriting.
118 // The argument ids and idr is optional and specify the identifier of the
119 // substitution and rewriter respectively to be used. For details, see
120 // theory/builtin/proof_checker.h.
122 // ======== Substitution + Rewriting predicate introduction
124 // In this rule, we provide a formula F and conclude it, under the condition
125 // that it rewrites to true under a proven substitution.
127 // Children: (P1:F1, ..., Pn:Fn)
128 // Arguments: (F, (ids (idr)?)?)
129 // ---------------------------------------------------------------
132 // Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)) == true
133 // where ids and idr are method identifiers.
135 // More generally, this rule also holds when:
136 // Rewriter::rewrite(toWitness(F')) == true
137 // where F' is the result of the left hand side of the equality above. Here,
138 // notice that we apply rewriting on the witness form of F', meaning that this
139 // rule may conclude an F whose Skolem form is justified by the definition of
140 // its (fresh) Skolem variables. For example, this rule may justify the
141 // conclusion (= k t) where k is the purification Skolem for t, whose
142 // witness form is (witness ((x T)) (= x t)).
144 // Furthermore, notice that the rewriting and substitution is applied only
145 // within the side condition, meaning the rewritten form of the witness form
146 // of F does not escape this rule.
148 // ======== Substitution + Rewriting predicate elimination
150 // In this rule, if we have proven a formula F, then we may conclude its
151 // rewritten form under a proven substitution.
153 // Children: (P1:F, P2:F1, ..., P_{n+1}:Fn)
154 // Arguments: ((ids (idr)?)?)
155 // ----------------------------------------
159 // Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)).
160 // where ids and idr are method identifiers.
162 // We rewrite only on the Skolem form of F, similar to MACRO_SR_EQ_INTRO.
164 // ======== Substitution + Rewriting predicate transform
166 // In this rule, if we have proven a formula F, then we may provide a formula
167 // G and conclude it if F and G are equivalent after rewriting under a proven
170 // Children: (P1:F, P2:F1, ..., P_{n+1}:Fn)
171 // Arguments: (G, (ids (idr)?)?)
172 // ----------------------------------------
175 // Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)) ==
176 // Rewriter{idr}(G*sigma{ids}(Fn)*...*sigma{ids}(F1))
178 // More generally, this rule also holds when:
179 // Rewriter::rewrite(toWitness(F')) == Rewriter::rewrite(toWitness(G'))
180 // where F' and G' are the result of each side of the equation above. Here,
181 // witness forms are used in a similar manner to MACRO_SR_PRED_INTRO above.
182 MACRO_SR_PRED_TRANSFORM
,
184 //================================================= Processing rules
185 // ======== Remove Term Formulas Axiom
188 // ---------------------------------------------------------------
189 // Conclusion: RemoveTermFormulas::getAxiomFor(t).
190 REMOVE_TERM_FORMULA_AXIOM
,
192 //================================================= Trusted rules
193 // ======== Theory lemma
195 // Arguments: (F, tid)
196 // ---------------------------------------------------------------
198 // where F is a (T-valid) theory lemma generated by theory with TheoryId tid.
199 // This is a "coarse-grained" rule that is used as a placeholder if a theory
200 // did not provide a proof for a lemma or conflict.
202 // ======== Theory Rewrite
204 // Arguments: (F, tid, rid)
205 // ----------------------------------------
207 // where F is an equality of the form (= t t') where t' is obtained by
208 // applying the kind of rewriting given by the method identifier rid, which
210 // { RW_REWRITE_THEORY_PRE, RW_REWRITE_THEORY_POST, RW_REWRITE_EQ_EXT }
211 // Notice that the checker for this rule does not replay the rewrite to ensure
212 // correctness, since theory rewriter methods are not static. For example,
213 // the quantifiers rewriter involves constructing new bound variables that are
214 // not guaranteed to be consistent on each call.
216 // The rules in this section have the signature of a "trusted rule":
220 // ---------------------------------------------------------------
223 // where F is an equality of the form t = t' where t was replaced by t'
224 // based on some preprocessing pass, or otherwise F was added as a new
225 // assertion by some preprocessing pass.
227 // where F was added as a new assertion by some preprocessing pass.
229 // where F is an equality of the form t = Theory::ppRewrite(t) for some
230 // theory. Notice this is a "trusted" rule.
232 // where F was added as a new assertion by theory preprocessing.
233 THEORY_PREPROCESS_LEMMA
,
234 // where F is an equality of the form t = t' where t was replaced by t'
235 // based on theory expand definitions.
237 // where F is an existential (exists ((x T)) (P x)) used for introducing
238 // a witness term (witness ((x T)) (P x)).
240 // where F is an equality (= t t') that holds by a form of rewriting that
241 // could not be replayed during proof postprocessing.
243 // where F is an equality (= t t') that holds by a form of substitution that
244 // could not be replayed during proof postprocessing.
246 // where F is an equality (= t t') that holds by a form of substitution that
247 // could not be determined by the TrustSubstitutionMap.
250 //================================================= Boolean rules
251 // ======== Resolution
254 // Arguments: (pol, L)
255 // ---------------------
258 // - C1 and C2 are nodes viewed as clauses, i.e., either an OR node with
259 // each children viewed as a literal or a node viewed as a literal. Note
260 // that an OR node could also be a literal.
261 // - pol is either true or false, representing the polarity of the pivot on
263 // - L is the pivot of the resolution, which occurs as is (resp. under a
264 // NOT) in C1 and negatively (as is) in C2 if pol = true (pol = false).
265 // C is a clause resulting from collecting all the literals in C1, minus the
266 // first occurrence of the pivot or its negation, and C2, minus the first
267 // occurrence of the pivot or its negation, according to the policy above.
268 // If the resulting clause has a single literal, that literal itself is the
269 // result; if it has no literals, then the result is false; otherwise it's
270 // an OR node of the resulting literals.
272 // Note that it may be the case that the pivot does not occur in the
273 // clauses. In this case the rule is not unsound, but it does not correspond
274 // to resolution but rather to a weakening of the clause that did not have a
275 // literal eliminated.
277 // ======== N-ary Resolution
278 // Children: (P1:C_1, ..., Pm:C_n)
279 // Arguments: (pol_1, L_1, ..., pol_{n-1}, L_{n-1})
280 // ---------------------
283 // - let C_1 ... C_n be nodes viewed as clauses, as defined above
284 // - let "C_1 <>_{L,pol} C_2" represent the resolution of C_1 with C_2 with
285 // pivot L and polarity pol, as defined above
286 // - let C_1' = C_1 (from P1),
287 // - for each i > 1, let C_i' = C_{i-1} <>_{L_{i-1}, pol_{i-1}} C_i'
288 // The result of the chain resolution is C = C_n'
290 // ======== Factoring
293 // ---------------------
296 // Set representations of C1 and C2 is the same and the number of literals in
297 // C2 is smaller than that of C1
299 // ======== Reordering
302 // ---------------------
305 // Set representations of C1 and C2 is the same but the number of literals in
306 // C2 is the same of that of C1
308 // ======== N-ary Resolution + Factoring + Reordering
309 // Children: (P1:C_1, ..., Pm:C_n)
310 // Arguments: (C, pol_1, L_1, ..., pol_{n-1}, L_{n-1})
311 // ---------------------
314 // - let C_1 ... C_n be nodes viewed as clauses, as defined in RESOLUTION
315 // - let "C_1 <>_{L,pol} C_2" represent the resolution of C_1 with C_2 with
316 // pivot L and polarity pol, as defined in RESOLUTION
317 // - let C_1' be equal, in its set representation, to C_1 (from P1),
318 // - for each i > 1, let C_i' be equal, it its set representation, to
319 // C_{i-1} <>_{L_{i-1}, pol_{i-1}} C_i'
320 // The result of the chain resolution is C, which is equal, in its set
321 // representation, to C_n'
327 // ---------------------
328 // Conclusion: (or F (not F))
330 // ======== Equality resolution
331 // Children: (P1:F1, P2:(= F1 F2))
333 // ---------------------
335 // Note this can optionally be seen as a macro for EQUIV_ELIM1+RESOLUTION.
337 // ======== Modus ponens
338 // Children: (P1:F1, P2:(=> F1 F2))
340 // ---------------------
342 // Note this can optionally be seen as a macro for IMPLIES_ELIM+RESOLUTION.
344 // ======== Double negation elimination
345 // Children: (P:(not (not F)))
347 // ---------------------
350 // ======== Contradiction
351 // Children: (P1:F P2:(not F))
353 // ---------------------
356 // ======== And elimination
357 // Children: (P:(and F1 ... Fn))
359 // ---------------------
362 // ======== And introduction
363 // Children: (P1:F1 ... Pn:Fn))
365 // ---------------------
366 // Conclusion: (and P1 ... Pn)
368 // ======== Not Or elimination
369 // Children: (P:(not (or F1 ... Fn)))
371 // ---------------------
372 // Conclusion: (not Fi)
374 // ======== Implication elimination
375 // Children: (P:(=> F1 F2))
377 // ---------------------
378 // Conclusion: (or (not F1) F2)
380 // ======== Not Implication elimination version 1
381 // Children: (P:(not (=> F1 F2)))
383 // ---------------------
386 // ======== Not Implication elimination version 2
387 // Children: (P:(not (=> F1 F2)))
389 // ---------------------
390 // Conclusion: (not F2)
392 // ======== Equivalence elimination version 1
393 // Children: (P:(= F1 F2))
395 // ---------------------
396 // Conclusion: (or (not F1) F2)
398 // ======== Equivalence elimination version 2
399 // Children: (P:(= F1 F2))
401 // ---------------------
402 // Conclusion: (or F1 (not F2))
404 // ======== Not Equivalence elimination version 1
405 // Children: (P:(not (= F1 F2)))
407 // ---------------------
408 // Conclusion: (or F1 F2)
410 // ======== Not Equivalence elimination version 2
411 // Children: (P:(not (= F1 F2)))
413 // ---------------------
414 // Conclusion: (or (not F1) (not F2))
416 // ======== XOR elimination version 1
417 // Children: (P:(xor F1 F2)))
419 // ---------------------
420 // Conclusion: (or F1 F2)
422 // ======== XOR elimination version 2
423 // Children: (P:(xor F1 F2)))
425 // ---------------------
426 // Conclusion: (or (not F1) (not F2))
428 // ======== Not XOR elimination version 1
429 // Children: (P:(not (xor F1 F2)))
431 // ---------------------
432 // Conclusion: (or F1 (not F2))
434 // ======== Not XOR elimination version 2
435 // Children: (P:(not (xor F1 F2)))
437 // ---------------------
438 // Conclusion: (or (not F1) F2)
440 // ======== ITE elimination version 1
441 // Children: (P:(ite C F1 F2))
443 // ---------------------
444 // Conclusion: (or (not C) F1)
446 // ======== ITE elimination version 2
447 // Children: (P:(ite C F1 F2))
449 // ---------------------
450 // Conclusion: (or C F2)
452 // ======== Not ITE elimination version 1
453 // Children: (P:(not (ite C F1 F2)))
455 // ---------------------
456 // Conclusion: (or (not C) (not F1))
458 // ======== Not ITE elimination version 1
459 // Children: (P:(not (ite C F1 F2)))
461 // ---------------------
462 // Conclusion: (or C (not F2))
465 //================================================= De Morgan rules
467 // Children: (P:(not (and F1 ... Fn))
469 // ---------------------
470 // Conclusion: (or (not F1) ... (not Fn))
472 //================================================= CNF rules
473 // ======== CNF And Pos
475 // Arguments: ((and F1 ... Fn), i)
476 // ---------------------
477 // Conclusion: (or (not (and F1 ... Fn)) Fi)
479 // ======== CNF And Neg
481 // Arguments: ((and F1 ... Fn))
482 // ---------------------
483 // Conclusion: (or (and F1 ... Fn) (not F1) ... (not Fn))
485 // ======== CNF Or Pos
487 // Arguments: ((or F1 ... Fn))
488 // ---------------------
489 // Conclusion: (or (not (or F1 ... Fn)) F1 ... Fn)
491 // ======== CNF Or Neg
493 // Arguments: ((or F1 ... Fn), i)
494 // ---------------------
495 // Conclusion: (or (or F1 ... Fn) (not Fi))
497 // ======== CNF Implies Pos
499 // Arguments: ((implies F1 F2))
500 // ---------------------
501 // Conclusion: (or (not (implies F1 F2)) (not F1) F2)
503 // ======== CNF Implies Neg version 1
505 // Arguments: ((implies F1 F2))
506 // ---------------------
507 // Conclusion: (or (implies F1 F2) F1)
509 // ======== CNF Implies Neg version 2
511 // Arguments: ((implies F1 F2))
512 // ---------------------
513 // Conclusion: (or (implies F1 F2) (not F2))
515 // ======== CNF Equiv Pos version 1
517 // Arguments: ((= F1 F2))
518 // ---------------------
519 // Conclusion: (or (not (= F1 F2)) (not F1) F2)
521 // ======== CNF Equiv Pos version 2
523 // Arguments: ((= F1 F2))
524 // ---------------------
525 // Conclusion: (or (not (= F1 F2)) F1 (not F2))
527 // ======== CNF Equiv Neg version 1
529 // Arguments: ((= F1 F2))
530 // ---------------------
531 // Conclusion: (or (= F1 F2) F1 F2)
533 // ======== CNF Equiv Neg version 2
535 // Arguments: ((= F1 F2))
536 // ---------------------
537 // Conclusion: (or (= F1 F2) (not F1) (not F2))
539 // ======== CNF Xor Pos version 1
541 // Arguments: ((xor F1 F2))
542 // ---------------------
543 // Conclusion: (or (not (xor F1 F2)) F1 F2)
545 // ======== CNF Xor Pos version 2
547 // Arguments: ((xor F1 F2))
548 // ---------------------
549 // Conclusion: (or (not (xor F1 F2)) (not F1) (not F2))
551 // ======== CNF Xor Neg version 1
553 // Arguments: ((xor F1 F2))
554 // ---------------------
555 // Conclusion: (or (xor F1 F2) (not F1) F2)
557 // ======== CNF Xor Neg version 2
559 // Arguments: ((xor F1 F2))
560 // ---------------------
561 // Conclusion: (or (xor F1 F2) F1 (not F2))
563 // ======== CNF ITE Pos version 1
565 // Arguments: ((ite C F1 F2))
566 // ---------------------
567 // Conclusion: (or (not (ite C F1 F2)) (not C) F1)
569 // ======== CNF ITE Pos version 2
571 // Arguments: ((ite C F1 F2))
572 // ---------------------
573 // Conclusion: (or (not (ite C F1 F2)) C F2)
575 // ======== CNF ITE Pos version 3
577 // Arguments: ((ite C F1 F2))
578 // ---------------------
579 // Conclusion: (or (not (ite C F1 F2)) F1 F2)
581 // ======== CNF ITE Neg version 1
583 // Arguments: ((ite C F1 F2))
584 // ---------------------
585 // Conclusion: (or (ite C F1 F2) (not C) (not F1))
587 // ======== CNF ITE Neg version 2
589 // Arguments: ((ite C F1 F2))
590 // ---------------------
591 // Conclusion: (or (ite C F1 F2) C (not F2))
593 // ======== CNF ITE Neg version 3
595 // Arguments: ((ite C F1 F2))
596 // ---------------------
597 // Conclusion: (or (ite C F1 F2) (not F1) (not F2))
600 //================================================= Equality rules
601 // ======== Reflexive
604 // ---------------------
605 // Conclusion: (= t t)
607 // ======== Symmetric
608 // Children: (P:(= t1 t2)) or (P:(not (= t1 t2)))
610 // -----------------------
611 // Conclusion: (= t2 t1) or (not (= t2 t1))
613 // ======== Transitivity
614 // Children: (P1:(= t1 t2), ..., Pn:(= t{n-1} tn))
616 // -----------------------
617 // Conclusion: (= t1 tn)
619 // ======== Congruence
620 // Children: (P1:(= t1 s1), ..., Pn:(= tn sn))
621 // Arguments: (<kind> f?)
622 // ---------------------------------------------
623 // Conclusion: (= (<kind> f? t1 ... tn) (<kind> f? s1 ... sn))
624 // Notice that f must be provided iff <kind> is a parameterized kind, e.g.
625 // APPLY_UF. The actual node for <kind> is constructible via
626 // ProofRuleChecker::mkKindNode.
628 // ======== True intro
631 // ----------------------------------------
632 // Conclusion: (= F true)
634 // ======== True elim
635 // Children: (P:(= F true))
637 // ----------------------------------------
640 // ======== False intro
641 // Children: (P:(not F))
643 // ----------------------------------------
644 // Conclusion: (= F false)
646 // ======== False elim
647 // Children: (P:(= F false))
649 // ----------------------------------------
650 // Conclusion: (not F)
655 // ---------------------
656 // Conclusion: (= t TheoryUfRewriter::getHoApplyForApplyUf(t))
657 // For example, this rule concludes (f x y) = (HO_APPLY (HO_APPLY f x) y)
659 // ======== Congruence
660 // Children: (P1:(= f g), P2:(= t1 s1), ..., Pn+1:(= tn sn))
662 // ---------------------------------------------
663 // Conclusion: (= (f t1 ... tn) (g s1 ... sn))
664 // Notice that this rule is only used when the application kinds are APPLY_UF.
667 //================================================= Array rules
668 // ======== Read over write
669 // Children: (P:(not (= i1 i2)))
670 // Arguments: ((select (store a i2 e) i1))
671 // ----------------------------------------
672 // Conclusion: (= (select (store a i2 e) i1) (select a i1))
673 ARRAYS_READ_OVER_WRITE
,
674 // ======== Read over write, contrapositive
675 // Children: (P:(not (= (select (store a i2 e) i1) (select a i1)))
677 // ----------------------------------------
678 // Conclusion: (= i1 i2)
679 ARRAYS_READ_OVER_WRITE_CONTRA
,
680 // ======== Read over write 1
682 // Arguments: ((select (store a i e) i))
683 // ----------------------------------------
684 // Conclusion: (= (select (store a i e) i) e)
685 ARRAYS_READ_OVER_WRITE_1
,
686 // ======== Extensionality
687 // Children: (P:(not (= a b)))
689 // ----------------------------------------
690 // Conclusion: (not (= (select a k) (select b k)))
691 // where k is arrays::SkolemCache::getExtIndexSkolem((not (= a b))).
693 // ======== Array Trust
694 // Children: (P1 ... Pn)
696 // ---------------------
700 //================================================= Bit-Vector rules
704 // ---------------------
705 // Conclusion: (= t bitblast(t))
707 // ======== Eager Atom
710 // ---------------------
711 // Conclusion: (= F F[0])
712 // where F is of kind BITVECTOR_EAGER_ATOM
715 //================================================= Datatype rules
716 // ======== Unification
717 // Children: (P:(= (C t1 ... tn) (C s1 ... sn)))
719 // ----------------------------------------
720 // Conclusion: (= ti si)
721 // where C is a constructor.
723 // ======== Instantiate
726 // ----------------------------------------
727 // Conclusion: (= ((_ is C) t) (= t (C (sel_1 t) ... (sel_n t))))
728 // where C is the n^th constructor of the type of T, and (_ is C) is the
729 // discriminator (tester) for C.
733 // Arguments: ((sel_i (C_j t_1 ... t_n)))
734 // ----------------------------------------
735 // Conclusion: (= (sel_i (C_j t_1 ... t_n)) r)
736 // where C_j is a constructor, r is t_i if sel_i is a correctly applied
737 // selector, or TypeNode::mkGroundTerm() of the proper type otherwise. Notice
738 // that the use of mkGroundTerm differs from the rewriter which uses
739 // mkGroundValue in this case.
744 // ----------------------------------------
745 // Conclusion: (or ((_ is C1) t) ... ((_ is Cn) t))
748 // Children: (P1:((_ is Ci) t), P2: ((_ is Cj) t))
750 // ----------------------------------------
754 // ======== Datatype Trust
755 // Children: (P1 ... Pn)
757 // ---------------------
761 //================================================= Quantifiers rules
762 // ======== Witness intro
763 // Children: (P:(exists ((x T)) F[x]))
765 // ----------------------------------------
766 // Conclusion: (= k (witness ((x T)) F[x]))
767 // where k is the Skolem form of (witness ((x T)) F[x]).
769 // ======== Exists intro
770 // Children: (P:F[t])
771 // Arguments: ((exists ((x T)) F[x]))
772 // ----------------------------------------
773 // Conclusion: (exists ((x T)) F[x])
774 // This rule verifies that F[x] indeed matches F[t] with a substitution
777 // ======== Skolemize
778 // Children: (P:(exists ((x1 T1) ... (xn Tn)) F))
780 // ----------------------------------------
781 // Conclusion: F*sigma
782 // sigma maps x1 ... xn to their representative skolems obtained by
783 // SkolemManager::mkSkolemize, returned in the skolems argument of that
784 // method. Alternatively, can use negated forall as a premise.
786 // ======== Instantiate
787 // Children: (P:(forall ((x1 T1) ... (xn Tn)) F))
788 // Arguments: (t1 ... tn)
789 // ----------------------------------------
790 // Conclusion: F*sigma
791 // sigma maps x1 ... xn to t1 ... tn.
794 //================================================= String rules
795 //======================== Core solver
796 // ======== Concat eq
797 // Children: (P1:(= (str.++ t1 ... tn t) (str.++ t1 ... tn s)))
798 // Arguments: (b), indicating if reverse direction
799 // ---------------------
800 // Conclusion: (= t s)
802 // Notice that t or s may be empty, in which case they are implicit in the
803 // concatenation above. For example, if
804 // P1 concludes (= x (str.++ x z)), then
805 // (CONCAT_EQ P1 :args false) concludes (= "" z)
807 // Also note that constants are split, such that if
808 // P1 concludes (= (str.++ "abc" x) (str.++ "a" y)), then
809 // (CONCAT_EQ P1 :args false) concludes (= (str.++ "bc" x) y)
810 // This splitting is done only for constants such that Word::splitConstant
813 // ======== Concat unify
814 // Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)),
815 // P2:(= (str.len t1) (str.len s1)))
816 // Arguments: (b), indicating if reverse direction
817 // ---------------------
818 // Conclusion: (= t1 s1)
820 // ======== Concat conflict
821 // Children: (P1:(= (str.++ c1 t) (str.++ c2 s)))
822 // Arguments: (b), indicating if reverse direction
823 // ---------------------
825 // Where c1, c2 are constants such that Word::splitConstant(c1,c2,index,b)
826 // is null, in other words, neither is a prefix of the other.
828 // ======== Concat split
829 // Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)),
830 // P2:(not (= (str.len t1) (str.len s1))))
831 // Arguments: (false)
832 // ---------------------
833 // Conclusion: (or (= t1 (str.++ s1 r_t)) (= s1 (str.++ t1 r_s)))
835 // r_t = (witness ((z String)) (= z (suf t1 (str.len s1)))),
836 // r_s = (witness ((z String)) (= z (suf s1 (str.len t1)))).
838 // or the reverse form of the above:
840 // Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)),
841 // P2:(not (= (str.len t2) (str.len s2))))
843 // ---------------------
844 // Conclusion: (or (= t2 (str.++ r_t s2)) (= s2 (str.++ r_s t2)))
846 // r_t = (witness ((z String)) (= z (pre t2 (- (str.len t2) (str.len
847 // s2))))), r_s = (witness ((z String)) (= z (pre s2 (- (str.len s2)
850 // Above, (suf x n) is shorthand for (str.substr x n (- (str.len x) n)) and
851 // (pre x n) is shorthand for (str.substr x 0 n).
853 // ======== Concat constant split
854 // Children: (P1:(= (str.++ t1 t2) (str.++ c s2)),
855 // P2:(not (= (str.len t1) 0)))
856 // Arguments: (false)
857 // ---------------------
858 // Conclusion: (= t1 (str.++ c r))
860 // r = (witness ((z String)) (= z (suf t1 1))).
862 // or the reverse form of the above:
864 // Children: (P1:(= (str.++ t1 t2) (str.++ s1 c)),
865 // P2:(not (= (str.len t2) 0)))
867 // ---------------------
868 // Conclusion: (= t2 (str.++ r c))
870 // r = (witness ((z String)) (= z (pre t2 (- (str.len t2) 1)))).
872 // ======== Concat length propagate
873 // Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)),
874 // P2:(> (str.len t1) (str.len s1)))
875 // Arguments: (false)
876 // ---------------------
877 // Conclusion: (= t1 (str.++ s1 r_t))
879 // r_t = (witness ((z String)) (= z (suf t1 (str.len s1))))
881 // or the reverse form of the above:
883 // Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)),
884 // P2:(> (str.len t2) (str.len s2)))
885 // Arguments: (false)
886 // ---------------------
887 // Conclusion: (= t2 (str.++ r_t s2))
889 // r_t = (witness ((z String)) (= z (pre t2 (- (str.len t2) (str.len
892 // ======== Concat constant propagate
893 // Children: (P1:(= (str.++ t1 w1 t2) (str.++ w2 s)),
894 // P2:(not (= (str.len t1) 0)))
895 // Arguments: (false)
896 // ---------------------
897 // Conclusion: (= t1 (str.++ w3 r))
899 // w1, w2, w3, w4 are words,
902 // p = Word::overlap((suf w2 1), w1),
903 // r = (witness ((z String)) (= z (suf t1 (str.len w3)))).
904 // In other words, w4 is the largest suffix of (suf w2 1) that can contain a
905 // prefix of w1; since t1 is non-empty, w3 must therefore be contained in t1.
907 // or the reverse form of the above:
909 // Children: (P1:(= (str.++ t1 w1 t2) (str.++ s w2)),
910 // P2:(not (= (str.len t2) 0)))
912 // ---------------------
913 // Conclusion: (= t2 (str.++ r w3))
915 // w1, w2, w3, w4 are words,
916 // w3 is (suf w2 (- (str.len w2) p)),
917 // w4 is (pre w2 (- (str.len w2) p)),
918 // p = Word::roverlap((pre w2 (- (str.len w2) 1)), w1),
919 // r = (witness ((z String)) (= z (pre t2 (- (str.len t2) (str.len w3))))).
920 // In other words, w4 is the largest prefix of (pre w2 (- (str.len w2) 1))
921 // that can contain a suffix of w1; since t2 is non-empty, w3 must therefore
922 // be contained in t2.
924 // ======== String decompose
925 // Children: (P1: (>= (str.len t) n)
926 // Arguments: (false)
927 // ---------------------
928 // Conclusion: (and (= t (str.++ w1 w2)) (= (str.len w1) n))
930 // Children: (P1: (>= (str.len t) n)
932 // ---------------------
933 // Conclusion: (and (= t (str.++ w1 w2)) (= (str.len w2) n))
935 // w1 is (witness ((z String)) (= z (pre t n)))
936 // w2 is (witness ((z String)) (= z (suf t n)))
938 // ======== Length positive
941 // ---------------------
942 // Conclusion: (or (and (= (str.len t) 0) (= t "")) (> (str.len t 0)))
944 // ======== Length non-empty
945 // Children: (P1:(not (= t "")))
947 // ---------------------
948 // Conclusion: (not (= (str.len t) 0))
949 STRING_LENGTH_NON_EMPTY
,
950 //======================== Extended functions
951 // ======== Reduction
954 // ---------------------
955 // Conclusion: (and R (= t w))
956 // where w = strings::StringsPreprocess::reduce(t, R, ...).
957 // In other words, R is the reduction predicate for extended term t, and w is
958 // (witness ((z T)) (= z t))
959 // Notice that the free variables of R are w and the free variables of t.
961 // ======== Eager Reduction
963 // Arguments: (t, id?)
964 // ---------------------
966 // where R = strings::TermRegistry::eagerReduce(t, id).
967 STRING_EAGER_REDUCTION
,
968 //======================== Regular expressions
969 // ======== Regular expression intersection
970 // Children: (P:(str.in.re t R1), P:(str.in.re t R2))
972 // ---------------------
973 // Conclusion: (str.in.re t (re.inter R1 R2)).
975 // ======== Regular expression unfold positive
976 // Children: (P:(str.in.re t R))
978 // ---------------------
979 // Conclusion:(RegExpOpr::reduceRegExpPos((str.in.re t R))),
980 // corresponding to the one-step unfolding of the premise.
982 // ======== Regular expression unfold negative
983 // Children: (P:(not (str.in.re t R)))
985 // ---------------------
986 // Conclusion:(RegExpOpr::reduceRegExpNeg((not (str.in.re t R)))),
987 // corresponding to the one-step unfolding of the premise.
989 // ======== Regular expression unfold negative concat fixed
990 // Children: (P:(not (str.in.re t R)))
992 // ---------------------
993 // Conclusion:(RegExpOpr::reduceRegExpNegConcatFixed((not (str.in.re t
994 // R)),L,i)) where RegExpOpr::getRegExpConcatFixed((not (str.in.re t R)), i) =
995 // L. corresponding to the one-step unfolding of the premise, optimized for
996 // fixed length of component i of the regular expression concatenation R.
997 RE_UNFOLD_NEG_CONCAT_FIXED
,
998 // ======== Regular expression elimination
1000 // Arguments: (F, b)
1001 // ---------------------
1002 // Conclusion: (= F strings::RegExpElimination::eliminate(F, b))
1003 // where b is a Boolean indicating whether we are using aggressive
1004 // eliminations. Notice this rule concludes (= F F) if no eliminations
1005 // are performed for F.
1007 //======================== Code points
1009 // Arguments: (t, s)
1010 // ---------------------
1011 // Conclusion:(or (= (str.code t) (- 1))
1012 // (not (= (str.code t) (str.code s)))
1015 //======================== Sequence unit
1016 // Children: (P:(= (seq.unit x) (seq.unit y)))
1018 // ---------------------
1019 // Conclusion:(= x y)
1020 // Also applies to the case where (seq.unit y) is a constant sequence
1022 STRING_SEQ_UNIT_INJ
,
1023 // ======== String Trust
1026 // ---------------------
1030 //================================================= Arithmetic rules
1031 // ======== Adding Inequalities
1032 // Note: an ArithLiteral is a term of the form (>< poly const)
1034 // >< is >=, >, ==, <, <=, or not(== ...).
1035 // poly is a polynomial
1036 // const is a rational constant
1038 // Children: (P1:l1, ..., Pn:ln)
1039 // where each li is an ArithLiteral
1040 // not(= ...) is dis-allowed!
1042 // Arguments: (k1, ..., kn), non-zero reals
1043 // ---------------------
1044 // Conclusion: (>< (* k t1) (* k t2))
1045 // where >< is the fusion of the combination of the ><i, (flipping each it
1046 // its ki is negative). >< is always one of <, <=
1047 // NB: this implies that lower bounds must have negative ki,
1048 // and upper bounds must have positive ki.
1049 // t1 is the sum of the polynomials.
1050 // t2 is the sum of the constants.
1051 ARITH_SCALE_SUM_UPPER_BOUNDS
,
1053 // ======== Tightening Strict Integer Upper Bounds
1054 // Children: (P:(< i c))
1055 // where i has integer type.
1057 // ---------------------
1058 // Conclusion: (<= i greatestIntLessThan(c)})
1061 // ======== Tightening Strict Integer Lower Bounds
1062 // Children: (P:(> i c))
1063 // where i has integer type.
1065 // ---------------------
1066 // Conclusion: (>= i leastIntGreaterThan(c)})
1069 // ======== Trichotomy of the reals
1072 // ---------------------
1074 // where (not A) (not B) and C
1075 // are (> x c) (< x c) and (= x c)
1077 // note that "not" here denotes arithmetic negation, flipping
1081 // ======== Arithmetic operator elimination
1084 // ---------------------
1085 // Conclusion: arith::OperatorElim::getAxiomFor(t)
1086 ARITH_OP_ELIM_AXIOM
,
1088 // ======== Int Trust
1089 // Children: (P1 ... Pn)
1091 // ---------------------
1095 //======== Multiplication tangent plane
1097 // Arguments: (t, x, y, a, b, sgn)
1098 // ---------------------
1100 // sgn=-1: (= (<= t tplane) (or (and (<= x a) (>= y b)) (and (>= x a) (<= y b)))
1101 // sgn= 1: (= (>= t tplane) (or (and (<= x a) (<= y b)) (and (>= x a) (>= y b)))
1102 // Where x,y are real terms (variables or extended terms), t = (* x y)
1103 // (possibly under rewriting), a,b are real constants, and sgn is either -1
1104 // or 1. tplane is the tangent plane of x*y at (a,b): b*x + a*y - a*b
1107 //================================================= Unknown rule
1112 * Converts a proof rule to a string. Note: This function is also used in
1113 * `safe_print()`. Changing this function name or signature will result in
1114 * `safe_print()` printing "<unsupported>" instead of the proper strings for
1117 * @param id The proof rule
1118 * @return The name of the proof rule
1120 const char* toString(PfRule id
);
1123 * Writes a proof rule name to a stream.
1125 * @param out The stream to write to
1126 * @param id The proof rule to write to the stream
1127 * @return The stream
1129 std::ostream
& operator<<(std::ostream
& out
, PfRule id
);
1131 /** Hash function for proof rules */
1132 struct PfRuleHashFunction
1134 size_t operator()(PfRule id
) const;
1135 }; /* struct PfRuleHashFunction */
1139 #endif /* CVC4__EXPR__PROOF_RULE_H */