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
|
(**************************************************************************)
(* *)
(* The Alt-Ergo theorem prover *)
(* Copyright (C) 2006-2011 *)
(* *)
(* Sylvain Conchon *)
(* Evelyne Contejean *)
(* *)
(* Francois Bobot *)
(* Mohamed Iguernelala *)
(* Stephane Lescuyer *)
(* Alain Mebsout *)
(* *)
(* CNRS - INRIA - Universite Paris Sud *)
(* *)
(* This file is distributed under the terms of the CeCILL-C licence *)
(* *)
(**************************************************************************)
val fmt : Format.formatter
val file : string ref
val parse_only : bool
val type_only : bool
val stopb : int
val stepsb : int
val age_limite : int
val notriggers : bool
val debug : bool
val debug_cc : bool
val debug_use : bool
val debug_uf : bool
val debug_fm : bool
val debug_sum : bool
val debug_arith : bool
val debug_bitv : bool
val debug_ac : bool
val debug_sat : bool
val debug_sat_simple : bool
val debug_typing : bool
val debug_constr : bool
val debug_pairs : bool
val debug_arrays : bool
val debug_combine : bool
val verbose : bool
val debug_dispatch : bool
val tracefile :string
val smtfile :bool ref
val smt2file :bool ref
val satmode : bool ref
val bjmode : bool
val glouton : bool
val triggers_var : bool
val redondance : int
val astuce : bool
val select : int
val cin : in_channel
val no_rm_eq_existential : bool
val nocontracongru : bool
val omega : bool
val arrays : bool
val pairs : bool
val term_like_pp : bool
val debug_types : bool
val all_models : bool
val smt_arrays : bool
val goal_directed : bool
val bouclage : int
val max_split : Num.num
val rewriting : bool
val proof : bool
val debug_proof : bool
val rules : int
val debug_split : bool
val restricted : bool
|
