blob: f62f01a9daa2f97821455e28e3a041f2ba8c92f1 (
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
|
(**************************************************************************)
(* *)
(* 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 *)
(* *)
(**************************************************************************)
val gen_constant : string list list -> string -> Structures.constr lazy_t
(* Int63 *)
val cint : Structures.constr lazy_t
val ceq63 : Structures.constr lazy_t
(* PArray *)
val carray : Structures.constr lazy_t
(* nat *)
val cnat : Structures.constr lazy_t
val cO : Structures.constr lazy_t
val cS : Structures.constr lazy_t
(* Positive *)
val cpositive : Structures.constr lazy_t
val cxI : Structures.constr lazy_t
val cxO : Structures.constr lazy_t
val cxH : Structures.constr lazy_t
val ceqbP : Structures.constr lazy_t
(* N *)
val cN : Structures.constr lazy_t
val cN0 : Structures.constr lazy_t
val cNpos : Structures.constr lazy_t
val cof_nat : Structures.constr lazy_t
(* Z *)
val cZ : Structures.constr lazy_t
val cZ0 : Structures.constr lazy_t
val cZpos : Structures.constr lazy_t
val cZneg : Structures.constr lazy_t
val copp : Structures.constr lazy_t
val cadd : Structures.constr lazy_t
val csub : Structures.constr lazy_t
val cmul : Structures.constr lazy_t
val cltb : Structures.constr lazy_t
val cleb : Structures.constr lazy_t
val cgeb : Structures.constr lazy_t
val cgtb : Structures.constr lazy_t
val ceqbZ : Structures.constr lazy_t
(* Booleans *)
val cbool : Structures.constr lazy_t
val ctrue : Structures.constr lazy_t
val cfalse : Structures.constr lazy_t
val candb : Structures.constr lazy_t
val corb : Structures.constr lazy_t
val cxorb : Structures.constr lazy_t
val cnegb : Structures.constr lazy_t
val cimplb : Structures.constr lazy_t
val ceqb : Structures.constr lazy_t
val cifb : Structures.constr lazy_t
val ciff : Structures.constr lazy_t
val creflect : Structures.constr lazy_t
(* Lists *)
val clist : Structures.constr lazy_t
val cnil : Structures.constr lazy_t
val ccons : Structures.constr lazy_t
val clength : Structures.constr lazy_t
(* Option *)
val coption : Structures.constr lazy_t
val cSome : Structures.constr lazy_t
val cNone : Structures.constr lazy_t
(* Pairs *)
val cpair : Structures.constr lazy_t
val cprod : Structures.constr lazy_t
(* Dependent pairs *)
val csigT : Structures.constr lazy_t
(* Logical Operators *)
val cnot : Structures.constr lazy_t
val ceq : Structures.constr lazy_t
val crefl_equal : Structures.constr lazy_t
val cconj : Structures.constr lazy_t
val cand : Structures.constr lazy_t
(* Bit vectors *)
val cbitvector : Structures.constr lazy_t
val cof_bits : Structures.constr lazy_t
val cbitOf : Structures.constr lazy_t
val cbv_eq : Structures.constr lazy_t
val cbv_not : Structures.constr lazy_t
val cbv_neg : Structures.constr lazy_t
val cbv_and : Structures.constr lazy_t
val cbv_or : Structures.constr lazy_t
val cbv_xor : Structures.constr lazy_t
val cbv_add : Structures.constr lazy_t
val cbv_mult : Structures.constr lazy_t
val cbv_ult : Structures.constr lazy_t
val cbv_slt : Structures.constr lazy_t
val cbv_concat : Structures.constr lazy_t
val cbv_extr : Structures.constr lazy_t
val cbv_zextn : Structures.constr lazy_t
val cbv_sextn : Structures.constr lazy_t
val cbv_shl : Structures.constr lazy_t
val cbv_shr : Structures.constr lazy_t
(* Arrays *)
val cfarray : Structures.constr lazy_t
val cselect : Structures.constr lazy_t
val cstore : Structures.constr lazy_t
val cdiff : Structures.constr lazy_t
val cequalarray : Structures.constr lazy_t
(* OrderedType *)
(* SMT_terms *)
val cState_C_t : Structures.constr lazy_t
val cState_S_t : Structures.constr lazy_t
val cdistinct : Structures.constr lazy_t
val ctype : Structures.constr lazy_t
val cTZ : Structures.constr lazy_t
val cTbool : Structures.constr lazy_t
val cTpositive : Structures.constr lazy_t
val cTBV : Structures.constr lazy_t
val cTFArray : Structures.constr lazy_t
val cTindex : Structures.constr lazy_t
val cinterp_t : Structures.constr lazy_t
val cdec_interp : Structures.constr lazy_t
val cord_interp : Structures.constr lazy_t
val ccomp_interp : Structures.constr lazy_t
val cinh_interp : Structures.constr lazy_t
val cinterp_eqb : Structures.constr lazy_t
val ctyp_compdec : Structures.constr lazy_t
val cTyp_compdec : Structures.constr lazy_t
val cunit_typ_compdec : Structures.constr lazy_t
val cte_carrier : Structures.constr lazy_t
val cte_compdec : Structures.constr lazy_t
val ceqb_of_compdec : Structures.constr lazy_t
val cCompDec : Structures.constr lazy_t
val cbool_compdec : Structures.constr lazy_t
val cZ_compdec : Structures.constr lazy_t
val cPositive_compdec : Structures.constr lazy_t
val cBV_compdec : Structures.constr lazy_t
val cFArray_compdec : Structures.constr lazy_t
val ctval : Structures.constr lazy_t
val cTval : Structures.constr lazy_t
val cCO_xH : Structures.constr lazy_t
val cCO_Z0 : Structures.constr lazy_t
val cCO_BV : Structures.constr lazy_t
val cUO_xO : Structures.constr lazy_t
val cUO_xI : Structures.constr lazy_t
val cUO_Zpos : Structures.constr lazy_t
val cUO_Zneg : Structures.constr lazy_t
val cUO_Zopp : Structures.constr lazy_t
val cUO_BVbitOf : Structures.constr lazy_t
val cUO_BVnot : Structures.constr lazy_t
val cUO_BVneg : Structures.constr lazy_t
val cUO_BVextr : Structures.constr lazy_t
val cUO_BVzextn : Structures.constr lazy_t
val cUO_BVsextn : Structures.constr lazy_t
val cBO_Zplus : Structures.constr lazy_t
val cBO_Zminus : Structures.constr lazy_t
val cBO_Zmult : Structures.constr lazy_t
val cBO_Zlt : Structures.constr lazy_t
val cBO_Zle : Structures.constr lazy_t
val cBO_Zge : Structures.constr lazy_t
val cBO_Zgt : Structures.constr lazy_t
val cBO_eq : Structures.constr lazy_t
val cBO_BVand : Structures.constr lazy_t
val cBO_BVor : Structures.constr lazy_t
val cBO_BVxor : Structures.constr lazy_t
val cBO_BVadd : Structures.constr lazy_t
val cBO_BVmult : Structures.constr lazy_t
val cBO_BVult : Structures.constr lazy_t
val cBO_BVslt : Structures.constr lazy_t
val cBO_BVconcat : Structures.constr lazy_t
val cBO_BVshl : Structures.constr lazy_t
val cBO_BVshr : Structures.constr lazy_t
val cBO_select : Structures.constr lazy_t
val cBO_diffarray : Structures.constr lazy_t
val cTO_store : Structures.constr lazy_t
val cNO_distinct : Structures.constr lazy_t
val catom : Structures.constr lazy_t
val cAcop : Structures.constr lazy_t
val cAuop : Structures.constr lazy_t
val cAbop : Structures.constr lazy_t
val cAtop : Structures.constr lazy_t
val cAnop : Structures.constr lazy_t
val cAapp : Structures.constr lazy_t
val cform : Structures.constr lazy_t
val cFatom : Structures.constr lazy_t
val cFtrue : Structures.constr lazy_t
val cFfalse : Structures.constr lazy_t
val cFnot2 : Structures.constr lazy_t
val cFand : Structures.constr lazy_t
val cFor : Structures.constr lazy_t
val cFxor : Structures.constr lazy_t
val cFimp : Structures.constr lazy_t
val cFiff : Structures.constr lazy_t
val cFite : Structures.constr lazy_t
val cFbbT : Structures.constr lazy_t
val cis_true : Structures.constr lazy_t
val cvalid_sat_checker : Structures.constr lazy_t
val cinterp_var_sat_checker : Structures.constr lazy_t
val make_certif_ops :
string list list ->
Structures.constr array option ->
Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t *
Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t *
Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t *
Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t *
Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t *
Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t *
Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t *
Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t *
Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t *
Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t *
Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t *
Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t *
Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t *
Structures.constr lazy_t * Structures.constr lazy_t
(* Some constructions *)
val ceq_refl_true : Structures.constr lazy_t
val eq_refl_true : unit -> Structures.constr
val vm_cast_true_no_check : Structures.constr -> Structures.constr
val vm_cast_true : Environ.env -> Structures.constr -> Structures.constr
val mkNat : int -> Structures.constr
val mkN : int -> Structures.constr
val mk_bv_list : bool list -> Structures.constr
(* Reification *)
val mk_bool : Structures.constr -> bool
val mk_bool_list : Structures.constr -> bool list
val mk_nat : Structures.constr -> int
val mk_N : Structures.constr -> int
val mk_Z : Structures.constr -> int
val mk_bvsize : Structures.constr -> int
(* Switches between constr and OCaml *)
val option_of_constr_option : Structures.constr -> Structures.constr option
val list_of_constr_tuple : Structures.constr -> Structures.constr list
|
