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 // toWitness(Rewriter{idr}(toSkolem(t)*sigma{ids}(Fn)*...*sigma{ids}(F1)))
106 // toSkolem(...) converts terms from witness form to Skolem form,
107 // toWitness(...) converts terms from Skolem form to witness form.
110 // toSkolem(t')=Rewriter{idr}(toSkolem(t)*sigma{ids}(Fn)*...*sigma{ids}(F1))
111 // In other words, from the point of view of Skolem forms, this rule
112 // transforms t to t' by standard substitution + rewriting.
114 // The argument ids and idr is optional and specify the identifier of the
115 // substitution and rewriter respectively to be used. For details, see
116 // theory/builtin/proof_checker.h.
118 // ======== Substitution + Rewriting predicate introduction
120 // In this rule, we provide a formula F and conclude it, under the condition
121 // that it rewrites to true under a proven substitution.
123 // Children: (P1:F1, ..., Pn:Fn)
124 // Arguments: (F, (ids (idr)?)?)
125 // ---------------------------------------------------------------
128 // Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)) == true
129 // where ids and idr are method identifiers.
131 // Notice that we apply rewriting on the witness form of F, meaning that this
132 // rule may conclude an F whose Skolem form is justified by the definition of
133 // its (fresh) Skolem variables. Furthermore, notice that the rewriting and
134 // substitution is applied only within the side condition, meaning the
135 // rewritten form of the witness form of F does not escape this rule.
137 // ======== Substitution + Rewriting predicate elimination
139 // In this rule, if we have proven a formula F, then we may conclude its
140 // rewritten form under a proven substitution.
142 // Children: (P1:F, P2:F1, ..., P_{n+1}:Fn)
143 // Arguments: ((ids (idr)?)?)
144 // ----------------------------------------
148 // toWitness(Rewriter{idr}(toSkolem(F)*sigma{ids}(Fn)*...*sigma{ids}(F1)).
149 // where ids and idr are method identifiers.
151 // We rewrite only on the Skolem form of F, similar to MACRO_SR_EQ_INTRO.
153 // ======== Substitution + Rewriting predicate transform
155 // In this rule, if we have proven a formula F, then we may provide a formula
156 // G and conclude it if F and G are equivalent after rewriting under a proven
159 // Children: (P1:F, P2:F1, ..., P_{n+1}:Fn)
160 // Arguments: (G, (ids (idr)?)?)
161 // ----------------------------------------
164 // Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)) ==
165 // Rewriter{idr}(G*sigma{ids}(Fn)*...*sigma{ids}(F1))
167 // Notice that we apply rewriting on the witness form of F and G, similar to
168 // MACRO_SR_PRED_INTRO.
169 MACRO_SR_PRED_TRANSFORM
,
171 //================================================= Boolean rules
175 // ---------------------
176 // Conclusion: (or F (not F))
178 // ======== And elimination
179 // Children: (P:(and F1 ... Fn))
181 // ---------------------
184 // ======== And introduction
185 // Children: (P1:F1 ... Pn:Fn))
187 // ---------------------
188 // Conclusion: (and P1 ... Pn)
190 // ======== Not Or elimination
191 // Children: (P:(not (or F1 ... Fn)))
193 // ---------------------
194 // Conclusion: (not Fi)
196 // ======== Implication elimination
197 // Children: (P:(=> F1 F2))
199 // ---------------------
200 // Conclusion: (or (not F1) F2)
202 // ======== Not Implication elimination version 1
203 // Children: (P:(not (=> F1 F2)))
205 // ---------------------
208 // ======== Not Implication elimination version 2
209 // Children: (P:(not (=> F1 F2)))
211 // ---------------------
212 // Conclusion: (not F2)
214 // ======== Equivalence elimination version 1
215 // Children: (P:(= F1 F2))
217 // ---------------------
218 // Conclusion: (or (not F1) F2)
220 // ======== Equivalence elimination version 2
221 // Children: (P:(= F1 F2))
223 // ---------------------
224 // Conclusion: (or F1 (not F2))
226 // ======== Not Equivalence elimination version 1
227 // Children: (P:(not (= F1 F2)))
229 // ---------------------
230 // Conclusion: (or F1 F2)
232 // ======== Not Equivalence elimination version 2
233 // Children: (P:(not (= F1 F2)))
235 // ---------------------
236 // Conclusion: (or (not F1) (not F2))
238 // ======== XOR elimination version 1
239 // Children: (P:(xor F1 F2)))
241 // ---------------------
242 // Conclusion: (or F1 F2)
244 // ======== XOR elimination version 2
245 // Children: (P:(xor F1 F2)))
247 // ---------------------
248 // Conclusion: (or (not F1) (not F2))
250 // ======== Not XOR elimination version 1
251 // Children: (P:(not (xor F1 F2)))
253 // ---------------------
254 // Conclusion: (or F1 (not F2))
256 // ======== Not XOR elimination version 2
257 // Children: (P:(not (xor F1 F2)))
259 // ---------------------
260 // Conclusion: (or (not F1) F2)
262 // ======== ITE elimination version 1
263 // Children: (P:(ite C F1 F2))
265 // ---------------------
266 // Conclusion: (or (not C) F1)
268 // ======== ITE elimination version 2
269 // Children: (P:(ite C F1 F2))
271 // ---------------------
272 // Conclusion: (or C F2)
274 // ======== Not ITE elimination version 1
275 // Children: (P:(not (ite C F1 F2)))
277 // ---------------------
278 // Conclusion: (or (not C) (not F1))
280 // ======== Not ITE elimination version 1
281 // Children: (P:(not (ite C F1 F2)))
283 // ---------------------
284 // Conclusion: (or C (not F2))
286 // ======== Not ITE elimination version 1
287 // Children: (P1:P P2:(not P))
289 // ---------------------
290 // Conclusion: (false)
293 //================================================= De Morgan rules
295 // Children: (P:(not (and F1 ... Fn))
297 // ---------------------
298 // Conclusion: (or (not F1) ... (not Fn))
300 //================================================= CNF rules
301 // ======== CNF And Pos
303 // Arguments: ((and F1 ... Fn), i)
304 // ---------------------
305 // Conclusion: (or (not (and F1 ... Fn)) Fi)
307 // ======== CNF And Neg
309 // Arguments: ((and F1 ... Fn))
310 // ---------------------
311 // Conclusion: (or (and F1 ... Fn) (not F1) ... (not Fn))
313 // ======== CNF Or Pos
315 // Arguments: ((or F1 ... Fn))
316 // ---------------------
317 // Conclusion: (or (not (or F1 ... Fn)) F1 ... Fn)
319 // ======== CNF Or Neg
321 // Arguments: ((or F1 ... Fn), i)
322 // ---------------------
323 // Conclusion: (or (or F1 ... Fn) (not Fi))
325 // ======== CNF Implies Pos
327 // Arguments: ((implies F1 F2))
328 // ---------------------
329 // Conclusion: (or (not (implies F1 F2)) (not F1) F2)
331 // ======== CNF Implies Neg version 1
333 // Arguments: ((implies F1 F2))
334 // ---------------------
335 // Conclusion: (or (implies F1 F2) F1)
337 // ======== CNF Implies Neg version 2
339 // Arguments: ((implies F1 F2))
340 // ---------------------
341 // Conclusion: (or (implies F1 F2) (not F2))
343 // ======== CNF Equiv Pos version 1
345 // Arguments: ((= F1 F2))
346 // ---------------------
347 // Conclusion: (or (not (= F1 F2)) (not F1) F2)
349 // ======== CNF Equiv Pos version 2
351 // Arguments: ((= F1 F2))
352 // ---------------------
353 // Conclusion: (or (not (= F1 F2)) F1 (not F2))
355 // ======== CNF Equiv Neg version 1
357 // Arguments: ((= F1 F2))
358 // ---------------------
359 // Conclusion: (or (= F1 F2) F1 F2)
361 // ======== CNF Equiv Neg version 2
363 // Arguments: ((= F1 F2))
364 // ---------------------
365 // Conclusion: (or (= F1 F2) (not F1) (not F2))
367 // ======== CNF Xor Pos version 1
369 // Arguments: ((xor F1 F2))
370 // ---------------------
371 // Conclusion: (or (not (xor F1 F2)) F1 F2)
373 // ======== CNF Xor Pos version 2
375 // Arguments: ((xor F1 F2))
376 // ---------------------
377 // Conclusion: (or (not (xor F1 F2)) (not F1) (not F2))
379 // ======== CNF Xor Neg version 1
381 // Arguments: ((xor F1 F2))
382 // ---------------------
383 // Conclusion: (or (xor F1 F2) (not F1) F2)
385 // ======== CNF Xor Neg version 2
387 // Arguments: ((xor F1 F2))
388 // ---------------------
389 // Conclusion: (or (xor F1 F2) F1 (not F2))
391 // ======== CNF ITE Pos version 1
393 // Arguments: ((ite C F1 F2))
394 // ---------------------
395 // Conclusion: (or (not (ite C F1 F2)) (not C) F1)
397 // ======== CNF ITE Pos version 2
399 // Arguments: ((ite C F1 F2))
400 // ---------------------
401 // Conclusion: (or (not (ite C F1 F2)) C F2)
403 // ======== CNF ITE Pos version 3
405 // Arguments: ((ite C F1 F2))
406 // ---------------------
407 // Conclusion: (or (not (ite C F1 F2)) F1 F2)
409 // ======== CNF ITE Neg version 1
411 // Arguments: ((ite C F1 F2))
412 // ---------------------
413 // Conclusion: (or (ite C F1 F2) (not C) (not F1))
415 // ======== CNF ITE Neg version 2
417 // Arguments: ((ite C F1 F2))
418 // ---------------------
419 // Conclusion: (or (ite C F1 F2) C (not F2))
421 // ======== CNF ITE Neg version 3
423 // Arguments: ((ite C F1 F2))
424 // ---------------------
425 // Conclusion: (or (ite C F1 F2) (not F1) (not F2))
428 //================================================= Equality rules
429 // ======== Reflexive
432 // ---------------------
433 // Conclusion: (= t t)
435 // ======== Symmetric
436 // Children: (P:(= t1 t2)) or (P:(not (= t1 t2)))
438 // -----------------------
439 // Conclusion: (= t2 t1) or (not (= t2 t1))
441 // ======== Transitivity
442 // Children: (P1:(= t1 t2), ..., Pn:(= t{n-1} tn))
444 // -----------------------
445 // Conclusion: (= t1 tn)
447 // ======== Congruence (subsumed by Substitute?)
448 // Children: (P1:(= t1 s1), ..., Pn:(= tn sn))
450 // ---------------------------------------------
451 // Conclusion: (= (f t1 ... tn) (f s1 ... sn))
453 // ======== True intro
456 // ----------------------------------------
457 // Conclusion: (= F true)
459 // ======== True elim
460 // Children: (P:(= F true)
462 // ----------------------------------------
465 // ======== False intro
466 // Children: (P:(not F))
468 // ----------------------------------------
469 // Conclusion: (= F false)
471 // ======== False elim
472 // Children: (P:(= F false)
474 // ----------------------------------------
475 // Conclusion: (not F)
478 //================================================= Quantifiers rules
479 // ======== Witness intro
480 // Children: (P:F[t])
482 // ----------------------------------------
483 // Conclusion: (= t (witness ((x T)) F[x]))
484 // where x is a BOUND_VARIABLE unique to the pair F,t.
486 // ======== Exists intro
487 // Children: (P:F[t])
489 // ----------------------------------------
490 // Conclusion: (exists ((x T)) F[x])
491 // where x is a BOUND_VARIABLE unique to the pair F,t.
493 // ======== Skolemize
494 // Children: (P:(exists ((x1 T1) ... (xn Tn)) F))
496 // ----------------------------------------
497 // Conclusion: F*sigma
498 // sigma maps x1 ... xn to their representative skolems obtained by
499 // SkolemManager::mkSkolemize, returned in the skolems argument of that
502 // ======== Instantiate
503 // Children: (P:(forall ((x1 T1) ... (xn Tn)) F))
504 // Arguments: (t1 ... tn)
505 // ----------------------------------------
506 // Conclusion: F*sigma
507 // sigma maps x1 ... xn to t1 ... tn.
510 // ======== Adding Inequalities
511 // Note: an ArithLiteral is a term of the form (>< poly const)
513 // >< is >=, >, ==, <, <=, or not(== ...).
514 // poly is a polynomial
515 // const is a rational constant
517 // Children: (P1:l1, ..., Pn:ln)
518 // where each li is an ArithLiteral
519 // not(= ...) is dis-allowed!
521 // Arguments: (k1, ..., kn), non-zero reals
522 // ---------------------
523 // Conclusion: (>< (* k t1) (* k t2))
524 // where >< is the fusion of the combination of the ><i, (flipping each it
525 // its ki is negative). >< is always one of <, <=
526 // NB: this implies that lower bounds must have negative ki,
527 // and upper bounds must have positive ki.
528 // t1 is the sum of the polynomials.
529 // t2 is the sum of the constants.
530 ARITH_SCALE_SUM_UPPER_BOUNDS
,
532 // ======== Tightening Strict Integer Upper Bounds
533 // Children: (P:(< i c))
534 // where i has integer type.
536 // ---------------------
537 // Conclusion: (<= i greatestIntLessThan(c)})
540 // ======== Tightening Strict Integer Lower Bounds
541 // Children: (P:(> i c))
542 // where i has integer type.
544 // ---------------------
545 // Conclusion: (>= i leastIntGreaterThan(c)})
548 // ======== Trichotomy of the reals
551 // ---------------------
553 // where (not A) (not B) and C
554 // are (> x c) (< x c) and (= x c)
556 // note that "not" here denotes arithmetic negation, flipping
560 // ======== Arithmetic operator elimination
563 // ---------------------
564 // Conclusion: arith::OperatorElim::getAxiomFor(t)
567 // ======== Int Trust
568 // Children: (P1 ... Pn)
570 // ---------------------
574 //================================================= Unknown rule
579 * Converts a proof rule to a string. Note: This function is also used in
580 * `safe_print()`. Changing this function name or signature will result in
581 * `safe_print()` printing "<unsupported>" instead of the proper strings for
584 * @param id The proof rule
585 * @return The name of the proof rule
587 const char* toString(PfRule id
);
590 * Writes a proof rule name to a stream.
592 * @param out The stream to write to
593 * @param id The proof rule to write to the stream
596 std::ostream
& operator<<(std::ostream
& out
, PfRule id
);
600 #endif /* CVC4__EXPR__PROOF_RULE_H */