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