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 "cvc5_private.h"
18 #ifndef CVC5__PROOF__PROOF_RULE_H
19 #define CVC5__PROOF__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 * Rules with prefix MACRO_ are those that can be defined in terms of other
46 * rules. These exist for convienience. We provide their definition in the line
49 enum class PfRule
: uint32_t
51 //================================================= Core rules
52 //======================== Assume and Scope
53 // ======== Assumption (a leaf)
59 // This rule has special status, in that an application of assume is an
60 // open leaf in a proof that is not (yet) justified. An assume leaf is
61 // analogous to a free variable in a term, where we say "F is a free
62 // assumption in proof P" if it contains an application of F that is not
63 // bound by SCOPE (see below).
65 // ======== Scope (a binder for assumptions)
67 // Arguments: (F1, ..., Fn)
69 // Conclusion: (=> (and F1 ... Fn) F) or (not (and F1 ... Fn)) if F is false
71 // This rule has a dual purpose with ASSUME. It is a way to close
72 // assumptions in a proof. We require that F1 ... Fn are free assumptions in
73 // P and say that F1, ..., Fn are not free in (SCOPE P). In other words, they
74 // are bound by this application. For example, the proof node:
75 // (SCOPE (ASSUME F) :args F)
76 // has the conclusion (=> F F) and has no free assumptions. More generally, a
77 // proof with no free assumptions always concludes a valid formula.
80 //======================== Builtin theory (common node operations)
81 // ======== Substitution
82 // Children: (P1:F1, ..., Pn:Fn)
83 // Arguments: (t, (ids)?)
84 // ---------------------------------------------------------------
85 // Conclusion: (= t t*sigma{ids}(Fn)*...*sigma{ids}(F1))
86 // where sigma{ids}(Fi) are substitutions, which notice are applied in
88 // Notice that ids is a MethodId identifier, which determines how to convert
89 // the formulas F1, ..., Fn into substitutions.
93 // Arguments: (t, (idr)?)
94 // ----------------------------------------
95 // Conclusion: (= t Rewriter{idr}(t))
96 // where idr is a MethodId identifier, which determines the kind of rewriter
97 // to apply, e.g. Rewriter::rewrite.
102 // ----------------------------------------
103 // Conclusion: (= t Evaluator::evaluate(t))
104 // Note this is equivalent to:
105 // (REWRITE t MethodId::RW_EVALUATE)
107 // ======== Substitution + Rewriting equality introduction
109 // In this rule, we provide a term t and conclude that it is equal to its
110 // rewritten form under a (proven) substitution.
112 // Children: (P1:F1, ..., Pn:Fn)
113 // Arguments: (t, (ids (ida (idr)?)?)?)
114 // ---------------------------------------------------------------
115 // Conclusion: (= t t')
118 // Rewriter{idr}(t*sigma{ids, ida}(Fn)*...*sigma{ids, ida}(F1))
120 // In other words, from the point of view of Skolem forms, this rule
121 // transforms t to t' by standard substitution + rewriting.
123 // The arguments ids, ida and idr are optional and specify the identifier of
124 // the substitution, the substitution application and rewriter respectively to
125 // be used. For details, see theory/builtin/proof_checker.h.
127 // ======== Substitution + Rewriting predicate introduction
129 // In this rule, we provide a formula F and conclude it, under the condition
130 // that it rewrites to true under a proven substitution.
132 // Children: (P1:F1, ..., Pn:Fn)
133 // Arguments: (F, (ids (ida (idr)?)?)?)
134 // ---------------------------------------------------------------
137 // Rewriter{idr}(F*sigma{ids, ida}(Fn)*...*sigma{ids, ida}(F1)) == true
138 // where ids and idr are method identifiers.
140 // More generally, this rule also holds when:
141 // Rewriter::rewrite(toOriginal(F')) == true
142 // where F' is the result of the left hand side of the equality above. Here,
143 // notice that we apply rewriting on the original form of F', meaning that
144 // this rule may conclude an F whose Skolem form is justified by the
145 // definition of its (fresh) Skolem variables. For example, this rule may
146 // justify the conclusion (= k t) where k is the purification Skolem for t,
147 // e.g. where the original form of k is t.
149 // Furthermore, notice that the rewriting and substitution is applied only
150 // within the side condition, meaning the rewritten form of the original form
151 // of F does not escape this rule.
153 // ======== Substitution + Rewriting predicate elimination
155 // In this rule, if we have proven a formula F, then we may conclude its
156 // rewritten form under a proven substitution.
158 // Children: (P1:F, P2:F1, ..., P_{n+1}:Fn)
159 // Arguments: ((ids (ida (idr)?)?)?)
160 // ----------------------------------------
164 // Rewriter{idr}(F*sigma{ids, ida}(Fn)*...*sigma{ids, ida}(F1)).
165 // where ids and idr are method identifiers.
167 // We rewrite only on the Skolem form of F, similar to MACRO_SR_EQ_INTRO.
169 // ======== Substitution + Rewriting predicate transform
171 // In this rule, if we have proven a formula F, then we may provide a formula
172 // G and conclude it if F and G are equivalent after rewriting under a proven
175 // Children: (P1:F, P2:F1, ..., P_{n+1}:Fn)
176 // Arguments: (G, (ids (ida (idr)?)?)?)
177 // ----------------------------------------
180 // Rewriter{idr}(F*sigma{ids, ida}(Fn)*...*sigma{ids, ida}(F1)) ==
181 // Rewriter{idr}(G*sigma{ids, ida}(Fn)*...*sigma{ids, ida}(F1))
183 // More generally, this rule also holds when:
184 // Rewriter::rewrite(toOriginal(F')) == Rewriter::rewrite(toOriginal(G'))
185 // where F' and G' are the result of each side of the equation above. Here,
186 // original forms are used in a similar manner to MACRO_SR_PRED_INTRO above.
187 MACRO_SR_PRED_TRANSFORM
,
188 //================================================= Processing rules
189 // ======== Remove Term Formulas Axiom
192 // ---------------------------------------------------------------
193 // Conclusion: RemoveTermFormulas::getAxiomFor(t).
194 REMOVE_TERM_FORMULA_AXIOM
,
196 //================================================= Trusted rules
197 // ======== Theory lemma
199 // Arguments: (F, tid)
200 // ---------------------------------------------------------------
202 // where F is a (T-valid) theory lemma generated by theory with TheoryId tid.
203 // This is a "coarse-grained" rule that is used as a placeholder if a theory
204 // did not provide a proof for a lemma or conflict.
206 // ======== Theory Rewrite
208 // Arguments: (F, tid, rid)
209 // ----------------------------------------
211 // where F is an equality of the form (= t t') where t' is obtained by
212 // applying the kind of rewriting given by the method identifier rid, which
214 // { RW_REWRITE_THEORY_PRE, RW_REWRITE_THEORY_POST, RW_REWRITE_EQ_EXT }
215 // Notice that the checker for this rule does not replay the rewrite to ensure
216 // correctness, since theory rewriter methods are not static. For example,
217 // the quantifiers rewriter involves constructing new bound variables that are
218 // not guaranteed to be consistent on each call.
220 // The remaining rules in this section have the signature of a "trusted rule":
224 // ---------------------------------------------------------------
227 // Unless stated below, the expected children vector of the rule is empty.
229 // where F is an equality of the form t = t' where t was replaced by t'
230 // based on some preprocessing pass, or otherwise F was added as a new
231 // assertion by some preprocessing pass.
233 // where F was added as a new assertion by some preprocessing pass.
235 // where F is an equality of the form t = Theory::ppRewrite(t) for some
236 // theory. Notice this is a "trusted" rule.
238 // where F was added as a new assertion by theory preprocessing.
239 THEORY_PREPROCESS_LEMMA
,
240 // where F is an equality of the form t = t' where t was replaced by t'
241 // based on theory expand definitions.
243 // where F is an existential (exists ((x T)) (P x)) used for introducing
244 // a witness term (witness ((x T)) (P x)).
246 // where F is an equality (= t t') that holds by a form of rewriting that
247 // could not be replayed during proof postprocessing.
249 // where F is an equality (= t t') that holds by a form of substitution that
250 // could not be replayed during proof postprocessing.
252 // where F is an equality (= t t') that holds by a form of substitution that
253 // could not be determined by the TrustSubstitutionMap. This inference may
254 // contain possibly multiple children corresponding to the formulas used to
255 // derive the substitution.
257 // where F is a solved equality of the form (= x t) derived as the solved
258 // form of F', where F' is given as a child.
260 // where F is a fact derived by a theory-specific inference
262 // ========= SAT Refutation for assumption-based unsat cores
263 // Children: (P1, ..., Pn)
265 // ---------------------
267 // Note: P1, ..., Pn correspond to the unsat core determined by the SAT
271 //================================================= Boolean rules
272 // ======== Resolution
275 // Arguments: (pol, L)
276 // ---------------------
279 // - C1 and C2 are nodes viewed as clauses, i.e., either an OR node with
280 // each children viewed as a literal or a node viewed as a literal. Note
281 // that an OR node could also be a literal.
282 // - pol is either true or false, representing the polarity of the pivot on
284 // - L is the pivot of the resolution, which occurs as is (resp. under a
285 // NOT) in C1 and negatively (as is) in C2 if pol = true (pol = false).
286 // C is a clause resulting from collecting all the literals in C1, minus the
287 // first occurrence of the pivot or its negation, and C2, minus the first
288 // occurrence of the pivot or its negation, according to the policy above.
289 // If the resulting clause has a single literal, that literal itself is the
290 // result; if it has no literals, then the result is false; otherwise it's
291 // an OR node of the resulting literals.
293 // Note that it may be the case that the pivot does not occur in the
294 // clauses. In this case the rule is not unsound, but it does not correspond
295 // to resolution but rather to a weakening of the clause that did not have a
296 // literal eliminated.
298 // ======== N-ary Resolution
299 // Children: (P1:C_1, ..., Pm:C_n)
300 // Arguments: (pol_1, L_1, ..., pol_{n-1}, L_{n-1})
301 // ---------------------
304 // - let C_1 ... C_n be nodes viewed as clauses, as defined above
305 // - let "C_1 <>_{L,pol} C_2" represent the resolution of C_1 with C_2 with
306 // pivot L and polarity pol, as defined above
307 // - let C_1' = C_1 (from P1),
308 // - for each i > 1, let C_i' = C_{i-1} <>_{L_{i-1}, pol_{i-1}} C_i'
309 // The result of the chain resolution is C = C_n'
311 // ======== Factoring
314 // ---------------------
317 // Set representations of C1 and C2 is the same and the number of literals in
318 // C2 is smaller than that of C1
320 // ======== Reordering
323 // ---------------------
326 // Set representations of C1 and C2 are the same and the number of literals
327 // in C2 is the same of that of C1
329 // ======== N-ary Resolution + Factoring + Reordering
330 // Children: (P1:C_1, ..., Pm:C_n)
331 // Arguments: (C, pol_1, L_1, ..., pol_{n-1}, L_{n-1})
332 // ---------------------
335 // - let C_1 ... C_n be nodes viewed as clauses, as defined in RESOLUTION
336 // - let "C_1 <>_{L,pol} C_2" represent the resolution of C_1 with C_2 with
337 // pivot L and polarity pol, as defined in RESOLUTION
338 // - let C_1' be equal, in its set representation, to C_1 (from P1),
339 // - for each i > 1, let C_i' be equal, it its set representation, to
340 // C_{i-1} <>_{L_{i-1}, pol_{i-1}} C_i'
341 // The result of the chain resolution is C, which is equal, in its set
342 // representation, to C_n'
344 // As above but not checked
345 MACRO_RESOLUTION_TRUST
,
350 // ---------------------
351 // Conclusion: (or F (not F))
353 // ======== Equality resolution
354 // Children: (P1:F1, P2:(= F1 F2))
356 // ---------------------
358 // Note this can optionally be seen as a macro for EQUIV_ELIM1+RESOLUTION.
360 // ======== Modus ponens
361 // Children: (P1:F1, P2:(=> F1 F2))
363 // ---------------------
365 // Note this can optionally be seen as a macro for IMPLIES_ELIM+RESOLUTION.
367 // ======== Double negation elimination
368 // Children: (P:(not (not F)))
370 // ---------------------
373 // ======== Contradiction
374 // Children: (P1:F P2:(not F))
376 // ---------------------
379 // ======== And elimination
380 // Children: (P:(and F1 ... Fn))
382 // ---------------------
385 // ======== And introduction
386 // Children: (P1:F1 ... Pn:Fn))
388 // ---------------------
389 // Conclusion: (and P1 ... Pn)
391 // ======== Not Or elimination
392 // Children: (P:(not (or F1 ... Fn)))
394 // ---------------------
395 // Conclusion: (not Fi)
397 // ======== Implication elimination
398 // Children: (P:(=> F1 F2))
400 // ---------------------
401 // Conclusion: (or (not F1) F2)
403 // ======== Not Implication elimination version 1
404 // Children: (P:(not (=> F1 F2)))
406 // ---------------------
409 // ======== Not Implication elimination version 2
410 // Children: (P:(not (=> F1 F2)))
412 // ---------------------
413 // Conclusion: (not F2)
415 // ======== Equivalence elimination version 1
416 // Children: (P:(= F1 F2))
418 // ---------------------
419 // Conclusion: (or (not F1) F2)
421 // ======== Equivalence elimination version 2
422 // Children: (P:(= F1 F2))
424 // ---------------------
425 // Conclusion: (or F1 (not F2))
427 // ======== Not Equivalence elimination version 1
428 // Children: (P:(not (= F1 F2)))
430 // ---------------------
431 // Conclusion: (or F1 F2)
433 // ======== Not Equivalence elimination version 2
434 // Children: (P:(not (= F1 F2)))
436 // ---------------------
437 // Conclusion: (or (not F1) (not F2))
439 // ======== XOR elimination version 1
440 // Children: (P:(xor F1 F2)))
442 // ---------------------
443 // Conclusion: (or F1 F2)
445 // ======== XOR elimination version 2
446 // Children: (P:(xor F1 F2)))
448 // ---------------------
449 // Conclusion: (or (not F1) (not F2))
451 // ======== Not XOR elimination version 1
452 // Children: (P:(not (xor F1 F2)))
454 // ---------------------
455 // Conclusion: (or F1 (not F2))
457 // ======== Not XOR elimination version 2
458 // Children: (P:(not (xor F1 F2)))
460 // ---------------------
461 // Conclusion: (or (not F1) F2)
463 // ======== ITE elimination version 1
464 // Children: (P:(ite C F1 F2))
466 // ---------------------
467 // Conclusion: (or (not C) F1)
469 // ======== ITE elimination version 2
470 // Children: (P:(ite C F1 F2))
472 // ---------------------
473 // Conclusion: (or C F2)
475 // ======== Not ITE elimination version 1
476 // Children: (P:(not (ite C F1 F2)))
478 // ---------------------
479 // Conclusion: (or (not C) (not F1))
481 // ======== Not ITE elimination version 1
482 // Children: (P:(not (ite C F1 F2)))
484 // ---------------------
485 // Conclusion: (or C (not F2))
488 //================================================= De Morgan rules
490 // Children: (P:(not (and F1 ... Fn))
492 // ---------------------
493 // Conclusion: (or (not F1) ... (not Fn))
495 //================================================= CNF rules
496 // ======== CNF And Pos
498 // Arguments: ((and F1 ... Fn), i)
499 // ---------------------
500 // Conclusion: (or (not (and F1 ... Fn)) Fi)
502 // ======== CNF And Neg
504 // Arguments: ((and F1 ... Fn))
505 // ---------------------
506 // Conclusion: (or (and F1 ... Fn) (not F1) ... (not Fn))
508 // ======== CNF Or Pos
510 // Arguments: ((or F1 ... Fn))
511 // ---------------------
512 // Conclusion: (or (not (or F1 ... Fn)) F1 ... Fn)
514 // ======== CNF Or Neg
516 // Arguments: ((or F1 ... Fn), i)
517 // ---------------------
518 // Conclusion: (or (or F1 ... Fn) (not Fi))
520 // ======== CNF Implies Pos
522 // Arguments: ((implies F1 F2))
523 // ---------------------
524 // Conclusion: (or (not (implies F1 F2)) (not F1) F2)
526 // ======== CNF Implies Neg version 1
528 // Arguments: ((implies F1 F2))
529 // ---------------------
530 // Conclusion: (or (implies F1 F2) F1)
532 // ======== CNF Implies Neg version 2
534 // Arguments: ((implies F1 F2))
535 // ---------------------
536 // Conclusion: (or (implies F1 F2) (not F2))
538 // ======== CNF Equiv Pos version 1
540 // Arguments: ((= F1 F2))
541 // ---------------------
542 // Conclusion: (or (not (= F1 F2)) (not F1) F2)
544 // ======== CNF Equiv Pos version 2
546 // Arguments: ((= F1 F2))
547 // ---------------------
548 // Conclusion: (or (not (= F1 F2)) F1 (not F2))
550 // ======== CNF Equiv Neg version 1
552 // Arguments: ((= F1 F2))
553 // ---------------------
554 // Conclusion: (or (= F1 F2) F1 F2)
556 // ======== CNF Equiv Neg version 2
558 // Arguments: ((= F1 F2))
559 // ---------------------
560 // Conclusion: (or (= F1 F2) (not F1) (not F2))
562 // ======== CNF Xor Pos version 1
564 // Arguments: ((xor F1 F2))
565 // ---------------------
566 // Conclusion: (or (not (xor F1 F2)) F1 F2)
568 // ======== CNF Xor Pos version 2
570 // Arguments: ((xor F1 F2))
571 // ---------------------
572 // Conclusion: (or (not (xor F1 F2)) (not F1) (not F2))
574 // ======== CNF Xor Neg version 1
576 // Arguments: ((xor F1 F2))
577 // ---------------------
578 // Conclusion: (or (xor F1 F2) (not F1) F2)
580 // ======== CNF Xor Neg version 2
582 // Arguments: ((xor F1 F2))
583 // ---------------------
584 // Conclusion: (or (xor F1 F2) F1 (not F2))
586 // ======== CNF ITE Pos version 1
588 // Arguments: ((ite C F1 F2))
589 // ---------------------
590 // Conclusion: (or (not (ite C F1 F2)) (not C) F1)
592 // ======== CNF ITE Pos version 2
594 // Arguments: ((ite C F1 F2))
595 // ---------------------
596 // Conclusion: (or (not (ite C F1 F2)) C F2)
598 // ======== CNF ITE Pos version 3
600 // Arguments: ((ite C F1 F2))
601 // ---------------------
602 // Conclusion: (or (not (ite C F1 F2)) F1 F2)
604 // ======== CNF ITE Neg version 1
606 // Arguments: ((ite C F1 F2))
607 // ---------------------
608 // Conclusion: (or (ite C F1 F2) (not C) (not F1))
610 // ======== CNF ITE Neg version 2
612 // Arguments: ((ite C F1 F2))
613 // ---------------------
614 // Conclusion: (or (ite C F1 F2) C (not F2))
616 // ======== CNF ITE Neg version 3
618 // Arguments: ((ite C F1 F2))
619 // ---------------------
620 // Conclusion: (or (ite C F1 F2) (not F1) (not F2))
623 //================================================= Equality rules
624 // ======== Reflexive
627 // ---------------------
628 // Conclusion: (= t t)
630 // ======== Symmetric
631 // Children: (P:(= t1 t2)) or (P:(not (= t1 t2)))
633 // -----------------------
634 // Conclusion: (= t2 t1) or (not (= t2 t1))
636 // ======== Transitivity
637 // Children: (P1:(= t1 t2), ..., Pn:(= t{n-1} tn))
639 // -----------------------
640 // Conclusion: (= t1 tn)
642 // ======== Congruence
643 // Children: (P1:(= t1 s1), ..., Pn:(= tn sn))
644 // Arguments: (<kind> f?)
645 // ---------------------------------------------
646 // Conclusion: (= (<kind> f? t1 ... tn) (<kind> f? s1 ... sn))
647 // Notice that f must be provided iff <kind> is a parameterized kind, e.g.
648 // APPLY_UF. The actual node for <kind> is constructible via
649 // ProofRuleChecker::mkKindNode.
651 // ======== True intro
654 // ----------------------------------------
655 // Conclusion: (= F true)
657 // ======== True elim
658 // Children: (P:(= F true))
660 // ----------------------------------------
663 // ======== False intro
664 // Children: (P:(not F))
666 // ----------------------------------------
667 // Conclusion: (= F false)
669 // ======== False elim
670 // Children: (P:(= F false))
672 // ----------------------------------------
673 // Conclusion: (not F)
678 // ---------------------
679 // Conclusion: (= t TheoryUfRewriter::getHoApplyForApplyUf(t))
680 // For example, this rule concludes (f x y) = (HO_APPLY (HO_APPLY f x) y)
682 // ======== Congruence
683 // Children: (P1:(= f g), P2:(= t1 s1), ..., Pn+1:(= tn sn))
685 // ---------------------------------------------
686 // Conclusion: (= (f t1 ... tn) (g s1 ... sn))
687 // Notice that this rule is only used when the application kinds are APPLY_UF.
690 //================================================= Array rules
691 // ======== Read over write
692 // Children: (P:(not (= i1 i2)))
693 // Arguments: ((select (store a i1 e) i2))
694 // ----------------------------------------
695 // Conclusion: (= (select (store a i1 e) i2) (select a i2))
696 ARRAYS_READ_OVER_WRITE
,
697 // ======== Read over write, contrapositive
698 // Children: (P:(not (= (select (store a i2 e) i1) (select a i1)))
700 // ----------------------------------------
701 // Conclusion: (= i1 i2)
702 ARRAYS_READ_OVER_WRITE_CONTRA
,
703 // ======== Read over write 1
705 // Arguments: ((select (store a i e) i))
706 // ----------------------------------------
707 // Conclusion: (= (select (store a i e) i) e)
708 ARRAYS_READ_OVER_WRITE_1
,
709 // ======== Extensionality
710 // Children: (P:(not (= a b)))
712 // ----------------------------------------
713 // Conclusion: (not (= (select a k) (select b k)))
714 // where k is arrays::SkolemCache::getExtIndexSkolem((not (= a b))).
716 // ======== Array Trust
717 // Children: (P1 ... Pn)
719 // ---------------------
723 //================================================= Bit-Vector rules
724 // Note: bitblast() represents the result of the bit-blasted term as a
725 // bit-vector consisting of the output bits of the bit-blasted circuit
726 // representation of the term. Terms are bit-blasted according to the
727 // strategies defined in
728 // theory/bv/bitblast/bitblast_strategies_template.h.
732 // ---------------------
733 // Conclusion: (= t bitblast(t))
735 // ======== Bitblast Bit-Vector Constant, Variable
737 // Arguments: (= t bitblast(t))
738 // ---------------------
739 // Conclusion: (= t bitblast(t))
740 // ======== Bitblast Bit-Vector Terms
742 // Arguments: (= (KIND bitblast(child_1) ... bitblast(child_n)) bitblast(t))
743 // ---------------------
744 // Conclusion: (= (KIND bitblast(child_1) ... bitblast(child_n)) bitblast(t))
747 // ======== Eager Atom
750 // ---------------------
751 // Conclusion: (= F F[0])
752 // where F is of kind BITVECTOR_EAGER_ATOM
755 //================================================= Datatype rules
756 // ======== Unification
757 // Children: (P:(= (C t1 ... tn) (C s1 ... sn)))
759 // ----------------------------------------
760 // Conclusion: (= ti si)
761 // where C is a constructor.
763 // ======== Instantiate
766 // ----------------------------------------
767 // Conclusion: (= ((_ is C) t) (= t (C (sel_1 t) ... (sel_n t))))
768 // where C is the n^th constructor of the type of T, and (_ is C) is the
769 // discriminator (tester) for C.
773 // Arguments: ((sel_i (C_j t_1 ... t_n)))
774 // ----------------------------------------
775 // Conclusion: (= (sel_i (C_j t_1 ... t_n)) r)
776 // where C_j is a constructor, r is t_i if sel_i is a correctly applied
777 // selector, or TypeNode::mkGroundTerm() of the proper type otherwise. Notice
778 // that the use of mkGroundTerm differs from the rewriter which uses
779 // mkGroundValue in this case.
784 // ----------------------------------------
785 // Conclusion: (or ((_ is C1) t) ... ((_ is Cn) t))
788 // Children: (P1:((_ is Ci) t), P2: ((_ is Cj) t))
790 // ----------------------------------------
794 // ======== Datatype Trust
795 // Children: (P1 ... Pn)
797 // ---------------------
801 //================================================= Quantifiers rules
802 // ======== Skolem intro
805 // ----------------------------------------
806 // Conclusion: (= k t)
807 // where t is the original form of skolem k.
809 // ======== Exists intro
810 // Children: (P:F[t])
811 // Arguments: ((exists ((x T)) F[x]))
812 // ----------------------------------------
813 // Conclusion: (exists ((x T)) F[x])
814 // This rule verifies that F[x] indeed matches F[t] with a substitution
817 // ======== Skolemize
818 // Children: (P:(exists ((x1 T1) ... (xn Tn)) F))
820 // ----------------------------------------
821 // Conclusion: F*sigma
822 // sigma maps x1 ... xn to their representative skolems obtained by
823 // SkolemManager::mkSkolemize, returned in the skolems argument of that
824 // method. Alternatively, can use negated forall as a premise. The witness
825 // terms for the returned skolems can be obtained by
826 // SkolemManager::getWitnessForm.
828 // ======== Instantiate
829 // Children: (P:(forall ((x1 T1) ... (xn Tn)) F))
830 // Arguments: (t1 ... tn)
831 // ----------------------------------------
832 // Conclusion: F*sigma
833 // sigma maps x1 ... xn to t1 ... tn.
835 // ======== (Trusted) quantifiers preprocess
838 // ---------------------------------------------------------------
840 // where F is an equality of the form t = QuantifiersRewriter::preprocess(t)
841 QUANTIFIERS_PREPROCESS
,
843 //================================================= String rules
844 //======================== Core solver
845 // ======== Concat eq
846 // Children: (P1:(= (str.++ t1 ... tn t) (str.++ t1 ... tn s)))
847 // Arguments: (b), indicating if reverse direction
848 // ---------------------
849 // Conclusion: (= t s)
851 // Notice that t or s may be empty, in which case they are implicit in the
852 // concatenation above. For example, if
853 // P1 concludes (= x (str.++ x z)), then
854 // (CONCAT_EQ P1 :args false) concludes (= "" z)
856 // Also note that constants are split, such that if
857 // P1 concludes (= (str.++ "abc" x) (str.++ "a" y)), then
858 // (CONCAT_EQ P1 :args false) concludes (= (str.++ "bc" x) y)
859 // This splitting is done only for constants such that Word::splitConstant
862 // ======== Concat unify
863 // Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)),
864 // P2:(= (str.len t1) (str.len s1)))
865 // Arguments: (b), indicating if reverse direction
866 // ---------------------
867 // Conclusion: (= t1 s1)
869 // ======== Concat conflict
870 // Children: (P1:(= (str.++ c1 t) (str.++ c2 s)))
871 // Arguments: (b), indicating if reverse direction
872 // ---------------------
874 // Where c1, c2 are constants such that Word::splitConstant(c1,c2,index,b)
875 // is null, in other words, neither is a prefix of the other.
877 // ======== Concat split
878 // Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)),
879 // P2:(not (= (str.len t1) (str.len s1))))
880 // Arguments: (false)
881 // ---------------------
882 // Conclusion: (or (= t1 (str.++ s1 r_t)) (= s1 (str.++ t1 r_s)))
884 // r_t = (skolem (suf t1 (str.len s1)))),
885 // r_s = (skolem (suf s1 (str.len t1)))).
887 // or the reverse form of the above:
889 // Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)),
890 // P2:(not (= (str.len t2) (str.len s2))))
892 // ---------------------
893 // Conclusion: (or (= t2 (str.++ r_t s2)) (= s2 (str.++ r_s t2)))
895 // r_t = (skolem (pre t2 (- (str.len t2) (str.len s2))))),
896 // r_s = (skolem (pre s2 (- (str.len s2) (str.len t2))))).
898 // Above, (suf x n) is shorthand for (str.substr x n (- (str.len x) n)) and
899 // (pre x n) is shorthand for (str.substr x 0 n).
901 // ======== Concat constant split
902 // Children: (P1:(= (str.++ t1 t2) (str.++ c s2)),
903 // P2:(not (= (str.len t1) 0)))
904 // Arguments: (false)
905 // ---------------------
906 // Conclusion: (= t1 (str.++ c r))
908 // r = (skolem (suf t1 1)).
910 // or the reverse form of the above:
912 // Children: (P1:(= (str.++ t1 t2) (str.++ s1 c)),
913 // P2:(not (= (str.len t2) 0)))
915 // ---------------------
916 // Conclusion: (= t2 (str.++ r c))
918 // r = (skolem (pre t2 (- (str.len t2) 1))).
920 // ======== Concat length propagate
921 // Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)),
922 // P2:(> (str.len t1) (str.len s1)))
923 // Arguments: (false)
924 // ---------------------
925 // Conclusion: (= t1 (str.++ s1 r_t))
927 // r_t = (skolem (suf t1 (str.len s1)))
929 // or the reverse form of the above:
931 // Children: (P1:(= (str.++ t1 t2) (str.++ s1 s2)),
932 // P2:(> (str.len t2) (str.len s2)))
933 // Arguments: (false)
934 // ---------------------
935 // Conclusion: (= t2 (str.++ r_t s2))
937 // r_t = (skolem (pre t2 (- (str.len t2) (str.len s2)))).
939 // ======== Concat constant propagate
940 // Children: (P1:(= (str.++ t1 w1 t2) (str.++ w2 s)),
941 // P2:(not (= (str.len t1) 0)))
942 // Arguments: (false)
943 // ---------------------
944 // Conclusion: (= t1 (str.++ w3 r))
946 // w1, w2, w3, w4 are words,
949 // p = Word::overlap((suf w2 1), w1),
950 // r = (skolem (suf t1 (str.len w3))).
951 // In other words, w4 is the largest suffix of (suf w2 1) that can contain a
952 // prefix of w1; since t1 is non-empty, w3 must therefore be contained in t1.
954 // or the reverse form of the above:
956 // Children: (P1:(= (str.++ t1 w1 t2) (str.++ s w2)),
957 // P2:(not (= (str.len t2) 0)))
959 // ---------------------
960 // Conclusion: (= t2 (str.++ r w3))
962 // w1, w2, w3, w4 are words,
963 // w3 is (suf w2 (- (str.len w2) p)),
964 // w4 is (pre w2 (- (str.len w2) p)),
965 // p = Word::roverlap((pre w2 (- (str.len w2) 1)), w1),
966 // r = (skolem (pre t2 (- (str.len t2) (str.len w3)))).
967 // In other words, w4 is the largest prefix of (pre w2 (- (str.len w2) 1))
968 // that can contain a suffix of w1; since t2 is non-empty, w3 must therefore
969 // be contained in t2.
971 // ======== String decompose
972 // Children: (P1: (>= (str.len t) n)
973 // Arguments: (false)
974 // ---------------------
975 // Conclusion: (and (= t (str.++ w1 w2)) (= (str.len w1) n))
977 // Children: (P1: (>= (str.len t) n)
979 // ---------------------
980 // Conclusion: (and (= t (str.++ w1 w2)) (= (str.len w2) n))
982 // w1 is (skolem (pre t n))
983 // w2 is (skolem (suf t n))
985 // ======== Length positive
988 // ---------------------
989 // Conclusion: (or (and (= (str.len t) 0) (= t "")) (> (str.len t) 0))
991 // ======== Length non-empty
992 // Children: (P1:(not (= t "")))
994 // ---------------------
995 // Conclusion: (not (= (str.len t) 0))
996 STRING_LENGTH_NON_EMPTY
,
997 //======================== Extended functions
998 // ======== Reduction
1001 // ---------------------
1002 // Conclusion: (and R (= t w))
1003 // where w = strings::StringsPreprocess::reduce(t, R, ...).
1004 // In other words, R is the reduction predicate for extended term t, and w is
1006 // Notice that the free variables of R are w and the free variables of t.
1008 // ======== Eager Reduction
1011 // ---------------------
1013 // where R = strings::TermRegistry::eagerReduce(t).
1014 STRING_EAGER_REDUCTION
,
1015 //======================== Regular expressions
1016 // ======== Regular expression intersection
1017 // Children: (P:(str.in.re t R1), P:(str.in.re t R2))
1019 // ---------------------
1020 // Conclusion: (str.in.re t (re.inter R1 R2)).
1022 // ======== Regular expression unfold positive
1023 // Children: (P:(str.in.re t R))
1025 // ---------------------
1026 // Conclusion:(RegExpOpr::reduceRegExpPos((str.in.re t R))),
1027 // corresponding to the one-step unfolding of the premise.
1029 // ======== Regular expression unfold negative
1030 // Children: (P:(not (str.in.re t R)))
1032 // ---------------------
1033 // Conclusion:(RegExpOpr::reduceRegExpNeg((not (str.in.re t R)))),
1034 // corresponding to the one-step unfolding of the premise.
1036 // ======== Regular expression unfold negative concat fixed
1037 // Children: (P:(not (str.in.re t R)))
1039 // ---------------------
1040 // Conclusion:(RegExpOpr::reduceRegExpNegConcatFixed((not (str.in.re t
1041 // R)),L,i)) where RegExpOpr::getRegExpConcatFixed((not (str.in.re t R)), i) =
1042 // L. corresponding to the one-step unfolding of the premise, optimized for
1043 // fixed length of component i of the regular expression concatenation R.
1044 RE_UNFOLD_NEG_CONCAT_FIXED
,
1045 // ======== Regular expression elimination
1047 // Arguments: (F, b)
1048 // ---------------------
1049 // Conclusion: (= F strings::RegExpElimination::eliminate(F, b))
1050 // where b is a Boolean indicating whether we are using aggressive
1051 // eliminations. Notice this rule concludes (= F F) if no eliminations
1052 // are performed for F.
1054 //======================== Code points
1056 // Arguments: (t, s)
1057 // ---------------------
1058 // Conclusion:(or (= (str.code t) (- 1))
1059 // (not (= (str.code t) (str.code s)))
1062 //======================== Sequence unit
1063 // Children: (P:(= (seq.unit x) (seq.unit y)))
1065 // ---------------------
1066 // Conclusion:(= x y)
1067 // Also applies to the case where (seq.unit y) is a constant sequence
1069 STRING_SEQ_UNIT_INJ
,
1070 // ======== String Trust
1073 // ---------------------
1077 //================================================= Arithmetic rules
1078 // ======== Adding Inequalities
1079 // Note: an ArithLiteral is a term of the form (>< poly const)
1081 // >< is >=, >, ==, <, <=, or not(== ...).
1082 // poly is a polynomial
1083 // const is a rational constant
1085 // Children: (P1:l1, ..., Pn:ln)
1086 // where each li is an ArithLiteral
1087 // not(= ...) is dis-allowed!
1089 // Arguments: (k1, ..., kn), non-zero reals
1090 // ---------------------
1091 // Conclusion: (>< t1 t2)
1092 // where >< is the fusion of the combination of the ><i, (flipping each it
1093 // its ki is negative). >< is always one of <, <=
1094 // NB: this implies that lower bounds must have negative ki,
1095 // and upper bounds must have positive ki.
1096 // t1 is the sum of the scaled polynomials (k_1 * poly_1 + ... + k_n *
1097 // poly_n) t2 is the sum of the scaled constants (k_1 * const_1 + ... + k_n
1099 MACRO_ARITH_SCALE_SUM_UB
,
1100 // ======== Sum Upper Bounds
1101 // Children: (P1, ... , Pn)
1102 // where each Pi has form (><i, Li, Ri)
1103 // for ><i in {<, <=, ==}
1104 // Conclusion: (>< L R)
1105 // where >< is < if any ><i is <, and <= otherwise.
1106 // L is (+ L1 ... Ln)
1107 // R is (+ R1 ... Rn)
1109 // ======== Tightening Strict Integer Upper Bounds
1110 // Children: (P:(< i c))
1111 // where i has integer type.
1113 // ---------------------
1114 // Conclusion: (<= i greatestIntLessThan(c)})
1116 // ======== Tightening Strict Integer Lower Bounds
1117 // Children: (P:(> i c))
1118 // where i has integer type.
1120 // ---------------------
1121 // Conclusion: (>= i leastIntGreaterThan(c)})
1123 // ======== Trichotomy of the reals
1126 // ---------------------
1128 // where (not A) (not B) and C
1129 // are (> x c) (< x c) and (= x c)
1131 // note that "not" here denotes arithmetic negation, flipping
1134 // ======== Arithmetic operator elimination
1137 // ---------------------
1138 // Conclusion: arith::OperatorElim::getAxiomFor(t)
1139 ARITH_OP_ELIM_AXIOM
,
1140 // ======== Int Trust
1141 // Children: (P1 ... Pn)
1143 // ---------------------
1147 //======== Multiplication sign inference
1149 // Arguments: (f1, ..., fk, m)
1150 // ---------------------
1151 // Conclusion: (=> (and f1 ... fk) (~ m 0))
1152 // Where f1, ..., fk are variables compared to zero (less, greater or not
1153 // equal), m is a monomial from these variables, and ~ is the comparison (less
1154 // or greater) that results from the signs of the variables. All variables
1155 // with even exponent in m should be given as not equal to zero while all
1156 // variables with odd exponent in m should be given as less or greater than
1159 //======== Multiplication with positive factor
1161 // Arguments: (m, (rel lhs rhs))
1162 // ---------------------
1163 // Conclusion: (=> (and (> m 0) (rel lhs rhs)) (rel (* m lhs) (* m rhs)))
1164 // Where rel is a relation symbol.
1166 //======== Multiplication with negative factor
1168 // Arguments: (m, (rel lhs rhs))
1169 // ---------------------
1170 // Conclusion: (=> (and (< m 0) (rel lhs rhs)) (rel_inv (* m lhs) (* m rhs)))
1171 // Where rel is a relation symbol and rel_inv the inverted relation symbol.
1173 //======== Multiplication tangent plane
1175 // Arguments: (t, x, y, a, b, sgn)
1176 // ---------------------
1178 // sgn=-1: (= (<= t tplane) (or (and (<= x a) (>= y b)) (and (>= x a) (<= y
1179 // b))) sgn= 1: (= (>= t tplane) (or (and (<= x a) (<= y b)) (and (>= x a)
1181 // Where x,y are real terms (variables or extended terms), t = (* x y)
1182 // (possibly under rewriting), a,b are real constants, and sgn is either -1
1183 // or 1. tplane is the tangent plane of x*y at (a,b): b*x + a*y - a*b
1186 // ================ Lemmas for transcendentals
1187 //======== Assert bounds on PI
1189 // Arguments: (l, u)
1190 // ---------------------
1191 // Conclusion: (and (>= real.pi l) (<= real.pi u))
1192 // Where l (u) is a valid lower (upper) bound on pi.
1194 //======== Exp at negative values
1197 // ---------------------
1198 // Conclusion: (= (< t 0) (< (exp t) 1))
1199 ARITH_TRANS_EXP_NEG
,
1200 //======== Exp is always positive
1203 // ---------------------
1204 // Conclusion: (> (exp t) 0)
1205 ARITH_TRANS_EXP_POSITIVITY
,
1206 //======== Exp grows super-linearly for positive values
1209 // ---------------------
1210 // Conclusion: (or (<= t 0) (> exp(t) (+ t 1)))
1211 ARITH_TRANS_EXP_SUPER_LIN
,
1212 //======== Exp at zero
1215 // ---------------------
1216 // Conclusion: (= (= t 0) (= (exp t) 1))
1217 ARITH_TRANS_EXP_ZERO
,
1218 //======== Exp is approximated from above for negative values
1220 // Arguments: (d, t, l, u)
1221 // ---------------------
1222 // Conclusion: (=> (and (>= t l) (<= t u)) (<= (exp t) (secant exp l u t))
1223 // Where d is an even positive number, t an arithmetic term and l (u) a lower
1224 // (upper) bound on t. Let p be the d'th taylor polynomial at zero (also
1225 // called the Maclaurin series) of the exponential function. (secant exp l u
1226 // t) denotes the secant of p from (l, exp(l)) to (u, exp(u)) evaluated at t,
1227 // calculated as follows:
1228 // (p(l) - p(u)) / (l - u) * (t - l) + p(l)
1229 // The lemma states that if t is between l and u, then (exp t) is below the
1230 // secant of p from l to u.
1231 ARITH_TRANS_EXP_APPROX_ABOVE_NEG
,
1232 //======== Exp is approximated from above for positive values
1234 // Arguments: (d, t, l, u)
1235 // ---------------------
1236 // Conclusion: (=> (and (>= t l) (<= t u)) (<= (exp t) (secant-pos exp l u t))
1237 // Where d is an even positive number, t an arithmetic term and l (u) a lower
1238 // (upper) bound on t. Let p* be a modification of the d'th taylor polynomial
1239 // at zero (also called the Maclaurin series) of the exponential function as
1240 // follows where p(d-1) is the regular Maclaurin series of degree d-1:
1241 // p* = p(d-1) * (1 + t^n / n!)
1242 // (secant-pos exp l u t) denotes the secant of p from (l, exp(l)) to (u,
1243 // exp(u)) evaluated at t, calculated as follows:
1244 // (p(l) - p(u)) / (l - u) * (t - l) + p(l)
1245 // The lemma states that if t is between l and u, then (exp t) is below the
1246 // secant of p from l to u.
1247 ARITH_TRANS_EXP_APPROX_ABOVE_POS
,
1248 //======== Exp is approximated from below
1250 // Arguments: (d, t)
1251 // ---------------------
1252 // Conclusion: (>= (exp t) (maclaurin exp d t))
1253 // Where d is an odd positive number and (maclaurin exp d t) is the d'th
1254 // taylor polynomial at zero (also called the Maclaurin series) of the
1255 // exponential function evaluated at t. The Maclaurin series for the
1256 // exponential function is the following:
1257 // e^x = \sum_{n=0}^{\infty} x^n / n!
1258 ARITH_TRANS_EXP_APPROX_BELOW
,
1259 //======== Sine is always between -1 and 1
1262 // ---------------------
1263 // Conclusion: (and (<= (sin t) 1) (>= (sin t) (- 1)))
1264 ARITH_TRANS_SINE_BOUNDS
,
1265 //======== Sine arg shifted to -pi..pi
1267 // Arguments: (x, y, s)
1268 // ---------------------
1271 // (= (sin y) (sin x))
1272 // (ite (<= -pi x pi) (= x y) (= x (+ y (* 2 pi s))))
1274 // Where x is the argument to sine, y is a new real skolem that is x shifted
1275 // into -pi..pi and s is a new integer skolem that is the number of phases y
1277 ARITH_TRANS_SINE_SHIFT
,
1278 //======== Sine is symmetric with respect to negation of the argument
1281 // ---------------------
1282 // Conclusion: (= (- (sin t) (sin (- t))) 0)
1283 ARITH_TRANS_SINE_SYMMETRY
,
1284 //======== Sine is bounded by the tangent at zero
1287 // ---------------------
1289 // (=> (> t 0) (< (sin t) t))
1290 // (=> (< t 0) (> (sin t) t))
1292 ARITH_TRANS_SINE_TANGENT_ZERO
,
1293 //======== Sine is bounded by the tangents at -pi and pi
1296 // ---------------------
1298 // (=> (> t -pi) (> (sin t) (- -pi t)))
1299 // (=> (< t pi) (< (sin t) (- pi t)))
1301 ARITH_TRANS_SINE_TANGENT_PI
,
1302 //======== Sine is approximated from above for negative values
1304 // Arguments: (d, t, lb, ub, l, u)
1305 // ---------------------
1306 // Conclusion: (=> (and (>= t lb) (<= t ub)) (<= (sin t) (secant sin l u t))
1307 // Where d is an even positive number, t an arithmetic term, lb (ub) a
1308 // symbolic lower (upper) bound on t (possibly containing pi) and l (u) the
1309 // evaluated lower (upper) bound on t. Let p be the d'th taylor polynomial at
1310 // zero (also called the Maclaurin series) of the sine function. (secant sin l
1311 // u t) denotes the secant of p from (l, sin(l)) to (u, sin(u)) evaluated at
1312 // t, calculated as follows:
1313 // (p(l) - p(u)) / (l - u) * (t - l) + p(l)
1314 // The lemma states that if t is between l and u, then (sin t) is below the
1315 // secant of p from l to u.
1316 ARITH_TRANS_SINE_APPROX_ABOVE_NEG
,
1317 //======== Sine is approximated from above for positive values
1319 // Arguments: (d, t, c, lb, ub)
1320 // ---------------------
1321 // Conclusion: (=> (and (>= t lb) (<= t ub)) (<= (sin t) (upper sin c))
1322 // Where d is an even positive number, t an arithmetic term, c an arithmetic
1323 // constant, and lb (ub) a symbolic lower (upper) bound on t (possibly
1324 // containing pi). Let p be the d'th taylor polynomial at zero (also called
1325 // the Maclaurin series) of the sine function. (upper sin c) denotes the upper
1326 // bound on sin(c) given by p and lb,ub are such that sin(t) is the maximum of
1327 // the sine function on (lb,ub).
1328 ARITH_TRANS_SINE_APPROX_ABOVE_POS
,
1329 //======== Sine is approximated from below for negative values
1331 // Arguments: (d, t, c, lb, ub)
1332 // ---------------------
1333 // Conclusion: (=> (and (>= t lb) (<= t ub)) (>= (sin t) (lower sin c))
1334 // Where d is an even positive number, t an arithmetic term, c an arithmetic
1335 // constant, and lb (ub) a symbolic lower (upper) bound on t (possibly
1336 // containing pi). Let p be the d'th taylor polynomial at zero (also called
1337 // the Maclaurin series) of the sine function. (lower sin c) denotes the lower
1338 // bound on sin(c) given by p and lb,ub are such that sin(t) is the minimum of
1339 // the sine function on (lb,ub).
1340 ARITH_TRANS_SINE_APPROX_BELOW_NEG
,
1341 //======== Sine is approximated from below for positive values
1343 // Arguments: (d, t, lb, ub, l, u)
1344 // ---------------------
1345 // Conclusion: (=> (and (>= t lb) (<= t ub)) (>= (sin t) (secant sin l u t))
1346 // Where d is an even positive number, t an arithmetic term, lb (ub) a
1347 // symbolic lower (upper) bound on t (possibly containing pi) and l (u) the
1348 // evaluated lower (upper) bound on t. Let p be the d'th taylor polynomial at
1349 // zero (also called the Maclaurin series) of the sine function. (secant sin l
1350 // u t) denotes the secant of p from (l, sin(l)) to (u, sin(u)) evaluated at
1351 // t, calculated as follows:
1352 // (p(l) - p(u)) / (l - u) * (t - l) + p(l)
1353 // The lemma states that if t is between l and u, then (sin t) is above the
1354 // secant of p from l to u.
1355 ARITH_TRANS_SINE_APPROX_BELOW_POS
,
1357 // ================ CAD Lemmas
1358 // We use IRP for IndexedRootPredicate.
1360 // A formula "Interval" describes that a variable (xn is none is given) is
1361 // within a particular interval whose bounds are given as IRPs. It is either
1362 // an open interval or a point interval:
1363 // (IRP k poly) < xn < (IRP k poly)
1364 // xn == (IRP k poly)
1366 // A formula "Cell" describes a portion
1367 // of the real space in the following form:
1368 // Interval(x1) and Interval(x2) and ...
1369 // We implicitly assume a Cell to go up to n-1 (and can be empty).
1371 // A formula "Covering" is a set of Intervals, implying that xn can be in
1372 // neither of these intervals. To be a covering (of the real line), the union
1373 // of these intervals should be the real numbers.
1374 // ======== CAD direct conflict
1375 // Children (Cell, A)
1376 // ---------------------
1377 // Conclusion: (false)
1378 // A direct interval is generated from an assumption A (in variables x1...xn)
1379 // over a Cell (in variables x1...xn). It derives that A evaluates to false
1380 // over the Cell. In the actual algorithm, it means that xn can not be in the
1381 // topmost interval of the Cell.
1382 ARITH_NL_CAD_DIRECT
,
1383 // ======== CAD recursive interval
1384 // Children (Cell, Covering)
1385 // ---------------------
1386 // Conclusion: (false)
1387 // A recursive interval is generated from a Covering (for xn) over a Cell
1388 // (in variables x1...xn-1). It generates the conclusion that no xn exists
1389 // that extends the Cell and satisfies all assumptions.
1390 ARITH_NL_CAD_RECURSIVE
,
1392 //================================================ Place holder for Lfsc rules
1393 // ======== Lfsc rule
1394 // Children: (P1 ... Pn)
1395 // Arguments: (id, Q, A1, ..., Am)
1396 // ---------------------
1400 //================================================= Unknown rule
1405 * Converts a proof rule to a string. Note: This function is also used in
1406 * `safe_print()`. Changing this function name or signature will result in
1407 * `safe_print()` printing "<unsupported>" instead of the proper strings for
1410 * @param id The proof rule
1411 * @return The name of the proof rule
1413 const char* toString(PfRule id
);
1416 * Writes a proof rule name to a stream.
1418 * @param out The stream to write to
1419 * @param id The proof rule to write to the stream
1420 * @return The stream
1422 std::ostream
& operator<<(std::ostream
& out
, PfRule id
);
1424 /** Hash function for proof rules */
1425 struct PfRuleHashFunction
1427 size_t operator()(PfRule id
) const;
1428 }; /* struct PfRuleHashFunction */
1432 #endif /* CVC5__PROOF__PROOF_RULE_H */