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.
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 //================================================= Unknown rule
176 * Converts a proof rule to a string. Note: This function is also used in
177 * `safe_print()`. Changing this function name or signature will result in
178 * `safe_print()` printing "<unsupported>" instead of the proper strings for
181 * @param id The proof rule
182 * @return The name of the proof rule
184 const char* toString(PfRule id
);
187 * Writes a proof rule name to a stream.
189 * @param out The stream to write to
190 * @param id The proof rule to write to the stream
193 std::ostream
& operator<<(std::ostream
& out
, PfRule id
);
197 #endif /* CVC4__EXPR__PROOF_RULE_H */