12 type stature = ATP_Problem_Generate.stature |
12 type stature = ATP_Problem_Generate.stature |
13 type type_enc = ATP_Problem_Generate.type_enc |
13 type type_enc = ATP_Problem_Generate.type_enc |
14 type reconstructor = ATP_Proof_Reconstruct.reconstructor |
14 type reconstructor = ATP_Proof_Reconstruct.reconstructor |
15 type play = ATP_Proof_Reconstruct.play |
15 type play = ATP_Proof_Reconstruct.play |
16 type minimize_command = ATP_Proof_Reconstruct.minimize_command |
16 type minimize_command = ATP_Proof_Reconstruct.minimize_command |
17 type relevance_fudge = Sledgehammer_Filter_Iter.relevance_fudge |
|
18 |
17 |
19 datatype mode = Auto_Try | Try | Normal | Auto_Minimize | Minimize |
18 datatype mode = Auto_Try | Try | Normal | Auto_Minimize | Minimize |
20 |
19 |
21 type params = |
20 type params = |
22 {debug: bool, |
21 {debug: bool, |
37 slice: bool, |
36 slice: bool, |
38 minimize: bool option, |
37 minimize: bool option, |
39 timeout: Time.time, |
38 timeout: Time.time, |
40 preplay_timeout: Time.time, |
39 preplay_timeout: Time.time, |
41 expect: string} |
40 expect: string} |
|
41 |
|
42 type relevance_fudge = |
|
43 {local_const_multiplier : real, |
|
44 worse_irrel_freq : real, |
|
45 higher_order_irrel_weight : real, |
|
46 abs_rel_weight : real, |
|
47 abs_irrel_weight : real, |
|
48 skolem_irrel_weight : real, |
|
49 theory_const_rel_weight : real, |
|
50 theory_const_irrel_weight : real, |
|
51 chained_const_irrel_weight : real, |
|
52 intro_bonus : real, |
|
53 elim_bonus : real, |
|
54 simp_bonus : real, |
|
55 local_bonus : real, |
|
56 assum_bonus : real, |
|
57 chained_bonus : real, |
|
58 max_imperfect : real, |
|
59 max_imperfect_exp : real, |
|
60 threshold_divisor : real, |
|
61 ridiculous_threshold : real} |
42 |
62 |
43 datatype prover_fact = |
63 datatype prover_fact = |
44 Untranslated_Fact of (string * stature) * thm | |
64 Untranslated_Fact of (string * stature) * thm | |
45 SMT_Weighted_Fact of (string * stature) * (int option * thm) |
65 SMT_Weighted_Fact of (string * stature) * (int option * thm) |
46 |
66 |
122 open ATP_Systems |
142 open ATP_Systems |
123 open ATP_Problem_Generate |
143 open ATP_Problem_Generate |
124 open ATP_Proof_Reconstruct |
144 open ATP_Proof_Reconstruct |
125 open Metis_Tactic |
145 open Metis_Tactic |
126 open Sledgehammer_Util |
146 open Sledgehammer_Util |
127 open Sledgehammer_Filter_Iter |
147 |
128 |
148 |
129 (** The Sledgehammer **) |
149 (** The Sledgehammer **) |
130 |
150 |
131 datatype mode = Auto_Try | Try | Normal | Auto_Minimize | Minimize |
151 datatype mode = Auto_Try | Try | Normal | Auto_Minimize | Minimize |
132 |
152 |
279 |
299 |
280 fun kill_provers () = Async_Manager.kill_threads das_tool "prover" |
300 fun kill_provers () = Async_Manager.kill_threads das_tool "prover" |
281 fun running_provers () = Async_Manager.running_threads das_tool "prover" |
301 fun running_provers () = Async_Manager.running_threads das_tool "prover" |
282 val messages = Async_Manager.thread_messages das_tool "prover" |
302 val messages = Async_Manager.thread_messages das_tool "prover" |
283 |
303 |
|
304 |
284 (** problems, results, ATPs, etc. **) |
305 (** problems, results, ATPs, etc. **) |
285 |
306 |
286 type params = |
307 type params = |
287 {debug: bool, |
308 {debug: bool, |
288 verbose: bool, |
309 verbose: bool, |
302 slice: bool, |
323 slice: bool, |
303 minimize: bool option, |
324 minimize: bool option, |
304 timeout: Time.time, |
325 timeout: Time.time, |
305 preplay_timeout: Time.time, |
326 preplay_timeout: Time.time, |
306 expect: string} |
327 expect: string} |
|
328 |
|
329 type relevance_fudge = |
|
330 {local_const_multiplier : real, |
|
331 worse_irrel_freq : real, |
|
332 higher_order_irrel_weight : real, |
|
333 abs_rel_weight : real, |
|
334 abs_irrel_weight : real, |
|
335 skolem_irrel_weight : real, |
|
336 theory_const_rel_weight : real, |
|
337 theory_const_irrel_weight : real, |
|
338 chained_const_irrel_weight : real, |
|
339 intro_bonus : real, |
|
340 elim_bonus : real, |
|
341 simp_bonus : real, |
|
342 local_bonus : real, |
|
343 assum_bonus : real, |
|
344 chained_bonus : real, |
|
345 max_imperfect : real, |
|
346 max_imperfect_exp : real, |
|
347 threshold_divisor : real, |
|
348 ridiculous_threshold : real} |
307 |
349 |
308 datatype prover_fact = |
350 datatype prover_fact = |
309 Untranslated_Fact of (string * stature) * thm | |
351 Untranslated_Fact of (string * stature) * thm | |
310 SMT_Weighted_Fact of (string * stature) * (int option * thm) |
352 SMT_Weighted_Fact of (string * stature) * (int option * thm) |
311 |
353 |