1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
|
//
// We give a semi-formal description of each proof rule in proof_kinds files.
//
// Formulas and terms in all children, arguments, and conclusions are assumed to
// be in *witness* form (see expr/proof_skolem_cache.h).
//======================== Assume and Scope
// ======== Assumption (a leaf)
// Children: none
// Arguments: (F)
// --------------
// Conclusion: F
//
// This rule has special status, in that an application of assume is an
// open leaf in a proof that is not (yet) justified. An assume leaf is
// analogous to a free variable in a term, where we say "F is a free
// assumption in proof P" if it contains an application of F that is not
// bound by SCOPE (see below).
proofrule ASSUME 0 1 ::CVC4::theory::builtin::BuiltinProofRuleChecker
// ======== Assumption (a leaf)
// Children: (P:F)
// Arguments: (F1, ..., Fn)
// --------------
// Conclusion: (=> (and F1 ... Fn) F) or (not (and F1 ... Fn)) if F is false
//
// This rule has a dual purpose with ASSUME. It is a way to close
// assumptions in a proof. We require that F1 ... Fn are free assumptions in
// P and say that F1, ..., Fn are not free in (SCOPE P). In other words, they
// are bound by this application. For example, the proof node:
// (SCOPE (ASSUME F) :args F)
// has the conclusion (=> F F) and has no free assumptions. More generally, a
// proof with no free assumptions always concludes a valid formula.
proofrule SCOPE 1 1: ::CVC4::theory::builtin::BuiltinProofRuleChecker
//======================== Node operations
// ======== Substitution
// Children: (P1:(= x1 t1), ..., Pn:(= xn tn))
// Arguments: (t, id?)
// ---------------------------------------------------------------
// Conclusion: (= t t.substitute(xn,tn). ... .substitute(x1,t1))
// Notice that the orientation of the premises matters.
proofrule SUBS 1: 1 ::CVC4::theory::builtin::BuiltinProofRuleChecker
// ======== Rewrite
// Children: none
// Arguments: (t, id?)
// ----------------------------------------
// Conclusion: (= t Rewriter::rewrite(t))
proofrule REWRITE 0 1 ::CVC4::theory::builtin::BuiltinProofRuleChecker
// NOTE: these technically rely on TRANS/TRUE_ELIM, which are UF
// ======== Substitution + Rewriting equality introduction
//
// In this rule, we provide a term t and conclude that it is equal to its
// rewritten form under a (proven) substitution.
//
// Children: (P1:(= x1 t1), ..., Pn:(= xn tn))
// Arguments: (t, id?)
// ---------------------------------------------------------------
// Conclusion: (= t t')
// where
// t' is toWitness(Rewriter{id}(toSkolem(t).substitute(x1...xn,t1...tn)))
// toSkolem(...) converts terms from witness form to Skolem form,
// toWitness(...) converts terms from Skolem form to witness form.
//
// Notice that:
// toSkolem(t') = Rewriter{id}(toSkolem(t).substitute(x1...xn,t1...tn))
// In other words, from the point of view of Skolem forms, this rule transforms
// t to t' by standard substitution + rewriting.
//
// The argument id is optional and specifies the identifier of the rewriter to
// be used (see theory/builtin/proof_checker.h).
macro MACRO_SR_EQ_INTRO 0: 1:2 ::CVC4::theory::builtin::BuiltinProofRuleChecker {
(TRANS
(SUBS <children> t)
(REWRITE <t.substitute(x1,t1). ... .substitute(xn,tn)>))
}
// ======== Substitution + Rewriting predicate introduction
//
// In this rule, we provide a formula F and conclude it, under the condition
// that it rewrites to true under a proven substitution.
//
// Children: (P1:(= x1 t1), ..., Pn:(= xn tn))
// Arguments: (F, id?)
// ---------------------------------------------------------------
// Conclusion: F
// where
// Rewriter{id}(F.substitute(x1...xn,t1...tn)) == true
//
// Notice that we apply rewriting on the witness form of F, meaning that this
// rule may conclude an F whose Skolem form is justified by the definition of
// its (fresh) Skolem variables. Furthermore, notice that the rewriting and
// substitution is applied only within the side condition, meaning the rewritten
// form of the witness form of F does not escape this rule.
macro MACRO_SR_PRED_INTRO 0: 1:2 ::CVC4::theory::builtin::BuiltinProofRuleChecker {
(TRUE_ELIM
(MACRO_SR_EQ_INTRO <children> F))
}
// ======== Substitution + Rewriting predicate elimination
//
// In this rule, if we have proven a formula F, then we may conclude its
// rewritten form under a proven substitution.
//
// Children: (P1:F, P2:(= x1 t1), ..., P_{n+1}:(= xn tn))
// Arguments: (id?)
// ----------------------------------------
// Conclusion: F'
// where
// F' is toWitness(Rewriter{id}(toSkolem(F).substitute(x1...xn,t1...tn))).
//
// We rewrite only on the Skolem form of F, similar to MACRO_SR_EQ_INTRO.
macro MACRO_SR_PRED_ELIM 1: 0:1 {
(TRUE_ELIM
(TRANS
(SYMM (MACRO_SR_EQ_INTRO <children>[1:] F))
(TRUE_INTRO <children>[0])))
}
// ======== Substitution + Rewriting predicate transform
//
// In this rule, if we have proven a formula F, then we may provide a formula
// G and conclude it if F and G are equivalent after rewriting under a proven
// substitution.
//
// Children: (P1:F, P2:(= x1 t1), ..., P_{n+1}:(= xn tn))
// Arguments: (G, id?)
// ----------------------------------------
// Conclusion: G
// where
// Rewriter{id}(F.substitute(x1...xn,t1...tn)) ==
// Rewriter{id}(G.substitute(x1...xn,t1...tn))
//
// Notice that we apply rewriting on the witness form of F and G, similar to
// MACRO_SR_PRED_INTRO.
macro MACRO_SR_PRED_TRANSFORM 1: 1:2 {
(TRUE_ELIM
(TRANS
(MACRO_SR_EQ_INTRO <children>[1:] G)
(SYMM (MACRO_SR_EQ_INTRO <children>[1:] F))
(TRUE_INTRO <children>[0])))
}
// ======== Untrustworthy theory lemma
// Children: none
// Arguments: (F, tid)
// ---------------------------------------------------------------
// Conclusion: F
// where F is a (T-valid) theory lemma generated by theory with TheoryId tid.
// This is a "coarse-grained" rule that is used as a placeholder if a theory
// did not provide a proof for a lemma or conflict.
proofrule THEORY_LEMMA 0 1 ::CVC4::theory::builtin::BuiltinProofRuleChecker
|
