blob: 53622ac08424cd97241d03f65d8357022357a024 (
plain)
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
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
|
(**************************************************************************)
(* *)
(* SMTCoq *)
(* Copyright (C) 2011 - 2022 *)
(* *)
(* See file "AUTHORS" for the list of authors *)
(* *)
(* This file is distributed under the terms of the CeCILL-C licence *)
(* *)
(**************************************************************************)
type coqTerm = CoqInterface.constr lazy_t
(* Int63 *)
val cint : coqTerm
val ceq63 : coqTerm
(* PArray *)
val carray : coqTerm
val cmake : coqTerm
val cset : coqTerm
(* is_true *)
val cis_true : coqTerm
(* nat *)
val cnat : coqTerm
val cO : coqTerm
val cS : coqTerm
(* Positive *)
val cpositive : coqTerm
val cxI : coqTerm
val cxO : coqTerm
val cxH : coqTerm
val ceqbP : coqTerm
(* N *)
val cN : coqTerm
val cN0 : coqTerm
val cNpos : coqTerm
val cof_nat : coqTerm
(* Z *)
val cZ : coqTerm
val cZ0 : coqTerm
val cZpos : coqTerm
val cZneg : coqTerm
val copp : coqTerm
val cadd : coqTerm
val csub : coqTerm
val cmul : coqTerm
val cltb : coqTerm
val cleb : coqTerm
val cgeb : coqTerm
val cgtb : coqTerm
val ceqbZ : coqTerm
(* Booleans *)
val cbool : coqTerm
val ctrue : coqTerm
val cfalse : coqTerm
val candb : coqTerm
val corb : coqTerm
val cxorb : coqTerm
val cnegb : coqTerm
val cimplb : coqTerm
val ceqb : coqTerm
val cifb : coqTerm
val creflect : coqTerm
(* Lists *)
val clist : coqTerm
val cnil : coqTerm
val ccons : coqTerm
val clength : coqTerm
(* Option *)
val coption : coqTerm
val cSome : coqTerm
val cNone : coqTerm
(* Pairs *)
val cpair : coqTerm
val cprod : coqTerm
(* Dependent pairs *)
val csigT : coqTerm
(* Logical Operators *)
val cnot : coqTerm
val cconj : coqTerm
val cand : coqTerm
val ciff : coqTerm
(* Equality *)
val ceq : coqTerm
val crefl_equal : coqTerm
(* Micromega *)
val micromega_coq_proofTerm : coqTerm
(* Bit vectors *)
val cbitvector : coqTerm
val cof_bits : coqTerm
val cbitOf : coqTerm
val cbv_eq : coqTerm
val cbv_not : coqTerm
val cbv_neg : coqTerm
val cbv_and : coqTerm
val cbv_or : coqTerm
val cbv_xor : coqTerm
val cbv_add : coqTerm
val cbv_mult : coqTerm
val cbv_ult : coqTerm
val cbv_slt : coqTerm
val cbv_concat : coqTerm
val cbv_extr : coqTerm
val cbv_zextn : coqTerm
val cbv_sextn : coqTerm
val cbv_shl : coqTerm
val cbv_shr : coqTerm
(* Arrays *)
val cfarray : coqTerm
val cselect : coqTerm
val cstore : coqTerm
val cdiff : coqTerm
val cequalarray : coqTerm
(* SMTCoq terms *)
val cState_C_t : coqTerm
val cState_S_t : coqTerm
val cdistinct : coqTerm
val ctype : coqTerm
val cTZ : coqTerm
val cTbool : coqTerm
val cTpositive : coqTerm
val cTBV : coqTerm
val cTFArray : coqTerm
val cTindex : coqTerm
val cinterp_t : coqTerm
val cdec_interp : coqTerm
val cord_interp : coqTerm
val ccomp_interp : coqTerm
val cinh_interp : coqTerm
val cinterp_eqb : coqTerm
val ctval : coqTerm
val cTval : coqTerm
val cCO_xH : coqTerm
val cCO_Z0 : coqTerm
val cCO_BV : coqTerm
val cUO_xO : coqTerm
val cUO_xI : coqTerm
val cUO_Zpos : coqTerm
val cUO_Zneg : coqTerm
val cUO_Zopp : coqTerm
val cUO_BVbitOf : coqTerm
val cUO_BVnot : coqTerm
val cUO_BVneg : coqTerm
val cUO_BVextr : coqTerm
val cUO_BVzextn : coqTerm
val cUO_BVsextn : coqTerm
val cBO_Zplus : coqTerm
val cBO_Zminus : coqTerm
val cBO_Zmult : coqTerm
val cBO_Zlt : coqTerm
val cBO_Zle : coqTerm
val cBO_Zge : coqTerm
val cBO_Zgt : coqTerm
val cBO_eq : coqTerm
val cBO_BVand : coqTerm
val cBO_BVor : coqTerm
val cBO_BVxor : coqTerm
val cBO_BVadd : coqTerm
val cBO_BVmult : coqTerm
val cBO_BVult : coqTerm
val cBO_BVslt : coqTerm
val cBO_BVconcat : coqTerm
val cBO_BVshl : coqTerm
val cBO_BVshr : coqTerm
val cBO_select : coqTerm
val cBO_diffarray : coqTerm
val cTO_store : coqTerm
val cNO_distinct : coqTerm
val catom : coqTerm
val cAcop : coqTerm
val cAuop : coqTerm
val cAbop : coqTerm
val cAtop : coqTerm
val cAnop : coqTerm
val cAapp : coqTerm
val cform : coqTerm
val cFatom : coqTerm
val cFtrue : coqTerm
val cFfalse : coqTerm
val cFnot2 : coqTerm
val cFand : coqTerm
val cFor : coqTerm
val cFxor : coqTerm
val cFimp : coqTerm
val cFiff : coqTerm
val cFite : coqTerm
val cFbbT : coqTerm
(* SMTCoq Classes *)
val ctyp_compdec : coqTerm
val cTyp_compdec : coqTerm
val cte_carrier : coqTerm
val cte_compdec : coqTerm
val ceqb_of_compdec : coqTerm
val cCompDec : coqTerm
val cunit_typ_compdec : coqTerm
val cbool_compdec : coqTerm
val cZ_compdec : coqTerm
val cPositive_compdec : coqTerm
val cBV_compdec : coqTerm
val cFArray_compdec : coqTerm
(* SMTCoq Trace *)
type certif_ops =
coqTerm * coqTerm * coqTerm *
coqTerm * coqTerm * coqTerm *
coqTerm * coqTerm * coqTerm *
coqTerm * coqTerm * coqTerm *
coqTerm * coqTerm * coqTerm *
coqTerm * coqTerm * coqTerm *
coqTerm * coqTerm * coqTerm *
coqTerm * coqTerm * coqTerm *
coqTerm * coqTerm * coqTerm *
coqTerm * coqTerm * coqTerm *
coqTerm * coqTerm * coqTerm *
coqTerm * coqTerm * coqTerm *
coqTerm * coqTerm * coqTerm *
coqTerm * coqTerm
val csat_checker_valid : coqTerm
val csat_checker_interp_var : coqTerm
val csat_checker_Certif : coqTerm
val csat_checker_dimacs : coqTerm
val csat_checker_certif : coqTerm
val csat_checker_theorem_checker : coqTerm
val csat_checker_checker : coqTerm
val csat_checker_certif_ops : certif_ops
val ccnf_checker_certif : coqTerm
val ccnf_checker_Certif : coqTerm
val ccnf_checker_checker_b_correct : coqTerm
val ccnf_checker_checker_b : coqTerm
val ccnf_checker_checker_eq_correct : coqTerm
val ccnf_checker_checker_eq : coqTerm
val ccnf_checker_certif_ops : certif_ops
val ceuf_checker_Certif : coqTerm
val ceuf_checker_certif : coqTerm
val ceuf_checker_checker : coqTerm
val ceuf_checker_checker_correct : coqTerm
val ceuf_checker_checker_b_correct : coqTerm
val ceuf_checker_checker_b : coqTerm
val ceuf_checker_checker_eq_correct : coqTerm
val ceuf_checker_checker_eq : coqTerm
val ceuf_checker_checker_debug : coqTerm
val ceuf_checker_name_step : coqTerm
val ceuf_checker_Name_Res : coqTerm
val ceuf_checker_Name_Weaken : coqTerm
val ceuf_checker_Name_ImmFlatten : coqTerm
val ceuf_checker_Name_CTrue : coqTerm
val ceuf_checker_Name_CFalse : coqTerm
val ceuf_checker_Name_BuildDef : coqTerm
val ceuf_checker_Name_BuildDef2 : coqTerm
val ceuf_checker_Name_BuildProj : coqTerm
val ceuf_checker_Name_ImmBuildDef : coqTerm
val ceuf_checker_Name_ImmBuildDef2 : coqTerm
val ceuf_checker_Name_ImmBuildProj : coqTerm
val ceuf_checker_Name_EqTr : coqTerm
val ceuf_checker_Name_EqCgr : coqTerm
val ceuf_checker_Name_EqCgrP : coqTerm
val ceuf_checker_Name_LiaMicromega : coqTerm
val ceuf_checker_Name_LiaDiseq : coqTerm
val ceuf_checker_Name_SplArith : coqTerm
val ceuf_checker_Name_SplDistinctElim : coqTerm
val ceuf_checker_Name_BBVar : coqTerm
val ceuf_checker_Name_BBConst : coqTerm
val ceuf_checker_Name_BBOp : coqTerm
val ceuf_checker_Name_BBNot : coqTerm
val ceuf_checker_Name_BBNeg : coqTerm
val ceuf_checker_Name_BBAdd : coqTerm
val ceuf_checker_Name_BBConcat : coqTerm
val ceuf_checker_Name_BBMul : coqTerm
val ceuf_checker_Name_BBUlt : coqTerm
val ceuf_checker_Name_BBSlt : coqTerm
val ceuf_checker_Name_BBEq : coqTerm
val ceuf_checker_Name_BBDiseq : coqTerm
val ceuf_checker_Name_BBExtract : coqTerm
val ceuf_checker_Name_BBZextend : coqTerm
val ceuf_checker_Name_BBSextend : coqTerm
val ceuf_checker_Name_BBShl : coqTerm
val ceuf_checker_Name_BBShr : coqTerm
val ceuf_checker_Name_RowEq : coqTerm
val ceuf_checker_Name_RowNeq : coqTerm
val ceuf_checker_Name_Ext : coqTerm
val ceuf_checker_Name_Hole : coqTerm
val ceuf_checker_certif_ops : CoqInterface.constr array option -> certif_ops
(* Some constructions *)
val ceq_refl_true : coqTerm
val eq_refl_true : unit -> CoqInterface.constr
val vm_cast_true_no_check : CoqInterface.constr -> CoqInterface.constr
val vm_cast_true : Environ.env -> CoqInterface.constr -> CoqInterface.constr
val mkNat : int -> CoqInterface.constr
val mkN : int -> CoqInterface.constr
val mk_bv_list : bool list -> CoqInterface.constr
val mkArray : Constr.types * Constr.t array -> Constr.t
(* Reification *)
val mk_bool : CoqInterface.constr -> bool
val mk_bool_list : CoqInterface.constr -> bool list
val mk_nat : CoqInterface.constr -> int
val mk_N : CoqInterface.constr -> int
val mk_Z : CoqInterface.constr -> int
val mk_bvsize : CoqInterface.constr -> int
(* Switches between constr and OCaml *)
val option_of_constr_option : CoqInterface.constr -> CoqInterface.constr option
val list_of_constr_tuple : CoqInterface.constr -> CoqInterface.constr list
|
