-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathPartialRefBasics.prf
167 lines (166 loc) · 6.06 KB
/
PartialRefBasics.prf
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
158
159
160
161
162
163
164
165
166
(PartialRefBasics
(fmPartRef 0
(fmPartRef-1 nil 3659523903
("" (skolem 1 (fm1 fm2))
(("" (bddsimp)
(("1" (expand "|=")
(("1" (expand fmPartialRefinement)
(("1" (expand subset?)
(("1" (skolem 1 c)
(("1" (inst -1 c)
(("1" (expand member) (("1" (bddsimp) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand fmPartialRefinement)
(("2" (expand "|=")
(("2" (expand subset?)
(("2" (skolem 1 c)
(("2" (inst -1 c)
(("2" (expand member) (("2" (bddsimp) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((fmPartialRefinement const-decl "bool" PartialRefBasics
nil)
(member const-decl "bool" sets nil)
(Conf formal-type-decl nil PartialRefBasics nil)
(subset? const-decl "bool" sets nil)
(\|= const-decl "bool" SPLrefinement nil))
shostak))
(amPartRefFilter_TCC1 0
(amPartRefFilter_TCC1-1 nil 3669373797 ("" (subtype-tcc) nil nil) nil
nil))
(amPartRefFilter 0
(amPartRefFilter-1 nil 3669373798
("" (skolem 1 (am1 am2 anSet))
(("" (bddsimp)
(("" (expand amPartialRef)
(("" (bddsimp)
(("" (expand "|>")
(("" (bddsimp)
(("1" (skolem 1 an)
(("1" (expand filter)
(("1" (expand dom)
(("1" (expand subset?)
(("1" (inst -1 an)
(("1" (expand member)
(("1" (assert)
(("1" (flatten)
(("1"
(skolem -4 a)
(("1"
(flatten)
(("1"
(inst -3 an)
(("1"
(bddsimp)
(("1"
(skolem -4 (aNew a2))
(("1"
(flatten)
(("1"
(inst 1 aNew a2)
(("1" (bddsimp) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand filter)
(("2" (expand dom)
(("2" (decompose-equality 1)
(("2" (bddsimp)
(("1" (skolem -1 r)
(("1" (expand subset?)
(("1" (inst -3 "x!1")
(("1" (expand member)
(("1"
(bddsimp)
(("1"
(skolem -4 r2)
(("1"
(inst 1 r2)
(("1" (bddsimp) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand subset?)
(("2" (inst -2 "x!1")
(("2" (expand member)
(("2" (skolem -1 r2)
(("2"
(flatten)
(("2"
(bddsimp)
(("2"
(skolem -3 r)
(("2"
(inst 1 r)
(("2" (bddsimp) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((filter const-decl "mapping" maps nil)
(subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(Asset formal-type-decl nil PartialRefBasics nil)
(AssetName formal-type-decl nil PartialRefBasics nil)
(dom const-decl "set[S]" maps nil)
(boolean nonempty-type-decl nil booleans nil)
(AM type-eq-decl nil SPLrefinement nil)
([\|\|] formal-const-decl
"[CK -> [mapping -> [Conf -> finite_sets[Asset].finite_set]]]"
PartialRefBasics nil)
(mapping type-eq-decl nil maps nil)
({\|\|} formal-const-decl "[FM -> set[Conf]]"
PartialRefBasics nil)
(CK formal-type-decl nil PartialRefBasics nil)
(FM formal-type-decl nil PartialRefBasics nil)
(Conf formal-type-decl nil PartialRefBasics nil)
(unique const-decl "bool" maps nil)
(finite_set type-eq-decl nil finite_sets nil)
(is_finite const-decl "bool" finite_sets nil)
(set type-eq-decl nil sets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(\|> const-decl "bool" SPLrefinement nil)
(amPartialRef const-decl "bool" PartialRefBasics nil))
shostak)))