blob: 3e3ae2c31e5045847cdae4e6721ef4b27d598131 (
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
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
|
val negb : bool -> bool
type nat =
| O
| S of nat
type comparison =
| Eq
| Lt
| Gt
val compOpp : comparison -> comparison
val plus : nat -> nat -> nat
val app : 'a1 list -> 'a1 list -> 'a1 list
val nth : nat -> 'a1 list -> 'a1 -> 'a1
val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list
type positive =
| XI of positive
| XO of positive
| XH
val psucc : positive -> positive
val pplus : positive -> positive -> positive
val pplus_carry : positive -> positive -> positive
val p_of_succ_nat : nat -> positive
val pdouble_minus_one : positive -> positive
type positive_mask =
| IsNul
| IsPos of positive
| IsNeg
val pdouble_plus_one_mask : positive_mask -> positive_mask
val pdouble_mask : positive_mask -> positive_mask
val pdouble_minus_two : positive -> positive_mask
val pminus_mask : positive -> positive -> positive_mask
val pminus_mask_carry : positive -> positive -> positive_mask
val pminus : positive -> positive -> positive
val pmult : positive -> positive -> positive
val pcompare : positive -> positive -> comparison -> comparison
val psize : positive -> nat
type n =
| N0
| Npos of positive
val pow_pos : ('a1 -> 'a1 -> 'a1) -> 'a1 -> positive -> 'a1
type z =
| Z0
| Zpos of positive
| Zneg of positive
val zdouble_plus_one : z -> z
val zdouble_minus_one : z -> z
val zdouble : z -> z
val zPminus : positive -> positive -> z
val zplus : z -> z -> z
val zopp : z -> z
val zminus : z -> z -> z
val zmult : z -> z -> z
val zcompare : z -> z -> comparison
val zabs : z -> z
val zmax : z -> z -> z
val zle_bool : z -> z -> bool
val zge_bool : z -> z -> bool
val zgt_bool : z -> z -> bool
val zeq_bool : z -> z -> bool
val n_of_nat : nat -> n
val zdiv_eucl_POS : positive -> z -> z * z
val zdiv_eucl : z -> z -> z * z
val zdiv : z -> z -> z
type 'c pol =
| Pc of 'c
| Pinj of positive * 'c pol
| PX of 'c pol * positive * 'c pol
val p0 : 'a1 -> 'a1 pol
val p1 : 'a1 -> 'a1 pol
val peq : ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> bool
val mkPinj_pred : positive -> 'a1 pol -> 'a1 pol
val mkPX :
'a1 -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol
val mkXi : 'a1 -> 'a1 -> positive -> 'a1 pol
val mkX : 'a1 -> 'a1 -> 'a1 pol
val popp : ('a1 -> 'a1) -> 'a1 pol -> 'a1 pol
val paddC : ('a1 -> 'a1 -> 'a1) -> 'a1 pol -> 'a1 -> 'a1 pol
val psubC : ('a1 -> 'a1 -> 'a1) -> 'a1 pol -> 'a1 -> 'a1 pol
val paddI :
('a1 -> 'a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol ->
positive -> 'a1 pol -> 'a1 pol
val psubI :
('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) ->
'a1 pol -> positive -> 'a1 pol -> 'a1 pol
val paddX :
'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol
-> positive -> 'a1 pol -> 'a1 pol
val psubX :
'a1 -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1
pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol
val padd :
'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol ->
'a1 pol
val psub :
'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1
-> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol
val pmulC_aux :
'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 -> 'a1
pol
val pmulC :
'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1
-> 'a1 pol
val pmulI :
'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol ->
'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol
val pmul :
'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol
val psquare :
'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
bool) -> 'a1 pol -> 'a1 pol
type 'c pExpr =
| PEc of 'c
| PEX of positive
| PEadd of 'c pExpr * 'c pExpr
| PEsub of 'c pExpr * 'c pExpr
| PEmul of 'c pExpr * 'c pExpr
| PEopp of 'c pExpr
| PEpow of 'c pExpr * n
val mk_X : 'a1 -> 'a1 -> positive -> 'a1 pol
val ppow_pos :
'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
bool) -> ('a1 pol -> 'a1 pol) -> 'a1 pol -> 'a1 pol -> positive -> 'a1 pol
val ppow_N :
'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
bool) -> ('a1 pol -> 'a1 pol) -> 'a1 pol -> n -> 'a1 pol
val norm_aux :
'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol
type 'a bFormula =
| TT
| FF
| X
| A of 'a
| Cj of 'a bFormula * 'a bFormula
| D of 'a bFormula * 'a bFormula
| N of 'a bFormula
| I of 'a bFormula * 'a bFormula
type 'term' clause = 'term' list
type 'term' cnf = 'term' clause list
val tt : 'a1 cnf
val ff : 'a1 cnf
val or_clause_cnf : 'a1 clause -> 'a1 cnf -> 'a1 cnf
val or_cnf : 'a1 cnf -> 'a1 cnf -> 'a1 cnf
val and_cnf : 'a1 cnf -> 'a1 cnf -> 'a1 cnf
val xcnf :
('a1 -> 'a2 cnf) -> ('a1 -> 'a2 cnf) -> bool -> 'a1 bFormula -> 'a2 cnf
val cnf_checker : ('a1 list -> 'a2 -> bool) -> 'a1 cnf -> 'a2 list -> bool
val tauto_checker :
('a1 -> 'a2 cnf) -> ('a1 -> 'a2 cnf) -> ('a2 list -> 'a3 -> bool) -> 'a1
bFormula -> 'a3 list -> bool
type 'c polC = 'c pol
type op1 =
| Equal
| NonEqual
| Strict
| NonStrict
type 'c nFormula = 'c polC * op1
val opAdd : op1 -> op1 -> op1 option
type 'c psatz =
| PsatzIn of nat
| PsatzSquare of 'c polC
| PsatzMulC of 'c polC * 'c psatz
| PsatzMulE of 'c psatz * 'c psatz
| PsatzAdd of 'c psatz * 'c psatz
| PsatzC of 'c
| PsatzZ
val pexpr_times_nformula :
'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
bool) -> 'a1 polC -> 'a1 nFormula -> 'a1 nFormula option
val nformula_times_nformula :
'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
bool) -> 'a1 nFormula -> 'a1 nFormula -> 'a1 nFormula option
val nformula_plus_nformula :
'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> 'a1
nFormula -> 'a1 nFormula option
val eval_Psatz :
'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz -> 'a1
nFormula option
val check_inconsistent :
'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> bool
val check_normalised_formulas :
'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz -> bool
type op2 =
| OpEq
| OpNEq
| OpLe
| OpGe
| OpLt
| OpGt
type 'c formula = { flhs : 'c pExpr; fop : op2; frhs : 'c pExpr }
val flhs : 'a1 formula -> 'a1 pExpr
val fop : 'a1 formula -> op2
val frhs : 'a1 formula -> 'a1 pExpr
val norm :
'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol
val psub0 :
'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1
-> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol
val padd0 :
'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol ->
'a1 pol
val xnormalise :
'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 nFormula
list
val cnf_normalise :
'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 nFormula
cnf
val xnegate :
'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 nFormula
list
val cnf_negate :
'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 ->
'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 nFormula
cnf
val xdenorm : positive -> 'a1 pol -> 'a1 pExpr
val denorm : 'a1 pol -> 'a1 pExpr
val simpl_cone :
'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 psatz ->
'a1 psatz
type q = { qnum : z; qden : positive }
val qnum : q -> z
val qden : q -> positive
val qeq_bool : q -> q -> bool
val qle_bool : q -> q -> bool
val qplus : q -> q -> q
val qmult : q -> q -> q
val qopp : q -> q
val qminus : q -> q -> q
val qinv : q -> q
val qpower_positive : q -> positive -> q
val qpower : q -> z -> q
val pgcdn : nat -> positive -> positive -> positive
val pgcd : positive -> positive -> positive
val zgcd : z -> z -> z
type 'a t =
| Empty
| Leaf of 'a
| Node of 'a t * 'a * 'a t
val find : 'a1 -> 'a1 t -> positive -> 'a1
type zWitness = z psatz
val zWeakChecker : z nFormula list -> z psatz -> bool
val psub1 : z pol -> z pol -> z pol
val padd1 : z pol -> z pol -> z pol
val norm0 : z pExpr -> z pol
val xnormalise0 : z formula -> z nFormula list
val normalise : z formula -> z nFormula cnf
val xnegate0 : z formula -> z nFormula list
val negate : z formula -> z nFormula cnf
val ceiling : z -> z -> z
type zArithProof =
| DoneProof
| RatProof of zWitness * zArithProof
| CutProof of zWitness * zArithProof
| EnumProof of zWitness * zWitness * zArithProof list
val zgcdM : z -> z -> z
val zgcd_pol : z polC -> z * z
val zdiv_pol : z polC -> z -> z polC
val makeCuttingPlane : z polC -> z polC * z
val genCuttingPlane : z nFormula -> ((z polC * z) * op1) option
val nformula_of_cutting_plane : ((z polC * z) * op1) -> z nFormula
val is_pol_Z0 : z polC -> bool
val eval_Psatz0 : z nFormula list -> zWitness -> z nFormula option
val check_inconsistent0 : z nFormula -> bool
val zChecker : z nFormula list -> zArithProof -> bool
val zTautoChecker : z formula bFormula -> zArithProof list -> bool
val n_of_Z : z -> n
type qWitness = q psatz
val qWeakChecker : q nFormula list -> q psatz -> bool
val qnormalise : q formula -> q nFormula cnf
val qnegate : q formula -> q nFormula cnf
val qTautoChecker : q formula bFormula -> qWitness list -> bool
type rWitness = z psatz
val rWeakChecker : z nFormula list -> z psatz -> bool
val rnormalise : z formula -> z nFormula cnf
val rnegate : z formula -> z nFormula cnf
val rTautoChecker : z formula bFormula -> rWitness list -> bool
|
