1 /********************* */
4 ** Top contributors (to current version):
5 ** Haniel Barbosa, Andrew Reynolds
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.
94 // ======== Substitution + Rewriting equality introduction
96 // In this rule, we provide a term t and conclude that it is equal to its
97 // rewritten form under a (proven) substitution.
99 // Children: (P1:F1, ..., Pn:Fn)
100 // Arguments: (t, (ids (idr)?)?)
101 // ---------------------------------------------------------------
102 // Conclusion: (= t t')
105 // Rewriter{idr}(t*sigma{ids}(Fn)*...*sigma{ids}(F1))
107 // In other words, from the point of view of Skolem forms, this rule
108 // transforms t to t' by standard substitution + rewriting.
110 // The argument ids and idr is optional and specify the identifier of the
111 // substitution and rewriter respectively to be used. For details, see
112 // theory/builtin/proof_checker.h.
114 // ======== Substitution + Rewriting predicate introduction
116 // In this rule, we provide a formula F and conclude it, under the condition
117 // that it rewrites to true under a proven substitution.
119 // Children: (P1:F1, ..., Pn:Fn)
120 // Arguments: (F, (ids (idr)?)?)
121 // ---------------------------------------------------------------
124 // Rewriter{idr}(toWitness(F)*sigma{ids}(Fn)*...*sigma{ids}(F1)) == true
125 // where ids and idr are method identifiers.
127 // Notice that we apply rewriting on the witness form of F, meaning that this
128 // rule may conclude an F whose Skolem form is justified by the definition of
129 // its (fresh) Skolem variables. Furthermore, notice that the rewriting and
130 // substitution is applied only within the side condition, meaning the
131 // rewritten form of the witness form of F does not escape this rule.
133 // ======== Substitution + Rewriting predicate elimination
135 // In this rule, if we have proven a formula F, then we may conclude its
136 // rewritten form under a proven substitution.
138 // Children: (P1:F, P2:F1, ..., P_{n+1}:Fn)
139 // Arguments: ((ids (idr)?)?)
140 // ----------------------------------------
144 // Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)).
145 // where ids and idr are method identifiers.
147 // We rewrite only on the Skolem form of F, similar to MACRO_SR_EQ_INTRO.
149 // ======== Substitution + Rewriting predicate transform
151 // In this rule, if we have proven a formula F, then we may provide a formula
152 // G and conclude it if F and G are equivalent after rewriting under a proven
155 // Children: (P1:F, P2:F1, ..., P_{n+1}:Fn)
156 // Arguments: (G, (ids (idr)?)?)
157 // ----------------------------------------
160 // Rewriter{idr}(toWitness(F)*sigma{ids}(Fn)*...*sigma{ids}(F1)) ==
161 // Rewriter{idr}(toWitness(G)*sigma{ids}(Fn)*...*sigma{ids}(F1))
163 // Notice that we apply rewriting on the witness form of F and G, similar to
164 // MACRO_SR_PRED_INTRO.
165 MACRO_SR_PRED_TRANSFORM
,
166 // ======== Theory Rewrite
168 // Arguments: (t, preRewrite?)
169 // ----------------------------------------
170 // Conclusion: (= t t')
172 // t' is the result of applying either a pre-rewrite or a post-rewrite step
173 // to t (depending on the second argument).
176 //================================================= Processing rules
177 // ======== Remove Term Formulas Axiom
180 // ---------------------------------------------------------------
181 // Conclusion: RemoveTermFormulas::getAxiomFor(t).
182 REMOVE_TERM_FORMULA_AXIOM
,
184 //================================================= Trusted rules
185 // The rules in this section have the signature of a "trusted rule":
189 // ---------------------------------------------------------------
192 // where F is an equality of the form t = t' where t was replaced by t'
193 // based on some preprocessing pass, or otherwise F was added as a new
194 // assertion by some preprocessing pass.
196 // where F was added as a new assertion by some preprocessing pass.
198 // where F is an equality of the form t = Theory::ppRewrite(t) for some
199 // theory. Notice this is a "trusted" rule.
201 // where F was added as a new assertion by theory preprocessing.
202 THEORY_PREPROCESS_LEMMA
,
203 // where F is an existential (exists ((x T)) (P x)) used for introducing
204 // a witness term (witness ((x T)) (P x)).
207 //================================================= Boolean rules
211 // ---------------------
212 // Conclusion: (or F (not F))
214 // ======== Equality resolution
215 // Children: (P1:F1, P2:(= F1 F2))
217 // ---------------------
219 // Note this can optionally be seen as a macro for EQUIV_ELIM1+RESOLUTION.
221 // ======== And elimination
222 // Children: (P:(and F1 ... Fn))
224 // ---------------------
227 // ======== And introduction
228 // Children: (P1:F1 ... Pn:Fn))
230 // ---------------------
231 // Conclusion: (and P1 ... Pn)
233 // ======== Not Or elimination
234 // Children: (P:(not (or F1 ... Fn)))
236 // ---------------------
237 // Conclusion: (not Fi)
239 // ======== Implication elimination
240 // Children: (P:(=> F1 F2))
242 // ---------------------
243 // Conclusion: (or (not F1) F2)
245 // ======== Not Implication elimination version 1
246 // Children: (P:(not (=> F1 F2)))
248 // ---------------------
251 // ======== Not Implication elimination version 2
252 // Children: (P:(not (=> F1 F2)))
254 // ---------------------
255 // Conclusion: (not F2)
257 // ======== Equivalence elimination version 1
258 // Children: (P:(= F1 F2))
260 // ---------------------
261 // Conclusion: (or (not F1) F2)
263 // ======== Equivalence elimination version 2
264 // Children: (P:(= F1 F2))
266 // ---------------------
267 // Conclusion: (or F1 (not F2))
269 // ======== Not Equivalence elimination version 1
270 // Children: (P:(not (= F1 F2)))
272 // ---------------------
273 // Conclusion: (or F1 F2)
275 // ======== Not Equivalence elimination version 2
276 // Children: (P:(not (= F1 F2)))
278 // ---------------------
279 // Conclusion: (or (not F1) (not F2))
281 // ======== XOR elimination version 1
282 // Children: (P:(xor F1 F2)))
284 // ---------------------
285 // Conclusion: (or F1 F2)
287 // ======== XOR elimination version 2
288 // Children: (P:(xor F1 F2)))
290 // ---------------------
291 // Conclusion: (or (not F1) (not F2))
293 // ======== Not XOR elimination version 1
294 // Children: (P:(not (xor F1 F2)))
296 // ---------------------
297 // Conclusion: (or F1 (not F2))
299 // ======== Not XOR elimination version 2
300 // Children: (P:(not (xor F1 F2)))
302 // ---------------------
303 // Conclusion: (or (not F1) F2)
305 // ======== ITE elimination version 1
306 // Children: (P:(ite C F1 F2))
308 // ---------------------
309 // Conclusion: (or (not C) F1)
311 // ======== ITE elimination version 2
312 // Children: (P:(ite C F1 F2))
314 // ---------------------
315 // Conclusion: (or C F2)
317 // ======== Not ITE elimination version 1
318 // Children: (P:(not (ite C F1 F2)))
320 // ---------------------
321 // Conclusion: (or (not C) (not F1))
323 // ======== Not ITE elimination version 1
324 // Children: (P:(not (ite C F1 F2)))
326 // ---------------------
327 // Conclusion: (or C (not F2))
329 // ======== Not ITE elimination version 1
330 // Children: (P1:P P2:(not P))
332 // ---------------------
333 // Conclusion: (false)
336 //================================================= De Morgan rules
338 // Children: (P:(not (and F1 ... Fn))
340 // ---------------------
341 // Conclusion: (or (not F1) ... (not Fn))
343 //================================================= CNF rules
344 // ======== CNF And Pos
346 // Arguments: ((and F1 ... Fn), i)
347 // ---------------------
348 // Conclusion: (or (not (and F1 ... Fn)) Fi)
350 // ======== CNF And Neg
352 // Arguments: ((and F1 ... Fn))
353 // ---------------------
354 // Conclusion: (or (and F1 ... Fn) (not F1) ... (not Fn))
356 // ======== CNF Or Pos
358 // Arguments: ((or F1 ... Fn))
359 // ---------------------
360 // Conclusion: (or (not (or F1 ... Fn)) F1 ... Fn)
362 // ======== CNF Or Neg
364 // Arguments: ((or F1 ... Fn), i)
365 // ---------------------
366 // Conclusion: (or (or F1 ... Fn) (not Fi))
368 // ======== CNF Implies Pos
370 // Arguments: ((implies F1 F2))
371 // ---------------------
372 // Conclusion: (or (not (implies F1 F2)) (not F1) F2)
374 // ======== CNF Implies Neg version 1
376 // Arguments: ((implies F1 F2))
377 // ---------------------
378 // Conclusion: (or (implies F1 F2) F1)
380 // ======== CNF Implies Neg version 2
382 // Arguments: ((implies F1 F2))
383 // ---------------------
384 // Conclusion: (or (implies F1 F2) (not F2))
386 // ======== CNF Equiv Pos version 1
388 // Arguments: ((= F1 F2))
389 // ---------------------
390 // Conclusion: (or (not (= F1 F2)) (not F1) F2)
392 // ======== CNF Equiv Pos version 2
394 // Arguments: ((= F1 F2))
395 // ---------------------
396 // Conclusion: (or (not (= F1 F2)) F1 (not F2))
398 // ======== CNF Equiv Neg version 1
400 // Arguments: ((= F1 F2))
401 // ---------------------
402 // Conclusion: (or (= F1 F2) F1 F2)
404 // ======== CNF Equiv Neg version 2
406 // Arguments: ((= F1 F2))
407 // ---------------------
408 // Conclusion: (or (= F1 F2) (not F1) (not F2))
410 // ======== CNF Xor Pos version 1
412 // Arguments: ((xor F1 F2))
413 // ---------------------
414 // Conclusion: (or (not (xor F1 F2)) F1 F2)
416 // ======== CNF Xor Pos version 2
418 // Arguments: ((xor F1 F2))
419 // ---------------------
420 // Conclusion: (or (not (xor F1 F2)) (not F1) (not F2))
422 // ======== CNF Xor Neg version 1
424 // Arguments: ((xor F1 F2))
425 // ---------------------
426 // Conclusion: (or (xor F1 F2) (not F1) F2)
428 // ======== CNF Xor Neg version 2
430 // Arguments: ((xor F1 F2))
431 // ---------------------
432 // Conclusion: (or (xor F1 F2) F1 (not F2))
434 // ======== CNF ITE Pos version 1
436 // Arguments: ((ite C F1 F2))
437 // ---------------------
438 // Conclusion: (or (not (ite C F1 F2)) (not C) F1)
440 // ======== CNF ITE Pos version 2
442 // Arguments: ((ite C F1 F2))
443 // ---------------------
444 // Conclusion: (or (not (ite C F1 F2)) C F2)
446 // ======== CNF ITE Pos version 3
448 // Arguments: ((ite C F1 F2))
449 // ---------------------
450 // Conclusion: (or (not (ite C F1 F2)) F1 F2)
452 // ======== CNF ITE Neg version 1
454 // Arguments: ((ite C F1 F2))
455 // ---------------------
456 // Conclusion: (or (ite C F1 F2) (not C) (not F1))
458 // ======== CNF ITE Neg version 2
460 // Arguments: ((ite C F1 F2))
461 // ---------------------
462 // Conclusion: (or (ite C F1 F2) C (not F2))
464 // ======== CNF ITE Neg version 3
466 // Arguments: ((ite C F1 F2))
467 // ---------------------
468 // Conclusion: (or (ite C F1 F2) (not F1) (not F2))
471 //================================================= Equality rules
472 // ======== Reflexive
475 // ---------------------
476 // Conclusion: (= t t)
478 // ======== Symmetric
479 // Children: (P:(= t1 t2)) or (P:(not (= t1 t2)))
481 // -----------------------
482 // Conclusion: (= t2 t1) or (not (= t2 t1))
484 // ======== Transitivity
485 // Children: (P1:(= t1 t2), ..., Pn:(= t{n-1} tn))
487 // -----------------------
488 // Conclusion: (= t1 tn)
490 // ======== Congruence
491 // Children: (P1:(= t1 s1), ..., Pn:(= tn sn))
492 // Arguments: (<kind> f?)
493 // ---------------------------------------------
494 // Conclusion: (= (<kind> f? t1 ... tn) (<kind> f? s1 ... sn))
495 // Notice that f must be provided iff <kind> is a parameterized kind, e.g.
496 // APPLY_UF. The actual node for <kind> is constructible via
497 // ProofRuleChecker::mkKindNode.
499 // ======== True intro
502 // ----------------------------------------
503 // Conclusion: (= F true)
505 // ======== True elim
506 // Children: (P:(= F true)
508 // ----------------------------------------
511 // ======== False intro
512 // Children: (P:(not F))
514 // ----------------------------------------
515 // Conclusion: (= F false)
517 // ======== False elim
518 // Children: (P:(= F false)
520 // ----------------------------------------
521 // Conclusion: (not F)
526 // ---------------------
527 // Conclusion: (= t TheoryUfRewriter::getHoApplyForApplyUf(t))
528 // For example, this rule concludes (f x y) = (HO_APPLY (HO_APPLY f x) y)
530 // ======== Congruence
531 // Children: (P1:(= f g), P2:(= t1 s1), ..., Pn+1:(= tn sn))
533 // ---------------------------------------------
534 // Conclusion: (= (f t1 ... tn) (g s1 ... sn))
535 // Notice that this rule is only used when the application kinds are APPLY_UF.
538 //================================================= Quantifiers rules
539 // ======== Witness intro
540 // Children: (P:F[t])
542 // ----------------------------------------
543 // Conclusion: (= t (witness ((x T)) F[x]))
544 // where x is a BOUND_VARIABLE unique to the pair F,t.
546 // ======== Exists intro
547 // Children: (P:F[t])
549 // ----------------------------------------
550 // Conclusion: (exists ((x T)) F[x])
551 // where x is a BOUND_VARIABLE unique to the pair F,t.
553 // ======== Skolemize
554 // Children: (P:(exists ((x1 T1) ... (xn Tn)) F))
556 // ----------------------------------------
557 // Conclusion: F*sigma
558 // sigma maps x1 ... xn to their representative skolems obtained by
559 // SkolemManager::mkSkolemize, returned in the skolems argument of that
562 // ======== Instantiate
563 // Children: (P:(forall ((x1 T1) ... (xn Tn)) F))
564 // Arguments: (t1 ... tn)
565 // ----------------------------------------
566 // Conclusion: F*sigma
567 // sigma maps x1 ... xn to t1 ... tn.
570 //================================================= String rules
571 //======================== Core solver
572 // ======== Concat eq
573 // Children: (P1:(= (str.++ t1 ... tn t) (str.++ t1 ... tn s)))
574 // Arguments: (b), indicating if reverse direction
575 // ---------------------
576 // Conclusion: (= t s)
578 // Notice that t or s may be empty, in which case they are implicit in the
579 // concatenation above. For example, if
580 // P1 concludes (= x (str.++ x z)), then
581 // (CONCAT_EQ P1 :args false) concludes (= "" z)
583 // Also note that constants are split, such that if
584 // P1 concludes (= (str.++ "abc" x) (str.++ "a" y)), then
585 // (CONCAT_EQ P1 :args false) concludes (= (str.++ "bc" x) y)
586 // This splitting is done only for constants such that Word::splitConstant
589 // ======== Concat unify
590 // Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)),
591 // P2:(= (str.len t1) (str.len s1)))
592 // Arguments: (b), indicating if reverse direction
593 // ---------------------
594 // Conclusion: (= t1 s1)
596 // ======== Concat conflict
597 // Children: (P1:(= (str.++ c1 t) (str.++ c2 s)))
598 // Arguments: (b), indicating if reverse direction
599 // ---------------------
601 // Where c1, c2 are constants such that Word::splitConstant(c1,c2,index,b)
602 // is null, in other words, neither is a prefix of the other.
604 // ======== Concat split
605 // Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)),
606 // P2:(not (= (str.len t1) (str.len s1))))
607 // Arguments: (false)
608 // ---------------------
609 // Conclusion: (or (= t1 (str.++ s1 r_t)) (= s1 (str.++ t1 r_s)))
611 // r_t = (witness ((z String)) (= z (suf t1 (str.len s1)))),
612 // r_s = (witness ((z String)) (= z (suf s1 (str.len t1)))).
614 // or the reverse form of the above:
616 // Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)),
617 // P2:(not (= (str.len t2) (str.len s2))))
619 // ---------------------
620 // Conclusion: (or (= t2 (str.++ r_t s2)) (= s2 (str.++ r_s t2)))
622 // r_t = (witness ((z String)) (= z (pre t2 (- (str.len t2) (str.len
623 // s2))))), r_s = (witness ((z String)) (= z (pre s2 (- (str.len s2)
626 // Above, (suf x n) is shorthand for (str.substr x n (- (str.len x) n)) and
627 // (pre x n) is shorthand for (str.substr x 0 n).
629 // ======== Concat constant split
630 // Children: (P1:(= (str.++ t1 t2) (str.++ c s2)),
631 // P2:(not (= (str.len t1) 0)))
632 // Arguments: (false)
633 // ---------------------
634 // Conclusion: (= t1 (str.++ c r))
636 // r = (witness ((z String)) (= z (suf t1 1))).
638 // or the reverse form of the above:
640 // Children: (P1:(= (str.++ t1 t2) (str.++ s1 c)),
641 // P2:(not (= (str.len t2) 0)))
643 // ---------------------
644 // Conclusion: (= t2 (str.++ r c))
646 // r = (witness ((z String)) (= z (pre t2 (- (str.len t2) 1)))).
648 // ======== Concat length propagate
649 // Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)),
650 // P2:(> (str.len t1) (str.len s1)))
651 // Arguments: (false)
652 // ---------------------
653 // Conclusion: (= t1 (str.++ s1 r_t))
655 // r_t = (witness ((z String)) (= z (suf t1 (str.len s1))))
657 // or the reverse form of the above:
659 // Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)),
660 // P2:(> (str.len t2) (str.len s2)))
661 // Arguments: (false)
662 // ---------------------
663 // Conclusion: (= t2 (str.++ r_t s2))
665 // r_t = (witness ((z String)) (= z (pre t2 (- (str.len t2) (str.len
668 // ======== Concat constant propagate
669 // Children: (P1:(= (str.++ t1 w1 t2) (str.++ w2 s)),
670 // P2:(not (= (str.len t1) 0)))
671 // Arguments: (false)
672 // ---------------------
673 // Conclusion: (= t1 (str.++ w3 r))
675 // w1, w2, w3, w4 are words,
678 // p = Word::overlap((suf w2 1), w1),
679 // r = (witness ((z String)) (= z (suf t1 (str.len w3)))).
680 // In other words, w4 is the largest suffix of (suf w2 1) that can contain a
681 // prefix of w1; since t1 is non-empty, w3 must therefore be contained in t1.
683 // or the reverse form of the above:
685 // Children: (P1:(= (str.++ t1 w1 t2) (str.++ s w2)),
686 // P2:(not (= (str.len t2) 0)))
688 // ---------------------
689 // Conclusion: (= t2 (str.++ r w3))
691 // w1, w2, w3, w4 are words,
692 // w3 is (suf w2 (- (str.len w2) p)),
693 // w4 is (pre w2 (- (str.len w2) p)),
694 // p = Word::roverlap((pre w2 (- (str.len w2) 1)), w1),
695 // r = (witness ((z String)) (= z (pre t2 (- (str.len t2) (str.len w3))))).
696 // In other words, w4 is the largest prefix of (pre w2 (- (str.len w2) 1))
697 // that can contain a suffix of w1; since t2 is non-empty, w3 must therefore
698 // be contained in t2.
700 // ======== String decompose
701 // Children: (P1: (>= (str.len t) n)
702 // Arguments: (false)
703 // ---------------------
704 // Conclusion: (and (= t (str.++ w1 w2)) (= (str.len w1) n))
706 // Children: (P1: (>= (str.len t) n)
708 // ---------------------
709 // Conclusion: (and (= t (str.++ w1 w2)) (= (str.len w2) n))
711 // w1 is (witness ((z String)) (= z (pre t n)))
712 // w2 is (witness ((z String)) (= z (suf t n)))
714 // ======== Length positive
717 // ---------------------
718 // Conclusion: (or (and (= (str.len t) 0) (= t "")) (> (str.len t 0)))
720 // ======== Length non-empty
721 // Children: (P1:(not (= t "")))
723 // ---------------------
724 // Conclusion: (not (= (str.len t) 0))
725 STRING_LENGTH_NON_EMPTY
,
726 //======================== Extended functions
727 // ======== Reduction
730 // ---------------------
731 // Conclusion: (and R (= t w))
732 // where w = strings::StringsPreprocess::reduce(t, R, ...).
733 // In other words, R is the reduction predicate for extended term t, and w is
734 // (witness ((z T)) (= z t))
735 // Notice that the free variables of R are w and the free variables of t.
737 // ======== Eager Reduction
739 // Arguments: (t, id?)
740 // ---------------------
742 // where R = strings::TermRegistry::eagerReduce(t, id).
743 STRING_EAGER_REDUCTION
,
744 //======================== Regular expressions
745 // ======== Regular expression intersection
746 // Children: (P:(str.in.re t R1), P:(str.in.re t R2))
748 // ---------------------
749 // Conclusion: (str.in.re t (re.inter R1 R2)).
751 // ======== Regular expression unfold positive
752 // Children: (P:(str.in.re t R))
754 // ---------------------
755 // Conclusion:(RegExpOpr::reduceRegExpPos((str.in.re t R))),
756 // corresponding to the one-step unfolding of the premise.
758 // ======== Regular expression unfold negative
759 // Children: (P:(not (str.in.re t R)))
761 // ---------------------
762 // Conclusion:(RegExpOpr::reduceRegExpNeg((not (str.in.re t R)))),
763 // corresponding to the one-step unfolding of the premise.
765 // ======== Regular expression unfold negative concat fixed
766 // Children: (P:(not (str.in.re t R)))
768 // ---------------------
769 // Conclusion:(RegExpOpr::reduceRegExpNegConcatFixed((not (str.in.re t
770 // R)),L,i)) where RegExpOpr::getRegExpConcatFixed((not (str.in.re t R)), i) =
771 // L. corresponding to the one-step unfolding of the premise, optimized for
772 // fixed length of component i of the regular expression concatenation R.
773 RE_UNFOLD_NEG_CONCAT_FIXED
,
774 // ======== Regular expression elimination
777 // ---------------------
779 // where R = strings::RegExpElimination::eliminate(F).
781 //======================== Code points
784 // ---------------------
785 // Conclusion:(or (= (str.code t) (- 1))
786 // (not (= (str.code t) (str.code s)))
789 //======================== Sequence unit
790 // Children: (P:(= (seq.unit x) (seq.unit y)))
792 // ---------------------
793 // Conclusion:(= x y)
794 // Also applies to the case where (seq.unit y) is a constant sequence
797 // ======== String Trust
800 // ---------------------
804 //================================================= Arithmetic rules
805 // ======== Adding Inequalities
806 // Note: an ArithLiteral is a term of the form (>< poly const)
808 // >< is >=, >, ==, <, <=, or not(== ...).
809 // poly is a polynomial
810 // const is a rational constant
812 // Children: (P1:l1, ..., Pn:ln)
813 // where each li is an ArithLiteral
814 // not(= ...) is dis-allowed!
816 // Arguments: (k1, ..., kn), non-zero reals
817 // ---------------------
818 // Conclusion: (>< (* k t1) (* k t2))
819 // where >< is the fusion of the combination of the ><i, (flipping each it
820 // its ki is negative). >< is always one of <, <=
821 // NB: this implies that lower bounds must have negative ki,
822 // and upper bounds must have positive ki.
823 // t1 is the sum of the polynomials.
824 // t2 is the sum of the constants.
825 ARITH_SCALE_SUM_UPPER_BOUNDS
,
827 // ======== Tightening Strict Integer Upper Bounds
828 // Children: (P:(< i c))
829 // where i has integer type.
831 // ---------------------
832 // Conclusion: (<= i greatestIntLessThan(c)})
835 // ======== Tightening Strict Integer Lower Bounds
836 // Children: (P:(> i c))
837 // where i has integer type.
839 // ---------------------
840 // Conclusion: (>= i leastIntGreaterThan(c)})
843 // ======== Trichotomy of the reals
846 // ---------------------
848 // where (not A) (not B) and C
849 // are (> x c) (< x c) and (= x c)
851 // note that "not" here denotes arithmetic negation, flipping
855 // ======== Arithmetic operator elimination
858 // ---------------------
859 // Conclusion: arith::OperatorElim::getAxiomFor(t)
862 // ======== Int Trust
863 // Children: (P1 ... Pn)
865 // ---------------------
869 //================================================= Unknown rule
874 * Converts a proof rule to a string. Note: This function is also used in
875 * `safe_print()`. Changing this function name or signature will result in
876 * `safe_print()` printing "<unsupported>" instead of the proper strings for
879 * @param id The proof rule
880 * @return The name of the proof rule
882 const char* toString(PfRule id
);
885 * Writes a proof rule name to a stream.
887 * @param out The stream to write to
888 * @param id The proof rule to write to the stream
891 std::ostream
& operator<<(std::ostream
& out
, PfRule id
);
893 /** Hash function for proof rules */
894 struct PfRuleHashFunction
896 size_t operator()(PfRule id
) const;
897 }; /* struct PfRuleHashFunction */
901 #endif /* CVC4__EXPR__PROOF_RULE_H */