1 /********************* */
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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.
74 //================================================= Boolean rules
78 // ---------------------
79 // Conclusion: (or F (not F))
81 // ======== And elimination
82 // Children: (P:(and F1 ... Fn))
84 // ---------------------
87 // ======== And introduction
88 // Children: (P1:F1 ... Pn:Fn))
90 // ---------------------
91 // Conclusion: (and P1 ... Pn)
93 // ======== Not Or elimination
94 // Children: (P:(not (or F1 ... Fn)))
96 // ---------------------
97 // Conclusion: (not Fi)
99 // ======== Implication elimination
100 // Children: (P:(=> F1 F2))
102 // ---------------------
103 // Conclusion: (or (not F1) F2)
105 // ======== Not Implication elimination version 1
106 // Children: (P:(not (=> F1 F2)))
108 // ---------------------
111 // ======== Not Implication elimination version 2
112 // Children: (P:(not (=> F1 F2)))
114 // ---------------------
115 // Conclusion: (not F2)
117 // ======== Equivalence elimination version 1
118 // Children: (P:(= F1 F2))
120 // ---------------------
121 // Conclusion: (or (not F1) F2)
123 // ======== Equivalence elimination version 2
124 // Children: (P:(= F1 F2))
126 // ---------------------
127 // Conclusion: (or F1 (not F2))
129 // ======== Not Equivalence elimination version 1
130 // Children: (P:(not (= F1 F2)))
132 // ---------------------
133 // Conclusion: (or F1 F2)
135 // ======== Not Equivalence elimination version 2
136 // Children: (P:(not (= F1 F2)))
138 // ---------------------
139 // Conclusion: (or (not F1) (not F2))
141 // ======== XOR elimination version 1
142 // Children: (P:(xor F1 F2)))
144 // ---------------------
145 // Conclusion: (or F1 F2)
147 // ======== XOR elimination version 2
148 // Children: (P:(xor F1 F2)))
150 // ---------------------
151 // Conclusion: (or (not F1) (not F2))
153 // ======== Not XOR elimination version 1
154 // Children: (P:(not (xor F1 F2)))
156 // ---------------------
157 // Conclusion: (or F1 (not F2))
159 // ======== Not XOR elimination version 2
160 // Children: (P:(not (xor F1 F2)))
162 // ---------------------
163 // Conclusion: (or (not F1) F2)
165 // ======== ITE elimination version 1
166 // Children: (P:(ite C F1 F2))
168 // ---------------------
169 // Conclusion: (or (not C) F1)
171 // ======== ITE elimination version 2
172 // Children: (P:(ite C F1 F2))
174 // ---------------------
175 // Conclusion: (or C F2)
177 // ======== Not ITE elimination version 1
178 // Children: (P:(not (ite C F1 F2)))
180 // ---------------------
181 // Conclusion: (or (not C) (not F1))
183 // ======== Not ITE elimination version 1
184 // Children: (P:(not (ite C F1 F2)))
186 // ---------------------
187 // Conclusion: (or C (not F2))
189 // ======== Not ITE elimination version 1
190 // Children: (P1:P P2:(not P))
192 // ---------------------
193 // Conclusion: (false)
196 //================================================= De Morgan rules
198 // Children: (P:(not (and F1 ... Fn))
200 // ---------------------
201 // Conclusion: (or (not F1) ... (not Fn))
203 //================================================= CNF rules
204 // ======== CNF And Pos
206 // Arguments: ((and F1 ... Fn), i)
207 // ---------------------
208 // Conclusion: (or (not (and F1 ... Fn)) Fi)
210 // ======== CNF And Neg
212 // Arguments: ((and F1 ... Fn))
213 // ---------------------
214 // Conclusion: (or (and F1 ... Fn) (not F1) ... (not Fn))
216 // ======== CNF Or Pos
218 // Arguments: ((or F1 ... Fn))
219 // ---------------------
220 // Conclusion: (or (not (or F1 ... Fn)) F1 ... Fn)
222 // ======== CNF Or Neg
224 // Arguments: ((or F1 ... Fn), i)
225 // ---------------------
226 // Conclusion: (or (or F1 ... Fn) (not Fi))
228 // ======== CNF Implies Pos
230 // Arguments: ((implies F1 F2))
231 // ---------------------
232 // Conclusion: (or (not (implies F1 F2)) (not F1) F2)
234 // ======== CNF Implies Neg version 1
236 // Arguments: ((implies F1 F2))
237 // ---------------------
238 // Conclusion: (or (implies F1 F2) F1)
240 // ======== CNF Implies Neg version 2
242 // Arguments: ((implies F1 F2))
243 // ---------------------
244 // Conclusion: (or (implies F1 F2) (not F2))
246 // ======== CNF Equiv Pos version 1
248 // Arguments: ((= F1 F2))
249 // ---------------------
250 // Conclusion: (or (not (= F1 F2)) (not F1) F2)
252 // ======== CNF Equiv Pos version 2
254 // Arguments: ((= F1 F2))
255 // ---------------------
256 // Conclusion: (or (not (= F1 F2)) F1 (not F2))
258 // ======== CNF Equiv Neg version 1
260 // Arguments: ((= F1 F2))
261 // ---------------------
262 // Conclusion: (or (= F1 F2) F1 F2)
264 // ======== CNF Equiv Neg version 2
266 // Arguments: ((= F1 F2))
267 // ---------------------
268 // Conclusion: (or (= F1 F2) (not F1) (not F2))
270 // ======== CNF Xor Pos version 1
272 // Arguments: ((xor F1 F2))
273 // ---------------------
274 // Conclusion: (or (not (xor F1 F2)) F1 F2)
276 // ======== CNF Xor Pos version 2
278 // Arguments: ((xor F1 F2))
279 // ---------------------
280 // Conclusion: (or (not (xor F1 F2)) (not F1) (not F2))
282 // ======== CNF Xor Neg version 1
284 // Arguments: ((xor F1 F2))
285 // ---------------------
286 // Conclusion: (or (xor F1 F2) (not F1) F2)
288 // ======== CNF Xor Neg version 2
290 // Arguments: ((xor F1 F2))
291 // ---------------------
292 // Conclusion: (or (xor F1 F2) F1 (not F2))
294 // ======== CNF ITE Pos version 1
296 // Arguments: ((ite C F1 F2))
297 // ---------------------
298 // Conclusion: (or (not (ite C F1 F2)) (not C) F1)
300 // ======== CNF ITE Pos version 2
302 // Arguments: ((ite C F1 F2))
303 // ---------------------
304 // Conclusion: (or (not (ite C F1 F2)) C F2)
306 // ======== CNF ITE Pos version 3
308 // Arguments: ((ite C F1 F2))
309 // ---------------------
310 // Conclusion: (or (not (ite C F1 F2)) F1 F2)
312 // ======== CNF ITE Neg version 1
314 // Arguments: ((ite C F1 F2))
315 // ---------------------
316 // Conclusion: (or (ite C F1 F2) (not C) (not F1))
318 // ======== CNF ITE Neg version 2
320 // Arguments: ((ite C F1 F2))
321 // ---------------------
322 // Conclusion: (or (ite C F1 F2) C (not F2))
324 // ======== CNF ITE Neg version 3
326 // Arguments: ((ite C F1 F2))
327 // ---------------------
328 // Conclusion: (or (ite C F1 F2) (not F1) (not F2))
331 //======================== Builtin theory (common node operations)
332 // ======== Substitution
333 // Children: (P1:F1, ..., Pn:Fn)
334 // Arguments: (t, (ids)?)
335 // ---------------------------------------------------------------
336 // Conclusion: (= t t*sigma{ids}(Fn)*...*sigma{ids}(F1))
337 // where sigma{ids}(Fi) are substitutions, which notice are applied in
339 // Notice that ids is a MethodId identifier, which determines how to convert
340 // the formulas F1, ..., Fn into substitutions.
344 // Arguments: (t, (idr)?)
345 // ----------------------------------------
346 // Conclusion: (= t Rewriter{idr}(t))
347 // where idr is a MethodId identifier, which determines the kind of rewriter
348 // to apply, e.g. Rewriter::rewrite.
350 // ======== Substitution + Rewriting equality introduction
352 // In this rule, we provide a term t and conclude that it is equal to its
353 // rewritten form under a (proven) substitution.
355 // Children: (P1:F1, ..., Pn:Fn)
356 // Arguments: (t, (ids (idr)?)?)
357 // ---------------------------------------------------------------
358 // Conclusion: (= t t')
361 // toWitness(Rewriter{idr}(toSkolem(t)*sigma{ids}(Fn)*...*sigma{ids}(F1)))
362 // toSkolem(...) converts terms from witness form to Skolem form,
363 // toWitness(...) converts terms from Skolem form to witness form.
366 // toSkolem(t')=Rewriter{idr}(toSkolem(t)*sigma{ids}(Fn)*...*sigma{ids}(F1))
367 // In other words, from the point of view of Skolem forms, this rule
368 // transforms t to t' by standard substitution + rewriting.
370 // The argument ids and idr is optional and specify the identifier of the
371 // substitution and rewriter respectively to be used. For details, see
372 // theory/builtin/proof_checker.h.
374 // ======== Substitution + Rewriting predicate introduction
376 // In this rule, we provide a formula F and conclude it, under the condition
377 // that it rewrites to true under a proven substitution.
379 // Children: (P1:F1, ..., Pn:Fn)
380 // Arguments: (F, (ids (idr)?)?)
381 // ---------------------------------------------------------------
384 // Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)) == true
385 // where ids and idr are method identifiers.
387 // Notice that we apply rewriting on the witness form of F, meaning that this
388 // rule may conclude an F whose Skolem form is justified by the definition of
389 // its (fresh) Skolem variables. Furthermore, notice that the rewriting and
390 // substitution is applied only within the side condition, meaning the
391 // rewritten form of the witness form of F does not escape this rule.
393 // ======== Substitution + Rewriting predicate elimination
395 // In this rule, if we have proven a formula F, then we may conclude its
396 // rewritten form under a proven substitution.
398 // Children: (P1:F, P2:F1, ..., P_{n+1}:Fn)
399 // Arguments: ((ids (idr)?)?)
400 // ----------------------------------------
404 // toWitness(Rewriter{idr}(toSkolem(F)*sigma{ids}(Fn)*...*sigma{ids}(F1)).
405 // where ids and idr are method identifiers.
407 // We rewrite only on the Skolem form of F, similar to MACRO_SR_EQ_INTRO.
409 // ======== Substitution + Rewriting predicate transform
411 // In this rule, if we have proven a formula F, then we may provide a formula
412 // G and conclude it if F and G are equivalent after rewriting under a proven
415 // Children: (P1:F, P2:F1, ..., P_{n+1}:Fn)
416 // Arguments: (G, (ids (idr)?)?)
417 // ----------------------------------------
420 // Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)) ==
421 // Rewriter{idr}(G*sigma{ids}(Fn)*...*sigma{ids}(F1))
423 // Notice that we apply rewriting on the witness form of F and G, similar to
424 // MACRO_SR_PRED_INTRO.
425 MACRO_SR_PRED_TRANSFORM
,
427 //================================================= Unknown rule
432 * Converts a proof rule to a string. Note: This function is also used in
433 * `safe_print()`. Changing this function name or signature will result in
434 * `safe_print()` printing "<unsupported>" instead of the proper strings for
437 * @param id The proof rule
438 * @return The name of the proof rule
440 const char* toString(PfRule id
);
443 * Writes a proof rule name to a stream.
445 * @param out The stream to write to
446 * @param id The proof rule to write to the stream
449 std::ostream
& operator<<(std::ostream
& out
, PfRule id
);
453 #endif /* CVC4__EXPR__PROOF_RULE_H */