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
,
167 //================================================= Boolean rules
171 // ---------------------
172 // Conclusion: (or F (not F))
174 // ======== And elimination
175 // Children: (P:(and F1 ... Fn))
177 // ---------------------
180 // ======== And introduction
181 // Children: (P1:F1 ... Pn:Fn))
183 // ---------------------
184 // Conclusion: (and P1 ... Pn)
186 // ======== Not Or elimination
187 // Children: (P:(not (or F1 ... Fn)))
189 // ---------------------
190 // Conclusion: (not Fi)
192 // ======== Implication elimination
193 // Children: (P:(=> F1 F2))
195 // ---------------------
196 // Conclusion: (or (not F1) F2)
198 // ======== Not Implication elimination version 1
199 // Children: (P:(not (=> F1 F2)))
201 // ---------------------
204 // ======== Not Implication elimination version 2
205 // Children: (P:(not (=> F1 F2)))
207 // ---------------------
208 // Conclusion: (not F2)
210 // ======== Equivalence elimination version 1
211 // Children: (P:(= F1 F2))
213 // ---------------------
214 // Conclusion: (or (not F1) F2)
216 // ======== Equivalence elimination version 2
217 // Children: (P:(= F1 F2))
219 // ---------------------
220 // Conclusion: (or F1 (not F2))
222 // ======== Not Equivalence elimination version 1
223 // Children: (P:(not (= F1 F2)))
225 // ---------------------
226 // Conclusion: (or F1 F2)
228 // ======== Not Equivalence elimination version 2
229 // Children: (P:(not (= F1 F2)))
231 // ---------------------
232 // Conclusion: (or (not F1) (not F2))
234 // ======== XOR elimination version 1
235 // Children: (P:(xor F1 F2)))
237 // ---------------------
238 // Conclusion: (or F1 F2)
240 // ======== XOR elimination version 2
241 // Children: (P:(xor F1 F2)))
243 // ---------------------
244 // Conclusion: (or (not F1) (not F2))
246 // ======== Not XOR elimination version 1
247 // Children: (P:(not (xor F1 F2)))
249 // ---------------------
250 // Conclusion: (or F1 (not F2))
252 // ======== Not XOR elimination version 2
253 // Children: (P:(not (xor F1 F2)))
255 // ---------------------
256 // Conclusion: (or (not F1) F2)
258 // ======== ITE elimination version 1
259 // Children: (P:(ite C F1 F2))
261 // ---------------------
262 // Conclusion: (or (not C) F1)
264 // ======== ITE elimination version 2
265 // Children: (P:(ite C F1 F2))
267 // ---------------------
268 // Conclusion: (or C F2)
270 // ======== Not ITE elimination version 1
271 // Children: (P:(not (ite C F1 F2)))
273 // ---------------------
274 // Conclusion: (or (not C) (not F1))
276 // ======== Not ITE elimination version 1
277 // Children: (P:(not (ite C F1 F2)))
279 // ---------------------
280 // Conclusion: (or C (not F2))
282 // ======== Not ITE elimination version 1
283 // Children: (P1:P P2:(not P))
285 // ---------------------
286 // Conclusion: (false)
289 //================================================= De Morgan rules
291 // Children: (P:(not (and F1 ... Fn))
293 // ---------------------
294 // Conclusion: (or (not F1) ... (not Fn))
296 //================================================= CNF rules
297 // ======== CNF And Pos
299 // Arguments: ((and F1 ... Fn), i)
300 // ---------------------
301 // Conclusion: (or (not (and F1 ... Fn)) Fi)
303 // ======== CNF And Neg
305 // Arguments: ((and F1 ... Fn))
306 // ---------------------
307 // Conclusion: (or (and F1 ... Fn) (not F1) ... (not Fn))
309 // ======== CNF Or Pos
311 // Arguments: ((or F1 ... Fn))
312 // ---------------------
313 // Conclusion: (or (not (or F1 ... Fn)) F1 ... Fn)
315 // ======== CNF Or Neg
317 // Arguments: ((or F1 ... Fn), i)
318 // ---------------------
319 // Conclusion: (or (or F1 ... Fn) (not Fi))
321 // ======== CNF Implies Pos
323 // Arguments: ((implies F1 F2))
324 // ---------------------
325 // Conclusion: (or (not (implies F1 F2)) (not F1) F2)
327 // ======== CNF Implies Neg version 1
329 // Arguments: ((implies F1 F2))
330 // ---------------------
331 // Conclusion: (or (implies F1 F2) F1)
333 // ======== CNF Implies Neg version 2
335 // Arguments: ((implies F1 F2))
336 // ---------------------
337 // Conclusion: (or (implies F1 F2) (not F2))
339 // ======== CNF Equiv Pos version 1
341 // Arguments: ((= F1 F2))
342 // ---------------------
343 // Conclusion: (or (not (= F1 F2)) (not F1) F2)
345 // ======== CNF Equiv Pos version 2
347 // Arguments: ((= F1 F2))
348 // ---------------------
349 // Conclusion: (or (not (= F1 F2)) F1 (not F2))
351 // ======== CNF Equiv Neg version 1
353 // Arguments: ((= F1 F2))
354 // ---------------------
355 // Conclusion: (or (= F1 F2) F1 F2)
357 // ======== CNF Equiv Neg version 2
359 // Arguments: ((= F1 F2))
360 // ---------------------
361 // Conclusion: (or (= F1 F2) (not F1) (not F2))
363 // ======== CNF Xor Pos version 1
365 // Arguments: ((xor F1 F2))
366 // ---------------------
367 // Conclusion: (or (not (xor F1 F2)) F1 F2)
369 // ======== CNF Xor Pos version 2
371 // Arguments: ((xor F1 F2))
372 // ---------------------
373 // Conclusion: (or (not (xor F1 F2)) (not F1) (not F2))
375 // ======== CNF Xor Neg version 1
377 // Arguments: ((xor F1 F2))
378 // ---------------------
379 // Conclusion: (or (xor F1 F2) (not F1) F2)
381 // ======== CNF Xor Neg version 2
383 // Arguments: ((xor F1 F2))
384 // ---------------------
385 // Conclusion: (or (xor F1 F2) F1 (not F2))
387 // ======== CNF ITE Pos version 1
389 // Arguments: ((ite C F1 F2))
390 // ---------------------
391 // Conclusion: (or (not (ite C F1 F2)) (not C) F1)
393 // ======== CNF ITE Pos version 2
395 // Arguments: ((ite C F1 F2))
396 // ---------------------
397 // Conclusion: (or (not (ite C F1 F2)) C F2)
399 // ======== CNF ITE Pos version 3
401 // Arguments: ((ite C F1 F2))
402 // ---------------------
403 // Conclusion: (or (not (ite C F1 F2)) F1 F2)
405 // ======== CNF ITE Neg version 1
407 // Arguments: ((ite C F1 F2))
408 // ---------------------
409 // Conclusion: (or (ite C F1 F2) (not C) (not F1))
411 // ======== CNF ITE Neg version 2
413 // Arguments: ((ite C F1 F2))
414 // ---------------------
415 // Conclusion: (or (ite C F1 F2) C (not F2))
417 // ======== CNF ITE Neg version 3
419 // Arguments: ((ite C F1 F2))
420 // ---------------------
421 // Conclusion: (or (ite C F1 F2) (not F1) (not F2))
424 //================================================= Equality rules
425 // ======== Reflexive
428 // ---------------------
429 // Conclusion: (= t t)
431 // ======== Symmetric
432 // Children: (P:(= t1 t2)) or (P:(not (= t1 t2)))
434 // -----------------------
435 // Conclusion: (= t2 t1) or (not (= t2 t1))
437 // ======== Transitivity
438 // Children: (P1:(= t1 t2), ..., Pn:(= t{n-1} tn))
440 // -----------------------
441 // Conclusion: (= t1 tn)
443 // ======== Congruence (subsumed by Substitute?)
444 // Children: (P1:(= t1 s1), ..., Pn:(= tn sn))
446 // ---------------------------------------------
447 // Conclusion: (= (f t1 ... tn) (f s1 ... sn))
449 // ======== True intro
452 // ----------------------------------------
453 // Conclusion: (= F true)
455 // ======== True elim
456 // Children: (P:(= F true)
458 // ----------------------------------------
461 // ======== False intro
462 // Children: (P:(not F))
464 // ----------------------------------------
465 // Conclusion: (= F false)
467 // ======== False elim
468 // Children: (P:(= F false)
470 // ----------------------------------------
471 // Conclusion: (not F)
474 //================================================= Quantifiers rules
475 // ======== Witness intro
476 // Children: (P:F[t])
478 // ----------------------------------------
479 // Conclusion: (= t (witness ((x T)) F[x]))
480 // where x is a BOUND_VARIABLE unique to the pair F,t.
482 // ======== Exists intro
483 // Children: (P:F[t])
485 // ----------------------------------------
486 // Conclusion: (exists ((x T)) F[x])
487 // where x is a BOUND_VARIABLE unique to the pair F,t.
489 // ======== Skolemize
490 // Children: (P:(exists ((x1 T1) ... (xn Tn)) F))
492 // ----------------------------------------
493 // Conclusion: F*sigma
494 // sigma maps x1 ... xn to their representative skolems obtained by
495 // SkolemManager::mkSkolemize, returned in the skolems argument of that
498 // ======== Instantiate
499 // Children: (P:(forall ((x1 T1) ... (xn Tn)) F))
500 // Arguments: (t1 ... tn)
501 // ----------------------------------------
502 // Conclusion: F*sigma
503 // sigma maps x1 ... xn to t1 ... tn.
506 // ======== Adding Inequalities
507 // Note: an ArithLiteral is a term of the form (>< poly const)
509 // >< is >=, >, ==, <, <=, or not(== ...).
510 // poly is a polynomial
511 // const is a rational constant
513 // Children: (P1:l1, ..., Pn:ln)
514 // where each li is an ArithLiteral
515 // not(= ...) is dis-allowed!
517 // Arguments: (k1, ..., kn), non-zero reals
518 // ---------------------
519 // Conclusion: (>< (* k t1) (* k t2))
520 // where >< is the fusion of the combination of the ><i, (flipping each it
521 // its ki is negative). >< is always one of <, <=
522 // NB: this implies that lower bounds must have negative ki,
523 // and upper bounds must have positive ki.
524 // t1 is the sum of the polynomials.
525 // t2 is the sum of the constants.
526 ARITH_SCALE_SUM_UPPER_BOUNDS
,
528 // ======== Tightening Strict Integer Upper Bounds
529 // Children: (P:(< i c))
530 // where i has integer type.
532 // ---------------------
533 // Conclusion: (<= i greatestIntLessThan(c)})
536 // ======== Tightening Strict Integer Lower Bounds
537 // Children: (P:(> i c))
538 // where i has integer type.
540 // ---------------------
541 // Conclusion: (>= i leastIntGreaterThan(c)})
544 // ======== Trichotomy of the reals
547 // ---------------------
549 // where (not A) (not B) and C
550 // are (> x c) (< x c) and (= x c)
552 // note that "not" here denotes arithmetic negation, flipping
556 // ======== Arithmetic operator elimination
559 // ---------------------
560 // Conclusion: arith::OperatorElim::getAxiomFor(t)
563 // ======== Int Trust
564 // Children: (P1 ... Pn)
566 // ---------------------
570 //================================================= Unknown rule
575 * Converts a proof rule to a string. Note: This function is also used in
576 * `safe_print()`. Changing this function name or signature will result in
577 * `safe_print()` printing "<unsupported>" instead of the proper strings for
580 * @param id The proof rule
581 * @return The name of the proof rule
583 const char* toString(PfRule id
);
586 * Writes a proof rule name to a stream.
588 * @param out The stream to write to
589 * @param id The proof rule to write to the stream
592 std::ostream
& operator<<(std::ostream
& out
, PfRule id
);
596 #endif /* CVC4__EXPR__PROOF_RULE_H */