author | wenzelm |
Wed, 11 Dec 2013 18:02:22 +0100 | |
changeset 54717 | 42c209a6c225 |
parent 51182 | 962190eab40d |
child 55198 | 7a538e58b64e |
permissions | -rw-r--r-- |
48285 | 1 |
(* Title: HOL/TPTP/MaSh_Eval.thy |
48234 | 2 |
Author: Jasmin Blanchette, TU Muenchen |
3 |
*) |
|
4 |
||
48285 | 5 |
header {* MaSh Evaluation Driver *} |
48234 | 6 |
|
48285 | 7 |
theory MaSh_Eval |
48333 | 8 |
imports Complex_Main |
48234 | 9 |
begin |
10 |
||
48891 | 11 |
ML_file "mash_eval.ML" |
12 |
||
48284 | 13 |
sledgehammer_params |
50519 | 14 |
[provers = spass, max_facts = 32, strict, dont_slice, type_enc = mono_native, |
50925 | 15 |
lam_trans = lifting, timeout = 15, dont_preplay, minimize] |
48284 | 16 |
|
50925 | 17 |
declare [[sledgehammer_instantiate_inducts = false]] |
48236 | 18 |
|
48235 | 19 |
ML {* |
54717 | 20 |
Multithreading.max_threads_value () |
50458
85739c08d126
(re)introduce (even more) aggressive parallelism, for the benefit of those users with dozens of CPU cores
blanchet
parents:
50448
diff
changeset
|
21 |
*} |
85739c08d126
(re)introduce (even more) aggressive parallelism, for the benefit of those users with dozens of CPU cores
blanchet
parents:
50448
diff
changeset
|
22 |
|
85739c08d126
(re)introduce (even more) aggressive parallelism, for the benefit of those users with dozens of CPU cores
blanchet
parents:
50448
diff
changeset
|
23 |
ML {* |
48285 | 24 |
open MaSh_Eval |
48235 | 25 |
*} |
26 |
||
27 |
ML {* |
|
48333 | 28 |
val do_it = false (* switch to "true" to generate the files *) |
48251
6cdcfbddc077
moved most of MaSh exporter code to Sledgehammer
blanchet
parents:
48250
diff
changeset
|
29 |
val params = Sledgehammer_Isar.default_params @{context} [] |
50964
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset
|
30 |
val range = (1, NONE) |
51182
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
50964
diff
changeset
|
31 |
val linearize = false |
50513 | 32 |
val dir = "List" |
33 |
val prefix = "/tmp/" ^ dir ^ "/" |
|
34 |
val prob_dir = prefix ^ "mash_problems" |
|
48235 | 35 |
*} |
36 |
||
37 |
ML {* |
|
48250
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48245
diff
changeset
|
38 |
if do_it then |
50448
0a740d127187
have MaSh evaluator keep all raw problem/solution files in a directory
blanchet
parents:
50437
diff
changeset
|
39 |
Isabelle_System.mkdir (Path.explode prob_dir) |
0a740d127187
have MaSh evaluator keep all raw problem/solution files in a directory
blanchet
parents:
50437
diff
changeset
|
40 |
else |
0a740d127187
have MaSh evaluator keep all raw problem/solution files in a directory
blanchet
parents:
50437
diff
changeset
|
41 |
() |
0a740d127187
have MaSh evaluator keep all raw problem/solution files in a directory
blanchet
parents:
50437
diff
changeset
|
42 |
*} |
0a740d127187
have MaSh evaluator keep all raw problem/solution files in a directory
blanchet
parents:
50437
diff
changeset
|
43 |
|
0a740d127187
have MaSh evaluator keep all raw problem/solution files in a directory
blanchet
parents:
50437
diff
changeset
|
44 |
ML {* |
0a740d127187
have MaSh evaluator keep all raw problem/solution files in a directory
blanchet
parents:
50437
diff
changeset
|
45 |
if do_it then |
51182
962190eab40d
provide two modes for MaSh driver: linearized or real visibility
blanchet
parents:
50964
diff
changeset
|
46 |
evaluate_mash_suggestions @{context} params range linearize |
50953 | 47 |
[MePoN, MaSh_IsarN, MaSh_ProverN, MeSh_IsarN, MeSh_ProverN, IsarN] |
50964
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset
|
48 |
(SOME prob_dir) |
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset
|
49 |
(prefix ^ "mepo_suggestions") |
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset
|
50 |
(prefix ^ "mash_suggestions") |
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset
|
51 |
(prefix ^ "mash_prover_suggestions") |
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset
|
52 |
(prefix ^ "mesh_suggestions") |
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset
|
53 |
(prefix ^ "mesh_prover_suggestions") |
2a990baa09af
use precomputed MaSh/MePo data whenever available
blanchet
parents:
50953
diff
changeset
|
54 |
(prefix ^ "mash_eval") |
48250
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48245
diff
changeset
|
55 |
else |
1065c307fafe
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
blanchet
parents:
48245
diff
changeset
|
56 |
() |
48235 | 57 |
*} |
58 |
||
48234 | 59 |
end |