1signature tttSetup =
2sig
3
4  (** Recording **)
5  val ttt_record_flag   : bool ref
6  val ttt_reclet_flag   : bool ref
7  val ttt_recprove_flag : bool ref
8  val ttt_rectac_time   : real ref
9  val ttt_recproof_time : real ref
10  val ttt_printproof_flag : bool ref
11  (* orthogonalization *)
12  val ttt_ortho_flag   : bool ref
13  val ttt_ortho_radius : int ref
14  (* abstraction *)
15  val ttt_noabs_flag     : bool ref
16  val ttt_thmlarg_flag   : bool ref
17  val ttt_thmlarg_radius : int ref
18  val ttt_recgl_flag     : bool ref
19  (* prediction *)
20  val ttt_randdist_flag  : bool ref
21  val ttt_covdist_flag   : bool ref
22
23  (** Generating fof problems *)
24  val ttt_fof_flag : bool ref
25
26  (** Evaluation **)
27  val ttt_eval_flag     : bool ref
28  (* evaluated theorems *)
29  val one_in_option     : (int * int) option ref
30  val one_in_n          : unit -> bool
31  val ttt_evlet_flag    : bool ref
32  val ttt_evprove_flag  : bool ref
33  val evaluation_filter : (string -> bool) ref
34  (* preselection *)
35  val ttt_presel_radius : int ref
36  val ttt_namespacethm_flag : bool ref
37  (* search *)
38  val ttt_mcpol_coeff   : real ref
39  val ttt_mcevnone_flag : bool ref
40  val ttt_mcevtriv_flag : bool ref
41  val ttt_mcev_radius   : int ref
42  val ttt_mcev_coeff    : real ref
43  val ttt_mcev_pint     : int ref
44  val ttt_mcevinit_flag : bool ref
45  val ttt_mcevfail_flag : bool ref
46  (* metis *)
47  val ttt_metis_flag   : bool ref
48  val ttt_metis_time   : real ref
49  val ttt_metis_radius : int ref
50  (* proof presentation *)
51  val ttt_prettify_flag : bool ref
52  val ttt_minimize_flag : bool ref
53  (* eprover *)
54  val ttt_eprover_flag     : bool ref
55  val ttt_eprover_time     : int ref
56  val ttt_eprover_radius   : int ref
57  val ttt_eprover_async    : int ref
58  val eprover_eval_flag : bool ref
59  val eprover_save_flag : bool ref
60  (* term predictions *)
61  val ttt_termarg_flag : bool ref
62  val ttt_termarg_radius : int ref
63  val ttt_termarg_pint : int ref
64  val ttt_selflearn_flag : bool ref
65  (* initialization *)
66  val init_metis      : string -> unit
67
68
69end
70