src/HOL/TPTP/MaSh_Eval.thy
author wenzelm
Sun Sep 18 20:33:48 2016 +0200 (2016-09-18)
changeset 63915 bab633745c7f
parent 63167 0909deb8059b
child 69597 ff784d5a5bfb
permissions -rw-r--r--
tuned proofs;
blanchet@48285
     1
(*  Title:      HOL/TPTP/MaSh_Eval.thy
blanchet@48234
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@48234
     3
*)
blanchet@48234
     4
wenzelm@63167
     5
section \<open>MaSh Evaluation Driver\<close>
blanchet@48234
     6
blanchet@48285
     7
theory MaSh_Eval
blanchet@58206
     8
imports MaSh_Export_Base
blanchet@48234
     9
begin
blanchet@48234
    10
wenzelm@48891
    11
ML_file "mash_eval.ML"
wenzelm@48891
    12
blanchet@48284
    13
sledgehammer_params
blanchet@57456
    14
  [provers = e, max_facts = 64, strict, dont_slice, type_enc = poly_guards??,
blanchet@57456
    15
   lam_trans = combs, timeout = 30, dont_preplay, minimize]
blanchet@48236
    16
wenzelm@63167
    17
ML \<open>
wenzelm@62925
    18
Multithreading.max_threads ()
wenzelm@63167
    19
\<close>
blanchet@50458
    20
wenzelm@63167
    21
ML \<open>
blanchet@48285
    22
open MaSh_Eval
wenzelm@63167
    23
\<close>
blanchet@48235
    24
wenzelm@63167
    25
ML \<open>
blanchet@55208
    26
val params = Sledgehammer_Commands.default_params @{theory} []
blanchet@50513
    27
val prob_dir = prefix ^ "mash_problems"
wenzelm@63167
    28
\<close>
blanchet@48235
    29
wenzelm@63167
    30
ML \<open>
blanchet@48250
    31
if do_it then
blanchet@50448
    32
  Isabelle_System.mkdir (Path.explode prob_dir)
blanchet@50448
    33
else
blanchet@50448
    34
  ()
wenzelm@63167
    35
\<close>
blanchet@50448
    36
wenzelm@63167
    37
ML \<open>
blanchet@50448
    38
if do_it then
blanchet@57456
    39
  evaluate_mash_suggestions @{context} params range (SOME prob_dir)
blanchet@57456
    40
    [prefix ^ "mepo_suggestions",
blanchet@57456
    41
     prefix ^ "mash_suggestions",
blanchet@57456
    42
     prefix ^ "mash_prover_suggestions",
blanchet@57456
    43
     prefix ^ "mesh_suggestions",
blanchet@57456
    44
     prefix ^ "mesh_prover_suggestions"]
blanchet@57456
    45
    (prefix ^ "mash_eval")
blanchet@48250
    46
else
blanchet@48250
    47
  ()
wenzelm@63167
    48
\<close>
blanchet@48235
    49
blanchet@48234
    50
end